From 31340c5c350ba49681917ba1381cd0df17efede5 Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Tue, 21 Jul 2026 16:06:45 +0400 Subject: [PATCH 1/2] =?UTF-8?q?feat:=20circom/R1CS=20front-end=20=E2=80=94?= =?UTF-8?q?=20scribe=20import-r1cs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New crates/r1cs-front: parses the iden3 .r1cs binary format (magic/version/ sections; header prime, wire counts; sparse A/B/C linear combinations) and the companion .sym signal map, then expands each rank-1 row ⟨A,w⟩·⟨B,w⟩ = ⟨C,w⟩ exactly into gadget-ir's sum-of-products form: - wire 0 (constant 1) contributes to coefficients, never monomials; like monomials merge mod p; zero rows drop - coefficients canonicalize to signed form (p−1 → -1) so the emitted theorem stays generic over the field; circuits whose arithmetic only means something at the exact header prime (wide canonical coefficients, e.g. constant inverses) are REJECTED with guidance rather than mistranslated (v1 scope, --max-coeff-bits) - .sym names sanitize to Lean binders (main.in[0] → in_0), including the Lean keyword collision that bites in practice: circom's ubiquitous 'in' → 'in_' - build_r1cs_bytes is public so tests and fixtures need no circom install; examples/gen_fixtures.rs generates a correct Num2Bits(2) and the classic circomlib IsZero missing-constraint bug at the real BN254 prime scribe import-r1cs --r1cs f.r1cs --sym f.sym --spec '...' emits reviewable gadget TOML (constraints machine-derived; the spec stays the human trust root — R1CS carries constraints, never intent). The whole existing pipeline consumes it unchanged. Live proof of life: imported the buggy IsZero fixture and ran scribe judge — prove phase correctly exhausted, refuter found the kernel-checked textbook counterexample (in = 1, inv = 0, out = 1) at iteration 1 → UNSOUND, exit 2. The first R1CS-format circuit judged end-to-end. README: front-ends reframed (TOML = reviewable fixture format; circuits enter via r1cs-front or halva-bridge), import-r1cs section with the circom → import → judge flow. 8 new parser/conversion tests; workspace green; clippy clean. --- Cargo.lock | 45 ++ Cargo.toml | 1 + README.md | 35 +- crates/r1cs-front/Cargo.toml | 11 + crates/r1cs-front/examples/gen_fixtures.rs | 76 +++ crates/r1cs-front/src/lib.rs | 719 +++++++++++++++++++++ crates/scribe-cli/Cargo.toml | 2 + crates/scribe-cli/src/main.rs | 56 ++ crates/scribe-cli/src/orchestrate.rs | 99 +++ 9 files changed, 1034 insertions(+), 10 deletions(-) create mode 100644 crates/r1cs-front/Cargo.toml create mode 100644 crates/r1cs-front/examples/gen_fixtures.rs create mode 100644 crates/r1cs-front/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index c6c3436..549a21d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -58,6 +58,12 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "autocfg" +version = "1.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" + [[package]] name = "base64" version = "0.22.1" @@ -381,6 +387,34 @@ dependencies = [ "simd-adler32", ] +[[package]] +name = "num-bigint" +version = "0.4.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c89e69e7e0f03bea5ef08013795c25018e101932225a656383bd384495ecc367" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + [[package]] name = "once_cell" version = "1.21.4" @@ -435,6 +469,15 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "r1cs-front" +version = "0.1.0" +dependencies = [ + "gadget-ir", + "num-bigint", + "num-traits", +] + [[package]] name = "ring" version = "0.17.14" @@ -493,6 +536,8 @@ dependencies = [ "halva-bridge", "lean-emit", "proof-pilot", + "r1cs-front", + "toml", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 82abae6..1cafcde 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,6 +6,7 @@ members = [ "crates/proof-pilot", "crates/bench", "crates/halva-bridge", + "crates/r1cs-front", "crates/scribe-cli", ] diff --git a/README.md b/README.md index f19da5b..e93fa60 100644 --- a/README.md +++ b/README.md @@ -45,11 +45,12 @@ Three properties make this trustworthy: scribe is a small Rust workspace. The pipeline runs IR → Lean scaffold → LLM proof loop → kernel-accepted `.lean`: -1. **`gadget-ir`**: a minimal IR for polynomial constraints over a prime field (TOML → struct). -2. **`lean-emit`**: reads the IR and emits a Lean 4 file with the theorem statement and a `sorry`. -3. **`proof-pilot`**: drives an LLM backend in a loop: edit the proof → compile the target file → read the errors → repeat. Stops when the kernel accepts or the budget is exhausted. -4. **`halva-bridge`**: combines a Halva halo2 extraction with a user specification and (optionally) sends the resulting theorem to `proof-pilot`. -5. **`scribe-cli`**: the top-level `scribe` binary, with `verify`, `init`, and `demo` subcommands. +1. **`gadget-ir`**: the internal IR for polynomial constraints over a prime field. TOML is its *fixture format* — hand-authorable and PR-reviewable (which is what makes the negative gadgets auditable); real circuits enter through the front-ends below. +2. **`r1cs-front`**: the circom front-end — parses `.r1cs` binaries (+ `.sym` signal names) and expands each rank-1 row into the IR (`scribe import-r1cs`). +3. **`halva-bridge`**: the halo2 front-end — combines a Halva extraction with a user specification and (optionally) sends the resulting theorem to `proof-pilot`. +4. **`lean-emit`**: reads the IR and emits a Lean 4 file with the theorem statement (or its negation, for refutation) and a `sorry`. +5. **`proof-pilot`**: drives an LLM backend in a loop: edit the proof → compile the target file → read the errors → repeat. Stops when the kernel accepts or the budget is exhausted. +6. **`scribe-cli`**: the top-level `scribe` binary: `verify`, `refute`, `judge`, `import-r1cs`, `init`, `demo`. ## Getting Started @@ -159,6 +160,19 @@ The exit codes are stable and documented so third parties can script `scribe jud **Best-of-n sampling.** `--samples-per-iter K` (also on `verify`, `refute`, and `proof-pilot`) fires K attempts per iteration and lets the kernel filter: candidates are deduplicated, tried shortest-first, and the first to build wins. Parallel sampling is soundness-free — a wrong candidate costs a build, never a false acceptance — and the transcript records every candidate plus the acceptance index, so `--replay` determinism is preserved. +### `scribe import-r1cs` + +The circom front-end: from a compiled circuit to a judged verdict. + +```sh +circom mycircuit.circom --r1cs --sym # (any existing circom toolchain) +scribe import-r1cs --r1cs mycircuit.r1cs --sym mycircuit.sym \ + --spec "ZMod.val in_ < 4" -o mycircuit.gadget.toml +scribe judge --gadget mycircuit.gadget.toml # SOUND / UNSOUND / UNDETERMINED +``` + +Each rank-1 row `⟨A,w⟩·⟨B,w⟩ = ⟨C,w⟩` is expanded exactly into the sum-of-products IR; coefficients are canonicalized to signed form (`p − 1` → `-1`); signal names come from the `.sym` map (sanitized for Lean — `main.in` becomes `in_`). The emitted TOML is the reviewable artifact: the constraints are machine-derived, but the `soundness_spec` is the **human trust root** — R1CS carries constraints, never intent. Scope (v1): circuits whose canonicalized coefficients are small (bit-decomposition, boolean, mux — i.e. most of circomlib's core); circuits whose arithmetic only means something at the exact BN254 prime (inverses as constants) are rejected with a clear error rather than mistranslated. + ### `scribe init` Generates the editable Halva extractor project that `scribe verify --circuit` expects. @@ -290,11 +304,12 @@ Tags: `latest` (main branch), `sha-` (per-commit), `v` (releases ``` crates/ - gadget-ir/ constraint system IR + TOML deserialization - lean-emit/ IR → Lean 4 scaffold with sorry - proof-pilot/ LLM proof loop (patcher, lean runner, session logging, transcript, replay) - halva-bridge/ Halva extraction + semantic specification bridge - scribe-cli/ top-level `scribe` binary (verify + init + demo) + gadget-ir/ constraint system IR (TOML fixtures) + r1cs-front/ circom front-end: .r1cs/.sym → gadget IR + lean-emit/ IR → Lean 4 scaffold with sorry (prover + refutation modes) + proof-pilot/ LLM proof loop (patcher, lean runner, best-of-n, transcript, replay) + halva-bridge/ halo2 front-end: Halva extraction + semantic specification bridge + scribe-cli/ top-level `scribe` binary (verify, refute, judge, import-r1cs, init, demo) bench/ ZKGadgetEval benchmark suite lean/ZkGadgets/ the proven theorems (Field + 8 gadgets) examples/ IR / extraction + spec inputs for every gadget diff --git a/crates/r1cs-front/Cargo.toml b/crates/r1cs-front/Cargo.toml new file mode 100644 index 0000000..d217bce --- /dev/null +++ b/crates/r1cs-front/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "r1cs-front" +version.workspace = true +edition.workspace = true +license.workspace = true +description = "circom .r1cs / .sym front-end: parse R1CS binaries into scribe's gadget IR" + +[dependencies] +gadget-ir = { path = "../gadget-ir" } +num-bigint = "0.4" +num-traits = "0.2" diff --git a/crates/r1cs-front/examples/gen_fixtures.rs b/crates/r1cs-front/examples/gen_fixtures.rs new file mode 100644 index 0000000..cf35220 --- /dev/null +++ b/crates/r1cs-front/examples/gen_fixtures.rs @@ -0,0 +1,76 @@ +//! Generates two .r1cs fixtures with r1cs-front's builder (no circom install +//! needed): a correct Num2Bits(2) and the classic circomlib IsZero bug. +//! +//! ```sh +//! cargo run -p r1cs-front --example gen_fixtures -- +//! scribe import-r1cs --r1cs /iszero_buggy.r1cs --sym /iszero_buggy.sym \ +//! --spec "(in_ = 0 ∧ out = 1) ∨ (in_ ≠ 0 ∧ out = 0)" +//! scribe judge --gadget /iszero_buggy.gadget.toml # → UNSOUND +//! ``` +// +// Fixture notes: +// - num2bits2.r1cs: correct 2-bit decomposition (circomlib Num2Bits(2) shape) +// - iszero_buggy.r1cs: circomlib IsZero with the `in*out = 0` constraint DROPPED +// (the canonical audit bug — out is then unconstrained for in != 0) +use num_bigint::BigUint; +use r1cs_front::{build_r1cs_bytes, R1csConstraint}; + +fn main() { + let p = BigUint::parse_bytes( + b"21888242871839275222246405745257275088548364400416034343698204186575808495617", + 10, + ) + .unwrap(); + let one = BigUint::from(1u32); + let neg1 = &p - &one; + let dir = std::env::args().nth(1).expect("out dir"); + + // num2bits2: wires 0=1, 1=in, 2=out0, 3=out1 + let num2bits = vec![ + R1csConstraint { + a: vec![(2, one.clone())], + b: vec![(2, one.clone()), (0, neg1.clone())], + c: vec![], + }, + R1csConstraint { + a: vec![(3, one.clone())], + b: vec![(3, one.clone()), (0, neg1.clone())], + c: vec![], + }, + R1csConstraint { + a: vec![(2, one.clone()), (3, BigUint::from(2u32))], + b: vec![(0, one.clone())], + c: vec![(1, one.clone())], + }, + ]; + std::fs::write( + format!("{dir}/num2bits2.r1cs"), + build_r1cs_bytes(&p, 32, 4, &num2bits), + ) + .unwrap(); + std::fs::write( + format!("{dir}/num2bits2.sym"), + "1,1,0,main.in\n2,2,0,main.out[0]\n3,3,0,main.out[1]\n", + ) + .unwrap(); + + // iszero (BUGGY): wires 0=1, 1=in, 2=out, 3=inv + // kept: (-in)*(inv) + 1 - out = 0 i.e. out = 1 - in*inv + // DROPPED: in*out = 0 + let iszero_buggy = vec![R1csConstraint { + a: vec![(1, neg1.clone())], + b: vec![(3, one.clone())], + c: vec![(2, one.clone()), (0, neg1.clone())], + }]; + std::fs::write( + format!("{dir}/iszero_buggy.r1cs"), + build_r1cs_bytes(&p, 32, 4, &iszero_buggy), + ) + .unwrap(); + std::fs::write( + format!("{dir}/iszero_buggy.sym"), + "1,1,0,main.in\n2,2,0,main.out\n3,3,0,main.inv\n", + ) + .unwrap(); + println!("fixtures written to {dir}"); +} diff --git a/crates/r1cs-front/src/lib.rs b/crates/r1cs-front/src/lib.rs new file mode 100644 index 0000000..13741ce --- /dev/null +++ b/crates/r1cs-front/src/lib.rs @@ -0,0 +1,719 @@ +//! circom / R1CS front-end for scribe. +//! +//! Parses the iden3 `.r1cs` binary format (the interchange format emitted by +//! `circom --r1cs` and consumed by snarkjs) plus the companion `.sym` signal +//! map, and converts the rank-1 constraint system into scribe's `gadget-ir` — +//! from which the whole existing pipeline (Lean scaffolds, the proof loop, the +//! adversarial refuter, `scribe judge`) works unchanged. +//! +//! A rank-1 constraint `⟨A,w⟩ · ⟨B,w⟩ = ⟨C,w⟩` is expanded exactly into +//! gadget-ir's sum-of-products form: `Σᵢⱼ aᵢbⱼ·wᵢwⱼ − Σₖ cₖ·wₖ = 0`, with wire 0 +//! (the constant-1 wire) dropping out of monomials. Coefficients are reduced +//! mod the header prime and canonicalized to signed form (`p − 1` renders as +//! `-1`), keeping the emitted Lean statement generic over the field where the +//! circuit's arithmetic allows it — see [`ConvertOptions::max_coeff_bits`]. +//! +//! Format reference: + +use std::collections::BTreeMap; + +use gadget_ir::{Constraint, Gadget, Term, WitnessVar}; +use num_bigint::BigUint; +use num_traits::Zero; + +// ─── Errors ───────────────────────────────────────────────────────────────── + +#[derive(Debug)] +pub enum R1csError { + Io(std::io::Error), + /// Not an r1cs file, or an unsupported version. + BadMagic(String), + /// Structurally invalid content (truncated section, wire id out of range, …). + Malformed(String), + /// Valid file, but outside what the v1 converter supports. + Unsupported(String), +} + +impl std::fmt::Display for R1csError { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + R1csError::Io(e) => write!(f, "io: {e}"), + R1csError::BadMagic(m) => write!(f, "not an r1cs file: {m}"), + R1csError::Malformed(m) => write!(f, "malformed r1cs: {m}"), + R1csError::Unsupported(m) => write!(f, "unsupported by the v1 converter: {m}"), + } + } +} + +impl std::error::Error for R1csError {} + +impl From for R1csError { + fn from(e: std::io::Error) -> Self { + R1csError::Io(e) + } +} + +// ─── Parsed representation ────────────────────────────────────────────────── + +/// One sparse linear combination: `wire id → coefficient` (already reduced +/// mod the prime by the producer; we reduce again defensively). +pub type LinearCombination = Vec<(u32, BigUint)>; + +/// A rank-1 constraint `⟨A,w⟩ · ⟨B,w⟩ = ⟨C,w⟩`. +#[derive(Debug, Clone)] +pub struct R1csConstraint { + pub a: LinearCombination, + pub b: LinearCombination, + pub c: LinearCombination, +} + +/// A parsed `.r1cs` file (header + constraints). +#[derive(Debug, Clone)] +pub struct R1csFile { + /// The field prime from the header. + pub prime: BigUint, + /// Total wires, including wire 0 (the constant 1). + pub n_wires: u32, + pub n_pub_out: u32, + pub n_pub_in: u32, + pub n_prv_in: u32, + pub constraints: Vec, +} + +// ─── Binary parsing ───────────────────────────────────────────────────────── + +struct Reader<'a> { + buf: &'a [u8], + pos: usize, +} + +impl<'a> Reader<'a> { + fn new(buf: &'a [u8]) -> Self { + Reader { buf, pos: 0 } + } + + fn take(&mut self, n: usize, what: &str) -> Result<&'a [u8], R1csError> { + if self.pos + n > self.buf.len() { + return Err(R1csError::Malformed(format!( + "truncated while reading {what} ({n} bytes at offset {})", + self.pos + ))); + } + let s = &self.buf[self.pos..self.pos + n]; + self.pos += n; + Ok(s) + } + + fn u32(&mut self, what: &str) -> Result { + let b = self.take(4, what)?; + Ok(u32::from_le_bytes([b[0], b[1], b[2], b[3]])) + } + + fn u64(&mut self, what: &str) -> Result { + let b = self.take(8, what)?; + Ok(u64::from_le_bytes([ + b[0], b[1], b[2], b[3], b[4], b[5], b[6], b[7], + ])) + } +} + +/// Parse the iden3 `.r1cs` binary format from a byte buffer. +pub fn parse_r1cs_bytes(bytes: &[u8]) -> Result { + let mut r = Reader::new(bytes); + + let magic = r.take(4, "magic")?; + if magic != b"r1cs" { + return Err(R1csError::BadMagic(format!( + "magic is {magic:?}, expected \"r1cs\"" + ))); + } + let version = r.u32("version")?; + if version != 1 { + return Err(R1csError::BadMagic(format!( + "version {version}, only version 1 is supported" + ))); + } + let n_sections = r.u32("section count")?; + + // Sections may appear in any order; index them, then parse header before + // constraints (the constraint encoding needs the header's field size). + let mut sections: BTreeMap = BTreeMap::new(); + for _ in 0..n_sections { + let stype = r.u32("section type")?; + let ssize = r.u64("section size")? as usize; + let content = r.take(ssize, "section content")?; + // Duplicate section types are malformed; keep the first, reject rest. + if sections.insert(stype, content).is_some() { + return Err(R1csError::Malformed(format!( + "duplicate section type {stype}" + ))); + } + } + + let header = sections + .get(&1) + .ok_or_else(|| R1csError::Malformed("missing header section (type 1)".into()))?; + let mut h = Reader::new(header); + let n8 = h.u32("field size")? as usize; + if n8 == 0 || n8 > 64 { + return Err(R1csError::Malformed(format!( + "field size {n8} bytes out of range" + ))); + } + let prime = BigUint::from_bytes_le(h.take(n8, "prime")?); + if prime < BigUint::from(2u8) { + return Err(R1csError::Malformed("prime < 2".into())); + } + let n_wires = h.u32("nWires")?; + let n_pub_out = h.u32("nPubOut")?; + let n_pub_in = h.u32("nPubIn")?; + let n_prv_in = h.u32("nPrvIn")?; + let _n_labels = h.u64("nLabels")?; + let m_constraints = h.u32("mConstraints")?; + + let cs_section = sections + .get(&2) + .ok_or_else(|| R1csError::Malformed("missing constraints section (type 2)".into()))?; + let mut c = Reader::new(cs_section); + let mut constraints = Vec::with_capacity(m_constraints as usize); + for ci in 0..m_constraints { + let mut lcs: [LinearCombination; 3] = [Vec::new(), Vec::new(), Vec::new()]; + for lc in &mut lcs { + let nnz = c.u32("lc term count")?; + for _ in 0..nnz { + let wire = c.u32("wire id")?; + if wire >= n_wires { + return Err(R1csError::Malformed(format!( + "constraint {ci}: wire {wire} out of range (nWires = {n_wires})" + ))); + } + let coeff = BigUint::from_bytes_le(c.take(n8, "coefficient")?) % ′ + if !coeff.is_zero() { + lc.push((wire, coeff)); + } + } + } + let [a, b, c_lc] = lcs; + constraints.push(R1csConstraint { a, b, c: c_lc }); + } + + Ok(R1csFile { + prime, + n_wires, + n_pub_out, + n_pub_in, + n_prv_in, + constraints, + }) +} + +/// Parse a `.r1cs` file from disk. +pub fn parse_r1cs_file(path: &std::path::Path) -> Result { + parse_r1cs_bytes(&std::fs::read(path)?) +} + +// ─── .sym parsing ─────────────────────────────────────────────────────────── + +/// Parse a circom `.sym` file into `wire id → signal name`. +/// +/// Each line is `#label,#wire,#component,name` (e.g. `2,2,1,main.in[0]`); +/// wires optimized out by the compiler carry `-1` and are skipped. When +/// several labels map to one wire (signal aliasing after optimization), the +/// first name wins. +pub fn parse_sym(content: &str) -> BTreeMap { + let mut map = BTreeMap::new(); + for line in content.lines() { + let mut parts = line.splitn(4, ','); + let (Some(_label), Some(wire), Some(_component), Some(name)) = + (parts.next(), parts.next(), parts.next(), parts.next()) + else { + continue; + }; + let Ok(wire) = wire.trim().parse::() else { + continue; + }; + if wire < 0 { + continue; + } + map.entry(wire as u32) + .or_insert_with(|| name.trim().to_string()); + } + map +} + +// ─── Conversion to gadget-ir ──────────────────────────────────────────────── + +/// Options for [`to_gadget`]. +pub struct ConvertOptions { + /// Gadget name (becomes the Lean theorem name after sanitization). + pub name: String, + /// The soundness spec is the human trust root — R1CS carries constraints, + /// never intent, so it must be supplied, not derived. + pub soundness_spec: Option, + /// Reject any canonicalized coefficient wider than this many bits. + /// + /// Small signed coefficients (`-1`, powers of two, …) mean the same + /// polynomial over every prime field, so the emitted theorem can stay + /// generic over `p`. A huge canonical coefficient (e.g. an inverse of 2, + /// `(p+1)/2`) is only meaningful at the header prime — supporting those + /// needs prime-pinned emission, which v1 deliberately does not do. + /// Default 64. + pub max_coeff_bits: u64, +} + +impl Default for ConvertOptions { + fn default() -> Self { + ConvertOptions { + name: "r1cs-import".to_string(), + soundness_spec: None, + max_coeff_bits: 64, + } + } +} + +/// Render a mod-p coefficient in signed canonical form: values above `p/2` +/// render as the negative of their complement (`p − 1` → `"-1"`). +fn canonical_coeff(c: &BigUint, prime: &BigUint) -> String { + let half = prime >> 1; + if c > &half { + format!("-{}", prime - c) + } else { + c.to_string() + } +} + +/// Bit width of the magnitude of a signed canonical coefficient string. +fn canonical_bits(s: &str) -> u64 { + let mag = s.strip_prefix('-').unwrap_or(s); + mag.parse::().map(|b| b.bits()).unwrap_or(u64::MAX) +} + +/// A stable, Lean-friendly witness name from a `.sym` signal name: +/// `main.in[0]` → `in_0`, `main.child.out` → `child_out`. +fn lean_name(sym: &str) -> String { + let trimmed = sym.strip_prefix("main.").unwrap_or(sym); + let mut out = String::new(); + for ch in trimmed.chars() { + match ch { + 'a'..='z' | 'A'..='Z' | '0'..='9' | '_' => out.push(ch), + '.' | '[' => { + if !out.ends_with('_') { + out.push('_'); + } + } + _ => {} + } + } + let out = out.trim_matches('_').to_string(); + if out.is_empty() || out.chars().next().is_some_and(|c| c.is_ascii_digit()) { + return format!("w_{out}"); + } + // Lean 4 keywords make illegal binder names; `in` is a common circom + // signal name, so this bites in practice. + const LEAN_KEYWORDS: &[&str] = &[ + "in", "fun", "let", "do", "then", "else", "if", "match", "with", "by", "at", "from", + "have", "show", "open", "end", "def", "theorem", "example", "variable", "where", + ]; + if LEAN_KEYWORDS.contains(&out.as_str()) { + format!("{out}_") + } else { + out + } +} + +/// Convert a parsed R1CS into a `gadget_ir::Gadget`. +/// +/// Wire 0 is the constant-1 wire: it contributes to coefficients, never to +/// monomials. Every other wire that appears in some constraint becomes a +/// witness variable, named from `sym` when available (`w` otherwise). +/// Each rank-1 row expands to one gadget constraint +/// `Σᵢⱼ aᵢbⱼ·wᵢwⱼ − Σₖ cₖ·wₖ = 0`, with like monomials merged. +pub fn to_gadget( + r1cs: &R1csFile, + sym: &BTreeMap, + opts: &ConvertOptions, +) -> Result { + // Collect the wires that actually occur (excluding wire 0). + let mut used: std::collections::BTreeSet = std::collections::BTreeSet::new(); + for c in &r1cs.constraints { + for (w, _) in c.a.iter().chain(c.b.iter()).chain(c.c.iter()) { + if *w != 0 { + used.insert(*w); + } + } + } + + // Wire id → dense witness id, plus names (deduped after sanitization). + let mut witnesses = Vec::with_capacity(used.len()); + let mut wire_to_id: BTreeMap = BTreeMap::new(); + let mut seen_names: std::collections::BTreeSet = std::collections::BTreeSet::new(); + for (id, wire) in used.iter().enumerate() { + let mut name = sym + .get(wire) + .map(|s| lean_name(s)) + .unwrap_or_else(|| format!("w{wire}")); + if !seen_names.insert(name.clone()) { + name = format!("{name}_w{wire}"); + seen_names.insert(name.clone()); + } + witnesses.push(WitnessVar { id, name }); + wire_to_id.insert(*wire, id); + } + + let prime = &r1cs.prime; + let mut constraints = Vec::with_capacity(r1cs.constraints.len()); + for (ci, rc) in r1cs.constraints.iter().enumerate() { + // Accumulate coefficients per monomial. Key: sorted witness-id list + // (empty = constant term). + let mut acc: BTreeMap, BigUint> = BTreeMap::new(); + let add = |key: Vec, val: BigUint, acc: &mut BTreeMap, BigUint>| { + let entry = acc.entry(key).or_insert_with(BigUint::zero); + *entry = (&*entry + val) % prime; + }; + + // + A·B + for (wa, ca) in &rc.a { + for (wb, cb) in &rc.b { + let coeff = (ca * cb) % prime; + let mut key: Vec = Vec::new(); + if *wa != 0 { + key.push(wire_to_id[wa]); + } + if *wb != 0 { + key.push(wire_to_id[wb]); + } + key.sort_unstable(); + add(key, coeff, &mut acc); + } + } + // − C (as + (p − c)) + for (wc, cc) in &rc.c { + let neg = (prime - cc) % prime; + let key = if *wc == 0 { + Vec::new() + } else { + vec![wire_to_id[wc]] + }; + add(key, neg, &mut acc); + } + + let mut terms = Vec::new(); + for (vars, coeff) in acc { + if coeff.is_zero() { + continue; + } + let rendered = canonical_coeff(&coeff, prime); + let bits = canonical_bits(&rendered); + if bits > opts.max_coeff_bits { + return Err(R1csError::Unsupported(format!( + "constraint {ci}: canonical coefficient {rendered} is {bits} bits wide \ + (limit {}). This circuit's arithmetic is only meaningful at the header \ + prime; prime-pinned emission is not supported yet.", + opts.max_coeff_bits + ))); + } + terms.push(Term { + coeff: rendered, + vars, + }); + } + // A row that cancels to nothing is `0 = 0` — legal R1CS, nothing to state. + if terms.is_empty() { + continue; + } + constraints.push(Constraint { + label: format!("r1cs_{ci}"), + terms, + }); + } + + Ok(Gadget { + name: opts.name.clone(), + modulus: prime.to_string(), + witnesses, + constraints, + hypotheses: Vec::new(), + soundness_spec: opts.soundness_spec.clone(), + }) +} + +// ─── Test-support builder (also used by fixtures) ─────────────────────────── + +/// Serialize an [`R1csFile`]-shaped description back into the binary format. +/// Used by tests to build fixtures without a circom install; kept in the +/// public API so downstream tests (e.g. scribe-cli's) can do the same. +pub fn build_r1cs_bytes( + prime: &BigUint, + n8: usize, + n_wires: u32, + constraints: &[R1csConstraint], +) -> Vec { + let mut out = Vec::new(); + out.extend_from_slice(b"r1cs"); + out.extend_from_slice(&1u32.to_le_bytes()); // version + out.extend_from_slice(&2u32.to_le_bytes()); // two sections + + // Header section + let mut header = Vec::new(); + header.extend_from_slice(&(n8 as u32).to_le_bytes()); + let mut prime_bytes = prime.to_bytes_le(); + prime_bytes.resize(n8, 0); + header.extend_from_slice(&prime_bytes); + header.extend_from_slice(&n_wires.to_le_bytes()); + header.extend_from_slice(&0u32.to_le_bytes()); // nPubOut + header.extend_from_slice(&0u32.to_le_bytes()); // nPubIn + header.extend_from_slice(&0u32.to_le_bytes()); // nPrvIn + header.extend_from_slice(&(n_wires as u64).to_le_bytes()); // nLabels + header.extend_from_slice(&(constraints.len() as u32).to_le_bytes()); + out.extend_from_slice(&1u32.to_le_bytes()); + out.extend_from_slice(&(header.len() as u64).to_le_bytes()); + out.extend_from_slice(&header); + + // Constraints section + let mut cs = Vec::new(); + for c in constraints { + for lc in [&c.a, &c.b, &c.c] { + cs.extend_from_slice(&(lc.len() as u32).to_le_bytes()); + for (wire, coeff) in lc { + cs.extend_from_slice(&wire.to_le_bytes()); + let mut cb = coeff.to_bytes_le(); + cb.resize(n8, 0); + cs.extend_from_slice(&cb); + } + } + } + out.extend_from_slice(&2u32.to_le_bytes()); + out.extend_from_slice(&(cs.len() as u64).to_le_bytes()); + out.extend_from_slice(&cs); + + out +} + +// ─── Tests ────────────────────────────────────────────────────────────────── + +#[cfg(test)] +mod tests { + use super::*; + + fn p() -> BigUint { + // Small prime keeps fixtures readable; the parser never assumes BN254. + BigUint::from(101u32) + } + + fn big(n: u32) -> BigUint { + BigUint::from(n) + } + + /// wires: 0 = const 1, 1 = a, 2 = b, 3 = c; constraint: a * b = c + fn multiplier() -> Vec { + vec![R1csConstraint { + a: vec![(1, big(1))], + b: vec![(2, big(1))], + c: vec![(3, big(1))], + }] + } + + #[test] + fn roundtrip_multiplier() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + let parsed = parse_r1cs_bytes(&bytes).expect("parse"); + assert_eq!(parsed.prime, p()); + assert_eq!(parsed.n_wires, 4); + assert_eq!(parsed.constraints.len(), 1); + assert_eq!(parsed.constraints[0].a, vec![(1, big(1))]); + } + + #[test] + fn rejects_bad_magic_version_truncation_and_range() { + let good = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + + let mut bad = good.clone(); + bad[0] = b'x'; + assert!(matches!( + parse_r1cs_bytes(&bad), + Err(R1csError::BadMagic(_)) + )); + + let mut bad = good.clone(); + bad[4] = 9; // version + assert!(matches!( + parse_r1cs_bytes(&bad), + Err(R1csError::BadMagic(_)) + )); + + assert!(matches!( + parse_r1cs_bytes(&good[..good.len() - 3]), + Err(R1csError::Malformed(_)) + )); + + // wire id ≥ nWires + let out_of_range = vec![R1csConstraint { + a: vec![(9, big(1))], + b: vec![(2, big(1))], + c: vec![(3, big(1))], + }]; + let bytes = build_r1cs_bytes(&p(), 8, 4, &out_of_range); + assert!(matches!( + parse_r1cs_bytes(&bytes), + Err(R1csError::Malformed(_)) + )); + } + + #[test] + fn multiplier_converts_to_expected_terms() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let sym: BTreeMap = [ + (1, "main.a".to_string()), + (2, "main.b".to_string()), + (3, "main.c".to_string()), + ] + .into(); + let gadget = to_gadget( + &parsed, + &sym, + &ConvertOptions { + name: "multiplier".into(), + soundness_spec: Some("c = a * b".into()), + ..Default::default() + }, + ) + .expect("convert"); + + let names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect(); + assert_eq!(names, vec!["a", "b", "c"]); + assert_eq!(gadget.modulus, "101"); + assert_eq!(gadget.constraints.len(), 1); + // a*b - c = 0 → {coeff 1, vars [0,1]}, {coeff -1, vars [2]} + let terms = &gadget.constraints[0].terms; + assert_eq!(terms.len(), 2); + assert!(terms.iter().any(|t| t.coeff == "1" && t.vars == vec![0, 1])); + assert!(terms.iter().any(|t| t.coeff == "-1" && t.vars == vec![2])); + } + + /// Num2Bits(2): out0, out1 bits of in. + /// wires: 0 = 1, 1 = in, 2 = out0, 3 = out1 + /// out0 * (out0 - 1) = 0 + /// out1 * (out1 - 1) = 0 + /// out0 + 2*out1 = in (as lc·1 = in) + fn num2bits() -> Vec { + let one = big(1); + let neg1 = p() - big(1); + vec![ + R1csConstraint { + a: vec![(2, one.clone())], + b: vec![(2, one.clone()), (0, neg1.clone())], + c: vec![], + }, + R1csConstraint { + a: vec![(3, one.clone())], + b: vec![(3, one.clone()), (0, neg1.clone())], + c: vec![], + }, + R1csConstraint { + a: vec![(2, one.clone()), (3, big(2))], + b: vec![(0, one.clone())], + c: vec![(1, one)], + }, + ] + } + + #[test] + fn num2bits_expansion_and_signed_canonicalization() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &num2bits()); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let sym: BTreeMap = [ + (1, "main.in".to_string()), + (2, "main.out[0]".to_string()), + (3, "main.out[1]".to_string()), + ] + .into(); + let gadget = to_gadget(&parsed, &sym, &ConvertOptions::default()).unwrap(); + + let names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect(); + assert_eq!(names, vec!["in_", "out_0", "out_1"]); // `in` is a Lean keyword + + // Constraint 0: out0*out0 - out0 = 0 (p−1 canonicalizes to -1). + let c0 = &gadget.constraints[0].terms; + assert!(c0.iter().any(|t| t.coeff == "1" && t.vars == vec![1, 1])); + assert!(c0.iter().any(|t| t.coeff == "-1" && t.vars == vec![1])); + + // Constraint 2: out0 + 2*out1 - in = 0. + let c2 = &gadget.constraints[2].terms; + assert!(c2.iter().any(|t| t.coeff == "1" && t.vars == vec![1])); + assert!(c2.iter().any(|t| t.coeff == "2" && t.vars == vec![2])); + assert!(c2.iter().any(|t| t.coeff == "-1" && t.vars == vec![0])); + } + + #[test] + fn wide_coefficient_is_rejected_with_guidance() { + // A coefficient like an inverse only means something at THIS prime: + // over ZMod 101, inv(2) = 51 — 51 and -50 are both "wide" relative to + // a 5-bit limit, so the guard must fire. + let cs = vec![R1csConstraint { + a: vec![(1, big(51))], + b: vec![(0, big(1))], + c: vec![(2, big(1))], + }]; + let bytes = build_r1cs_bytes(&p(), 8, 3, &cs); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let opts = ConvertOptions { + max_coeff_bits: 5, + ..Default::default() + }; + let err = to_gadget(&parsed, &BTreeMap::new(), &opts).unwrap_err(); + assert!(matches!(err, R1csError::Unsupported(_))); + assert!(err.to_string().contains("prime-pinned")); + } + + #[test] + fn sym_parsing_names_aliases_and_optimized_wires() { + let sym = parse_sym( + "1,1,0,main.in\n\ + 2,2,0,main.out[0]\n\ + 3,-1,0,main.dropped\n\ + 4,2,0,main.alias_of_out\n\ + garbage line\n", + ); + assert_eq!(sym.get(&1).unwrap(), "main.in"); + assert_eq!(sym.get(&2).unwrap(), "main.out[0]"); // first name wins + assert!(!sym.values().any(|v| v.contains("dropped"))); + } + + #[test] + fn lean_name_sanitization() { + assert_eq!(lean_name("main.in[0]"), "in_0"); + assert_eq!(lean_name("main.child.out"), "child_out"); + assert_eq!(lean_name("main.x"), "x"); + assert_eq!(lean_name("main.0weird"), "w_0weird"); + // Lean keywords must not survive as binder names. + assert_eq!(lean_name("main.in"), "in_"); + assert_eq!(lean_name("main.fun"), "fun_"); + } + + #[test] + fn zero_row_is_dropped_and_like_monomials_merge() { + // (a + b) * 0 = 0 → empty row, dropped. + // (a)·(a) + (a)·(a) via A = [a, a] duplicates → coefficients merge. + let cs = vec![ + R1csConstraint { + a: vec![(1, big(1)), (2, big(1))], + b: vec![], + c: vec![], + }, + R1csConstraint { + a: vec![(1, big(1)), (1, big(1))], + b: vec![(1, big(1))], + c: vec![], + }, + ]; + let bytes = build_r1cs_bytes(&p(), 8, 3, &cs); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let gadget = to_gadget(&parsed, &BTreeMap::new(), &ConvertOptions::default()).unwrap(); + assert_eq!(gadget.constraints.len(), 1); + let terms = &gadget.constraints[0].terms; + assert_eq!(terms.len(), 1); + assert_eq!(terms[0].coeff, "2"); // merged 1+1 + assert_eq!(terms[0].vars, vec![0, 0]); // a * a + } +} diff --git a/crates/scribe-cli/Cargo.toml b/crates/scribe-cli/Cargo.toml index f05a83d..12530ef 100644 --- a/crates/scribe-cli/Cargo.toml +++ b/crates/scribe-cli/Cargo.toml @@ -14,4 +14,6 @@ clap = { version = "4", features = ["derive"] } gadget-ir = { path = "../gadget-ir" } halva-bridge = { path = "../halva-bridge" } lean-emit = { path = "../lean-emit" } +r1cs-front = { path = "../r1cs-front" } +toml = "0.8" proof-pilot = { path = "../proof-pilot" } diff --git a/crates/scribe-cli/src/main.rs b/crates/scribe-cli/src/main.rs index 465a5cb..2b2c230 100644 --- a/crates/scribe-cli/src/main.rs +++ b/crates/scribe-cli/src/main.rs @@ -75,6 +75,17 @@ enum Commands { /// 2 = UNSOUND (kernel-checked counterexample to the spec) /// 3 = infrastructure error Judge(judge_cmd::JudgeArgs), + + /// Import a circom .r1cs circuit (plus its .sym signal map) as a + /// reviewable gadget TOML. + /// + /// Parses the iden3 R1CS binary format, expands each rank-1 row into + /// scribe's sum-of-products IR (coefficients canonicalized to signed + /// form), and writes gadget TOML — the auditable artifact the rest of the + /// pipeline consumes: `scribe judge --gadget out.toml`, `scribe refute`, + /// the eval suite. R1CS carries constraints, never intent, so the + /// soundness spec is yours to state via --spec. + ImportR1cs(import_r1cs_cmd::ImportR1csArgs), } mod verify_cmd { @@ -384,6 +395,48 @@ mod judge_cmd { } } +mod import_r1cs_cmd { + use clap::Args; + + #[derive(Args)] + pub struct ImportR1csArgs { + /// Path to the .r1cs binary (circom --r1cs output). + #[arg(long, value_name = "FILE")] + pub r1cs: String, + + /// Path to the companion .sym signal map (circom --sym output). + /// Optional; without it, witnesses are named w. + #[arg(long, value_name = "FILE")] + pub sym: Option, + + /// Soundness spec: a Lean proposition over the witness names + /// (e.g. "ZMod.val in_ < 4"). Omitting it emits TOML without a spec, + /// which downstream commands will refuse to judge — the spec is the + /// human trust root, not something R1CS can supply. + #[arg(long, value_name = "EXPR")] + pub spec: Option, + + /// Gadget name (default: the .r1cs file stem). + #[arg(long, value_name = "NAME")] + pub name: Option, + + /// Extra hypothesis for the theorem, repeatable, as NAME:LEAN_TYPE + /// (e.g. "hp:p > 4"). Use for load-bearing field-size bounds. + #[arg(long = "hypothesis", value_name = "NAME:TYPE")] + pub hypotheses: Vec, + + /// Reject canonical coefficients wider than this many bits (circuits + /// whose arithmetic only means something at the exact header prime + /// need prime-pinned emission, which is not supported yet). + #[arg(long, value_name = "BITS", default_value = "64")] + pub max_coeff_bits: u64, + + /// Output TOML path (default: .gadget.toml next to input). + #[arg(short = 'o', long, value_name = "FILE")] + pub output: Option, + } +} + fn main() { let cli = Cli::parse(); @@ -407,6 +460,9 @@ fn main() { Commands::Judge(args) => { orchestrate::run_judge(args); } + Commands::ImportR1cs(args) => { + orchestrate::run_import_r1cs(args); + } } } diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs index f6f301b..ae7fe52 100644 --- a/crates/scribe-cli/src/orchestrate.rs +++ b/crates/scribe-cli/src/orchestrate.rs @@ -13,6 +13,7 @@ use proof_pilot::transcript; use crate::demo_cmd::DemoArgs; use crate::extract; +use crate::import_r1cs_cmd::ImportR1csArgs; use crate::judge_cmd::JudgeArgs; use crate::refute_cmd::RefuteArgs; use crate::verify_cmd::VerifyArgs; @@ -460,6 +461,104 @@ pub fn run_refute(args: RefuteArgs) { } } +// ── scribe import-r1cs ─────────────────────────────────────────────────────── + +/// Convert a circom .r1cs (+ optional .sym) into reviewable gadget TOML. +pub fn run_import_r1cs(args: ImportR1csArgs) { + let r1cs_path = Path::new(&args.r1cs); + let r1cs = r1cs_front::parse_r1cs_file(r1cs_path).unwrap_or_else(|e| { + eprintln!("error: cannot parse {}: {e}", args.r1cs); + process::exit(1); + }); + eprintln!( + "[scribe] parsed {}: {} wires, {} constraints, prime ~2^{}", + args.r1cs, + r1cs.n_wires, + r1cs.constraints.len(), + r1cs.prime.bits().saturating_sub(1) + ); + + let sym = match &args.sym { + Some(path) => { + let content = fs::read_to_string(path).unwrap_or_else(|e| { + eprintln!("error: cannot read {path}: {e}"); + process::exit(1); + }); + r1cs_front::parse_sym(&content) + } + None => { + eprintln!("[scribe] no --sym given; witnesses will be named w"); + Default::default() + } + }; + + let name = args.name.clone().unwrap_or_else(|| { + r1cs_path + .file_stem() + .map(|s| s.to_string_lossy().into_owned()) + .unwrap_or_else(|| "r1cs-import".to_string()) + }); + let opts = r1cs_front::ConvertOptions { + name, + soundness_spec: args.spec.clone(), + max_coeff_bits: args.max_coeff_bits, + }; + let mut gadget = r1cs_front::to_gadget(&r1cs, &sym, &opts).unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(1); + }); + + for h in &args.hypotheses { + let Some((hname, ltype)) = h.split_once(':') else { + eprintln!("error: --hypothesis must be NAME:LEAN_TYPE, got '{h}'"); + process::exit(1); + }; + gadget.hypotheses.push(gadget_ir::Hypothesis { + name: hname.trim().to_string(), + lean_type: ltype.trim().to_string(), + }); + } + + if gadget.soundness_spec.is_none() { + eprintln!( + "[scribe] warning: no --spec given. R1CS carries constraints, never intent; \ + without a human-stated spec the TOML cannot be judged." + ); + } + + let out_path = args.output.clone().unwrap_or_else(|| { + let stem = r1cs_path + .file_stem() + .map(|s| s.to_string_lossy().into_owned()) + .unwrap_or_else(|| "r1cs-import".to_string()); + let parent = r1cs_path.parent().unwrap_or(Path::new(".")); + parent + .join(format!("{stem}.gadget.toml")) + .to_string_lossy() + .into_owned() + }); + let header = format!( + "# Imported from {} by `scribe import-r1cs`.\n\ + # Constraints are machine-derived from the R1CS; the soundness_spec is the\n\ + # HUMAN trust root — review it as carefully as you would a theorem statement.\n", + args.r1cs + ); + let body = toml::to_string_pretty(&gadget).unwrap_or_else(|e| { + eprintln!("error: cannot serialize gadget: {e}"); + process::exit(1); + }); + fs::write(&out_path, format!("{header}{body}")).unwrap_or_else(|e| { + eprintln!("error: cannot write {out_path}: {e}"); + process::exit(1); + }); + eprintln!( + "[scribe] wrote {out_path} ({} witnesses, {} constraints)", + gadget.witnesses.len(), + gadget.constraints.len() + ); + println!("{out_path}"); +} + // ── scribe judge ───────────────────────────────────────────────────────────── /// Judge exit codes — stable and documented so third parties can script From 63d32dae4deafcc51f6725cc3f77309a15946aa0 Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Tue, 21 Jul 2026 17:30:30 +0400 Subject: [PATCH 2/2] Fix PR review findings --- crates/proof-pilot/prompts/lean-prover.md | 40 +++++++ crates/proof-pilot/src/lsp_feedback.rs | 49 +++++++- crates/proof-pilot/src/main.rs | 47 ++++++-- crates/r1cs-front/src/lib.rs | 133 ++++++++++++++++++++-- crates/scribe-cli/src/orchestrate.rs | 35 ++++++ 5 files changed, 287 insertions(+), 17 deletions(-) create mode 100644 crates/proof-pilot/prompts/lean-prover.md diff --git a/crates/proof-pilot/prompts/lean-prover.md b/crates/proof-pilot/prompts/lean-prover.md new file mode 100644 index 0000000..8c65a74 --- /dev/null +++ b/crates/proof-pilot/prompts/lean-prover.md @@ -0,0 +1,40 @@ +You are an expert Lean 4 proof engineer. + +## Task + +You receive a Lean 4 file with a theorem whose proof body is `sorry` or a prior +failed attempt. Replace only the proof body so the Lean kernel accepts the file +with zero errors and zero `sorry`. + +## Hard Constraints + +- Do not modify the theorem statement. +- Do not use `sorry`, `axiom`, or `native_decide`. +- Do not invent unavailable lemmas. If unsure, use Lean search tactics such as + `exact?` or `apply?`. +- You may add `import` lines at the top of the code block if needed. +- You may introduce local `have` statements inside the proof body. + +## Response Format + +Return a single fenced Lean code block containing the complete proof body. +Optionally prepend import lines. Do not include explanation unless you are stuck. + +## Useful Patterns + +- Polynomial equalities: try `ring`, `ring_nf`, or `linear_combination`. +- From `h : a - b = 0`, derive `a = b` with `linear_combination h` or + `sub_eq_zero.mp h`. +- For boolean field constraints like `h : b * b - b = 0`, rewrite to + `b * (b - 1) = 0` and use `mul_eq_zero.mp`. +- For goals over `ZMod p`, avoid ordered arithmetic tactics such as `linarith`; + prefer algebraic tactics. + +## Common Imports + +```lean +import Mathlib.Tactic.Ring +import Mathlib.Tactic.LinearCombination +import Mathlib.Data.ZMod.Basic +import Mathlib.Algebra.Field.ZMod +``` diff --git a/crates/proof-pilot/src/lsp_feedback.rs b/crates/proof-pilot/src/lsp_feedback.rs index 42503da..a5e5a07 100644 --- a/crates/proof-pilot/src/lsp_feedback.rs +++ b/crates/proof-pilot/src/lsp_feedback.rs @@ -5,7 +5,7 @@ //! Lean language server — replacing flat `lake build` text parsing. use std::io::{BufRead, BufReader, Write}; -use std::path::Path; +use std::path::{Path, PathBuf}; use std::process::{Child, Command, Stdio}; use serde_json::Value; @@ -228,7 +228,7 @@ const LSP_SERVER_SOURCE: &str = include_str!("../scripts/lsp-server.py"); fn find_script() -> Result { // Explicit override, then repo-local copies (development), then the - // embedded source materialized into a stable per-user temp path. + // embedded source materialized into a stable per-user cache path. if let Ok(path) = std::env::var("PROOF_PILOT_LSP_SERVER") { if Path::new(&path).exists() { return Ok(path); @@ -247,14 +247,47 @@ fn find_script() -> Result { return Ok(c.to_string()); } } - let dir = std::env::temp_dir().join("proof-pilot"); + let dir = user_private_cache_dir()?.join("lsp"); std::fs::create_dir_all(&dir).map_err(|e| format!("create {}: {e}", dir.display()))?; + set_private_dir_permissions(&dir)?; let path = dir.join("lsp-server.py"); std::fs::write(&path, LSP_SERVER_SOURCE) .map_err(|e| format!("write embedded lsp-server.py: {e}"))?; Ok(path.to_string_lossy().into_owned()) } +fn user_private_cache_dir() -> Result { + let root = std::env::var_os("XDG_CACHE_HOME") + .map(PathBuf::from) + .or_else(|| std::env::var_os("LOCALAPPDATA").map(PathBuf::from)) + .or_else(|| std::env::var_os("HOME").map(|home| PathBuf::from(home).join(".cache"))) + .or_else(|| { + std::env::var_os("USERPROFILE") + .map(|home| PathBuf::from(home).join("AppData").join("Local")) + }) + .ok_or_else(|| { + "cannot determine a user-private cache directory for embedded lsp-server.py".to_string() + })?; + Ok(root.join("proof-pilot")) +} + +#[cfg(unix)] +fn set_private_dir_permissions(dir: &Path) -> Result<(), String> { + use std::os::unix::fs::PermissionsExt; + + let mut permissions = std::fs::metadata(dir) + .map_err(|e| format!("stat {}: {e}", dir.display()))? + .permissions(); + permissions.set_mode(0o700); + std::fs::set_permissions(dir, permissions) + .map_err(|e| format!("chmod 700 {}: {e}", dir.display())) +} + +#[cfg(not(unix))] +fn set_private_dir_permissions(_dir: &Path) -> Result<(), String> { + Ok(()) +} + fn parse_feedback(json_str: &str) -> Result { let val: Value = serde_json::from_str(json_str).map_err(|e| format!("parse feedback JSON: {e}"))?; @@ -672,6 +705,16 @@ mod tests { assert!(err.contains("loogle unavailable")); } + #[test] + fn embedded_lsp_cache_avoids_shared_tmp_default() { + let cache_dir = user_private_cache_dir().expect("cache dir should resolve in tests"); + assert_eq!( + cache_dir.file_name().and_then(|s| s.to_str()), + Some("proof-pilot") + ); + assert_ne!(cache_dir, std::env::temp_dir().join("proof-pilot")); + } + #[test] fn goal_to_search_query_extracts_target() { let state = "x : ZMod p\nh : x * x - x = 0\n⊢ x = 0 ∨ x = 1"; diff --git a/crates/proof-pilot/src/main.rs b/crates/proof-pilot/src/main.rs index ae7514d..d427968 100644 --- a/crates/proof-pilot/src/main.rs +++ b/crates/proof-pilot/src/main.rs @@ -5,6 +5,7 @@ use proof_pilot::session::{self, SessionConfig, SessionResult}; use proof_pilot::transcript; const DEFAULT_SYSTEM_PROMPT: &str = "prompts/lean-prover.md"; +const EMBEDDED_SYSTEM_PROMPT: &str = include_str!("../prompts/lean-prover.md"); fn main() { let args: Vec = std::env::args().collect(); @@ -46,6 +47,7 @@ fn main() { let mut max_iterations = 10u32; let mut model: Option = None; let mut system_prompt_file = Some(DEFAULT_SYSTEM_PROMPT.to_string()); + let mut system_prompt_explicit = false; let mut transcript_path: Option = None; let mut save_transcript: Option = None; // --notes takes an optional explicit path; None means "derive from lean_file". @@ -79,6 +81,7 @@ fn main() { } "--system-prompt" => { system_prompt_file = Some(flag_value(&args, &mut i, "--system-prompt")); + system_prompt_explicit = true; } "--transcript" => { transcript_path = Some(flag_value(&args, &mut i, "--transcript")); @@ -174,13 +177,10 @@ fn main() { // ── Normal proof-pilot session ─────────────────────────────────────────── - // Read system prompt from file if provided - let system_prompt = system_prompt_file.map(|path| { - std::fs::read_to_string(&path).unwrap_or_else(|e| { - eprintln!("error reading system prompt {}: {}", path, e); - std::process::exit(1); - }) - }); + // Read system prompt from file if provided. The default falls back to an + // embedded crate-local prompt so the crates.io binary is self-contained. + let system_prompt = + system_prompt_file.map(|path| read_system_prompt(&path, system_prompt_explicit)); // Construct backend let backend = make_backend(&backend_name, model, api_key, base_url).unwrap_or_else(|e| { @@ -257,6 +257,27 @@ fn main() { } } +fn read_system_prompt(path: &str, explicit: bool) -> String { + match std::fs::read_to_string(path) { + Ok(prompt) => prompt, + Err(e) if explicit => { + eprintln!("error reading system prompt {path}: {e}"); + std::process::exit(1); + } + Err(e) if path == DEFAULT_SYSTEM_PROMPT => { + eprintln!( + "[proof-pilot] warning: could not read default system prompt {path}: {e}; \ + using bundled prompt" + ); + EMBEDDED_SYSTEM_PROMPT.to_string() + } + Err(e) => { + eprintln!("error reading system prompt {path}: {e}"); + std::process::exit(1); + } + } +} + fn flag_value(args: &[String], i: &mut usize, flag: &str) -> String { *i += 1; args.get(*i).cloned().unwrap_or_else(|| { @@ -264,3 +285,15 @@ fn flag_value(args: &[String], i: &mut usize, flag: &str) -> String { std::process::exit(1); }) } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn embedded_default_system_prompt_is_available() { + assert!(EMBEDDED_SYSTEM_PROMPT.contains("Lean 4")); + assert!(EMBEDDED_SYSTEM_PROMPT.contains("Do not use `sorry`")); + assert!(EMBEDDED_SYSTEM_PROMPT.contains("Do not modify the theorem statement")); + } +} diff --git a/crates/r1cs-front/src/lib.rs b/crates/r1cs-front/src/lib.rs index 13741ce..b23920f 100644 --- a/crates/r1cs-front/src/lib.rs +++ b/crates/r1cs-front/src/lib.rs @@ -149,6 +149,12 @@ pub fn parse_r1cs_bytes(bytes: &[u8]) -> Result { ))); } } + if r.pos != r.buf.len() { + return Err(R1csError::Malformed(format!( + "trailing bytes after section table at offset {}", + r.pos + ))); + } let header = sections .get(&1) @@ -170,6 +176,12 @@ pub fn parse_r1cs_bytes(bytes: &[u8]) -> Result { let n_prv_in = h.u32("nPrvIn")?; let _n_labels = h.u64("nLabels")?; let m_constraints = h.u32("mConstraints")?; + if h.pos != h.buf.len() { + return Err(R1csError::Malformed(format!( + "trailing bytes in header section at offset {}", + h.pos + ))); + } let cs_section = sections .get(&2) @@ -196,6 +208,12 @@ pub fn parse_r1cs_bytes(bytes: &[u8]) -> Result { let [a, b, c_lc] = lcs; constraints.push(R1csConstraint { a, b, c: c_lc }); } + if c.pos != c.buf.len() { + return Err(R1csError::Malformed(format!( + "trailing bytes in constraints section at offset {}", + c.pos + ))); + } Ok(R1csFile { prime, @@ -324,8 +342,10 @@ fn lean_name(sym: &str) -> String { /// Convert a parsed R1CS into a `gadget_ir::Gadget`. /// /// Wire 0 is the constant-1 wire: it contributes to coefficients, never to -/// monomials. Every other wire that appears in some constraint becomes a -/// witness variable, named from `sym` when available (`w` otherwise). +/// monomials. Every other wire that appears in some constraint, or appears in +/// the `.sym` map, becomes a witness variable. Preserving named unconstrained +/// wires is essential: specs often mention public outputs precisely to catch +/// dangling-output bugs. /// Each rank-1 row expands to one gadget constraint /// `Σᵢⱼ aᵢbⱼ·wᵢwⱼ − Σₖ cₖ·wₖ = 0`, with like monomials merged. pub fn to_gadget( @@ -333,7 +353,7 @@ pub fn to_gadget( sym: &BTreeMap, opts: &ConvertOptions, ) -> Result { - // Collect the wires that actually occur (excluding wire 0). + // Collect constrained wires plus named `.sym` wires (excluding wire 0). let mut used: std::collections::BTreeSet = std::collections::BTreeSet::new(); for c in &r1cs.constraints { for (w, _) in c.a.iter().chain(c.b.iter()).chain(c.c.iter()) { @@ -342,19 +362,34 @@ pub fn to_gadget( } } } + for wire in sym.keys().copied().filter(|w| *w != 0) { + if wire >= r1cs.n_wires { + return Err(R1csError::Malformed(format!( + ".sym references wire {wire}, but nWires = {}", + r1cs.n_wires + ))); + } + used.insert(wire); + } // Wire id → dense witness id, plus names (deduped after sanitization). let mut witnesses = Vec::with_capacity(used.len()); let mut wire_to_id: BTreeMap = BTreeMap::new(); let mut seen_names: std::collections::BTreeSet = std::collections::BTreeSet::new(); for (id, wire) in used.iter().enumerate() { - let mut name = sym + let base_name = sym .get(wire) .map(|s| lean_name(s)) .unwrap_or_else(|| format!("w{wire}")); - if !seen_names.insert(name.clone()) { - name = format!("{name}_w{wire}"); - seen_names.insert(name.clone()); + let mut name = base_name.clone(); + let mut suffix = 0usize; + while !seen_names.insert(name.clone()) { + suffix += 1; + name = if suffix == 1 { + format!("{base_name}_w{wire}") + } else { + format!("{base_name}_w{wire}_{suffix}") + }; } witnesses.push(WitnessVar { id, name }); wire_to_id.insert(*wire, id); @@ -504,6 +539,24 @@ mod tests { BigUint::from(n) } + fn append_to_section(mut bytes: Vec, section_type: u32, extra: &[u8]) -> Vec { + let mut pos = 12usize; // magic + version + section count + loop { + let stype = u32::from_le_bytes(bytes[pos..pos + 4].try_into().unwrap()); + let size_pos = pos + 4; + let size = u64::from_le_bytes(bytes[size_pos..size_pos + 8].try_into().unwrap()); + let content_start = pos + 12; + let content_end = content_start + size as usize; + if stype == section_type { + let new_size = size + extra.len() as u64; + bytes[size_pos..size_pos + 8].copy_from_slice(&new_size.to_le_bytes()); + bytes.splice(content_end..content_end, extra.iter().copied()); + return bytes; + } + pos = content_end; + } + } + /// wires: 0 = const 1, 1 = a, 2 = b, 3 = c; constraint: a * b = c fn multiplier() -> Vec { vec![R1csConstraint { @@ -546,6 +599,23 @@ mod tests { Err(R1csError::Malformed(_)) )); + let mut trailing_file = good.clone(); + trailing_file.push(0); + assert!(matches!( + parse_r1cs_bytes(&trailing_file), + Err(R1csError::Malformed(_)) + )); + + assert!(matches!( + parse_r1cs_bytes(&append_to_section(good.clone(), 1, &[0])), + Err(R1csError::Malformed(_)) + )); + + assert!(matches!( + parse_r1cs_bytes(&append_to_section(good.clone(), 2, &[0])), + Err(R1csError::Malformed(_)) + )); + // wire id ≥ nWires let out_of_range = vec![R1csConstraint { a: vec![(9, big(1))], @@ -716,4 +786,53 @@ mod tests { assert_eq!(terms[0].coeff, "2"); // merged 1+1 assert_eq!(terms[0].vars, vec![0, 0]); // a * a } + + #[test] + fn named_unconstrained_sym_wires_are_preserved_as_witnesses() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let sym: BTreeMap = [ + (1, "main.a".to_string()), + (2, "main.b".to_string()), + (3, "main.c".to_string()), + (4, "main.dangling_out".to_string()), + ] + .into(); + let mut parsed = parsed; + parsed.n_wires = 5; + + let gadget = to_gadget(&parsed, &sym, &ConvertOptions::default()).unwrap(); + let names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect(); + + assert_eq!(names, vec!["a", "b", "c", "dangling_out"]); + } + + #[test] + fn repaired_name_collisions_are_deduped_until_unique() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let sym: BTreeMap = [ + (1, "main.a".to_string()), + (2, "main.a_w3".to_string()), + (3, "main.a".to_string()), + ] + .into(); + + let gadget = to_gadget(&parsed, &sym, &ConvertOptions::default()).unwrap(); + let names: Vec<&str> = gadget.witnesses.iter().map(|w| w.name.as_str()).collect(); + + assert_eq!(names, vec!["a", "a_w3", "a_w3_2"]); + } + + #[test] + fn sym_wire_out_of_range_is_malformed() { + let bytes = build_r1cs_bytes(&p(), 8, 4, &multiplier()); + let parsed = parse_r1cs_bytes(&bytes).unwrap(); + let sym: BTreeMap = [(4, "main.out_of_range".to_string())].into(); + + let err = to_gadget(&parsed, &sym, &ConvertOptions::default()).unwrap_err(); + + assert!(matches!(err, R1csError::Malformed(_))); + assert!(err.to_string().contains(".sym references wire 4")); + } } diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs index ae7fe52..6061250 100644 --- a/crates/scribe-cli/src/orchestrate.rs +++ b/crates/scribe-cli/src/orchestrate.rs @@ -569,6 +569,17 @@ const EXIT_UNDETERMINED: i32 = 1; const EXIT_UNSOUND: i32 = 2; const EXIT_INFRA: i32 = 3; +fn require_judge_spec(gadget: &gadget_ir::Gadget) -> Result<(), String> { + if gadget.soundness_spec.is_some() { + Ok(()) + } else { + Err(format!( + "gadget '{}' has no soundness_spec; there is no spec to judge", + gadget.name + )) + } +} + /// Prove AND attack: the dual-sided verdict. /// /// Prover first — a kernel-accepted proof settles the question (no @@ -580,6 +591,10 @@ pub fn run_judge(args: JudgeArgs) { eprintln!("error: cannot load gadget {}: {e}", args.gadget); process::exit(EXIT_INFRA); }); + require_judge_spec(&gadget).unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(EXIT_INFRA); + }); let lake_dir = resolve_lake_dir(args.lake_dir.as_deref()); let sanitized: String = gadget @@ -947,4 +962,24 @@ mod tests { Some(FALLBACK_SYSTEM_PROMPT) ); } + + #[test] + fn judge_rejects_gadget_without_soundness_spec() { + let gadget = gadget_ir::Gadget { + name: "constraints-without-intent".to_string(), + modulus: "7".to_string(), + soundness_spec: None, + hypotheses: vec![], + witnesses: vec![gadget_ir::WitnessVar { + id: 0, + name: "x".to_string(), + }], + constraints: vec![], + }; + + let err = require_judge_spec(&gadget).expect_err("missing spec must be rejected"); + + assert!(err.contains("no soundness_spec")); + assert!(err.contains("constraints-without-intent")); + } }