ArghDA M6 follow-on: Lean #print axioms audit — honest Unknown→Proven

.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 = 95 },
   { 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 = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 92 },
   { 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 },
@@ -75,6 +75,22 @@ milestones = [
 # has recently been set up". Permanent — future PRs satisfy the gate
 # automatically. NB the template is fine; only extraction-origin repos drift.
 #
+# M6 FOLLOW-ON landed 2026-07-01: the Lean `#print axioms` audit — the honest
+# Unknown→Proven promotion. On a clean elaboration (base verdict Unknown),
+# check_file now runs an audit: parse decl names (theorem/lemma/def/abbrev/
+# instance, skipping attrs/modifiers/anonymous), copy the source to a fresh
+# TEMP DIR (std-only, no new dep; cleaned up) + append `#print axioms <name>`
+# per decl, run `lean`, and classify (ground-truthed vs Lean 4.13.0):
+#   all decls "does not depend on any axioms" or only {propext, Classical.choice,
+#   Quot.sound} → Proven; any sorryAx → Admitted; any OTHER axiom (e.g.
+#   native_decide's) → Postulated. Audit failure (imports unresolvable in the
+#   temp dir, no decls, lean absent) → None → stays Unknown (honest, never
+#   wrong). REACH: import-free files (temp-dir copy elaborates without
+#   LEAN_PATH); imported files need lake-env (still the remaining M6 follow-on).
+#   129 tests (+2 unit: decl_names, classify_axioms). Dogfooded REAL lean:
+#   rfl→proven-eligible, Classical→proven-eligible, native_decide→POSTULATED
+#   (the audit catches what bare elaboration hides), sorry→admitted. M6 now 92%.
+#
 # M4 FOLLOW-ON landed 2026-07-01: Idris2 `.ipkg`-declared roots. discover_roots
 # now unions (a) `.ipkg` `main = <Module>` resolved to its .idr (honouring an
 # optional quoted `sourcedir`; `--` comments stripped; first existing candidate
@@ -242,7 +258,7 @@ milestones = [
 actions = [
   "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.",
+  "M6 follow-on: #print axioms audit DONE (import-free files promote honestly); remaining = lake-env/LEAN_PATH so imported files can be checked + audited too.",
   "M4 follow-on: .ipkg-declared roots DONE; remaining = 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 (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).",
@@ -254,8 +270,8 @@ 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-M4-followon: 93 lib + 34 integration = 127 tests pass. codeql.yml added
-# (code-scanning gate fix). doctor/groove/dispatch
+# post-M6-followon: 95 lib + 34 integration = 129 tests pass. codeql.yml added
+# (code-scanning gate fix). Lean #print axioms audit dogfooded. 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

src/prover/lean.rs

@@ -10,12 +10,19 @@
 //! * exit non-zero → [`Verdict::Error`] (elaboration failed).
 //! * exit 0, output mentions `sorry` → [`Verdict::Admitted`] (a hole rode
 //!   along on a green elaboration).
-//! * exit 0, clean → [`Verdict::Unknown`] — the file elaborates, but without
-//!   a `#print axioms` audit arghda will NOT claim it proven (it could still
-//!   use `native_decide`, `sorryAx`, or other axioms). Promoting `Unknown` →
-//!   `Proven` via a per-declaration `#print axioms` audit is the follow-on.
+//! * exit 0, clean → run the **`#print axioms` audit** and promote honestly:
+//!   `Proven` if every declaration depends only on the standard axioms
+//!   (`propext`, `Classical.choice`, `Quot.sound`); `Postulated` if a
+//!   non-standard axiom sneaks in (e.g. the one `native_decide` introduces —
+//!   which a bare elaboration would NOT reveal); `Admitted` on `sorryAx`. If
+//!   the audit can't run (no declarations, `lean` absent, or the file imports
+//!   modules the bare temp-dir copy can't resolve), it stays `Verdict::Unknown`.
 //! * binary absent → [`Verdict::Unavailable`].
 //!
+//! The audit currently reaches import-free files (a temp-dir copy elaborates
+//! them without `LEAN_PATH`); auditing imported files needs `lake env`
+//! resolution — a documented follow-on.
+//!
 //! Lean modules are dotted (`Mathlib.Data.Nat` ↔ `Mathlib/Data/Nat.lean`),
 //! so [`crate::graph::module_name_of`] is reused. Imports are top-level
 //! `import Mod` lines; Lean `open` is a *namespace* directive, not a
@@ -30,8 +37,14 @@ use anyhow::{Context, Result};
 use std::fs;
 use std::path::{Path, PathBuf};
 use std::process::Command;
+use std::time::{SystemTime, UNIX_EPOCH};
 use walkdir::WalkDir;
 
+/// Lean's standard, trusted axioms — a proof depending only on these is
+/// sound (this is the mathlib convention). Anything else (sorryAx, or the
+/// axioms `native_decide` introduces) is not.
+const STANDARD_AXIOMS: &[&str] = &["propext", "Classical.choice", "Quot.sound"];
+
 const TAIL_LINES: usize = 40;
 
 /// The Lean4 theorem prover.
@@ -63,7 +76,18 @@ impl Backend for Lean {
             Ok(out) => {
                 let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
                 combined.push_str(&String::from_utf8_lossy(&out.stderr));
-                let verdict = lean_verdict(&combined, out.status.success());
+                let mut verdict = lean_verdict(&combined, out.status.success());
+                // A clean elaboration is only `Unknown` on its own — run the
+                // `#print axioms` audit to promote it honestly: Proven if every
+                // declaration depends only on the standard axioms, Postulated
+                // if a non-standard axiom (e.g. `native_decide`'s) sneaks in,
+                // Admitted on sorryAx. If the audit can't run (imports need
+                // lake, no declarations, tool absent) it stays `Unknown`.
+                if verdict == Verdict::Unknown {
+                    if let Some(audited) = axiom_audit(file) {
+                        verdict = audited;
+                    }
+                }
                 Ok(Outcome {
                     available: true,
                     exit_code: out.status.code(),
@@ -170,6 +194,124 @@ fn tail(s: &str, n: usize) -> String {
     lines[start..].join("\n")
 }
 
+/// The declaration names in a Lean source that can depend on axioms
+/// (`theorem`/`lemma`/`def`/`abbrev`/`instance`), skipping leading
+/// attributes/modifiers and anonymous decls. Deliberately conservative: a
+/// missed name just isn't audited; a mis-parsed name makes `lean` error and
+/// the audit falls back to `Unknown` — it never yields a wrong verdict.
+fn decl_names(src: &str) -> Vec<String> {
+    const KEYWORDS: &[&str] = &["theorem", "lemma", "def", "abbrev", "instance"];
+    const MODIFIERS: &[&str] = &[
+        "private",
+        "protected",
+        "noncomputable",
+        "partial",
+        "unsafe",
+        "scoped",
+        "local",
+        "mutual",
+    ];
+    let mut names = Vec::new();
+    for line in src.lines() {
+        let tokens: Vec<&str> = line.split_whitespace().collect();
+        let mut i = 0;
+        // Skip leading `@[..]` attributes and declaration modifiers.
+        while let Some(tk) = tokens.get(i) {
+            if tk.starts_with("@[") || MODIFIERS.contains(tk) {
+                i += 1;
+            } else {
+                break;
+            }
+        }
+        if tokens.get(i).is_some_and(|tk| KEYWORDS.contains(tk)) {
+            if let Some(name_tok) = tokens.get(i + 1) {
+                let name: String = name_tok
+                    .chars()
+                    .take_while(|c| c.is_alphanumeric() || *c == '_' || *c == '.' || *c == '\'')
+                    .collect();
+                if !name.is_empty() {
+                    names.push(name);
+                }
+            }
+        }
+    }
+    names.dedup();
+    names
+}
+
+/// Classify the combined output of a batch of `#print axioms` commands:
+/// any `sorryAx` ⇒ Admitted; else any non-standard axiom ⇒ Postulated; else
+/// (all clean or standard-only) ⇒ Proven.
+fn classify_axioms(output: &str) -> Verdict {
+    let mut saw_nonstandard = false;
+    for line in output.lines() {
+        let Some(open) = line.find("depends on axioms: [") else {
+            continue; // "does not depend on any axioms" ⇒ clean, skip
+        };
+        let rest = &line[open + "depends on axioms: [".len()..];
+        let list = rest.split(']').next().unwrap_or(rest);
+        for ax in list.split(',') {
+            let ax = ax.trim();
+            if ax == "sorryAx" {
+                return Verdict::Admitted;
+            }
+            if !ax.is_empty() && !STANDARD_AXIOMS.contains(&ax) {
+                saw_nonstandard = true;
+            }
+        }
+    }
+    if saw_nonstandard {
+        Verdict::Postulated
+    } else {
+        Verdict::Proven
+    }
+}
+
+/// Run a `#print axioms` audit on `file`'s declarations. Copies the source
+/// into a fresh temp dir, appends `#print axioms <name>` per declaration,
+/// and runs `lean`. Returns the classified verdict, or `None` when the audit
+/// can't be trusted — no declarations, `lean` absent, or the copy fails to
+/// elaborate (e.g. it imports modules that need `lake env`/`LEAN_PATH`, which
+/// a bare temp dir lacks). `None` ⇒ the caller keeps the honest `Unknown`.
+fn axiom_audit(file: &Path) -> Option<Verdict> {
+    let src = fs::read_to_string(file).ok()?;
+    let names = decl_names(&src);
+    if names.is_empty() {
+        return None;
+    }
+
+    let nanos = SystemTime::now()
+        .duration_since(UNIX_EPOCH)
+        .map(|d| d.as_nanos())
+        .unwrap_or(0);
+    let dir = std::env::temp_dir().join(format!("arghda-audit-{}-{}", std::process::id(), nanos));
+    fs::create_dir_all(&dir).ok()?;
+
+    let mut body = src;
+    body.push('\n');
+    for n in &names {
+        body.push_str(&format!("#print axioms {n}\n"));
+    }
+    let audit_file = dir.join("Audit.lean");
+
+    let verdict = match fs::write(&audit_file, &body) {
+        Ok(()) => match Command::new("lean").arg(&audit_file).output() {
+            // Only trust the audit if the copy elaborated cleanly; otherwise
+            // (imports unresolved in the temp dir, etc.) stay Unknown.
+            Ok(out) if out.status.success() => {
+                let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
+                combined.push_str(&String::from_utf8_lossy(&out.stderr));
+                Some(classify_axioms(&combined))
+            }
+            _ => None,
+        },
+        Err(_) => None,
+    };
+
+    let _ = fs::remove_dir_all(&dir);
+    verdict
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -208,6 +350,52 @@ mod tests {
         assert!(!imports.iter().any(|i| i.contains("Ignored")));
     }
 
+    #[test]
+    fn decl_names_parses_keywords_modifiers_attributes() {
+        let src = "\
+@[simp] theorem foo : True := trivial\n\
+private def bar : Nat := 0\n\
+lemma baz.qux : 1 = 1 := rfl\n\
+noncomputable def qq : Nat := 0\n\
+example : True := trivial\n\
+-- theorem commented : ...\n\
+#eval 1\n";
+        let names = decl_names(src);
+        assert!(names.contains(&"foo".to_string()));
+        assert!(names.contains(&"bar".to_string()));
+        assert!(names.contains(&"baz.qux".to_string()), "dotted names kept");
+        assert!(names.contains(&"qq".to_string()), "modifier skipped");
+        // `example` is anonymous → not audited; `#eval` is not a decl.
+        assert!(!names.iter().any(|n| n == "example" || n == "1"));
+    }
+
+    #[test]
+    fn classify_axioms_maps_the_ground_truthed_output() {
+        // The three shapes ground-truthed against Lean 4.13.0.
+        assert_eq!(
+            classify_axioms("'t' does not depend on any axioms"),
+            Verdict::Proven
+        );
+        assert_eq!(
+            classify_axioms("'c' depends on axioms: [propext, Classical.choice, Quot.sound]"),
+            Verdict::Proven,
+        );
+        assert_eq!(
+            classify_axioms("'g' depends on axioms: [sorryAx]"),
+            Verdict::Admitted
+        );
+        assert_eq!(
+            classify_axioms("'n' depends on axioms: [Lean.ofReduceBool]"),
+            Verdict::Postulated,
+            "native_decide's axiom is non-standard ⇒ amber",
+        );
+        // Mixed: any sorryAx dominates.
+        assert_eq!(
+            classify_axioms("'a' depends on axioms: [propext]\n'b' depends on axioms: [sorryAx]"),
+            Verdict::Admitted
+        );
+    }
+
     #[test]
     fn verdict_is_honest_about_sorry_and_the_missing_audit() {
         // A green elaboration is only Unknown without a #print axioms audit;
@@ -227,13 +415,14 @@ mod tests {
         std::fs::write(&f, "theorem t : 1 = 1 := rfl\n").unwrap();
         let out = Lean.check_file(&f, tmp.path()).unwrap();
         if out.available {
-            // Never fabricated Proven: a clean Lean file is Unknown (audit
-            // absent), a sorry file Admitted, a broken file Error.
+            // Honest verdict invariant: never fabricated. With the axioms
+            // audit a clean `rfl` proof is promoted to Proven; `ok` iff
+            // Proven; and the value is always one of the real states.
             assert!(matches!(
                 out.verdict,
-                Verdict::Unknown | Verdict::Admitted | Verdict::Error
+                Verdict::Proven | Verdict::Unknown | Verdict::Admitted | Verdict::Error
             ));
-            assert!(!out.ok, "lean never reports `ok` without an axioms audit");
+            assert_eq!(out.ok, out.verdict == Verdict::Proven);
         } else {
             assert_eq!(out.verdict, Verdict::Unavailable);
         }