MlKemCorrect.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 19 of 63 lines trusted trust banner B3, trusted in part 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: ML-KEM-768 δ-correctness (MlKem.CorrectWith)

Trusted in part. The theorems of Computational/Theorems/ use MlKem.honestExchangeFails from this file; CorrectWith is checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Defines the single-exchange failure predicate MlKem.honestExchangeFails over the incremental ML-KEM wrappers (generate, encaps1, ek_matches_header, encaps2 with the issue-1275 fix-up, and decaps in States.lean), and the average-case δ-correctness hypothesis MlKem.CorrectWith over uniform 64-byte keygen seed and 32-byte encapsulation randomness (FIPS 203 §3.2, Table 1; DEV-SPQR6).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open OracleComp ENNReal

def MlKem.honestExchangeFailsL33–51 ↗#

Returns true when one honest SPQR ML-KEM exchange fails on 64-byte keygen seed and 32-byte encapsulation randomness m: any wrapper (generate, encaps1, encaps2, decaps) errors, ek_matches_header rejects the generated ek, or the decapsulated secret differs from the encapsulated one.

def MlKem.honestExchangeFails (K : MlKem) (seed : List.Vector (BitVec 8) 64)
    (m : List.Vector (BitVec 8) 32) : Bool :=
  match LibsignalSpqrV1.generate K seed.toList with
  | .error _ => true
  | .ok (keys, _) =>
    match LibsignalSpqrV1.encaps1 K keys.hdr m.toList with
    | .error _ => true
    | .ok ((ct1, es, ssB), _) =>
      if !(LibsignalSpqrV1.ek_matches_header K keys.ek keys.hdr) then true else
      match LibsignalSpqrV1.encaps2 K keys.ek es with
      | .error _ => true
      | .ok ct2 =>
        match LibsignalSpqrV1.decaps K keys.dk ct1 ct2 with
        | .error _ => true
        | .ok ssA => decide (ssA ≠ ssB)

1 declaration not shown (lines 53–64): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.MlKem.CorrectWith

end CryptoVerification.LibsignalSpqrV1