MlKem.lean🔗

Tier 2 · definitions used by the computational proof and symbolic proof 6 headline theorems depend on it 30 of 86 lines trusted trust banner B2, trusted: definitions used by the statement source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

SPQR V1: libcrux ML-KEM-768 incremental API (MlKem)

Trusted: definitions used by the statement.

Models the incremental ML-KEM-768 entry points of libcrux_ml_kem::mlkem768::incremental (called via extern stubs in Hooks.lean) as a record MlKem of uninterpreted functions (keyPair, encaps1, encaps2, decaps, validPk), with slice projections MlKem.fromSeed (pk1Off, pk2Off) and length-checked public-key validation MlKem.validPkBytes. No correctness or security property is built into MlKem; correctness enters only as explicit hypotheses in MlKemCorrect.lean and KemFailFind.lean.

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

abbrev BytesL31 ↗#

abbrev Bytes := List (BitVec 8)

abbrev pk1OffL33–34 ↗#

Byte offset of pk1 (hdr, 64 bytes) inside 2400-byte KeyPairCompressedBytes (2304..2368).

abbrev pk1Off : Nat := 2304

abbrev pk2OffL36–37 ↗#

Byte offset of pk2 (ek, 1152 bytes) inside 2400-byte KeyPairCompressedBytes (1152..2304).

abbrev pk2Off : Nat := 1152

structure MlKemL39–52 ↗#

Uninterpreted incremental ML-KEM-768 interface (spqr/src/incremental_mlkem768.rs:28–171):

keyPair: 2400-byte compressed keypair from a 64-byte seed (from_seed);
encaps1: first encapsulation step (hdr, rand) ↦ Option (ct1, es, ss) (none on Err);
encaps2: second encapsulation step (es, ek) ↦ ct2;
decaps: compressed-key decapsulation (dk, ct1, ct2) ↦ ss;
validPk: encapsulation-key check on 64-byte hdr and 1152-byte ek.

structure MlKem where
  keyPair : List.Vector (BitVec 8) 64 → List.Vector (BitVec 8) 2400
  encaps1 : Bytes → List.Vector (BitVec 8) 32 →
    Option (List.Vector (BitVec 8) 960 × List.Vector (BitVec 8) 2080 × List.Vector (BitVec 8) 32)
  encaps2 : List.Vector (BitVec 8) 2080 → List.Vector (BitVec 8) 1152 → List.Vector (BitVec 8) 128
  decaps : List.Vector (BitVec 8) 2400 → List.Vector (BitVec 8) 960 → List.Vector (BitVec 8) 128 →
    List.Vector (BitVec 8) 32
  validPk : Bytes → Bytes → Bool

def MlKem.fromSeedL54–60 ↗#

Splits kp = K.keyPair seed into (hdr, ek, dk) at pk1Off (2304..2368) and pk2Off (1152..2304), with dk = kp.

@[irreducible] def MlKem.fromSeed (K : MlKem) (seed : List.Vector (BitVec 8) 64) :
    List.Vector (BitVec 8) 64 × List.Vector (BitVec 8) 1152 × List.Vector (BitVec 8) 2400 :=
  (⟨((K.keyPair seed).toList.drop pk1Off).take 64, byK:MlKemseed:List.Vector (BitVec 8) 64⊢ (List.take 64 (List.drop pk1Off (K.keyPair seed).toList)).length = 64 simp [pk1Off]All goals completed! 🐙⟩,
   ⟨((K.keyPair seed).toList.drop pk2Off).take 1152, byK:MlKemseed:List.Vector (BitVec 8) 64⊢ (List.take 1152 (List.drop pk2Off (K.keyPair seed).toList)).length = 1152 simp [pk2Off]All goals completed! 🐙⟩,
   K.keyPair seed)

5 declarations not shown (lines 62–79): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.MlKem.fromSeed_dk, CryptoVerification.LibsignalSpqrV1.MlKem.fromSeed_hdr, CryptoVerification.LibsignalSpqrV1.MlKem.fromSeed_ek, CryptoVerification.LibsignalSpqrV1.MlKem.fromSeed_pk1, CryptoVerification.LibsignalSpqrV1.MlKem.fromSeed_pk2

def MlKem.validPkBytesL81–87 ↗#

Full validate_pk_bytes(hdr, ek).is_ok() check: hdr.length == 64 && ek.length == 1152 followed by K.validPk hdr ek.

def MlKem.validPkBytes (K : MlKem) (hdr ek : Bytes) : Bool :=
  hdr.length == 64 && ek.length == 1152 && K.validPk hdr ek

end CryptoVerification.LibsignalSpqrV1