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

LatticeCrypto.lean

@@ -30,7 +30,9 @@ import LatticeCrypto.MLDSA.Arithmetic
 import LatticeCrypto.MLDSA.Concrete.Encoding
 import LatticeCrypto.MLDSA.Concrete.FFI
 import LatticeCrypto.MLDSA.Concrete.Instance
+import LatticeCrypto.MLDSA.Concrete.Laws
 import LatticeCrypto.MLDSA.Concrete.NTT
+import LatticeCrypto.MLDSA.Concrete.NonVacuity
 import LatticeCrypto.MLDSA.Concrete.Rounding
 import LatticeCrypto.MLDSA.Concrete.Sampling
 import LatticeCrypto.MLDSA.Encoding

LatticeCrypto/MLDSA/Concrete/NonVacuity.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2026 Oleksandr Vovkotrub. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oleksandr Vovkotrub
+-/
+import LatticeCrypto.MLDSA.Concrete.Laws
+
+/-!
+# Hypothesis-consistency certificate for `MLDSA.Primitives.Laws` (issue #228)
+
+`MLDSA.euf_cma_security_of_nma` is gated on `h_laws : Primitives.Laws prims nttOps`.  A conditional
+theorem asserts nothing if its hypothesis is uninhabitable, and `#print axioms` cannot detect that.
+This file rules that out with a kernel-checked witness: after the honest-sampling reformulation
+(the false `expandS_honest_sampling` uniformity field is gone, its gap carried as the explicit
+additive `honestSamplingSlack`/`idealGap`), `Primitives.Laws` is genuinely **inhabitable**.
+
+This is a **logical consistency (inhabitance) witness only**: `seedRevealingPrims` publishes the
+key-generation seed as the public `ρ`, so it is neither a faithful nor a secure ML-DSA
+instantiation, and no security claim about concrete ML-DSA follows from it.
+
+The witness `seedRevealingPrims` is `concretePrimitives` with the public `ρ`-component of
+`expandSeed`
+overridden to be the identity in the seed.  Every field consumed by the thirteen banked
+`concrete_*` laws is definitionally unchanged, so those laws transfer verbatim; the only remaining
+field, the determinacy assumption `keyVector_t0_determined`, holds trivially because the override
+makes the published seed-component injective (matching `ρ` forces the same seed, hence the same
+`t₀`).  This is the structural feature distinguishing the *satisfiable* `keyVector_t0_determined`
+from the *unsatisfiable* (cardinality-false) `expandS_honest_sampling` it replaced.
+
+**Trust surface.**  `mldsa_laws_inhabited` depends on `propext`, `Classical.choice`, `Quot.sound`,
+**and** the pre-existing `native_decide` certificate for the concrete `256×256` NTT matrix inversion
+(`MLDSA.Concrete.invNTTMatrix_nttMatrix_entry`, routed in through `concrete_transform`).  That
+`native_decide` axiom is **not** introduced here — it is already carried by every concrete ML-DSA
+fact (e.g. `concrete_transform` itself), since `concreteNTTRingOps` is the only `NTTRingLaws`
+instance in the tree.  The *abstract* headline `MLDSA.euf_cma_security_of_nma` (quantified over
+`nttOps`) is itself axiom-clean `[propext, Classical.choice, Quot.sound]`; this certificate only
+witnesses that its `Laws` hypothesis can be met by the concrete layer (whose NTT-correctness trust
+assumption it inherits).
+-/
+
+open MLDSA
+
+set_option maxRecDepth 4000
+
+namespace MLDSA
+
+/-- `concretePrimitives p` with the public `ρ`-component of `expandSeed` overridden to be the
+identity in the seed.  Every other field — including all fields consumed by the thirteen
+`concrete_*` laws — is definitionally equal to `concretePrimitives p`, so those laws transfer
+unchanged.  The override makes the published seed-component injective, which is exactly what
+`keyVector_t0_determined` needs.
+
+A **logical consistency witness** for `Primitives.Laws`: publishing the seed as `ρ` discards
+key secrecy, so this is not a faithful or secure ML-DSA instantiation — it exists to show the
+`Laws` hypothesis type is inhabited. -/
+def seedRevealingPrims (p : Params) : MLDSA.Primitives p :=
+  { MLDSA.Concrete.concretePrimitives p with
+      expandSeed := fun s => (s, ((MLDSA.Concrete.concretePrimitives p).expandSeed s).2) }
+
+/-- `Primitives.Laws (seedRevealingPrims p) concreteNTTRingOps` for any approved `p`.  Thirteen
+fields are
+the banked `concrete_*` lemmas (they typecheck because every field consumed there is defeq between
+`seedRevealingPrims p` and `concretePrimitives p`); `keyVector_t0_determined` needs only the
+hypothesis
+`((seedRevealingPrims p).expandSeed s).1 = ((seedRevealingPrims p).expandSeed s').1`, which
+reduces to `s = s'`,
+after which the two sides of the conclusion are syntactically identical. -/
+theorem seedRevealingPrims_laws (p : Params) (hp : p.isApproved) :
+    MLDSA.Primitives.Laws (seedRevealingPrims p) MLDSA.Concrete.concreteNTTRingOps where
+  sampleInBall_norm        := MLDSA.Concrete.concrete_sampleInBall_norm p
+  expandS_bound            := MLDSA.Concrete.concrete_expandS_bound p
+  expandMask_bound         := MLDSA.Concrete.concrete_expandMask_bound p hp
+  transform                := MLDSA.Concrete.concrete_transform
+  high_low_decomp          := MLDSA.Concrete.concrete_high_low_decomp p
+  lowBits_bound            := MLDSA.Concrete.concrete_lowBits_bound p hp
+  hide_low                 := MLDSA.Concrete.concrete_hide_low p hp
+  highBitsShift_injective  := MLDSA.Concrete.concrete_highBitsShift_injective p hp
+  useHint_makeHint         := MLDSA.Concrete.concrete_useHint_makeHint p hp
+  power2Round_decomp       := MLDSA.Concrete.concrete_power2Round_decomp p
+  power2Round_bound        := MLDSA.Concrete.concrete_power2Round_bound p
+  w1Encode_injective       := MLDSA.Concrete.concrete_w1Encode_injOn p hp
+  sampleInBall_smul_bound  := MLDSA.Concrete.concrete_sampleInBall_smul_bound p
+  keyVector_t0_determined  := by
+    intro s s' hρ _
+    -- `((seedRevealingPrims p).expandSeed s).1` reduces to `s`, so `hρ : s = s'`.
+    simp only [seedRevealingPrims] at hρ
+    subst hρ
+    rfl
+
+/-- **The #228 non-vacuity certificate.**  There is an approved parameter set and a primitive
+bundle whose `Primitives.Laws` is inhabited — so `MLDSA.euf_cma_security_of_nma` is not
+true-but-vacuous.  (See the trust-surface note in the module docstring on the inherited concrete
+NTT `native_decide` axiom.) -/
+theorem mldsa_laws_inhabited :
+    ∃ (p : Params) (prims : MLDSA.Primitives p),
+      Nonempty (MLDSA.Primitives.Laws prims MLDSA.Concrete.concreteNTTRingOps) :=
+  ⟨mldsa44, seedRevealingPrims mldsa44, ⟨seedRevealingPrims_laws mldsa44 (Or.inl rfl)⟩⟩
+
+end MLDSA

