ArghDA M6: Lean4 backend + honest cross-backend check verdicts

.machine_readable/6a2/STATE.a2ml

@@ -46,7 +46,7 @@ milestones = [
   { 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 = 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 = 0 },
+  { 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 = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 },
@@ -60,6 +60,28 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M6 landed 2026-07-01 (85%): the Lean4 backend — sixth backend. src/prover/
+# lean.rs: `lean <file>` elaboration. The honesty subtlety Lean forces: a green
+# exit does NOT mean proven (sorry is only a warning; exit 0). So the verdict is
+# NOT exit-code-only like agda/idris2 — it PARSES output: exit≠0→Error; exit 0 +
+# "sorry" in output→Admitted; exit 0 clean→Unknown (elaborated but NOT audited —
+# arghda refuses to claim Proven without a #print axioms audit; matches the plan's
+# "honest Unknown when the audit is absent"). Dotted modules reuse module_name_of;
+# .lean module_to_path; import parser (top-level `import Mod`; `open` is a
+# namespace directive, NOT an edge — deliberately ignored); Main.lean roots.
+# src/lint/lean.rs: LeanEscapeHatch (sorry/admit/native_decide/unsafe) named
+# "escape-hatch". Wired via --backend lean4. Ground-truthed vs Lean 4.13.0.
+# HONESTY FIX exposed by M6 (applies to ALL backends): the `check` command's
+# verdict was collapsing to proven-eligible/rejected, mislabelling a clean Lean
+# file "rejected" and an SMT `sat` "rejected". Now reports the real verdict word
+# (proven-eligible/refuted/unknown/admitted/postulated/rejected); the human line
+# drops the assistant-centric ok/FAILED. 119 tests (86 lib + 33 integration;
+# +5 lean unit +4 lean-escape unit +2 lean integration). Dogfooded REAL lean:
+# clean proof→unknown, sorry→admitted; re-dogfooded z3 sat→refuted, unsat→
+# proven-eligible, agda→proven-eligible; doctor now 6 backends. Follow-ons (the
+# 15%): lake-env/LEAN_PATH for project-wide multi-file resolution; the per-decl
+# #print axioms audit to promote Unknown→Proven.
+#
 # M0 COMPLETED 2026-07-01: the `arghda doctor` subcommand lands, closing the
 # last M0 gap. Probes every known backend by running `<command> --version`;
 # reports runnable/detail honestly (runnable=false only when the binary truly
@@ -162,10 +184,10 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M0 + M1 + M2 + M3 + M4 + M5 DONE. Five backends across both interaction models (agda, agda-cubical, idris2 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine core complete. Next:",
-  "Flying-Logic epic M6: Lean4 adapter (lake build + #print axioms audit → honest Unknown soundness when the audit is absent). Lean 4.13.0 provisioned. Sixth backend.",
-  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds it).",
+  "M0-M6 DONE. SIX backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine essentially complete. Next:",
+  "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds the manifest).",
   "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome).",
+  "M6 follow-on (15%): 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.",
@@ -177,10 +199,10 @@ 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-M0-doctor: 80 lib + 28 integration = 108 tests pass. `arghda doctor`
-# dogfooded: 5/5 backends runnable. All five backends dogfooded via real CLI:
-# agda + agda-cubical + idris2 (Assistant), z3 + cvc5 (Solver). Dogfooded
-# historically against echo-types + agda-unused.
+# post-M6: 86 lib + 33 integration = 119 tests pass. `arghda doctor` dogfooded:
+# 6/6 backends runnable. All six dogfooded via real CLI: agda + agda-cubical +
+# idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded historically against
+# echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

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

src/lint/lean.rs

@@ -0,0 +1,116 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Lean4 `escape-hatch` (warn) — surface soundness escape hatches.
+//!
+//! The Lean4 analogue of the Agda/Idris2 escape-hatch rules; shares the rule
+//! *name* `escape-hatch` so the reasoning graph caps any hit at amber.
+//!
+//! Flags `sorry` and `admit` (proof holes), `native_decide` (trusts the
+//! compiler's evaluation, outside the kernel) and `unsafe` (bypasses the
+//! termination/positivity checks). Lean `--check`/elaboration exits 0 even
+//! with `sorry` present (it is only a *warning*), so without this rule — and
+//! without the `#print axioms` audit — such gaps ride along invisibly. That
+//! is why the Lean backend's own verdict is at best `Unknown` on a green
+//! elaboration absent the audit.
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct LeanEscapeHatch;
+
+const ESCAPE_TOKENS: &[&str] = &["sorry", "admit", "native_decide", "unsafe"];
+
+impl LintRule for LeanEscapeHatch {
+    fn name(&self) -> &'static str {
+        "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
+            }
+            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 `sorryAx_helper` or a
+/// namespaced `Foo.admit` do not spuriously match the bare keyword).
+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(LeanEscapeHatch)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn sorry_is_warned_under_escape_hatch() {
+        let r = lint_str("theorem t : 1 = 1 := by sorry\n");
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].rule, "escape-hatch");
+        assert!(r.diagnostics[0].message.contains("sorry"));
+    }
+
+    #[test]
+    fn native_decide_and_unsafe_are_warned() {
+        let r = lint_str("unsafe def f : Nat := 0\nexample : P := by native_decide\n");
+        assert_eq!(r.warns().count(), 2);
+    }
+
+    #[test]
+    fn escape_token_in_comment_is_ignored() {
+        let r = lint_str("def x : Nat := 0 -- TODO: no sorry here\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn clean_lean_file_is_silent() {
+        let r = lint_str("theorem t : 1 = 1 := rfl\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}

src/lint/mod.rs

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

src/main.rs

@@ -5,7 +5,7 @@ use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
     build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend,
-    BackendKind, Idris2, LintRule, RuleConfig, Smt, State, Workspace,
+    BackendKind, Idris2, Lean, LintRule, RuleConfig, Smt, State, Verdict, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -16,7 +16,7 @@ use walkdir::WalkDir;
 type RuleSet = Vec<Box<dyn LintRule>>;
 
 /// Every backend `--backend` accepts and `doctor` probes.
-const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "z3", "cvc5"];
+const KNOWN_BACKENDS: &[&str] = &["agda", "agda-cubical", "idris2", "lean4", "z3", "cvc5"];
 
 /// Resolve a `--backend` name to a backend instance. Agda is the default and
 /// v0.1 reference; Idris2 is the estate ABI language.
@@ -25,19 +25,20 @@ fn backend_for(name: &str) -> Result<Box<dyn Backend>> {
         "agda" => Ok(Box::new(Agda)),
         "agda-cubical" => Ok(Box::new(AgdaCubical)),
         "idris2" => Ok(Box::new(Idris2)),
+        "lean4" => Ok(Box::new(Lean)),
         "z3" => Ok(Box::new(Smt::z3())),
         "cvc5" => Ok(Box::new(Smt::cvc5())),
-        other => {
-            anyhow::bail!("unknown backend `{other}` (known: agda, agda-cubical, idris2, z3, cvc5)")
-        }
+        other => anyhow::bail!(
+            "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, z3, cvc5)"
+        ),
     }
 }
 
 #[derive(Parser)]
 #[command(
     name = "arghda",
     version,
-    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Z3, CVC5)"
+    about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Z3, CVC5)"
 )]
 struct Cli {
     #[command(subcommand)]
@@ -64,7 +65,8 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
+        /// `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Also run the external `agda-unused` analyser and re-emit its
@@ -83,7 +85,8 @@ enum Cmd {
         /// Include root (search path). Defaults to the file's directory.
         #[arg(long)]
         include_root: Option<PathBuf>,
-        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
+        /// `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Emit the report as JSON.
@@ -106,7 +109,8 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
+        /// `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
     },
@@ -129,7 +133,8 @@ enum Cmd {
         /// `<PATH>/.arghda/config.toml` if present.
         #[arg(long)]
         config: Option<PathBuf>,
-        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `z3`, `cvc5`.
+        /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`,
+        /// `z3`, `cvc5`.
         #[arg(long, default_value = "agda")]
         backend: String,
         /// Run the backend on every node to populate REAL prover verdicts
@@ -405,12 +410,24 @@ fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: boo
         run_lints(file, &ctx, &rules).with_context(|| format!("linting {}", file.display()))?;
     let outcome = backend.check_file(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
+    // "proven-eligible" — a clean-but-unaudited Lean file is `unknown`, an
+    // SMT `sat` is `refuted`, never silently "rejected"/"ok".
     let verdict = if !outcome.available {
         "backend-unavailable"
-    } else if outcome.ok && !report.has_hard_block() {
-        "proven-eligible"
-    } else {
+    } else if report.has_hard_block() {
         "rejected"
+    } else {
+        match outcome.verdict {
+            Verdict::Proven => "proven-eligible",
+            Verdict::Refuted => "refuted",
+            Verdict::Unknown => "unknown",
+            Verdict::Admitted => "admitted",
+            Verdict::Postulated => "postulated",
+            Verdict::Error => "rejected",
+            Verdict::Unavailable => "backend-unavailable",
+        }
     };
 
     if json {
@@ -426,13 +443,12 @@ fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: boo
         println!("{}", file.display());
         if outcome.available {
             println!(
-                "  {}: exit {}, {}",
+                "  {}: exit {}",
                 backend.name(),
                 outcome
                     .exit_code
                     .map(|c| c.to_string())
                     .unwrap_or_else(|| "?".into()),
-                if outcome.ok { "ok" } else { "FAILED" }
             );
         } else {
             println!(