KemFailFind.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 12 of 76 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 failure-finding assumption (KemFailFind) and bad event (KemFailBad)

Trusted in part. MlKem.KemFailFindAdversary, MlKem.kemFailFindGame, MlKem.kemFailFindAdvantage, MlKem.tapePairFails and MlKem.KemFailBad (Computational/docs/TRUSTED_BASE.md §3): computational failure-search game (KemFailFind, kemFailFindAdvantage) on K : MlKem and the real-game bad event charged by the headline statements.

In LibsignalGame, sender coins on transmit-P and chall-P are chosen by the adversary (whereas receive coins are uniform, DEV-LS1), so average-case correctness (MlKem.CorrectWith) does not rule out decapsulation failure along an execution trace. Because K : MlKem is an unkeyed deterministic primitive with non-zero failure density (δ ≈ 2^-164.8 in ML-KEM-768, FIPS 203 §3.2 Table 1), a non-uniform constant adversary achieves advantage 1, so headline statements must not quantify over sup_B or evaluate kemFailFindAdvantage on an ∃-bound reduction. Instead, the headline statements charge MlKem.KemFailBad directly on the protocol adversary's logged 64-byte send tapes; a fixed extractor outputting a logged pair (seed, m) reduces KemFailBad to KemFailFind.

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open OracleComp OracleSpec ENNReal

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

CryptoVerification.LibsignalSpqrV1.MlKem.KemFailFindAdversary, CryptoVerification.LibsignalSpqrV1.MlKem.kemFailFindGame, CryptoVerification.LibsignalSpqrV1.KemFailFind, CryptoVerification.LibsignalSpqrV1.MlKem.kemFailFindAdvantage, CryptoVerification.LibsignalSpqrV1.kemFailFindAdvantage

Real-game KEM-failure bad event (KemFailBad)

def MlKem.tapePairFailsL62–77 ↗#

Whether 64-byte send tapes t₁, t₂ form a failing honest SPQR V1 ML-KEM exchange (K.honestExchangeFails t₁ (t₂.take 32)).

def MlKem.tapePairFails (K : MlKem) (t₁ t₂ : List (BitVec 8)) : Bool :=
  if h₁ : t₁.length = 64 then
    if h₂ : t₂.length = 64 then
      K.honestExchangeFails ⟨t₁, h₁⟩ ⟨t₂.take 32, byK:MlKemt₁:List (BitVec 8)t₂:List (BitVec 8)h₁:t₁.length = 64h₂:t₂.length = 64⊢ (List.take 32 t₂).length = 32 simp [h₂]All goals completed! 🐙⟩
    else false
  else false

def MlKem.KemFailBadL71–74 ↗#

KEM-failure bad event on a log of 64-byte send tapes: some ordered pair (t₁, t₂) satisfies K.tapePairFails t₁ t₂.

def MlKem.KemFailBad (K : MlKem) (log : List (List (BitVec 8))) : Bool :=
  log.any fun t₁ => log.any fun t₂ => K.tapePairFails t₁ t₂

end CryptoVerification.LibsignalSpqrV1