feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228) by alik-eth · Pull Request #467 · Verified-zkEVM/VCVio

alik-eth · 2026-07-02T13:00:31Z

Closes #228.

EUF-CMA security of the proof-level ML-DSA scheme via the Fiat-Shamir-with-aborts CMA-to-NMA reduction (Theorem 3/Lemma 7, CRYPTO 2023), stated over the corrected short-secret Module-LWE model per review.

Stacked content: the Primitives.Laws repair + concrete witness is #479 and the WithAbort expectation-algebra roots landed in #465; this branch carries #479's files byte-identically — except Concrete/NonVacuity.lean, where the witness certificate is re-pointed at the live short-model consumers — and rebases (take-ours on that one file) once it merges.

The corrected model (review points 1 & 2)

mldsaMLWEShort / mldsaMatrixMLWE — the MLWE assumption with secrets and errors uniform on the η-bounded box (sampleShortVec), seed-based and uniform-matrix forms. The uniform-secret mldsaMLWE (information-theoretically zero advantage — the review's catch) is retired, along with honestSamplingSlack and the old headline chain.
Idealized short-key generation keygenShort samples ρ, K, (s₁, s₂) independently; the key-swap hop against it is an exact identity (no statistical slack). The material-based relation validKeyPairShort replaces the ∃-seed relation on the short path, and satisfiability certificates are banked: keygenShort_generable, keygen0_generable — every relation/pinning hypothesis pair in the headlines is inhabited by a kernel-checked witness.
Named idealizations with inspectable content replace caller-supplied inequalities: expandAIdealization (XOF-as-random-matrix; discharges the seed→matrix bridge via the proven advantage_mldsaMLWEShort_le_matrix + matrixLift) and expandSReplacement (PRG reading of ExpandSeed/ExpandS against the correct box marginal). Both docstrings disclose the unrestricted-quantifier caveat pending the cost model (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460).

Headlines (all `[propext, Classical.choice, Quot.sound]`)

nma_security_short — EUF-NMA ≤ MLWE(+εbridge) + SelfTargetMSIS, at keygenShort; needs no Primitives.Laws.
nma_security_short_matrix — the literature-facing packaging at the uniform-matrix problem (+εA).
nma_security_fips — the FIPS seed-derived keygen connected to the short model at cost +εPRG (expandSReplacement); the cross-scheme bridge is proven, not assumed.
euf_cma_security_of_nma_short — the CMA composition (bound: MLWE + STMSIS + cmaToNmaLoss), plus the re-pointed asymptotic corollary.

SelfTargetMSIS: point 4 became a soundness fix

Formalizing the requested algebraic bridge proved the tailored problem was easy: SelfTargetMSIS.Problem.isValid never received the hash preimage, so nothing bound the recomputed commitment to the hashed pair — at sampled parameters acceptance degenerated to two norm gates (z = 0 + empty hint won outright; this pre-dates the redesign). Fixed at the API: isValid now takes the HashInput, the experiment threads the cache-consistent preimage, and mldsaSTMSISShort carries the binding conjunct. The corrected characterization mldsaSTMSISShort_isValid_expandA_iff shows winning now requires a random-oracle fixed point — the genuine self-target task. The full algebraic iff (stmsisAlgebraicSolution, mldsaSTMSISShort_isValid_iff) states the matrix equation and norm bounds explicitly; the residual distance to the [A | I] normal form is documented in-file.

Honest scoping

HVZK obstruction (proved, documented): under the material relation, t₀ is not a function of pk (a small s₂ perturbation preserves t₁ but shifts t₀), so no exact-on-accept simulator covers all short-valid pairs with t₁-only public keys — consistent with the literature stating HVZK with full t public. The CMA wrapper therefore keeps HVZK as an abstract satisfiable hypothesis; the seed-relation HVZK theorem (idsWithAbort_hvzk_real) remains for the FIPS path.
Scope section documents the idealized proof-level model (point 5); no PPT/cost tracking yet (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460) — the asymptotic statement quantifies numerical sequences only (point 3).
Module split per point 6: WithAbort/Security → 10 phase modules, GhostBodies → 5.

Verification

Full CI library set green on v4.31.0; zero non-sorry warnings; every headline and certificate kernel-checked; the SIS namespace (Falcon's) byte-unchanged by the API fix.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

github-actions · 2026-07-02T13:00:51Z

🤖 PR Summary

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

Summary

This PR (feat) completes the EUF-CMA security proof for the proof-level ML-DSA scheme via the Fiat-Shamir-with-aborts CMA-to-NMA reduction (Theorem 3/Lemma 7, CRYPTO 2023). It states the result over a corrected short-secret Module-LWE model, following a review that identified a flaw (the original mldsaMLWE had uniform secrets, giving information-theoretically zero advantage).

Corrected Security Model

New assumptions: mldsaMLWEShort / mldsaMatrixMLWE — MLWE with secrets and errors uniform on the η-bounded box (sampleShortVec). The uniform-secret mldsaMLWE is retired.
Idealized key generation: keygenShort samples ρ, K, (s₁, s₂) independently. The material-based relation validKeyPairShort replaces the existential-seed relation. Satisfiability certificates (keygenShort_generable, keygen0_generable) are provided.
Named idealizations with inspectable content: expandAIdealization (XOF-as-random-matrix) and expandSReplacement (PRG reading of ExpandSeed/ExpandS). Both docstrings note the unrestricted-quantifier caveat pending the cost model (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460).

Headline Theorems (all `[propext, Classical.choice, Quot.sound]`)

nma_security_short — EUF-NMA ≤ MLWE(+εbridge) + SelfTargetMSIS, at keygenShort; requires no Primitives.Laws.
nma_security_short_matrix — Literature-facing packaging at the uniform-matrix problem (+εA).
nma_security_fips — FIPS seed-derived keygen connected to the short model at cost +εPRG (expandSReplacement).
euf_cma_security_of_nma_short — The CMA composition (bound: MLWE + STMSIS + cmaToNmaLoss).

SelfTargetMSIS Soundness Fix

Formalizing the algebraic bridge proved the tailored problem was easy: SelfTargetMSIS.Problem.isValid never received the hash preimage, so nothing bound the recomputed commitment to the hashed pair. Fixed: isValid now takes the HashInput, the experiment threads the cache-consistent preimage, and mldsaSTMSISShort carries the binding conjunct.

Infrastructure & Non-Vacuity

Primitives.Laws witnesses: Concrete/Laws.lean provides 13 of 14 fields for the concrete ML-DSA instance. Concrete/NonVacuity.lean provides a logical consistency certificate (seedRevealingPrims_laws) and an existential witness (mldsa_laws_inhabited), though the witness is not a secure instantiation.
Hypothesis non-vacuity: MLDSA/NonVacuity.lean proves the premises of euf_cma_security_of_nma_short are inhabited (trivial witnesses, no security claim).
Refactored samplers: Concrete/Sampling.lean refactors three rejection-sampling loops to fuel-bounded structural recursion and provides structural output bounds (sampleInBall_norm, sampleEtaPoly_norm, expandS_bound).

Ghost-Body & Security Proof Infrastructure (Fiat-Shamir with Aborts)

The WithAbort/Security module is split into 10 phase modules; GhostBodies into 5. Key additions:

Ghost-layer hybrid handler: ghostHybridImpl (ghost layer for the hybrid argument), ghostNmaImpl (layered ghost-tagged NMA handler), with overlay projections and support invariants.
Hybrid hop lemmas (HopLemmas.lean): Four main lemmas bridging the standard unforgeability experiment to the simulated run via three hybrid hops (G₀→G₁→G₂→G₃).
NMA reduction (NMAReduction.lean): Coupling between nested managed simulation and ghost-tagged NMA implementation via proj2.
Ghost-read charge (GhostReadCharge.lean): Bounds the overall bad-flag probability by ENNReal.ofReal (qS·(qH+1)·ε/(1−p_abort)).
Read recording & tape factorization (ReadRecording.lean, TapeFactorization.lean): First-moment reductions bounding deferred-draw bad flag probability.
Loss.lean: Defines cmaToNmaLoss as a sum of four terms.
Assembly.lean: Completes the CMA-to-NMA proof with headline euf_cma_to_nma.

Other Changes

Primitives.lean: Relaxed expandMask_bound (to p.gamma1), weakened w1Encode_injective to Set.InjOn, removed the field expandS_honest_sampling.
Concrete/Encoding.lean: Adds roundtrip/injectivity proofs for encoding/decoding (simpleBitUnpackPoly_simpleBitPackPoly, w1Encode_injOn).
Concrete/Rounding.lean: Proves highBits_coeff_val_lt_m (valid commitment window).
Ring/Norms.lean: Adds cInfNorm_mul_le (bound for negacyclic product — core of the challenge-product bound).
VCVio.lean: Adds imports for the new submodules.
LatticeCrypto.lean: Adds imports for new ML-DSA modules.
Documentation fix in HashSig/SLHDSA/Security.lean: Updates comment to cite the correct theorem.

Caveats

Sorry/admit: None reported in the per-file summaries. The file summaries for ShortIntegerSolution.lean, Security.lean, Security.lean (the main MLDSA security file? — see missing summaries), GhostBodies.lean, Bodies.lean, CouplingEngine.lean, and HiddenReadFold.lean were not parseable; however, the available summaries explicitly state 'No sorry or admit appear' for all parsed files.
Missing per-file summaries for several key files (LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean, LatticeCrypto/MLDSA/Security.lean, VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies.lean, VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Bodies.lean, VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean, VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean, VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HiddenReadFold.lean) could not be parsed from the provided data. The overview must be read with this incompleteness in mind.
The HiddenReadFold.lean summary is truncated. The ShortIntegerSolution.lean summary could not be parsed. The Security.lean (MLDSA) and Security.lean (WithAbort) summaries were also not parseable. The GhostBodies.lean and Bodies.lean summaries are unavailable.
The split into ghost-body and security modules is extensive and this description only summarizes the major new definitions. The full scope of the GhostBodies and Security submodules is best understood by reviewing the file structure.

CI & Build

Full CI green on v4.31.0; zero non-sorry warnings; every headline and certificate kernel-checked; the SIS namespace (Falcon's) byte-unchanged.

Statistics

Metric	Count
📝 Files Changed	33
✅ Lines Added	14649
❌ Lines Removed	633

Lean Declarations

✏️ Removed: 12 declaration(s)

LatticeCrypto/MLDSA/Security.lean (1)

theorem euf_cma_security

LatticeCrypto/MLDSA/SecurityNMA.lean (8)

def keygen1 : ProbComp (PublicKey p prims × SecretKey p)
noncomputable def distinguisherB
noncomputable def mldsaMLWE (p : Params) (prims : Primitives p)
noncomputable def mldsaSTMSIS (M : Type) :
private theorem stmsis_tail_le
theorem nmaAdvantage_keygen1_le_stmsis
theorem nma_keyswap_hop (h_laws : Primitives.Laws prims nttOps)
theorem nma_security (h_laws : Primitives.Laws prims nttOps)

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: 393 declaration(s)

LatticeCrypto/MLDSA/Concrete/Encoding.lean (27)

private def packBitsList (vals : Array Nat) (width : Nat) : List Nat
private theorem array_getD_eq_getElem {α : Type} (a : Array α) {i : Nat}
private theorem ba_getElem?_getD (ba : ByteArray) (i : Nat) :
private theorem bitOf_lt_two (b : UInt8) (j : Nat) : bitOf b j < 2
private theorem bitOf_packByte_fin :
private theorem bitsToBytes_size_of_mod (bits : Array Nat) (h : bits.size % 8 = 0) :
private theorem byteArrayToList_injective : Function.Injective byteArrayToList
private theorem bytearray_mk_getByteD {arr : Array UInt8} {i : Nat} (h : i < arr.size) :
private theorem bytesToBits_bitsToBytes_getD {bits : Array Nat} {i : Nat}
private theorem bytesToBits_getD_lt_two (bytes : ByteArray) (i : Nat) :
private theorem forIn_push_flatten (l : List Nat) (g : Nat → List Nat) (a : Array Nat) :
private theorem getByteD_bitsToBytes (bits : Array Nat) (b : Nat)
private theorem getD_flatMap_const_len {α} [Inhabited α] (n width : Nat) (h : Nat → Nat → α)
private theorem getElem_flatten_const {α} (chunks : List (List α)) (sz : Nat)
private theorem ofDigits_bits (v width : Nat) (hv : v < 2 ^ width) :
private theorem packBitsList_getD (vals : Array Nat) (width i bit : Nat)
private theorem packBitsList_length (vals : Array Nat) (width : Nat) :
private theorem packNatArray_eq (vals : Array Nat) (width : Nat) :
private theorem packPolyVector_data_toList {k : Nat} (v : Vector Rq k) (pack : Rq → ByteArray) :
private theorem simpleBitPackPoly_size (f : Rq) (m : Nat) :
private theorem sliceByteArray_packPolyVector {k : Nat} (v : Vector Rq k) (pack : Rq → ByteArray)
private theorem unpackNatArray_getD_lt (count width : Nat) (bytes : ByteArray) (i : Nat) :
private theorem unpackNatArray_packNatArray_getD (vals : Array Nat) (width i : Nat)
private theorem unpackPolyVector_packPolyVector {k chunkSize : Nat} (v : Vector Rq k)
theorem bitUnpackPoly_get (bytes : ByteArray) (a b : ℤ) (i : Fin ringDegree) :
theorem simpleBitUnpackPoly_simpleBitPackPoly (f : Rq) (b : Nat)
theorem w1Encode_injOn (p : Params) :

LatticeCrypto/MLDSA/Concrete/Laws.lean (17)

private theorem approved_gamma1_width (hp : p.isApproved) :
private theorem highBits_coeff_val_lt_width (hp : p.isApproved) (r : Rq) (c : Fin ringDegree) :
theorem bitUnpackPoly_z_cInfNorm_le (bytes : ByteArray) (γ : ℕ)
theorem concrete_expandMask_bound (hp : p.isApproved) (rhoDoublePrime : Bytes 64) (kappa : ℕ) :
theorem concrete_expandS_bound (rhoPrime : Bytes 64) :
theorem concrete_hide_low (hp : p.isApproved) (r s : Rq) (b : ℕ)
theorem concrete_highBitsShift_injective (hp : p.isApproved) :
theorem concrete_high_low_decomp (r : Rq) :
theorem concrete_lowBits_bound (hp : p.isApproved) (r : Rq) :
theorem concrete_power2Round_bound (r : Rq) :
theorem concrete_power2Round_decomp (r : Rq) :
theorem concrete_sampleInBall_norm (cTilde : CommitHashBytes p) :
theorem concrete_sampleInBall_smul_bound
theorem concrete_transform : NTTRingLaws concreteNTTRingOps
theorem concrete_useHint_makeHint (hp : p.isApproved) (z r : Rq) (hz : polyNorm z ≤ p.gamma2) :
theorem concrete_w1Encode_injOn (hp : p.isApproved) :
theorem polyNorm_eq_cInfNorm (f : Rq) : polyNorm f = LatticeCrypto.cInfNorm f

LatticeCrypto/MLDSA/Concrete/NonVacuity.lean (3)

def seedRevealingPrims (p : Params) : MLDSA.Primitives p
theorem mldsa_laws_inhabited :
theorem seedRevealingPrims_laws (p : Params) (hp : p.isApproved) :

LatticeCrypto/MLDSA/Concrete/Rounding.lean (1)

theorem highBits_coeff_val_lt_m (p : Params) (hp : p.isApproved) (r : Rq) (i : Fin ringDegree) :

LatticeCrypto/MLDSA/Concrete/Sampling.lean (35)

private def EtaInv (eta : ℕ) (c : Array ℤ) : Prop
private def countNZ (out : Array Coeff) : ℕ
private def rejEtaCoeffsAux (eta : Nat) (stream : ByteArray) :
private def rejEtaStep (eta : Nat) (byte : Nat) (coeffs : Array ℤ) : Array ℤ
private def rejUniformCoeffsAux (stream : ByteArray) :
private def sampleInBallFindChosen (stream : ByteArray) (i : Nat) :
private def sampleInBallLoop (stream : ByteArray) (signs hi : Nat) :
private def sampleInBallStep (stream : ByteArray) (signs : Nat) (i : Nat)
private theorem EtaInv_condPush (eta : ℕ) (c : Array ℤ) (v : ℤ) (cond : Prop) [Decidable cond]
private theorem EtaInv_mkEmpty (eta : ℕ) : EtaInv eta (Array.mkEmpty ringDegree)
private theorem centeredRepr_zero_cast_le (eta : ℕ) :
private theorem countNZ_replicate_zero : countNZ (Array.replicate ringDegree (0 : Coeff)) = 0
private theorem countNZ_sampleInBallLoop_le (stream : ByteArray) (signs : ℕ) (p : Params) :
private theorem countNZ_set!_eq (out : Array Coeff) (a : ℕ) (ha : a < ringDegree)
private theorem findChosen_le (stream : ByteArray) (i : ℕ) :
private theorem getD_push_or {α : Type*} [Inhabited α] (a : Array α) (v d : α) (j : ℕ) :
private theorem getD_set!_ne (out : Array Coeff) (a : ℕ) (u : Coeff) (j : ℕ) (hj : j ≠ a) :
private theorem getD_set!_or {α : Type*} [Inhabited α] (a : Array α) (i : ℕ) (v d : α) (j : ℕ) :
private theorem getD_set!_self (out : Array Coeff) (a : ℕ) (ha : a < out.size) (u : Coeff) :
private theorem l1Norm_ofFn_eq_countNZ (coeffs : Array Coeff) :
private theorem loop_countNZ_le (stream : ByteArray) (signs hi : ℕ) (hhi : hi ≤ ringDegree) :
private theorem polyNorm_eq_cInfNorm' (f : Rq) : polyNorm f = LatticeCrypto.cInfNorm f
private theorem rejEtaCoeffsAux_mem (eta : ℕ) (stream : ByteArray) :
private theorem rejEtaStep_mem (eta byte : ℕ) (coeffs : Array ℤ)
private theorem requireFullEtaSample_mem (eta : ℕ) (coeffs : Array ℤ) (hInv : EtaInv eta coeffs) :
private theorem sampleInBallLoop_mem (stream : ByteArray) (signs hi : ℕ) :
private theorem sampleInBallStep_mem (stream : ByteArray) (signs i : ℕ) (out : Array Coeff)
private theorem step_countNZ_le (stream : ByteArray) (signs i : ℕ) (out : Array Coeff)
private theorem step_fresh (stream : ByteArray) (signs i : ℕ) (out : Array Coeff) (pos signIdx : ℕ)
private theorem step_size (stream : ByteArray) (signs i : ℕ) (out : Array Coeff) (pos signIdx : ℕ)
theorem expandS_bound (rhoPrime : Bytes 64) (p : Params) :
theorem sampleEtaPoly_norm (eta : ℕ) (seed : Bytes 64) (nonce : ℕ) :
theorem sampleInBall_coeff_mem (p : Params) (seed : CommitHashBytes p) (i : Fin ringDegree) :
theorem sampleInBall_l1Norm (p : Params) (seed : CommitHashBytes p) :
theorem sampleInBall_norm (p : Params) (seed : CommitHashBytes p) :

LatticeCrypto/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 : ℕ) :

LatticeCrypto/MLDSA/Scheme.lean (3)

@[simp] theorem validKeyPairShort_eq_true_iff (pk : PublicKey p prims) (sk : SecretKey p) :
def identificationSchemeShort
noncomputable def validKeyPairShort (pk : PublicKey p prims) (sk : SecretKey p) : Bool

LatticeCrypto/MLDSA/SecurityNMA.lean (38)

def expandAIdealization (p : Params) (prims : Primitives p)
def expandSReplacement (εPRG : ℝ) : Prop
def hrFips :
def stmsisAlgebraicSolution (aHat : TqMatrix p.k p.l) (pk : PublicKey p prims)
lemma advantage_mldsaMLWEShort_le_matrix {εA : ℝ}
lemma mem_support_sampleShortVec {k b : ℕ} [SampleableType (RqVec k)] {v : RqVec k}
lemma polyVecBounded_zero (k b : ℕ) : polyVecBounded (0 : RqVec k) b
noncomputable def distinguisherBShort
noncomputable def extractorCShort [Inhabited (Commitment p prims)] [Inhabited (Response p prims)]
noncomputable def hrShort :
noncomputable def keygenShort : ProbComp (PublicKey p prims × SecretKey p)
noncomputable def keygenShort1 : ProbComp (PublicKey p prims × SecretKey p)
noncomputable def matrixLift
noncomputable def mldsaMLWEShort (p : Params) (prims : Primitives p)
noncomputable def mldsaMatrixMLWE (p : Params)
noncomputable def mldsaSTMSISShort (M : Type) :
noncomputable def nmaAdvantageShort
noncomputable def nmaGameShort
noncomputable def sampleShortVec (k b : ℕ) [SampleableType (RqVec k)] : ProbComp (RqVec k)
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_laws : Primitives.Laws prims nttOps)
theorem keygen0_generable :
theorem keygenShort_generable :
theorem mldsaSTMSISShort_isValid_expandA_iff (pk : PublicKey p prims)
theorem mldsaSTMSISShort_isValid_iff (h_laws : Primitives.Laws prims nttOps)
theorem negligible_ofReal_geometric (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) :
theorem nmaAdvantage_keygenShort1_le_stmsis
theorem nmaGameShort_eq_keygen_bind
theorem nma_keyswap_hop_short
theorem nma_security_fips
theorem nma_security_short_matrix (maxAttempts : ℕ) (εA : ℝ)
theorem nma_security_short

LatticeCrypto/Ring/Norms.lean (6)

private def intConvCoeff (f g : Fin n → ZMod q) (k : Fin n) : ℤ
private theorem intConvCoeff_natAbs_le (f g : Fin n → ZMod q) (k : Fin n) (bg : ℕ)
private theorem mul_get_eq_convCoeff (f g : (vectorNegacyclicRing (ZMod q) n).Poly) (i : Fin n) :
private theorem negacyclicConvCoeff_eq_intCast (f g : Fin n → ZMod q) (k : Fin n) :
theorem cInfNorm_mul_le (f g : (vectorNegacyclicRing (ZMod q) n).Poly) :
theorem l1Norm_eq_sum (p : Poly (ZMod q) n) :

LatticeCrypto/Ring/Transform.lean (1)

theorem coeffScalarVecMul_get {k} (c : ring.Poly) (v : PolyVec ring.Poly k) (j : Fin k) :

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)

