fix(MLDSA): make Primitives.Laws inhabitable; bank the FIPS-shaped concrete witness by alik-eth · Pull Request #479 · Verified-zkEVM/VCVio

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

Extracts the ML-DSA Primitives.Laws repair and its concrete witness out of #467, per @quangvdao's review there, so it can land independently of the EUF-CMA development. #467 will be rebased on top once this merges.

The problem

On main, Primitives.Laws is uninhabitable — three fields are jointly (and individually) unsatisfiable — so every Laws-conditional MLDSA statement (nma_security, completeness, HVZK) is vacuously true. #print axioms cannot see this: the theorems are axiom-clean, they just assert nothing at any realizable instance.

expandS_honest_sampling asserts the deterministic image of 2^256 seeds is uniform on RqVec l × RqVec k — false by cardinality (2^256 < |Rq|).
w1Encode_injective demands injectivity on the full Vector High p.k carrier — false for the truncating packer.
expandMask_bound uses γ₁ − 1 where FIPS 204's ExpandMask coefficients lie in [-γ₁ + 1, γ₁] — spec drift.

The fix

expandS_honest_sampling 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. This is honest: trivially satisfiable at idealGap = 1, quantitative under a ROM reading of the XOF.
w1Encode_injective weakens to Set.InjOn on vectors of highBits representatives — exactly what commitment binding uses (w₁ always arises as such a vector).
expandMask_bound corrected to γ₁.

The witness (the non-vacuity certificate)

Concrete/Laws.lean + Concrete/NonVacuity.lean prove MLDSA.mldsa_laws_inhabited: the FIPS-shaped seedRevealingPrims (= concretePrimitives with the ρ-component of expandSeed exposed, a logical-consistency witness only) satisfies all Laws fields for any approved parameter set. Primitives.Laws is now inhabitable, so the conditional security statements have content.

Verification

lake build of the full CI library set on leanprover/lean4:v4.31.0: green, zero non-sorry warnings.
#print axioms MLDSA.nma_security: [propext, Classical.choice, Quot.sound].
#print axioms MLDSA.mldsa_laws_inhabited / seedRevealingPrims_laws: the same plus the one pre-existing, disclosed native_decide axiom for the NTT matrix inversion identity (invNTTMatrix_nttMatrix_entry).

The diff outside Primitives.lean + Concrete/ is the key-swap adaptation in SecurityNMA.lean and supporting norm lemmas in Ring/.

…tness 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

github-actions · 2026-07-12T23:31:53Z

🤖 PR Summary

MLDSA Primitives.Laws Fix and Non-Vacuity Certificate (FIPS 204 Alignment)

This PR repairs the Primitives.Laws structure, making it inhabitable (non-vacuously satisfiable) for all approved ML-DSA parameter sets. The primary changes correct three unsatisfiable fields, restore the binder to match FIPS 204 specifications, and provide a concrete witness, mldsa_laws_inhabited, proving non-vacuity.

Mathematical Formalization

LatticeCrypto/MLDSA/Primitives.lean – Laws Correction:
- expandS_honest_sampling (removed): Asserted deterministic expansion of 2^256 seeds gave a uniform distribution on RqVec l × RqVec k, which is false by cardinality. Replaced with a total-variation slack hypothesis honestSamplingSlack idealGap, threaded through nma_keyswap_hop and nma_security as an additive term + idealGap.
- w1Encode_injective (weakened to Set.InjOn ...): Now restricts injectivity to vectors that are in the range of highBits (i.e., contains w1 values). This is sufficient for commitment binding. The original Function.Injective was false for the truncating packer.
- expandMask_bound (fixed bound): Changed incorrect gamma1 - 1 to gamma1, matching the specification that ExpandMask coefficients lie in [–γ₁ + 1, γ₁].

Proof Completion / Sorries Removed

No new sorry or admit placeholders are introduced. The existing native_decide axiom for the NTT matrix inversion identity (invNTTMatrix_nttMatrix_entry) remains, as disclosed in axioms for mldsa_laws_inhabited.

Protocols / Soundness

honestSamplingSlack defined in LatticeCrypto/MLDSA/SecurityNMA.lean as a Prop parameterized by idealGap. The slack models the total-variation distance between the real secret derivation (via ExpandSeed/ExpandS) and an ideal independent-uniform secret. The theorem nma_keyswap_hop and nma_security now accept this slack and adjust the bound accordingly (|·| ≤ Adv^{MLWE} + idealGap). This fix prevents vacuously true security statements by replacing the previous false equality.

Infrastructure / CI

lake build completes cleanly on leanprover/lean4:v4.31.0 with zero non-sorry warnings.
#print axioms MLDSA.nma_security confirms: [propext, Classical.choice, Quot.sound].

