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

…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

… security docstrings intrinsic Remove the unreferenced ghost-read charge scaffolding from the CMA-to-NMA development and rewrite the surviving docstrings to describe what the declarations state and how they are proved. Deleted (each verified unreferenced across the tree before removal): * `Security/GhostReadCharge.lean` in full (all six declarations unused). * `Security/HiddenReadFold.lean` in full; its two live arithmetic lemmas `geomAttemptSum_le` and `geomSum_le` move to `Security/TapeFactorization.lean`, the only consumer. * Fifteen declarations in `Security/CouplingEngine.lean` — the eager/lazy averaged-bad engine, the single-draw ghost-blind atoms, and the `deferredDraw*` block that duplicates the live `deferredDrawRead*` chain in `TapeFactorization.lean`. The nineteen declarations reachable from `probEvent_ghostHybridImpl_bad_le_ghostBlind`, `ghostBlind_bad_le_deferredDraw`, `deferredDrawImpl`, `ghostSignDrawBody`, and `tapeSignBody` are kept. * The lazy-fire and `memCharge` blocks in `GhostBodies/BodyBounds.lean`, which were reachable only from the deleted modules. The linear import chain is rewired accordingly: `CouplingEngine` now imports `BodyHops`, and `VCVio.lean` / `WithAbort/Security.lean` drop the two removed modules. Documentation changes carry no proof-term or statement edits: * `TapeFactorization.lean`: the docstrings of `readRecord_expected_pairs_le`, `readRecord_expected_pairs_tape_le`, and `readRecord_expected_coincidences_le` now state the bound and its proof route (tape factorization, per-pair value-freeness, the arithmetic reduction) instead of describing them as open. * `NMAReduction.lean`: the ~150-line planning block inside the completed proof of `hybridSimRun_le_managedRun_verify` is replaced by a three-part outline of the proof actually executed (link fusion, the common layered ghost-tagged run, the verify-tail split), including the state-function obstruction that motivates the layered state. * `WithAbort/Security.lean` and `CouplingEngine.lean` no longer describe the coupling module as off the live path; it carries `ghostBlind_bad_le_deferredDraw`, `deferredDrawImpl`, `tapeSignBody`, and the per-body tape factorization that `TapeFactorization.lean` consumes. * Change-history and workstream wording ("previously", "supersedes", "redesigned", "banked", "campaign", "Piece A/B", "Stage 1/2/3", "M1/M2/M3") is replaced by intrinsic descriptions throughout the touched files. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0122T9NmFkn5purmULtP2cME

…trinsically `Concrete/Laws.lean` and `Concrete/NonVacuity.lean` described their contents by contrast with earlier revisions ("now provable", "banked", "there are no longer any false-as-stated fields", "the unsatisfiable field it replaced"). Restate them by what they say: which `Primitives.Laws` fields the thirteen `concrete_*` theorems discharge and from which concrete layer, why `keyVector_t0_determined` stays an abstract ROM assumption, and why the injective published seed-component of `seedRevealingPrims` satisfies it. The status section now points at `MLDSA.mldsa_laws_inhabited` for the inhabitance witness. No statements, proofs, or attribution headers are changed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0122T9NmFkn5purmULtP2cME

github-actions · 2026-07-25T19:38:14Z

🤖 PR Summary

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

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

This PR completes the EUF-CMA security proof for the ML-DSA signature scheme (Fiat-Shamir-with-aborts) by formalizing the CMA-to-NMA reduction (Theorem 3/Lemma 7, CRYPTO 2023) over a corrected short-secret Module-LWE (MLWE) model. The work supersedes the prior placeholder euf_cma_security theorem, which has been removed in favor of fully quantified, kernel-checked statements.

Architectural thrust: The proof chain flows: CMAdv ≤ NMAadv + cmaToNmaLoss (the reduction), NMAadv ≤ MLWE + SelfTargetMSIS (STMSIS). The MLWE assumptions now use short-uniform secrets/errors (sampleShortVec, η-bounded) rather than a retired uniform-secret model. The key-swap hop (keygen real vs. uniform) is an exact identity, eliminating statistical slack. The SelfTargetMSIS problem was re-engineered: isValid now takes the hash preimage, fixing a critical soundness bug where the original API permitted trivial acceptance (e.g., z=0, empty hint). The corrected characterization (mldsaSTMSISShort_isValid_expandA_iff) requires a random-oracle fixed point.

Key components by area:

Mathematical Formalization

Short-secret MLWE assumptions (replacing retired mldsaMLWE):
- mldsaMLWEShort: seed-based, sampleShortVec secrets/errors
- mldsaMatrixMLWE: uniform-matrix variant, used in literature-facing packaging
- keygenShort: idealized short-key generation (samples ρ, K, (s₁, s₂) independently)
- validKeyPairShort: material-based key relation, replacing existential-seed validKeyPair
- Satisfiability certificates: keygenShort_generable, keygen0_generable (kernel-checked witnesses)
Corrected SelfTargetMSIS (mldsaSTMSISShort):
- isValid now takes HashInput (the preimage), ensuring binding
- Full algebraic iff via stmsisAlgebraicSolution, mldsaSTMSISShort_isValid_iff
- Residual distance to [A | I] normal form documented
Idealizations with caveats (no cost model yet, feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460):
- expandAIdealization: XOF-as-random-matrix, proven via advantage_mldsaMLWEShort_le_matrix + matrixLift
- expandSReplacement: PRG reading of ExpandSeed/ExpandS against the correct box marginal
Encoding injectivity (Concrete/Encoding.lean):
- w1Encode_injOn: proven injective on the set of commitment vectors whose coefficients lie in the valid bit width
- Full roundtrip theorems for simpleBitPackPoly/simpleBitUnpackPoly, packPolyVector/unpackPolyVector
Norms and ring properties:
- l1Norm_eq_sum, cInfNorm_mul_le (centered ℓ∞ bound for negacyclic ring)
- coeffScalarVecMul_get (transform being a ring isomorphism property)

Proof Completion (sorries removed)

Headline theorems (all [propext, Classical.choice, Quot.sound]):
- nma_security_short: EUF-NMA ≤ MLWE + STMSIS at keygenShort (no Primitives.Laws dependency)
- nma_security_short_matrix: literature-facing uniform-matrix packaging (+εA)
- nma_security_fips: FIPS seed-derived keygen connected to short model at cost +εPRG
- euf_cma_security_of_nma_short: CMA composition (bound: MLWE + STMSIS + cmaToNmaLoss), plus asymptotic corollary
- trivial_euf_cma_security_of_nma_short: trivial bound at degenerate parameters (non-vacuity witness)
Non-vacuity certificates (logical consistency):
- mldsa_laws_inhabited (Concrete): Primitives.Laws non-vacuous via seedRevealingPrims
- mldsa_short_cma_hyps_inhabited (MLDSA): all headline hypotheses simultaneously satisfiable

