ML-KEM primitives, for every FIPS 203 parameter set

VCVio's pure-Lean NTT, encoding and CBD, with SHA-3/SHAKE from the pure-Lean Keccak sponge in HashSig.SLHDSA.Concrete.Keccak in place of VCVio's FFI hash bindings.

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.vectorToByteArray {n : ℕ} (v : Vector UInt8 n) : ByteArray

Equations

• Cryptlib.Primitives.KEM.FIPS203.vectorToByteArray v = Cryptlib.Util.Bytes.ofVector v

def Cryptlib.Primitives.KEM.FIPS203.byteArrayToVector (ba : ByteArray) (offset n : ℕ) : Vector UInt8 n

n bytes of ba from offset.

Equations

• Cryptlib.Primitives.KEM.FIPS203.byteArrayToVector ba offset n = Vector.ofFn fun (x : Fin n) => match x with | ⟨i, isLt⟩ => ba.get! (offset + i)

SampleNTT (FIPS 203 Algorithm 7): rejection sampling from SHAKE-128

def Cryptlib.Primitives.KEM.FIPS203.rejectionSample (stream : ByteArray) : Array MLKEM.Coeff

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.KEM.FIPS203.requireFullRejectionSample (coeffs : Array MLKEM.Coeff) : Array MLKEM.Coeff

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.KEM.FIPS203.concreteSampleNTT (rho : MLKEM.Seed32) (j i : ℕ) : MLKEM.Tq

Equations

• One or more equations did not get rendered due to their size.

PRF + CBD (FIPS 203 Algorithms 6 + 8), and the two hash wrappers

def Cryptlib.Primitives.KEM.FIPS203.prfCBD (eta : ℕ) (sigma : MLKEM.Seed32) (n : ℕ) : MLKEM.Rq

PRF_η(σ, N) = SHAKE-256(σ ‖ N, 64η) followed by CBD_η.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.KEM.FIPS203.hashG (input : ByteArray) : MLKEM.Seed32 × MLKEM.Seed32

G(input) = SHA3-512(input), split into two 32-byte halves.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.KEM.FIPS203.hashH (input : ByteArray) : Vector UInt8 32

H(input) = SHA3-256(input) as a 32-byte vector.

Equations

• Cryptlib.Primitives.KEM.FIPS203.hashH input = Cryptlib.Primitives.KEM.FIPS203.byteArrayToVector (SLHDSA.Concrete.Keccak.sha3_256 input) 0 32

A faster byteEncodeVec

VCVio's byteEncodeVec computes each output byte by encoding that byte's whole polynomial again, so encoding u re-encodes each polynomial 32·d_u times; it was nearly all of encapsulation's time. This version encodes each polynomial once and reads the bytes from that.

def Cryptlib.Primitives.KEM.FIPS203.byteEncodeVecFast (d : ℕ) {k : ℕ} (v : MLKEM.RqVec k) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Primitives.KEM.FIPS203.byteEncodeVecFast_eq (d : ℕ) {k : ℕ} (v : MLKEM.RqVec k) : byteEncodeVecFast d v = MLKEM.Concrete.byteEncodeVec d v

Primitives instance per parameter set

def Cryptlib.Primitives.KEM.FIPS203.concretePrimitives (params : MLKEM.Params) (encoding : MLKEM.Encoding params) (hEnc : encoding.EncodedTHat = ByteArray) (hU : encoding.EncodedU = ByteArray) (hV : encoding.EncodedV = ByteArray) : MLKEM.Primitives params encoding

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.params (ps : MLKEM.ParameterSet) : MLKEM.Params

The FIPS 203 parameters of ps.

Equations

• Cryptlib.Primitives.KEM.FIPS203.params ps = ps.params

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.encoding (ps : MLKEM.ParameterSet) : MLKEM.Encoding (params ps)

VCVio's pure-Lean Concrete.Encoding, with byteEncodeVecFast for byteEncodeDUVec.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Primitives.KEM.FIPS203.encoding_eq (ps : MLKEM.ParameterSet) : encoding ps = MLKEM.Concrete.concreteEncoding (params ps)

theorem Cryptlib.Primitives.KEM.FIPS203.encodingLaws (ps : MLKEM.ParameterSet) : (encoding ps).Laws

Encoding round-trip laws, from VCVio's via encoding_eq.

theorem Cryptlib.Primitives.KEM.FIPS203.encoding_byteEncodeDUVec_size (ps : MLKEM.ParameterSet) (u : MLKEM.RqVec (params ps).k) : ByteArray.size ((encoding ps).byteEncodeDUVec u) = 32 * (params ps).du * (params ps).k

def Cryptlib.Primitives.KEM.FIPS203.primitives (ps : MLKEM.ParameterSet) : MLKEM.Primitives (params ps) (encoding ps)

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Primitives.KEM.FIPS203.hEncEq (ps : MLKEM.ParameterSet) : (encoding ps).EncodedTHat = ByteArray

The encoded types are ByteArray; typeclass search does not see this without these casts.

theorem Cryptlib.Primitives.KEM.FIPS203.hUEq (ps : MLKEM.ParameterSet) : (encoding ps).EncodedU = ByteArray

theorem Cryptlib.Primitives.KEM.FIPS203.hVEq (ps : MLKEM.ParameterSet) : (encoding ps).EncodedV = ByteArray

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.ring : MLKEM.NTTRingOps

VCVio's NTT ring operations.

Equations

• Cryptlib.Primitives.KEM.FIPS203.ring = MLKEM.Concrete.concreteNTTRingOps