ML-KEM: fixed-width wire types

VCVio's key and ciphertext types wrapped in subtypes that fix their encoded sizes, so that decode ∘ encode = id holds. The Encoded* fields are ByteArray only up to unfolding, so tBytes/uBytes/vBytes cast them explicitly. Each decode* is split into a plain decode*Val and a well-formedness theorem; proving the round trip under the subtype directly exceeds maxRecDepth.

theorem Cryptlib.Primitives.KEM.FIPS203.secretKeyBytes_eq (ps : MLKEM.ParameterSet) : (params ps).secretKeyBytes = 384 * (params ps).k + (384 * (params ps).k + (32 + (32 + 32)))

theorem Cryptlib.Primitives.KEM.FIPS203.ciphertextBytes_eq (ps : MLKEM.ParameterSet) : (params ps).ciphertextBytes = 32 * (params ps).du * (params ps).k + 32 * (params ps).dv

def Cryptlib.Primitives.KEM.FIPS203.tBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedTHat) : ByteArray

x : encoding.EncodedTHat, as a plain ByteArray.

Equations

• Cryptlib.Primitives.KEM.FIPS203.tBytes ps x = cast ⋯ x

def Cryptlib.Primitives.KEM.FIPS203.bytesT (ps : MLKEM.ParameterSet) (x : ByteArray) : (encoding ps).EncodedTHat

The reverse of tBytes.

Equations

• Cryptlib.Primitives.KEM.FIPS203.bytesT ps x = cast ⋯ x

theorem Cryptlib.Primitives.KEM.FIPS203.tBytes_bytesT (ps : MLKEM.ParameterSet) (x : ByteArray) : tBytes ps (bytesT ps x) = x

theorem Cryptlib.Primitives.KEM.FIPS203.bytesT_tBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedTHat) : bytesT ps (tBytes ps x) = x

def Cryptlib.Primitives.KEM.FIPS203.uBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedU) : ByteArray

x : encoding.EncodedU, as a plain ByteArray.

Equations

• Cryptlib.Primitives.KEM.FIPS203.uBytes ps x = cast ⋯ x

def Cryptlib.Primitives.KEM.FIPS203.bytesU (ps : MLKEM.ParameterSet) (x : ByteArray) : (encoding ps).EncodedU

Equations

• Cryptlib.Primitives.KEM.FIPS203.bytesU ps x = cast ⋯ x

theorem Cryptlib.Primitives.KEM.FIPS203.uBytes_bytesU (ps : MLKEM.ParameterSet) (x : ByteArray) : uBytes ps (bytesU ps x) = x

theorem Cryptlib.Primitives.KEM.FIPS203.bytesU_uBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedU) : bytesU ps (uBytes ps x) = x

def Cryptlib.Primitives.KEM.FIPS203.vBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedV) : ByteArray

x : encoding.EncodedV, as a plain ByteArray.

Equations

• Cryptlib.Primitives.KEM.FIPS203.vBytes ps x = cast ⋯ x

def Cryptlib.Primitives.KEM.FIPS203.bytesV (ps : MLKEM.ParameterSet) (x : ByteArray) : (encoding ps).EncodedV

Equations

• Cryptlib.Primitives.KEM.FIPS203.bytesV ps x = cast ⋯ x

theorem Cryptlib.Primitives.KEM.FIPS203.vBytes_bytesV (ps : MLKEM.ParameterSet) (x : ByteArray) : vBytes ps (bytesV ps x) = x

theorem Cryptlib.Primitives.KEM.FIPS203.bytesV_vBytes (ps : MLKEM.ParameterSet) (x : (encoding ps).EncodedV) : bytesV ps (vBytes ps x) = x

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.PublicKey (ps : MLKEM.ParameterSet) : Type

An encapsulation key whose tHatEncoded is 384 * k bytes.

Equations

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

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.PrivateKey (ps : MLKEM.ParameterSet) : Type

A decapsulation key whose two encoded polynomial vectors are 384 * k bytes each.

Equations

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

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.FIPS203.CT (ps : MLKEM.ParameterSet) : Type

A ciphertext whose uEncoded/vEncoded are 32 * du * k/32 * dv bytes.

Equations

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

PublicKey

def Cryptlib.Primitives.KEM.FIPS203.encodePublicKey (ps : MLKEM.ParameterSet) (pk : PublicKey ps) : Vector UInt8 (params ps).publicKeyBytes

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decodePublicKey (ps : MLKEM.ParameterSet) (v : Vector UInt8 (params ps).publicKeyBytes) : Option (PublicKey ps)

Equations

• Cryptlib.Primitives.KEM.FIPS203.decodePublicKey ps v = some ⟨Cryptlib.Primitives.KEM.FIPS203.decodePublicKeyVal✝ ps v, ⋯⟩

theorem Cryptlib.Primitives.KEM.FIPS203.decode_encode_pub (ps : MLKEM.ParameterSet) (pk : PublicKey ps) : decodePublicKey ps (encodePublicKey ps pk) = some pk

PrivateKey

def Cryptlib.Primitives.KEM.FIPS203.encodePrivateKey (ps : MLKEM.ParameterSet) (sk : PrivateKey ps) : Vector UInt8 (params ps).secretKeyBytes

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decodePrivateKey (ps : MLKEM.ParameterSet) (v : Vector UInt8 (params ps).secretKeyBytes) : Option (PrivateKey ps)

Equations

• Cryptlib.Primitives.KEM.FIPS203.decodePrivateKey ps v = some ⟨Cryptlib.Primitives.KEM.FIPS203.decodePrivateKeyVal✝ ps v, ⋯⟩

theorem Cryptlib.Primitives.KEM.FIPS203.decode_encode_priv (ps : MLKEM.ParameterSet) (sk : PrivateKey ps) : decodePrivateKey ps (encodePrivateKey ps sk) = some sk

CT (ciphertext)

def Cryptlib.Primitives.KEM.FIPS203.encodeCiphertext (ps : MLKEM.ParameterSet) (c : CT ps) : Vector UInt8 (params ps).ciphertextBytes

Equations

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

def Cryptlib.Primitives.KEM.FIPS203.decodeCiphertext (ps : MLKEM.ParameterSet) (v : Vector UInt8 (params ps).ciphertextBytes) : Option (CT ps)

Equations

• Cryptlib.Primitives.KEM.FIPS203.decodeCiphertext ps v = some ⟨Cryptlib.Primitives.KEM.FIPS203.decodeCiphertextVal✝ ps v, ⋯⟩

theorem Cryptlib.Primitives.KEM.FIPS203.decode_encode_ct (ps : MLKEM.ParameterSet) (c : CT ps) : decodeCiphertext ps (encodeCiphertext ps c) = some c