Proof obligation for `kpke_delta_correct` in `LatticeCrypto/MLKEM/Security.lean`

[quangvdao]

A proof in LatticeCrypto/MLKEM/Security.lean contains a sorry.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

(η₁, η₂) and compression parameters (d_u, d_v); concrete values are given in FIPS 203 Table 1:

- ML-KEM-512:  δ ≈ 2⁻¹³⁸·⁸
- ML-KEM-768:  δ ≈ 2⁻¹⁶⁴·⁸
- ML-KEM-1024: δ ≈ 2⁻¹⁷⁴·⁸ -/
theorem kpke_delta_correct :

[alik-eth]

The statement as written is vacuously true and shouldn't be closed as-is:

∃ δ : ℝ≥0∞, (KPKE.asExplicitCoins …).deltaCorrect δ

Since ℝ≥0∞ contains ⊤ and deltaCorrect ⊤ is ∀ msg, Pr[…] ≤ ⊤ (true by le_top), the whole thing closes in one line via ⟨⊤, fun _ => le_top⟩ — axiom-clean but content-free. It does not establish the "concrete failure bound δ ≈ 2⁻¹³⁸·⁸…" the docstring promises.

Suggested fix before this becomes a real obligation: bound δ by a concrete value, e.g. deltaCorrect (concreteDelta params) for an explicit concreteDelta, or ∃ δ ≤ c, deltaCorrect δ with c the FIPS 203 Table 1 value. Then the proof carries the actual concentration/compression-error argument.

[alik-eth]

