feat: BI-1 serve socket + Julia oracle + project-root + sandbox + parser fix

BI-1 (per docs/ECHIDNA-INTEGRATION.adoc §BI-1):
- New `burrower serve --socket <path>` Unix-socket endpoint exposing
  swarm/attempt/ledger/ping over line-delimited JSON.
- Sync std::os::unix UnixListener with thread-per-connection (no tokio
  dep added — corpus loads + ledger ops are independent per request).
- Verified via socat: ping/unknown-cmd/malformed-json all roundtrip.
- SocketGuard cleans the socket on normal Drop; defensive bind-side
  unlink handles SIGTERM-killed stale sockets (known Drop limitation).

Oracle (safe-learning c — adversarial test generation):
- New oracle module dispatches `tools/julia-oracle.jl` as a subprocess
  with an A2ML descriptor argument; parses the verdict line.
- OracleVerdict::Disagree and FuzzCounter block the proof attempt
  ("lemma statement is suspect"); other verdicts are advisory.
- record_to_ledger appends an Oracle-authored learning entry with
  pattern_kind in {oracle-counter-example, oracle-fuzz-counter,
  oracle-agree, oracle-fuzz-clean, oracle-inapplicable, oracle-
  subprocess-error}.
- 5 unit tests over verdict parsing.
- Wired into burrower-cli `attempt` via --oracle / --oracle-descriptor /
  --oracle-project / --oracle-julia. End-to-end verified: a deliberately
  wrong tropical-determinant lemma is blocked BEFORE specialists run.

Project-root + sandbox plumbing:
- ProverConfig gains project_root: Option<PathBuf> + sandbox: String.
- run_probe forwards `--project-root` and `--sandbox` to echidna when
  set. burrower-cli `attempt` exposes both as flags.
- This is what makes the EI-1 + safe-learning-b chain functional from
  the burrower side.

Critical bugfix (discovered during the headline dogfood):
- run_probe's success/failure marker was stdout-only. Echidna's
  OutputFormatter writes its verdict to STDERR, so every attempt was
  misclassified as "inconclusive output" and demoted to a
  generic-failure anti-pattern. Fixed: parser now scans both streams
  AND falls back on the exit code. Without this, the swarm's failure
  diagnostics were useless.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

crates/burrower-cli/src/main.rs

@@ -98,12 +98,44 @@ enum Cmd {
         /// Output format: `text` (default) or `json`.
         #[arg(long, default_value = "text")]
         format: String,
+        /// Project root for echidna's EI-1 `--project-root` flag.
+        /// Required for goals importing project-specific theories.
+        #[arg(long)]
+        project_root: Option<PathBuf>,
+        /// Sandbox mode for prover invocation (safe-learning b).
+        /// One of: none (default), bwrap, podman.
+        #[arg(long, default_value = "none")]
+        sandbox: String,
+        /// Path to tools/julia-oracle.jl (safe-learning c). When set,
+        /// the oracle runs BEFORE the specialist playbook; a
+        /// `disagree` or `fuzz-counter` verdict skips the proof.
+        #[arg(long)]
+        oracle: Option<PathBuf>,
+        /// Oracle descriptor (a2ml). Required when --oracle is set.
+        #[arg(long)]
+        oracle_descriptor: Option<PathBuf>,
+        /// Optional --project=<dir> for julia (path to repo with Manifest.toml).
+        #[arg(long)]
+        oracle_project: Option<PathBuf>,
+        /// Path to the julia binary (default: julia on PATH).
+        #[arg(long, default_value = "julia")]
+        oracle_julia: PathBuf,
     },
     /// Burrow Ledger inspection.
     Ledger {
         #[command(subcommand)]
         sub: LedgerCmd,
     },
+    /// BI-1: expose the swarm over a Unix socket so echidna and
+    /// echidnabot can both consume `swarm` / `attempt` / `ledger`
+    /// commands without re-instantiating the corpus per call.
+    /// Protocol: line-delimited JSON {cmd, args} → {ok, result|error}.
+    /// See proof-burrower/docs/ECHIDNA-INTEGRATION.adoc §BI-1.
+    Serve {
+        /// Path to the Unix socket to bind. Defaults to /tmp/burrower.sock.
+        #[arg(long, default_value = "/tmp/burrower.sock")]
+        socket: PathBuf,
+    },
 }
 
 #[derive(Subcommand)]
@@ -225,20 +257,63 @@ fn handle_ledger(cmd: LedgerCmd) -> Result<()> {
     Ok(())
 }
 
