@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM512.kemMLKEM512 : KEM.KEM

ML-KEM-512 with the FIPS 203 expanded private key.

Equations

• Cryptlib.Primitives.KEM.MLKEM512.kemMLKEM512 = Cryptlib.Primitives.KEM.FIPS203.kem MLKEM.ParameterSet.MLKEM512

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM512.kemMLKEM512Seed : KEM.KEM

ML-KEM-512 with the ek ‖ d ‖ z seed private key.

Equations

• Cryptlib.Primitives.KEM.MLKEM512.kemMLKEM512Seed = Cryptlib.Primitives.KEM.FIPS203.kemSeed MLKEM.ParameterSet.MLKEM512