From bd721b015b12c560bd1c168584cf9dd7b71d147b Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Sat, 18 Jul 2026 18:40:39 +0400 Subject: [PATCH] feat: grow the negative corpus to five audit-bug classes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three new negative gadgets (suite 18-20), each mirroring a distinct real-world under-constraint class rather than repeating 'missing boolean constraint': - zero-indicator: is-zero missing its x*out = 0 half — a nonzero x claims out = 1 via inv = 0 (the classic production isZero bug) - swap-pair: swap gate with the out2 mux constraint dropped — a dangling output wire - inverse-gate: x*inv - inv = 0 instead of x*inv - 1 = 0 — a one-term typo; right constraint count, wrong polynomial All specs are kernel-checked FALSE (concrete counterexamples verified against the exact lean-emit-emitted statements at p = 5, documented in each TOML) — these are refutable theorems, not merely hard ones. Names stay neutral: the model sees nothing marking them as traps; kind = "negative" lives only in the manifest. Suite is now 15 positives + 5 negatives. --- README.md | 4 +- benchmark/suite.toml | 21 +++++++ .../18-neg-is-zero-missing-constraint.toml | 39 +++++++++++++ .../19-neg-swap-unconstrained-output.toml | 56 +++++++++++++++++++ .../20-neg-wrong-inverse-constraint.toml | 34 +++++++++++ 5 files changed, 152 insertions(+), 2 deletions(-) create mode 100644 benchmark/suite/18-neg-is-zero-missing-constraint.toml create mode 100644 benchmark/suite/19-neg-swap-unconstrained-output.toml create mode 100644 benchmark/suite/20-neg-wrong-inverse-constraint.toml diff --git a/README.md b/README.md index ad20df3..9289755 100644 --- a/README.md +++ b/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. diff --git a/benchmark/suite.toml b/benchmark/suite.toml index 3010204..60c534b 100644 --- a/benchmark/suite.toml +++ b/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" diff --git a/benchmark/suite/18-neg-is-zero-missing-constraint.toml b/benchmark/suite/18-neg-is-zero-missing-constraint.toml new file mode 100644 index 0000000..1f2c687 --- /dev/null +++ b/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 = [] }, +] diff --git a/benchmark/suite/19-neg-swap-unconstrained-output.toml b/benchmark/suite/19-neg-swap-unconstrained-output.toml new file mode 100644 index 0000000..1a9f24d --- /dev/null +++ b/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] }, +] diff --git a/benchmark/suite/20-neg-wrong-inverse-constraint.toml b/benchmark/suite/20-neg-wrong-inverse-constraint.toml new file mode 100644 index 0000000..474e649 --- /dev/null +++ b/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] }, +]