Specs for ML-KEM by abentkamp · Pull Request #1480 · celabshq/libcrux

abentkamp · 2026-06-16T10:50:09Z

This PR adds a hacspec-style reference implementation for ML-KEM. It includes cross-tests with the actual ML-KEM implementation, an F* and a Lean extraction. The PR builds on top of the SHA3-spec PR #1399.

The PR is structured into four clean commits:

just the spec
cross-spec tests
F*
Lean

This is the basis for the Lean verification of ML-KEM in libcrux-iot.

jschneider-bensch

Leaving some comments already before the rest of the review.

jschneider-bensch

I've left more comments, mostly around documentation and naming of functions. Is renaming a function okay in terms of updating the proofs, would you say?

The other set of suggestions concern the use of FieldElement and its operations, where we could use the Rust type system more effectively to maintain the boundedness invariant, instead of mixing up the type's own operations with direct field accesses and allowing construction of the type independent of its new method.
I think some of the documentation issues are inherited from the impl, where some documentation has outdated references that refer to the initial public draft of FIPS203, instead of the final version. While the documentation deviated from the published standard in some ways I found no issues with the implementation code.
Can you add test vector testing for the spec here, using libcrux-kats, so we have the same test vector coverage here as on the impl side?

jschneider-bensch · 2026-06-24T14:37:36Z

These changes cause a rustfmt error.

jschneider-bensch · 2026-06-24T14:42:59Z

This file does not need to be changed at all.

jschneider-bensch · 2026-06-25T06:39:50Z

+/// Output: encryption key ekₚₖₑ ∈ 𝔹^{384k+32}.
+/// Output: decryption key dkₚₖₑ ∈ 𝔹^{384k}.
+///
+/// d ←$ B


This is the key_generation_seed and is not sampled internally, but is an input.

Suggested change

/// d ←$ B

Input: randomness d ∈ 𝔹^{32}

jschneider-bensch · 2026-06-25T06:40:51Z

+/// Output: decryption key dkₚₖₑ ∈ 𝔹^{384k}.
+///
+/// d ←$ B
+/// (ρ,σ) ← G(d)


The rank is part of the input to G here.

Suggested change

/// (ρ,σ) ← G(d)

/// (ρ,σ) ← G(d‖k)

jschneider-bensch · 2026-06-25T06:48:06Z

+/// N ← 0
+/// for (i ← 0; i < k; i++)
+///     for(j ← 0; j < k; j++)
+///         Â[i,j] ← SampleNTT(XOF(ρ, j, i))


This line deviates from the presentation in the standard.

Suggested change

/// Â[i,j] ← SampleNTT(XOF(ρ, j, i))

/// Â[i,j] ← SampleNTT(ρ‖j‖i)

While the current state is what actually happens at the beginning of SampleNTT, I prefer the presentation of the standard since it makes clear how (in particular in which order) the function arguments are to be combined to one input for SampleNTT.

jschneider-bensch · 2026-06-25T08:37:15Z

+
+#[hax_lib::attributes]
+impl FieldElement {
+    #[hax_lib::requires(val < FIELD_MODULUS)]


Why enforce this with a pre-condition here, instead of doing the reduction % FIELD_MODULUS in the constructor for FieldElement? The bound could be post-condition instead and making the val field private instead of pub would ensure that no out-of-bounds field element can be created in the Rust domain already as long as the operations preserve this too.

jschneider-bensch · 2026-06-25T08:43:59Z

+/// `deserialize_then_decompress_u` function (which fuses the NTT into
+/// the per-element decompress loop).
+#[hax_lib::requires(RANK <= 4 && (du == 10 || du == 11) && ciphertext.len() == (RANK * COEFFICIENTS_IN_RING_ELEMENT * du) / 8)]
+pub fn deserialize_then_decompress_u_then_ntt<const RANK: usize>(


It looks like this function is not used in ind_cpa::decrypt_unpacked?

jschneider-bensch · 2026-06-25T08:49:23Z

+    let ek: [u8; EK_SIZE] = serialize_public_key::<RANK, EK_SIZE>(&t_as_ntt, &seed_for_A);
+    let public_key_hash: [u8; 32] = H(&ek);
+
+    let mut implicit_rejection_value = [0u8; 32];


This seems unnecessary, since z is already a reference to a [u8;32] and could be cloned below instead.

jschneider-bensch · 2026-06-25T08:56:35Z

Can you add a section on the F* extraction as well? I think there is no script to drive it and it's not clear what it should prove.

jschneider-bensch · 2026-06-25T08:58:02Z

+
+## Extraction via HAX
+
+### Lean


Is there anything that is proven in lean about this spec on its own, or is the extraction just used for the functional correctness proof of the impl?

abentkamp force-pushed the alex/mlkem-specs branch 5 times, most recently from 3bb7365 to fcefc79 Compare June 16, 2026 15:23

abentkamp marked this pull request as ready for review June 16, 2026 15:25

abentkamp requested a review from a team as a code owner June 16, 2026 15:25

abentkamp requested review from franziskuskiefer, jschneider-bensch and robinhundt and removed request for a team and franziskuskiefer June 16, 2026 15:25

abentkamp force-pushed the alex/mlkem-specs branch from fcefc79 to ba4350d Compare June 17, 2026 09:09

claude added 4 commits June 17, 2026 09:14

[ml-kem] Add hacspec ML-KEM specification and internal tests

aa90910

[ml-kem] Add cross-spec equivalence tests against the implementation

99c9938

[ml-kem] Add F* extraction of the spec

52a6b05

[ml-kem] Add aeneas-Lean extraction of the spec

a4cfb1e

abentkamp force-pushed the alex/mlkem-specs branch from ba4350d to a4cfb1e Compare June 17, 2026 09:31

abentkamp mentioned this pull request Jun 17, 2026

[MLKEM] Part 1: Cross-spec tests celabshq/libcrux-iot#170

Open

Base automatically changed from sha3-spec-upstream to main June 22, 2026 11:53

jschneider-bensch mentioned this pull request Jun 23, 2026

Specs for ML-DSA #1488

Open

jschneider-bensch reviewed Jun 23, 2026

View reviewed changes

Comment thread CHANGELOG.md

Comment thread specs/sha3/hax_aeneas.py

Comment thread specs/ml-kem/src/ind_cca.rs

Comment thread specs/ml-kem/src/ind_cca.rs

Comment thread specs/ml-kem/src/ind_cca.rs

Comment thread specs/ml-kem/src/ind_cca.rs

Comment thread specs/ml-kem/src/ind_cca.rs

abentkamp added 5 commits June 23, 2026 16:55

[mlkem] remove changelog entries

c6bcf1a

Merge remote-tracking branch 'origin/main' into alex/mlkem-specs

343c456

[sha3] update Readme to new hax-evit version

8fcb983

[mlkem] Add ML-KEM Readme

7c82219

[mlkem] fix cargo fmt

6330a8c

jschneider-bensch requested changes Jun 25, 2026

View reviewed changes

	/// Â[i,j] ← SampleNTT(XOF(ρ, j, i))
	/// Â[i,j] ← SampleNTT(ρ‖j‖i)

Uh oh!

Conversation

abentkamp commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jschneider-bensch left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jschneider-bensch left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

abentkamp commented Jun 16, 2026 •

edited

Loading