ArghDA M4: Idris2 backend + --backend selector — genuinely multi-backend

.gitignore

@@ -21,3 +21,8 @@ result-*
 
 # Agda compiled interface files (generated by typecheck runs)
 *.agdai
+
+# Idris2 compiled output (generated by `idris2 --check` runs)
+build/
+*.ttc
+*.ttm

.machine_readable/6a2/STATE.a2ml

@@ -44,7 +44,7 @@ milestones = [
   { 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 = 100 },
-  { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 },
+  { 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 = 0 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 },
   { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 },
@@ -60,6 +60,22 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M4 landed 2026-07-01 (90%): the Idris2 backend — arghda is now genuinely
+# multi-backend. src/prover/idris2.rs: `idris2 --check --source-dir <root>
+# <file>` (ground-truthed vs Idris2 0.7.0), exit-code-only verdict; dotted
+# module names reuse graph::module_name_of; .idr module_to_path; Idris2 import
+# parser (`import [public] Mod [as Alias]`, top-level — no `open`); Main.idr
+# root discovery. src/lint/idris2.rs: Idris2EscapeHatch (believe_me/assert_total
+# /assert_smaller/idris_crash + `%default partial`), named "escape-hatch" so it
+# reuses the reason-graph amber cap. WIRED via a new `--backend agda|idris2` CLI
+# selector on scan/check/dag/reason (backend_for()); unknown backend errors
+# cleanly. 93 tests (70 lib + 23 integration; +9 Idris2 unit +3 Idris2
+# integration; the graph/dag/reason tests are hermetic — text parsing, no binary
+# needed). Dogfooded with REAL idris2 on PATH: `check --backend idris2` →
+# proven-eligible; `reason --backend idris2 --check` → live typechecks, Main cone
+# proven+wired, Orphan proven-but-unwired. Follow-ons (the missing 10%):
+# .ipkg-declared roots, totality-hole (`?name`) + per-def `partial` lint.
+#
 # M3 landed 2026-07-01: the Flying-Logic reasoning graph (src/reason/) — the
 # headline capability. Wraps DagDocument verbatim (ReasonDocument.dag) + adds a
 # per-node Verdict, And|Or edge juncts, and a memoised, cycle-safe, DEMOTE-ONLY
@@ -104,10 +120,10 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M1 (Backend trait) + M3 (reasoning graph) DONE. Next, all unblocked by the stable trait — pick per priority:",
-  "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.",
+  "M1 (Backend trait) + M3 (reasoning graph) + M4 (Idris2) DONE. Next, all unblocked by the stable trait + --backend selector:",
+  "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the FIRST Solver-kind backend; SMT-LIB2 -> unsat(Proven)/sat(Refuted)/unknown(Unknown). Both binaries provisioned. Exercises the Solver half of the taxonomy (no imports; isolated nodes).",
   "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden).",
+  "M4 follow-on (the missing 10%): .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) so `arghda reason <workspace>` lights the cone without --check.",
   "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).",
   "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.",
@@ -119,10 +135,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-M3: 61 lib + 20 integration = 81 tests pass. Dogfooded via real CLI
-# runs: `dag` JSON byte-compatible; `check` + `reason --check` ran real agda
-# typechecks (proven-eligible / all-Proven+wired cone). Dogfooded historically
-# against echo-types + agda-unused.
+# post-M4: 70 lib + 23 integration = 93 tests pass. Dogfooded via real CLI
+# runs on BOTH backends: agda (`check`/`reason --check`) and idris2 (`check
+# --backend idris2` → proven-eligible; `reason --backend idris2 --check` →
+# live-typechecked cone). Dogfooded historically against echo-types +
+# agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

@@ -30,6 +30,6 @@ 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 prover::{default_backend, Agda, Backend, BackendKind, Idris2, Outcome, Verdict};
 pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode};
 pub use workspace::{StaleEntry, State, Workspace};

src/lint/idris2.rs

