fix: non-vacuous range-check specs + verdict-engine hypothesis audit

examples/halva-range-check/spec.lean

@@ -3,12 +3,17 @@
 import Mathlib.Algebra.Field.ZMod
 import Mathlib.Tactic.LinearCombination
 
-/-- Specification: when the range-check selector is enabled at a row,
-    the advice value in that row is in [0, 10).
-    Requires the prime P > 10 so that ZMod P casts are injective on Fin 10. -/
+/-- Specification: when the range-check selector is enabled at a row, the advice
+    value in that row is genuinely in [0, 10) — its canonical natural representative
+    `ZMod.val` is `< 10`.
+
+    This is the honest, non-vacuous statement. The form
+    `∃ k : Fin 10, (k.val : ZMod P) = advice` is vacuous when `P ≤ 10` (the casts of
+    `0..9` then cover all of `ZMod P`), so it is provable without ever using `hp`.
+    `ZMod.val advice < 10` cannot be proved without `hp : P > 10`. -/
 def Spec (c: ValidCircuit P P_Prime) (hp: P > 10): Prop :=
   ∀ row : ℕ, c.get_selector 0 row = 1 →
-    ∃ k : Fin 10, (k.val : ZMod P) = c.get_advice 0 row
+    ZMod.val (c.get_advice 0 row) < 10
 
 /-- Soundness: if the circuit meets all halo2 constraints (extracted by Halva),
     then it satisfies the range-check specification.

lean/ZkGadgets.lean

@@ -1,3 +1,4 @@
+import ZkGadgets.Audit
 import ZkGadgets.Field
 import ZkGadgets.RangeCheck
 import ZkGadgets.ConditionalSelect

lean/ZkGadgets/Audit.lean

@@ -0,0 +1,99 @@
+import Lean
+
+/-!
+# Spec audit — hypothesis-liveness checks (verdict engine, C1)
+
+The Lean kernel checks that a *proof* is correct, but nothing checks that the
+*statement* is meaningful. This module is the deterministic core of a "verdict
+engine": a refuter that complements the (single-sided) proof loop by flagging
+degenerate statements a kernel-accepted proof would otherwise hide.
+
+It implements **C1, hypothesis-liveness**, which catches two real regression
+classes that both shipped in this repo at one point:
+
+* **Decorative hypothesis** — a statement carries an explicit hypothesis its proof
+  never uses (e.g. a bound passed to a `Spec` but ignored). `#audit_uses` flags it.
+* **Dropped side-condition** — an intended hypothesis never reaches the signature
+  (e.g. a `variable (hp : p > 256)` the theorem never references, so Lean omits it).
+  `#audit_requires` guards a load-bearing condition by name.
+
+Both commands fail the build (`logError`) when they fire, so they act as live CI
+gates next to a theorem. The remaining checks — finite-model non-vacuity probes
+(C2), antecedent satisfiability (C3), and an adversarial refuter (C4) — are future
+work and not implemented here.
+-/
+
+open Lean Elab Command Meta
+
+namespace ScribeAudit
+
+/-- The names of a declaration's **explicit, proposition-typed** binders that do not
+    occur in its proof term — i.e. hypotheses the proof never uses. A non-empty
+    result is a "decorative hypothesis" smell. -/
+def unusedHyps (declName : Name) : MetaM (Array Name) := do
+  let info ← getConstInfo declName
+  -- `ConstantInfo.value?` excludes theorems, so match explicitly.
+  let value ← match info with
+    | .thmInfo ti => pure ti.value
+    | .defnInfo di => pure di.value
+    | _ => throwError "audit: '{declName}' has no proof term to inspect"
+  lambdaTelescope value fun args body => do
+    let mut unused : Array Name := #[]
+    for arg in args do
+      let fvarId := arg.fvarId!
+      let ldecl ← fvarId.getDecl
+      -- only consider explicit hypotheses; skip implicits and instance arguments
+      if ldecl.binderInfo.isExplicit && (← isProp ldecl.type) then
+        unless body.hasAnyFVar (· == fvarId) do
+          unused := unused.push ldecl.userName
+    return unused
+
+/-- Render a declaration's type as a flat string for substring checks. -/
+def signatureString (declName : Name) : MetaM String := do
+  let info ← getConstInfo declName
+  return toString (← ppExpr info.type)
+
+end ScribeAudit
+
+/-- `#audit_uses thm` fails the build if `thm` has an explicit hypothesis its proof
+    never uses (a decorative / possibly-vacuous hypothesis). Silent on success, so it
+    works as a live regression gate placed next to a theorem. -/
+elab "#audit_uses " id:ident : command => do
+  liftTermElabM do
+    let declName ← realizeGlobalConstNoOverload id
+    let unused ← ScribeAudit.unusedHyps declName
+    unless unused.isEmpty do
+      let names := String.intercalate ", " (unused.toList.map toString)
+      logError m!"audit ✗ {declName}: unused (possibly decorative) hypotheses: {names}"
+
+/-- `#audit_requires thm "needle"` fails the build unless `needle` appears in `thm`'s
+    signature. Use it to pin a load-bearing side-condition (e.g. `"p > 256"`) so that
+    silently dropping it — the classic vacuous-spec regression — turns the build red. -/
+elab "#audit_requires " id:ident needle:str : command => do
+  liftTermElabM do
+    let declName ← realizeGlobalConstNoOverload id
+    let sig ← ScribeAudit.signatureString declName
+    let needleStr := needle.getString
+    unless (sig.splitOn needleStr).length ≥ 2 do
+      logError m!"audit ✗ {declName}: required hypothesis '{needleStr}' is absent from the signature — it may have been dropped"
+
+namespace ScribeAudit.SelfTest
+
+-- The decoy below deliberately ignores a hypothesis; that is the property under test.
+set_option linter.unusedVariables false
+
+-- A hypothesis the proof never uses: must be reported.
+private theorem decoy_decorative (n : Nat) (hbig : n > 5) : n = n := rfl
+-- A hypothesis the proof genuinely uses: must not be reported.
+private theorem decoy_live (n : Nat) (h : n = 0) : n = 0 := h
+
+-- Deterministic unit test of the detection logic (independent of message wording).
+run_cmd liftTermElabM do
+  let bad ← ScribeAudit.unusedHyps ``decoy_decorative
+  unless bad == #[`hbig] do
+    throwError "audit self-test failed: expected [hbig] unused, got {bad}"
+  let good ← ScribeAudit.unusedHyps ``decoy_live
+  unless good.isEmpty do
+    throwError "audit self-test failed: expected no unused hyps, got {good}"
+
+end ScribeAudit.SelfTest

