From 203fc00b767a50b87ddca67c15314cb353fd4309 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 06:54:51 +0000 Subject: [PATCH] =?UTF-8?q?ArghDA=20M1:=20Backend=20abstraction=20?= =?UTF-8?q?=E2=80=94=20make=20the=20engine=20prover-parametric?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The keystone refactor of the "Flying Logic for provers/solvers" epic. Every Agda-baked seam now lives behind an object-safe `Backend` trait, so the four-state workspace, DAG builder, content-hash invalidation and the cycle-safe reachability walk are backend-neutral. Agda is the first (v0.1 reference) impl; adding Idris2/Lean4/Z3/CVC5/… now means an impl, not a rewrite. Behaviour is unchanged — this is the promised pure refactor with the test suite as the oracle: the 64 pre-existing tests (50 lib + 14 integration) all stay green, +2 new Agda-backend tests = 66 passing. clippy -D warnings, fmt and the SPDX gate are clean; the `dag` JSON output is byte-compatible and `check` still runs a real Agda typecheck. New `src/prover/`: - `Backend` trait: name/kind/extensions/safe_mode/check_file + module_name_of/module_to_path/direct_imports/discover_roots/lint_rules. - `BackendKind { Assistant, Solver }` — the two interaction models. - `Verdict { Proven, Refuted, Unknown, Admitted, Postulated, Error, Unavailable }` — the common verdict both models map into; only Proven is green, Admitted/Postulated are amber. - `Outcome` — superset of the old AgdaOutcome (raw process facts + kind + verdict). - `src/agda.rs` -> `src/prover/agda.rs` (Agda impl; owns the shell-out, delegates parsing to `graph::` free fns and the lint pack to `lint::`). Verdict is exit-code-only (0 -> Proven, ran-nonzero -> Error, absent -> Unavailable) — arghda never claims a result Agda did not return; Admitted/Postulated stay lint-derived, not manufactured from a green exit. - `graph::build` and `dag::build` gain a `&dyn Backend` parameter and use the backend's extension filter + import parsing; the reachability walk and its cycle-termination regression are untouched. - `main.rs` scan/check/dag/resolve_roots_and_rules route through the backend; the `check` JSON key `agda` -> `backend` (now carries kind + verdict). - STATE.a2ml records M1 = 100%. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .gitignore | 3 + .machine_readable/6a2/STATE.a2ml | 34 +++++-- src/agda.rs | 84 ----------------- src/dag.rs | 11 ++- src/graph.rs | 25 +++-- src/lib.rs | 14 ++- src/main.rs | 61 ++++++++---- src/prover/agda.rs | 143 ++++++++++++++++++++++++++++ src/prover/mod.rs | 157 +++++++++++++++++++++++++++++++ tests/dag.rs | 29 +++++- 10 files changed, 428 insertions(+), 133 deletions(-) delete mode 100644 src/agda.rs create mode 100644 src/prover/agda.rs create mode 100644 src/prover/mod.rs diff --git a/.gitignore b/.gitignore index b733efa..67f1b67 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,6 @@ dist-newstyle/ .direnv/ result result-* + +# Agda compiled interface files (generated by typecheck runs) +*.agdai diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 2393c32..b6bc9a7 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -41,7 +41,7 @@ milestones = [ [route-to-flying-logic] milestones = [ { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes", completion = 80 }, - { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 0 }, + { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 }, { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 }, { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 0 }, { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 }, @@ -59,6 +59,21 @@ milestones = [ # are scripted (behind --heavy/--mizar) but not installed this session. # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). +# +# M1 landed 2026-07-01 as the promised PURE REFACTOR — behaviour unchanged, +# oracle held: the 64 pre-existing tests (50 lib + 14 integration) all stay +# green, +2 new Agda-backend tests = 66 passing; clippy -D warnings + fmt + +# SPDX all clean; `dag` JSON output byte-compatible. New src/prover/ module: +# Backend trait (name/kind/extensions/safe_mode/check_file/module_name_of/ +# module_to_path/direct_imports/discover_roots/lint_rules), BackendKind +# {Assistant|Solver}, Verdict {Proven|Refuted|Unknown|Admitted|Postulated| +# Error|Unavailable}, Outcome (superset of the old AgdaOutcome + kind + +# verdict). src/agda.rs -> src/prover/agda.rs (Agda = first impl; owns the +# shell-out, delegates parsing to graph:: free fns + lint pack to lint::). +# graph::build + dag::build + main's scan/check/dag/resolve_roots_and_rules +# all consume &dyn Backend; the cycle-safe reachability walk is untouched and +# inherited free. Agda verdict is exit-code-only (0 -> Proven, ran-nonzero -> +# Error, absent -> Unavailable); Admitted/Postulated stay lint-derived amber. [blockers-and-issues] # No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are @@ -72,21 +87,24 @@ milestones = [ [critical-next-actions] actions = [ - "Flying-Logic epic M1: introduce the Backend trait (Assistant|Solver) and move agda.rs to prover/agda.rs as a PURE REFACTOR — the 50 existing tests are the oracle, they must stay green with no behaviour change. This is the keystone everything else rides on.", - "Flying-Logic epic M3: src/reason reasoning graph (And|Or juncts + demote-only cycle-safe Verdict propagation) — independent of new backends, lands the headline capability early.", + "M1 keystone DONE (Backend trait, pure refactor, 66 tests green). Next, in parallel now that the trait is stable:", + "Flying-Logic epic M3: src/reason reasoning graph (And|Or juncts + demote-only cycle-safe Verdict propagation over the common Verdict) — independent of new backends, lands the headline capability early.", + "Flying-Logic epic M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; believe_me/assert_total/%partial escape-hatches) — Idris2 v0.7.0 is provisioned.", + "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the Solver kind; SMT-LIB2 -> sat(Refuted)/unsat(Proven)/unknown(Unknown). Both binaries are provisioned.", + "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden).", "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).", - "Transitive-import closure hashing landed; follow-up: expose it as a --include-root CLI flag on promote/stale.", "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.", ] [maintenance-status] -last-run-utc = "2026-06-20" +last-run-utc = "2026-07-01" last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 -# `just check` (fmt-check + clippy -D warnings + build + test) green; ~50 lib -# tests + integration suites pass. Dogfooded against echo-types + a live -# agda-unused build. +# `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green +# post-M1: 52 lib + 14 integration = 66 tests pass. `dag`/`check` dogfooded +# via real CLI runs (dag JSON byte-compatible; check ran a real agda typecheck +# -> proven-eligible). Dogfooded historically against echo-types + agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/src/agda.rs b/src/agda.rs deleted file mode 100644 index ee65ad2..0000000 --- a/src/agda.rs +++ /dev/null @@ -1,84 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -//! Shelling out to `agda` to typecheck a file. -//! -//! ArghDA never proves anything itself — it asks Agda. This module runs -//! the typechecker and captures the verdict. If `agda` is not on `PATH` -//! it degrades gracefully (`available: false`) rather than erroring, so -//! the rest of the engine still works in an Agda-less environment (CI -//! linting, DAG extraction, triage moves). - -use anyhow::Result; -use serde::Serialize; -use std::path::Path; -use std::process::Command; - -const TAIL_LINES: usize = 40; - -/// Result of a typecheck attempt. -#[derive(Clone, Debug, Serialize)] -pub struct AgdaOutcome { - /// Whether the `agda` binary was found and executed. - pub available: bool, - /// Process exit code, if the process ran. - pub exit_code: Option, - /// `true` iff agda exited 0. - pub ok: bool, - /// Last few lines of combined stdout+stderr (for surfacing errors). - pub output_tail: String, -} - -impl AgdaOutcome { - fn unavailable() -> Self { - Self { - available: false, - exit_code: None, - ok: false, - output_tail: String::new(), - } - } -} - -/// Typecheck `file` with `include_root` on the search path -/// (`agda -i `). -pub fn check_file(file: &Path, include_root: &Path) -> Result { - let output = Command::new("agda") - .arg("-i") - .arg(include_root) - .arg(file) - .output(); - - match output { - Ok(out) => { - let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); - combined.push_str(&String::from_utf8_lossy(&out.stderr)); - Ok(AgdaOutcome { - available: true, - exit_code: out.status.code(), - ok: out.status.success(), - output_tail: tail(&combined, TAIL_LINES), - }) - } - Err(e) if e.kind() == std::io::ErrorKind::NotFound => Ok(AgdaOutcome::unavailable()), - Err(e) => Err(e.into()), - } -} - -fn tail(s: &str, n: usize) -> String { - let lines: Vec<&str> = s.lines().collect(); - let start = lines.len().saturating_sub(n); - lines[start..].join("\n") -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn tail_keeps_last_n_lines() { - assert_eq!(tail("a\nb\nc\nd", 2), "c\nd"); - assert_eq!(tail("only", 5), "only"); - assert_eq!(tail("", 3), ""); - } -} diff --git a/src/dag.rs b/src/dag.rs index 8c7a210..d5e90d3 100644 --- a/src/dag.rs +++ b/src/dag.rs @@ -13,6 +13,7 @@ use crate::diagnostic::Severity; use crate::graph::{self, Edge}; use crate::lint::{run_lints, unpinned_headline, LintContext, LintRule}; +use crate::prover::Backend; use crate::timestamp::now_rfc3339; use anyhow::{Context, Result}; use regex::Regex; @@ -61,18 +62,20 @@ pub struct DagDocument { } /// Build the DAG document for the source tree at `include_root`, using -/// `entry_modules` (the union of CI roots) for the orphan-reachability rule, -/// `rules` as the lint pack, and `headline_pattern` (the same regex the -/// `unpinned-headline` rule uses) to populate each node's `headlines` array. +/// `backend` for the per-language import graph, `entry_modules` (the union +/// of CI roots) for the orphan-reachability rule, `rules` as the lint pack, +/// and `headline_pattern` (the same regex the `unpinned-headline` rule +/// uses) to populate each node's `headlines` array. pub fn build( include_root: &Path, entry_modules: &[PathBuf], rules: &[Box], headline_pattern: &str, + backend: &dyn Backend, ) -> Result { let headline_matcher = Regex::new(headline_pattern) .with_context(|| format!("compiling headline pattern `{headline_pattern}`"))?; - let graph = graph::build(include_root)?; + let graph = graph::build(include_root, backend)?; let ctx = LintContext { include_root, entry_modules, diff --git a/src/graph.rs b/src/graph.rs index a0a7869..fa5929f 100644 --- a/src/graph.rs +++ b/src/graph.rs @@ -14,6 +14,7 @@ //! include root: the graph is the project's internal dependency DAG, so //! stdlib / external imports are intentionally omitted. +use crate::prover::Backend; use anyhow::{Context, Result}; use serde::Serialize; use std::collections::{BTreeMap, HashSet}; @@ -177,10 +178,14 @@ pub struct ImportGraph { pub edges: Vec, } -/// Walk every `.agda` file under `include_root` and build the internal -/// import graph. Output is deterministic (nodes and edges are sorted), -/// which keeps the emitted DAG stable for diffing and tests. -pub fn build(include_root: &Path) -> Result { +/// Walk every source file the `backend` claims (by extension) under +/// `include_root` and build the internal import graph, using the backend's +/// per-language module-name / import parsing. Output is deterministic +/// (nodes and edges are sorted), which keeps the emitted DAG stable for +/// diffing and tests. A solver backend with no import notion yields an +/// edge-free set of isolated nodes, which is valid. +pub fn build(include_root: &Path, backend: &dyn Backend) -> Result { + let exts = backend.extensions(); // module id -> relative file path, for every in-tree module. let mut by_id: BTreeMap = BTreeMap::new(); for entry in WalkDir::new(include_root) @@ -188,10 +193,14 @@ pub fn build(include_root: &Path) -> Result { .filter_map(|e| e.ok()) { let path = entry.path(); - if path.extension().and_then(|s| s.to_str()) != Some("agda") { + let is_source = path + .extension() + .and_then(|s| s.to_str()) + .is_some_and(|e| exts.contains(&e)); + if !is_source { continue; } - if let Some(id) = module_name_of(path, include_root) { + if let Some(id) = backend.module_name_of(path, include_root) { let rel = path .strip_prefix(include_root) .unwrap_or(path) @@ -210,8 +219,8 @@ pub fn build(include_root: &Path) -> Result { let mut edges = Vec::new(); for id in by_id.keys() { - let path = module_to_path(id, include_root); - for imp in direct_imports(&path)? { + let path = backend.module_to_path(id, include_root); + for imp in backend.direct_imports(&path)? { // Keep only edges to modules that exist in-tree. if by_id.contains_key(&imp) { edges.push(Edge { diff --git a/src/lib.rs b/src/lib.rs index 7e0a8ee..be22bfa 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,12 +1,15 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -//! arghda-core: proof-workspace manager for Agda. +//! arghda-core: proof-workspace manager for provers and solvers. //! -//! Public surface is intentionally small: `Workspace`, the lint traits, -//! and the diagnostic types. The CLI in `main.rs` is a thin consumer. +//! Agda is the first (v0.1 reference) backend; every prover-specific seam +//! lives behind the [`prover::Backend`] trait, so the four-state workspace, +//! DAG builder and content-hash invalidation are backend-neutral. Public +//! surface is intentionally small: `Workspace`, the `Backend` trait, the +//! lint traits, and the diagnostic types. The CLI in `main.rs` is a thin +//! consumer. -pub mod agda; pub mod config; pub mod dag; pub mod diagnostic; @@ -15,15 +18,16 @@ pub mod graph; pub mod hash; pub mod lint; pub mod proven; +pub mod prover; pub mod timestamp; pub mod unused; pub mod watcher; pub mod workspace; -pub use agda::{check_file, AgdaOutcome}; pub use dag::{build as build_dag, DagDocument}; pub use diagnostic::{Diagnostic, LintReport, Severity}; pub use event::{Event, EventKind}; pub use graph::{build as build_graph, ImportGraph}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; +pub use prover::{default_backend, Agda, Backend, BackendKind, Outcome, Verdict}; pub use workspace::{StaleEntry, State, Workspace}; diff --git a/src/main.rs b/src/main.rs index 3d6f803..2a83a58 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,8 +4,8 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ - build_dag, check_file, default_rules, event, graph, rules_with_config, run_lints, unused, - watcher, LintRule, RuleConfig, State, Workspace, + build_dag, event, run_lints, unused, watcher, Agda, Backend, LintRule, RuleConfig, State, + Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -177,12 +177,14 @@ fn scan( unused: bool, json: bool, ) -> Result<()> { + let backend = Agda; let (roots, rules, _cfg) = - resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; + resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?; let ctx = LintContext { include_root, entry_modules: &roots, }; + let exts = backend.extensions(); let mut reports = Vec::new(); for entry in WalkDir::new(include_root) @@ -190,7 +192,11 @@ fn scan( .filter_map(|e| e.ok()) { let path = entry.path(); - if path.extension().and_then(|s| s.to_str()) != Some("agda") { + let is_source = path + .extension() + .and_then(|s| s.to_str()) + .is_some_and(|e| exts.contains(&e)); + if !is_source { continue; } let report = @@ -274,7 +280,8 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { // The orphan rule self-skips when the file is its own root, which is // exactly what a single-file check wants. - let rules = default_rules(); + let backend = Agda; + let rules = backend.lint_rules(&RuleConfig::default())?; let roots = [file.to_path_buf()]; let ctx = LintContext { include_root, @@ -282,11 +289,11 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { }; let report = run_lints(file, &ctx, &rules).with_context(|| format!("linting {}", file.display()))?; - let agda = check_file(file, include_root)?; + let outcome = backend.check_file(file, include_root)?; - let verdict = if !agda.available { - "agda-unavailable" - } else if agda.ok && !report.has_hard_block() { + let verdict = if !outcome.available { + "backend-unavailable" + } else if outcome.ok && !report.has_hard_block() { "proven-eligible" } else { "rejected" @@ -296,23 +303,28 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { let payload = serde_json::json!({ "version": "0.1", "file": file, - "agda": agda, + "backend": outcome, "lint": report, "verdict": verdict, }); println!("{}", serde_json::to_string_pretty(&payload)?); } else { println!("{}", file.display()); - if agda.available { + if outcome.available { println!( - " agda: exit {}, {}", - agda.exit_code + " {}: exit {}, {}", + backend.name(), + outcome + .exit_code .map(|c| c.to_string()) .unwrap_or_else(|| "?".into()), - if agda.ok { "ok" } else { "FAILED" } + if outcome.ok { "ok" } else { "FAILED" } ); } else { - println!(" agda: not found on PATH (typecheck skipped)"); + println!( + " {}: not found on PATH (typecheck skipped)", + backend.name() + ); } for d in &report.diagnostics { println!(" [{}] {}: {}", sev_tag(d.severity), d.rule, d.message); @@ -328,9 +340,16 @@ fn dag( headline_pattern: Option<&str>, config: Option<&Path>, ) -> Result<()> { + let backend = Agda; let (roots, rules, cfg) = - resolve_roots_and_rules(include_root, entry, headline_pattern, config)?; - let doc = build_dag(include_root, &roots, &rules, &cfg.headline_pattern)?; + resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?; + let doc = build_dag( + include_root, + &roots, + &rules, + &cfg.headline_pattern, + &backend, + )?; println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) } @@ -369,6 +388,7 @@ fn resolve_roots_and_rules( entry: &[PathBuf], headline_pattern: Option<&str>, config: Option<&Path>, + backend: &dyn Backend, ) -> Result<(Vec, RuleSet, RuleConfig)> { for e in entry { if !e.is_file() { @@ -376,7 +396,7 @@ fn resolve_roots_and_rules( } } let roots = if entry.is_empty() { - graph::discover_roots(include_root) + backend.discover_roots(include_root) } else { entry.to_vec() }; @@ -386,12 +406,13 @@ fn resolve_roots_and_rules( "note: no root modules (All.agda/Smoke.agda) found under {}; skipping orphan-module rule", include_root.display() ); - rules_with_config(&cfg)? + backend + .lint_rules(&cfg)? .into_iter() .filter(|r| r.name() != "orphan-module") .collect() } else { - rules_with_config(&cfg)? + backend.lint_rules(&cfg)? }; Ok((roots, rules, cfg)) } diff --git a/src/prover/agda.rs b/src/prover/agda.rs new file mode 100644 index 0000000..22f23a5 --- /dev/null +++ b/src/prover/agda.rs @@ -0,0 +1,143 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Agda backend — arghda's first (and v0.1 reference) [`Backend`]. +//! +//! Owns the `agda` shell-out; delegates import-graph parsing to the +//! Agda-specific free functions in [`crate::graph`] and the lint pack to +//! [`crate::lint`]. Assistant model: `agda -i `; exit 0 → +//! [`Verdict::Proven`], a run that errors → [`Verdict::Error`], an absent +//! binary → [`Verdict::Unavailable`]. Exit-code only — arghda never claims +//! a result Agda did not return. `Admitted`/`Postulated` are amber overlays +//! surfaced by the lint pack (they are not process facts), so `check_file` +//! deliberately does not manufacture them from a green exit. + +use super::{Backend, BackendKind, Outcome, Verdict}; +use crate::graph; +use crate::lint::{rules_with_config, LintRule, RuleConfig}; +use anyhow::Result; +use std::path::{Path, PathBuf}; +use std::process::Command; + +const TAIL_LINES: usize = 40; + +/// The Agda proof assistant. +#[derive(Clone, Copy, Debug, Default)] +pub struct Agda; + +impl Backend for Agda { + fn name(&self) -> &'static str { + "agda" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["agda"] + } + + fn safe_mode(&self) -> Option<&'static str> { + Some("--safe --without-K") + } + + /// Typecheck `file` with `include_root` on the search path + /// (`agda -i `). + fn check_file(&self, file: &Path, include_root: &Path) -> Result { + let output = Command::new("agda") + .arg("-i") + .arg(include_root) + .arg(file) + .output(); + + match output { + Ok(out) => { + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); + combined.push_str(&String::from_utf8_lossy(&out.stderr)); + let ok = out.status.success(); + Ok(Outcome { + available: true, + exit_code: out.status.code(), + ok, + output_tail: tail(&combined, TAIL_LINES), + kind: BackendKind::Assistant, + // Exit-code only: 0 is the sole signal Agda gives that + // means "typechecked". Admitted/Postulated are + // lint-derived overlays, not process facts. + verdict: if ok { Verdict::Proven } else { Verdict::Error }, + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { + Ok(Outcome::unavailable(BackendKind::Assistant)) + } + Err(e) => Err(e.into()), + } + } + + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option { + graph::module_name_of(file, include_root) + } + + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf { + graph::module_to_path(module, include_root) + } + + fn direct_imports(&self, file: &Path) -> Result> { + graph::direct_imports(file) + } + + fn discover_roots(&self, include_root: &Path) -> Vec { + graph::discover_roots(include_root) + } + + fn lint_rules(&self, cfg: &RuleConfig) -> Result>> { + rules_with_config(cfg) + } +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn tail_keeps_last_n_lines() { + assert_eq!(tail("a\nb\nc\nd", 2), "c\nd"); + assert_eq!(tail("only", 5), "only"); + assert_eq!(tail("", 3), ""); + } + + #[test] + fn agda_backend_identity() { + assert_eq!(Agda.name(), "agda"); + assert_eq!(Agda.kind(), BackendKind::Assistant); + assert_eq!(Agda.extensions(), &["agda"]); + assert_eq!(Agda.safe_mode(), Some("--safe --without-K")); + } + + #[test] + fn check_file_is_honest_about_availability() { + // We cannot guarantee agda is absent in every environment, so we + // assert the honesty invariant either way: absent ⇒ the graceful + // `Unavailable` form (never an Err); present ⇒ the verdict is + // strictly exit-code-derived, never fabricated. + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("X.agda"); + std::fs::write(&f, "module X where\n").unwrap(); + let out = Agda.check_file(&f, tmp.path()).unwrap(); + if out.available { + assert!(matches!(out.verdict, Verdict::Proven | Verdict::Error)); + assert_eq!(out.ok, out.verdict == Verdict::Proven); + } else { + assert_eq!(out.verdict, Verdict::Unavailable); + assert!(!out.ok); + assert!(out.exit_code.is_none()); + } + } +} diff --git a/src/prover/mod.rs b/src/prover/mod.rs new file mode 100644 index 0000000..13cb0ac --- /dev/null +++ b/src/prover/mod.rs @@ -0,0 +1,157 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Prover/solver backend abstraction — the seam that makes arghda +//! prover-parametric. +//! +//! ArghDA never proves anything itself; a [`Backend`] is a thin, honest +//! adapter over an external tool. Two interaction models are unified here: +//! *assistants* (typecheck a file → exit code is the verdict) and *solvers* +//! (feed a query → parse `sat`/`unsat`/`unknown`). Both map their real, +//! observed result into a common [`Verdict`]. +//! +//! Hard rule (owner directive + AGENTIC.a2ml): a backend NEVER reports a +//! verdict the tool did not emit. [`Backend::check_file`] derives its +//! verdict from the actual exit code / parsed output, and degrades to +//! [`Verdict::Unavailable`] when the tool is absent rather than pretending +//! success. This is the module boundary where that honesty is enforced. +//! +//! Everything backend-neutral — the four-state machine (`workspace`), the +//! DAG builder (`dag`), content-hash invalidation (`proven`), and the +//! cycle-safe reachability walk (`graph::transitive_imports`) — consumes +//! `&dyn Backend` and inherits cycle safety for free. + +use crate::lint::{LintRule, RuleConfig}; +use anyhow::Result; +use serde::Serialize; +use std::path::{Path, PathBuf}; + +pub mod agda; + +pub use agda::Agda; + +/// The two backend interaction models. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] +#[serde(rename_all = "lowercase")] +pub enum BackendKind { + /// A proof assistant: typecheck a source file; the exit code is the + /// verdict (Agda, Idris2, Lean4, Coq/Rocq, Isabelle, Mizar). + Assistant, + /// A solver: feed a query and parse `sat`/`unsat`/`unknown` (Z3, CVC5). + Solver, +} + +/// The common verdict both interaction models map into. +/// +/// Only [`Verdict::Proven`] is "green". `Admitted`/`Postulated` are amber — +/// a goal *stated* but not discharged — and must never be counted as proof +/// (this is exactly the silent-failure class the linter and the estate's +/// proof-drift work name). `Refuted`/`Unknown` are the solver outcomes. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] +#[serde(rename_all = "kebab-case")] +pub enum Verdict { + /// Assistant exited 0, or solver returned `unsat` (VC discharged). + Proven, + /// Solver returned `sat` — a counterexample/model exists. + Refuted, + /// Solver returned `unknown`, or the run timed out. + Unknown, + /// The tool ran, but the artefact contains an admitted goal. + Admitted, + /// The tool ran, but the artefact contains a postulate/axiom. + Postulated, + /// The tool ran and errored (type error, parse error, …). + Error, + /// The tool was not found / could not be executed. + Unavailable, +} + +/// The result of a [`Backend::check_file`] invocation. +/// +/// A superset of the old `AgdaOutcome`: it keeps the raw process facts +/// (`available`, `exit_code`, `ok`, `output_tail`) and adds the backend +/// `kind` plus the mapped [`Verdict`], so a caller sees both what the tool +/// literally did and how arghda classifies it. +#[derive(Clone, Debug, Serialize)] +pub struct Outcome { + /// Whether the tool binary was found and executed. + pub available: bool, + /// Process exit code, if the process ran. + pub exit_code: Option, + /// `true` iff the tool exited 0 (assistant) / returned `unsat` (solver). + pub ok: bool, + /// Last few lines of combined stdout+stderr (for surfacing errors). + pub output_tail: String, + /// Which interaction model produced this outcome. + pub kind: BackendKind, + /// The verdict derived *only* from the tool's actual output. + pub verdict: Verdict, +} + +impl Outcome { + /// The tool was not found on `PATH`; the graceful-degradation form. + pub fn unavailable(kind: BackendKind) -> Self { + Self { + available: false, + exit_code: None, + ok: false, + output_tail: String::new(), + kind, + verdict: Verdict::Unavailable, + } + } +} + +/// An object-safe adapter over one external prover or solver. +/// +/// Exactly the seams that used to be hardcoded to Agda live behind this +/// trait: invocation ([`Backend::check_file`]), the import-graph trio +/// ([`Backend::module_name_of`] / [`Backend::module_to_path`] / +/// [`Backend::direct_imports`]), root discovery +/// ([`Backend::discover_roots`]), and the per-language lint pack +/// ([`Backend::lint_rules`]). Solvers legitimately return empty imports and +/// no roots — isolated DAG nodes are valid. +pub trait Backend: Send + Sync { + /// Stable identifier (`"agda"`, `"idris2"`, `"z3"`, …). + fn name(&self) -> &'static str; + + /// Assistant or solver. + fn kind(&self) -> BackendKind; + + /// Source-file extensions this backend claims, without the dot + /// (`["agda"]`, `["smt2"]`). + fn extensions(&self) -> &'static [&'static str]; + + /// The tool's safe/total mode flag, if any (for `doctor` / display). + fn safe_mode(&self) -> Option<&'static str> { + None + } + + /// Run the tool on `file` and return its *actual* verdict. Must degrade + /// to [`Outcome::unavailable`] when the tool is absent rather than + /// erroring, so the rest of the engine still works tool-less. + fn check_file(&self, file: &Path, include_root: &Path) -> Result; + + /// Dotted module name for `file` under `include_root` + /// (`Ordinal/Closure.agda` → `Ordinal.Closure`). `None` if unresolvable. + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option; + + /// Inverse of [`Backend::module_name_of`]. + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf; + + /// The modules `file` imports. In-tree resolution is the caller's job; + /// a solver with no import notion returns an empty vec. + fn direct_imports(&self, file: &Path) -> Result>; + + /// Conventional CI entry modules under `include_root` (e.g. Agda's + /// `All.agda` / `Smoke.agda`). May be empty. + fn discover_roots(&self, include_root: &Path) -> Vec; + + /// The per-language lint pack, parameterised by operator config. + fn lint_rules(&self, cfg: &RuleConfig) -> Result>>; +} + +/// The default backend when none is selected: Agda, the v0.1 language. +pub fn default_backend() -> Box { + Box::new(Agda) +} diff --git a/tests/dag.rs b/tests/dag.rs index e227172..ef79153 100644 --- a/tests/dag.rs +++ b/tests/dag.rs @@ -4,7 +4,7 @@ //! `dag` document construction over the fixtures. use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; -use arghda_core::{build_dag, default_rules}; +use arghda_core::{build_dag, default_rules, Agda}; use std::path::PathBuf; fn fixture(name: &str) -> PathBuf { @@ -19,7 +19,14 @@ fn fixture(name: &str) -> PathBuf { fn dag_over_orphan_fixture_has_expected_shape() { let root = fixture("orphan"); let roots = [root.join("All.agda")]; - let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); + let doc = build_dag( + &root, + &roots, + &default_rules(), + DEFAULT_HEADLINE_PATTERN, + &Agda, + ) + .unwrap(); // Nodes are deterministic and sorted by module id. let ids: Vec<&str> = doc.nodes.iter().map(|n| n.id.as_str()).collect(); @@ -57,7 +64,14 @@ fn dag_over_orphan_fixture_has_expected_shape() { fn dag_over_wellformed_fixture_is_all_clean() { let root = fixture("wellformed"); let roots = [root.join("All.agda")]; - let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); + let doc = build_dag( + &root, + &roots, + &default_rules(), + DEFAULT_HEADLINE_PATTERN, + &Agda, + ) + .unwrap(); assert_eq!(doc.version, "0.1"); assert!( @@ -74,7 +88,14 @@ fn dag_over_wellformed_fixture_is_all_clean() { fn dag_populates_node_headlines() { let root = fixture("headlines"); let roots = [root.join("All.agda")]; - let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap(); + let doc = build_dag( + &root, + &roots, + &default_rules(), + DEFAULT_HEADLINE_PATTERN, + &Agda, + ) + .unwrap(); // `Thm` declares two top-level headline signatures (sorted, deduped); its // indented `private` helper is not top-level and is not surfaced.