Protocols / Soundness

CMA-to-NMA reduction (WithAbort/Security/):
- Complete chain: Security.lean umbrella (9 submodules), Bodies.lean (4 hybrid signing bodies: real, prog, trans, sim; shared signProgramCont), BodyBounds.lean (collision bounds, TV induction), GhostLayer.lean (ghost cache layer, ghostSignBody, ghostHybridImpl), NMAHandler.lean (layered ghost-tagged NMA handler), Projections.lean (per-step projections, signed invariants)
- Loss.lean: cmaToNmaLoss defined and decomposed (per-key loss + δ)
- CouplingEngine.lean (923 lines): deferred-draw layer, identical-until-bad lemmas, tape factorization theorem (evalDist_ghostSignDrawBody_eq_drawList_tapeSignBody)
- ReadRecording.lean: read-recording handler with coupling to deferred draws, Markov bound
- TapeFactorization.lean: first-moment reduction, fold-level tape factorization, attempt-count growth bounds
- HopLemmas.lean: 4 hybrid hop lemmas (Real→Prog→Trans→Sim) with pointwise hypotheses
- NMAReduction.lean (925 lines): NMA reduction construction, simulatedNmaAdv, probOutput_hybridExp_sim_le_managedRoNmaExp
- Assembly.lean: euf_cma_to_nma headline, simulatedNmaAdv_nmaHashQueryBound
Concrete instantiation (Concrete/Laws.lean):
- concrete_* theorems discharge 13/14 fields of Primitives.Laws; keyVector_t0_determined left abstract (inherent RO modeling assumption)
- nonceBound_theorem renamed to expandMask_bound with corrected gamma1 bound
Security summary (Security.lean):
- Old placeholder MainTheorem section removed; replaced by pointer to MLDSA.euf_cma_security_of_nma_short
- Statistical loss formula corrected: qS·ζ_zk/(1-p) (not qS·ζ_zk)

Infrastructure / CI

Full library green on v4.31.0; zero non-sorry warnings; kernel-checked
SIS namespace (Falcon) byte-unchanged by STMSIS API fix

Documentation