lean/ZkGadgets/HalvaRangeCheck.lean

@@ -4,6 +4,7 @@ import Mathlib.Data.ZMod.Defs
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Algebra.Field.ZMod
 import Mathlib.Tactic.LinearCombination
+import ZkGadgets.Audit
 
 set_option linter.unusedVariables false
 
@@ -113,12 +114,19 @@ def meets_constraints (c: ValidCircuit P P_Prime): Prop :=
   all_shuffles c ∧
   ∀ col row: ℕ, (row < c.n ∧ row ≥ c.usable_rows) → c.1.Instance col row = c.1.InstanceUnassigned col row
 
-/-- Specification: when the range-check selector is enabled at a row,
-    the advice value in that row is in [0, 10).
-    Requires the prime P > 10 so that ZMod P casts are injective on Fin 10. -/
+/-- Specification: when the range-check selector is enabled at a row, the advice
+    value in that row is genuinely in [0, 10) — i.e. its canonical natural
+    representative `ZMod.val` is `< 10`.
+
+    This is the honest, non-vacuous statement. The earlier form
+    `∃ k : Fin 10, (k.val : ZMod P) = advice` is vacuous when `P ≤ 10` (the casts of
+    `0..9` then cover all of `ZMod P`), so it is provable without ever using `hp` —
+    making `hp` decorative. `ZMod.val advice < 10` cannot be proved without `hp`:
+    the bound `P > 10` is exactly what forces `ZMod.val` to agree with the small
+    integer the advice cell encodes. -/
 def Spec (c: ValidCircuit P P_Prime) (hp: P > 10): Prop :=
   ∀ row : ℕ, c.get_selector 0 row = 1 →
-    ∃ k : Fin 10, (k.val : ZMod P) = c.get_advice 0 row
+    ZMod.val (c.get_advice 0 row) < 10
 
 /-- Soundness: if the circuit meets all halo2 constraints (extracted by Halva),
     then it satisfies the range-check specification.
@@ -127,44 +135,62 @@ theorem soundness (c: ValidCircuit P P_Prime) (hp: P > 10)
     (h: meets_constraints c): Spec c hp := by
   haveI : Fact (Nat.Prime P) := ⟨P_Prime⟩
   intro row hsel
