Hedged ML-KEM-512

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.encaps512Hedged (ek : MLKEM.EncapsulationKey (FIPS203.params MLKEM.ParameterSet.MLKEM512) (FIPS203.encoding MLKEM.ParameterSet.MLKEM512)) (m : MLKEM.Message) : MLKEM.SharedSecret × MLKEM.Ciphertext (FIPS203.params MLKEM.ParameterSet.MLKEM512) (FIPS203.encoding MLKEM.ParameterSet.MLKEM512)

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.encaps512Hedged = Cryptlib.Primitives.KEM.MLKEMHedged.encapsHedged MLKEM.ParameterSet.MLKEM512

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged512 : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged512 = Cryptlib.Primitives.KEM.MLKEMHedged.kem MLKEM.ParameterSet.MLKEM512

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged512Seed : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged512Seed = Cryptlib.Primitives.KEM.MLKEMHedged.kemSeed MLKEM.ParameterSet.MLKEM512