Proof obligation for `kpke_ind_cpa_security` 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:

messages was encrypted, so the adversary's advantage is 0. The gap between the two cases
is exactly the MLWE advantage.

The concrete instantiation uses `k×k` matrices over `T_q` with secrets and errors sampled
from `CBD(η₁)` in the NTT domain. -/
theorem kpke_ind_cpa_security :

[alik-eth]

Flagging that the current shape is (very likely) vacuous: the MLWE instance is existentially chosen by the prover and is not pinned to the K-PKE/Kyber parameters.

∃ mlwe : LearningWithErrors.Problem …, ∀ cpaAdv, ∃ mlweAdv,
  (IND_CPA_advantage cpaAdv).toReal ≤ |LearningWithErrors.advantage mlwe mlweAdv|

Because mlwe is ∃-quantified, one can pick a degenerate Problem whose distr/uniformDistr have disjoint support (e.g. noiseless := 0, sampleUniform := pure 1); a trivial distinguisher then gives |advantage mlwe mlweAdv| = 1 ≥ (IND_CPA_advantage …).toReal (which is ≤ 1). The reduction proves nothing about K-PKE.

Suggested fix: fix mlwe to the actual Kyber MLWE instance (k×k over T_q, secrets/errors from CBD(η₁) in the NTT domain) rather than ∃ mlwe, so the bound ties IND-CPA to the real hardness assumption.

[alik-eth]

Proposal: redesign kpke_ind_cpa_security (#214)

Status of the current statement (LatticeCrypto/MLKEM/Security.lean:99): ∃ mlwe : LearningWithErrors.Problem …, ∀ cpaAdv, ∃ mlweAdv, … — vacuous exactly as flagged in the earlier comment (prover picks a degenerate Problem with disjoint supports, advantage 1). Two updates from checking current code: (1) LearningWithErrors.Problem is now a re-export of NoisyLearning.Problem (#480), which is precisely the right target for pinned instances; (2) the statement also has no query bound: the framework IND-CPA game is a multi-query LR-oracle game (INDCPA/Oracle.lean), and a constant-sized MLWE bound is unprovable for unbounded-query adversaries even after pinning — the hybrid loss is q_e. Proposal follows the #467 playbook (mldsaMLWEShort/mldsaMatrixMLWE, SecurityNMA.lean:448).

1. Correct distributional model — pinned NoisyLearning.Problem instances

Two hops, two pinned instances (secrets/errors are CBD(η), not uniform; cbdVec from the #213 proposal, i.e. a proof-level home for Concrete.cbdSample):

/-- Keygen hop: t̂ = ·ŝ + ê vs uniform, k samples, NTT domain. -/
noncomputable def mlkemMLWEKeys (params ring) :
    NoisyLearning.Problem (TqMatrix k k) (TqVec k) (TqVec k) where
  sampleChallenge := $ᵗ TqMatrix k k          -- seed-based twin: ρ ↦ publicMatrix ρ, see §2
  sampleSecret := ring.nttVec <$> cbdVec η₁ k
  sampleError  := ring.nttVec <$> cbdVec η₁ k
  noiseless    := fun ŝ  => ring.matVecMul  ŝ
  sampleUniform := $ᵗ TqVec k

/-- Encryption hop: (u, v) pre-compression vs uniform, k+1 samples, normal domain. -/
noncomputable def mlkemMLWEEnc (params ring) :
    NoisyLearning.Problem (TqMatrix k k × TqVec k) (RqVec k) (RqVec k × Rq) where
  sampleSecret := cbdVec η₁ k                  -- y
  sampleError  := Prod.mk <$> cbdVec η₂ k <*> cbdSample η₂   -- (e₁, e₂)
  noiseless    := fun y (Â, t̂) => (ring.invNTTVec (ring.matTransposeVecMul  (ring.nttVec y)),
                                    ring.invNTT (ring.dot t̂ (ring.nttVec y)))
  …

Note the second instance is not matrixProblem-shaped (k+1 samples, product output, NTT/inverse-NTT in the noiseless map) — NoisyLearning.Problem's generality covers it as-is, which is a good early stress test of #480. Compression of (u, v) is public post-processing, so it rides on top of the hop.

2. Headline + FIPS corollary via named idealizations

/-- Ideal scheme (honest CBD sampling, uniform Â), single-challenge adversary. -/
theorem kpke_ideal_ind_cpa (adv) (hq : adv.MakesAtMostQueries 1) :
    ∃ B₁ B₂, (IND_CPA_advantage adv).toReal ≤
      |advantage (mlkemMLWEKeys …) B₁| + |advantage (mlkemMLWEEnc …) B₂|
-- multi-query corollary at factor q_e via the existing MultiQueryHybrid infra:
--   … (hq : adv.MakesAtMostQueries q_e) : … ≤ q_e * (|…B₁| + |…B₂|)

The FIPS scheme (KPKE.asExplicitCoins: seed-derived  via sampleNTT, PRF-derived noise) connects at explicitly-priced cost through named, inspectable assumptions, precedents expandAIdealization/expandSReplacement (#467, SecurityNMA.lean:484/:320): sampleNTTIdealization εA ((ρ, publicMatrix ρ) vs (ρ, Â) uniform-independent), keyDerivationReplacement εK, coinsDerivationReplacement εE (shared with #213). Corollary: … ≤ |…B₁| + |…B₂| + εA + εK + εE. Each Prop docstring carries #467's honesty caveat: unrestricted quantifiers are only satisfiable at large ε for fixed deterministic prims; read computationally pending the cost model (#460).

3. Satisfiability certificates as a gate

Per the #467 gate (keygenShort_generable, SecurityNMA.lean:271, which is the discipline that caught the uninhabitable Primitives.Laws / the information-theoretically-trivial uniform-secret mldsaMLWE): every pinned instance and pinning hypothesis ships a kernel-checked witness. Here: mlkemMLWEKeys/mlkemMLWEEnc are definitions (inhabited by construction — the gate is that they are non-degenerate: a lemma that distr ≠ uniformDistr supports overlap, or simply that CBD sampling is a probability, plus an instantiation example at mlkem768); any hGen : pke.keygen = idealKeygen-style pinning gets a _generable certificate. What fails the gate today: the ∃-quantified mlwe (content-free witness passes), and the absent query bound (no hypothesis to certify, but the unbounded claim is false once pinned).

4. Honest scoping and out of scope

• In scope: pinned instances; ideal-scheme single-challenge headline (the real Kyber Thm-1-style proof); multi-query corollary; FIPS corollary via the three named replacements.
• Out of scope: concrete numeric MLWE hardness (assumption, by design); PPT/cost bounds on the reduction (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460); δ-correctness (Proof obligation for kpke_delta_correct in LatticeCrypto/MLKEM/Security.lean #213) and the FO composition (Proof obligation for ind_cca_security in LatticeCrypto/MLKEM/Security.lean #215, and 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 which block it); byte-level Encoding refinement.
• Landing order: (a) proof-level CBD home (shared with Proof obligation for kpke_delta_correct in LatticeCrypto/MLKEM/Security.lean #213); (b) pinned instances + non-degeneracy certificates; (c) kpke_ideal_ind_cpa (the bulk of the work — the two game hops); (d) multi-query + FIPS corollaries. Steps (a)–(b) are small and unblock Proof obligation for ind_cca_security in LatticeCrypto/MLKEM/Security.lean #215's restatement immediately.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77