…and 243 more not listed.

✏️ Affected: 2 declaration(s) (line number changed)

private def rejEtaCoeffs (eta : Nat) (stream : ByteArray) : Array ℤ in LatticeCrypto/MLDSA/Concrete/Sampling.lean moved from L92 to L141
private def rejUniformCoeffs (stream : ByteArray) : Array Coeff in LatticeCrypto/MLDSA/Concrete/Sampling.lean moved from L55 to L75

sorry Tracking

✅ Removed: 2 `sorry`(s)

LatticeCrypto/MLDSA/Security.lean (1)

theorem euf_cma_security (L363)

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

theorem euf_cma_bound (L119)

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 (+1452/-329)
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean (+1396/-0)
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean (+1892/-0)
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/NMAReduction.lean (+1041/-0)
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/TapeFactorization.lean (+2566/-0)

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

📄 **Per-File Summaries**

HashSig/SLHDSA/Security.lean: The comment block in HashSig/SLHDSA/Security.lean was updated to replace a vague reference to LatticeCrypto.MLDSA.Security.euf_cma_security with a precise citation of the theorem LatticeCrypto.MLDSA.euf_cma_security_of_nma_short, clarifying the lattice analogue used for the deferred proof. The wording now reads: 'multi-target → single-target p-fold loss are research-level and deferred). The lattice analogue is the sound EUF-CMA bound LatticeCrypto.MLDSA.euf_cma_security_of_nma_short.' This change improves the documentation by explicitly naming the relied-upon result, making the dependency clearer for future formalization efforts.
LatticeCrypto.lean: Added imports for LatticeCrypto.MLDSA.Concrete.Laws, LatticeCrypto.MLDSA.Concrete.NonVacuity, and LatticeCrypto.MLDSA.NonVacuity, making new ML-DSA law lemmas and non-vacuity proofs available project-wide.
LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The SelfTargetMSIS Prob...admit were introduced.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
LatticeCrypto/MLDSA/Concrete/Encoding.lean: Adds a large block of proofs establishing roundtrip and injectivity properties for the encoding/decoding pipeline. The new public theorems are bitUnpackPoly_get (each coefficient lies in the expected integer window), simpleBitUnpackPoly_simpleBitPackPoly (simpleBitUnpackPoly inverts simpleBitPackPoly on polynomials whose coefficients fit in the bit width), and w1Encode_injOn (the w1Encode function is injective on the set of commitment vectors whose every coefficient is below the w1 packer's bit capacity). Supporting private lemmas cover bit‑level helpers, packNatArray/unpackNatArray roundtrip (unpackNatArray_packNatArray_getD), and vector‑level slicing (unpackPolyVector_packPolyVector). No sorry or admit appear.
LatticeCrypto/MLDSA/Concrete/Laws.lean: This file (LatticeCrypto/MLDSA/Concrete/Laws.lean) is newly created and provides standalone, provable concrete_* theorem witnesses for 13 of the 14 fields in the abstract Primitives.Laws interface, targeting the concrete concretePrimitives ML-DSA instance. Key contributions include: eight algebraic/rounding fields (concrete_transform, concrete_high_low_decomp, concrete_lowBits_bound, concrete_hide_low, concrete_highBitsShift_injective, concrete_useHint_makeHint, concrete_power2Round_decomp, concrete_power2Round_bound) proved via existing concrete rounding lemmas (Concrete/Rounding.lean) and NTT laws (Concrete/NTT.lean) bridged by the identity polyNorm_eq_cInfNorm; two byte-encoding fields (concrete_expandMask_bound, concrete_w1Encode_injOn) proved using decoder range bounds and packer properties from Concrete/Encoding.lean; two sampler-bound fields (concrete_sampleInBall_norm, concrete_expandS_bound) discharged via fuel induction on the structural-recursion samplers in Concrete/Sampling.lean; and the challenge-product bound (concrete_sampleInBall_smul_bound) assembled from a generic negacyclic-convolution infinity-norm bound (cInfNorm_mul_le), the challenge ℓ₁ count (sampleInBall_l1Norm), and component law (coeffScalarVecMul_get). The file explicitly notes that one abstract field (keyVector_t0_determined, a random-oracle modeling assumption) remains unproven by design — no sorry or admit is used, and no full aggregate Primitives.Laws witness is constructed.
LatticeCrypto/MLDSA/Concrete/NonVacuity.lean: Added file NonVacuity.lean providing a logical consistency certificate for the hypothesis MLDSA.Primitives.Laws (issue Proof obligation for cmaToNmaLoss_bound in LatticeCrypto/MLDSA/Security.lean #228). Defines seedRevealingPrims, a variant of concretePrimitives whose expandSeed component returns the seed as the public ρ, and proves seedRevealingPrims_laws that this bundle satisfies all thirteen concrete_* lemmas and the keyVector_t0_determined condition. This is used to give mldsa_laws_inhabited, an existential witness ⟨mldsa44, seedRevealingPrims mldsa44, …⟩ showing that the Laws hypothesis is non‑vacuous. The file explicitly notes that this witness is not a secure instantiation and inherits the concrete NTT native_decide axiom from concrete_transform.
LatticeCrypto/MLDSA/Concrete/Rounding.lean: Added a new theorem highBits_coeff_val_lt_m which proves that for approved parameters each coefficient of highBits lies in the valid commitment window [0, (q-1)/(2*gamma2)-1] — that is, its ZMod value is strictly below (q-1)/(2*gamma2). This establishes the range produced by Algorithm 37 and the domain on which the w1 packer is injective. The proof uses highBitsCoeff_lt_m and BalancedDecomp.ofApproved.
LatticeCrypto/MLDSA/Concrete/Sampling.lean: The file refactors three rejection-sampling loops (rejUniformCoeffs, rejEtaCoeffs, and sampleInBall) from imperative while loops to fuel-bounded structural recursion, introducing auxiliary functions (rejUniformCoeffsAux, rejEtaCoeffsAux, rejEtaStep, sampleInBallFindChosen, sampleInBallStep, sampleInBallLoop) that replicate the original loop guards and per-iteration logic exactly. It adds a large set of theorems establishing structural output bounds: polyNorm_eq_cInfNorm' (equality of two norm definitions), sampleInBall_coeff_mem and sampleInBall_norm (every coefficient of sampleInBall is -1, 0, or 1), sampleInBall_l1Norm (ℓ₁ norm of the challenge is at most τ), sampleEtaPoly_norm (each coefficient of sampleEtaPoly is bounded by η), and expandS_bound (both halves of expandS are η-bounded). These theorems are supported by internal lemmas (getD_set!_or, getD_push_or, countNZ, EtaInv) that track values through array updates and fuel recursions. The changes also include a set_option maxRecDepth 4000 to accommodate deeper recursion proofs.
LatticeCrypto/MLDSA/NonVacuity.lean: This new file proves the non-vacuity (inhabitance) of the hypothesis frontier of MLDSA.euf_cma_security_of_nma_short by constructing trivial witnesses for all its premises at arbitrary parameters, with no quantitative security content. It defines a never-aborting simulator neverAbortSim, the good-key event honestNoAbortGood, and a forger trivialForger that makes no queries, and supplies supporting lemmas (neverAbortSim_hvzk, probOutput_none_neverAbortSim, trivialForger_signHashQueryBound, expandAIdealization_one). The main theorem mldsa_short_cma_hyps_inhabited simultaneously discharges every hypothesis (hGen, hStmsis, hhvzk at ζ_zk=1, hGood/hGuess/hAbort/hAbortSim at δ=1/ε=1/p_abort=0, hQ at qS=qH=0, and hMlweBridge at εbridge=1), and trivial_euf_cma_security_of_nma_short instantiates the conditional headline to obtain a trivial bound, confirming logical consistency without any security claim.
LatticeCrypto/MLDSA/Primitives.lean: In Primitives.Laws, the law expandMask_bound was relaxed: the bound changed from p.gamma1 - 1 to p.gamma1, with the docstring updated to note that ExpandMask output coefficients lie in [-γ₁ + 1, γ₁]. The law w1Encode_injective was weakened from global injectivity to Set.InjOn on the set of commitment vectors whose every component is in the image of highBits, reflecting that the encoder is only injective on that valid range. The law expandS_honest_sampling, which modeled honest secret sampling via random oracles, was completely removed, and the comment on keyVector_t0_determined was updated to remove reference to that removed field.
LatticeCrypto/MLDSA/Scheme.lean: This diff adds a new validKeyPairShort predicate for ML-DSA key pairs, which characterizes validity via existence of bounded-norm secret vectors (s1, s2) and seeds (rho, key) such that the public key material t = A·s1 + s2 is correctly split by Power2Round and the commitment root tr is correctly hashed — without requiring the material to derive from a deterministic seed. A validKeyPairShort_eq_true_iff theorem provides the equivalence with the existential condition, and a new identificationSchemeShort constant reuses the same commit/respond/verify algorithms as the existing identificationScheme but indexed by validKeyPairShort, enabling security statements that assume material-valid key generation.
LatticeCrypto/MLDSA/Security.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The statistical loss for...tivity side-conditions.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
LatticeCrypto/MLDSA/SecurityNMA.lean: This diff restructures LatticeCrypto/MLDSA/SecurityNMA.lean from a proof of the MLWE key-swap hop (Lemma 7, Step 1) into a full short-key MLWE reduction for ML-DSA EUF-NMA security. The changes add: the short-secret sampler sampleShortVec and idealized key generators keygenShort / keygenShort1 (replacing keygen0 / keygen1); the expandSReplacement PRG/XOF assumption for FIPS-keygen transfer; the expandAIdealization assumption and the bridge lemma advantage_mldsaMLWEShort_le_matrix from seed-based mldsaMLWEShort to matrix-based mldsaMatrixMLWE; the short-model NMA game nmaGameShort and its distinguisher distinguisherBShort; the exact key-swap inequality nma_keyswap_hop_short (which no longer relies on expandS_honest_sampling); and the generable-relation certificates keygenShort_generable / keygen0_generable. The module docstring expands to cover the short-key model, the algebraic content of mldsaSTMSISShort, and the scope of idealizations.
LatticeCrypto/Ring/Norms.lean: The diff adds a new theorem l1Norm_eq_sum that expresses l1Norm as the sum of the centered absolute values of the coefficients. It then introduces a private infrastructure (intConvCoeff, negacyclicConvCoeff_eq_intCast, intConvCoeff_natAbs_le, mul_get_eq_convCoeff) to prove the public theorem cInfNorm_mul_le, which bounds the centered infinity norm of a negacyclic product by l1Norm f * cInfNorm g. This bound is the algebraic core of the ML‑DSA challenge‑product bound. The omit [NeZero q] clause is used in two private lemmas to drop the NeZero assumption.
LatticeCrypto/Ring/Transform.lean: Added theorem coeffScalarVecMul_get stating that for any coefficient c : ring.Poly and vector v : PolyVec ring.Poly k, the j-th entry of coeffScalarVecMul c v equals c * v.get j. This follows from the transform being a ring isomorphism (laws.toHat_mul and laws.fromHat_toHat).
VCVio.lean: The diff adds import lines for two new submodules of VCVio.CryptoFoundations.FiatShamir.WithAbort: the GhostBodies family (Bodies, BodyBounds, GhostLayer, NMAHandler, Projections) and the Security family (Assembly, BodyHops, CouplingEngine, GhostReadCharge, HiddenReadFold, HopLemmas, Loss, NMAReduction, ReadRecording, TapeFactorization). This makes the theorems, definitions, and structures in those modules available in VCVio.lean; no definitions, proofs, or sorry/admit decls are modified or added in this file itself.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new module GhostBo...ir.WithAbort.Security.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Bodies.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file introduces...mit` statements appear.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean: This new file introduces the ghost-layer body bounds for the Fiat-Shamir with aborts reduction. It defines the collision budget signCollisionBound (with lemmas signCollisionBound_zero, signCollisionBound_succ, signCollisionBound_mono, signCollisionBound_eq) and per-attempt abort and collision bounds (tsum_probOutput_commit_mul_abort_le, probEvent_commit_hit_le). The core deferred-sampling ghost read is formalized as lazyGhostFire and eagerMultiReadBad, with commutation lemmas (lazyGhostFire_one_eq, probOutput_lazyGhostFire_one, probEvent_ghostHybridImpl_read_bad_single_eq_lazyFire, probOutput_eagerMultiReadBad_eq_lazyFire_or, probOutput_eagerMultiReadBad_empty_eq_lazyFire) and a charged-step bound (probOutput_lazyGhostFire_true_le, probOutput_lazyGhostFire_true_le_enncard). The lazy ghost hybrid handler lazyGhostHybridImpl is defined, and its equivalence to the eager handler on uniform and signing queries is shown (lazyGhostHybridImpl_run_unif_eq, lazyGhostHybridImpl_run_sign_eq). Eager-run bad-flag absorption and read-step HIT collapses are proved (support_simulateQ_ghostHybridImpl_bad, probEvent_simulateQ_ghostHybridImpl_bad_eq_true, tsum_ghostHybridImpl_read_hit_eq, tsum_ghostHybridImpl_read_step_split). The two body-level cores of the Sign→Prog hop are established: the within-signing-query TV-distance bound ofReal_tvDist_run_fsAbortSignLoop_progSignBody_le and expected cache growth of the reprogramming loop tsum_probOutput_run_progSignBody_mul_enncard_le. Finally, the ghost-layer growth of the reprogramming loop is bounded via run_ghostSignBody_succ and tsum_probOutput_run_ghostSignBody_mul_ghost_enncard_le. No sorry or admit appear in the diff.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/GhostLayer.lean: The new file GhostLayer.lean adds ghost-layer machinery for the hybrid argument in the Fiat-Shamir with aborts reduction. It defines ghostSignBody, a signing body over a layered cache (real and ghost), and proves projection lemmas run_ghostSignBody_overlay and run_ghostSignBody_fst that recover the prog and trans signing bodies, along with helper lemmas overlayCache_cacheQuery_uncacheQuery, overlayCache_cacheQuery_ghost, toSet_uncacheQuery_subset, enncard_uncacheQuery_le, overlayCache_apply_ghost_some, overlayCache_apply_ghost_none, overlayCache_cacheQuery_real_of_ghost_none, overlayCache_empty, and randomOracle_run_eq_roStep. It further defines the instrumented hybrid handler ghostHybridImpl (parameterized by progSide) with a monotone bad flag, the ghost-blind handler ghostBlindImpl (a wrapper for the Trans-side handler), and proves agreement and monotonicity lemmas ghostHybridImpl_agree_good, ghostHybridImpl_bad_mono, ghostBlindImpl_eq_ghostHybridImpl_false, ghostBlindImpl_agree_good, and ghostBlindImpl_bad_mono. Finally, it defines the run-level hybrid handlers hybridBaseImpl and hybridSignImpl on a hybrid state of a cache and signed-message list.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/NMAHandler.lean: This diff adds the entire file VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/NMAHandler.lean, which defines the layered ghost-tagged NMA (non-malleability) handler for the Fiat-Shamir with aborts reduction. It introduces the key definitions ghostSignProgramCont, simGhostSignBody, the baseEmbed embedding, and the ghostNmaImpl query handler, along with the NmaGhostState abbreviation. The file proves several theorems establishing the overlay projection (run_ghostSignProgramCont_overlay, run_simGhostSignBody_overlay, ghostNmaImpl_proj_hybrid, map_run_simulateQ_ghostNmaImpl_overlay) and ghost-domain support invariants (simGhostSignBody_support_ghost, ghostNmaImpl_preserves_signed_inv, ghostNmaImpl_run_signed_inv), which are essential for coupling the layered run to the ordinary hybrid run. It also defines the signLiveCollision predicate and lemma not_signLiveCollision_iff, which formalize the live-read/sign-program collision event that gates the divergence bound in the reduction.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Projections.lean: This new file in the GhostBodies directory of the Fiat-Shamir with aborts development provides the core projection lemmas that relate the ghost-instrumented hybrid implementation to the real hybrid games. It defines blindStepProj, the observable projection of a ghost-blind step, and proves the critical blindStepProj_map_ghostBlindImpl_indep lemma, which establishes that the output, real cache, signed list, and bad flag of a single ghost-blind step are independent of the ghost layer's stored values (only the domain of the ghost cache matters). The file also proves the per-step overlay projection ghostHybridImpl_proj_prog (projecting the Prog-side ghost handler onto the Prog hybrid handler) and the ghost-forgetting projection ghostHybridImpl_proj_trans (projecting the Trans-side ghost handler onto the Trans hybrid handler). Finally, it establishes the ghost-domain invariant ghostHybridImpl_preserves_signed_inv, which states that along any ghost-instrumented run, every key in the ghost cache has its message component recorded in the signed list.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The file has been almost...orry`) no longer exist.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Assembly.lean: Adds the module Assembly.lean completing the CMA-to-NMA security proof for Fiat-Shamir with aborts. It defines simulatedEufNmaAdv (a plain EUF‑NMA adversary obtained by forgetting the managed cache), proves managedRoNmaExp_simulatedNmaAdv_eq_eufNmaExp (the managed‑RO NMA experiment equals the plain EUF‑NMA experiment under Option B), states the headline theorem euf_cma_to_nma (bounding CMA advantage by managed‑RO NMA success plus cmaToNmaLoss), and provides simulatedNmaAdv_nmaHashQueryBound (showing the reduction issues at most qH live hash queries). No sorry or admit appear.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/BodyHops.lean: This new file adds the core components of the Trans→Sim hop and the hybrid experiment for the CMA-to-NMA security reduction of Fiat-Shamir with aborts. It defines the lemma tvDist_run_transSignBody_simSignBody_le bounding the total-variation distance between the real and simulated signing bodies, the noncomputable def hybridExpAtKey for the hybrid unforgeability experiment at a fixed key pair, and the noncomputable def hybridVerifyCont for the verification-and-freshness continuation. Three auxiliary lemmas are also provided: hybridExpAtKey_eq_run_bind expressing the experiment as a bind, hybridVerifyCont_cache_congr showing cache insensitivity away from the forged message, and probOutput_true_hybridVerifyCont_of_mem showing that success probability is zero when the message was already signed.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean: Summary unavailable — error: Model 'deepseek/deepseek-v4-flash' hit the output token cap before producing complete structured output; increase max_tokens or lower the thinking budget.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/GhostReadCharge.lean: This new file, GhostReadCharge.lean, adds the lazy-side ghost-read charge lemmas for the EUF‑CMA security proof of the Fiat‑Shamir‑with‑abort transform. It defines isQueryBoundP_cast_pred' (transport of a query‑bound across propositionally equal predicates), probEvent_bad_bind_eq_tsum_false (bad‑flag pass‑through for a bad‑free computation), probEvent_lazyGhostHybridImpl_charged_step (the charged‑step premise for a lazy ghost random‑oracle read, bounding the fire‑draw probability by enncard(ghost cache)·ofReal ε), and two lemmas (lazyGhostHybridImpl_run_unif_bad_false and lazyGhostHybridImpl_run_sign_bad_false) that each state the lazy‑ghost handler preserves the non‑bad flag for uniform and signing queries. The main theorem, probEvent_lazyGhostHybridImpl_bad_le, assembles these ingredients via the single‑world accumulator and charged‑read/expected‑growth fold to bound the overall bad‑flag probability by ENNReal.ofReal (qS·(qH+1)·ε/(1−p_abort)), a key component of the security bound.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HiddenReadFold.lean: This file adds the HiddenReadFold module to the EUF-CMA security proof for Fiat-Shamir with aborts. It provides the core lemmas for the
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HopLemmas.lean: This new file (979 lines) adds the hybrid hop lemmas for the EUF-CMA security reduction of the Fiat-Shamir-with-aborts transform, stated per key pair under pointwise hypotheses. It defines and proves four main lemmas: probOutput_unforgeableExp_eq_hybridExpAtKey_real (the G₀ bridge lemma showing the real-signing hybrid experiment reproduces the standard unforgeability experiment's success probability), probOutput_hybridExpAtKey_real_le_prog (G₀ → G₁, bounding the cost of replacing caching hash by overwrite-reprogramming), probOutput_hybridExpAtKey_prog_le_trans (G₁ → G₂, bounding the cost of dropping reprogramming of rejected attempts using a ghost-instrumented identical-until-bad argument), and probOutput_hybridExpAtKey_trans_le_sim (G₂ → G₃, bounding the cost of substituting the private honest-execution loop with the HVZK simulator loop). Additional supporting helpers include flagLift (lifting a handler to carry a never-touched bad flag) and sum_natCast_mul_pow_le_sq_sum_pow (a real inequality used in the G₀→G₁ bound). No sorry or admit appear.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Loss.lean: Adds the file Loss.lean defining the CMA-to-NMA statistical loss for the Fiat-Shamir-with-aborts reduction after Theorem 3 (CRYPTO 2023). It introduces two noncomputable functions: cmaToNmaLoss, the overall loss as a sum of four terms including query bounds, commitment-guessing probability, abort probability, simulator error, and key-regularity failure; and perKeyLoss, the per-key part excluding the key-regularity failure. The lemma cmaToNmaLoss_eq_perKeyLoss_add states the equality cmaToNmaLoss = perKeyLoss + δ. No sorry or admit appear.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/NMAReduction.lean: This new file (1041 lines) defines the NMA (non-adaptive) reduction for the Fiat-Shamir-with-aborts EUF-CMA security proof. It introduces and proves the key coupling lemmas between a two-layer nested managed simulation (nmaOuterImpl inner handler + nmaInnerImpl outer runtime handler), a single linked handler nmaLinkImpl, and a ghost-tagged layered NMA implementation ghostNmaImpl. The new definitions include the handlers nmaOuterImpl, nmaInnerImpl, and nmaLinkImpl, the projection function proj2, and the NMA adversary simulatedNmaAdv. The file proves the critical per-step projection lemmas hproj2_unif, hproj2_ro, hproj2_ro_ghost_hit, hproj2_ro_fresh, and hproj2_sign, which together establish hproj2_evalDist — an unconditional per-query distributional equality between the projected ghost-tagged step and the linked managed step. These are lifted to whole runs by evalDist_map_run_simulateQ_ghostNmaImpl_proj2 and managedRun_eq_link_run, and the overall bound hybridSimRun_le_managedRun_verify ties the hybrid experiment's success probability to the managed reduction's. No sorry or admit are present; the extensive commentary documents previously open sub-goals that are now resolved by the redesigned proj2 and the proven per-step lemmas.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/ReadRecording.lean: This new file introduces the read-recording handler deferredDrawReadImpl, which extends the deferred-draw handler by appending the commitment component of each adversarial random-oracle read to an extra List Commit component, making the read-time bad flag (whether a read hits the current drawn list) equivalent to a final-state predicate (some recorded read-commit lies in the final drawn list). It defines the coupling invariant deferredReadInv and proves per-query coupling deferredDrawRead_step and inductive run coupling deferredDrawRead_run, which together yield the reduction deferredDraw_bad_le_readRecord that the deferred-draw bad flag probability is at most the probability of the final-state read-hit predicate. Finally, readRecord_pred_le_expected_coincidences applies the Markov (first-moment) inequality to bound that predicate by the expected number of recorded read-commits that fall in the drawn list, isolating the per-position independence as the remaining open content.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/TapeFactorization.lean: This file introduces the first-moment reduction scaffolding and fold-level tape factorization for the EUF-CMA security proof of the Fiat-Shamir with aborts transform. It defines the tape-consuming read-recording handler tapeDrawReadImpl and proves the core equivalence evalDist_deferredDrawRead_eq_drawList_tapeDrawRead, showing that the read-recording run with deferred draws distributes as a single front draw block followed by a tape-consuming run. Auxiliary results include deterministic and expected length bounds on the read and drawn lists (deferredDrawReadImpl_run_readlist_length_le, deferredDrawRead_run_expected_drawnlist_length_le), an upper bound on the expected attempt count (deferredDrawRead_attemptKn_mean_le), and lemmas for combining draw blocks (drawList_combine_take_drop, evalDist_signStep_commute).

Last updated: 2026-07-13 21:09 UTC.

alik-eth · 2026-07-06T09:04:23Z

Rebased onto main now that #465 is merged — the diff is down to this PR's own commits. Full CI set green locally at the new tip.

quangvdao

Thank you for taking on a very difficult proof chain. There is substantial reusable work here—the Fiat–Shamir-with-aborts hybrids, deferred-sampling machinery, encoding and sampling laws, and ring-norm lemmas are all valuable. I am requesting changes because the current ML-DSA headline relies on a serious distributional misformalization and several assumptions that are too close to assuming the intended reduction.

The blocking issues are:

Correct the MLWE distribution. mldsaMLWE samples both s₁ and s₂ uniformly from their entire RqVec carriers. Uniform additive error makes A·s₁+s₂ itself uniform, so this decisional problem has zero distinguishing advantage for an information-theoretic reason. It is not the short-secret/small-error Module-LWE assumption used for ML-DSA.

Please define the ideal problem using explicit short secret/error samplers matching the intended ML-DSA/literature distribution, and then establish the appropriate bridge to the standard matrix-based MLWE problem. hMlweBridge should become a genuine, weaker embedding/assumption with inspectable content, not a caller-supplied inequality that carries the whole reduction.
Redesign honestSamplingSlack. It currently compares deterministic ExpandSeed/ExpandS output with independent uniform full-ring vectors. For concrete ML-DSA this TV distance is near one: the real output is supported on η-bounded vectors, while the comparison distribution has full-ring support. Thus a negligible idealGap is not plausibly satisfiable, and idealGap = 1 makes the bound vacuous.

Please compare against the correct short-secret marginal and model the ideal XOF/random-function step explicitly, or introduce a clearly computational XOF/PRG replacement assumption. Merely labeling the current gap as a ROM assumption is not sufficient when prims is a fixed deterministic function.
Fix the asymptotic/non-vacuity claims. euf_cma_security_asymptotic_real_satisfiable only chooses numerical negligible sequences; it does not instantiate honestSamplingSlack, MLWE/STMSIS, hMlweBridge, the scheme family, or the other security hypotheses. Please remove or rename it to describe only the numerical loss regime. Likewise, idealPrims exposes the key-generation seed as public ρ; it is useful as a logical consistency witness for Primitives.Laws, but not as a faithful or secure ML-DSA instantiation. Document and name it accordingly.
Expose a standard SelfTargetMSIS target. mldsaSTMSIS.isValid is presently defined through the ML-DSA identification verifier. The extraction is useful, but to justify the literature-facing hardness claim we need a bridge to an explicit algebraic SelfTargetMSIS relation with the matrix equation and norm bounds, or the theorem must clearly stop at this tailored intermediate problem.
Scope the theorem to the model actually covered. The result is for the proof-level FiatShamirWithAbort (identificationScheme …), not yet the full FIPS signing/encoding path. That is acceptable for this stage: concrete FIPS implementation security is not a prerequisite. Please describe it as security of the idealized proof-level ML-DSA model and list the idealizations, rather than “end-to-end ML-DSA.” The objective is a meaningful unforgeability theorem for a reasonably accurate model under genuinely weaker assumptions.
Split the generic engine into reviewable modules. An 8k-line WithAbort/Security.lean plus the 2.7k-line GhostBodies.lean is too difficult to maintain and semantically review. Please separate at least retry/cache primitives, game definitions/identification, Sign→Prog, Prog→Trans/deferred sampling, Trans→Sim, managed-NMA bridge, and final assembly. The concrete algebra/law results are also good candidates for an independent PR if that helps preserve progress while the security statement is redesigned.

There is also no formal PPT/cost preservation yet. Please mention this briefly rather than treating it as a blocker here. #460 is dtumad's work toward the machine/PPT layer; until that infrastructure is available, reviewers need to manually verify that each constructed reduction plausibly preserves polynomial time and does not rely on exhaustive/noncomputable computation in the cryptographic path. In particular, avoid calling the current unrestricted-adversary asymptotic theorem a theorem about “poly-time adversaries.”

Finally, #477 is already merged, so please update this branch to current main and rerun CI.

The key requested outcome is not more assumptions around the present statement: it is a corrected short-distribution model and theorem statements whose hypotheses are strictly weaker, meaningful, and plausibly instantiable for the idealized ML-DSA scheme.

alik-eth · 2026-07-12T18:48:32Z

@quangvdao Thank you — points 1 and 2 are genuine catches and I want to acknowledge them plainly: with both secret and error uniform over the full ring, mldsaMLWE is information-theoretically zero-advantage as a decisional problem, so hMlweBridge was silently carrying the entire hardness step; and honestSamplingSlack against full-ring uniform vectors makes a small idealGap unsatisfiable for any η-bounded instantiation. Neither is fixable by relabeling — agreed the fix is the short-distribution redesign.

Itemized plan:

MLWE distribution: define explicit short secret/error samplers matching the ML-DSA literature distribution, restate the ideal problem over them, and make hMlweBridge a genuine seed→matrix embedding with inspectable content. Main redesign campaign.
honestSamplingSlack: rebuild the keyswap hop comparing against the correct short-secret marginal, with an explicit XOF/PRG-replacement assumption as the computational step (not a ROM label on a deterministic function). Part of the same redesign.
Renames: doing now — the asymptotic satisfiability witness gets a name describing only the numerical loss regime, and idealPrims is documented (and named) as a logical consistency witness for Primitives.Laws, explicitly not a faithful instantiation.
SelfTargetMSIS: will export the explicit algebraic relation with matrix equation and norm bounds plus a bridge from the verifier-tailored intermediate, or clearly stop at the intermediate with honest naming — folded into the redesign.
Scope docs: doing now — security of the idealized proof-level ML-DSA model, with the idealization list.
Module split: doing now, along the cut you list (retry/cache primitives, game definitions, Sign→Prog, Prog→Trans/deferred sampling, Trans→Sim, managed-NMA bridge, assembly).

PPT-limitation note and the 4.31 rebase land with the next push.

Proposal, per your suggestion: extract the concrete algebra/laws work (Ring/Norms additions, MLDSA/Concrete/{Encoding,Laws,Rounding,Sampling}, and the Primitives.Laws field corrections they witness) into an independent PR so that progress is preserved while the security statement is redesigned here. If that works I'll do the split with the next push, and sequence the redesign campaign after the #466 items unless you'd rather it first.

…etMSIS + ROM) Sound ML-DSA EUF-CMA reduction MLDSA.euf_cma_security_of_nma: CMA->NMA via FiatShamirWithAbort + nma_security, with the honest-sampling gap carried as an explicit additive idealGap slack (the false expandS_honest_sampling field removed). Concrete algebraic Laws + the Primitives.Laws non-vacuity witness (Concrete/NonVacuity), plus the supporting Ring norm lemmas. Claude-Session: https://claude.ai/code/session_01C7GAM6ykxZoXwDXmtdLqrA

…strings (add /(1-p)) The `cmaToNmaLoss` prose in `MLDSA/Security.lean` (module docstring + the `cmaToNmaLoss` wrapper docstring) wrote the HVZK term as `qS·ζ_zk`, but the delegated `FiatShamirWithAbort.cmaToNmaLoss` definition is `qS·ζ_zk/(1-p)` (the simulator is glued across the restart loop of expected length ≤ 1/(1-p)). Prose now matches the definition. Claude-Session: https://claude.ai/code/session_01C7GAM6ykxZoXwDXmtdLqrA

The two per-attempt bound lemmas never use the instance in their types; the cache-hit proof obtains it explicitly via Classical.decEq to keep instance search deterministic. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

… new Laws and GhostBodies modules Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

quangvdao · 2026-07-12T18:56:24Z

yeah do the split. for MLWE definition, I prefer a centralized, generic definition of LWE that works for general modules and error distribution - one umbrella master definition, then specialized into plain / unstructured LWE, module LWE, ring LWE, different error distributions (even hamming weight error as well), etc.

So in fact what I'm looking for here is a central NoisyLearningProblem definition that can specialize to both LWE and LPN type assumptions, then specialize down to MLWE as used in ML-DSA. Put this in the right place, probably in VCVio core.

This is not the original scope of this PR but I think we should have such a self contained PR to aid all future developments.

alik-eth · 2026-07-12T19:07:43Z

Will do — extracting the concrete algebra/laws slice (Ring/Norms additions, MLDSA/Concrete/*, the Primitives.Laws corrections) as its own PR. On the LWE ask: agreed, and it dovetails with review point 1 — I'll draft a self-contained NoisyLearningProblem PR in VCVio core (one master definition over general modules with pluggable secret/error samplers, decision and search variants; specializations to plain LWE / MLWE / RLWE / LPN-style Hamming-weight error), and the corrected short-distribution ML-DSA MLWE then lands as an instantiation of it in the redesign here. Renames and scope docs from the review are already staged.

…ot lemmas; adapt WithAbort to Lean 4.31 Drop the two private WithAbort copies of the expectation-algebra lemmas that landed at the EvalDist root in Verified-zkEVM#465 (tsum_probOutput_map_mul et al.) and re-point their uses. Toolchain adaptation: zero_le' deprecation, simpa post-simp defeq checks replaced by default-transparency exact/unfold at the local-spec sites, gcongr reflexive-factor discharge, and a direct Mathlib.Data.Nat.Choose.Cast import for Nat.cast_choose_two. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…eframe the concrete witness Add a "Scope: an idealized proof-level ML-DSA model" section to SecurityNMA (transcript signatures, seed-based problems, idealGap semantics, no cost model). Rename the concrete witness primitives idealPrims -> seedRevealingPrims and present the Laws instance as a logical-consistency (inhabitance) witness only, with no quantitative security content. Rename the satisfiability lemma to asymptotic_loss_regime_satisfiable and state that its adversary sequence chooses numerical sequences only. Drop a change tactic that became a no-op on Lean 4.31. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-12T23:06:42Z

First response batch pushed (branch force-updated over the update-branch merge; rebased on current main, Lean v4.31.0, full CI set green, zero non-sorry warnings, MLDSA.euf_cma_security_of_nma / nma_security re-verified [propext, Classical.choice, Quot.sound]):

Scope section added to SecurityNMA.lean ("an idealized proof-level ML-DSA model": transcript signatures, seed-based problems, idealGap semantics, no cost model — these are not poly-time statements).
idealPrims → seedRevealingPrims renamed throughout the concrete witness, and the Laws instance is now presented as a logical-consistency (inhabitance) witness only, with no quantitative security content. The satisfiability lemma is renamed asymptotic_loss_regime_satisfiable and its docstring states the adversary sequence chooses numerical sequences only.
Deduped the two WithAbort private copies of the expectation-algebra lemmas that landed at the EvalDist root in feat(framework): deferred-sampling + relational-coupling engine #465.

Still in flight from the review, in order: the WithAbort/Security.lean module split, the concrete-laws extraction into its own PR, the central NoisyLearningProblem definition in VCVio core (design drafted — the existing LearningWithErrors.Problem shape lifts cleanly and specializes to LWE/MLWE/LPN and the short-distribution ML-DSA MLWE), and then the short-distribution redesign of mldsaMLWE on top of it.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…o a directory of phase modules Split the 8k-line development along its proof phases: Loss, BodyHops, GhostReadCharge, HiddenReadFold, CouplingEngine (banked infrastructure, off the live path), ReadRecording, TapeFactorization, HopLemmas, NMAReduction, and Assembly (the headline euf_cma_to_nma). The umbrella module keeps the import path, so consumers are unchanged. Content is moved verbatim; each module re-declares the shared variable scaffold. The three List-counting private lemmas move with their only consumers into TapeFactorization. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…ectory of phase modules Split along the development's phases: Bodies (retry loops and the four signing bodies), GhostLayer, Projections, BodyBounds, and NMAHandler. The umbrella module keeps the import path, so consumers are unchanged; content is moved verbatim with the shared variable block re-declared per module. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-12T23:29:03Z

Second split executed: the Primitives.Laws repair + FIPS-shaped concrete witness is now #479 (self-contained off main: the three-field fix, the honestSamplingSlack key-swap threading adapted to main's SecurityNMA, and the kernel-checked mldsa_laws_inhabited certificate). The laws files there are byte-identical to this branch's, so this PR's diff shrinks to the EUF-CMA development once #479 lands and this branch rebases.

Also pushed here: WithAbort/Security.lean (8k lines) is now split into a directory of ten phase modules (Loss → … → Assembly), and GhostBodies.lean into five, both with umbrella modules keeping the import paths — content moved verbatim, zero consumer churn, headlines re-verified axiom-clean after each split.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-12T23:33:01Z

The central noisy-learning definition is now #480 (NoisyLearning.Problem in VCVio core, specializing to LWE/module-LWE/ring-LWE/LPN, with LatticeCrypto's LearningWithErrors as a compatibility re-export). The short-distribution mldsaMLWE redesign here will instantiate it with η-bounded samplers.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…LWE problems First step of the short-distribution redesign (review points 1/2): - sampleShortVec: the uniform distribution on the eta-bounded box S_eta^k, the secret/error distribution of ML-DSA's Module-LWE assumption (with the decidability instance and the zero-vector membership witness). - keygenShort / keygenShort1: idealized key generation sampling rho, K, and the short secrets independently, with t = ExpandA(rho)*s1 + s2 real vs uniform. The key-swap hop against these is an exact identity, carrying no statistical slack. - mldsaMLWEShort: the seed-based short-secret MLWE problem (uniform rho, box-uniform s1/s2) - not information-theoretically trivial, unlike a uniform-error variant. - mldsaMatrixMLWE: the literature-facing uniform-matrix form. - expandAIdealization: the quantified XOF-as-random-matrix step with inspectable content, replacing the caller-supplied hMlweBridge inequality; computational reading documented pending the cost model (Verified-zkEVM#460). Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…hop and the seed-to-matrix bridge nma_keyswap_hop_short: against keygenShort/keygenShort1 the NMA-game gap is bounded by the mldsaMLWEShort advantage of distinguisherB, with both branch identifications exact monad identities (the unused key/s1/s2 draws strip via probOutput_bind_const); no statistical slack term. advantage_mldsaMLWEShort_le_matrix: the seed-based short problem reduces to the uniform-matrix form at the cost of one expandAIdealization application; the uniform branches agree exactly (matrix draw strips, independent uniform draws commute via evalDist_bind_comm_probComp). Both kernel-checked [propext, Classical.choice, Quot.sound]; file clean under the CI linter set. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

… security headlines Add the idealized short-key-model security chain on top of the proven exact key-swap hop, addressing the review finding that the uniform-secret MLWE formalization made the assumption trivially satisfiable: - mldsaSTMSISShort: the SelfTargetMSIS instance whose parameters are sampled from the uniform-t short-key generator keygenShort1, and extractorCShort, its typed extractor (same run as extractorC). - nmaAdvantage_keygenShort1_le_stmsis: the SelfTargetMSIS extraction bound at keygenShort1; the per-key read-back comparison stmsis_tail_le applies verbatim since it never inspects the key distribution. - nma_security_short: the corrected EUF-NMA headline over keygenShort. The key-swap leg is the exact nma_keyswap_hop_short against mldsaMLWEShort (secrets uniform on the eta-bounded box), so the bound is MLWE + SelfTargetMSIS with no idealGap slack and no honestSamplingSlack or Primitives.Laws hypotheses. - euf_cma_security_of_nma_short (+ _hvzk): the CMA-to-NMA composition wrappers over the short model, again without the idealGap summand. All additions are additive; existing declarations are unchanged. Each new declaration depends on exactly [propext, Classical.choice, Quot.sound]. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…rt headlines; name the matrix lift Generalize the hMlweBridge hypothesis of nma_security_short and the two euf_cma_security_of_nma_short wrappers with an explicit bridge slack εbridge, carried additively inside the MLWE summand of each bound. The canonical discharge is now fully proven material: mlwe := mldsaMatrixMLWE, εbridge := εA, witness matrixLift (the named seed-to-matrix adversary lift) with advantage_mldsaMLWEShort_le_matrix under expandAIdealization — the recipe is documented on the headline's docstring. εbridge := 0 with an exact embedding recovers the previous shape. All headline axioms re-verified [propext, Classical.choice, Quot.sound]; file clean under the CI linter set. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

… re-tagged scheme Add `validKeyPairShort`, the ∃-material analogue of the ∃-seed `validKeyPair`: a pair is short-valid when it is assembled from seeds `ρ`, `K` and `η`-bounded short vectors `(s₁, s₂)` via `t = ExpandA(ρ)·s₁ + s₂` and `Power2Round`. Unlike the seed form it is satisfiable by idealized key generators that sample the material directly, so a `GenerableRelation` over it can carry `keygenShort`. Add the matching simp lemma `validKeyPairShort_eq_true_iff` and `identificationSchemeShort`, the field-copy of `identificationScheme` tagged at the new relation (the relation is only a type index; the operations are shared projections). Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…eygenShort Prove `hrShort : GenerableRelation _ _ (validKeyPairShort p prims)` with generator `keygenShort`: support analysis of the key draw plus `mem_support_sampleShortVec` (box-sampler outputs are η-bounded on their support) supplies the ∃-material witness. Record the explicit satisfiability certificate `keygenShort_generable` for the short-model `hGen` hypothesis. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…the material relation The short-model statements previously hypothesized `hr : GenerableRelation _ _ (validKeyPair …)` with `hGen : hr.gen = keygenShort`, an uninhabitable pair (`gen_sound` forces the support of `keygenShort` inside the ∃-seed image, which cardinality forbids), making them vacuously true. Re-target the short path at `validKeyPairShort` / `identificationSchemeShort`, which `keygenShort` genuinely generates (`hrShort`, `keygenShort_generable`): - twin the rel-indexed NMA plumbing (`nmaGameShort`, `nmaAdvantageShort`, `distinguisherBShort`, `nmaGameShort_eq_keygen_bind`, `stmsis_tail_le_short`); - retag `mldsaSTMSISShort.isValid` at the short scheme's verifier; - re-state `nma_keyswap_hop_short`, `nmaAdvantage_keygenShort1_le_stmsis`, `nma_security_short`, and `euf_cma_security_of_nma_short` over the new relation and scheme; - drop `euf_cma_security_of_nma_short_hvzk`: in the short model the withheld key part t₀ is not determined by the public key across material-valid pairs (distinct bounded (s₂, t₀ = t₀' + e) witnesses collide on (ρ, t₁)), so the exact-on-accept simulator behind `idsWithAbort_hvzk_real` has no sound short-relation port; the general headline keeps the HVZK obligation as an abstract, satisfiable hypothesis instead. Pre-existing seed-model declarations are unchanged. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…rity model Inhabit the seed-relation hGen pair with the FIPS generator (hrFips + keygen0_generable certificate), name the computational XOF-replacement assumption expandSReplacement against the correct short-secret marginal (rho, K uniform; s1, s2 uniform on the eta-box, matching keygenShort's draws exactly), and derive the FIPS-keygen NMA corollary nma_security_fips: the keygen0 game differs from the keygenShort game by one application of the expandSReplacement distinguisher at the shared forge-and-verify tail (the two scheme tags carry the same verify), so the short-model bound transfers at an additive epsilon_PRG. All new declarations axiom-clean [propext, Classical.choice, Quot.sound]. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…on chain The short-secret model is now the sole ML-DSA reduction: delete the uniform-secret problem statements and hops (mldsaMLWE, mldsaSTMSIS, keygen1, distinguisherB, honestSamplingSlack, nma_keyswap_hop, stmsis_tail_le, nmaAdvantage_keygen1_le_stmsis, nma_security, euf_cma_security_of_nma, euf_cma_security_of_nma_hvzk), retype extractorC at mldsaSTMSISShort (anonymous constructor; run body unchanged), and re-point the asymptotic headline at the short wrapper as euf_cma_security_asymptotic_short (abstract HVZK simulator family, MLWE-bridge slack family; numerical content unchanged), with asymptotic_loss_regime_satisfiable's witness reshaped to the new internal bound. Module overview, section prose, and cross-file references now describe the short chain (nma_keyswap_hop_short, nmaAdvantage_keygenShort1_le_stmsis, nma_security_short, euf_cma_security_of_nma_short) with the FIPS connection carried by expandSReplacement / nma_security_fips. Full CI build set green; all live headlines axiom-clean [propext, Classical.choice, Quot.sound]. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

… headline nma_security_short_matrix: nma_security_short with the abstract-problem bridge discharged onto the uniform-matrix short-secret problem mldsaMatrixMLWE via matrixLift and advantage_mldsaMLWEShort_le_matrix, under the expandAIdealization assumption. Every hypothesis is a satisfiable pinned equality, a proven reduction, or the named XOF idealization. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…it algebraic relation Review point 4 (PR Verified-zkEVM#467): expose what an accepted solution of the tailored SelfTargetMSIS problem means algebraically. - computeWApprox_eq_mul_sub_smul: under the transform laws the verifier's recomputation is the coefficient-domain matrix expression A*z - c*(t1*2^d). - stmsisAlgebraicSolution + mldsaSTMSISShort_isValid_iff: accepted solutions are exactly the verifier's norm gates plus the hint-recovered matrix equation over R_q (iff, both directions proven). - identificationSchemeShort_verify_eq_true_iff: the NMA verifier's accept is exactly the self-target equation against the published commitment w1. - mldsaSTMSISShort_isValid_expandA_iff: at the matched parameters published by sampleParams acceptance degenerates to the two norm gates; isValid cannot see the hash preimage, so the security theorems stop at this tailored intermediate problem (module + problem docstrings state the scope honestly). All new declarations kernel-check at [propext, Classical.choice, Quot.sound]; pre-existing declarations byte-unchanged except sanctioned docstring updates. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…ugh SelfTargetMSIS.isValid Extend `SelfTargetMSIS.Problem.isValid` to receive the hash preimage (`Challenge → Target → HashInput → HashOutput → Response → Bool`) and thread the cache-consistent preimage through `SelfTargetMSIS.experiment`, so instantiations can bind the solution's recomputed commitment to the commitment component of the pair that was hashed — the self-target binding of the literature relation. Document the binding contract on the structure and in the module docstring. The `SIS` namespace is untouched. Adapt the ML-DSA consumer to the new arity: `mldsaSTMSISShort` receives the preimage (not yet consumed), and the algebraic-layer lemmas plus the extraction tail gain the preimage argument. The binding conjunct itself lands in the follow-up commit. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…e hashed commitment Consume the hash-preimage argument of `SelfTargetMSIS.Problem.isValid` in the tailored ML-DSA problem: `mldsaSTMSISShort.isValid` now additionally requires the commitment recomputed from the response to equal the commitment component of the hashed preimage (`hashInput.2 = w'`), the genuine self-target binding of the literature relation. At the sampled parameters `Â = ExpandA(ρ)` acceptance is now the norm gates plus the preimage binding (`mldsaSTMSISShort_isValid_expandA_iff`, replacing the previous norm-gates-only degeneration): the trivial response `z = 0` with a weight-0 hint wins only if the adversary hashed the exact commitment `UseHint(0, -SampleInBall(c̃)·(t₁·2^d))` before the oracle answered `c̃` on that preimage. `stmsisAlgebraicSolution` gains the binding conjunct and `mldsaSTMSISShort_isValid_iff` re-expresses it; the extraction bound `nmaAdvantage_keygenShort1_le_stmsis` re-proves unchanged in structure — the binding is exactly the cache read-back fact the accept branch of `stmsis_tail_le_short` already establishes (the middle conjunct of `verify` identifies the recomputed commitment with the forged `w'`). Docstrings record the remaining distance to the literature normal form ([A | I] concatenation, c-coefficient extraction). Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-13T11:27:23Z

@quangvdao The redesign you requested is complete and pushed (13 commits; body rewritten). Point by point:

1 — MLWE distribution corrected. mldsaMLWEShort/mldsaMatrixMLWE sample secrets and errors uniform on the η-bounded box; the uniform-secret problem and its chain are retired outright. The bridge to the standard matrix form is a proven reduction (advantage_mldsaMLWEShort_le_matrix via the named matrixLift), costed by the quantified expandAIdealization assumption — hMlweBridge is no longer a caller-supplied inequality, and its canonical discharge is packaged as nma_security_short_matrix.

2 — honestSamplingSlack redesigned away. The headline (nma_security_short) runs at honestly-sampled short keys, where the key-swap hop is an exact identity — no statistical slack exists to bound. The deterministic FIPS derivation enters only through nma_security_fips at cost εPRG via expandSReplacement, stated against the correct short marginal with the computational reading (and its limits pending #460) disclosed in the docstring. Every relation/pinning hypothesis is backed by a kernel-checked satisfiability certificate (keygenShort_generable, keygen0_generable) — we adopted this as a standing gate after the review.

3 — done in the earlier round (rename + numerical-sequences-only framing); the asymptotic corollary is now re-pointed at the short headline.

4 — became a soundness fix. Formalizing your requested algebraic bridge produced a kernel-checked proof that the tailored problem was easy: the SelfTargetMSIS.Problem.isValid API never saw the hash preimage, so acceptance at sampled parameters was just two norm gates (a z = 0 forgery won outright — this pre-dates this PR's redesign). We extended the API with the HashInput, added the binding conjunct to mldsaSTMSISShort, re-proved the extraction (the binding is exactly the cache read-back fact the proof already had), and the corrected characterization shows winning now requires a genuine RO fixed point. The full algebraic iff (stmsisAlgebraicSolution) states the matrix equation and norm bounds; the residual distance to the [A|I] normal form is documented rather than papered over. Falcon's SIS namespace is untouched.

5 & 6 — scope section and splits landed earlier in this round.

One finding worth flagging beyond the review's asks: under the material key relation, t₀ is provably not determined by the public key, so exact-on-accept HVZK simulation is impossible with t₁-only public keys (consistent with the literature stating HVZK with full t public). The CMA wrapper keeps HVZK abstract and satisfiable; the obstruction and its counterexample construction are documented in-code.

All headlines and certificates check at [propext, Classical.choice, Quot.sound]; full CI set green; zero sorries in the touched files.

…nside the idealization quantifiers Move the [IsUniformSpec unifSpec] binding of expandAIdealization from the section-variable telescope to inside the universal quantifier, so consumers instantiate it at their ambient instance instead of inheriting the baked section fvar. This removes the instance diamond that advantage_mldsaMLWEShort_le_matrix previously bridged via a toPMF-projection equality; the workaround (rename_i/letI shadowing plus the ext_ips/hips haves) is deleted and hA now applies directly. expandSReplacement already elaborates at the global instance (its section declares no IsUniformSpec variable) and is unchanged. All theorem statements are textually unchanged. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…rt CMA headline Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth force-pushed the pr/mldsa228 branch from 0dc2b72 to 9f5c2f2 Compare July 2, 2026 18:58

alik-eth mentioned this pull request Jul 2, 2026

feat(framework): deferred-sampling + relational-coupling engine #465

Merged

alik-eth force-pushed the pr/mldsa228 branch from 9f5c2f2 to 5a902d0 Compare July 6, 2026 09:04

Abraxas1010 mentioned this pull request Jul 10, 2026

Proposal: hash-based post-quantum signature lane (Generalized XMSS / leanSig) over a tweakable hash Verified-zkEVM/ArkLib#625

Open

aryaethn mentioned this pull request Jul 11, 2026

Proof obligation for OW_PCVA_bound in VCVio/CryptoFoundations/FujisakiOkamoto/TTransform.lean #189

Open

quangvdao requested changes Jul 12, 2026

View reviewed changes

alik-eth added 4 commits July 12, 2026 21:54

chore(MLDSA/Verified-zkEVM#228): credit campaign co-authorship on the…

5576281

… new Laws and GhostBodies modules Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth added 2 commits July 13, 2026 01:59

alik-eth force-pushed the pr/mldsa228 branch from aa05412 to 223f073 Compare July 12, 2026 23:01

alik-eth added 2 commits July 13, 2026 02:14

alik-eth mentioned this pull request Jul 12, 2026

fix(MLDSA): make Primitives.Laws inhabitable; bank the FIPS-shaped concrete witness #479

Open

alik-eth mentioned this pull request Jul 12, 2026

feat(CryptoFoundations): central NoisyLearning problem family in VCVio core #480

Open

alik-eth added 5 commits July 13, 2026 09:28

alik-eth added 8 commits July 13, 2026 11:47

alik-eth changed the title ~~feat(MLDSA): EUF-CMA via CMA→NMA — MLWE + SelfTargetMSIS + ROM (#228)~~ feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228) Jul 13, 2026

test(MLDSA/Verified-zkEVM#228): witness the joint frontier of the sho…

b74b02b

…rt CMA headline Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth requested a review from quangvdao July 15, 2026 15:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228)#467

feat(MLDSA): EUF-CMA via CMA→NMA over the short-secret MLWE model (#228)#467
alik-eth wants to merge 23 commits into
Verified-zkEVM:mainfrom
alik-eth:pr/mldsa228

alik-eth commented Jul 2, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 2, 2026 •

edited

Loading

Uh oh!

alik-eth commented Jul 6, 2026

Uh oh!

quangvdao left a comment

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

quangvdao commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 13, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

alik-eth commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The corrected model (review points 1 & 2)

Headlines (all [propext, Classical.choice, Quot.sound])

SelfTargetMSIS: point 4 became a soundness fix

Honest scoping

Verification

Uh oh!

github-actions Bot commented Jul 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Summary

Corrected Security Model

Headline Theorems (all [propext, Classical.choice, Quot.sound])

SelfTargetMSIS Soundness Fix

Infrastructure & Non-Vacuity

Ghost-Body & Security Proof Infrastructure (Fiat-Shamir with Aborts)

Other Changes

Caveats

CI & Build

Uh oh!

alik-eth commented Jul 6, 2026

Uh oh!

quangvdao left a comment

Choose a reason for hiding this comment

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

quangvdao commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 12, 2026

Uh oh!

alik-eth commented Jul 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

alik-eth commented Jul 2, 2026 •

edited

Loading

Headlines (all `[propext, Classical.choice, Quot.sound]`)

github-actions Bot commented Jul 2, 2026 •

edited

Loading

Headline Theorems (all `[propext, Classical.choice, Quot.sound]`)

alik-eth commented Jul 13, 2026 •

edited

Loading