circom/R1CS front-end: scribe import-r1cs

Cargo.toml

@@ -6,6 +6,7 @@ members = [
     "crates/proof-pilot",
     "crates/bench",
     "crates/halva-bridge",
+    "crates/r1cs-front",
     "crates/scribe-cli",
 ]
 

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-<commit>` (per-commit), `v<semver>` (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

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
+```

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<String, String> {
     // 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<String, String> {
             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<PathBuf, String> {
+    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<LspFeedback, String> {
     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";

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<String> = std::env::args().collect();
@@ -46,6 +47,7 @@ fn main() {
     let mut max_iterations = 10u32;
     let mut model: Option<String> = None;
     let mut system_prompt_file = Some(DEFAULT_SYSTEM_PROMPT.to_string());
+    let mut system_prompt_explicit = false;
     let mut transcript_path: Option<String> = None;
     let mut save_transcript: Option<String> = 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,10 +257,43 @@ 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(|| {
         eprintln!("missing value for {}", flag);
         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"));
+    }
+}

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"