ArghDA M1: Backend abstraction — make the engine prover-parametric (#32)

## What & why

The keystone 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 become backend-neutral. Agda is the first
(v0.1 reference) impl; adding Idris2 / Lean4 / Z3 / CVC5 / Coq /
Isabelle / Mizar is now *an impl*, not a rewrite.

Follow-on from M0 (toolchain provisioning, merged as #31). #31 being
merged, this is a fresh PR on the same working branch.

## This is a pure refactor — the test suite is the oracle

Behaviour is unchanged, ground-truthed by running the tools (not
inferred):

- **`cargo test`** — the 64 pre-existing tests (50 lib + 14 integration)
all stay green; +2 new Agda-backend tests = **66 passing, 0 failed**.
- **`cargo clippy --all-targets --all-features -- -D warnings`** —
clean.
- **`cargo fmt --check`** — clean.
- **`scripts/check-spdx.sh .`** — `SPDX licence invariant: OK`.
- **Dogfood** — `arghda dag tests/fixtures/wellformed` emits
byte-compatible JSON (`version: "0.1"`, same nodes/edges); `arghda check
…/All.agda` ran a **real** Agda typecheck → `proven-eligible` (agda is
present from #31's provisioning).

## Changes

**New `src/prover/`:**
- `Backend` trait — `name` / `kind` / `extensions` / `safe_mode` /
`check_file` + the import-graph trio (`module_name_of` /
`module_to_path` / `direct_imports`) + `discover_roots` + `lint_rules`.
- `BackendKind { Assistant, Solver }` — the two interaction models
(typecheck-a-file vs SMT query).
- `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`).

**Refactor:**
- `src/agda.rs` → `src/prover/agda.rs`. `Agda` is the first impl: owns
the `agda` 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,
never manufactured from a green exit.
- `graph::build` and `dag::build` take `&dyn Backend` and use the
backend's extension filter + import parsing. **The cycle-safe
reachability walk and its `transitive_imports_terminates_on_a_cycle`
regression are untouched** — cycle safety is inherited free by every
backend.
- `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%; `.gitignore` ignores `*.agdai`.

## Honesty note (owner directive + AGENTIC.a2ml)

The `Backend` module is the boundary where "never report a verdict the
tool did not emit" is enforced: `check_file` derives its verdict from
the actual exit code and degrades to `Unavailable` when the binary is
absent.

## Next (trait now stable → parallelisable)

M3 reasoning-graph (`src/reason`), M4 Idris2, M5 SMT (Z3/CVC5), M2
Cubical-Agda.

---
_Generated by [Claude
Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.gitignore

@@ -18,3 +18,6 @@ dist-newstyle/
 .direnv/
 result
 result-*
+
+# Agda compiled interface files (generated by typecheck runs)
+*.agdai

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

src/agda.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<dyn LintRule>],
     headline_pattern: &str,
+    backend: &dyn Backend,
 ) -> Result<DagDocument> {
     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,

src/dag.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,21 +178,29 @@ pub struct ImportGraph {
     pub edges: Vec<Edge>,
 }
 
-/// 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<ImportGraph> {
+/// 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<ImportGraph> {
+    let exts = backend.extensions();
     // module id -> relative file path, for every in-tree module.
     let mut by_id: BTreeMap<String, PathBuf> = BTreeMap::new();
     for entry in WalkDir::new(include_root)
         .into_iter()
         .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<ImportGraph> {
 
     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 {

src/graph.rs

@@ -1,12 +1,15 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-//! 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};