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