+#[allow(clippy::too_many_arguments)]
 fn handle_attempt(
     goal: String,
     echidna: PathBuf,
     timeout: u32,
     ledger: PathBuf,
     format: String,
+    project_root: Option<PathBuf>,
+    sandbox: String,
+    oracle: Option<PathBuf>,
+    oracle_descriptor: Option<PathBuf>,
+    oracle_project: Option<PathBuf>,
+    oracle_julia: PathBuf,
 ) -> Result<()> {
     let parsed = parse_goal(&goal);
     let swarm = Swarm::new();
     let l = Ledger::open(&ledger)?;
+
+    // Safe-learning (c): if an oracle script + descriptor were
+    // supplied, run the oracle BEFORE specialist playbooks. A blocking
+    // verdict (disagree / fuzz-counter) means the lemma statement is
+    // suspect and we skip the playbook entirely. Either way the result
+    // is recorded in the ledger so the swarm learns the lemma's
+    // numerical character even when no proof is attempted.
+    if let (Some(script), Some(descriptor)) = (oracle.as_ref(), oracle_descriptor.as_ref()) {
+        let cfg = burrower_core::oracle::OracleConfig {
+            script: script.clone(),
+            descriptor: descriptor.clone(),
+            julia: oracle_julia.clone(),
+            project: oracle_project.clone(),
+        };
+        let verdict = burrower_core::oracle::run(&cfg);
+        burrower_core::oracle::record_to_ledger(&l, &parsed, &cfg, &verdict);
+        eprintln!("oracle: {:?}", verdict);
+        if verdict.blocks_attempt() {
+            eprintln!(
+                "oracle BLOCKS attempt (lemma statement suspect or oracle inconsistent); \
+                 skipping specialist playbooks. Ledger records this as `{}`.",
+                verdict.pattern_kind()
+            );
+            // Emit a json result-shape consistent with the normal path.
+            if format == "json" {
+                println!("{}", serde_json::json!({
+                    "blocked_by_oracle": true,
+                    "verdict_kind": verdict.pattern_kind(),
+                }));
+            }
+            return Ok(());
+        }
+    }
+
     let prover = ProverConfig {
         echidna_path: echidna,
         timeout_secs: timeout,
         workdir: None,
+        project_root,
+        sandbox,
     };
     let attempts = swarm.attempt_all(&parsed, &prover, Some(&l));
 
@@ -293,10 +368,19 @@ fn handle_attempt(
 fn main() -> Result<()> {
     let cli = Cli::parse();
     match cli.cmd {
-        Cmd::Attempt { goal, echidna, timeout, ledger, format } => {
-            return handle_attempt(goal, echidna, timeout, ledger, format)
+        Cmd::Attempt {
+            goal, echidna, timeout, ledger, format,
+            project_root, sandbox,
+            oracle, oracle_descriptor, oracle_project, oracle_julia,
+        } => {
+            return handle_attempt(
+                goal, echidna, timeout, ledger, format,
+                project_root, sandbox,
+                oracle, oracle_descriptor, oracle_project, oracle_julia,
+            )
         }
         Cmd::Ledger { sub } => return handle_ledger(sub),
+        Cmd::Serve { socket } => return burrower_core::serve::run(socket),
         Cmd::Index { root, output } => {
             let corpus = Corpus::index(&root)?;
             corpus.save(&output)?;

crates/burrower-core/src/attempt.rs

@@ -65,6 +65,17 @@ pub struct ProverConfig {
     pub timeout_secs: u32,
     /// Workdir for probe files. Defaults to `/tmp` if unset.
     pub workdir: Option<PathBuf>,
+    /// Project root for echidna's EI-1 `--project-root` flag (2026-04-26).
+    /// When set, every probe is dispatched as
+    /// `echidna prove --project-root <p> ...`, letting the probe's
+    /// theory imports resolve against the project's existing ROOT.
+    /// Without this, probes can only `imports Main`.
+    pub project_root: Option<PathBuf>,
+    /// Sandbox mode forwarded to echidna's `--sandbox` flag
+    /// (safe-learning b, 2026-04-26). One of "none" | "bwrap" | "podman".
+    /// Default "none" preserves backwards compatibility; recommend
+    /// "bwrap" when running specialist playbooks against unverified goals.
+    pub sandbox: String,
 }
 
 impl Default for ProverConfig {
@@ -73,6 +84,8 @@ impl Default for ProverConfig {
             echidna_path: PathBuf::from("echidna"),
             timeout_secs: 60,
             workdir: None,
+            project_root: None,
+            sandbox: "none".to_string(),
         }
     }
 }
@@ -207,51 +220,85 @@ pub fn run_probe(
     }
 
     let start = Instant::now();
-    let output = Command::new(&config.echidna_path)
-        .arg("prove")
+    let mut cmd = Command::new(&config.echidna_path);
+    cmd.arg("prove")
         .arg(&probe_path)
         .arg("--prover")
         .arg("Isabelle")
         .arg("-t")
-        .arg(config.timeout_secs.to_string())
-        .output();
+        .arg(config.timeout_secs.to_string());
+    // EI-1: forward the project root so probes importing project-
+    // specific theories (Tropical_v2, walks_def, ...) resolve.
+    if let Some(p) = config.project_root.as_ref() {
+        cmd.arg("--project-root").arg(p);
+    }
+    // safe-learning b: forward the sandbox mode. echidna defaults to
+    // "none" so an unset value is the same as the legacy path.
+    if config.sandbox != "none" && !config.sandbox.is_empty() {
+        cmd.arg("--sandbox").arg(&config.sandbox);
+    }
+    let output = cmd.output();
     let elapsed = start.elapsed();
     let elapsed_ms = elapsed.as_millis() as u64;
 
     match output {
         Ok(o) => {
             let stdout = String::from_utf8_lossy(&o.stdout);
             let stderr = String::from_utf8_lossy(&o.stderr);
-            if stdout.contains("Proof verified successfully") {
-                AttemptResult::Succeeded {
-                    duration_ms: elapsed_ms,
-                }
-            } else if stdout.contains("Proof verification failed")
-                || stderr.contains("FAILED")
-                || stderr.contains("error")
-            {
-                let err_excerpt: String = stdout
-                    .lines()
-                    .chain(stderr.lines())
+
+            // Discovered 2026-04-26 during the swarm-dogfood session:
+            // echidna's "Proof verified successfully" / "Proof verification
+            // failed" lines come from `OutputFormatter`, which writes to
+            // STDERR, not stdout. The previous stdout-only check made every
+            // attempt look "inconclusive" and demoted real failures to
+            // generic-failure anti-patterns. We now scan BOTH streams and
+            // also fall back on the exit code so a non-zero exit with no
+            // standard marker still becomes Failed (not Inconclusive).
+            let combined_lines: Vec<&str> =
+                stdout.lines().chain(stderr.lines()).collect();
+            let says_success = combined_lines
+                .iter()
+                .any(|l| l.contains("Proof verified successfully") || l.contains("✓ Proof verified"));
+            let says_failure = combined_lines.iter().any(|l| {
+                l.contains("Proof verification failed")
+                    || l.contains("✗ Proof verification failed")
+                    || l.contains("FAILED")
+            });
+            let exit_failed = !o.status.success();
+
+            if says_success {
+                AttemptResult::Succeeded { duration_ms: elapsed_ms }
+            } else if says_failure || exit_failed {
+                let err_excerpt: String = combined_lines
+                    .iter()
                     .filter(|l| {
-                        l.contains("***") || l.contains("Failed") || l.contains("error")
+                        l.contains("***")
+                            || l.contains("Failed")
+                            || l.contains("error")
+                            || l.contains("Unable")
                     })
                     .take(3)
+                    .copied()
                     .collect::<Vec<_>>()
                     .join(" | ");
                 AttemptResult::Failed {
                     error: if err_excerpt.is_empty() {
-                        "non-success exit; no diagnostic captured".to_string()
+                        format!(
+                            "exit {} — no standard diagnostic captured",
+                            o.status.code().unwrap_or(-1)
+                        )
                     } else {
                         err_excerpt
                     },
                     duration_ms: elapsed_ms,
                 }
             } else {
-                // Inconclusive — treat as failed with raw context.
+                // Truly inconclusive — exit 0, no markers either way.
                 AttemptResult::Failed {
-                    error: format!("inconclusive output (first 200 chars): {}",
-                                   stdout.chars().take(200).collect::<String>()),
+                    error: format!(
+                        "inconclusive output (no success/failure marker, exit 0): {}",
+                        stdout.chars().take(200).collect::<String>()
+                    ),
                     duration_ms: elapsed_ms,
                 }
             }
@@ -433,6 +480,8 @@ mod tests {
             echidna_path: PathBuf::from("/nonexistent/echidna"),
             timeout_secs: 5,
             workdir: None,
+            project_root: None,
+            sandbox: "none".to_string(),
         };
         let r = run_probe(probe, &cfg, "missing_test.thy");
         assert!(matches!(r, AttemptResult::Skipped { .. }));

crates/burrower-core/src/lib.rs

@@ -32,6 +32,8 @@ pub mod ranking;
 pub mod specialist;
 pub mod ledger;
 pub mod attempt;
+pub mod serve;
+pub mod oracle;
 
 pub use goal::{parse_goal, Goal};
 pub use corpus::{Corpus, IndexedLemma, LibraryKind};