ArghDA M7: Echidna dispatch seam — completes the engine-spine deliverable

claude · claude · commit ca594382a3fa · 2026-07-01T09:51:51.000Z
The last piece of the engine-spine deliverable (M0-M7 + M11). A thin indirection so a backend's check can route locally or (in future) to the Echidna multi-prover orchestrator, returning the SAME Outcome contract. - `src/dispatch.rs` — `Dispatch { Local, Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome`. Local = fully real (delegates to `backend.check_file`). `Dispatch::parse` accepts `local` / `echidna` / `echidna=<url>`. - `src/main.rs` — `--dispatch local|echidna[=<url>]` wired on `check` and `reason --check`. ## Honest-stub discipline Echidna's orchestrator API is unconfirmed (it may not exist yet) and this seam explicitly does not block on it. Rather than invent an unverifiable HTTP contract and risk fabricating a verdict, the Echidna route returns `available: false` / `Unavailable` with a clear reason — never a made-up result (the same discipline as cicd-squabbler's "exits EX_UNAVAILABLE rather than fake OK"). The value delivered now is the *seam*: one indirection point with the Outcome contract preserved, so wiring the real (feature-gated) client later touches only `Dispatch::run` — no backend or caller changes. ## Verified (ran, not inferred) - `cargo test` → 124 passing, 0 failed (+3 dispatch unit: parse; echidna-never-fabricates; local-delegates). - clippy -D warnings, fmt, SPDX clean. - Dogfooded: `--dispatch local` z3 unsat → proven-eligible; `--dispatch echidna` → backend-unavailable (honest); `--dispatch bogus` → clean error. - STATE.a2ml: M7 = 70% (real orchestrator client is the follow-on); completion 92%, maturity beta. The engine-spine deliverable is complete. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -11,12 +11,12 @@ status = "active"  # active | paused | archived
 
 [project-context]
 name = "arghda-core"
-purpose = "Lightweight proof-workspace manager for Agda — the language-agnostic engine half of arghda. A four-state triage workspace (inbox/working/proven/rejected) as file moves, a lint pack targeting the silent-failure class, a first-class import-graph DAG, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. It never proves anything; Agda does."
-completion-percentage = 85
+purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Six backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4 assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do."
+completion-percentage = 92
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
-maturity = "alpha"         # experimental | alpha | beta | production | lts
+maturity = "beta"          # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
@@ -47,7 +47,7 @@ milestones = [
   { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 },
   { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 85 },
-  { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 },
+  { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 },
   { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 },
   { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 },
@@ -60,6 +60,22 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the
+# engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local,
+# Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome`
+# preserving the SAME Outcome contract on both routes. Local = fully real
+# (delegates to backend.check_file). Echidna = an HONEST STUB: Echidna's
+# orchestrator API is unconfirmed (may not exist), and the seam explicitly does
+# NOT block on it, so rather than invent an unverifiable HTTP contract and risk
+# fabricating a verdict, the Echidna route returns available:false / Unavailable
+# with a clear reason (mirrors cicd-squabbler's "exits EX_UNAVAILABLE rather than
+# fake OK" precedent). Wired via `--dispatch local|echidna[=<url>]` on `check`
+# and `reason --check`. 124 tests (+3 dispatch unit: parse; echidna-never-
+# fabricates; local-delegates). Dogfooded: local z3 unsat→proven-eligible;
+# echidna→backend-unavailable (honest); bogus→clean error. Follow-on (the 30%):
+# the real orchestrator HTTP client, feature-gated, once Echidna's API is
+# confirmed — only Dispatch::run changes (no backend/caller churn).
+#
 # M11 landed 2026-07-01: studio JSON freeze (reason/0.1) + Groove manifest —
 # closes the ONE open v0.1 milestone (Groove service manifest, was 0%). Two
 # deliverables. (1) Studio JSON freeze: a reason/0.1 JSON CONTRACT test in
@@ -200,12 +216,12 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M0-M6 + M11 DONE. The v0.1 spec is now CLOSED (Groove manifest was the last open milestone). Engine-spine deliverable (M0-M7 + M11) is complete bar M7. Six backends + reasoning graph + doctor + groove. Remaining:",
-  "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome) — completes the engine-spine deliverable.",
+  "ENGINE-SPINE DELIVERABLE COMPLETE: M0-M7 + M11 all landed. v0.1 spec closed. Six backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor + groove + dispatch seam. Remaining work is refinement + the heavy tail:",
+  "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.",
   "M6 follow-on: lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.",
   "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.",
   "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).",
-  "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.",
+  "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).",
 ]
 
 [maintenance-status]
@@ -214,11 +230,11 @@ last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 0
 open-failures = 0
 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green
-# post-M11: 88 lib + 33 integration = 121 tests pass. `arghda doctor`/`groove`
-# dogfooded: 6/6 backends runnable; manifest emits + writes /.well-known/groove.
-# All six backends dogfooded via real CLI: agda + agda-cubical + idris2 + lean4
-# (Assistant), z3 + cvc5 (Solver). Dogfooded historically vs echo-types +
-# agda-unused.
+# post-M7: 91 lib + 33 integration = 124 tests pass. doctor/groove/dispatch
+# dogfooded: 6/6 backends runnable; groove writes /.well-known/groove; --dispatch
+# local real, echidna honest-stub. All six backends dogfooded via real CLI: agda
+# + agda-cubical + idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded
+# historically vs echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]
diff --git a/src/dispatch.rs b/src/dispatch.rs
@@ -0,0 +1,138 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! The Echidna dispatch seam.
+//!
+//! A backend's `check_file` can run one of two ways, both returning the SAME
+//! [`Outcome`] contract:
+//! * [`Dispatch::Local`] — shell out to the tool directly (the default, and
+//!   the fully-real baseline).
+//! * [`Dispatch::Echidna`] — route to the Echidna multi-prover orchestrator
+//!   (Zig-API, port 8090) which runs the check elsewhere and returns the
+//!   verdict.
+//!
+//! **Honest-stub discipline.** Echidna's orchestrator repo/API is unconfirmed
+//! (it may not exist yet), and this seam explicitly *does not block on Echidna
+//! existing*. Rather than invent an unverifiable HTTP contract and risk
+//! fabricating a verdict, the Echidna route is an honest stub: it returns an
+//! [`Outcome`] with `available: false` / [`Verdict::Unavailable`] and a clear
+//! reason — never a made-up result. This mirrors the estate precedent
+//! (cicd-squabbler's webhook server "exits EX_UNAVAILABLE rather than fake
+//! OK"). Wiring the real orchestrator client (feature-gated) is the follow-on,
+//! gated on Echidna's confirmed API.
+//!
+//! The value delivered now is the *seam*: one indirection point where a route
+//! is chosen, with the `Outcome` contract preserved, so adding the real client
+//! later touches only [`Dispatch::run`] — no backend or caller changes.
+
+use crate::prover::{Backend, BackendKind, Outcome, Verdict};
+use anyhow::{bail, Result};
+use std::path::Path;
+
+/// How a check is dispatched.
+pub enum Dispatch {
+    /// Shell out to the tool locally (default; fully real).
+    Local,
+    /// Route to the Echidna orchestrator at `base_url` (honest stub for now).
+    Echidna { base_url: String },
+}
+
+impl Dispatch {
+    /// The conventional Echidna orchestrator endpoint.
+    pub const DEFAULT_ECHIDNA_URL: &'static str = "http://127.0.0.1:8090";
+
+    /// Parse a `--dispatch` value: `local` (default), `echidna`, or
+    /// `echidna=<url>`.
+    pub fn parse(s: &str) -> Result<Dispatch> {
+        if let Some((head, url)) = s.split_once('=') {
+            if head == "echidna" {
+                return Ok(Dispatch::Echidna {
+                    base_url: url.to_string(),
+                });
+            }
+        } else if s == "echidna" {
+            return Ok(Dispatch::Echidna {
+                base_url: Self::DEFAULT_ECHIDNA_URL.to_string(),
+            });
+        } else if s == "local" {
+            return Ok(Dispatch::Local);
+        }
+        bail!("unknown --dispatch `{s}` (known: local, echidna, echidna=<url>)")
+    }
+
+    /// Run `backend`'s check via the chosen route. The `Outcome` contract is
+    /// identical regardless of route.
+    pub fn run(&self, backend: &dyn Backend, file: &Path, include_root: &Path) -> Result<Outcome> {
+        match self {
+            Dispatch::Local => backend.check_file(file, include_root),
+            Dispatch::Echidna { base_url } => Ok(echidna_stub(backend.kind(), base_url)),
+        }
+    }
+}
+
+/// The honest Echidna stub: the seam is wired and returns the standard
+/// `Outcome` shape, but reports `Unavailable` with a reason instead of
+/// fabricating a verdict.
+fn echidna_stub(kind: BackendKind, base_url: &str) -> Outcome {
+    Outcome {
+        available: false,
+        exit_code: None,
+        ok: false,
+        output_tail: format!(
+            "echidna dispatch seam is wired ({base_url}) but the orchestrator \
+             client is not built in this configuration; no verdict fabricated"
+        ),
+        kind,
+        verdict: Verdict::Unavailable,
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::prover::{Agda, Smt};
+
+    #[test]
+    fn parse_dispatch_values() {
+        assert!(matches!(Dispatch::parse("local").unwrap(), Dispatch::Local));
+        match Dispatch::parse("echidna").unwrap() {
+            Dispatch::Echidna { base_url } => assert_eq!(base_url, Dispatch::DEFAULT_ECHIDNA_URL),
+            _ => panic!("expected echidna"),
+        }
+        match Dispatch::parse("echidna=http://host:9000").unwrap() {
+            Dispatch::Echidna { base_url } => assert_eq!(base_url, "http://host:9000"),
+            _ => panic!("expected echidna with url"),
+        }
+        assert!(Dispatch::parse("nonsense").is_err());
+    }
+
+    #[test]
+    fn echidna_route_is_an_honest_stub_never_fabricates() {
+        // The seam preserves the backend's kind but reports Unavailable with
+        // a reason — it must never claim Proven/Refuted it did not obtain.
+        let d = Dispatch::parse("echidna").unwrap();
+        let tmp = tempfile::tempdir().unwrap();
+        let f = tmp.path().join("q.smt2");
+        std::fs::write(&f, "(check-sat)\n").unwrap();
+        let out = d.run(&Smt::z3(), &f, tmp.path()).unwrap();
+        assert_eq!(out.verdict, Verdict::Unavailable);
+        assert!(!out.available);
+        assert_eq!(out.kind, BackendKind::Solver, "kind is preserved");
+        assert!(out.output_tail.contains("echidna"));
+        assert!(out.output_tail.contains("no verdict fabricated"));
+    }
+
+    #[test]
+    fn local_route_delegates_to_the_backend() {
+        // Local dispatch is exactly backend.check_file — same honesty either
+        // way (present ⇒ real verdict; absent ⇒ Unavailable).
+        let d = Dispatch::Local;
+        let tmp = tempfile::tempdir().unwrap();
+        let f = tmp.path().join("X.agda");
+        std::fs::write(&f, "module X where\n").unwrap();
+        let via_dispatch = d.run(&Agda, &f, tmp.path()).unwrap();
+        let direct = Agda.check_file(&f, tmp.path()).unwrap();
+        assert_eq!(via_dispatch.available, direct.available);
+        assert_eq!(via_dispatch.verdict, direct.verdict);
+    }
+}
diff --git a/src/lib.rs b/src/lib.rs
@@ -13,6 +13,7 @@
 pub mod config;
 pub mod dag;
 pub mod diagnostic;
+pub mod dispatch;
 pub mod event;
 pub mod graph;
 pub mod groove;
@@ -28,6 +29,7 @@ pub mod workspace;
 
 pub use dag::{build as build_dag, DagDocument};
 pub use diagnostic::{Diagnostic, LintReport, Severity};
+pub use dispatch::Dispatch;
 pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use groove::{manifest as groove_manifest, GrooveManifest};
diff --git a/src/main.rs b/src/main.rs
@@ -5,7 +5,7 @@ use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
     build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical,
-    Backend, BackendKind, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict,
+    Backend, BackendKind, Dispatch, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict,
     Workspace,
 };
 use clap::{Parser, Subcommand};
@@ -90,6 +90,10 @@ enum Cmd {
         /// `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
+        /// Where the check runs: `local` (default) or `echidna[=<url>]`
+        /// (route to the Echidna orchestrator).
+        #[arg(long, default_value = "local")]
+        dispatch: String,
         /// Emit the report as JSON.
         #[arg(long)]
         json: bool,
@@ -143,6 +147,10 @@ enum Cmd {
         /// default, in which case clean nodes are `unknown`.
         #[arg(long)]
         check: bool,
+        /// With `--check`, where each check runs: `local` (default) or
+        /// `echidna[=<url>]`.
+        #[arg(long, default_value = "local")]
+        dispatch: String,
     },
     /// Claim a file: inbox -> working.
     Claim { workspace: PathBuf, file: String },
@@ -210,8 +218,9 @@ fn main() -> Result<()> {
             file,
             include_root,
             backend,
+            dispatch,
             json,
-        } => check(&file, include_root.as_deref(), &backend, json)?,
+        } => check(&file, include_root.as_deref(), &backend, &dispatch, json)?,
         Cmd::Dag {
             path,
             entry,
@@ -232,13 +241,15 @@ fn main() -> Result<()> {
             config,
             backend,
             check,
+            dispatch,
         } => reason(
             &path,
             &entry,
             headline_pattern.as_deref(),
             config.as_deref(),
             &backend,
             check,
+            &dispatch,
         )?,
         Cmd::Claim { workspace, file } => {
             transition(&workspace, &file, State::Inbox, State::Working)?
@@ -419,7 +430,13 @@ fn scan(
     Ok(())
 }
 
-fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: bool) -> Result<()> {
+fn check(
+    file: &Path,
+    include_root: Option<&Path>,
+    backend_name: &str,
+    dispatch: &str,
+    json: bool,
+) -> Result<()> {
     if !file.is_file() {
         anyhow::bail!("file not found: {}", file.display());
     }
@@ -443,7 +460,7 @@ fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: boo
     };
     let report =
         run_lints(file, &ctx, &rules).with_context(|| format!("linting {}", file.display()))?;
-    let outcome = backend.check_file(file, include_root)?;
+    let outcome = Dispatch::parse(dispatch)?.run(backend.as_ref(), file, include_root)?;
 
     // Honest verdict: a lint hard-block rejects; otherwise report the
     // backend's ACTUAL verdict word. Only `Proven` (with no hard block) is
@@ -532,6 +549,7 @@ fn reason(
     config: Option<&Path>,
     backend_name: &str,
     do_check: bool,
+    dispatch: &str,
 ) -> Result<()> {
     let backend = backend_for(backend_name)?;
     let (roots, rules, cfg) = resolve_roots_and_rules(
@@ -556,9 +574,10 @@ fn reason(
     let mut verdicts = std::collections::BTreeMap::new();
     let stale = std::collections::BTreeSet::new();
     if do_check {
+        let route = Dispatch::parse(dispatch)?;
         for node in &dag_doc.nodes {
             let file = include_root.join(&node.file);
-            let outcome = backend.check_file(&file, include_root)?;
+            let outcome = route.run(backend.as_ref(), &file, include_root)?;
             if outcome.available {
                 verdicts.insert(node.id.clone(), outcome.verdict);
             }
