Grow the negative corpus to five audit-bug classes

README.md

@@ -217,7 +217,7 @@ Every theorem below is complete and kernel-checked (`lake build` is green, and e
 
 ## Benchmark: ZKGadgetEval
 
-`crates/bench` runs the proof loop over a 17-gadget suite (`benchmark/suite.toml`, tiers 1–3 by difficulty) and reports statistics an eval can be judged on, not just a smoke-test pass count:
+`crates/bench` runs the proof loop over a 20-gadget suite (`benchmark/suite.toml`, tiers 1–3 by difficulty) and reports statistics an eval can be judged on, not just a smoke-test pass count:
 
 ```sh
 cargo run -p zkgadget-eval -- --backend claude --budget 5 \
@@ -226,7 +226,7 @@ cargo run -p zkgadget-eval -- --backend claude --budget 5 \
 
 - **`--samples k`** — resample each gadget *k* times; per gadget the JSON reports the unbiased **pass@k** estimator (`1 − C(n−c,k)/C(n,k)`) for every `k ≤ n` plus a **Wilson 95% interval** on the per-sample prove probability, so run-to-run variance is measured instead of hidden.
 - **`--modes build,lsp`** — the feedback-mode axis (raw `lake build` text vs. structured LSP goal states) runs inside one invocation as an A/B; the summary is broken down per mode.
-- **Negative gadgets** — the suite contains deliberately under-constrained circuits whose spec is *false* (`kind = "negative"`): a 2-bit range check missing a boolean constraint, and a gadget whose only constraint is `x − x = 0` with spec `x = 0`. The loop is graded on **refusing** to prove them. A "proved" negative is a soundness alarm: the run prints it loudly and exits `2`. Without negatives, a suite cannot distinguish "the loop proves true specs" from "the loop proves anything you hand it".
+- **Negative gadgets** — the suite contains five deliberately buggy circuits whose spec is *false* (`kind = "negative"`), spanning distinct audit-bug classes: a range check missing a boolean constraint, a vacuous `x − x = 0` constraint, the classic is-zero gadget missing its `x·out = 0` half, a swap gate with a dangling output wire, and a one-term constraint typo (`x·inv − inv` for `x·inv − 1`). Every spec is kernel-checked *false* (a concrete counterexample refutes it, documented in each TOML), gadget names are neutral so nothing the model sees marks them as traps, and the loop is graded on **refusing** to prove them. A "proved" negative is a soundness alarm: the run prints it loudly and exits `2`. Without negatives, a suite cannot distinguish "the loop proves true specs" from "the loop proves anything you hand it".
 
 Honest limitations: the suite exercises algebraic gate constraints only (no lookup or permutation arguments — see the scope note above), and samples are independent reruns of the same nondeterministic loop, not seed-controlled.
 

benchmark/suite.toml

@@ -117,3 +117,24 @@ tier = 1
 constraints = 1
 kind = "negative"
 description = "NEGATIVE: only constraint is x - x = 0, spec claims x = 0 — spec is false"
+
+[[gadgets]]
+file = "suite/18-neg-is-zero-missing-constraint.toml"
+tier = 2
+constraints = 1
+kind = "negative"
+description = "NEGATIVE: is-zero missing the x*out = 0 constraint — nonzero x can claim out = 1"
+
+[[gadgets]]
+file = "suite/19-neg-swap-unconstrained-output.toml"
+tier = 2
+constraints = 2
+kind = "negative"
+description = "NEGATIVE: swap gate with the out2 mux constraint dropped — out2 is a dangling wire"
+
+[[gadgets]]
+file = "suite/20-neg-wrong-inverse-constraint.toml"
+tier = 1
+constraints = 1
+kind = "negative"
+description = "NEGATIVE: inverse constraint typo (x*inv - inv = 0) — satisfied by inv = 0 for any x"

benchmark/suite/18-neg-is-zero-missing-constraint.toml

@@ -0,0 +1,39 @@
+# NEGATIVE GADGET — the classic is-zero bug. The proof loop MUST fail here.
+#
+# A real is-zero gadget needs BOTH constraints:
+#   x * out = 0               (dropped here — the bug)
+#   x * x_inv + out - 1 = 0
+# With only the completeness constraint, a nonzero x can claim out = 1 by
+# setting x_inv = 0. This is the exact under-constraint class repeatedly found
+# in production isZero gadgets during audits.
+#
+# Counterexample (kernel-checked at p = 5): x = 1, x_inv = 0, out = 1
+# satisfies the remaining constraint (1*0 + 1 - 1 = 0) but violates the spec.
+#
+# The gadget `name` is deliberately NEUTRAL (it becomes the theorem name the
+# model sees); only this manifest-side file marks it negative.
+
+name = "zero-indicator"
+modulus = "21888242871839275222246405745257275088548364400416034343698204186575808495617"
+soundness_spec = "(x = 0 ∧ out = 1) ∨ (x ≠ 0 ∧ out = 0)"
+
+[[witnesses]]
+id = 0
+name = "x"
+
+[[witnesses]]
+id = 1
+name = "x_inv"
+
+[[witnesses]]
+id = 2
+name = "out"
+
+# x * x_inv + out - 1 = 0   (the x * out = 0 constraint is DELIBERATELY OMITTED)
+[[constraints]]
+label = "completeness"
+terms = [
+    { coeff = "1", vars = [0, 1] },
+    { coeff = "1", vars = [2] },
+    { coeff = "-1", vars = [] },
+]

benchmark/suite/19-neg-swap-unconstrained-output.toml

@@ -0,0 +1,56 @@
+# NEGATIVE GADGET — unconstrained output wire. The proof loop MUST fail here.
+#
+# A swap gate needs a mux constraint on BOTH outputs:
+#   b*(b-1) = 0
+#   out1 - in1 + b*in1 - b*in2 = 0
+#   out2 - in2 - b*in1 + b*in2 = 0   (dropped here — the bug)
+# With out2 unconstrained, the "swap" can emit any value on its second wire.
+# Dangling/unconstrained output wires are a staple of real circuit audits.
+#
+# Counterexample (kernel-checked at p = 5): b = 0, in1 = in2 = out1 = 0,
+# out2 = 1 satisfies both remaining constraints but violates the spec.
+#
+# The gadget `name` is deliberately NEUTRAL (it becomes the theorem name the
+# model sees); only this manifest-side file marks it negative.
+
+name = "swap-pair"
+modulus = "21888242871839275222246405745257275088548364400416034343698204186575808495617"
+soundness_spec = "(b = 0 ∧ out1 = in1 ∧ out2 = in2) ∨ (b = 1 ∧ out1 = in2 ∧ out2 = in1)"
+
+[[witnesses]]
+id = 0
+name = "b"
+
+[[witnesses]]
+id = 1
+name = "in1"
+
+[[witnesses]]
+id = 2
+name = "in2"
+
+[[witnesses]]
+id = 3
+name = "out1"
+
+[[witnesses]]
+id = 4
+name = "out2"
+
+# b^2 - b = 0
+[[constraints]]
+label = "boolean"
+terms = [
+    { coeff = "1", vars = [0, 0] },
+    { coeff = "-1", vars = [0] },
+]
+
+# out1 - in1 + b*in1 - b*in2 = 0   (the out2 mux constraint is DELIBERATELY OMITTED)
+[[constraints]]
+label = "mux1"
+terms = [
+    { coeff = "1", vars = [3] },
+    { coeff = "-1", vars = [1] },
+    { coeff = "1", vars = [0, 1] },
+    { coeff = "-1", vars = [0, 2] },
+]

benchmark/suite/20-neg-wrong-inverse-constraint.toml

@@ -0,0 +1,34 @@
+# NEGATIVE GADGET — a one-term typo in the constraint. The proof loop MUST fail.
+#
+# The real nonzero-check constrains  x * x_inv - 1 = 0  (x has an inverse).
+# This one constrains  x * x_inv - x_inv = 0, i.e. x_inv * (x - 1) = 0 — the
+# constant 1 replaced by x_inv, as a plausible copy/paste or wiring typo.
+# The constraint is now satisfied by x_inv = 0 regardless of x, so it proves
+# nothing about x. Wrong-constant typos are a distinct bug class from missing
+# constraints: the constraint COUNT is right, the polynomial is wrong.
+#
+# Counterexample (kernel-checked at p = 5): x = 0, x_inv = 0 satisfies the
+# constraint (0 - 0 = 0) but violates the spec x ≠ 0.
+#
+# The gadget `name` is deliberately NEUTRAL (it becomes the theorem name the
+# model sees); only this manifest-side file marks it negative.
+
+name = "inverse-gate"
+modulus = "21888242871839275222246405745257275088548364400416034343698204186575808495617"
+soundness_spec = "x ≠ 0"
+
+[[witnesses]]
+id = 0
+name = "x"
+
+[[witnesses]]
+id = 1
+name = "x_inv"
+
+# x * x_inv - x_inv = 0   (should be x * x_inv - 1 = 0; the typo is the bug)
+[[constraints]]
+label = "inverse"
+terms = [
+    { coeff = "1", vars = [0, 1] },
+    { coeff = "-1", vars = [1] },
+]