-  unfold meets_constraints at h
-  obtain ⟨_, _, _, _, _, _, hgates, _⟩ := h
-  unfold all_gates gate_0 at hgates
-  have hgate := hgates row
-  simp only [hsel, one_mul] at hgate
-  set v := c.get_advice 0 row with hv
-  -- Product of 10 factors = 0; since ZMod P is a field (prime P), split on which factor is 0
-  rcases mul_eq_zero.mp hgate with h | h
-  · rcases mul_eq_zero.mp h with h | h
+  -- The gate forces the advice value to be one of the field elements 0..9.
+  have hex : ∃ k : Fin 10, ((k.val : ℕ) : ZMod P) = c.get_advice 0 row := by
+    unfold meets_constraints at h
+    obtain ⟨_, _, _, _, _, _, hgates, _⟩ := h
+    unfold all_gates gate_0 at hgates
+    have hgate := hgates row
+    simp only [hsel, one_mul] at hgate
+    set v := c.get_advice 0 row with hv
+    -- Product of 10 factors = 0; since ZMod P is a field (prime P), split on which factor is 0
+    rcases mul_eq_zero.mp hgate with h | h
     · rcases mul_eq_zero.mp h with h | h
       · rcases mul_eq_zero.mp h with h | h
         · rcases mul_eq_zero.mp h with h | h
           · rcases mul_eq_zero.mp h with h | h
             · rcases mul_eq_zero.mp h with h | h
               · rcases mul_eq_zero.mp h with h | h
                 · rcases mul_eq_zero.mp h with h | h
-                  · -- v = 0
-                    exact ⟨⟨0, by omega⟩, by simpa using h.symm⟩
-                  · -- 1 + -v = 0  →  v = 1
-                    have hv1 : v = 1 := by linear_combination -h
-                    exact ⟨⟨1, by omega⟩, by simpa using hv1.symm⟩
-                · -- 2 + -v = 0  →  v = 2
-                  have hv2 : v = 2 := by linear_combination -h
-                  exact ⟨⟨2, by omega⟩, by simpa using hv2.symm⟩
-              · have hv3 : v = 3 := by linear_combination -h
-                exact ⟨⟨3, by omega⟩, by simpa using hv3.symm⟩
-            · have hv4 : v = 4 := by linear_combination -h
-              exact ⟨⟨4, by omega⟩, by simpa using hv4.symm⟩
-          · have hv5 : v = 5 := by linear_combination -h
-            exact ⟨⟨5, by omega⟩, by simpa using hv5.symm⟩
-        · have hv6 : v = 6 := by linear_combination -h
-          exact ⟨⟨6, by omega⟩, by simpa using hv6.symm⟩
-      · have hv7 : v = 7 := by linear_combination -h
-        exact ⟨⟨7, by omega⟩, by simpa using hv7.symm⟩
-    · have hv8 : v = 8 := by linear_combination -h
-      exact ⟨⟨8, by omega⟩, by simpa using hv8.symm⟩
-  · have hv9 : v = 9 := by linear_combination -h
-    exact ⟨⟨9, by omega⟩, by simpa using hv9.symm⟩
+                  · rcases mul_eq_zero.mp h with h | h
+                    · -- v = 0
+                      exact ⟨⟨0, by omega⟩, by simpa using h.symm⟩
+                    · -- 1 + -v = 0  →  v = 1
+                      have hv1 : v = 1 := by linear_combination -h
+                      exact ⟨⟨1, by omega⟩, by simpa using hv1.symm⟩
+                  · -- 2 + -v = 0  →  v = 2
+                    have hv2 : v = 2 := by linear_combination -h
+                    exact ⟨⟨2, by omega⟩, by simpa using hv2.symm⟩
+                · have hv3 : v = 3 := by linear_combination -h
+                  exact ⟨⟨3, by omega⟩, by simpa using hv3.symm⟩
+              · have hv4 : v = 4 := by linear_combination -h
+                exact ⟨⟨4, by omega⟩, by simpa using hv4.symm⟩
+            · have hv5 : v = 5 := by linear_combination -h
+              exact ⟨⟨5, by omega⟩, by simpa using hv5.symm⟩
+          · have hv6 : v = 6 := by linear_combination -h
+            exact ⟨⟨6, by omega⟩, by simpa using hv6.symm⟩
+        · have hv7 : v = 7 := by linear_combination -h
+          exact ⟨⟨7, by omega⟩, by simpa using hv7.symm⟩
+      · have hv8 : v = 8 := by linear_combination -h
+        exact ⟨⟨8, by omega⟩, by simpa using hv8.symm⟩
+    · have hv9 : v = 9 := by linear_combination -h
+      exact ⟨⟨9, by omega⟩, by simpa using hv9.symm⟩
+  -- Convert membership in {0..9} to the honest bound. This step needs `hp : P > 10`:
+  -- without it `ZMod.val` of the cast could wrap around and exceed 10.
+  obtain ⟨k, hk⟩ := hex
+  have hkP : (k.val : ℕ) < P := by have := k.isLt; omega
+  rw [← hk, ZMod.val_natCast_of_lt hkP]
+  exact k.isLt
+
+/-- Non-vacuity witness: the bound `ZMod.val advice < 10` is a genuine restriction.
+    In `ZMod 11` (prime, > 10) the element `10` refutes it, so the spec is not
+    `True` in disguise and the `P > 10` hypothesis is load-bearing. -/
+example : ¬ ((10 : ZMod 11).val < 10) := by decide
 
 
 end RangeCheck
