From 265889203bdcc1dc13bdf4269c67dc5f7a337325 Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Tue, 21 Jul 2026 02:50:46 +0400 Subject: [PATCH 1/2] feat: scribe judge (dual-sided verdicts) + best-of-n sampling MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit scribe judge --gadget : the verdict engine as one command. Prover runs first (a kernel-accepted proof settles the question and sound gadgets usually prove in 1-2 iterations); only on exhaustion does the adversarial refuter run. Verdicts carry kernel-checked artifacts and STABLE documented exit codes so third parties can script judge in their own CI: 0 SOUND / 1 UNDETERMINED / 2 UNSOUND / 3 infrastructure error. Best-of-n sampling (--samples-per-iter K on judge, verify, refute, proof-pilot, and halva-bridge): K attempts per iteration, kernel filters. Design per review amendments: - Replay determinism preserved: the journal records EVERY candidate (CandidateRecord: response, status accepted/build_failed/patch_rejected/ duplicate/not_tried, build output) plus the acceptance index; --replay applies source_after states as before, and pre-best-of-n transcripts load unchanged (serde defaults, round-trip tested). - Candidates are hash-deduplicated before the build phase (low-temperature samples collapse to identical proofs; builds dominate cost) and tried shortest-first, ties broken by sampling order for determinism. - Sampling is concurrent (Backend now Send + Sync; scoped threads), builds sequential with early exit; feedback on total failure is the LAST tried candidate's error, matching the file state on disk. - Lake-build mode only; LSP mode warns and samples once. Live validation: judge(boolean-check, samples-per-iter=2) → SOUND exit 0 at iteration 1; judge(zero-indicator negative) → prove exhausts, refuter finds the counterexample at iteration 1 → UNSOUND exit 2. 8 new tests (planner dedupe/ordering/reject paths, old-journal compat, judge and refute arg parsing); workspace green; clippy clean. --- README.md | 22 ++ crates/bench/src/main.rs | 1 + crates/halva-bridge/src/lib.rs | 7 +- crates/halva-bridge/src/main.rs | 12 + crates/lean-emit/src/lib.rs | 20 +- crates/proof-pilot/src/backend.rs | 6 +- crates/proof-pilot/src/journal.rs | 33 +- crates/proof-pilot/src/main.rs | 12 + crates/proof-pilot/src/notes.rs | 2 + crates/proof-pilot/src/replay.rs | 4 + crates/proof-pilot/src/session.rs | 442 ++++++++++++++++++++++----- crates/proof-pilot/src/transcript.rs | 4 + crates/scribe-cli/src/main.rs | 113 ++++++- crates/scribe-cli/src/orchestrate.rs | 152 ++++++++- 14 files changed, 748 insertions(+), 82 deletions(-) diff --git a/README.md b/README.md index 6dbed50..f19da5b 100644 --- a/README.md +++ b/README.md @@ -137,6 +137,28 @@ scribe refute --gadget examples/range-check/gadget.toml \ 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 judge` + +The verdict engine as one command: prove AND attack, and say which side won. + +```sh +scribe judge --gadget examples/range-check/gadget.toml \ + [--prove-iters N] [--refute-iters M] [--prime P] [--samples-per-iter K] +``` + +The prover runs first (a kernel-accepted proof settles the question — no counterexample can exist, and sound gadgets usually prove in an iteration or two). Only if proving exhausts its budget does the adversarial refuter run. The verdict is backed by a kernel-checked artifact whenever it is not UNDETERMINED: + +| Exit code | Verdict | Meaning | +|---|---|---| +| `0` | **SOUND** | kernel-accepted proof of the spec (path printed) | +| `1` | **UNDETERMINED** | neither proof nor refutation within budget | +| `2` | **UNSOUND** | kernel-checked counterexample (path printed) | +| `3` | — | infrastructure error | + +The exit codes are stable and documented so third parties can script `scribe judge` in their own CI. + +**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 init` Generates the editable Halva extractor project that `scribe verify --circuit` expects. diff --git a/crates/bench/src/main.rs b/crates/bench/src/main.rs index b74e59b..a560597 100644 --- a/crates/bench/src/main.rs +++ b/crates/bench/src/main.rs @@ -419,6 +419,7 @@ fn main() { system_prompt: system_prompt.clone(), transcript: Some(transcript_path), use_lsp: *mode == Mode::Lsp, + samples_per_iter: 1, }; eprint!( diff --git a/crates/halva-bridge/src/lib.rs b/crates/halva-bridge/src/lib.rs index 64e0fa7..0edfc5c 100644 --- a/crates/halva-bridge/src/lib.rs +++ b/crates/halva-bridge/src/lib.rs @@ -926,7 +926,12 @@ private theorem helper : True := by }; let combined = scaffold_soundness(&halva, &config); let re_pos = combined.find(reenable).expect("re-enable present"); - assert!(combined.find("set_option linter.unusedVariables false").unwrap() < re_pos); + assert!( + combined + .find("set_option linter.unusedVariables false") + .unwrap() + < re_pos + ); assert!(re_pos < combined.find("def Spec").unwrap()); // Raw mode: same placement, before the snippet body. diff --git a/crates/halva-bridge/src/main.rs b/crates/halva-bridge/src/main.rs index 4ce81c7..788bfda 100644 --- a/crates/halva-bridge/src/main.rs +++ b/crates/halva-bridge/src/main.rs @@ -37,6 +37,7 @@ fn main() { let mut system_prompt_file = Some(DEFAULT_SYSTEM_PROMPT.to_string()); let mut transcript = None; let mut use_lsp = false; + let mut samples_per_iter = 1u32; let mut backend_name = String::from("claude"); let mut api_key: Option = None; let mut base_url: Option = None; @@ -76,6 +77,16 @@ fn main() { } "--transcript" => transcript = Some(flag_value(&args, &mut i, "--transcript")), "--lsp" => use_lsp = true, + "--samples-per-iter" => { + samples_per_iter = flag_value(&args, &mut i, "--samples-per-iter") + .parse() + .ok() + .filter(|&n| n >= 1) + .unwrap_or_else(|| { + eprintln!("invalid --samples-per-iter value (must be >= 1)"); + process::exit(1); + }); + } "--no-audit-gate" => audit_gate = false, "--backend" => backend_name = flag_value(&args, &mut i, "--backend"), "--api-key" => api_key = Some(flag_value(&args, &mut i, "--api-key")), @@ -183,6 +194,7 @@ fn main() { system_prompt, transcript, use_lsp, + samples_per_iter, }; let (result, _journal) = session::run(&config, backend.as_ref()); diff --git a/crates/lean-emit/src/lib.rs b/crates/lean-emit/src/lib.rs index 2d052f7..8ac435f 100644 --- a/crates/lean-emit/src/lib.rs +++ b/crates/lean-emit/src/lib.rs @@ -217,10 +217,16 @@ fn substitute_p(s: &str, prime: u64) -> String { /// 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 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 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 @@ -263,14 +269,20 @@ pub fn emit_refutation(gadget: &Gadget, prime: u64) -> Result witness_names.join(" ") )); for h in &gadget.hypotheses { - out.push_str(&format!(" {} →\n", substitute_p(&h.lean_type, prime))); + 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))); + 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)); diff --git a/crates/proof-pilot/src/backend.rs b/crates/proof-pilot/src/backend.rs index fe1dc7c..3e4b887 100644 --- a/crates/proof-pilot/src/backend.rs +++ b/crates/proof-pilot/src/backend.rs @@ -8,7 +8,11 @@ use std::process::Command; /// Trait for LLM backends that can complete proof attempts. -pub trait Backend { +/// +/// `Send + Sync` so best-of-n sampling can issue concurrent `complete` calls +/// from scoped threads; implementations take `&self` and hold no interior +/// mutability. +pub trait Backend: Send + Sync { /// Send a prompt to the model and return the response text. fn complete(&self, prompt: &str, system_prompt: Option<&str>) -> Result; diff --git a/crates/proof-pilot/src/journal.rs b/crates/proof-pilot/src/journal.rs index 0c54506..c992b8a 100644 --- a/crates/proof-pilot/src/journal.rs +++ b/crates/proof-pilot/src/journal.rs @@ -5,6 +5,26 @@ //! (P4 NOTES.md, P5 transcript replay) consume this type; it must remain //! serde-stable. +/// One sampled candidate within a best-of-n iteration. +/// +/// Recorded for every sample when `samples_per_iter > 1` so the transcript is a +/// complete, deterministic record: `--replay` applies `source_after` states and +/// never re-derives from responses, but an auditor must be able to see every +/// candidate the kernel filtered and which one was accepted. +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct CandidateRecord { + /// 0-based index in sampling order (the order responses were requested). + pub sample_index: u32, + /// Raw LLM response for this sample. + pub llm_response: String, + /// What happened to this candidate: `"accepted"`, `"build_failed"`, + /// `"patch_rejected"`, `"duplicate"` (identical patched source as an earlier + /// sample), or `"not_tried"` (an earlier candidate was accepted first). + pub status: String, + /// Build output for candidates that were built; empty otherwise. + pub build_output: String, +} + /// A single LLM iteration within a proof session. #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] pub struct IterationRecord { @@ -16,7 +36,9 @@ pub struct IterationRecord { pub source_after: String, /// Full prompt sent to the LLM. pub prompt: String, - /// Raw text response from the LLM. + /// Raw text response from the LLM. Under best-of-n this is the response + /// whose patch ended the iteration (the accepted candidate, or the last + /// candidate tried when all failed) — consistent with `source_after`. pub llm_response: String, /// Build / LSP error text shown to the LLM for this iteration. pub build_errors: String, @@ -26,6 +48,15 @@ pub struct IterationRecord { pub suggestions: Vec, /// `true` if the patch was successfully applied; `false` if it was rejected. pub patch_applied: bool, + /// All sampled candidates, in sampling order. Empty when `samples_per_iter` + /// is 1 (the single response is already `llm_response`). `#[serde(default)]` + /// keeps pre-best-of-n transcripts loadable unchanged. + #[serde(default)] + pub candidates: Vec, + /// `sample_index` of the accepted candidate, when one was accepted under + /// best-of-n sampling. + #[serde(default)] + pub accepted_sample: Option, } /// Complete record of one proof completion session. diff --git a/crates/proof-pilot/src/main.rs b/crates/proof-pilot/src/main.rs index 0816d76..70c0b3a 100644 --- a/crates/proof-pilot/src/main.rs +++ b/crates/proof-pilot/src/main.rs @@ -55,6 +55,7 @@ fn main() { let mut verify = false; let mut allow_toolchain_mismatch = false; let mut use_lsp = false; + let mut samples_per_iter = 1u32; let mut backend_name = String::from("claude"); let mut api_key: Option = None; let mut base_url: Option = None; @@ -107,6 +108,16 @@ fn main() { "--lsp" => { use_lsp = true; } + "--samples-per-iter" => { + samples_per_iter = flag_value(&args, &mut i, "--samples-per-iter") + .parse() + .ok() + .filter(|&n| n >= 1) + .unwrap_or_else(|| { + eprintln!("invalid --samples-per-iter value (must be >= 1)"); + std::process::exit(1); + }); + } "--backend" => { backend_name = flag_value(&args, &mut i, "--backend"); } @@ -183,6 +194,7 @@ fn main() { system_prompt, transcript: transcript_path, use_lsp, + samples_per_iter, }; let (result, journal) = session::run(&config, backend.as_ref()); diff --git a/crates/proof-pilot/src/notes.rs b/crates/proof-pilot/src/notes.rs index 8627c2c..13015f3 100644 --- a/crates/proof-pilot/src/notes.rs +++ b/crates/proof-pilot/src/notes.rs @@ -422,6 +422,8 @@ mod tests { goal_states: goals.iter().map(|s| s.to_string()).collect(), suggestions: suggestions.iter().map(|s| s.to_string()).collect(), patch_applied: applied, + candidates: Vec::new(), + accepted_sample: None, } } diff --git a/crates/proof-pilot/src/replay.rs b/crates/proof-pilot/src/replay.rs index ee19eda..f8e1e78 100644 --- a/crates/proof-pilot/src/replay.rs +++ b/crates/proof-pilot/src/replay.rs @@ -202,6 +202,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: true, + candidates: Vec::new(), + accepted_sample: None, }, IterationRecord { index: 2, @@ -214,6 +216,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: true, + candidates: Vec::new(), + accepted_sample: None, }, ], } diff --git a/crates/proof-pilot/src/session.rs b/crates/proof-pilot/src/session.rs index e82d7b7..090bb03 100644 --- a/crates/proof-pilot/src/session.rs +++ b/crates/proof-pilot/src/session.rs @@ -3,7 +3,7 @@ use std::io::Write; use std::path::Path; use crate::backend::Backend; -use crate::journal::{IterationRecord, SessionJournal}; +use crate::journal::{CandidateRecord, IterationRecord, SessionJournal}; use crate::lean_runner::{has_forbidden_tactics, run_lake_build_for_file}; use crate::lsp_feedback::{ error_suggestions, feedback_as_build_output, format_lsp_feedback, format_probe_results, @@ -26,6 +26,12 @@ pub struct SessionConfig { pub transcript: Option, /// Use Lean LSP for structured feedback instead of lake build text parsing. pub use_lsp: bool, + /// Best-of-n: sampled proof attempts per iteration (default 1). The kernel + /// filters — candidates are deduplicated, tried shortest-first, and the + /// first to build wins. Soundness-free parallelism: a wrong candidate costs + /// a build, never a false acceptance. Lake-build mode only; LSP mode warns + /// and samples once. + pub samples_per_iter: u32, } /// Outcome of a proof session. @@ -93,6 +99,13 @@ fn run_with_lsp( let lean_path = Path::new(&config.lean_file); let lake_dir = Path::new(&config.lake_dir); + if config.samples_per_iter > 1 { + eprintln!( + "[proof-pilot] warning: --samples-per-iter applies to lake-build mode; \ + LSP mode samples once per iteration" + ); + } + let mut log = open_log(config); log_line( &mut log, @@ -215,6 +228,8 @@ fn run_with_lsp( goal_states: last_feedback.goal_states(), suggestions: last_feedback.suggestions(), patch_applied: false, + candidates: Vec::new(), + accepted_sample: None, }); continue; @@ -311,6 +326,8 @@ fn run_with_lsp( goal_states: last_feedback.goal_states(), suggestions: last_feedback.suggestions(), patch_applied, + candidates: Vec::new(), + accepted_sample: None, }); if let Some(result) = iteration_result { @@ -481,6 +498,121 @@ fn enrich_feedback( } } +// ─── Best-of-n sampling ───────────────────────────────────────────────────── + +/// Everything the build phase needs for one best-of-n iteration, planned +/// deterministically before any file is written. +struct SamplePlan { + /// One record per sample, in sampling order. `patch_rejected` / `duplicate` + /// are final; the rest start as `"not_tried"` and are updated by the build + /// phase. + records: Vec, + /// `(sample_index, patched_source)` in build order: shortest patched source + /// first (ties broken by sampling order, so the plan is deterministic given + /// the responses). + try_order: Vec<(u32, String)>, +} + +/// Request `k` completions. For `k > 1` the calls run concurrently on scoped +/// threads (the kernel filters, so parallel sampling is soundness-free); the +/// returned vector is in sampling order regardless of completion order. +fn sample_responses( + backend: &dyn Backend, + prompt: &str, + system_prompt: Option<&str>, + k: u32, +) -> Vec> { + if k <= 1 { + return vec![backend.complete(prompt, system_prompt)]; + } + std::thread::scope(|scope| { + let handles: Vec<_> = (0..k) + .map(|_| scope.spawn(|| backend.complete(prompt, system_prompt))) + .collect(); + handles + .into_iter() + .map(|h| { + h.join().unwrap_or_else(|_| { + Err(crate::backend::BackendError::RequestFailed( + "sampling thread panicked".to_string(), + )) + }) + }) + .collect() + }) +} + +/// Plan the build phase: apply the patcher to each response (pure — no file is +/// touched), record rejects, hash-dedupe identical patched sources (samples at +/// low temperature frequently collapse to the same proof, and builds dominate +/// cost), and order the survivors shortest-first. +fn plan_candidates( + source_before: &str, + responses: &[String], + build_output: &str, + target_file: &str, +) -> SamplePlan { + let mut records: Vec = Vec::with_capacity(responses.len()); + let mut planned: Vec<(u32, String)> = Vec::new(); + let mut seen: std::collections::HashSet = std::collections::HashSet::new(); + + for (i, response) in responses.iter().enumerate() { + let sample_index = i as u32; + match apply_patch_with_diagnostics(source_before, response, build_output, Some(target_file)) + { + Ok(patched) => { + use std::hash::{Hash, Hasher}; + let mut hasher = std::collections::hash_map::DefaultHasher::new(); + patched.hash(&mut hasher); + if seen.insert(hasher.finish()) { + planned.push((sample_index, patched)); + records.push(CandidateRecord { + sample_index, + llm_response: response.clone(), + status: "not_tried".to_string(), + build_output: String::new(), + }); + } else { + records.push(CandidateRecord { + sample_index, + llm_response: response.clone(), + status: "duplicate".to_string(), + build_output: String::new(), + }); + } + } + Err(e) => { + records.push(CandidateRecord { + sample_index, + llm_response: response.clone(), + status: "patch_rejected".to_string(), + build_output: format!("patch error: {e}"), + }); + } + } + } + + // Shortest candidate first; sampling order breaks ties deterministically. + planned.sort_by(|a, b| a.1.len().cmp(&b.1.len()).then(a.0.cmp(&b.0))); + + SamplePlan { + records, + try_order: planned, + } +} + +fn set_candidate_status( + records: &mut [CandidateRecord], + sample_index: u32, + status: &str, + build_output: String, +) { + if let Some(r) = records.iter_mut().find(|r| r.sample_index == sample_index) { + r.status = status.to_string(); + r.build_output = build_output; + } +} + // ─── Original lake-build feedback loop (unchanged logic) ──────────────────── fn run_with_lake_build( @@ -539,97 +671,177 @@ fn run_with_lake_build( log_line(&mut log, &format!("[prompt]\n{}\n", prompt)); - let llm_response = match backend.complete(&prompt, config.system_prompt.as_deref()) { - Ok(r) => r, - Err(e) => return SessionResult::Failed(format!("backend: {e}")), - }; + // Sample k candidates (concurrently when k > 1); the kernel filters. + let k = config.samples_per_iter.max(1); + let sampled = sample_responses(backend, &prompt, config.system_prompt.as_deref(), k); + let responses: Vec = sampled + .iter() + .filter_map(|r| r.as_ref().ok().cloned()) + .collect(); + if responses.is_empty() { + let e = sampled + .into_iter() + .find_map(|r| r.err()) + .expect("no responses implies at least one error"); + return SessionResult::Failed(format!("backend: {e}")); + } + if responses.len() < k as usize { + eprintln!( + "[proof-pilot] warning: {}/{} sample(s) failed; continuing with the rest", + k as usize - responses.len(), + k + ); + } + for (i, r) in responses.iter().enumerate() { + log_line(&mut log, &format!("[llm response, sample {i}]\n{r}\n")); + } - log_line(&mut log, &format!("[llm response]\n{}\n", llm_response)); + // Plan: patch each candidate (pure), dedupe, shortest-first. + let mut plan = plan_candidates(&source_before, &responses, &last_stderr, &config.lean_file); - // Apply patch - let (patched, patch_applied, build_errors_after) = match apply_patch_with_diagnostics( - &source_before, - &llm_response, - &last_stderr, - Some(&config.lean_file), - ) { - Ok(p) => (p, true, last_stderr.clone()), - Err(e) => { - eprintln!("[proof-pilot] patch rejected: {}", e); - log_line(&mut log, &format!("[patch] REJECTED: {}\n", e)); - let combined_error = format!("(patch error: {})\n{}", e, last_stderr); + // Journal candidate records only under genuine best-of-n; with k = 1 the + // single response is already `llm_response` (schema-stable with old runs). + let record_candidates = k > 1; - journal.push(IterationRecord { - index: iteration, - source_before: source_before.clone(), - source_after: source_before.clone(), - prompt: prompt.clone(), - llm_response: llm_response.clone(), - build_errors: last_stderr.clone(), - goal_states: Vec::new(), - suggestions: Vec::new(), - patch_applied: false, - }); + if plan.try_order.is_empty() { + // Every candidate was rejected by the patcher. + let first_reason = plan + .records + .iter() + .find(|r| r.status == "patch_rejected") + .map(|r| r.build_output.clone()) + .unwrap_or_else(|| "patch error: no candidates".to_string()); + eprintln!("[proof-pilot] patch rejected: {first_reason}"); + log_line(&mut log, &format!("[patch] REJECTED: {first_reason}\n")); + let combined_error = format!("({})\n{}", first_reason, last_stderr); + + journal.push(IterationRecord { + index: iteration, + source_before: source_before.clone(), + source_after: source_before.clone(), + prompt: prompt.clone(), + llm_response: responses[0].clone(), + build_errors: last_stderr.clone(), + goal_states: Vec::new(), + suggestions: Vec::new(), + patch_applied: false, + candidates: if record_candidates { + plan.records + } else { + Vec::new() + }, + accepted_sample: None, + }); - last_stderr = combined_error; - continue; + last_stderr = combined_error; + continue; + } + + // Build phase: sequential with early exit — success costs one build. + let mut accepted: Option<(u32, String)> = None; + let mut last_failed: Option<(u32, String, String)> = None; + let try_order = std::mem::take(&mut plan.try_order); + for (sample_index, patched) in &try_order { + log_line( + &mut log, + &format!("[patched file, sample {sample_index}]\n{patched}\n"), + ); + if let Err(e) = fs::write(lean_path, patched) { + return SessionResult::Failed(format!("write {}: {}", config.lean_file, e)); } + match run_lake_build_for_file(lake_dir, lean_path) { + Ok(r) + if r.success + && !has_forbidden_tactics(&r.combined, Some(&config.lean_file)) => + { + set_candidate_status(&mut plan.records, *sample_index, "accepted", r.combined); + accepted = Some((*sample_index, patched.clone())); + break; + } + Ok(r) => { + log_line( + &mut log, + &format!("[build] FAIL (sample {sample_index})\n{}\n", r.combined), + ); + set_candidate_status( + &mut plan.records, + *sample_index, + "build_failed", + r.combined.clone(), + ); + last_failed = Some((*sample_index, patched.clone(), r.combined)); + } + Err(e) => return SessionResult::Failed(format!("lake build: {}", e)), + } + } + + let response_for = |sample_index: u32| -> String { + plan.records + .iter() + .find(|r| r.sample_index == sample_index) + .map(|r| r.llm_response.clone()) + .unwrap_or_default() }; - log_line(&mut log, &format!("[patched file]\n{}\n", patched)); + if let Some((sample_index, patched)) = accepted { + eprintln!("[proof-pilot] proof accepted at iteration {}", iteration); + log_line( + &mut log, + &format!("[build] SUCCESS at iteration {iteration} (sample {sample_index})\n"), + ); + + journal.push(IterationRecord { + index: iteration, + source_before, + source_after: patched, + prompt, + llm_response: response_for(sample_index), + build_errors: last_stderr.clone(), + goal_states: Vec::new(), + suggestions: Vec::new(), + patch_applied: true, + candidates: if record_candidates { + plan.records + } else { + Vec::new() + }, + accepted_sample: if record_candidates { + Some(sample_index) + } else { + None + }, + }); - // Write patched file - if let Err(e) = fs::write(lean_path, &patched) { - return SessionResult::Failed(format!("write {}: {}", config.lean_file, e)); + return SessionResult::Proven { + iterations: iteration, + }; } - // Rebuild - let (build_result, new_stderr) = match run_lake_build_for_file(lake_dir, lean_path) { - Ok(r) if r.success && !has_forbidden_tactics(&r.combined, Some(&config.lean_file)) => { - eprintln!("[proof-pilot] proof accepted at iteration {}", iteration); - log_line( - &mut log, - &format!("[build] SUCCESS at iteration {}\n", iteration), - ); - - journal.push(IterationRecord { - index: iteration, - source_before, - source_after: patched, - prompt, - llm_response, - build_errors: build_errors_after, - goal_states: Vec::new(), - suggestions: Vec::new(), - patch_applied, - }); - - return SessionResult::Proven { - iterations: iteration, - }; - } - Ok(r) => { - eprintln!("[proof-pilot] build failed, retrying..."); - log_line(&mut log, &format!("[build] FAIL\n{}\n", r.combined)); - let stderr = r.combined.clone(); - (r.combined, stderr) - } - Err(e) => return SessionResult::Failed(format!("lake build: {}", e)), - }; + // All candidates failed to build. The file on disk holds the LAST tried + // candidate, so record and feed back exactly that state. + let (sample_index, patched, build_output) = + last_failed.expect("non-empty try_order with no acceptance has a last failure"); + eprintln!("[proof-pilot] build failed, retrying..."); journal.push(IterationRecord { index: iteration, source_before, source_after: patched, prompt, - llm_response, - build_errors: build_result, + llm_response: response_for(sample_index), + build_errors: build_output.clone(), goal_states: Vec::new(), suggestions: Vec::new(), - patch_applied, + patch_applied: true, + candidates: if record_candidates { + plan.records + } else { + Vec::new() + }, + accepted_sample: None, }); - last_stderr = new_stderr; + last_stderr = build_output; } log_line( @@ -749,6 +961,92 @@ mod tests { use super::*; use crate::lsp_feedback::{Diagnostic, GoalState}; + const SORRY_SOURCE: &str = "theorem foo : True := by\n sorry\n"; + + fn fenced(body: &str) -> String { + format!("```lean\n{body}\n```") + } + + #[test] + fn plan_dedupes_orders_shortest_first_and_records_rejects() { + let responses = vec![ + fenced("exact True.intro"), // sample 0: longer proof + fenced("trivial"), // sample 1: shorter proof + fenced("trivial"), // sample 2: duplicate of 1 + "no code block".to_string(), // sample 3: patcher must reject + ]; + let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); + + // Build order: shortest patched source first, then the longer one. + assert_eq!(plan.try_order.len(), 2); + assert_eq!(plan.try_order[0].0, 1); + assert_eq!(plan.try_order[1].0, 0); + assert!(plan.try_order[0].1.len() < plan.try_order[1].1.len()); + assert!(plan.try_order[0].1.contains("trivial")); + + // Records cover every sample, in sampling order, with final statuses for + // duplicates and rejects. + let statuses: Vec<&str> = plan.records.iter().map(|r| r.status.as_str()).collect(); + assert_eq!( + statuses, + vec!["not_tried", "not_tried", "duplicate", "patch_rejected"] + ); + assert!(plan.records[3].build_output.starts_with("patch error:")); + } + + #[test] + fn plan_length_ties_break_by_sampling_order() { + // Same length, different content — deterministic order must follow + // sampling order, not hash order. + let responses = vec![fenced("simp_a"), fenced("simp_b")]; + let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); + assert_eq!(plan.try_order.len(), 2); + assert_eq!(plan.try_order[0].0, 0); + assert_eq!(plan.try_order[1].0, 1); + } + + #[test] + fn plan_all_rejected_yields_empty_try_order() { + let responses = vec!["nope".to_string(), "also nope".to_string()]; + let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); + assert!(plan.try_order.is_empty()); + assert!(plan + .records + .iter() + .all(|r| r.status == "patch_rejected")); + } + + #[test] + fn set_candidate_status_targets_by_sample_index() { + let responses = vec![fenced("trivial"), fenced("exact True.intro")]; + let mut plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); + set_candidate_status(&mut plan.records, 1, "accepted", "ok".to_string()); + assert_eq!(plan.records[1].status, "accepted"); + assert_eq!(plan.records[1].build_output, "ok"); + assert_eq!(plan.records[0].status, "not_tried"); + } + + #[test] + fn pre_best_of_n_journal_json_still_loads() { + // An IterationRecord serialized before the candidates/accepted_sample + // fields existed must deserialize with defaults — the replay + // determinism contract includes old transcripts. + let old = r#"{ + "index": 1, + "source_before": "a", + "source_after": "b", + "prompt": "p", + "llm_response": "r", + "build_errors": "", + "goal_states": [], + "suggestions": [], + "patch_applied": true + }"#; + let rec: IterationRecord = serde_json::from_str(old).expect("old journal must load"); + assert!(rec.candidates.is_empty()); + assert_eq!(rec.accepted_sample, None); + } + #[test] fn lsp_prompt_preserves_lake_fallback_output() { let feedback = diff --git a/crates/proof-pilot/src/transcript.rs b/crates/proof-pilot/src/transcript.rs index befdad4..2027a4b 100644 --- a/crates/proof-pilot/src/transcript.rs +++ b/crates/proof-pilot/src/transcript.rs @@ -110,6 +110,8 @@ mod tests { goal_states: vec!["⊢ True".to_string()], suggestions: vec!["try trivial".to_string()], patch_applied: true, + candidates: Vec::new(), + accepted_sample: None, }, IterationRecord { index: 2, @@ -121,6 +123,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: false, + candidates: Vec::new(), + accepted_sample: None, }, ], } diff --git a/crates/scribe-cli/src/main.rs b/crates/scribe-cli/src/main.rs index ffb3dde..465a5cb 100644 --- a/crates/scribe-cli/src/main.rs +++ b/crates/scribe-cli/src/main.rs @@ -61,6 +61,20 @@ enum Commands { /// refutation found within the budget; evidence, not proof, of soundness); /// 1 = infrastructure error. Refute(refute_cmd::RefuteArgs), + + /// Judge a gadget: prove AND attack, emit a verdict. + /// + /// Runs the prover loop first (a kernel-accepted proof settles the question + /// — no counterexample can exist). If proving exhausts its budget, runs the + /// adversarial refuter. The verdict is backed by a kernel-checked artifact + /// whenever it is SOUND or UNSOUND. + /// + /// Exit codes (stable — script against them): + /// 0 = SOUND (kernel-accepted proof of the spec) + /// 1 = UNDETERMINED (neither proof nor refutation within budget) + /// 2 = UNSOUND (kernel-checked counterexample to the spec) + /// 3 = infrastructure error + Judge(judge_cmd::JudgeArgs), } mod verify_cmd { @@ -170,6 +184,11 @@ mod verify_cmd { /// Use Lean LSP for structured feedback instead of raw `lake build` text. #[arg(long)] pub lsp: bool, + + /// Best-of-n: sampled proof attempts per iteration; the kernel filters + /// (default: 1). Lake-build mode only. + #[arg(long, value_name = "K", default_value = "1")] + pub samples_per_iter: u32, } } @@ -308,6 +327,60 @@ mod refute_cmd { /// Transcript log file path (optional). #[arg(long, value_name = "FILE")] pub transcript: Option, + + /// Best-of-n: sampled refutation attempts per iteration; the kernel + /// filters (default: 1). + #[arg(long, value_name = "K", default_value = "1")] + pub samples_per_iter: u32, + } +} + +mod judge_cmd { + use clap::Args; + + #[derive(Args)] + pub struct JudgeArgs { + /// Gadget IR file (TOML) to judge. + #[arg(long, value_name = "FILE")] + pub gadget: String, + + /// Probe prime for the refutation phase (default: auto from `p > N` + /// hypotheses, floor 5). + #[arg(long, value_name = "P")] + pub prime: Option, + + /// Maximum prover iterations (default: 5). + #[arg(long, value_name = "N", default_value = "5")] + pub prove_iters: u32, + + /// Maximum refuter iterations (default: 4). + #[arg(long, value_name = "N", default_value = "4")] + pub refute_iters: u32, + + /// Best-of-n: sampled attempts per iteration in BOTH phases; the kernel + /// filters (default: 1). + #[arg(long, value_name = "K", default_value = "1")] + pub samples_per_iter: u32, + + /// Lake project directory (default: $LAKE_DIR env var, else `lean`). + #[arg(long, value_name = "DIR")] + pub lake_dir: Option, + + /// 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, } } @@ -331,6 +404,9 @@ fn main() { Commands::Refute(args) => { orchestrate::run_refute(args); } + Commands::Judge(args) => { + orchestrate::run_judge(args); + } } } @@ -473,10 +549,43 @@ mod tests { } } + #[test] + fn judge_args_parse_with_defaults() { + let cli = + Cli::try_parse_from(["scribe", "judge", "--gadget", "g.toml"]).expect("should parse"); + if let Commands::Judge(args) = cli.command { + assert_eq!(args.gadget, "g.toml"); + assert_eq!(args.prove_iters, 5); + assert_eq!(args.refute_iters, 4); + assert_eq!(args.samples_per_iter, 1); + assert_eq!(args.prime, None); + } else { + panic!("expected Judge"); + } + + let cli = Cli::try_parse_from([ + "scribe", + "judge", + "--gadget", + "g.toml", + "--samples-per-iter", + "3", + "--prove-iters", + "2", + ]) + .expect("should parse"); + if let Commands::Judge(args) = cli.command { + assert_eq!(args.samples_per_iter, 3); + assert_eq!(args.prove_iters, 2); + } else { + panic!("expected Judge"); + } + } + #[test] fn refute_args_parse_with_defaults() { - let cli = Cli::try_parse_from(["scribe", "refute", "--gadget", "g.toml"]) - .expect("should parse"); + 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 diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs index ab4b4fa..d0a38c5 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::judge_cmd::JudgeArgs; use crate::refute_cmd::RefuteArgs; use crate::verify_cmd::VerifyArgs; @@ -46,7 +47,12 @@ fn resolve_system_prompt_from( explicit: Option<&str>, prompts_dir: Option, ) -> Option { - resolve_prompt_from(explicit, prompts_dir, "lean-prover.md", FALLBACK_SYSTEM_PROMPT) + resolve_prompt_from( + explicit, + prompts_dir, + "lean-prover.md", + FALLBACK_SYSTEM_PROMPT, + ) } fn resolve_prompt_from( @@ -187,6 +193,7 @@ pub fn run_verify(args: VerifyArgs) { system_prompt, transcript: args.transcript.clone(), use_lsp: args.lsp, + samples_per_iter: args.samples_per_iter, }; let (result, journal) = session::run(&config, backend.as_ref()); @@ -371,6 +378,7 @@ pub fn run_refute(args: RefuteArgs) { system_prompt, transcript: args.transcript.clone(), use_lsp: false, + samples_per_iter: args.samples_per_iter, }; let (result, _journal) = session::run(&config, backend.as_ref()); @@ -402,6 +410,147 @@ pub fn run_refute(args: RefuteArgs) { } } +// ── scribe judge ───────────────────────────────────────────────────────────── + +/// Judge exit codes — stable and documented so third parties can script +/// `scribe judge` in their own CI: 0 SOUND, 1 UNDETERMINED, 2 UNSOUND, +/// 3 infrastructure error. +const EXIT_SOUND: i32 = 0; +const EXIT_UNDETERMINED: i32 = 1; +const EXIT_UNSOUND: i32 = 2; +const EXIT_INFRA: i32 = 3; + +/// Prove AND attack: the dual-sided verdict. +/// +/// Prover first — a kernel-accepted proof settles the question (no +/// counterexample can exist), and sound gadgets usually prove in an iteration +/// or two, so this order minimizes expected cost. Only when proving exhausts +/// its budget does the adversarial refuter run. +pub fn run_judge(args: JudgeArgs) { + 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(EXIT_INFRA); + }); + + let lake_dir = resolve_lake_dir(args.lake_dir.as_deref()); + let sanitized: String = gadget + .name + .chars() + .map(|c| if c.is_ascii_alphanumeric() { c } else { '_' }) + .collect(); + let backend = make_backend( + &args.backend, + args.model.clone(), + args.api_key.clone(), + args.base_url.clone(), + ); + eprintln!("[scribe judge] backend: {}", backend.name()); + + let read_prompt = |path: Option| -> Option { + path.map(|p| { + fs::read_to_string(&p).unwrap_or_else(|e| { + eprintln!("error: cannot read system prompt {p}: {e}"); + process::exit(EXIT_INFRA); + }) + }) + }; + + // ── Phase 1: prove ─────────────────────────────────────────────────────── + let prove_scaffold = lean_emit::emit_lean(&gadget).unwrap_or_else(|e| { + eprintln!("error: cannot emit prover scaffold: {e}"); + process::exit(EXIT_INFRA); + }); + let prove_path = format!("{lake_dir}/ZkGadgets/Bench/Judge{sanitized}.lean"); + if let Some(parent) = Path::new(&prove_path).parent() { + let _ = fs::create_dir_all(parent); + } + if let Err(e) = fs::write(&prove_path, &prove_scaffold) { + eprintln!("error: cannot write {prove_path}: {e}"); + process::exit(EXIT_INFRA); + } + eprintln!( + "[scribe judge] phase 1/2 — prove ({} iterations max): {prove_path}", + args.prove_iters + ); + + let prove_config = SessionConfig { + lean_file: prove_path.clone(), + lake_dir: lake_dir.clone(), + max_iterations: args.prove_iters, + system_prompt: read_prompt(resolve_system_prompt(None)), + transcript: None, + use_lsp: false, + samples_per_iter: args.samples_per_iter, + }; + match session::run(&prove_config, backend.as_ref()).0 { + SessionResult::Proven { iterations } => { + eprintln!("[scribe judge] kernel accepted a proof in {iterations} iteration(s)"); + println!("SOUND: {prove_path}"); + process::exit(EXIT_SOUND); + } + SessionResult::Failed(msg) => { + eprintln!("[scribe judge] fatal error in prove phase: {msg}"); + process::exit(EXIT_INFRA); + } + SessionResult::Exhausted { iterations, .. } => { + eprintln!( + "[scribe judge] no proof in {iterations} iteration(s) — \ + escalating to the refuter" + ); + } + } + + // ── Phase 2: refute ────────────────────────────────────────────────────── + let prime = args + .prime + .unwrap_or_else(|| lean_emit::refutation_prime(&gadget, 5)); + let refute_scaffold = lean_emit::emit_refutation(&gadget, prime).unwrap_or_else(|e| { + eprintln!("error: cannot emit refutation scaffold: {e}"); + process::exit(EXIT_INFRA); + }); + let refute_path = format!("{lake_dir}/ZkGadgets/Bench/Refute{sanitized}.lean"); + if let Err(e) = fs::write(&refute_path, &refute_scaffold) { + eprintln!("error: cannot write {refute_path}: {e}"); + process::exit(EXIT_INFRA); + } + eprintln!( + "[scribe judge] phase 2/2 — refute at p = {prime} ({} iterations max): {refute_path}", + args.refute_iters + ); + + let refute_config = SessionConfig { + lean_file: refute_path.clone(), + lake_dir, + max_iterations: args.refute_iters, + system_prompt: read_prompt(resolve_refuter_prompt(None)), + transcript: None, + use_lsp: false, + samples_per_iter: args.samples_per_iter, + }; + match session::run(&refute_config, backend.as_ref()).0 { + SessionResult::Proven { iterations } => { + eprintln!( + "[scribe judge] ⚠ kernel-checked counterexample found in {iterations} \ + iteration(s) at p = {prime}" + ); + println!("UNSOUND: {refute_path}"); + process::exit(EXIT_UNSOUND); + } + SessionResult::Failed(msg) => { + eprintln!("[scribe judge] fatal error in refute phase: {msg}"); + process::exit(EXIT_INFRA); + } + SessionResult::Exhausted { .. } => { + eprintln!( + "[scribe judge] no proof and no refutation within budget — \ + the spec's status is genuinely open at these budgets" + ); + println!("UNDETERMINED: {}", args.gadget); + process::exit(EXIT_UNDETERMINED); + } + } +} + pub fn run_demo(args: DemoArgs) { let lake_dir = resolve_lake_dir(args.lake_dir.as_deref()); @@ -536,6 +685,7 @@ fn run_demo_live(args: &DemoArgs, lake_dir: &str) { system_prompt, transcript: None, use_lsp: false, + samples_per_iter: 1, }; let (result, _journal) = session::run(&config, backend.as_ref()); From 915fc5199bf6e755caea49d3f51473f2567a23e9 Mon Sep 17 00:00:00 2001 From: Samuel Akinosho <39565075+LucidSamuel@users.noreply.github.com> Date: Tue, 21 Jul 2026 03:04:02 +0400 Subject: [PATCH 2/2] fix: judge exit-code contract for backend errors + journal completeness under partial sampling failures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review findings on #17: - High: make_backend (and require_api_key) exited 1 internally on missing keys/URLs/unknown backends, so 'scribe judge --backend anthropic' without ANTHROPIC_API_KEY exited 1 — violating judge's documented exit-3 infrastructure contract. make_backend now returns Result and the CALLER owns the exit code: judge exits 3, verify/refute/demo/proof-pilot/halva-bridge keep their documented 1. Verified: judge → 3 (missing key and unknown backend), refute → 1. - Medium: partial concurrent-sample failures were filtered out before planning, so candidate records omitted them and sample_index/accepted_sample no longer referred to the original K requested samples. plan_candidates now consumes the raw Result vector: failed requests are recorded in place with status "request_failed" (error in build_output, empty llm_response) and surviving candidates keep their original indexes. 'The journal records every candidate' now includes sampling failures; new unit test pins it. --- crates/halva-bridge/src/main.rs | 5 +- crates/proof-pilot/src/backend.rs | 89 +++++++++++---------- crates/proof-pilot/src/journal.rs | 4 +- crates/proof-pilot/src/main.rs | 5 +- crates/proof-pilot/src/replay.rs | 8 +- crates/proof-pilot/src/session.rs | 111 +++++++++++++++++++-------- crates/proof-pilot/src/transcript.rs | 8 +- crates/scribe-cli/src/orchestrate.rs | 24 +++++- 8 files changed, 163 insertions(+), 91 deletions(-) diff --git a/crates/halva-bridge/src/main.rs b/crates/halva-bridge/src/main.rs index 788bfda..b3c3019 100644 --- a/crates/halva-bridge/src/main.rs +++ b/crates/halva-bridge/src/main.rs @@ -185,7 +185,10 @@ fn main() { }) }); - let backend = make_backend(&backend_name, model, api_key, base_url); + let backend = make_backend(&backend_name, model, api_key, base_url).unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(1); + }); let config = SessionConfig { lean_file: out_path.clone(), diff --git a/crates/proof-pilot/src/backend.rs b/crates/proof-pilot/src/backend.rs index 3e4b887..2dea0dc 100644 --- a/crates/proof-pilot/src/backend.rs +++ b/crates/proof-pilot/src/backend.rs @@ -289,90 +289,89 @@ pub fn resolve_api_key(explicit: Option<&str>, env_var: &str) -> Option } /// Require an API key, resolving from an explicit value or environment variable. -/// -/// Prints an error and calls `std::process::exit(1)` if neither is available. -pub fn require_api_key(explicit: Option<&str>, env_var: &str, backend: &str) -> String { - resolve_api_key(explicit, env_var).unwrap_or_else(|| { - eprintln!("{backend} backend requires --api-key or {env_var} env var"); - std::process::exit(1); - }) +pub fn require_api_key( + explicit: Option<&str>, + env_var: &str, + backend: &str, +) -> Result { + resolve_api_key(explicit, env_var) + .ok_or_else(|| format!("{backend} backend requires --api-key or {env_var} env var")) } -/// Construct a `Box` from a name, optional model, API key, and base URL. -/// -/// Recognized names: `claude` / `claude-cli`, `anthropic`, `openai`, `leanstral`, -/// `leanstral-local`, `openai-compat`. -/// Exits the process with a diagnostic message if the name is unknown or required -/// parameters (key, URL) are missing. /// Default model for the `claude`/`anthropic` backends when `--model` is not /// given. Kept in one place because retired models fail at request time (e.g. /// claude-sonnet-4-20250514 was retired 2026-06-15 and broke every default run). pub const DEFAULT_ANTHROPIC_MODEL: &str = "claude-sonnet-5"; +/// Construct a `Box` from a name, optional model, API key, and base URL. +/// +/// Recognized names: `claude` / `claude-cli`, `anthropic`, `openai`, `leanstral`, +/// `leanstral-local`, `openai-compat`. +/// +/// Returns `Err` with a diagnostic message if the name is unknown or required +/// parameters (key, URL) are missing — the CALLER owns the exit code, because +/// different commands document different infrastructure-error codes (`scribe +/// judge` exits 3, `scribe refute` exits 1). pub fn make_backend( name: &str, model: Option, api_key: Option, base_url: Option, -) -> Box { +) -> Result, String> { match name { "claude" | "claude-cli" => { let m = model.unwrap_or_else(|| DEFAULT_ANTHROPIC_MODEL.into()); - Box::new(ClaudeCli::new(m)) + Ok(Box::new(ClaudeCli::new(m))) } "anthropic" => { let m = model.unwrap_or_else(|| DEFAULT_ANTHROPIC_MODEL.into()); - let key = require_api_key(api_key.as_deref(), "ANTHROPIC_API_KEY", "anthropic"); + let key = require_api_key(api_key.as_deref(), "ANTHROPIC_API_KEY", "anthropic")?; let mut b = AnthropicApi::new(m, key); if let Some(url) = base_url { b = b.with_base_url(url); } - Box::new(b) + Ok(Box::new(b)) } "openai" => { let m = model.unwrap_or_else(|| "gpt-4o".into()); - let key = require_api_key(api_key.as_deref(), "OPENAI_API_KEY", "openai"); + let key = require_api_key(api_key.as_deref(), "OPENAI_API_KEY", "openai")?; let url = base_url.unwrap_or_else(|| "https://api.openai.com/v1".into()); - Box::new( + Ok(Box::new( OpenAiCompatible::new(m, Some(key), url) .with_completion_tokens() .with_name("openai".into()), - ) + )) } "leanstral" => { let m = model.unwrap_or_else(|| "leanstral-v1".into()); - let key = require_api_key(api_key.as_deref(), "LEANSTRAL_API_KEY", "leanstral"); - let url = base_url.unwrap_or_else(|| { - eprintln!( - "leanstral backend requires --base-url (e.g. https://api.leanstral.ai/v1)" - ); - std::process::exit(1); - }); - Box::new(OpenAiCompatible::new(m, Some(key), url).with_name("leanstral".into())) + let key = require_api_key(api_key.as_deref(), "LEANSTRAL_API_KEY", "leanstral")?; + let url = base_url.ok_or_else(|| { + "leanstral backend requires --base-url (e.g. https://api.leanstral.ai/v1)" + .to_string() + })?; + Ok(Box::new( + OpenAiCompatible::new(m, Some(key), url).with_name("leanstral".into()), + )) } "leanstral-local" => { let m = model.unwrap_or_else(|| "leanstral-v1".into()); let url = base_url.unwrap_or_else(|| "http://localhost:8000/v1".into()); - Box::new(OpenAiCompatible::new(m, api_key, url).with_name("leanstral-local".into())) + Ok(Box::new( + OpenAiCompatible::new(m, api_key, url).with_name("leanstral-local".into()), + )) } "openai-compat" => { - let m = model.unwrap_or_else(|| { - eprintln!("openai-compat backend requires --model"); - std::process::exit(1); - }); - let url = base_url.unwrap_or_else(|| { - eprintln!("openai-compat backend requires --base-url"); - std::process::exit(1); - }); - Box::new(OpenAiCompatible::new(m, api_key, url).with_name("openai-compat".into())) - } - other => { - eprintln!("unknown backend: {other}"); - eprintln!( - "available: claude, anthropic, openai, leanstral, leanstral-local, openai-compat" - ); - std::process::exit(1); + let m = model.ok_or_else(|| "openai-compat backend requires --model".to_string())?; + let url = + base_url.ok_or_else(|| "openai-compat backend requires --base-url".to_string())?; + Ok(Box::new( + OpenAiCompatible::new(m, api_key, url).with_name("openai-compat".into()), + )) } + other => Err(format!( + "unknown backend: {other}\navailable: claude, anthropic, openai, leanstral, \ + leanstral-local, openai-compat" + )), } } diff --git a/crates/proof-pilot/src/journal.rs b/crates/proof-pilot/src/journal.rs index c992b8a..ab9f5d1 100644 --- a/crates/proof-pilot/src/journal.rs +++ b/crates/proof-pilot/src/journal.rs @@ -19,7 +19,9 @@ pub struct CandidateRecord { pub llm_response: String, /// What happened to this candidate: `"accepted"`, `"build_failed"`, /// `"patch_rejected"`, `"duplicate"` (identical patched source as an earlier - /// sample), or `"not_tried"` (an earlier candidate was accepted first). + /// sample), `"not_tried"` (an earlier candidate was accepted first), or + /// `"request_failed"` (the backend call itself failed — `llm_response` is + /// empty and the error is in `build_output`). pub status: String, /// Build output for candidates that were built; empty otherwise. pub build_output: String, diff --git a/crates/proof-pilot/src/main.rs b/crates/proof-pilot/src/main.rs index 70c0b3a..ae7514d 100644 --- a/crates/proof-pilot/src/main.rs +++ b/crates/proof-pilot/src/main.rs @@ -183,7 +183,10 @@ fn main() { }); // Construct backend - let backend = make_backend(&backend_name, model, api_key, base_url); + let backend = make_backend(&backend_name, model, api_key, base_url).unwrap_or_else(|e| { + eprintln!("error: {e}"); + std::process::exit(1); + }); eprintln!("[proof-pilot] backend: {}", backend.name()); diff --git a/crates/proof-pilot/src/replay.rs b/crates/proof-pilot/src/replay.rs index f8e1e78..0fd3ef7 100644 --- a/crates/proof-pilot/src/replay.rs +++ b/crates/proof-pilot/src/replay.rs @@ -202,8 +202,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: true, - candidates: Vec::new(), - accepted_sample: None, + candidates: Vec::new(), + accepted_sample: None, }, IterationRecord { index: 2, @@ -216,8 +216,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: true, - candidates: Vec::new(), - accepted_sample: None, + candidates: Vec::new(), + accepted_sample: None, }, ], } diff --git a/crates/proof-pilot/src/session.rs b/crates/proof-pilot/src/session.rs index 090bb03..4aa7581 100644 --- a/crates/proof-pilot/src/session.rs +++ b/crates/proof-pilot/src/session.rs @@ -542,22 +542,37 @@ fn sample_responses( }) } -/// Plan the build phase: apply the patcher to each response (pure — no file is -/// touched), record rejects, hash-dedupe identical patched sources (samples at -/// low temperature frequently collapse to the same proof, and builds dominate -/// cost), and order the survivors shortest-first. +/// Plan the build phase from the raw sampling results: request failures are +/// recorded in place (so `sample_index` always refers to the original K +/// requested samples and the journal genuinely records every candidate), then +/// each successful response is patched (pure — no file is touched), rejects +/// recorded, identical patched sources hash-deduped (samples at low temperature +/// frequently collapse to the same proof, and builds dominate cost), and the +/// survivors ordered shortest-first. fn plan_candidates( source_before: &str, - responses: &[String], + samples: &[Result], build_output: &str, target_file: &str, ) -> SamplePlan { - let mut records: Vec = Vec::with_capacity(responses.len()); + let mut records: Vec = Vec::with_capacity(samples.len()); let mut planned: Vec<(u32, String)> = Vec::new(); let mut seen: std::collections::HashSet = std::collections::HashSet::new(); - for (i, response) in responses.iter().enumerate() { + for (i, sample) in samples.iter().enumerate() { let sample_index = i as u32; + let response = match sample { + Ok(r) => r, + Err(e) => { + records.push(CandidateRecord { + sample_index, + llm_response: String::new(), + status: "request_failed".to_string(), + build_output: format!("backend: {e}"), + }); + continue; + } + }; match apply_patch_with_diagnostics(source_before, response, build_output, Some(target_file)) { Ok(patched) => { @@ -674,37 +689,47 @@ fn run_with_lake_build( // Sample k candidates (concurrently when k > 1); the kernel filters. let k = config.samples_per_iter.max(1); let sampled = sample_responses(backend, &prompt, config.system_prompt.as_deref(), k); - let responses: Vec = sampled - .iter() - .filter_map(|r| r.as_ref().ok().cloned()) - .collect(); - if responses.is_empty() { + let ok_count = sampled.iter().filter(|r| r.is_ok()).count(); + if ok_count == 0 { let e = sampled .into_iter() .find_map(|r| r.err()) .expect("no responses implies at least one error"); return SessionResult::Failed(format!("backend: {e}")); } - if responses.len() < k as usize { + if ok_count < k as usize { eprintln!( "[proof-pilot] warning: {}/{} sample(s) failed; continuing with the rest", - k as usize - responses.len(), + k as usize - ok_count, k ); } - for (i, r) in responses.iter().enumerate() { - log_line(&mut log, &format!("[llm response, sample {i}]\n{r}\n")); + let first_ok_response = sampled + .iter() + .find_map(|r| r.as_ref().ok()) + .cloned() + .expect("ok_count > 0"); + for (i, r) in sampled.iter().enumerate() { + match r { + Ok(text) => log_line(&mut log, &format!("[llm response, sample {i}]\n{text}\n")), + Err(e) => log_line( + &mut log, + &format!("[llm response, sample {i}] FAILED: {e}\n"), + ), + } } - // Plan: patch each candidate (pure), dedupe, shortest-first. - let mut plan = plan_candidates(&source_before, &responses, &last_stderr, &config.lean_file); + // Plan: patch each candidate (pure), dedupe, shortest-first. The plan's + // records cover ALL k requested samples — including request failures — + // with sample_index referring to the original sampling order. + let mut plan = plan_candidates(&source_before, &sampled, &last_stderr, &config.lean_file); // Journal candidate records only under genuine best-of-n; with k = 1 the // single response is already `llm_response` (schema-stable with old runs). let record_candidates = k > 1; if plan.try_order.is_empty() { - // Every candidate was rejected by the patcher. + // Every successful sample was rejected by the patcher. let first_reason = plan .records .iter() @@ -720,7 +745,7 @@ fn run_with_lake_build( source_before: source_before.clone(), source_after: source_before.clone(), prompt: prompt.clone(), - llm_response: responses[0].clone(), + llm_response: first_ok_response.clone(), build_errors: last_stderr.clone(), goal_states: Vec::new(), suggestions: Vec::new(), @@ -970,10 +995,10 @@ mod tests { #[test] fn plan_dedupes_orders_shortest_first_and_records_rejects() { let responses = vec![ - fenced("exact True.intro"), // sample 0: longer proof - fenced("trivial"), // sample 1: shorter proof - fenced("trivial"), // sample 2: duplicate of 1 - "no code block".to_string(), // sample 3: patcher must reject + Ok(fenced("exact True.intro")), // sample 0: longer proof + Ok(fenced("trivial")), // sample 1: shorter proof + Ok(fenced("trivial")), // sample 2: duplicate of 1 + Ok("no code block".to_string()), // sample 3: patcher must reject ]; let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); @@ -998,27 +1023,51 @@ mod tests { fn plan_length_ties_break_by_sampling_order() { // Same length, different content — deterministic order must follow // sampling order, not hash order. - let responses = vec![fenced("simp_a"), fenced("simp_b")]; + let responses = vec![Ok(fenced("simp_a")), Ok(fenced("simp_b"))]; let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); assert_eq!(plan.try_order.len(), 2); assert_eq!(plan.try_order[0].0, 0); assert_eq!(plan.try_order[1].0, 1); } + #[test] + fn plan_records_request_failures_at_original_indexes() { + // A failed concurrent sample must appear in the records at its original + // sample_index — "the journal records every candidate" includes partial + // sampling failures, and accepted_sample must keep referring to the + // originally requested K samples. + let responses = vec![ + Err(crate::backend::BackendError::RequestFailed( + "boom".to_string(), + )), + Ok(fenced("trivial")), + Ok(fenced("exact True.intro")), + ]; + let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); + + assert_eq!(plan.records.len(), 3); + assert_eq!(plan.records[0].status, "request_failed"); + assert_eq!(plan.records[0].sample_index, 0); + assert!(plan.records[0].llm_response.is_empty()); + assert!(plan.records[0].build_output.contains("boom")); + // Surviving candidates keep their ORIGINAL indexes (1 and 2), shortest + // first. + assert_eq!(plan.try_order.len(), 2); + assert_eq!(plan.try_order[0].0, 1); + assert_eq!(plan.try_order[1].0, 2); + } + #[test] fn plan_all_rejected_yields_empty_try_order() { - let responses = vec!["nope".to_string(), "also nope".to_string()]; + let responses = vec![Ok("nope".to_string()), Ok("also nope".to_string())]; let plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); assert!(plan.try_order.is_empty()); - assert!(plan - .records - .iter() - .all(|r| r.status == "patch_rejected")); + assert!(plan.records.iter().all(|r| r.status == "patch_rejected")); } #[test] fn set_candidate_status_targets_by_sample_index() { - let responses = vec![fenced("trivial"), fenced("exact True.intro")]; + let responses = vec![Ok(fenced("trivial")), Ok(fenced("exact True.intro"))]; let mut plan = plan_candidates(SORRY_SOURCE, &responses, "", "Foo.lean"); set_candidate_status(&mut plan.records, 1, "accepted", "ok".to_string()); assert_eq!(plan.records[1].status, "accepted"); diff --git a/crates/proof-pilot/src/transcript.rs b/crates/proof-pilot/src/transcript.rs index 2027a4b..c7a63f1 100644 --- a/crates/proof-pilot/src/transcript.rs +++ b/crates/proof-pilot/src/transcript.rs @@ -110,8 +110,8 @@ mod tests { goal_states: vec!["⊢ True".to_string()], suggestions: vec!["try trivial".to_string()], patch_applied: true, - candidates: Vec::new(), - accepted_sample: None, + candidates: Vec::new(), + accepted_sample: None, }, IterationRecord { index: 2, @@ -123,8 +123,8 @@ mod tests { goal_states: vec![], suggestions: vec![], patch_applied: false, - candidates: Vec::new(), - accepted_sample: None, + candidates: Vec::new(), + accepted_sample: None, }, ], } diff --git a/crates/scribe-cli/src/orchestrate.rs b/crates/scribe-cli/src/orchestrate.rs index d0a38c5..2775cec 100644 --- a/crates/scribe-cli/src/orchestrate.rs +++ b/crates/scribe-cli/src/orchestrate.rs @@ -183,7 +183,11 @@ pub fn run_verify(args: VerifyArgs) { args.model.clone(), args.api_key.clone(), args.base_url.clone(), - ); + ) + .unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(1); + }); eprintln!("[scribe] backend: {}", backend.name()); let config = SessionConfig { @@ -368,7 +372,11 @@ pub fn run_refute(args: RefuteArgs) { args.model.clone(), args.api_key.clone(), args.base_url.clone(), - ); + ) + .unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(1); + }); eprintln!("[scribe] refuter backend: {}", backend.name()); let config = SessionConfig { @@ -443,7 +451,11 @@ pub fn run_judge(args: JudgeArgs) { args.model.clone(), args.api_key.clone(), args.base_url.clone(), - ); + ) + .unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(EXIT_INFRA); + }); eprintln!("[scribe judge] backend: {}", backend.name()); let read_prompt = |path: Option| -> Option { @@ -675,7 +687,11 @@ fn run_demo_live(args: &DemoArgs, lake_dir: &str) { args.model.clone(), args.api_key.clone(), args.base_url.clone(), - ); + ) + .unwrap_or_else(|e| { + eprintln!("error: {e}"); + process::exit(1); + }); eprintln!("[scribe demo --live] backend: {}", backend.name()); let config = SessionConfig {