From ca594382a3fa37bba5d9e5a1d6aee8182c06af96 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 09:51:51 +0000 Subject: [PATCH 1/2] =?UTF-8?q?ArghDA=20M7:=20Echidna=20dispatch=20seam=20?= =?UTF-8?q?=E2=80=94=20completes=20the=20engine-spine=20deliverable?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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=`. - `src/main.rs` — `--dispatch local|echidna[=]` 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 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/6a2/STATE.a2ml | 40 ++++++--- src/dispatch.rs | 138 +++++++++++++++++++++++++++++++ src/lib.rs | 2 + src/main.rs | 29 +++++-- 4 files changed, 192 insertions(+), 17 deletions(-) create mode 100644 src/dispatch.rs diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index b0a7616..c9cd696 100644 --- 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[=]` 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 new file mode 100644 index 0000000..ea1846c --- /dev/null +++ b/src/dispatch.rs @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! 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=`. + pub fn parse(s: &str) -> Result { + 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=)") + } + + /// 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 { + 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 index 55285b0..dbed3ab 100644 --- 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 index 6ef03ad..4c222ee 100644 --- 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[=]` + /// (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[=]`. + #[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,6 +241,7 @@ fn main() -> Result<()> { config, backend, check, + dispatch, } => reason( &path, &entry, @@ -239,6 +249,7 @@ fn main() -> Result<()> { 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); } From cbad28805a4b11c42471ab8453018e0ab220774d Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 09:59:45 +0000 Subject: [PATCH 2/2] ci: add estate-standard CodeQL workflow (unblocks code-scanning merge gate) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit arghda-core's `main` branch protection requires Code Scanning results, but the repo shipped no CodeQL workflow — so auto-merge waits forever ("Waiting for Code Scanning results. Code Scanning may not be configured for the target branch"). Earlier PRs only merged because the owner merged them manually; auto-merge enforces the gate strictly. Root cause: arghda-core was EXTRACTED from echo-types rather than instantiated from rsr-template-repo, so it never inherited the template's `codeql.yml`. This restores the canonical estate workflow verbatim (identical to rsr-template-repo + cicd-squabbler, which is green): - `language: actions`, `build-mode: none` — the estate default; scans the workflow files every repo has, avoiding the "no source files" failures that `rust`/`javascript-typescript` extractors produce (CodeQL's Rust support is limited). Per hypatia `codeql_language_matrix_mismatch`. - Triggers on `push: [main]` (establishes the code-scanning BASELINE on the target branch — the missing piece the error names) AND `pull_request` (produces results on every PR). SHA-pinned actions. Permanent fix: once this lands on `main`, the push-trigger run establishes the baseline and every future PR's code-scanning gate is satisfied automatically — no more manual-merge workaround. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .github/workflows/codeql.yml | 45 ++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 .github/workflows/codeql.yml diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml new file mode 100644 index 0000000..cdac17f --- /dev/null +++ b/.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 }}"