Grow the negative corpus to five audit-bug classes#14
Conversation
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.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bd721b015b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| ## 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: |
There was a problem hiding this comment.
Because this line now describes the default benchmark as a 20-gadget suite, the unchanged “Results so far” paragraph below reads as if it covers the expanded corpus. Those numbers are from the old suite: benchmark/RESULTS.md documents 15 positives + 2 negatives, and the reported 16/16 refusals matches 2 negatives × 2 modes × (1+3 samples), not the 5-negative suite, which would have 40 negative sessions. Until the suite is rerun or the paragraph is labeled pre-expansion, readers will misinterpret refusal coverage for the new negative classes.
Useful? React with 👍 / 👎.
| [[gadgets]] | ||
| file = "suite/18-neg-is-zero-missing-constraint.toml" |
There was a problem hiding this comment.
Adding new benchmark cases here changes the corpus while version remains 0.2.0, and the runner serializes only that manifest version as suite_version in result JSON. That makes old 17-gadget result files and new 20-gadget result files look like the same suite version, which can corrupt pass/refusal comparisons and cached benchmark provenance; please bump the suite version along with the added cases.
Useful? React with 👍 / 👎.
1 participant
Three new negative gadgets (suite 18–20), each a distinct real-world under-constraint class:
zero-indicatorx·out = 0halfswap-pairinverse-gatex·inv − invforx·inv − 1Every spec is verified false against the exact
lean-emit-emitted theorem statement at p = 5 (refutations kernel-checked before landing; witnesses documented in each TOML) — refutable theorems, not merely hard ones. Names stay neutral;kind = "negative"lives only in the manifest. Suite is now 15 positives + 5 negatives; README updated.Next suite run will grade the loop on refusing all five.