scribe refute: the adversarial refuter (verdict engine C4)#16
Conversation
The dual side of the proof loop: instead of proving a spec, attack it. - lean-emit::emit_refutation: the gadget's soundness statement at a concrete small prime, NEGATED, with sorry + #audit_axioms gate. refutation_prime picks the smallest prime satisfying the gadget's p > N hypotheses; substitute_p concretizes p in specs, hypotheses, and constraint casts. - scribe refute --gadget <toml>: emits the target and runs proof-pilot with a dedicated adversarial prompt (prompts/lean-refuter.md). A kernel-accepted proof of the negation IS a concrete counterexample — witness values satisfying every constraint while violating the spec. Verdicts: REFUTED (exit 2, the alarm) / SURVIVED (exit 0, evidence not proof) / infrastructure error (exit 1). - The refuter prompt teaches the specialize-and-decide proof shape and the honest-refusal rule: no code block when the statement looks true. Live validation (claude-sonnet-5): all three new negative gadgets REFUTED in 1 iteration each — for zero-indicator the model found exactly the documented counterexample (x = 1, inv = 0, out = 1) — and the true boolean-check spec SURVIVED with the model declining to emit any proof attempt in all 3 iterations. Exit codes verified 2/2/2/0. C4 closes the verdict-engine roadmap from the July review: C1-C3 probe statements statically at build time; C4 attacks them dynamically with the same kernel arbitration as the prover.
![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: 2ebabac2a2
ℹ️ 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".
| if let Some(rest) = t.strip_prefix("p").map(str::trim_start) { | ||
| if let Some(bound) = rest.strip_prefix('>').map(str::trim) { | ||
| if let Ok(n) = bound.parse::<u64>() { |
There was a problem hiding this comment.
When a gadget writes a normal Lean hypothesis like lean_type = "(p > 256)", this parser misses the bound because it only accepts strings starting exactly with p. The auto-selected prime stays at the floor (5), and emit_refutation then substitutes the hypothesis into the theorem as (5 > 256) →, making the universal statement vacuously true so underconstrained gadgets can incorrectly report SURVIVED. Please normalize/parse parenthesized bound forms or reject unrecognized p bounds before choosing the probe prime.
Useful? React with 👍 / 👎.
| let prime = args | ||
| .prime | ||
| .unwrap_or_else(|| lean_emit::refutation_prime(&gadget, 5)); |
There was a problem hiding this comment.
When --prime is supplied, the value bypasses refutation_prime and is emitted without checking that it is prime or satisfies the gadget's p > N hypotheses. For example, --prime 5 on a gadget with hp : p > 256 generates a false antecedent and can make an unsafe circuit SURVIVED; a composite value can also produce a REFUTED result from ZMod P even though the original theorem is only over prime fields. Please validate the supplied prime against the same conditions before emitting the scaffold.
Useful? React with 👍 / 👎.
1 participant
Replaces #15 (auto-closed when its stacked base branch was deleted on the #14 merge; same commit).
The dual side of the proof loop — instead of proving a spec, attack it:
scribe refute --gadget benchmark/suite/18-neg-is-zero-missing-constraint.toml # ⚠ REFUTED in 1 iteration(s): a kernel-checked counterexample exists at p = 5 (exit 2)lean-emit::emit_refutationemits the soundness statement at a concrete small prime, negated, withsorry+#audit_axiomsgate.refutation_primeauto-picks the smallest prime satisfying the gadget'sp > Nbounds;substitute_pconcretizespeverywhere (identifier-aware).scribe refuteruns proof-pilot on it with a dedicated adversarial prompt (prompts/lean-refuter.md): specialize-and-decideproof shape plus an honest-refusal rule — no code block when the statement looks true. A kernel-accepted refutation is exactly as trustworthy as a kernel-accepted proof.Live validation (claude-sonnet-5): all three #14 negatives REFUTED in 1 iteration each — for
zero-indicatorthe model found exactly the counterexample documented in the TOML (x = 1, inv = 0, out = 1) — and the trueboolean-checkspec SURVIVED, with the model declining to emit any proof attempt in all 3 iterations. Exit codes verified 2/2/2/0.This closes the verdict engine from the July review: C1–C3 probe statements statically at build time, C4 attacks them dynamically, and both sides answer to the same kernel. 22 new/updated Rust tests; clippy clean; README + Audit.lean docs updated.