[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
robinhundt
reviewed
Jun 30, 2026
robinhundt
left a comment
robinhundt
left a comment
Contributor
There was a problem hiding this comment.
Thanks for the PR! I have some questions regarding the top-level theorems that I'd like to resolve before we merge this. I've only looked in detail at the compute_As_plus_e_fc theorem, but I think my comment also applies to the other top-level theorems.
Comment on lines
+3883
to
+3886
| ⦃ ⇓ p => ⌜ hacspec_ml_kem.matrix.compute_As_plus_e | ||
| (lift_matrix_from_slice matrix_A K) | ||
| (lift_vec s_as_ntt) (lift_vec error_as_ntt) | ||
| = .ok (lift_vec p.1) ⌝ ⦄ := by |
Contributor
There was a problem hiding this comment.
If I understand correctly, this only proves that the output of the spec and impl is equal after applying the lift functions to the inputs of the spec and the output of the impl. My concerns with this are:
- To understand whether this theorem actually captures what we want (equivalence of the implementation), you have to also understand the lift function.
- I could imagine degenerate lift functions that just map every input to 0, making the equivalence proof easier, but not actually proving what we want.
- The lift functions reduce their inputs modulo
Q. Therefore, if the impl returned a value ofQ + 100but the spec returned100, the equivalence would still hold although the spec and impl disagree.
Could the theorem also prove that the output of the impl is in [0, q) and then use that to state that the actual values of the impl output and spec output are equivalent? (Modulo casting between i16 and u16).
This would strengthen what the theorem proves (which might anyway be needed for proofs of higher-level parts of ML-KEM down the line) and reduce the necessity to understand lift for assessing how the outputs are compared.
I think lifting would still be necessary for the inputs, so it would be beneficial if these were simplified and made more explicit, with some helper theorems that can be audited to increase the confidence in lift behaving as expected. Here is a suggestion by claude for how this could be achieved:
Claude suggestion
You can't drop the input lift (Technique 1's lift_vec on inputs remains), but you can make the reviewer trust it from short auditable lemmas rather than its definition. Two properties suffice:- Faithfulness / characterization — already essentially present in this repo as zmodOfFE_feOfZMod (Spec.lean:93). The analogue you'd want is:
theorem lift_fe_spec (x : Std.I16) : zmodOfFE (lift_fe x) = (x.val : ZMod 3329) - Reading just this statement tells you "lifting an input then projecting back gives exactly the i16 taken mod q" — i.e. the bridge is the intended reduction, full stop.
- Injectivity (up to mod q) — rules out the vacuity worry you raised in the first place. If lift x = lift y → x ≡ y (mod q) is a stated lemma, a collapsing/constant lift is
impossible by a checkable fact, not by inspecting code.
This converts "read and understand the lift tower" into "read three theorem statements." That's the realistic best case while keeping the current theorem strength.
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
3 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.