LatticeCrypto/MLDSA/Concrete/Rounding.lean

@@ -652,6 +652,23 @@ theorem highBitsShift_injective_of_isApproved (p : Params)
     simpa [highBitsShift] using congrArg (fun v : Rq => v.get j) hxy
   exact IsUnit.mul_right_injective (BalancedDecomp.ofApproved hp).hunit hcoeff
 
+/-- For approved parameters, each `HighBits` coefficient lies in the valid commitment window
+`[0, (q - 1) / (2 γ₂) - 1]`: its `ZMod` value is strictly below `(q - 1) / (2 γ₂)`. This is the
+range produced by Algorithm 37 and the domain on which the `w₁` packer is injective. -/
+theorem highBits_coeff_val_lt_m (p : Params) (hp : p.isApproved) (r : Rq) (i : Fin ringDegree) :
+    ((highBits p r).get i).val < (modulus - 1) / (2 * p.gamma2) := by
+  have hcoeff : highBitsCoeff (r.get i) p.gamma2 < (modulus - 1) / (2 * p.gamma2) := by
+    have ctx := BalancedDecomp.ofApproved hp
+    have h2 : (2 * p.gamma2) / 2 = p.gamma2 := by
+      rcases hp with rfl | rfl | rfl <;> decide
+    have := highBitsCoeff_lt_m ctx (r.get i)
+    rwa [h2] at this
+  have hval : ((highBits p r).get i).val = highBitsCoeff (r.get i) p.gamma2 := by
+    simp only [highBits, Vector.get_ofFn]
+    rw [ZMod.val_natCast_of_lt (lt_of_lt_of_le hcoeff (by
+      rcases hp with rfl | rfl | rfl <;> decide))]
+  rw [hval]; exact hcoeff
+
 /-- Concrete `Power2RoundOps` with `Power2High = Rq`. -/
 def concretePower2RoundOps : MLDSA.Power2RoundOps where
   Power2High := Power2High