Extensive docstrings on connection to CRYPTO 2023 (Theorem 3/Lemma 7)
HVZK obstruction documented: under material relation, t₀ not function of pk (CMA wrapper keeps HVZK abstract)
Scope section: idealized proof-level model, no PPT/cost tracking (feat(OracleComp): oracle strategies as dynamical systems, oracle machines, and TM-grounded poly-time adversaries #460)

Refactoring

Module split: WithAbort/Security → 10 phase modules, GhostBodies → 5
SecurityNMA.lean: reoriented around keygenShort; old keygen1, mldsaMLWE, distinguisherB removed
Primitives.lean: expandS_honest_sampling removed; w1Encode_injective tightened to Set.InjOn
Sampling.lean: 3 rejection loops refactored to fuel-bounded recursion; proofs added for norm bounds
VCVio.lean: imports updated for new submodules
VCVio/CryptoFoundations/FiatShamir/WithAbort/ reorganized: Security.lean now umbrella re-export
HashSig/SLHDSA/Security.lean: reference to LatticeCrypto.MLDSA.euf_cma_security_of_nma_short added in deferred section

No sorry or admit appear in any file summary. All proofs are complete.

Statistics

Metric	Count
📝 Files Changed	32
✅ Lines Added	11668
❌ Lines Removed	637

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: 332 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 (15)

lemma ofReal_tvDist_bind_le_tsum {α β : Type} (oa : ProbComp α) (f g : α → ProbComp β) :

…and 182 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 2 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/Security/TapeFactorization.lean (+2580/-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 file adds a reference to the lattice analogue LatticeCrypto.MLDSA.euf_cma_security_of_nma_short in the section documenting what is still deferred, clarifying the connection to the existing sound EUF-CMA bound. The earlier listing of deferred research-level hops (CMA→NMA, WOTS+ one-wayness, Merkle/FORS binding, multi-target loss) is retained but now followed by this analogue, which replaces the previous placeholder reference to LatticeCrypto.MLDSA.Security.euf_cma_security. The rest of the file—including the top-level security, the ε_slh_dsa bounds, the QROM-secure theorem, and the sorry at the deferred proof—remains unchanged.
LatticeCrypto.lean: Added three new imports to LatticeCrypto.lean: LatticeCrypto.MLDSA.Concrete.Laws, LatticeCrypto.MLDSA.Concrete.NonVacuity, and LatticeCrypto.MLDSA.NonVacuity. These bring in modules that presumably provide formal properties (laws) and non-vacuity proofs for the ML-DSA scheme and its concrete instantiation.
LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean: The docstring for the SelfTargetMSIS problem was updated to reflect that the isValid predicate now takes the hashed hashInput preimage in addition to the RO's cached hashOutput, making the problem explicitly
LatticeCrypto/MLDSA/Concrete/Encoding.lean: The diff adds a large block of new theorems and a private definition (packBitsList) that collectively prove the roundtrip and injectivity properties of the ML-DSA encoding/decoding functions. It introduces bitUnpackPoly_get (public) bounding each decoded coefficient to b - v with v < 2^width, then develops packBitsList and auxiliary lemmas (forIn_push_flatten, packNatArray_eq, packBitsList_length, getD_flatMap_const_len, packBitsList_getD) to model packNatArray as a bit list, and adds bitsToBytes/bytesToBits roundtrip helpers (bitOf_packByte_fin, bytearray_mk_getByteD, getByteD_bitsToBytes, bitsToBytes_size_of_mod, bytesToBits_bitsToBytes_getD), ofDigits_bits, and unpackNatArray_packNatArray_getD to establish the unpackNatArray after packNatArray recovery. These culminate in the public theorem simpleBitUnpackPoly_simpleBitPackPoly (simpleBitPack is inverted by simpleBitUnpack on the valid range). At the vector level, packPolyVector_data_toList, sliceByteArray_packPolyVector, and unpackPolyVector_packPolyVector (private) prove that unpackPolyVector inverts packPolyVector when the per-polynomial codec is a left inverse. Finally, byteArrayToList_injective and the public theorem w1Encode_injOn establish that w1Encode is injective on the set of commitment vectors whose coefficients lie in the w₁ packer's valid bit width.
LatticeCrypto/MLDSA/Concrete/Laws.lean: This new file LatticeCrypto/MLDSA/Concrete/Laws.lean introduces the concrete_* theorems that discharge thirteen of the fourteen fields of Primitives.Laws for the concrete concretePrimitives instance under any approved parameter set. It leverages the verified rounding lemmas, NTT laws, byte-encoding decode ranges, and fuel-recursive sampler bounds from the Concrete/ subdirectory, bridged via the polyNorm_eq_cInfNorm identity. The file explicitly notes that the keyVector_t0_determined field, an inherent random-oracle modeling assumption, is left abstract and that a full Primitives.Laws witness is intentionally not assembled.
LatticeCrypto/MLDSA/Concrete/NonVacuity.lean: Added the file NonVacuity.lean to provide a logical consistency (inhabitance) certificate for MLDSA.Primitives.Laws (issue Proof obligation for cmaToNmaLoss_bound in LatticeCrypto/MLDSA/Security.lean #228). It defines seedRevealingPrims, a variant of concretePrimitives that overrides expandSeed to return the seed as the first component (the public ρ), and proves seedRevealingPrims_laws – for any approved Params, MLDSA.Primitives.Laws (seedRevealingPrims p) concreteNTTRingOps. The theorem mldsa_laws_inhabited constructs an explicit witness (mldsa44, seedRevealingPrims mldsa44, and a Nonempty proof), establishing that the Laws hypothesis is not vacuously true. The file also includes a detailed module docstring describing the trust surface: the proof depends on propext, Classical.choice, Quot.sound, and the pre-existing native_decide certificate for the NTT matrix inversion (inherited from concrete_transform). No sorry or admit appear.
LatticeCrypto/MLDSA/Concrete/Rounding.lean: This diff adds the theorem highBits_coeff_val_lt_m to LatticeCrypto/MLDSA/Concrete/Rounding.lean, which states that for approved parameters p, each coefficient of highBits p r (as a ZMod value) lies strictly below (modulus - 1) / (2 * p.gamma2). This confirms that the coefficients fall within the valid commitment window [0, (q - 1) / (2γ₂) - 1], matching Algorithm 37 and the domain where the w₁ packer is injective. The proof uses highBitsCoeff_lt_m (via BalancedDecomp.ofApproved) and the definition of highBits in terms of highBitsCoeff.
LatticeCrypto/MLDSA/Concrete/Sampling.lean: This diff refactors three core rejection-sampling loops—rejUniformCoeffs, rejEtaCoeffs, and the inner sampleInBall challenge loop—from imperative while/for constructs into structurally terminating fuel-bounded recursive functions (rejUniformCoeffsAux, rejEtaStep/rejEtaCoeffsAux, sampleInBallFindChosen/sampleInBallStep/sampleInBallLoop), preserving the original per-iteration guards and array mutations exactly. Accompanying these refactors are substantial proof additions: sampleInBall_coeff_mem and sampleInBall_norm establish that sampleInBall outputs coefficients in {-1,0,1} with infinity norm at most 1; sampleInBall_l1Norm bounds its centered ℓ₁ norm by τ; sampleEtaPoly_norm proves every coefficient of sampleEtaPoly has centered infinity norm at most η; and expandS_bound shows that both secret vectors from expandS satisfy polyVecBounded at parameter η. Supporting lemmas (getD_set!_or, countNZ_set!_eq, findChosen_le, EtaInv_condPush, rejEtaStep_mem, requireFullEtaSample_mem) build the necessary structural invariants for the fuel-induction proofs. No sorry or admit is introduced.
LatticeCrypto/MLDSA/NonVacuity.lean: The new file LatticeCrypto/MLDSA/NonVacuity.lean provides a logical consistency (inhabitance) witness for the conditional headline theorem MLDSA.euf_cma_security_of_nma_short. It defines neverAbortSim (a constant-transcript HVZK simulator), honestNoAbortGood (a good-key event where the honest prover never aborts), and trivialForger (a CMA forger making no queries and returning an aborted forgery), along with auxiliary lemmas (neverAbortSim_hvzk, probOutput_none_neverAbortSim, trivialForger_signHashQueryBound, expandAIdealization_one) that discharge each hypothesis of the headline at trivial parameter values (ε=1, ζ_zk=1, δ=1, p_abort=0, qS=qH=0, εbridge=1). The main theorem mldsa_short_cma_hyps_inhabited proves the conjunction of all hypotheses is simultaneously satisfiable, and trivial_euf_cma_security_of_nma_short applies the headline to the trivial forger, yielding a trivial bound with no quantitative security content. The file contains no sorry or admit; all proofs are complete.
LatticeCrypto/MLDSA/Primitives.lean: Modified Primitives.Laws for MLDSA: expandMask_bound now uses p.gamma1 (instead of p.gamma1 - 1) and its docstring reflects the correct centered infinity-norm bound; w1Encode_injective was tightened from global injectivity to Set.InjOn on the set of vectors whose every component is a highBits output, with an updated docstring explaining the encoder is not injective on the full carrier; the expandS_honest_sampling field (ROM joint‑uniformity assumption) was removed entirely; and the docstring of keyVector_t0_determined was updated to no longer reference expandS_honest_sampling.
LatticeCrypto/MLDSA/Scheme.lean: This diff adds two declarations. validKeyPairShort is a new noncomputable Boolean predicate that checks whether a public/secret key pair can be expressed in terms of bounded short vectors s1, s2 and seeds rho, key, capturing the algebraic key relationship t = A·s1 + s2 via Power2Round and ExpandA, without requiring the key material to be derived from a single seed. A corresponding validKeyPairShort_eq_true_iff theorem gives a simp lemma equating the predicate to its existential definition. The diff also adds identificationSchemeShort, a new IdenSchemeWithAbort constant that reuses the commit/respond/verify operations of the existing identificationScheme, but is tagged with the validKeyPairShort key relation instead of validKeyPair, for use in idealized security statements where key material is sampled directly rather than seed-derived.
LatticeCrypto/MLDSA/Security.lean: The statistical loss formula in the file's preamble comment is corrected: the term qS·ζ_zk is changed to qS·ζ_zk/(1-p). The documentation comment for the EUF‑NMA theorem updates the reference name from MLDSA.nma_security to MLDSA.nma_security_short. The entire MainTheorem section—which contained the placeholder theorem euf_cma_security (a sorry-filled statement with unsound constraints) and the accompanying open scoped Classical / variable block—is removed and replaced by a comment directing readers to the actual, fully‑quantitative security theorem MLDSA.euf_cma_security_of_nma_short in LatticeCrypto.MLDSA.SecurityNMA.
LatticeCrypto/MLDSA/SecurityNMA.lean: This diff substantially rewrites SecurityNMA.lean to reorient the ML-DSA EUF-NMA security proof around the idealized short-secret key generation (keygenShort) and the abstract mldsaMLWEShort / mldsaMatrixMLWE problems, replacing the previous keygen0/keygen1/mldsaMLWE/distinguisherB infrastructure. New definitions include the short-key generators keygenShort (real t) and keygenShort1 (uniform t), the uniform-box sampler sampleShortVec with its support lemma mem_support_sampleShortVec, the generable relations hrShort and hrFips with their satisfiability theorems keygenShort_generable and keygen0_generable, the quantified assumptions expandSReplacement (XOF replacement for secret derivation) and expandAIdealization (matrix-vs-idealization for ExpandA), the short-model games nmaGameShort and nmaAdvantageShort, the seed-based MLWE problem mldsaMLWEShort and the uniform-matrix problem mldsaMatrixMLWE, the distinguisher distinguisherBShort, the matrix-lifting wrapper matrixLift, the seed-to-matrix bridge lemma advantage_mldsaMLWEShort_le_matrix, and the short hop theorem nma_keyswap_hop_short. The old keygen1, mldsaMLWE (seed-based via ExpandSeed), distinguisherB, and the original nma_keyswap_hop (which required Primitives.Laws.expandS_honest_sampling) are removed. The file-level module docstring expands from the two-step "MLWE key-swap hop + SelfTargetMSIS extraction" plan to a three-step plan that adds explicit FIPS-keygen transfer via expandSReplacement and includes a detailed algebraic description of the tailored SelfTargetMSIS problem (mldsaSTMSISShort). No sorry or admit appears in the diff.
LatticeCrypto/Ring/Norms.lean: The file adds l1Norm_eq_sum, which expands the ℓ₁ norm as a sum of centered coefficient absolute values. A new block of definitions and theorems establishes the centered ℓ∞ norm bound cInfNorm_mul_le for the negacyclic ring: cInfNorm (f * g) ≤ l1Norm f * cInfNorm g. This is supported by the private integer convolution intConvCoeff and lemmas negacyclicConvCoeff_eq_intCast, intConvCoeff_natAbs_le, and mul_get_eq_convCoeff, which connect the ring product to the integer convolution and bound its absolute value.
LatticeCrypto/Ring/Transform.lean: Added theorem coeffScalarVecMul_get, which states that the j-th entry of coeffScalarVecMul c v equals c * (v.get j) — the component-wise action of coefficient-domain scalar-vector multiplication. The proof uses laws.toHat_mul and laws.fromHat_toHat, confirming that the property follows from the transform being a ring isomorphism. No sorry or admit were introduced.
VCVio.lean: This diff updates VCVio.lean to add import statements for two new submodules: VCVio.CryptoFoundations.FiatShamir.WithAbort.GhostBodies and its children (Bodies, BodyBounds, GhostLayer, NMAHandler, Projections), and VCVio.CryptoFoundations.FiatShamir.WithAbort.Security and its children (Assembly, BodyHops, CouplingEngine, HopLemmas, Loss, NMAReduction, ReadRecording, TapeFactorization). No existing imports, theorems, definitions, or other declarations are modified or removed.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies.lean: This diff adds a new umbrella module GhostBodies.lean that re-exports five submodules (Bodies, GhostLayer, Projections, BodyBounds, NMAHandler). The module's docstring documents the high-level structure of the CMA-to-NMA hybrid chain for the Fiat-Shamir-with-aborts transform, naming the four signing bodies (realSignBody, progSignBody, transSignBody, simSignBody), the two run-level hybrid handlers (hybridBaseImpl, hybridSignImpl), the ghost-layer reprogramming body (ghostSignBody) with its projections (run_ghostSignBody_overlay, run_ghostSignBody_fst), and the ghost-instrumented hybrid implementation (ghostHybridImpl) with its projections (ghostHybridImpl_proj_prog, ghostHybridImpl_proj_trans) and invariant (ghostHybridImpl_preserves_signed_inv). No new theorems, definitions, or sorry/admit are introduced in this file itself; it solely serves as a top-level re-export and documentation module.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Bodies.lean: This new file (Bodies.lean) defines the core first-success retry loop abstraction and the four hybrid signing-oracle bodies for the CMA-to-NMA reduction in the Fiat-Shamir with aborts setting. It introduces the abstract retry loop firstSome (a function ℕ → ProbComp (Option α)) and its associated lemmas firstSome_succ and tvDist_firstSome_le_geometric. The latter lemma provides a distributional bound on the total variation distance between two retry loops. The file then defines four noncomputable signing-oracle bodies: realSignBody (the real signing loop with caching), progSignAttempt / progSignBody (the all-attempts-reprogramming hybrid that overwrites the cache for every attempt), transSignBody (accepted-only-reprogramming hybrid, running privately on honest executions), and simSignBody (the simulated hybrid using a per-attempt HVZK simulator, with the secret key unused). It also defines the shared signProgramCont continuation that programs the accepted transcript's challenge into the cache. No sorry or admit are present in the diff.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/BodyBounds.lean: This new file BodyBounds.lean introduces ghost-layer bounds for the Fiat-Shamir with aborts signing-body development. It provides: (1) general lemmas tsum_probOutput_pure_mul, tsum_probOutput_bind_mul, tsum_probOutput_mul_le_add_of_le, and ofReal_tvDist_bind_le_tsum for manipulating expectations and total variation under probabilistic computations; (2) run-unfolding lemmas run_progSignBody_succ and run_simulateQ_fsAbortSignLoop_succ that expand one attempt of the reprogramming and real signing loops; (3) the signCollisionBound noncomputable definition and its properties signCollisionBound_zero, signCollisionBound_succ, signCollisionBound_mono, and signCollisionBound_eq, quantifying the within-query collision budget; (4) per-attempt bounds tsum_probOutput_commit_mul_abort_le (abort probability) and probEvent_commit_hit_le (commitment-guessing bound for cache hits); and (5) the two body-level cores of the Sign→Prog hop: ofReal_tvDist_run_fsAbortSignLoop_progSignBody_le (within-signing-query TV induction) and tsum_probOutput_run_progSignBody_mul_enncard_le (expected cache growth of the reprogramming loop). No sorry or admit appear.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/GhostLayer.lean: The file adds the ghost-layer machinery for the Fiat-Shamir with aborts CMA-to-NMA reduction. It defines overlayCache and uncacheQuery on QueryCache, proves six lemmas about their interaction (e.g., overlayCache_cacheQuery_uncacheQuery, overlayCache_cacheQuery_ghost, overlayCache_apply_ghost_some, overlayCache_apply_ghost_none, overlayCache_cacheQuery_real_of_ghost_none, overlayCache_empty). It then defines ghostSignBody — a signing body over a two-layer (real+ghost) cache — and proves run_ghostSignBody_overlay (overlaying the ghost layer recovers progSignBody), run_ghostSignBody_fst (forgetting the ghost layer recovers transSignBody), and run_ghostSignBody_fst_eq_transSignBody. It also defines roStep (a caching random‑oracle step as a ProbComp) and proves randomOracle_run_eq_roStep. Finally it introduces the ghost‑instrumented hybrid handlers: ghostHybridImpl (parameterized by progSide), GhostState (layered cache, message list, bad flag), the ghost‑blind handler ghostBlindImpl (alias for the Trans‑side handler), and the run‑level onCache, hybridBaseImpl, hybridSignImpl; it proves ghostHybridImpl_agree_good, ghostHybridImpl_bad_mono, ghostBlindImpl_agree_good, and ghostBlindImpl_bad_mono. No sorry or admit appear.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/NMAHandler.lean: This new file defines the layered ghost-tagged NMA handler for the Fiat-Shamir with aborts hybrid signing body, introducing ghostSignProgramCont, simGhostSignBody, NmaGhostState, baseEmbed, and ghostNmaImpl. Key lemmas include: run_ghostSignProgramCont_overlay and run_simGhostSignBody_overlay (showing ghost-layer programming projects to plain cache programming), simGhostSignBody_support_ghost (ghost entries originate from input or signed message), ghostNmaImpl_preserves_signed_inv and ghostNmaImpl_run_signed_inv (ghost-layer points' messages are recorded in signed list), ghostNmaImpl_proj_hybrid (per-step overlay projection equals hybrid handler), signLiveCollision predicate and not_signLiveCollision_iff (defining the divergence event), and map_run_simulateQ_ghostNmaImpl_overlay / _empty (full-run overlay equality for sub-lemma (a)). No sorry or admit are present.
VCVio/CryptoFoundations/FiatShamir/WithAbort/GhostBodies/Projections.lean: This file introduces the 'Projections' module for the ghost-instrumented Fiat-Shamir with aborts layer. It defines the blindStepProj projection and proves several lemmas: blindStepProj_map_ghostBlindImpl_indep establishes that the observable projection of a single ghost-blind step is independent of the ghost-layer values (depending only on the ghost domain), ghostHybridImpl_proj_prog and ghostHybridImpl_proj_trans show per-step projections of the ghost-instrumented run onto the Prog and Trans hybrid handlers, and ghostHybridImpl_preserves_signed_inv provides a ghost-domain invariant ensuring that any ghost entry's message component appears in the signed list. The file also includes supporting lemmas onCache_run, hybridSignImpl_run, roStep_of_some, roStep_of_none, hybridBaseImpl_run_ro, ghostHybridImpl_run_ro_ghost_some, ghostHybridImpl_run_ro_ghost_none, ghostHybridImpl_run_sign, and ghostSignBody_support_ghost, which expand the runtime behavior of the relevant components.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security.lean: This file was completely restructured from a single monolithic module containing two placeholder theorems (euf_cma_bound and euf_cma_bound_perfectHVZK, both with sorry) and the loss function cmaToNmaLoss into an umbrella module that imports and re-exports nine new submodules (Loss, BodyHops, CouplingEngine, ReadRecording, TapeFactorization, HopLemmas, NMAReduction, Assembly). The docstring now describes the overall proof structure and ties the quantitative parameters (ε, p_abort, δ) to a 'good key' event following Theorem 3 of Barbosa et al. (CRYPTO 2023). All previous placeholder content was removed; no new sorry or admit are introduced.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Assembly.lean: This new file Assembly.lean adds the final bridging lemmas and the headline CMA-to-NMA security theorem for the Fiat-Shamir-with-aborts transform. It defines simulatedEufNmaAdv, a plain EUF-NMA adversary that forgets the managed cache, and proves managedRoNmaExp_simulatedNmaAdv_eq_eufNmaExp establishing that its managed-RO NMA success probability equals the plain EUF-NMA advantage. The main theorem euf_cma_to_nma then bounds any EUF-CMA adversary's advantage by the managed-RO NMA success probability of simulatedNmaAdv plus an explicit statistical loss cmaToNmaLoss, under assumptions on the HVZK simulator (hhvzk), signing and hash query bounds (hQ), and a good-key event Good bounding commitment-guessing (hGuess), abort probabilities (hAbort, hAbortSim), and key-generation complement (hGood). Finally, simulatedNmaAdv_nmaHashQueryBound proves that the reduction issues at most qH live hash queries, matching the hash-query bound required for the reduction's soundness. No sorry or admit are present.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/BodyHops.lean: This new file adds the per-signing-query core bound tvDist_run_transSignBody_simSignBody_le (the Trans → Sim hop), the hybrid experiment definition hybridExpAtKey, its verification-and-freshness continuation hybridVerifyCont, and three supporting lemmas (hybridExpAtKey_eq_run_bind, hybridVerifyCont_cache_congr, probOutput_true_hybridVerifyCont_of_mem). Together they supply the formal machinery needed for the CMA-to-NMA reduction chain (games G₀–G₃). No sorry or admit occur.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/CouplingEngine.lean: This new file (923 lines) adds the deferred-draw layer of the ghost-read bound for the EUF-CMA security of Fiat-Shamir with aborts. It defines the deferred-draw handler deferredDrawImpl with its state DeferredState and draw-collecting signing body ghostSignDrawBody, and proves: (1) the identical-until-bad lemmas probEvent_ghostHybridImpl_bad_eq_ghostBlind and probEvent_ghostHybridImpl_bad_le_ghostBlind showing the eager ghost handler and ghost-blind handler have equal (respectively bounded) bad probabilities; (2) the body-level tape factorization theorem evalDist_ghostSignDrawBody_eq_drawList_tapeSignBody recasting one signing body's inline draws as consumption from a pre-drawn tape, together with supporting distributional lemmas (evalDist_bind_comm_probComp, evalDist_bind_const_neverFails, evalDist_bind_congr_left); (3) the coupling theorem ghostBlind_bad_le_deferredDraw and its building blocks deferredCoupleInv, deferredCouple_step, deferredCouple_run, and signBody_couple that bound the ghost-blind bad marginal by the deferred-draw bad marginal via a pointwise state invariant; and (4) expected length bounds tsum_probOutput_run_ghostSignDrawBody_mul_length_le and tsum_probOutput_run_ghostSignDrawBody_mul_length_le_tight for the drawn commitment list. All declarations are noncomputable but contain no sorry or admit.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/HopLemmas.lean: This new file adds the hybrid hop lemmas (probOutput_unforgeableExp_eq_hybridExpAtKey_real, probOutput_hybridExpAtKey_real_le_prog, probOutput_hybridExpAtKey_prog_le_trans, probOutput_hybridExpAtKey_trans_le_sim) that form the core of the CMA-to-NMA security reduction for Fiat-Shamir with aborts. It also defines the flagLift cache-lifting construct and proves the supporting lemmas flagLift_run, isQueryBoundP_cast_pred, and sum_natCast_mul_pow_le_sq_sum_pow. Each hop lemma states a per-key-pair bound on the difference in success probability between successive hybrid experiments, using pointwise hypotheses (hGuess, hAbort, hQ, hhvzk, etc.) and is fully proved without any sorry or admit. The file is a self-contained module that re-exports through VCVio.CryptoFoundations.FiatShamir.WithAbort.Security.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/Loss.lean: This file introduces the statistical loss formulas for the Fiat-Shamir-with-aborts CMA-to-NMA security reduction, after Theorem 3 of CRYPTO 2023. It defines the noncomputable functions cmaToNmaLoss and perKeyLoss, plus the lemma cmaToNmaLoss_eq_perKeyLoss_add which decomposes the total loss into the per-key part plus the key-regularity failure probability δ. The docstring explains the loss formula L = 2·qS·(qH+1)·ε/(1-p) + qS·ε·(qS+1)/(2·(1-p)²) + qS·ζ_zk/(1-p) + δ and describes the hybrid-argument source of each term.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/NMAReduction.lean: Adds the file NMAReduction.lean (925 lines), which constructs and proves correctness of the NMA (No-Message Attack) reduction for Fiat-Shamir with aborts. The file defines three key QueryImpl.Stateful handlers: nmaOuterImpl (the inner managed handler that forwards uniform queries, answers hash queries via a managed cache, and answers signing queries using the simulator loop), nmaInnerImpl (the outer runtime handler that forwards uniform queries and answers residual live random-oracle queries), and nmaLinkImpl (their linked composition over a product cache). It defines the state projection proj2 from the layered ghost-tagged NMA state onto the linked handler's product cache. The core technical contribution is a series of lemmas (hproj2_unif, hproj2_ro, hproj2_ro_ghost_hit, hproj2_ro_fresh, hproj2_sign) establishing per-query equality between the ghost-tagged implementation and the linked managed implementation under this projection, bundled into hproj2_evalDist. This is lifted to a whole-run distributional equality in evalDist_map_run_simulateQ_ghostNmaImpl_proj2. The file then defines simulatedNmaAdv (the managed-RO NMA adversary) and proves hybridSimRun_le_managedRun_verify, which bounds the success probability of the simulated hybrid experiment (with freshness check) by that of the managed-RO NMA experiment. This culminates in probOutput_hybridExp_sim_le_managedRoNmaExp, the main reduction lemma that the NMA security of the Fiat-Shamir-with-aborts transform is bounded by the CMA security of the underlying signature scheme.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/ReadRecording.lean: This new file ReadRecording.lean introduces the read-recording handler deferredDrawReadImpl, which is identical to deferredDrawImpl but additionally accumulates adversarial random-oracle read commitments into an extra List Commit in state (using the new DeferredReadState abbrev). It defines the coupling invariant deferredReadInv (the underlying deferred states match, and if the bad flag is set then some recorded read-commit lies in the drawn list) and proves the per-query coupling step deferredDrawRead_step (each of uniform/read/sign steps preserves the invariant with equal outputs). From that it derives the run coupling deferredDrawRead_run (by induction on the adversary oracle program) and then the reduction deferredDraw_bad_le_readRecord, which states that the probability of the deferred-draw bad flag (z.2.2 = true) is at most the probability that the read-recording run's final state satisfies ∃ rc ∈ z.2.2, rc ∈ z.2.1.1.2 (some recorded read-commit is in the final drawn list). Finally, readRecord_pred_le_expected_coincidences applies Markov's inequality to bound the latter probability by the expected number of coincidences (recorded read-commits that appear in the drawn list). No sorry or admit statements are present.
VCVio/CryptoFoundations/FiatShamir/WithAbort/Security/TapeFactorization.lean: This new file in the Fiat-Shamir with aborts EUF-CMA security development introduces the first-moment reduction scaffolding for the coincidence-count bound and the fold-level tape factorization. It provides several supporting lemmas: geometric sum bounds (geomAttemptSum_le, geomSum_le), deterministic readlist length bound (deferredDrawReadImpl_run_readlist_length_le), expected drawn-list and attempt-count growth bounds for both step and run (deferredDrawReadImpl_step_expected_drawnlist_length_le, deferredDrawRead_run_expected_drawnlist_length_le, deferredDrawReadImpl_step_expected_attemptCount_le, deferredDrawRead_run_expected_attemptCount_le), never-fail and prefix-growth theorems, and the expected attempt-count mean bound (deferredDrawRead_attemptKn_mean_le). The main contribution defines the tape-consuming handler tapeDrawReadImpl and proves the core fold-level factorization theorem: the signing-query draw blocks commute to the front of the opaque adversary fold (via evalDist_tapePreserving_step_commute, drawList_combine_take_drop, evalDist_signStep_commute), showing that the entire deferred-draw run distributes as a pre-drawn tape of maxAttempts per signing query followed by a tape-consuming run.
VCVio/ProgramLogic/Relational/SimulateQ.lean: The diff revises a block comment in SimulateQ.lean to improve the explanation of the telescoping scaffold (avgBadM). The earlier reference to probOutput_lazyGhostFire_one as the single-pending base case is replaced with a more direct description: 'the same mass a lazy handler charges at the read, whose single-pending base case is one deferred draw hitting the read point.' Additionally, the comment's comparison is updated from 'missing-framework analogue' to 'state-law analogue' of expectedQuerySlack, more accurately reflecting that the section carries a state-law plus averaged-output invariant rather than a per-state resource charge.

Last updated: 2026-07-25 19:38 UTC.

dtumad

Follow-up on the current head: the earlier distributional blockers have been addressed in a substantial and mathematically useful way. In particular, the short secret/error samplers now model the intended eta-bounded box rather than uniform full-ring error; the seed-to-matrix and seed-to-short-vector steps are explicit computational idealizations with the unrestricted-adversary caveat stated; and the numerical non-vacuity result is now scoped as a statement about the loss parameters rather than a concrete security instantiation.

The HashInput API change is also an important soundness repair. Threading the cache-consistent preimage into isValid, and then requiring the recomputed ML-DSA commitment to equal the hashed commitment, closes the trivial solution in the earlier tailored problem. The extra 1/(1-p) on the HVZK term is coherent with the definition here as TV distance for each optional signing attempt; it is the restart-loop cost, whereas the CRYPTO 2023 theorem uses an accepted-transcript simulator.

The main mathematical boundary I would keep visible is the remaining gap between mldsaSTMSISShort and the standard SelfTargetMSIS normal form. Definition 4 in the paper and the published EasyCrypt model use a solution y whose final coefficient block is the challenge and require H(([I_m | A] y, mu)) to equal that block. The new algebraic characterization is valuable, but the current ML-DSA relation still goes through UseHint / encoded HighBits and does not yet supply that reduction to the standard matrix relation. Describing the present endpoint as a tailored self-target problem is accurate; a literature-facing standard-STMSIS headline would benefit from a separate explicit reduction.

I would not try to merge the full branch as one unit yet. It is currently conflicted with main, was validated on Lean 4.31 while main is on 4.32, and combines about 11.7k added lines across the generic retry/coupling engine, concrete ML-DSA laws, corrected MLWE modeling, and the final composition. That makes both regression review and attribution of any merge repair unnecessarily difficult.

A natural incremental route, if useful, seems to be:

Extract the generic HashInput threading plus the ML-DSA binding conjunct first. This is independently necessary and also unblocks a sound review of #479.
Land the corrected short-MLWE definitions and exact short-key swap as a focused model PR.
Land the explicit reduction from the tailored verifier relation to standard SelfTargetMSIS once that normal-form bridge is complete.
Review the generic CMA-to-NMA engine separately, then compose the final headline on the smaller landed pieces.

This is meant as a suggested way to preserve and land the strongest parts of the branch, rather than a request to reshape the working branch itself. The current head contains real progress over the earlier review; the remaining concern is chiefly the standard-hardness endpoint and the amount of independent semantic content bundled into one merge.

alik-eth · 2026-07-28T10:41:05Z

@dtumad Thanks for the careful reads — and agreed on the decomposition. Bundling ~11.7k lines into one merge was making both regression review and repair attribution harder than they needed to be; splitting into independently-reviewable pieces is the right call.

Step 1 is up as #503: the generic SelfTargetMSIS.isValid HashInput threading plus the ML-DSA binding conjunct, off current main. It adds a lightweight characterization mldsaSTMSIS_isValid_eq_true_iff (acceptance ↔ verifier acceptance ∧ hashInput.2 = w') so the self-target requirement stays visible and hard to drop. Deliberately narrow — just the binding; LatticeCrypto/Extern green on 4.32, the two touched declarations kernel-clean.

I'll follow your order for the rest: (2) the short-secret MLWE model + exact short-key swap as a focused PR; (3) the explicit reduction from the tailored verifier relation to the standard SelfTargetMSIS normal form — the H([I_m | A]·y, μ) form with the challenge as y's final coefficient block — once that bridge is complete; (4) the generic CMA-to-NMA engine reviewed on its own, composing the headline last on the landed pieces. I'll narrow #467 down as those land rather than merging it as a unit.

On the endpoint: agreed the current relation goes through UseHint/encoded HighBits and stops at the tailored verifier form; a literature-facing standard-STMSIS headline needs the explicit normal-form reduction, and I'll keep that scoped honestly until (3) lands. Also noted your point that the extra 1/(1-p) on the HVZK term is the restart-loop cost vs the CRYPTO 2023 accepted-transcript simulator — that framing is in the docstring.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…NMA development moves to Verified-zkEVM#467 Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-28T11:50:52Z

Step 2 is up as #504: the short-secret MLWE model + the exact NMA key-swap hop, stacked on #503.

sampleShortVec / keygenShort(1) (η-box short secrets, idealized keygen), mldsaMLWEShort + mldsaMatrixMLWE (the corrected short-secret MLWE, fixing the full-ring-uniform zero-advantage issue), expandAIdealization + the proven seed→matrix bridge advantage_mldsaMLWEShort_le_matrix;
nma_keyswap_hop_short bounds the NMA-game gap by the mldsaMLWEShort advantage as an exact identity — no idealGap/honestSamplingSlack term;
validKeyPairShort/identificationSchemeShort with the satisfiability certificate keygenShort_generable, so the introduced hypotheses are inhabited.

Purely additive (the old mldsaMLWE/nma_security chain is untouched, retired when the headline moves over); the STMSIS/extraction/headline stays out for steps 3–4. Full CI set green on 4.32; the three load-bearing decls kernel-clean.

Remaining: (3) the explicit tailored→standard-STMSIS normal-form reduction, (4) the CMA-to-NMA engine, then compose the headline on the landed pieces and narrow #467 accordingly.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-28T15:34:10Z

Step 4a is up as #507: the generic Fiat-Shamir-with-aborts CMA-to-NMA reduction engine, as its own reviewable unit (no ML-DSA content — pure VCVio machinery, verified to import nothing from LatticeCrypto/Extern).

It brings euf_cma_to_nma and its supporting development (the WithAbort/Security/ phase modules + GhostBodies/ machinery) onto main, replacing the current 151-line stub — and in doing so removes two sorry-backed placeholder theorems (euf_cma_bound/_perfectHVZK, confirmed zero consumers repo-wide) in favour of the proven reduction. cmaToNmaLoss/perKeyLoss are preserved via the umbrella. euf_cma_to_nma kernel-clean; full CI set + test libs green on 4.32.

That leaves: composing the ML-DSA headline (nma_security_short/_fips on the landed legs #504/#506 + this engine) and the tailored→standard SelfTargetMSIS normal-form reduction (the one genuinely-new piece). The decomposition stack is now #503 (binding) / #504 (short-MLWE) / #506 (STMSIS leg) / #507 (engine), with #479 as the Laws/Extern base.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth · 2026-07-28T20:34:48Z

The composition capstone is up as #508: the full short-model EUF-NMA/CMA headline assembled on the landed pieces — nma_security_short (exact key-swap + reprogramming + STMSIS extraction), nma_security_fips (FIPS keygen via expandSReplacement), euf_cma_security_of_nma_short (CMA composition on the #507 engine's euf_cma_to_nma), the matrix corollary, and the joint frontier witness trivial_euf_cma_security_of_nma_short (every hypothesis inhabited at abstract params — no native_decide). All kernel-clean [propext, Classical.choice, Quot.sound], additive, full CI set green on 4.32.

So the decomposition of the old 11.7k-line #467 is now a reviewable stack: #503 (binding) → #504 (short-MLWE) → #506 (STMSIS leg) → #507 (engine, independent) → #508 (headline), with #479 as the narrowed Laws/Extern base. #467 itself can be closed/narrowed once these land. The one genuinely-new piece — the tailored→standard SelfTargetMSIS normal-form reduction — is in progress separately.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

…ncrete witness (#479) * fix(MLDSA): make Primitives.Laws inhabitable; bank the FIPS-shaped witness Three Laws fields were jointly unsatisfiable, making every Laws-conditional MLDSA statement vacuously true: - expandS_honest_sampling asserted that the deterministic image of 2^256 seeds is distributed as uniform RqVec l x RqVec k, which fails by cardinality. The field is dropped; the MLWE key-swap hop instead carries an explicit total-variation slack hypothesis honestSamplingSlack idealGap, threaded through nma_keyswap_hop and nma_security as + idealGap (trivially satisfiable at idealGap = 1, quantitative under a ROM reading). - w1Encode_injective demanded injectivity on the full Vector High p.k carrier, false for the truncating packer; weakened to Set.InjOn on vectors of highBits representatives, which is what commitment binding uses. - expandMask_bound used gamma1 - 1 where FIPS 204's ExpandMask coefficients lie in [-gamma1 + 1, gamma1]; corrected to gamma1. Concrete/Laws.lean + Concrete/NonVacuity.lean bank the kernel-checked witness: seedRevealingPrims (concretePrimitives with the rho-component of expandSeed exposed) satisfies all Laws fields for any approved parameter set, so Primitives.Laws is now inhabitable (mldsa_laws_inhabited). Supporting encoding/sampling/rounding lemmas and Ring norm additions included. Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77 * fix(MLDSA): drop dead Laws hypothesis from the NMA chain; cite the de-vacuified theorems - nma_keyswap_hop bound _h_laws : Primitives.Laws and _hGap : 0 <= idealGap without using either; nma_security forwarded its own h_laws only into that dead binder. Both unused parameters are removed and the single call site is updated. nma_security keeps hGap, which is genuinely used by the ENNReal.ofReal_add split. - Concrete/NonVacuity.lean cited MLDSA.euf_cma_security_of_nma three times, a declaration that does not exist in the tree. The citations now name the theorems that actually consume and project a Primitives.Laws argument: idsWithAbort_complete, idsWithAbort_hvzk, fipsSign_fipsVerify_correct, and the algebraic lemmas keyGenFromSeed_wApprox_eq / recoverT0_eq. - Bank honestSamplingSlack_one: tvDist never exceeds 1, so idealGap = 1 satisfies honestSamplingSlack for every prims. Its docstring states that it certifies satisfiability only and carries no quantitative content. - Rewrite reactive/change-history docstring wording in Concrete/Laws.lean, Concrete/NonVacuity.lean, and SecurityNMA.lean to describe what each field and definition is, per the repo's intrinsic-docstring policy. No Laws field or theorem conclusion changes; the only signature changes are the removal of the dead hypotheses. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0122T9NmFkn5purmULtP2cME * fix(MLDSA): model the NMA key swap over short-box MLWE instead of full-ring uniform The EUF-NMA key-swap hop was stated against an MLWE problem whose secret and error were both uniform over the full ring carriers. Adding an independent full-carrier-uniform error to a finite additive group makes the sum uniform whatever the secret is, so the real and uniform branches of that problem coincide and its advantage is identically zero for every adversary; the companion `honestSamplingSlack` predicate compared the deterministic, eta-bounded `ExpandS` output against independent full-ring uniform vectors, whose only witness was the vacuous `idealGap = 1`. Model the hop over the short-secret distribution the ML-DSA Module-LWE assumption is actually stated over. `sampleShortVec` draws uniformly from the eta-bounded box; `keygenShort` / `keygenShort1` sample rho, K and (s1, s2) independently with short secrets; `mldsaMLWEShort` takes both its secret and its error from that box. The key swap `nma_keyswap_hop_short` is then an exact monad identity with no statistical slack, and `nma_security_short` carries the MLWE advantage alone. The deterministic FIPS derivation is reached by `nma_security_fips` through the named `expandSReplacement` assumption, whose ideal branch is short sampling with the FIPS marginals rather than full-ring uniformity. `advantage_mldsaMLWEShort_le_matrix` discharges the seed-to-matrix bridge onto the standard uniform-matrix `mldsaMatrixMLWE` under `expandAIdealization`. The short-key statements are indexed by the material-based key relation `validKeyPairShort` and the scheme tag `identificationSchemeShort`, which `keygenShort` genuinely generates; `keygenShort_generable` and `keygen0_generable` record that both `hGen` hypotheses are inhabited. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0122T9NmFkn5purmULtP2cME * refactor(MLDSA): keep the algebraic law bounds in LatticeCrypto, laws in Extern The maintainer review asks that only the SHAKE-dependent obligations cross into `Extern/`. Split `Extern/MLDSA/Laws.lean` accordingly. `LatticeCrypto/MLDSA/Concrete/LawBounds.lean` (new) keeps the statements that are ordinary algebra over the rounding, NTT, and byte-encoding layers and never name the assembled `concretePrimitives` bundle: * `polyNorm_eq_cInfNorm`, the `polyNorm` / `LatticeCrypto.cInfNorm` bridge; * `concrete_transform`, the `NTTRingLaws` witness for `concreteNTTRingOps`; * `bitUnpackPoly_z_cInfNorm_le`, the decode-range bound for the `z`-window unpacker, which holds for an arbitrary byte input; * `approved_gamma1_width` and `highBits_coeff_val_lt_width`, the parameter-set side conditions the two encoding laws consume, promoted from `private` so the Extern-side proofs can cite them. `Extern/MLDSA/Laws.lean` retains the twelve `concrete_*` fields that mention `concretePrimitives`, and `Extern/MLDSA/NonVacuity.lean` the `seedRevealingPrims` inhabitance witness — all of which reach the SHAKE wiring in `Extern/MLDSA/Instance.lean` and `Extern/MLDSA/Sampling.lean`. Verified with `scripts/check-extern-isolation.sh`: no proof library imports `Extern.…`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0122T9NmFkn5purmULtP2cME * refactor(MLDSA): narrow #479 to the Laws/Extern scope; NMA development moves to #467 Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77 --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: Devon Tuma <dtumad@gmail.com>

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

Closed

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

Merged

alik-eth mentioned this pull request Jul 12, 2026

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

Merged

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

alik-eth added 7 commits July 13, 2026 11:54

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

claude added 2 commits July 25, 2026 19:30

dtumad reviewed Jul 27, 2026

View reviewed changes

alik-eth mentioned this pull request Jul 28, 2026

fix(LatticeCrypto): bind SelfTargetMSIS solutions to their hashed preimage #503

Merged

alik-eth added a commit to alik-eth/VCV-io that referenced this pull request Jul 28, 2026

refactor(MLDSA): narrow Verified-zkEVM#479 to the Laws/Extern scope; …

86dd401

…NMA development moves to Verified-zkEVM#467 Claude-Session: https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

alik-eth mentioned this pull request Jul 28, 2026

feat(MLDSA): short-secret MLWE model and the exact NMA key-swap hop #504

Merged

This was referenced Jul 28, 2026

feat(MLDSA): tailored SelfTargetMSIS problem and the NMA extraction bound #506

Open

feat(FiatShamir): Fiat-Shamir-with-aborts CMA-to-NMA reduction engine #507

Open

alik-eth mentioned this pull request Jul 28, 2026

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

Open

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!

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

Uh oh!

🤖 PR Summary

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

Mathematical Formalization

Proof Completion (sorries removed)

Protocols / Soundness

Infrastructure / CI

Documentation

Refactoring

Uh oh!

dtumad left a comment

Choose a reason for hiding this comment

Uh oh!

alik-eth commented Jul 28, 2026

Uh oh!

alik-eth commented Jul 28, 2026

Uh oh!

alik-eth commented Jul 28, 2026

Uh oh!

alik-eth commented Jul 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 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

github-actions Bot commented Jul 25, 2026 •

edited

Loading