+
+-- Verdict-engine guards (C1): the `P > 10` bound must stay in the signature, and the
+-- soundness proof must actually use it (it was decorative before the non-vacuity fix).
+#audit_requires RangeCheck.soundness "P > 10"
+#audit_uses RangeCheck.soundness

lean/ZkGadgets/RangeCheck.lean

@@ -1,4 +1,5 @@
 import ZkGadgets.Field
+import ZkGadgets.Audit
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.Fin.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
@@ -11,17 +12,27 @@ Constraint system:
   b_i * (b_i - 1) = 0       for i in [0, 8)   (each bit is boolean)
   sum (b_i * 2^i) = x                           (bit decomposition)
 
-Soundness: if the constraints hold and p > 256, then x is in [0, 256).
+Soundness: if the constraints hold and p > 256, then `x` is genuinely a byte,
+i.e. its canonical natural representative is in [0, 256).
+
+The conclusion is `ZMod.val x < 256`, NOT `∃ k : Fin 256, (k.val : ZMod p) = x`.
+The existential is vacuous whenever `p ≤ 256` (every field element is then the cast
+of some byte), so it would state something strictly weaker than "x is a byte" and
+could be proved without ever using `hp`. `ZMod.val x < 256` cannot be proved without
+`hp` — the bound `p > 256` is what makes `ZMod.val` agree with the integer value.
 -/
 
-variable (p : ℕ) [Fact (Nat.Prime p)] (hp : p > 256)
+variable (p : ℕ) [Fact (Nat.Prime p)]
 
 theorem range_check_8bit_sound
+    -- `hp` is an explicit, load-bearing hypothesis: the proof fails without it, and
+    -- `#check @range_check_8bit_sound` shows it in the signature (it is not dropped).
+    (hp : p > 256)
     (x : ZMod p)
     (bits : Fin 8 → ZMod p)
     (h_bit : ∀ i : Fin 8, bits i * (bits i - 1) = 0)
     (h_decomp : (∑ i : Fin 8, bits i * (2 : ZMod p) ^ (i : ℕ)) = x) :
-    ∃ k : Fin 256, (k.val : ZMod p) = x := by
+    ZMod.val x < 256 := by
   -- Each bit is 0 or 1 in ZMod p
   have h01 : ∀ i, bits i = 0 ∨ bits i = 1 := fun i => bit_boolean p (bits i) (h_bit i)
   -- Natural representative for each bit
@@ -40,9 +51,25 @@ theorem range_check_8bit_sound
       exact Nat.mul_le_mul_right _ (hle i)
     · simp only [Fin.sum_univ_succ, Fin.sum_univ_zero, Fin.val_zero, Fin.val_succ]
       omega
-  -- Provide the Fin 256 witness
-  exact ⟨⟨∑ i : Fin 8, nb i * 2 ^ (i : ℕ), hlt⟩, by
+  -- x is the cast of the natural weighted sum N, with N < 256.
+  have hxN : x = ((∑ i : Fin 8, nb i * 2 ^ (i : ℕ) : ℕ) : ZMod p) := by
     rw [← h_decomp]
     push_cast
     congr 1; ext i
-    rw [hcast i]⟩
+    rw [hcast i]
+  -- N < 256 < p (this is where `hp` is used), so `ZMod.val` of the cast is exactly N.
+  have hNp : (∑ i : Fin 8, nb i * 2 ^ (i : ℕ)) < p := by omega
+  rw [hxN, ZMod.val_natCast_of_lt hNp]
+  exact hlt
+
+/-- Non-vacuity witness: the byte bound `ZMod.val x < 256` is a genuine restriction,
+    not `True` in disguise. In `ZMod 257` (prime, > 256) the element `256` refutes the
+    conclusion — so the soundness theorem is saying something real, and dropping the
+    constraints (or the `p > 256` hypothesis) would make it false. This is the kind of
+    refutation a spec-level search should always be able to find for an honest spec. -/
+example : ¬ ((256 : ZMod 257).val < 256) := by decide
+
+-- Verdict-engine guards (C1): fail the build if the `p > 256` bound is ever dropped
+-- from the signature, or if the proof stops using a declared hypothesis.
+#audit_requires range_check_8bit_sound "p > 256"
+#audit_uses range_check_8bit_sound