feat(MLDSA): compose the short-model EUF-NMA/CMA headline

[alik-eth]

The capstone of the #467 decomposition: the composed short-model ML-DSA EUF-NMA/CMA security headline, assembled on the landed legs and engine. Purely additive.

Stacks on #503 (binding) / #504 (short-MLWE) / #506 (SelfTargetMSIS leg) / #507 (CMA-to-NMA engine). Until those land, this PR's diff shows their content too; its own contribution is the ~994 additive lines composing the headline. Once the four land, this shrinks to the headline layer.

What this adds

• nma_security_short — the EUF-NMA bound composing the exact key-swap hop (feat(MLDSA): short-secret MLWE model and the exact NMA key-swap hop #504's MLWE leg), the reprogramming hops (the feat(FiatShamir): Fiat-Shamir-with-aborts CMA-to-NMA reduction engine #507 engine), and the tailored-STMSIS extraction (feat(MLDSA): tailored SelfTargetMSIS problem and the NMA extraction bound #506): advantage ≤ ofReal(MLWE + εbridge) + SelfTargetMSIS.advantage. Needs no Primitives.Laws (the short key-swap is an exact identity).
• nma_security_short_matrix — the literature-facing corollary at the uniform-matrix MLWE, discharging the bridge via expandAIdealization.
• nma_security_fips — connects the FIPS seed-derived key generation to the short model at cost εPRG via the named expandSReplacement assumption, with the keygen0_generable/hrFips certificate.
• euf_cma_security_of_nma_short — the CMA-to-NMA composition, using the feat(FiatShamir): Fiat-Shamir-with-aborts CMA-to-NMA reduction engine #507 engine's euf_cma_to_nma; plus the re-pointed asymptotic corollary (euf_cma_security_asymptotic_short / asymptotic_loss_regime_satisfiable, numerical-loss regime only).
• The joint frontier witness (LatticeCrypto/MLDSA/NonVacuity.lean, new): mldsa_short_cma_hyps_inhabited + trivial_euf_cma_security_of_nma_short — every hypothesis of the CMA headline inhabited simultaneously at a concrete trivial adversary (consistency-only, no quantitative content).

Scope

Additive — the base's old-model mldsaMLWE/nma_security decls are untouched here (retired in a later cleanup). The tailored→standard SelfTargetMSIS normal-form reduction is separate follow-up work.

Verification

Off current main (v4.32.0). lake build of the full CI library set green. nma_security_short, nma_security_fips, euf_cma_security_of_nma_short, and the witness trivial_euf_cma_security_of_nma_short all kernel-check [propext, Classical.choice, Quot.sound] (the witness at abstract parameters — no native_decide). Both touched files CI-lint clean; no base declaration changed.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	21
✅ Lines Added	12756
❌ Lines Removed	140

---

Lean Declarations

✏️ Removed: 3 declaration(s)

VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean (3)

• noncomputable def cmaToNmaLoss (qS qH : ℕ) (ε p ζ_zk δ : ℝ) (_hp : p < 1) : ℝ
• theorem euf_cma_bound_perfectHVZK
• theorem euf_cma_bound

✏️ Added: 283 declaration(s)

LatticeCrypto/MLDSA/SecurityNMA.lean (21)

• def expandSReplacement (εPRG : ℝ) : Prop
• def hrFips :
• def stmsisAlgebraicSolution (aHat : TqMatrix p.k p.l) (pk : PublicKey p prims)
• noncomputable def extractorCShort [Inhabited (Commitment p prims)] [Inhabited (Response p prims)]
• noncomputable def mldsaSTMSISShort (M : Type) :
• private theorem negl_poly_slack
• private theorem stmsis_tail_le_short
• theorem asymptotic_loss_regime_satisfiable :
• theorem cmaToNmaLoss_negligible
• theorem computeWApprox_eq_mul_sub_smul (h_transform : NTTRingLaws nttOps)
• theorem euf_cma_security_asymptotic_short
• theorem euf_cma_security_of_nma_short [SampleableType (PublicKey p prims)]
• theorem identificationSchemeShort_verify_eq_true_iff (h_transform : NTTRingLaws nttOps)
• theorem keygen0_generable :
• theorem mldsaSTMSISShort_isValid_expandA_iff (pk : PublicKey p prims)
• theorem mldsaSTMSISShort_isValid_iff (h_transform : NTTRingLaws nttOps)
• theorem negligible_ofReal_geometric (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) :
• theorem nmaAdvantage_keygenShort1_le_stmsis
• theorem nma_security_fips
• theorem nma_security_short_matrix (maxAttempts : ℕ) (εA : ℝ)
• theorem nma_security_short

LatticeCryptoTest/MLDSA/NonVacuity.lean (9)

• def honestNoAbortGood : PublicKey p prims → SecretKey p → Prop
• lemma expandAIdealization_one : expandAIdealization p prims 1
• lemma neverAbortSim_hvzk :
• lemma probOutput_none_neverAbortSim (pk : PublicKey p prims) :
• lemma trivialForger_signHashQueryBound (maxAttempts : ℕ) (pk : PublicKey p prims) :
• noncomputable def neverAbortSim :
• noncomputable def trivialForger (maxAttempts : ℕ) :
• theorem mldsa_short_cma_hyps_inhabited (maxAttempts : ℕ) :
• theorem trivial_euf_cma_security_of_nma_short (maxAttempts : ℕ) :

VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Bodies.lean (9)

• def firstSome {α : Type} (attempt : ProbComp (Option α)) : ℕ → ProbComp (Option α)
• lemma firstSome_succ {α : Type} (attempt : ProbComp (Option α)) (n : ℕ) :
• lemma tvDist_firstSome_le_geometric {α : Type} (a₁ a₂ : ProbComp (Option α))
• noncomputable def progSignAttempt (pk : Stmt) (sk : Wit) (msg : M) :
• noncomputable def progSignBody (pk : Stmt) (sk : Wit) (msg : M) :
• noncomputable def realSignBody (pk : Stmt) (sk : Wit) (msg : M) :
• noncomputable def signProgramCont (msg : M) :
• noncomputable def simSignBody (pk : Stmt) (_sk : Wit) (msg : M) :
• noncomputable def transSignBody (pk : Stmt) (sk : Wit) (msg : M) :

VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean (42)

• @[simp] lemma memCharge_uncacheQuery_self (gh : (M × Commit →ₒ Chal).QueryCache)
• lemma lazyGhostFire_one_eq (pk : Stmt) (sk : Wit) (w' : Commit) :
• lemma lazyGhostHybridImpl_run_sign_eq (pk : Stmt) (sk : Wit) (msg : M)
• lemma lazyGhostHybridImpl_run_unif_eq (pk : Stmt) (sk : Wit) (n : unifSpec.Domain)
• lemma memCharge_cacheQuery_le (gh : (M × Commit →ₒ Chal).QueryCache)
• lemma memCharge_uncacheQuery_le (gh : (M × Commit →ₒ Chal).QueryCache)
• lemma ofReal_tvDist_bind_le_tsum {α β : Type} (oa : ProbComp α) (f g : α → ProbComp β) :
• lemma ofReal_tvDist_run_fsAbortSignLoop_progSignBody_le (pk : Stmt) (sk : Wit) (msg : M)
• lemma probEvent_commit_hit_le (pk : Stmt) (sk : Wit) {ε : ℝ}
• lemma probEvent_ghostHybridImpl_read_bad_single_eq_lazyFire
• lemma probEvent_simulateQ_ghostHybridImpl_bad_eq_true
• lemma probOutput_bind_or_pure_le (q : Bool) (mb : ProbComp Bool) :
• lemma probOutput_eagerMultiReadBad_empty_eq_lazyFire
• lemma probOutput_eagerMultiReadBad_eq_lazyFire_or
• lemma probOutput_ghostHybridImpl_read_bad
• lemma probOutput_lazyGhostFire_one (pk : Stmt) (sk : Wit) (w' : Commit) :
• lemma probOutput_lazyGhostFire_true_le (pk : Stmt) (sk : Wit) {ε : ℝ}
• lemma probOutput_lazyGhostFire_true_le_enncard (pk : Stmt) (sk : Wit) {ε : ℝ}
• lemma run_ghostSignBody_succ (pk : Stmt) (sk : Wit) (msg : M) (n : ℕ)
• lemma run_progSignBody_succ (pk : Stmt) (sk : Wit) (msg : M) (n : ℕ)
• lemma run_simulateQ_fsAbortSignLoop_succ (pk : Stmt) (sk : Wit) (msg : M) (n : ℕ)
• lemma signCollisionBound_eq (ε p : ℝ) (n : ℕ) (N : ℝ≥0∞) :
• lemma signCollisionBound_mono (ε p : ℝ) (n : ℕ) {N N' : ℝ≥0∞} (h : N ≤ N') :
• lemma signCollisionBound_succ (ε p : ℝ) (n : ℕ) (N : ℝ≥0∞) :
• lemma signCollisionBound_zero (ε p : ℝ) (N : ℝ≥0∞) :
• lemma support_simulateQ_ghostHybridImpl_bad
• lemma tsum_ghostHybridImpl_read_hit_eq
• lemma tsum_ghostHybridImpl_read_step_charge_le
• lemma tsum_ghostHybridImpl_read_step_split
• lemma tsum_probOutput_bind_mul {α β : Type} (oa : ProbComp α)
• lemma tsum_probOutput_commit_mul_abort_le (pk : Stmt) (sk : Wit) {p_abort : ℝ}
• lemma tsum_probOutput_commit_mul_writeHit_le (pk : Stmt) (sk : Wit) (msg : M)
• lemma tsum_probOutput_mul_le_add_of_le {α : Type} (oa : ProbComp α)
• lemma tsum_probOutput_pure_mul {β : Type} (y : β) (f : β → ℝ≥0∞) :
• lemma tsum_probOutput_run_ghostSignBody_mul_ghost_enncard_le (pk : Stmt) (sk : Wit) (msg : M)
• lemma tsum_probOutput_run_ghostSignBody_mul_memCharge_le (pk : Stmt) (sk : Wit) (msg : M)
• lemma tsum_probOutput_run_progSignBody_mul_enncard_le (pk : Stmt) (sk : Wit) (msg : M)
• noncomputable def eagerMultiReadBad (pk : Stmt) (sk : Wit) (msg : M) (mc : M × Commit)
• noncomputable def lazyGhostFire (pk : Stmt) (sk : Wit) (w' : Commit) :
• noncomputable def lazyGhostHybridImpl (pk : Stmt) (sk : Wit) :
• noncomputable def memCharge (gh : (M × Commit →ₒ Chal).QueryCache) (mc : M × Commit) :
• noncomputable def signCollisionBound (ε p : ℝ) (n : ℕ) (N : ℝ≥0∞) : ℝ≥0∞

VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/GhostLayer.lean (27)

• abbrev GhostState (M Commit Chal : Type) : Type
• def onCache {α : Type}
• def overlayCache (re gh : (M × Commit →ₒ Chal).QueryCache) :
• def uncacheQuery (cache : (M × Commit →ₒ Chal).QueryCache) (q : M × Commit) :
• lemma enncard_uncacheQuery_le (cache : (M × Commit →ₒ Chal).QueryCache) (q : M × Commit) :
• lemma ghostBlindImpl_agree_good (pk : Stmt) (sk : Wit)
• lemma ghostBlindImpl_bad_mono (pk : Stmt) (sk : Wit)
• lemma ghostBlindImpl_eq_ghostHybridImpl_false (pk : Stmt) (sk : Wit) :
• lemma ghostHybridImpl_agree_good (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_bad_mono (progSide : Bool) (pk : Stmt) (sk : Wit)
• lemma overlayCache_apply_ghost_none
• lemma overlayCache_apply_ghost_some
• lemma overlayCache_cacheQuery_ghost
• lemma overlayCache_cacheQuery_real_of_ghost_none
• lemma overlayCache_cacheQuery_uncacheQuery
• lemma overlayCache_empty (re : (M × Commit →ₒ Chal).QueryCache) :
• lemma randomOracle_run_eq_roStep (re : (M × Commit →ₒ Chal).QueryCache) (mc : M × Commit) :
• lemma run_ghostSignBody_fst (pk : Stmt) (sk : Wit) (msg : M) :
• lemma run_ghostSignBody_fst_eq_transSignBody (pk : Stmt) (sk : Wit) (msg : M)
• lemma run_ghostSignBody_overlay (pk : Stmt) (sk : Wit) (msg : M) :
• lemma toSet_uncacheQuery_subset (cache : (M × Commit →ₒ Chal).QueryCache) (q : M × Commit) :
• noncomputable def ghostBlindImpl (pk : Stmt) (sk : Wit) :
• noncomputable def ghostHybridImpl (progSide : Bool) (pk : Stmt) (sk : Wit) :
• noncomputable def ghostSignBody (pk : Stmt) (sk : Wit) (msg : M) :
• noncomputable def hybridBaseImpl :
• noncomputable def hybridSignImpl
• noncomputable def roStep (re : (M × Commit →ₒ Chal).QueryCache) (mc : M × Commit) :

VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/NMAHandler.lean (22)

• @[simp] lemma baseEmbed_empty :
• @[simp] lemma baseEmbed_inl (base : (M × Commit →ₒ Chal).QueryCache)
• @[simp] lemma baseEmbed_inr (base : (M × Commit →ₒ Chal).QueryCache) (mc : M × Commit) :
• abbrev NmaGhostState (M Commit Chal : Type) : Type
• def baseEmbed (base : (M × Commit →ₒ Chal).QueryCache) :
• def signLiveCollision (base : (M × Commit →ₒ Chal).QueryCache) (msg : M) (w : Commit) : Prop
• lemma baseEmbed_cacheQuery (base : (M × Commit →ₒ Chal).QueryCache)
• lemma ghostNmaImpl_preserves_signed_inv (pk : Stmt) (sk : Wit)
• lemma ghostNmaImpl_proj_hybrid (pk : Stmt) (sk : Wit)
• lemma ghostNmaImpl_run_ro (pk : Stmt) (sk : Wit) (mc : M × Commit)
• lemma ghostNmaImpl_run_sign (pk : Stmt) (sk : Wit) (msg : M)
• lemma ghostNmaImpl_run_signed_inv (pk : Stmt) (sk : Wit) {β : Type}
• lemma ghostNmaImpl_run_unif (pk : Stmt) (sk : Wit) (n : unifSpec.Domain)
• lemma map_run_simulateQ_ghostNmaImpl_overlay {β : Type} (pk : Stmt) (sk : Wit)
• lemma map_run_simulateQ_ghostNmaImpl_overlay_empty {β : Type} (pk : Stmt) (sk : Wit)
• lemma not_signLiveCollision_iff (base : (M × Commit →ₒ Chal).QueryCache) (msg : M) (w : Commit) :
• lemma run_ghostSignProgramCont_overlay (msg : M)
• lemma run_simGhostSignBody_overlay (pk : Stmt) (sk : Wit) (msg : M)
• lemma simGhostSignBody_support_ghost (pk : Stmt) (msg : M)
• noncomputable def ghostNmaImpl (pk : Stmt) (_sk : Wit) :
• noncomputable def ghostSignProgramCont (msg : M) :
• noncomputable def simGhostSignBody (pk : Stmt) (msg : M) :

VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Projections.lean (14)

• def blindStepProj
• lemma blindStepProj_map_ghostBlindImpl_indep (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_preserves_signed_inv (progSide : Bool) (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_proj_prog (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_proj_trans (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_run_ro_ghost_none (progSide : Bool) (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_run_ro_ghost_some (progSide : Bool) (pk : Stmt) (sk : Wit)
• lemma ghostHybridImpl_run_sign (progSide : Bool) (pk : Stmt) (sk : Wit)
• lemma ghostSignBody_support_ghost (pk : Stmt) (sk : Wit) (msg : M) :
• lemma hybridBaseImpl_run_ro (mc : M × Commit)
• lemma hybridSignImpl_run
• lemma onCache_run {α : Type}
• lemma roStep_of_none {re : (M × Commit →ₒ Chal).QueryCache} {mc : M × Commit}
• lemma roStep_of_some {re : (M × Commit →ₒ Chal).QueryCache} {mc : M × Commit} {v : Chal}

VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Assembly.lean (4)

• lemma managedRoNmaExp_simulatedNmaAdv_eq_eufNmaExp :
• lemma simulatedNmaAdv_nmaHashQueryBound
• noncomputable def simulatedEufNmaAdv :
• theorem euf_cma_to_nma

VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/BodyHops.lean (6)

• lemma hybridExpAtKey_eq_run_bind
• lemma hybridVerifyCont_cache_congr (pk : Stmt) (ms : M × Option (Commit × Resp))

…and 133 more not listed.

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean (1)

• theorem euf_cma_bound (L123)

---

Coverage Notes

• AI file summarization partially analyzed 5 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• LatticeCrypto/MLDSA/SecurityNMA.lean (+1121/-3)
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean (+1403/-0)
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean (+1898/-0)
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/NMAReduction.lean (+972/-0)
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/TapeFactorization.lean (+2570/-0)

* Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• LatticeCrypto/MLDSA/SecurityNMA.lean: The diff adds two public imports (VCVio.CryptoFoundations.Asymptotics.Negligible and Mathlib.Analysis.SpecificLimits.Normed), expands the module-level docstring to include a new Tailored vs. standard SelfTargetMSIS subsection that clarifies mldsaSTMSIS and mldsaSTMSISShort are tailored (verifier-relation) problems and states that reduction to the standard normal form is deferred, and introduces three new declarations: (1) hrFips, a GenerableRelation over validKeyPair whose generator is keygen0; (2) keygen0_generable, a theorem witnessing that such a relation exists (so the hGen hypothesis is non-vacuous); and (3) expandSReplacement, a Prop that formalizes the XOF-replacement assumption for ExpandSeed/ExpandS against the short-secret box distribution, quantified by a real bound εPRG.
• LatticeCryptoTest.lean: Adds a public import of LatticeCryptoTest.MLDSA.NonVacuity, making the definitions and theorems from that module available to users of this top-level file. This likely provides proofs or statements about non-vacuity of certain ML-DSA properties, supporting the verification of ML-DSA spec compliance.
• LatticeCryptoTest/MLDSA/NonVacuity.lean: This new file NonVacuity.lean provides a logical consistency (inhabitance) witness for the conditional theorem MLDSA.euf_cma_security_of_nma_short. It defines three concrete witness components — the never-aborting HVZK simulator neverAbortSim, the good-key event honestNoAbortGood (where the honest prover never aborts), and the trivial CMA forger trivialForger (making no oracle queries and returning (default, none)) — and then proves mldsa_short_cma_hyps_inhabited, a conjunction of every explicit hypothesis of the headline at trivial budgets (ε = 1, ζ_zk = 1, δ = 1, p_abort = 0, εbridge = 1) via supporting lemmas neverAbortSim_hvzk, probOutput_none_neverAbortSim, trivialForger_signHashQueryBound, and expandAIdealization_one. Finally, trivial_euf_cma_security_of_nma_short applies the headline theorem with these witnesses, discharging all hypotheses end-to-end. No sorry or admit appears; the file carries no quantitative security content, serving only to demonstrate that the hypothesis frontier of the CMA security statement is not vacuously uninhabitable.
• VCVio.lean: This change adds 15 new public import lines to VCVio.lean, exposing the entire VCVio.CryptoFoundations.FiatShamir.WithAbort.GhostBodies submodule (Bodies, BodyBounds, GhostLayer, NMAHandler, Projections) and the VCVio.CryptoFoundations.FiatShamir.WithAbort.Security submodule (Assembly, BodyHops, CouplingEngine, GhostReadCharge, HiddenReadFold, HopLemmas, Loss, NMAReduction, ReadRecording, TapeFactorization). These imports make the ghost‑body infrastructure and the security proofs for the Fiat‑Shamir with abort construction available to any code that imports VCVio, extending the public API with these new definitions and theorems.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies.lean: This is a new umbrella module that re-exports five submodules: Bodies, GhostLayer, Projections, BodyBounds, and NMAHandler. It provides a ghost-layer presentation of the Fiat-Shamir with aborts transform, including signing bodies (realSignBody, progSignBody, transSignBody, simSignBody), hybrid handlers (hybridBaseImpl, hybridSignImpl), projections onto hybrid games (run_ghostSignBody_overlay, run_ghostSignBody_fst, ghostHybridImpl_proj_prog, ghostHybridImpl_proj_trans), and a ghost-domain invariant (ghostHybridImpl_preserves_signed_inf). The module also introduces a monotone bad flag and a layered ghost-tagged NMA handler.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Bodies.lean: This new file introduces the ghost-layer machinery for the Fiat-Shamir with aborts protocol, containing two main components. First, it defines firstSome, a retry loop that iterates an optional sampler up to n times returning the first non-none result, along with supporting lemmas firstSome_succ and tvDist_firstSome_le_geometric (which bounds the total variation distance between two retry loops using a geometric series). Second, it defines the four hybrid signing-oracle bodies used in the CMA-to-NMA reduction: realSignBody (real signing loop with cache interaction on every attempt), progSignBody (all-attempts reprogramming hybrid that overwrites the cache with fresh challenges), transSignBody (accepted-only reprogramming that runs privately on honest executions), and simSignBody (HVZK-simulated variant that ignores the secret key), all implemented as StateT transformers over the random-oracle cache, with progSignAttempt and signProgramCont as their supporting building blocks. No sorry or admit appears in the diff.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean: This new file BodyBounds.lean introduces the ghost-layer machinery for the Fiat-Shamir with aborts hybrid proof, establishing bounds for the real-versus-reprogrammed signing loop (ofReal_tvDist_run_fsAbortSignLoop_progSignBody_le), the per-attempt collision and abort bounds (tsum_probOutput_commit_mul_abort_le, probEvent_commit_hit_le), the deferred-sampling (lazy) ghost read step and handler (lazyGhostFire, lazyGhostHybridImpl) with its charged-step bound (probOutput_lazyGhostFire_true_le, probOutput_lazyGhostFire_true_le_enncard), the two body-level cores of the Sign → Prog hop (including the TV induction and expected cache growth of progSignBody and ghostSignBody), and the per-target ghost-membership charge route (probOutput_eagerMultiReadBad_eq_lazyFire_or, probEvent_ghostHybridImpl_read_bad_single_eq_lazyFire). The file also includes auxiliary lemmas (tsum_probOutput_pure_mul, tsum_probOutput_bind_mul, tsum_probOutput_mul_le_add_of_le, ofReal_tvDist_bind_le_tsum) and the eager read HIT charge decomposition (tsum_ghostHybridImpl_read_hit_eq, tsum_ghostHybridImpl_read_step_split). No sorry or admit are present in the diff.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/GhostLayer.lean: This file introduces a ghost-layer abstraction for the Fiat-Shamir with aborts signing body, adding a two-layer cache (real + ghost) with the overlayCache and uncacheQuery operations, and proving lemmas about their interactions (overlayCache_cacheQuery_uncacheQuery, toSet_uncacheQuery_subset, enncard_uncacheQuery_le, overlayCache_cacheQuery_ghost, overlayCache_apply_ghost_some, overlayCache_apply_ghost_none, overlayCache_cacheQuery_real_of_ghost_none). It defines ghostSignBody on the layered cache, then proves the key projection lemmas run_ghostSignBody_overlay (overlaying recovers progSignBody) and run_ghostSignBody_fst (forgetting the ghost layer recovers transSignBody’s loop), with run_ghostSignBody_fst_eq_transSignBody as a corollary at the scheme's budget. It also defines roStep for a single caching random-oracle step, the GhostState abbreviation, the ghost-instrumented hybrid handler ghostHybridImpl with its ghostHybridImpl_agree_good and ghostHybridImpl_bad_mono lemmas, the ghost-blind handler ghostBlindImpl (as an alias for the Trans-side handler) with ghostBlindImpl_eq_ghostHybridImpl_false and ghostBlindImpl_agree_good, and finally the hybrid run-level handlers onCache, hybridBaseImpl, and hybridSignImpl. The file contains no sorry or admit.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/NMAHandler.lean: This new file introduces the layered ghost-tagged NMA handler for the Fiat-Shamir with aborts simulated hybrid. It defines ghostSignProgramCont and simGhostSignBody (ghost-layer versions of the sign program continuation and signing body that write to a ghost cache instead of the base cache), and proves overlay-projection lemmas (run_ghostSignProgramCont_overlay, run_simGhostSignBody_overlay) showing that overlaying ghost onto base recovers the original signProgramCont/simSignBody. The file also defines the ghostNmaImpl handler (with run lemmas ghostNmaImpl_run_unif, ghostNmaImpl_run_ro, ghostNmaImpl_run_sign), proves the ghost-domain invariant ghostNmaImpl_preserves_signed_inv and its whole-run lift ghostNmaImpl_run_signed_inv, establishes the per-step projection equality ghostNmaImpl_proj_hybrid (sub-lemma (a)), and introduces the signLiveCollision event and its negation lemma. These components together provide the foundation for the NMA bridge coupling the layered ghost-tagged run to the plain single-cache hybrid run, with no sorry or admit present.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Projections.lean: Summary unavailable — AI generation failed.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean: The file was restructured: the placeholder theorems euf_cma_bound and euf_cma_bound_perfectHVZK (both sorry) have been removed, and the module now re-exports submodules Loss, BodyHops, GhostReadCharge, HiddenReadFold, CouplingEngine, ReadRecording, TapeFactorization, HopLemmas, NMAReduction, and Assembly. The new module documentation describes the proof structure as a hybrid game chain (hybridExpAtKey over realSignBody, progSignBody, transSignBody, simSignBody) with parameters ε, p_abort, δ tied to a "good key" event, and the exposed API now includes cmaToNmaLoss and euf_cma_to_nma (the managed-RO NMA interface).
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Assembly.lean: This file adds the 'Assembly' module bridging the managed-RO NMA experiment to the plain EUF-NMA interface for Fiat-Shamir with aborts. It defines the cache-forgetting adversary simulatedEufNmaAdv and the lemma managedRoNmaExp_simulatedNmaAdv_eq_eufNmaExp proving that the success probabilities coincide via Option B. The central theorem euf_cma_to_nma assembles the complete CMA-to-NMA reduction, bounding the CMA advantage by the managed-RO NMA success probability plus cmaToNmaLoss. The lemma simulatedNmaAdv_nmaHashQueryBound establishes that the reduction issues at most qH live hash queries.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/BodyHops.lean: The new file BodyHops.lean adds the per-signing-query core of the Trans→Sim hop: the lemma tvDist_run_transSignBody_simSignBody_le bounds the total variation distance between the honest and simulated signing bodies. It also introduces the definitions hybridExpAtKey and hybridVerifyCont to factor the hybrid unforgeability experiment into an adversary run and a verification-and-freshness continuation, and proves supporting lemmas hybridExpAtKey_eq_run_bind, hybridVerifyCont_cache_congr, and probOutput_true_hybridVerifyCont_of_mem that describe the factorization, cache sensitivity, and vanishing success probability for re-used messages respectively. These components formalize the verification tail of the hybrid chain used in the CMA-to-NMA security proof.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean: This pull request replaces the old avgBadM_eager_le_lazy_joint proof with a significantly revised version, and adds three new lemmas (probEvent_ghostHybridImpl_bad_eq_ghostBlind, probEvent_ghostHybridImpl_bad_le_ghostBlind, probEvent_ghostBlind_bad_le_of_fac) and one new theorem (probEvent_ghostBlind_bad_le_of_fac). The core change is a complete reworking of the soundness argument; the old coupling-based proof of the eagerly-checked-ghost-read bound is replaced by a three-part decomposition (M1–M3) that isolates the 'bad' event probability. New lemmas state and prove: (M1) the equality of the 'bad' event probability under the eager hybrid and the ghost-blind handler (probEvent_ghostHybridImpl_bad_eq_ghostBlind), (M2) the immediate inequality of the same under the eager handler versus the ghost-blind handler (probEvent_ghostHybridImpl_bad_le_ghostBlind, a corollary of the equality), and (M3) a final bound on the ghost-blind handler's bad probability in terms of the protocol parameters (probEvent_ghostBlind_bad_le_of_fac). The new probEvent_ghostBlind_bad_le_of_fac theorem states the overall bound qS * (qH + 1) * ε / (1 - p_abort) given a per-commit guessing bound hGuess and an expected-number-of-ghost-keys bound hmean. All added lemmas and the theorem carry omit [SampleableType Stmt] annotations to avoid unnecessary typeclass constraints.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/GhostReadCharge.lean: This diff consists entirely of whitespace changes (adding trailing spaces to otherwise unchanged lines). No lemmas, definitions, or proofs were modified, added, or removed. The file's content, signatures, and logic remain identical.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HiddenReadFold.lean: This file introduces the HiddenReadFold module, which provides the direct probabilistic bound for the eager ghost-read bad probability in the EUF-CMA security proof for Fiat-Shamir with aborts. It defines the lemma hiddenReadList_fold_le_target, which averages the multi-key hidden-read fold to derive the target bound qS·(qH+1)·ε/(1-p). It also includes the geometric sum bounds geomAttemptSum_le and geomSum_le. The file establishes coupling theorems relTriple_ghostHybrid_lazyGhost_unif and relTriple_ghostHybrid_lazyGhost_sign relating the eager (ghostHybridImpl) and lazy (lazyGhostHybridImpl) ghost handlers for uniform and signing queries. Supporting measure-level lemmas are provided: tsum_probOutput_map_state_fixed, ghostHybridImpl_unif_expected_enncard, ghostHybridImpl_read_expected_enncard, ghostHybridImpl_sign_expected_enncard_le, ghostChargeK, ghostChargeInv, ghostHybridImpl_flag_preserved_le, ghostHybridImpl_read_expected_flag_le, avgBadM_ghostHybridImpl_threaded_carry, and avgBadM_ghostHybridImpl_threaded_K. These lemmas are used as bookkeeping for the threaded eager-charge bound in the security coupling engine.
• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HopLemmas.lean: This file HopLemmas.lean is new (983 lines) and provides the core bridge lemmas for the EUF-CMA security proof of the Fiat-Shamir-with-aborts transform. It contains:

• probOutput_unforgeableExp_eq_hybridExpAtKey_real (G₀ bridge): shows that at every key pair, the standard unforgeability experiment equals the real-signing hybrid experiment.
• flagLift and flagLift_run: lift a cache-level handler to one carrying a never-touched Bool flag in its state, enabling the expectedQuerySlack bridge.
• isQueryBoundP_cast_pred: transports a query-bound predicate across a propositionally equal choice of predicate and DecidablePred instance.
• sum_natCast_mul_pow_le_sq_sum_pow: an arithmetic inequality bounding the discrete first moment of a truncated geometric series by the square of its zeroth moment.
• probOutput_hybridExpAtKey_real_le_prog (G₀ → G₁): at a fixed key, replacing the real-signing hash cache by overwrite-reprogramming costs at most qS·ε·((qS+1)/(2·(1-p)²) + (qH+1)/(1-p)).
• probOutput_hybridExpAtKey_prog_le_trans (G₁ → G₂): at a fixed key, dropping the reprogramming of rejected attempts (keeping only the accepted transcript's programming) costs at most qS·(qH+1)·ε/(1-p).
• probOutput_hybridExpAtKey_trans_le_sim (G₂ → G₃): at a fixed key, replacing the honest-execution loop by the HVZK simulator loop costs at most qS·ζ_zk/(1-p).

• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Loss.lean: This new file defines cmaToNmaLoss and perKeyLoss, two noncomputable ℝ-valued functions representing the statistical loss of the CMA-to-NMA reduction for the Fiat-Shamir-with-aborts transform (after Theorem 3, CRYPTO 2023). cmaToNmaLoss accounts for adversarial hash query bounds qS and qH, per-key commitment-guessing probability ε, abort probability bound p, HVZK simulator error ζ_zk, and key-regularity failure δ; perKeyLoss is the per-key part without δ. The lemma cmaToNmaLoss_eq_perKeyLoss_add states cmaToNmaLoss = perKeyLoss + δ. These definitions are foundational to the security proof formalized in the surrounding modules.

• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/NMAReduction.lean: The file introduces the NMA reduction for the Fiat-Shamir-with-aborts security proof, defining the inner managed handler nmaOuterImpl, the outer runtime handler nmaInnerImpl, their linked composition nmaLinkImpl, and a redesigned state projection proj2 (mapping ((base,ghost),signed) to (baseEmbed (overlayCache base ghost), base)) that makes the per-step coupling exact. It proves per-step lemmas hproj2_unif, hproj2_ro, hproj2_ro_ghost_hit, hproj2_ro_fresh, and hproj2_sign, bundles them into hproj2_evalDist, then lifts to whole-run equality via evalDist_map_run_simulateQ_ghostNmaImpl_proj2 and managedRun_eq_link_run. It additionally provides helper lemmas simulateQ_unifSim_run, relTriple_graph_of_evalDist_map_eq, withCacheOverlay_verify_eq_of_miss, and probOutput_hybridVerifyCont_le_managed_verify, culminating in the bridge lemma probOutput_hybridExp_sim_le_managedRoNmaExp (proof incomplete in the diff) which bounds the simulated hybrid’s success probability by that of simulatedNmaAdv in the managed-RO NMA experiment. No sorry or admit appear in the provided diff.

• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/ReadRecording.lean: This new file (ReadRecording.lean) adds a read-recording handler deferredDrawReadImpl that extends the deferred-draw state DeferredState with an extra List Commit tracking every adversarial random-oracle read's commitment component. It defines the coupling invariant deferredReadInv and proves the per-query coupling theorem deferredDrawRead_step, the full run coupling theorem deferredDrawRead_run, the reduction deferredDraw_bad_le_readRecord (showing the deferred-draw run's read-time bad flag probability is ≤ the read-recording run's final-state predicate probability), and the Markov reduction readRecord_pred_le_expected_coincidences (bounding that final-state predicate by the expected coincidence count).

• VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/TapeFactorization.lean: The diff adds four theorems and two lemmas that extend the deferredDrawImpl security analysis to the deferredDrawReadImpl read-recording variant, showing the same deterministic and expected bounds hold for the recorded read-commit list, the drawn-list length, and the attempt count. The new theorems are:

• deferredDrawReadImpl_run_readlist_length_le — a deterministic bound that the recorded read-commit list length grows by at most qH (the number of random-oracle read queries), proved by induction on the oracle.

• deferredDrawReadImpl_step_expected_drawnlist_length_le — a per-step expected bound showing the drawn-list length expectation grows by at most 1/(1-p) on signing queries and 0 otherwise.

• deferredDrawRead_run_expected_drawnlist_length_le — an inductive extension of the step lemma to the full run, bounding the total expected drawn-list length by initial length + qSrem/(1-p).

• deferredDrawReadImpl_step_expected_attemptCount_le — the per-step expected bound for the sum drawnlist.length + signedlist.length, again charging 1/(1-p) only on signing queries.

The existing lemma deferredDrawRead_attemptKn_mean_le (already present in the file) is strengthened to use the new Z-based event structure and the deferredDrawReadImpl definition. The text also includes doc comments explaining the purpose of each theorem and how they relate to the underlying deferredDrawImpl proofs (the read-commit list is irrelevant to drawn/signed list bounds).

---

Last updated: 2026-08-09 08:28 UTC.

[dtumad]

I reviewed the PR-specific commit (ef1439a..16ac818d) separately from the four stacked dependencies. The finite NMA composition itself looks coherent: the real/short PRG hop instantiates the advertised distinguisher, and the CMA theorem goes through the managed-RO/plain-NMA equality before applying the short NMA bound. The asymptotic argument also appears mathematically valid under its stated family-wise assumptions, and its note that this is not yet a PPT/cost-model theorem is useful.

There are a couple of scope distinctions that I think would be worth making sharper before treating this as the ML-DSA headline:

1. euf_cma_security_of_nma_short is currently a theorem about the generic FiatShamirWithAbort signature type Option (Commitment × Response), where the commitment is carried in the signature. The published EasyCrypt Dilithium theorem first uses commitment recovery to reach that generic form; this adds one hash query per signing query, so its final loss uses qH + qS (and the resulting qH + qS + 1 term). The repository already documents exactly this distinction in MLDSA.cmaToNmaLoss in Security.lean. It might be clearest either to describe this theorem consistently as the commitment-carrying/standard-FS short-model composition, or to add the commitment-recovery bridge before calling it the end-to-end ML-DSA CMA headline. The same distinction also means the present CMA theorem is not yet the FIPS-keygen theorem; nma_security_fips is presently NMA-only.

2. nma_security_short_matrix discharges the seed-to-uniform-matrix MLWE bridge, which is useful, but its SelfTargetMSIS target is still the tailored mldsaSTMSISShort relation. Since the PR itself correctly says that the tailored-to-standard normal-form reduction remains follow-up work, wording such as “matrix-MLWE-facing” would be more precise than “literature-facing” for the whole theorem until that second bridge exists.

For comparison, the published mechanization makes both boundaries explicit: the final Dilithium theorem has the qH + qS loss, while the simplified-scheme proof contains the generic FS-with-aborts and commitment-recovery layers.

A smaller organizational suggestion: NonVacuity.lean is very candid that it proves only joint logical consistency at unit slacks and a no-query adversary. That certificate is fine as stated, but it may fit better as a test/example or a follow-up module rather than a new top-level LatticeCrypto.lean import; separating it and the asymptotic wrapper from the finite capstone would also make the semantic core easier to review and merge. The new file also just needs the standard blank line between its copyright header and imports.

Finally, the PR is currently conflicting because of its stacked history, so I would wait for #506/#507 to settle and then review the rebased, small diff. None of the points above calls for a maintainer-side semantic rewrite; they seem better left as author-directed framing/bridging choices.