Concrete Witness (Non-Vacuity)

LatticeCrypto/MLDSA/Concrete/Laws.lean (new): Proves 13 of the 14 fields of Primitives.Laws for the concrete concretePrimitives instance, covering all approved parameter sets. The remaining field, keyVector_t0_determined, is left abstract (inherent RO assumption). No sorry-backed aggregate witness is assembled here.
LatticeCrypto/MLDSA/Concrete/NonVacuity.lean (new): Defines seedRevealingPrims (overrides expandSeed with identity in seed) and proves seedRevealingPrims_laws using the 12 banked lemmas from Laws.lean. Provides mldsa_laws_inhabited, proving Primitives.Laws is inhabited for mldsa44, thus certifying non-vacuity of the security theorem.
LatticeCrypto/MLDSA/Concrete/Encoding.lean: Adds w1Encode_injOn proving w1Encode is injective on vectors whose coefficients are strictly below 2^simpleWidth((modulus-1)/(2*gamma2)-1). Also adds simpleBitUnpackPoly_simpleBitPackPoly for the decoder roundtrip.
LatticeCrypto/MLDSA/Concrete/Rounding.lean: Adds highBits_coeff_val_lt_m proving each highBits coefficient is in [0, (q-1)/(2γ₂)-1], the valid commitment window.
LatticeCrypto/MLDSA/Concrete/Sampling.lean: Adds structural output bounds for samplers: sampleInBall_coeff_mem (coeffs in {-1,0,1}), sampleInBall_norm (polyNorm ≤ 1), sampleInBall_l1Norm (centered ℓ₁ norm ≤ p.tau), expandS_bound (both components bounded).

Documentation / Meta

Updates to doc comments in Primitives.lean reflect the corrections (expandMask_bound bound, w1Encode_injective domain, removal of expandS_honest_sampling).
Module docstring in NonVacuity.lean explains structural changes from expandS_honest_sampling removal and inherited trust surface.
New imports import LatticeCrypto.MLDSA.Concrete.Laws and import LatticeCrypto.MLDSA.Concrete.NonVacuity added to the main library.

Refactoring

LatticeCrypto/MLDSA/Concrete/Sampling.lean: Refactors three rejection sampling functions (rejUniformCoeffs, rejEtaCoeffs, sampleInBall inner loop) from while-loop-based to structurally recursive, fuel-bounded Aux variants. This simplification paves the way for verification.
LatticeCrypto/Ring/Norms.lean: Adds cInfNorm_mul_le (cInfNorm (f * g) ≤ l1Norm f * cInfNorm g), used in sampleInBall_smul_bound.

Key Files

The core changes are in Primitives.lean (laws), SecurityNMA.lean (key-swap adaptation), and the new Concrete/Laws.lean and Concrete/NonVacuity.lean (witness). Remaining files (e.g., Encoding.lean, Rounding.lean, Sampling.lean) provide supporting lemmas; Ring/Norms.lean adds a norm bound used by the witness.

Statistics

Metric	Count
📝 Files Changed	10
✅ Lines Added	1609
❌ Lines Removed	128

Lean Declarations

✏️ Added: 91 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/SecurityNMA.lean (1)

def honestSamplingSlack (idealGap : ℝ) : Prop

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) :

✏️ Affected: 3 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
theorem nma_keyswap_hop (_h_laws : Primitives.Laws prims nttOps) in LatticeCrypto/MLDSA/SecurityNMA.lean moved from L334 to L372

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff largely conforms to the project's contributing guidelines, but there are a few items to note.

📄 **Per-File Summaries**

