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

.github/workflows/codeql.yml

@@ -0,0 +1,45 @@
+# SPDX-License-Identifier: MPL-2.0
+name: CodeQL Security Analysis
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+    branches: [main, master]
+  schedule:
+    - cron: '0 6 1 * *'   # monthly 1st 06:00 UTC (Actions burn cut, standards#288)
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+permissions:
+  contents: read
+jobs:
+  analyze:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    permissions:
+      contents: read
+      security-events: write
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          # Default to `actions` — scaffolded repos rarely have JS/TS
+          # source; `javascript-typescript` produced "no source files"
+          # failures on every CodeQL run. The `actions` extractor scans
+          # workflow files which every repo has. Override per-repo if
+          # the scaffolded project actually contains JS/TS code.
+          # Per hypatia rule `codeql_language_matrix_mismatch`.
+          - language: actions
+            build-mode: none
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        with:
+          languages: ${{ matrix.language }}
+          build-mode: ${{ matrix.build-mode }}
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        with:
+          category: "/language:${{ matrix.language }}"

.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"]

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);
+    }
+}

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};

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);
             }