@@ -0,0 +1,140 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Idris2 `escape-hatch` (warn) — surface soundness escape hatches.
+//!
+//! The Idris2 analogue of the Agda [`super::escape_hatch::EscapeHatch`]. It
+//! shares the rule *name* `escape-hatch` deliberately: the reasoning graph
+//! (`crate::reason`) caps any `escape-hatch` node at amber, so a `believe_me`
+//! in Idris2 and a `believe_me` in Agda get the same honest treatment.
+//!
+//! Flags the Idris2 trust/escape primitives `believe_me`, `assert_total`,
+//! `assert_smaller`, `idris_crash`, and the `%default partial` directive.
+//! Idris2 `--check` exits 0 even when these are present, so without this rule
+//! they would silently ride along in an otherwise-green verdict — exactly the
+//! silent-failure class arghda exists to surface. Totality holes (`?name`)
+//! and per-def `partial` modifiers are a documented follow-on.
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct Idris2EscapeHatch;
+
+const ESCAPE_TOKENS: &[&str] = &[
+    "believe_me",
+    "assert_total",
+    "assert_smaller",
+    "idris_crash",
+];
+
+impl LintRule for Idris2EscapeHatch {
+    fn name(&self) -> &'static str {
+        // Shared with the Agda rule on purpose — the reasoning graph's
+        // lint→verdict cap keys on this name.
+        "escape-hatch"
+    }
+
+    fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> {
+        let contents =
+            fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
+        for (i, line) in contents.lines().enumerate() {
+            let trimmed = line.trim_start();
+            if trimmed.starts_with("--") {
+                continue; // whole-line comment
+            }
+            // The `%default partial` directive turns off totality checking.
+            if trimmed.starts_with("%default") && trimmed.contains("partial") {
+                report.push(warn(
+                    self.name(),
+                    file,
+                    i + 1,
+                    "totality escape directive `%default partial`".to_string(),
+                ));
+            }
+            // Trust/escape primitives, ignoring any trailing line comment.
+            let code = line.split(" --").next().unwrap_or(line);
+            for tok in ESCAPE_TOKENS {
+                if has_token(code, tok) {
+                    report.push(warn(
+                        self.name(),
+                        file,
+                        i + 1,
+                        format!("escape primitive `{tok}`"),
+                    ));
+                }
+            }
+        }
+        Ok(())
+    }
+}
+
+fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic {
+    Diagnostic {
+        rule: rule.to_string(),
+        severity: Severity::Warn,
+        file: file.to_path_buf(),
+        message,
+        line: Some(line),
+    }
+}
+
+/// `tok` appears in `s` as a delimited token (so `assert_totally` or
+/// `believe_me_helper` do not match).
+fn has_token(s: &str, tok: &str) -> bool {
+    s.split(|c: char| c.is_whitespace() || "(){};,".contains(c))
+        .any(|w| w == tok)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_str(body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(Idris2EscapeHatch)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn believe_me_is_warned_under_the_escape_hatch_name() {
+        let r = lint_str("module M\n\nx : Nat\nx = believe_me 0\n");
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].rule, "escape-hatch");
+        assert!(r.diagnostics[0].message.contains("believe_me"));
+    }
+
+    #[test]
+    fn assert_total_and_default_partial_are_warned() {
+        let r = lint_str("%default partial\n\nf : Nat -> Nat\nf x = assert_total (f x)\n");
+        assert_eq!(r.warns().count(), 2);
+    }
+
+    #[test]
+    fn escape_token_in_comment_is_ignored() {
+        let r = lint_str("module M\n\nx : Nat\nx = 0 -- avoid believe_me here\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn longer_identifier_does_not_match() {
+        let r = lint_str("module M\n\nbelieve_me_helper : Nat\nbelieve_me_helper = 0\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn clean_idris_file_is_silent() {
+        let r = lint_str("module M\n\ngreeting : String\ngreeting = \"hi\"\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}

src/lint/mod.rs

@@ -6,6 +6,7 @@ use anyhow::Result;
 use std::path::{Path, PathBuf};
 
 pub mod escape_hatch;
+pub mod idris2;
 pub mod orphan_module;
 pub mod postulate;
 pub mod safe_pragma;