FIPS203-lean

Executable Lean 4.35 specification of FIPS 203 ML-KEM-1024, ML-KEM-768, and ML-KEM-512. Core Lean only; SHA3/SHAKE imports the Git-pinned FIPS202-lean.

Install Elan, Git and a C compiler. lean-toolchain selects Lean 4.35.0. No Mathlib is needed.

git clone https://github.com/CrocSwap/FIPS203-lean.git
cd FIPS203-lean
lake build
lake exe fips203_tests

The NIST fixtures are included, so running the tests needs no network access. Python 3 is optional for checking or fetching their recorded source files:

python3 scripts/fetch_vectors.py --check

To depend on this package from another Lake project:

[[require]]
name = "fips203"
git = "https://github.com/CrocSwap/FIPS203-lean.git"
rev = "d930e3b9aeebdf4e355806b7e4d900bcbc3d60fb"

Import Fips203 and use keyGen, encaps, and decaps in the Fips203 namespace. For example, Fips203.keyGen .mlkem1024 d z takes two explicit 32-byte seeds; see the result conventions below.

The package compiles and the executable passes 108 NIST ACVP cases: for each parameter set, 3 key generations, 3 encapsulations, 10 decapsulations, 10 encapsulation-key checks, and 10 decapsulation-key checks. ML-KEM-1024 runs first. Decapsulation includes both accepted and implicitly rejected ciphertexts (1024 rejection tcIds 96, 98, 101, 104, 105). Tests compare complete keys and ciphertexts, not their hashes. Arithmetic checks cover NTT inversion, 12-bit encoding, and compression/decompression; malformed lengths are rejected. Building compiles the runner; running it performs the vector checks.

Interface and structure

• Fips203/Arithmetic.lean: byte encoding, exact integer rounding, bit reversal, NTT/inverse NTT and multiplication (Algorithms 3–6, 9–12).
• Fips203/Sampling.lean: SHAKE128 rejection sampling and centered binomial noise (Algorithms 7–8), PRF wrapper.
• Fips203/KPKE.lean: K-PKE key generation/encryption/decryption (13–15).
• Fips203/MLKEM.lean: deterministic _internal functions (16–18), checked keyGen, encaps, decaps wrappers (19–21 and §7 input checks).

ParameterSet only admits the three standardized sets. Bytes are List UInt8, polynomials are length-256 Array Nat with canonical residues modulo 3329; NTT uses ordinary residues, with roots computed from 17 and bit reversal. Internal functions assume the standard's input dimensions. Use the checked wrappers for arbitrary byte inputs. Key generation returns (ek, dk); encapsulation returns (sharedSecret, ciphertext); decapsulation returns only the shared secret, including on implicit rejection. All three internal functions now return Option as well: none uniformly represents sampling exhaustion under Appendix B. The checked wrappers additionally return none on malformed inputs; their public result types are unchanged. A kernel-refinement adapter must distinguish these algorithm results from machine-model failures or proof-fuel exhaustion, and prove the actual native return and cleanup behavior.

Provenance

FIPS202-lean supplies SHA3/SHAKE. lakefile.toml and lake-manifest.json pin a full Git commit from that public repository. Lake checks out that revision into .lake/packages/fips202; a sibling checkout cannot change the dependency.

Standard: FIPS 203, final publication, Algorithms 3–21. Fixtures are unmodified prompt.json and expectedResults.json from NIST ACVP-Server, directories gen-val/json-files/ML-KEM-{keyGen,encapDecap}-FIPS203, commit 975de31eb83d87039ec88934fdc47d8c312b892d. vectors/provenance.json records immutable source URLs and SHA-256 digests. scripts/fetch_vectors.py downloads those exact files and checks their recorded hashes before writing any fixture; --check validates the included copies offline. Tests select the first three keygen/encapsulation cases and all decapsulation/input-check cases in each parameter group. Fixtures describe the FIPS203 revision, not the separate FIPS203-tr1 revision.

Scope and deviations

Randomness is explicit: keyGen p d z, encaps p ek m. No RNG or entropy, side-channel, secure-erasure, or cryptographic-module conformance claims. This is a readable functional specification, not a production crypto library. K-PKE is only a component of the KEM. No Mathlib, sorry, or admit. Sampling uses the standard's Appendix B permitted bound of 280 three-byte iterations (840 SHAKE128 bytes). An exhausted prefix returns a uniform none and never exposes a partial or padded polynomial. sampleNTTLoop recurses structurally on the remaining byte list, so every spec function is total and there is no partial def. This is a bounded execution variant; termination of the original unbounded SHAKE loop is not asserted. Appendix B's 2^-261 exhaustion estimate assumes the distributions stated in the standard; no cryptographic probability proof is claimed here.

Proof progress

Fips203/SamplingLemmas.lean proves that successful samples contain exactly 256 coefficients below q, that success is stable under appending bytes, and that the bounded result depends only on its permitted prefix. ModQ.lean, ModQNeg.lean, Polynomial.lean, BitReverse.lean and NTTConstants.lean provide modular arithmetic, representation invariants, local butterfly inversion, and root/index certificates. NTTLayout.lean, NTTLayers.lean and NTTComposition.lean lift the local butterflies through all seven layers. NTTInverse.lean proves inverseNTT_ntt and ntt_inverseNTT for every length-256 canonical polynomial, and preservation of that representation. The exported transforms use these pointwise layers. The previous imperative loops live in NTTReference.lean; tests compare them on a polynomial, but no general loop-correspondence theorem is claimed. Rounding.lean proves compress_decompress for every permitted compression width and input using integer bounds. All these modules compile. No security proof is claimed.

Native implementations and their constant-time or erasure guarantees are outside this package. Refinement to an unbounded native sampler would need an explicit termination premise as well as agreement on successful bounded results; the Appendix B probability estimate does not prove native termination.

Deferred checks

• Full ACVP suites, including remaining keygen/encapsulation cases.
• Correspondence with the FIPS pseudocode (including the unbounded sampler).
• Optional key-pair consistency procedure of §7.1.
• Errata and future revision review, including FIPS203-tr1 fixtures.
• Native kernels, constant-time behavior, RBG integration and memory erasure.

Builds use -j1 -M1400 and maxHeartbeats=50000 in lakefile.toml. CI uses lean-buildtools to check the actual compiler arguments and monitor memory. The test executable imports the JSON parser/printer and executable KEM modules. Status: compiles; representative vectors pass.

License

Project code is licensed under Apache-2.0. The unmodified NIST ACVP fixtures retain their upstream notice; see NOTICE. Maintained by Mister-Meeseeks in CrocSwap. Passing these fixtures is not NIST certification or cryptographic-module validation.