LatticeCrypto.lean: This diff adds two new import lines to LatticeCrypto.lean: import LatticeCrypto.MLDSA.Concrete.Laws and import LatticeCrypto.MLDSA.Concrete.NonVacuity. These imports bring in a module that presumably establishes algebraic or correctness laws for the concrete ML-DSA implementation, and a module that likely provides a proof of non-vacuity (i.e., that the specification is not trivially false). No sorry or admit statements were introduced.
LatticeCrypto/MLDSA/Concrete/Encoding.lean: This diff adds a significant body of supporting theory and several key theorems to Encoding.lean. It introduces new private helper theorems (bitOf_lt_two, array_getD_eq_getElem, bytesToBits_getD_lt_two, unpackNatArray_getD_lt) that establish bounds on the bit values produced by the existing bitUnpackPoly decoder; the main public theorem bitUnpackPoly_get then proves that each coefficient output by bitUnpackPoly is of the form b - v where v is a natural number strictly less than 2^(rangeWidth a b). A second block adds a functional model (packBitsList) and a series of private lemmas (forIn_push_flatten, packNatArray_eq, packBitsList_length, packBitsList_getD, bitOf_packByte_fin, bytearray_mk_getByteD, getByteD_bitsToBytes, bitsToBytes_size_of_mod, bytesToBits_bitsToBytes_getD, ofDigits_bits) that together characterize the roundtrip of packNatArray/unpackNatArray and bitsToBytes/bytesToBits. These culminate in the private lemma unpackNatArray_packNatArray_getD and the public theorem simpleBitUnpackPoly_simpleBitPackPoly, which states that simpleBitUnpackPoly inverts simpleBitPackPoly on any polynomial whose coefficients all lie strictly below 2^(simpleWidth b) (i.e., fit in the packer's bit width). A further set of private lemmas (ba_getElem?_getD, simpleBitPackPoly_size, packPolyVector_data_toList, getElem_flatten_const, sliceByteArray_packPolyVector, unpackPolyVector_packPolyVector, byteArrayToList_injective) establishes analogous vector-level roundtrip and injectivity results for the packPolyVector/unpackPolyVector combiners when the per-polynomial codec is a left inverse. These are then applied in the new public theorem w1Encode_injOn, which proves that w1Encode is injective on the set of commitment vectors whose every coefficient lies strictly below 2^simpleWidth((modulus - 1) / (2 * p.gamma2) - 1). No sorry or admit are added.
LatticeCrypto/MLDSA/Concrete/Laws.lean: This file (LatticeCrypto/MLDSA/Concrete/Laws.lean) is new and discharges 13 of the 14 fields of MLDSA.Primitives.Laws for the concrete concretePrimitives instance, across all approved parameter sets, using theorems from Concrete/Rounding.lean, Concrete/NTT.lean, Concrete/Encoding.lean, and Concrete/Sampling.lean. It proves: eight algebraic 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); two byte-encoding fields (concrete_expandMask_bound, concrete_w1Encode_injOn); two sampler-bound fields (concrete_sampleInBall_norm, concrete_expandS_bound); and the challenge-product bound concrete_sampleInBall_smul_bound (using the generic convolution-norm bound LatticeCrypto.cInfNorm_mul_le and sampleInBall_l1Norm). A bridge lemma polyNorm_eq_cInfNorm is provided. The file explicitly documents that the single remaining field keyVector_t0_determined is left abstract as an inherent random-oracle modeling assumption and that no sorry-backed aggregate witness is assembled.
LatticeCrypto/MLDSA/Concrete/NonVacuity.lean: This new file provides a non-vacuity certificate for the Primitives.Laws hypothesis required by the MLDSA.euf_cma_security_of_nma theorem. It defines seedRevealingPrims, a concrete MLDSA.Primitives bundle that overrides expandSeed to be the identity in the seed (making the keyVector_t0_determined law trivially true), and proves seedRevealingPrims_laws (a Primitives.Laws instance) by reusing the twelve existing banked concrete_* lemmas from LatticeCrypto.MLDSA.Concrete.Laws and a simple simp-based proof of keyVector_t0_determined. The existence theorem mldsa_laws_inhabited then witnesses Primitives.Laws for the approved parameter set mldsa44, ensuring that the security theorem is not vacuously true. The module docstring explains the structural change from the removed expandS_honest_sampling field and the inherited trust surface (including the pre-existing native_decide axiom for the concrete NTT matrix inversion).
LatticeCrypto/MLDSA/Concrete/Rounding.lean: This diff adds a new theorem highBits_coeff_val_lt_m which proves that for approved parameters, each coefficient of highBits is in the range [0, (q - 1) / (2 γ₂) - 1] as a ZMod value, which is the valid commitment window output by Algorithm 37 and the domain where the w₁ packer is injective. The proof uses highBitsCoeff_lt_m and the BalancedDecomp instance from hp, and performs case analysis on hp to compute (2 * p.gamma2) / 2 = p.gamma2. No sorry or admit are introduced, and no other definitions, signatures, or refactors are changed.
LatticeCrypto/MLDSA/Concrete/Sampling.lean: This diff replaces three while-loop-based rejection sampling functions (rejUniformCoeffs, rejEtaCoeffs, and the inner loop of sampleInBall) with structurally recursive, fuel-bounded Aux variants (rejUniformCoeffsAux, rejEtaStep / rejEtaCoeffsAux, sampleInBallFindChosen / sampleInBallStep / sampleInBallLoop), and factors rejEtaStep out as a separate function. It adds a large block of new theorems proving structural output bounds for these samplers: sampleInBall_coeff_mem and sampleInBall_norm (coefficients in {-1,0,1} with polyNorm ≤ 1), sampleInBall_l1Norm (centered ℓ₁ norm ≤ p.tau), sampleEtaPoly_norm (coefficients bounded by eta), and expandS_bound (both components of the secret vector are polyVecBounded). These lemmas also include auxiliary lemmas polyNorm_eq_cInfNorm', getD_set!_or, findChosen_le, step_size, step_fresh, countNZ-related invariants, EtaInv predicates, and requireFullEtaSample_mem.
LatticeCrypto/MLDSA/Primitives.lean: The diff modifies LatticeCrypto/MLDSA/Primitives.lean in the Primitives.Laws structure. The expandMask_bound law’s bound was changed from p.gamma1 - 1 to p.gamma1, with its doc comment updated to reflect that [γ₁, not γ₁-1] is the correct infinity-norm bound for ExpandMask output coefficients. The w1Encode_injective field was generalized from Function.Injective prims.w1Encode to Set.InjOn prims.w1Encode restricted to the set of vectors whose every component is in the range of highBits, and given an expanded doc comment explaining the narrower form is sufficient for the commitment-binding argument. Finally, the expandS_honest_sampling field was entirely removed, and the comment on the keyVector_t0_determined field was updated to remove the cross-reference to that removed field.
LatticeCrypto/MLDSA/SecurityNMA.lean: Added a new definition honestSamplingSlack (a Prop parameterized by a real idealGap) that quantifies the total-variation distance between the real secret derivation via ExpandSeed/ExpandS and an ideal independent-uniform secret derivation. The theorems nma_keyswap_hop and nma_security now take additional hypotheses idealGap, 0 ≤ idealGap, and hSlack : honestSamplingSlack … idealGap. The conclusion of nma_keyswap_hop changed from an equality bound |·| ≤ Adv^{MLWE} to |·| ≤ Adv^{MLWE} + idealGap; the proof uses hSlack and abs_probOutput_toReal_sub_le_tvDist instead of the previously assumed equality h_laws.expandS_honest_sampling. Consequently, nma_security’s bound now includes an additive term ENNReal.ofReal idealGap. The h_laws parameter in nma_keyswap_hop is now unused (underscored). Comments and the closing note were updated to explain that the deterministic XOFs cannot yield equality, so the slack is a quantitative ROM modeling assumption rather than a false equality.
LatticeCrypto/Ring/Norms.lean: This change adds several new theorems and supporting definitions to LatticeCrypto/Ring/Norms.lean, establishing a bound on the centered ℓ∞ norm of a negacyclic product of polynomials in ℤ_q[X]/(X^n + 1). Specifically, it adds l1Norm_eq_sum expressing the ℓ₁ norm as a sum of absolute centered coefficients; the private definitions intConvCoeff (an integer-valued negacyclic convolution) and intConvCoeff_natAbs_le (proving its absolute value is bounded by l1Norm f * cInfNorm g); negacyclicConvCoeff_eq_intCast (showing the ZMod q coefficient is the integer cast of intConvCoeff); mul_get_eq_convCoeff (equating a product's coefficient to the negacyclic convolution of coefficient functions); and the central result cInfNorm_mul_le which proves cInfNorm (f * g) ≤ l1Norm f * cInfNorm g, using a case split on whether 2 * bound < q. No new sorry or admit are introduced.
LatticeCrypto/Ring/Transform.lean: Added a new theorem coeffScalarVecMul_get which states that the j-th entry of coeffScalarVecMul c v equals c * (v.get j), establishing that coefficient-domain scalar-vector multiplication acts component-wise as the underlying ring multiplication. The proof uses coeffScalarVecMul, unhatVec_get, scalarVecMul, hatVec_get, Vector.get_map, the ring isomorphism property laws.toHat_mul, and laws.fromHat_toHat.

Last updated: 2026-07-12 23:31 UTC.

alik-eth mentioned this pull request Jul 12, 2026

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

Open

alik-eth mentioned this pull request Jul 12, 2026

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

Open

jasonsoroko mentioned this pull request Jul 14, 2026

LatticeCrypto: discharging the challenge–secret norm-bound hypotheses — offering a proved no-wraparound multiplication bound #469

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

fix(MLDSA): make Primitives.Laws inhabitable; bank the FIPS-shaped concrete witness#479
alik-eth wants to merge 1 commit into
Verified-zkEVM:mainfrom
alik-eth:mldsa-laws

alik-eth commented Jul 12, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

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

Uh oh!

The problem

The fix

The witness (the non-vacuity certificate)

Verification

Uh oh!

github-actions Bot commented Jul 12, 2026

🤖 PR Summary

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

alik-eth commented Jul 12, 2026 •

edited

Loading