scribe refute: the adversarial refuter (verdict engine C4) - #15
scribe refute: the adversarial refuter (verdict engine C4)#15LucidSamuel wants to merge 1 commit into
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".
| let prime = args | ||
| .prime | ||
| .unwrap_or_else(|| lean_emit::refutation_prime(&gadget, 5)); |
There was a problem hiding this comment.
When --prime is supplied, this bypasses the auto-selected bounded prime entirely. For a gadget with hp : p > 256, running scribe refute --prime 5 emits an antecedent 5 > 256 →, making the statement vacuously true and causing an under-constrained gadget to incorrectly SURVIVE; similarly a composite value would test ZMod n outside the original prime-field theorem. Please reject explicit primes that are composite or fail the gadget's declared p > N bounds before calling emit_refutation.
Useful? React with 👍 / 👎.
1 participant
Stacked on #14 (uses the new negative gadgets as its validation corpus; merge #14 first, then retarget or merge this into main).
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.