Proposal: redesign kpke_delta_correct (#213)

Status of the current statement (LatticeCrypto/MLKEM/Security.lean:70): ∃ δ : ℝ≥0∞, (KPKE.asExplicitCoins …).deltaCorrect δ closes by ⟨⊤, fun _ => le_top⟩ — vacuous, as flagged in the earlier comment. Checking against current code adds a stronger point: no non-trivial δ is provable at the current abstraction level at all. Primitives supplies noise as deterministic functions (prfEta1/2 : Seed32 → ℕ → Rq), Encoding.Laws has only roundtrip fields (no compression-error bounds), and MLKEM/Arithmetic.lean deliberately wires no norm bundle. For adversarial prims/encoding the decryption failure probability is 1, so pinning δ alone (the fix suggested on the issue) is necessary but not sufficient — the statement also has to move to a model where a δ is derivable. This mirrors the ML-DSA #467 situation exactly, and I propose transplanting that playbook. Owner call on all shape choices below.

1. Correct distributional model

Sample the noise honestly instead of deterministically deriving it. A CBD sampler already exists — MLKEM.Concrete.cbdSample (eta) : ProbComp Rq (uniform 64·η bytes through FIPS 203 Alg 8, LatticeCrypto/MLKEM/Concrete/CBD.lean:52) — the analogue of ML-DSA's sampleShortVec box sampler, except it already computes the exact CBD distribution as a pushforward. Decision needed: promote it (or an alias cbdVec η k : ProbComp (RqVec k) via ProbComp.sampleIID) to a proof-level home so Security.lean need not import Concrete/. Then define the idealized scheme:

def KPKE.idealScheme (params ring encoding) : AsymmEncAlg.ExplicitCoins ProbComp … where
  keygen  := do let ρ ← $ᵗ Seed32; let  ← $ᵗ TqMatrix k k   -- or  := publicMatrix ρ, see §2
                let s ← cbdVec η₁ k; let e ← cbdVec η₁ k; …   -- t̂ = ·NTT(s) + NTT(e)
  encrypt := …  -- y ← cbdVec η₁ k, e₁ ← cbdVec η₂ k, e₂ ← cbdSample η₂, fresh per call

2. Statement shape: deterministic core + exact δ, no ∃

• Prerequisite laws (new, satisfiability-certified per §3): an ∞-norm for the ML-KEM Rq (wire LatticeCrypto/Ring/Norms.lean, as ML-DSA does) and an Encoding.NoiseLaws extension: ‖decompressDU (compressDU u) − u‖∞ ≤ Bdu, same for dv, and the message gate ‖w − decompress1 (byteDecode1 m)‖∞ < ⌈q/4⌋ → byteEncode1 (compress1 w) = m.
• Deterministic core (real proof content, needs NTTRingLaws): if the accumulated noise w = eᵀy + e₂ + Δv − sᵀe₁ − sᵀΔu satisfies the q/4 bound, then decrypt (encrypt …) = msg.
• δ as a definition, not an existential: noncomputable def kpkeDeltaBad (params …) : ℝ≥0∞ := Pr[noise bound fails | s,e,y,e₁,e₂ ← CBD draws] — an explicit, inspectable expression.

theorem kpke_ideal_deltaCorrect (hRing : NTTRingLaws ring) (hEnc : encoding.NoiseLaws) :
    (KPKE.idealScheme params ring encoding).deltaCorrect (kpkeDeltaBad params ring encoding)

• FIPS transfer via named idealizations (feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228) #467 pattern, expandSReplacement / expandAIdealization precedents at SecurityNMA.lean:320/:484): keyDerivationReplacement εK (G/PRF_η₁ chain from d vs independent ρ, CBD draws) and coinsDerivationReplacement εE (per-encryption (y,e₁,e₂) from uniform Coins vs fresh CBD). The correctness experiment is itself a distinguisher, so:

theorem kpke_fips_deltaCorrect (hK : keyDerivationReplacement prims εK) (hE : …) :
    (KPKE.asExplicitCoins …).deltaCorrect (kpkeDeltaBad … + ENNReal.ofReal (εK + εE))

Both Props carry the honest caveat from #467: for fixed deterministic prims the unrestricted-quantifier form is only satisfiable at large ε (image-membership distinguisher); pending the cost model (#460) they are read computationally, and the docstring must say so.

3. Satisfiability certificates as a gate

Every new hypothesis ships a kernel-checked witness, per the #467 gate (keygenShort_generable, SecurityNMA.lean:271 — the discipline that caught Primitives.Laws being uninhabitable on main). Concretely: Encoding.NoiseLaws and NTTRingLaws certified against the concrete instance (MLKEM/Concrete/Instance.lean); kpkeDeltaBad ≠ ⊤ (it is a probability, ≤ 1 by construction); a nonVacuity example instantiating kpke_ideal_deltaCorrect at mlkem768. Today's statement fails the dual gate — it is satisfiable by a content-free witness (⊤); the redesign removes the existential entirely.

4. Honest scoping and out-of-scope list

• In scope (proof-level): deterministic noise-bound correctness; deltaCorrect (kpkeDeltaBad …) for the ideal scheme; FIPS transfer at + ofReal (εK + εE).
• Out of scope: the numeric FIPS Table-1 values (δ ≈ 2⁻¹³⁸·⁸ etc.) — these require the exact per-coefficient noise convolution (Kyber computes them by script); a follow-up issue could target kpkeDeltaBad mlkem768 ≤ 2⁻¹⁶⁴ via exact ℚ computation/native_decide, but it should not gate this redesign. Also out of scope: the FO composition (Proof obligation for ind_cca_security in LatticeCrypto/MLKEM/Security.lean #215) and anything touching Proof obligation for OW_PCVA_bound in VCVio/CryptoFoundations/FujisakiOkamoto/TTransform.lean #189/Proof obligation for IND_CCA_Advantage_composeWithKDM_le in VCVio/CryptoFoundations/FujisakiOkamoto/UTransform.lean #190/Proof obligation for IND_CCA_bound in VCVio/CryptoFoundations/FujisakiOkamoto/Composed.lean #191.
• Landing order: (a) norm wiring + Encoding.NoiseLaws + proof-level CBD home; (b) deterministic core; (c) kpkeDeltaBad + ideal-scheme theorem; (d) FIPS transfer. Step (c) is what Proof obligation for kpke_ind_cpa_security in LatticeCrypto/MLKEM/Security.lean #214 and Proof obligation for ind_cca_security in LatticeCrypto/MLKEM/Security.lean #215 consume.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77