From 2ebabac2a2baa423d7d95736c36e3c2a33e6f4e0 Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Sat, 18 Jul 2026 18:57:54 +0400 Subject: [PATCH] =?UTF-8?q?feat:=20scribe=20refute=20=E2=80=94=20the=20adv?= =?UTF-8?q?ersarial=20refuter=20(verdict=20engine=20C4)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 : 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. --- .gitignore | 6 +- Cargo.lock | 2 + README.md | 15 +- crates/lean-emit/src/lib.rs | 198 +++++++++++++++++++++++++++ crates/scribe-cli/Cargo.toml | 2 + crates/scribe-cli/src/main.rs | 106 ++++++++++++++ crates/scribe-cli/src/orchestrate.rs | 126 ++++++++++++++++- lean/ZkGadgets/Audit.lean | 6 +- prompts/lean-refuter.md | 56 ++++++++ 9 files changed, 509 insertions(+), 8 deletions(-) create mode 100644 prompts/lean-refuter.md diff --git a/.gitignore b/.gitignore index 0939910..e663e8b 100644 --- a/.gitignore +++ b/.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) diff --git a/Cargo.lock b/Cargo.lock index a7d7448..c6c3436 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -489,7 +489,9 @@ name = "scribe-cli" version = "0.1.0" dependencies = [ "clap", + "gadget-ir", "halva-bridge", + "lean-emit", "proof-pilot", ] diff --git a/README.md b/README.md index 9289755..6dbed50 100644 --- a/README.md +++ b/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. diff --git a/crates/lean-emit/src/lib.rs b/crates/lean-emit/src/lib.rs index 59c95d1..2d052f7 100644 --- a/crates/lean-emit/src/lib.rs +++ b/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 { 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::() { + 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 = 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 _refuted : +/// ¬ (∀ (vars : ZMod ), 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 { + 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 = diff --git a/crates/scribe-cli/Cargo.toml b/crates/scribe-cli/Cargo.toml index 0c6646e..f05a83d 100644 --- a/crates/scribe-cli/Cargo.toml +++ b/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" } diff --git a/crates/scribe-cli/src/main.rs b/crates/scribe-cli/src/main.rs index 99ebc96..ffb3dde 100644 --- a/crates/scribe-cli/src/main.rs +++ b/crates/scribe-cli/src/main.rs @@ -48,6 +48,19 @@ enum Commands { /// --circuit` expects: a Cargo project whose `cargo run --release` prints /// Halva Lean output to stdout. Init(init_cmd::InitArgs), + + /// Adversarially attack a gadget's spec: hunt for a kernel-checked + /// counterexample (verdict engine C4). + /// + /// Emits the soundness statement at a concrete small prime, NEGATED, and + /// runs an LLM refuter loop that tries to prove the negation — i.e. exhibit + /// witness values satisfying every constraint while violating the spec. + /// + /// Exit codes: 2 = REFUTED (a kernel-checked counterexample exists — the + /// circuit is under-constrained or the spec is wrong); 0 = SURVIVED (no + /// refutation found within the budget; evidence, not proof, of soundness); + /// 1 = infrastructure error. + Refute(refute_cmd::RefuteArgs), } mod verify_cmd { @@ -240,6 +253,64 @@ mod init_cmd { } } +mod refute_cmd { + use clap::Args; + + #[derive(Args)] + pub struct RefuteArgs { + /// Gadget IR file (TOML) whose soundness spec should be attacked. + #[arg(long, value_name = "FILE")] + pub gadget: String, + + /// Probe prime for the finite model. Default: the smallest prime + /// satisfying every `p > N` hypothesis the gadget declares (floor 5). + #[arg(long, value_name = "P")] + pub prime: Option, + + /// Output path for the refutation scaffold + /// (default: `/ZkGadgets/Bench/Refute.lean`). + #[arg(short = 'o', long, value_name = "FILE")] + pub output: Option, + + /// Write the scaffold and stop; skip the refuter loop. + #[arg(long)] + pub scaffold_only: bool, + + /// Lake project directory (default: $LAKE_DIR env var, else `lean`). + #[arg(long, value_name = "DIR")] + pub lake_dir: Option, + + /// Maximum refutation attempts (default: 6). + #[arg(long, value_name = "N", default_value = "6")] + pub max_iters: u32, + + /// LLM backend to use (default: claude). See `scribe verify --help`. + #[arg(long, value_name = "NAME", default_value = "claude")] + pub backend: String, + + /// Model name override. + #[arg(long, value_name = "MODEL")] + pub model: Option, + + /// API key for the selected backend. + #[arg(long, value_name = "KEY")] + pub api_key: Option, + + /// API base URL override. + #[arg(long, value_name = "URL")] + pub base_url: Option, + + /// System prompt file (default: $SCRIBE_PROMPTS_DIR/lean-refuter.md, + /// else `prompts/lean-refuter.md`). + #[arg(long, value_name = "FILE")] + pub system_prompt: Option, + + /// Transcript log file path (optional). + #[arg(long, value_name = "FILE")] + pub transcript: Option, + } +} + fn main() { let cli = Cli::parse(); @@ -257,6 +328,9 @@ fn main() { Commands::Init(args) => { init::run_init(args); } + Commands::Refute(args) => { + orchestrate::run_refute(args); + } } } @@ -399,6 +473,38 @@ mod tests { } } + #[test] + fn refute_args_parse_with_defaults() { + let cli = Cli::try_parse_from(["scribe", "refute", "--gadget", "g.toml"]) + .expect("should parse"); + if let Commands::Refute(args) = cli.command { + assert_eq!(args.gadget, "g.toml"); + assert_eq!(args.prime, None); // auto-picked from `p > N` hypotheses + assert_eq!(args.max_iters, 6); + assert!(!args.scaffold_only); + assert_eq!(args.backend, "claude"); + } else { + panic!("expected Refute"); + } + + let cli = Cli::try_parse_from([ + "scribe", + "refute", + "--gadget", + "g.toml", + "--prime", + "257", + "--scaffold-only", + ]) + .expect("should parse"); + if let Commands::Refute(args) = cli.command { + assert_eq!(args.prime, Some(257)); + assert!(args.scaffold_only); + } else { + panic!("expected Refute"); + } + } + #[test] fn verify_audit_gate_defaults_on_and_can_be_disabled() { let cli = Cli::try_parse_from([ diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs index 2f763c5..ab4b4fa 100644 --- a/crates/scribe-cli/src/orchestrate.rs +++ b/crates/scribe-cli/src/orchestrate.rs @@ -1,4 +1,4 @@ -//! Orchestration logic for `scribe verify` and `scribe demo`. +//! Orchestration logic for `scribe verify`, `scribe demo`, and `scribe refute`. use std::fs; use std::path::Path; @@ -13,11 +13,13 @@ use proof_pilot::transcript; use crate::demo_cmd::DemoArgs; use crate::extract; +use crate::refute_cmd::RefuteArgs; use crate::verify_cmd::VerifyArgs; // ── Default paths / environment ────────────────────────────────────────────── const FALLBACK_SYSTEM_PROMPT: &str = "prompts/lean-prover.md"; +const REFUTER_PROMPT_FILE: &str = "lean-refuter.md"; /// Resolve the system prompt path: /// 1. Explicit `--system-prompt ` flag. @@ -27,23 +29,42 @@ fn resolve_system_prompt(explicit: Option<&str>) -> Option { resolve_system_prompt_from(explicit, std::env::var("SCRIBE_PROMPTS_DIR").ok()) } +/// Same precedence for the adversarial refuter prompt (`lean-refuter.md`). +fn resolve_refuter_prompt(explicit: Option<&str>) -> Option { + resolve_prompt_from( + explicit, + std::env::var("SCRIBE_PROMPTS_DIR").ok(), + REFUTER_PROMPT_FILE, + "prompts/lean-refuter.md", + ) +} + /// Pure resolution split out of `resolve_system_prompt` so it can be unit /// tested without mutating the process environment (which races under the /// parallel test runner). fn resolve_system_prompt_from( explicit: Option<&str>, prompts_dir: Option, +) -> Option { + resolve_prompt_from(explicit, prompts_dir, "lean-prover.md", FALLBACK_SYSTEM_PROMPT) +} + +fn resolve_prompt_from( + explicit: Option<&str>, + prompts_dir: Option, + filename: &str, + fallback: &str, ) -> Option { if let Some(path) = explicit { return Some(path.to_string()); } if let Some(dir) = prompts_dir { - let path = format!("{dir}/lean-prover.md"); + let path = format!("{dir}/{filename}"); if Path::new(&path).exists() { return Some(path); } } - Some(FALLBACK_SYSTEM_PROMPT.to_string()) + Some(fallback.to_string()) } /// Resolve the lake dir: explicit `--lake-dir` → `$LAKE_DIR` → `lean`. @@ -282,6 +303,105 @@ const DEMO_STAGE_LABELS: [&str; 4] = [ "Stage 4: kernel-checked proof", ]; +// ── scribe refute ──────────────────────────────────────────────────────────── + +/// Verdict engine C4: adversarially attack a gadget's spec. Emits the negated +/// soundness statement at a concrete small prime and runs an LLM loop that +/// hunts for a kernel-checked counterexample. +/// +/// Exit codes: 2 = REFUTED (counterexample found — that is the alarm), +/// 0 = SURVIVED (budget exhausted without one), 1 = infrastructure error. +pub fn run_refute(args: RefuteArgs) { + let gadget = gadget_ir::load_gadget_file(Path::new(&args.gadget)).unwrap_or_else(|e| { + eprintln!("error: cannot load gadget {}: {e}", args.gadget); + process::exit(1); + }); + + let prime = args + .prime + .unwrap_or_else(|| lean_emit::refutation_prime(&gadget, 5)); + let scaffold = lean_emit::emit_refutation(&gadget, prime).unwrap_or_else(|e| { + eprintln!("error: cannot emit refutation scaffold: {e}"); + process::exit(1); + }); + + let lake_dir = resolve_lake_dir(args.lake_dir.as_deref()); + let out_path = args.output.clone().unwrap_or_else(|| { + let sanitized: String = gadget + .name + .chars() + .map(|c| if c.is_ascii_alphanumeric() { c } else { '_' }) + .collect(); + format!("{lake_dir}/ZkGadgets/Bench/Refute{sanitized}.lean") + }); + if let Some(parent) = Path::new(&out_path).parent() { + let _ = fs::create_dir_all(parent); + } + fs::write(&out_path, &scaffold).unwrap_or_else(|e| { + eprintln!("error: cannot write {out_path}: {e}"); + process::exit(1); + }); + eprintln!("[scribe] refutation target written: {out_path} (p = {prime})"); + + if args.scaffold_only { + println!("SCAFFOLD: {out_path}"); + return; + } + + let system_prompt_path = resolve_refuter_prompt(args.system_prompt.as_deref()); + let system_prompt = system_prompt_path.map(|path| { + fs::read_to_string(&path).unwrap_or_else(|e| { + eprintln!("error: cannot read system prompt {path}: {e}"); + process::exit(1); + }) + }); + + let backend = make_backend( + &args.backend, + args.model.clone(), + args.api_key.clone(), + args.base_url.clone(), + ); + eprintln!("[scribe] refuter backend: {}", backend.name()); + + let config = SessionConfig { + lean_file: out_path.clone(), + lake_dir, + max_iterations: args.max_iters, + system_prompt, + transcript: args.transcript.clone(), + use_lsp: false, + }; + + let (result, _journal) = session::run(&config, backend.as_ref()); + + match result { + SessionResult::Proven { iterations } => { + eprintln!( + "[scribe] ⚠ REFUTED in {iterations} iteration(s): a kernel-checked \ + counterexample exists at p = {prime}" + ); + eprintln!( + "[scribe] the circuit is under-constrained (or the spec is wrong); \ + the counterexample is in the proof of {out_path}" + ); + println!("REFUTED: {out_path}"); + process::exit(2); + } + SessionResult::Exhausted { iterations, .. } => { + eprintln!( + "[scribe] SURVIVED: no refutation found in {iterations} iteration(s) \ + at p = {prime} (evidence, not proof, of soundness)" + ); + println!("SURVIVED: {}", args.gadget); + } + SessionResult::Failed(msg) => { + eprintln!("[scribe] fatal error: {msg}"); + process::exit(1); + } + } +} + pub fn run_demo(args: DemoArgs) { let lake_dir = resolve_lake_dir(args.lake_dir.as_deref()); diff --git a/lean/ZkGadgets/Audit.lean b/lean/ZkGadgets/Audit.lean index 35c27a0..adff373 100644 --- a/lean/ZkGadgets/Audit.lean +++ b/lean/ZkGadgets/Audit.lean @@ -47,8 +47,10 @@ its conclusion can fail, and its side-conditions are load-bearing. The probes ar derived from the signature, so a spec that drifts back toward vacuity turns the build red. Scope: probes need decidable, enumerable instantiations — flat `ZMod p` gadget statements qualify; Halva circuit-level theorems (function-typed circuits) -keep hand-written witnesses instead. The adversarial LLM refuter (C4) remains -future work. +keep hand-written witnesses instead. The adversarial LLM refuter (C4) lives on +the Rust side as `scribe refute`: it emits the *negated* soundness statement at +a concrete prime and runs an LLM loop hunting for a kernel-checked +counterexample — the dynamic complement to these static probes. -/ open Lean Elab Command Meta diff --git a/prompts/lean-refuter.md b/prompts/lean-refuter.md new file mode 100644 index 0000000..2fb34fa --- /dev/null +++ b/prompts/lean-refuter.md @@ -0,0 +1,56 @@ +# Lean 4 Adversarial Refuter + +You are an adversarial circuit auditor. The file contains a theorem of the form + +``` +theorem _refuted : + ¬ (∀ (vars : ZMod

), hyp₁ → ... → constraintₖ = 0 → spec) := by + sorry +``` + +A kernel-accepted proof of this theorem is a **concrete counterexample**: witness +values over the small prime field `ZMod P` that satisfy every constraint while +violating the spec. Finding one means the circuit is under-constrained (or the +spec is wrong) — this is the bug class ZK audits exist to catch. + +## How to refute + +Think like a prover attacking a circuit: which wire is not pinned down? A missing +constraint, a dangling output, a constraint satisfied by a degenerate assignment +(zeros are a great first guess for inverse-style constraints). + +The canonical proof shape — introduce the universal, specialize it at your +counterexample, discharge the antecedents by `decide`, then let `decide` explode +the violated spec: + +```lean +intro h +have := h v₁ v₂ ... (by decide) (by decide) +revert this +decide +``` + +For a spec of the form `x ≠ 0`, specializing at `x = 0` gives a direct hit: + +```lean +exact fun h => h 0 0 (by decide) rfl +``` + +Work over the concrete prime in the statement — all arithmetic is decidable, so +`decide` closes every numeric side goal. If a `decide` times out, prefer smaller +witness values. + +## Hard rules + +- Do NOT change the theorem statement. Only replace the proof body after `:= by`. +- `sorry`, `admit`, `axiom`, and `native_decide` are forbidden and rejected. +- **Never fabricate.** If your candidate values do not check out, try different + ones. If the statement appears to be true (the constraints really do force the + spec), say so in plain text WITHOUT a code block — do not submit a proof + attempt you know is wrong. Failing honestly is the correct outcome for a sound + circuit: your refutation attempts are only meaningful because you refuse to + force them. + +Reply with a single fenced code block containing the proof body (optionally +preceded by `import` lines), or plain text explaining why no counterexample +exists if you believe the statement is true.