[ML-KEM] Part 3: Lean Verification#171
Open
abentkamp wants to merge 8 commits into
Open
Conversation
LibcruxIotMlKem/
Extraction/{Funs,Missing}.lean [unchanged]
Util/{CreateI,LoopSpecs,SliceSpecs}.lean [generic Aeneas glue]
Spec.lean
Spec/{Pure,Commute,StateIso,AlgEquiv,
ModularArith,Montgomery,NumericKeystones}.lean
Vector/Portable/Ntt.lean (was Equivalence/L2_NTTSteps)
Vector/Portable/Arithmetic/
{PerElement,Element,LoopHelper,BvMasks}.lean (was Equivalence/L0,L1 +
Util/PortableVector +
Util/BvMasks)
Polynomial/
NttDrivers.lean (was Equivalence/L3_NTTDrivers)
PolyOps.lean (was Equivalence/L6_PolyOps)
Sampling.lean (was BitMlKem/L7/Axioms §A1)
Serialize.lean (was BitMlKem/L7/Axioms §A2)
Matrix/Common.lean (was BitMlKem/L7/Common)
Matrix/ComputeMessage/{Impl,Correctness,
Bridges,FC}.lean (was BitMlKem/L7/{Impl,Correctness,FC}/
ComputeMessage)
Matrix/ComputeVectorU/{Impl,Correctness,FC}.lean
Matrix/ComputeRingElementV/{Impl,Correctness,FC}.lean
FCTargets.lean (was BitMlKem/FCTargets)
Removed:
BitMlKem/L7/Tests/* (numeric SEAM `#guard`
validations, not load-bearing)
BitMlKem/, Equivalence/ (now empty)
Layer-M / Mathlib-isolation prose dropped from Spec.lean, Spec/StateIso.lean,
Spec/AlgEquiv.lean, Vector/Portable/Arithmetic/{PerElement,BvMasks}.lean
— any file can `import Mathlib` directly.
Internal split of FCTargets.lean (33k LOC, §L0–L6 + §L3i + §L2.8/L6.3 +
§L7.1 + §L7-prep) into impl-mirrored sub-files is deferred to a
follow-up; the file currently retains the full FC ladder.
Namespaces unchanged (still libcrux_iot_ml_kem.BitMlKem.{FCTargets,L7,...}
internally) so the move is purely directory-level. Build green (1758
jobs, 0 errors) on the local-Hax setup.
Bottom-up dependency order:
Spec/Lift.lean (§0 lift tower + §0.5 _pure aliases)
Vector/Portable/Arithmetic/PerElement.lean (+ §L0 FC theorems)
Vector/Portable/Arithmetic/Element.lean (+ §L1 FC theorems)
Vector/Portable/Ntt.lean (+ §L2 FC theorems)
Polynomial/NttDrivers.lean (unchanged)
Polynomial/PolyOps.lean (unchanged)
Ntt.lean (§L3 forward NTT FC)
Polynomial/PolyOpsFcBarrett.lean (§L6.1 poly_barrett_reduce_fc)
InvertNtt.lean (§L3i inverse NTT FC)
Polynomial/PolyOpsFc.lean (§L6.{2,4,5,6,7})
Matrix/Common.lean (+ §L6.8 matrix.entry FC)
Polynomial/NttMultiply.lean (§L2.8 + §L6.3 NTT-multiply)
Matrix/ComputeAsPlusE.lean (§L7-prep + §L7.1 + §L7 docs)
The PolyOpsFc → PolyOpsFcBarrett split sidesteps a cycle:
`InvertNtt` (§L3i) calls `poly_barrett_reduce_fc` from §L6.1; the
remaining §L6.{2-7} body has no inverse-NTT dependency, so it can
sit downstream of `InvertNtt`.
Cross-section `private` helpers (e.g. `triple_of_ok_fc`,
`triple_exists_ok_fc`, `usize_*_ok_eq_fc`) were file-scoped in the
monolith; with the split they're made public so downstream sections
can still call them.
Build green (1764 jobs, 0 errors) on the local-Hax setup.
Each file now owns a namespace matching its path under
`libcrux_iot_ml_kem.<...>` (PascalCase, distinct from the lowercase
impl-side namespaces). The historical `libcrux_iot_ml_kem.BitMlKem.*`,
`libcrux_iot_ml_kem.Equivalence.*`, and aggregated `libcrux_iot_ml_kem.Util.*`
namespaces — relics of the old monolithic layout — are gone.
Highlights:
- `BitMlKem` -> `Spec` for Spec.lean; sibling Spec/* files get
`Spec.{AlgEquiv,Commute,Lift,ModularArith,Montgomery,NumericKeystones,Pure,StateIso}`.
- `BitMlKem.FCTargets` (cross-file aggregate) split per file:
`Spec.Lift`, `Ntt`, `InvertNtt`, `Polynomial.{PolyOpsFcBarrett,PolyOpsFc,NttMultiply}`,
`Serialize`, `Sampling`, `Matrix.{Common,ComputeAsPlusE}`,
`Vector.Portable.{Arithmetic.{PerElement,Element},Ntt}`.
- `BitMlKem.L7` -> per-file `Matrix.Common`, `Matrix.{ComputeMessage,ComputeRingElementV,ComputeVectorU}.{Impl,Correctness,FC,Bridges}`.
- `Equivalence` -> per-file `Polynomial.{NttDrivers,PolyOps}` and
`Vector.Portable.{Arithmetic.{PerElement,Element},Ntt}`.
- `Util` (aggregate of utilities) -> per-file `Util.{CreateI,LoopSpecs,SliceSpecs}`,
`Spec.{ModularArith,Montgomery,NumericKeystones}`, and
`Vector.Portable.Arithmetic.{BvMasks,LoopHelper}`.
Each block injects an `open` clause for the sibling new namespaces that
the old shared-namespace lookup made automatic; cross-file qualified
references (~890 of them) are mechanically remapped via the
decl-ownership map. The unused `Spec.lean` aliases `lift_poly_plain` /
`lift_poly_mont` are dropped — they would have collided with `Spec.Lift`'s
real `lift_poly_mont` def.
Build: `lake build LibcruxIotMlKem` — 1764 jobs, green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01B9N79V94LeHU5pUFtoShCe
…ADME Replaces the cryptic FC-layer codes (L1_5, L3_4_plus_inner_FC, L7_4_FC, ...) with names that match the function or layer each block handles: L1_5 -> CondSubtract3329 L1_5_FC -> CondSubtract3329FC L3_1..L3_3 -> Layer1..Layer3 (NttDrivers.lean) L3_1_B..L3_3_B -> Layer1Bounded..Layer3Bounded L3_5 -> Layer7 L3_4_Inner -> Layer4PlusInner L3_4_Outer -> Layer4PlusOuter L3_1_FC..L3_7_FC, L3_4_plus_*_FC -> Layer1FC..Layer4PlusOuterFC (Ntt.lean) L3i_*_FC -> Layer*FC (InvertNtt.lean) L6_1 -> BarrettReduce (PolyOps.lean) L6_1_FC -> BarrettReduceFC (PolyOpsFcBarrett.lean) L6_2_FC -> ReducingFromI32ArrayFC L6_4_FC..L6_7_FC -> AddErrorReduceFC..SubtractReduceFC L6_3_FC/L6_3b_FC/L6_3c_fill_FC -> UseCacheFC/HelpersFC/FillCacheFC L7_1a_FC..L7_1d_FC -> Stage1FillCacheFC..Stage4MatrixAddFC L7_2a_FC..L7_2c_FC -> Row0FillFC..AllRowsFillFC L7_3_FC -> ChunkLoopFC L7_4_FC -> S1LoopFC Same-name pairs in distinct files (e.g., `Layer1FC` in both `Ntt.lean` and `InvertNtt.lean`) coexist via their parent namespaces. `ChunkLoopFC` and `S1LoopFC` are intentionally distinct because `ComputeRingElementV.Impl`, `ComputeVectorU.Impl`, and `ComputeMessage.Impl` cross-reference each other's loop invariants. README is refreshed to use the new fully-qualified theorem names and the new file paths. Build: `lake build LibcruxIotMlKem` — 1764 jobs, green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01B9N79V94LeHU5pUFtoShCe
Across `Matrix/ComputeMessage/`, `Matrix/ComputeRingElementV/`, and `Matrix/ComputeVectorU/`, the file that holds the pure-Lean ↔ hacspec equational bridges is renamed from `Correctness.lean` to `Hacspec.lean`. The new name reflects what the file actually does: each L7.x trio already has `Impl.lean` (impl ↔ pure-Lean spec) and `FC.lean` (final glue) — the third file is the spec-side bridge to hacspec, so it should be called `Hacspec` for symmetry with the other two roles. Namespace `libcrux_iot_ml_kem.Matrix.<Compute>.Correctness` is renamed to `libcrux_iot_ml_kem.Matrix.<Compute>.Hacspec` everywhere; all imports and `open` clauses follow. Doc-string references are swept too. Build: `lake build LibcruxIotMlKem` — 1764 jobs, green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01B9N79V94LeHU5pUFtoShCe
The forward-NTT FC theorem was a leftover in `InvertNtt.lean` from the
original FCTargets split; move it to `Ntt.lean` so the file placement
matches its role.
Untangling the dep cycle required moving two lift-poly helpers
(`chunk_at_lift_poly_fc`, `flatten_chunks_eq_lift_poly_fc`) from
`Ntt.lean` to `Vector/Portable/Ntt.lean` — they only depend on
`Spec.Lift` and `LoopHelper`, so the new home is more natural anyway.
With those out of `Ntt`, `Polynomial/PolyOpsFcBarrett.lean` no longer
needs to import `Ntt`, which lets `Ntt.lean` now import `PolyOpsFcBarrett`
(for `poly_barrett_reduce_fc`). The new import chain:
Spec.Lift -> Vector.Portable.Ntt -> Polynomial.NttDrivers
-> Polynomial.PolyOpsFcBarrett -> Ntt -> Polynomial.PolyOpsFc -> InvertNtt
README updated to point `ntt_binomially_sampled_ring_element_fc` at
`Ntt.lean` with the new qualified name.
Build: `lake build LibcruxIotMlKem` — 1764 jobs, green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01B9N79V94LeHU5pUFtoShCe
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains the Lean Verification of ML-KEM.