scribe refute: the adversarial refuter (verdict engine C4)

.gitignore

@@ -20,10 +20,12 @@ benchmark/results/
 
 # Claude Code (local config, commands, prompts)
 .claude/
-# Ignore local prompt scratch files, but keep the project's system prompt —
-# proof-pilot / scribe-cli and the Docker image depend on prompts/lean-prover.md.
+# Ignore local prompt scratch files, but keep the project's system prompts —
+# proof-pilot / scribe-cli and the Docker image depend on lean-prover.md, and
+# `scribe refute` on lean-refuter.md.
 prompts/*
 !prompts/lean-prover.md
+!prompts/lean-refuter.md
 NOTES.md
 
 # MCP config (local dev)

README.md

@@ -37,7 +37,7 @@ Zero-knowledge circuits are notoriously hard to get right: a single under-constr
 Three properties make this trustworthy:
 
 - **Sound by construction.** Every proof in this repo is checked by the Lean 4 kernel, and an `#audit_axioms` gate next to each theorem runs the engine behind `#print axioms` at build time, rejecting anything that depends on more than the three standard axioms. That catches a transitive `sorryAx` (what `sorry`/`admit` elaborate to) or `native_decide`'s `ofReduceBool` reached through any dependency — which a textual grep cannot. See [`Audit.lean`](lean/ZkGadgets/Audit.lean).
-- **Specs audited, not just proofs.** A kernel-checked proof of a meaningless statement proves nothing, so a dual-sided **verdict engine** probes the statements themselves at build time: `#audit_uses` / `#audit_requires` (C1) fail the build on decorative or dropped hypotheses; `#audit_falsifiable` (C2) requires a kernel-checked refutation of the conclusion at a finite-model instantiation, killing vacuously-true specs; `#audit_satisfiable` (C3) requires a witness satisfying every constraint, killing impossible-antecedent specs. A theorem passing C1–C3 has demonstrated content: its constraints can hold, its conclusion can fail, and its side-conditions are load-bearing. (C4, an adversarial LLM refuter, is roadmap.)
+- **Specs audited, not just proofs.** A kernel-checked proof of a meaningless statement proves nothing, so a dual-sided **verdict engine** probes the statements themselves at build time: `#audit_uses` / `#audit_requires` (C1) fail the build on decorative or dropped hypotheses; `#audit_falsifiable` (C2) requires a kernel-checked refutation of the conclusion at a finite-model instantiation, killing vacuously-true specs; `#audit_satisfiable` (C3) requires a witness satisfying every constraint, killing impossible-antecedent specs. A theorem passing C1–C3 has demonstrated content: its constraints can hold, its conclusion can fail, and its side-conditions are load-bearing. `scribe refute` (C4) completes the dual side: an adversarial LLM loop attacks the spec itself, hunting for a kernel-checked counterexample — so a spec is only trusted after surviving the same class of refutation search that catches under-constrained circuits.
 - **Automated.** An LLM drives a closed feedback loop, edit the proof, compile, read the errors (or structured LSP goal states), repeat until the kernel accepts or the budget runs out.
 - **Real circuits.** The `halva-bridge` consumes actual Halva-style halo2 extraction output and proves soundness against a human-written specification.
 
@@ -124,6 +124,19 @@ Both forms run `proof-pilot` by default and exit `0` only when the Lean kernel a
 > [!NOTE]
 > **Scope.** `scribe verify --circuit` operates on a Halva *extractor project* — you still author the small extractor program that runs against your halo2 circuit. scribe does not read raw halo2 Rust source directly. The chain is: extractor-project output → Lean scaffold → LLM proof loop → kernel-accepted `.lean`.
 
+### `scribe refute`
+
+The adversarial half of the verdict engine (C4): instead of proving the spec, attack it.
+
+```sh
+scribe refute --gadget examples/range-check/gadget.toml \
+  [--prime P]        # default: smallest prime satisfying the gadget's `p > N` bounds
+  [--max-iters N]    # refutation attempts (default: 6)
+  [--scaffold-only]  # emit the negated statement and stop
+```
+
+The gadget's soundness statement is emitted at a concrete small prime, **negated**, and an LLM refuter loop (system prompt `prompts/lean-refuter.md`) tries to prove the negation — i.e. exhibit witness values that satisfy every constraint while violating the spec. A kernel-accepted refutation is exactly as trustworthy as a kernel-accepted proof, and carries its own `#audit_axioms` gate. Exit codes: `2` = **REFUTED** (the circuit is under-constrained or the spec is wrong — the counterexample is in the output file), `0` = **SURVIVED** (no refutation within budget; evidence, not proof), `1` = infrastructure error.
+
 ### `scribe init`
 
 Generates the editable Halva extractor project that `scribe verify --circuit` expects.

crates/lean-emit/src/lib.rs

@@ -8,6 +8,7 @@ pub enum EmitError {
     DuplicateWitnessId(usize),
     UnknownWitnessId { constraint: String, id: usize },
     DuplicateConstraintLabel(String),
+    MissingSpec,
 }
 
 impl std::fmt::Display for EmitError {
@@ -27,6 +28,9 @@ impl std::fmt::Display for EmitError {
             EmitError::DuplicateConstraintLabel(label) => {
                 write!(f, "duplicate generated constraint label: {}", label)
             }
+            EmitError::MissingSpec => {
+                write!(f, "gadget has no soundness_spec — nothing to refute")
+            }
         }
     }
 }
@@ -139,6 +143,141 @@ pub fn emit_lean_decomposed(gadget: &Gadget) -> Result<String, EmitError> {
     Ok(out)
 }
 
+/// Smallest prime strictly greater than or equal to `n` (trial division —
+/// refutation primes are tiny).
+fn next_prime_at_least(n: u64) -> u64 {
+    let mut candidate = n.max(2);
+    loop {
+        let mut is_prime = candidate >= 2;
+        let mut d = 2u64;
+        while d * d <= candidate {
+            if candidate.is_multiple_of(d) {
+                is_prime = false;
+                break;
+            }
+            d += 1;
+        }
+        if is_prime {
+            return candidate;
+        }
+        candidate += 1;
+    }
+}
+
+/// The field size for a refutation probe: the smallest prime satisfying every
+/// `p > N` hypothesis the gadget declares, and at least `min` (a floor like 5
+/// keeps degenerate tiny fields out). A refutation at one valid prime refutes
+/// the generic theorem.
+pub fn refutation_prime(gadget: &Gadget, min: u64) -> u64 {
+    let mut lower = min.max(2);
+    for h in &gadget.hypotheses {
+        let t = h.lean_type.trim();
+        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>() {
+                    lower = lower.max(n + 1);
+                }
+            }
+        }
+    }
+    next_prime_at_least(lower)
+}
+
+/// Replace the standalone identifier `p` in a spec / hypothesis string with a
+/// concrete prime literal (`p > 256` → `257 > 256`; `exp` stays untouched).
+fn substitute_p(s: &str, prime: u64) -> String {
+    let chars: Vec<char> = s.chars().collect();
+    let is_ident = |c: char| c.is_alphanumeric() || c == '_' || c == '\'';
+    let mut out = String::new();
+    for (i, &c) in chars.iter().enumerate() {
+        let standalone_p = c == 'p'
+            && (i == 0 || !is_ident(chars[i - 1]))
+            && (i + 1 == chars.len() || !is_ident(chars[i + 1]));
+        if standalone_p {
+            out.push_str(&prime.to_string());
+        } else {
+            out.push(c);
+        }
+    }
+    out
+}
+
+/// Emit a **refutation scaffold**: the gadget's soundness statement at a concrete
+/// small prime, negated, with a `sorry` body for the adversarial loop to fill.
+///
+/// ```text
+/// theorem <name>_refuted :
+///     ¬ (∀ (vars : ZMod <prime>), hyps → constraints → spec) := by
+///   sorry
+/// ```
+///
+/// A kernel-accepted proof of this theorem is a concrete counterexample: values
+/// satisfying every constraint while violating the spec — the gadget is
+/// under-constrained (or the spec is wrong). Exhausting the budget without one
+/// is evidence, not proof, that the spec survives attack. The `#audit_axioms`
+/// gate holds refutations to the same axiom standard as proofs.
+pub fn emit_refutation(gadget: &Gadget, prime: u64) -> Result<String, EmitError> {
+    let spec = gadget.soundness_spec.as_ref().ok_or(EmitError::MissingSpec)?;
+    let witness_names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect();
+    let witness_by_id = witness_map(gadget)?;
+    let theorem_name = format!("{}_refuted", sanitize_generated_ident(&gadget.name, "gadget"));
+    let constraint_labels = generated_constraint_labels(gadget)?;
+    let _ = constraint_labels; // labels documented in the header; antecedents are positional
+
+    let mut out = String::new();
+
+    // -- imports (same set the prover scaffolds use)
+    out.push_str("import ZkGadgets.Field\n");
+    out.push_str("import ZkGadgets.Audit\n");
+    out.push_str("import Mathlib.Data.ZMod.Basic\n");
+    out.push_str("import Mathlib.Algebra.Field.ZMod\n");
+    out.push_str("import Mathlib.Tactic.Ring\n");
+    out.push_str("import Mathlib.Tactic.LinearCombination\n\n");
+
+    // -- doc comment
+    out.push_str(&format!("/-!\n# {} — refutation target\n\n", gadget.name));
+    out.push_str(
+        "Auto-generated by lean-emit (refutation mode). Do not edit the theorem statement.\n\n",
+    );
+    out.push_str(&format!(
+        "A kernel-accepted proof of this theorem is a concrete counterexample at\n\
+         `p = {prime}`: witness values satisfying every constraint while violating the\n\
+         spec. That refutes the generic soundness statement — the circuit is\n\
+         under-constrained (or the spec is wrong).\n\n"
+    ));
+    out.push_str("Constraints:\n");
+    for c in &gadget.constraints {
+        out.push_str(&format!(
+            "  {} : {} = 0\n",
+            c.label,
+            emit_constraint_expr(c, &witness_by_id)?
+        ));
+    }
+    out.push_str(&format!("\nSpec under attack: {}\n", spec));
+    out.push_str("-/\n\n");
+
+    // -- theorem: the negated universally-quantified statement at the probe prime
+    out.push_str(&format!("theorem {}\n", theorem_name));
+    out.push_str(&format!(
+        "    : ¬ (∀ ({} : ZMod {prime}),\n",
+        witness_names.join(" ")
+    ));
+    for h in &gadget.hypotheses {
+        out.push_str(&format!("        {} →\n", substitute_p(&h.lean_type, prime)));
+    }
+    for c in &gadget.constraints {
+        // constraint expressions can carry `(1 : ZMod p)`-style casts
+        let expr = substitute_p(&emit_constraint_expr(c, &witness_by_id)?, prime);
+        out.push_str(&format!("        {} = 0 →\n", expr));
+    }
+    out.push_str(&format!("        ({})) := by\n  sorry\n", substitute_p(spec, prime)));
+
+    // -- audit gate: a refutation must rest on the trusted kernel axioms too
+    out.push_str(&audit_gate(&theorem_name));
+
+    Ok(out)
+}
+
 /// Render an `#audit_axioms` gate line for a theorem. Placed after the proof so
 /// `lake build` fails on an unproven or axiom-tainted scaffold rather than
 /// merely warning.
@@ -537,6 +676,65 @@ mod tests {
         ));
     }
 
+    #[test]
+    fn refutation_prime_honors_bounds() {
+        let gadget =
+            gadget_ir::load_gadget_file(&examples_dir().join("range-check/gadget.toml")).unwrap();
+        // hp : p > 256 forces the probe past the bound, to the next prime.
+        assert_eq!(refutation_prime(&gadget, 5), 257);
+        let no_hyp =
+            gadget_ir::load_gadget_file(&examples_dir().join("poseidon-sbox/gadget.toml")).unwrap();
+        assert_eq!(refutation_prime(&no_hyp, 5), 5);
+        assert_eq!(refutation_prime(&no_hyp, 6), 7);
+    }
+
+    #[test]
+    fn substitute_p_is_identifier_aware() {
+        assert_eq!(substitute_p("p > 256", 257), "257 > 256");
+        assert_eq!(substitute_p("(1 : ZMod p)", 5), "(1 : ZMod 5)");
+        // `p` inside identifiers must survive.
+        assert_eq!(substitute_p("exp + p_val + x", 5), "exp + p_val + x");
+        assert_eq!(substitute_p("ZMod.val x < 256", 257), "ZMod.val x < 256");
+    }
+
+    #[test]
+    fn emit_refutation_negates_statement_at_concrete_prime() {
+        let gadget =
+            gadget_ir::load_gadget_file(&examples_dir().join("range-check/gadget.toml")).unwrap();
+        let out = emit_refutation(&gadget, 257).unwrap();
+
+        assert!(out.contains("theorem range_check_8bit_refuted"));
+        // negated ∀ at the concrete prime; no generic field variable, no Fact binder
+        assert!(out.contains("¬ (∀ (x b0 b1 b2 b3 b4 b5 b6 b7 : ZMod 257),"));
+        assert!(!out.contains("variable (p"));
+        // the p-bound hypothesis and spec are concretized
+        assert!(out.contains("257 > 256 →"));
+        assert!(out.contains("(ZMod.val x < 256)) := by"));
+        // constraints appear as antecedents
+        assert!(out.contains("b0 * b0 - b0 = 0 →"));
+        // scaffold is red until refuted, and gated
+        assert!(out.contains("sorry"));
+        assert!(out.trim_end().ends_with(
+            "#audit_axioms range_check_8bit_refuted  -- proof must rest only on the trusted kernel axioms"
+        ));
+    }
+
+    #[test]
+    fn emit_refutation_requires_a_spec() {
+        let gadget = Gadget {
+            name: "no-spec".into(),
+            modulus: "7".into(),
+            soundness_spec: None,
+            hypotheses: vec![],
+            witnesses: vec![WitnessVar {
+                id: 0,
+                name: "x".into(),
+            }],
+            constraints: vec![],
+        };
+        assert_eq!(emit_refutation(&gadget, 5), Err(EmitError::MissingSpec));
+    }
+
     #[test]
     fn emit_conditional_select() {
         let gadget =

crates/scribe-cli/Cargo.toml

@@ -11,5 +11,7 @@ path = "src/main.rs"
 
 [dependencies]
 clap = { version = "4", features = ["derive"] }
+gadget-ir = { path = "../gadget-ir" }
 halva-bridge = { path = "../halva-bridge" }
+lean-emit = { path = "../lean-emit" }
 proof-pilot = { path = "../proof-pilot" }