ArghDA M3 follow-on: workspace-fed verdicts + staleness in reason

.machine_readable/6a2/STATE.a2ml

@@ -100,6 +100,22 @@ milestones = [
 # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired.
 # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint).
 #
+# M3 FOLLOW-ON landed 2026-07-01: workspace-fed verdicts + staleness in `reason`
+# — the reasoning graph now sources REAL verdicts from a four-state workspace's
+# `proven/` state, no re-check needed. New `arghda reason <path> --workspace
+# <ws>`: pure mapping `reason::workspace_verdicts(dag, proven, stale)` sets a
+# node whose file basename is in `proven/` to Proven (evidence "prover: proven"),
+# and if that same file is stale (content/closure hash changed since promotion,
+# via `Workspace::stale_proven`) inserts it into the stale set so the demote-only
+# fold lowers it back to Unknown (evidence "prover: proven; stale: closure hash
+# changed"). Matched by file basename (documented collision caveat). `--check`
+# stays authoritative — a fresh typecheck overrides + clears staleness. Honest by
+# construction: verdicts come only from a recorded promotion, never fabricated;
+# staleness dominates a stale Proven. 130 tests (+1 reason unit: proven lights
+# the cone, stale demotes). Dogfooded: fresh proven leaf → effective proven, un-
+# proven root → unknown; edit the proven file on disk → Good demoted to unknown
+# with the stale evidence string. M3 base was 100%; this is pure additive refinement.
+#
 # M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the
 # engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local,
 # Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome`
@@ -260,7 +276,7 @@ actions = [
   "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.",
   "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).",
+  "M3 follow-on: DONE — `reason --workspace <ws>` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.",
   "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning (Coq via opam ~1hr; Isabelle ~4GB; Mizar niche).",
 ]
 
@@ -270,8 +286,9 @@ 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-M6-followon: 95 lib + 34 integration = 129 tests pass. codeql.yml added
-# (code-scanning gate fix). Lean #print axioms audit dogfooded. doctor/groove/dispatch
+# post-M3-followon: 96 lib + 34 integration = 130 tests pass. codeql.yml added
+# (code-scanning gate fix). reason --workspace verdicts+staleness dogfooded.
+# 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/lib.rs

@@ -38,5 +38,7 @@ pub use prover::{
     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 reason::{
+    build as build_reason, workspace_verdicts, Junct, ReasonDocument, ReasonEdge, ReasonNode,
+};
 pub use workspace::{StaleEntry, State, Workspace};

src/main.rs

@@ -151,6 +151,12 @@ enum Cmd {
         /// `echidna[=<url>]`.
         #[arg(long, default_value = "local")]
         dispatch: String,
+        /// A four-state workspace whose `proven/` state supplies verdicts
+        /// WITHOUT re-checking: a node whose file is proven (and fresh) →
+        /// `proven`; proven-but-stale (content/closure hash changed) →
+        /// demoted to `unknown`. Matched by file basename.
+        #[arg(long)]
+        workspace: Option<PathBuf>,
     },
     /// Claim a file: inbox -> working.
     Claim { workspace: PathBuf, file: String },
@@ -242,6 +248,7 @@ fn main() -> Result<()> {
             backend,
             check,
             dispatch,
+            workspace,
         } => reason(
             &path,
             &entry,
@@ -250,6 +257,7 @@ fn main() -> Result<()> {
             &backend,
             check,
             &dispatch,
+            workspace.as_deref(),
         )?,
         Cmd::Claim { workspace, file } => {
             transition(&workspace, &file, State::Inbox, State::Working)?
@@ -542,6 +550,7 @@ fn dag(
     Ok(())
 }
 
+#[allow(clippy::too_many_arguments)]
 fn reason(
     include_root: &Path,
     entry: &[PathBuf],
@@ -550,6 +559,7 @@ fn reason(
     backend_name: &str,
     do_check: bool,
     dispatch: &str,
+    workspace: Option<&Path>,
 ) -> Result<()> {
     let backend = backend_for(backend_name)?;
     let (roots, rules, cfg) = resolve_roots_and_rules(
@@ -567,19 +577,37 @@ fn reason(
         backend.as_ref(),
     )?;
 
-    // Real prover verdicts by module id. Empty unless `--check`, in which
-    // case each node is typechecked for real (honest exit codes) — a green
-    // node is only ever `proven` because the tool returned 0. Staleness
-    // needs a workspace `proven/` state, so it stays empty here.
+    // Real prover verdicts by module id, plus the stale set.
     let mut verdicts = std::collections::BTreeMap::new();
-    let stale = std::collections::BTreeSet::new();
+    let mut stale = std::collections::BTreeSet::new();
+
+    // Source 1 — a workspace's `proven/` state (no re-check). The pure
+    // mapping lives in `reason::workspace_verdicts`; here we just read the
+    // proven + stale basename sets off the workspace and feed them in.
+    if let Some(ws_path) = workspace {
+        let ws = Workspace::open(ws_path)?;
+        let proven: std::collections::BTreeSet<String> = ws
+            .list(State::Proven)?
+            .iter()
+            .filter_map(|p| p.file_name().and_then(|s| s.to_str()).map(String::from))
+            .collect();
+        let stale_names: std::collections::BTreeSet<String> =
+            ws.stale_proven()?.into_iter().map(|e| e.file).collect();
+        let (wv, ws_stale) = arghda_core::workspace_verdicts(&dag_doc, &proven, &stale_names);
+        verdicts.extend(wv);
+        stale.extend(ws_stale);
+    }
+
+    // Source 2 — `--check`: typecheck each node for real (honest exit codes).
+    // A fresh check is authoritative, so it overrides workspace verdicts.
     if do_check {
         let route = Dispatch::parse(dispatch)?;
         for node in &dag_doc.nodes {
             let file = include_root.join(&node.file);
             let outcome = route.run(backend.as_ref(), &file, include_root)?;
             if outcome.available {
                 verdicts.insert(node.id.clone(), outcome.verdict);
+                stale.remove(&node.id); // a fresh real verdict is not stale
             }
         }
     }

src/reason/mod.rs

@@ -316,6 +316,37 @@ pub fn build(
     }
 }
 
+/// Derive reasoning inputs from a workspace's `proven/` state, WITHOUT
+/// re-checking: a node whose file basename is in `proven_basenames` gets a
+/// `Proven` self-verdict; if that basename is also in `stale_basenames`
+/// (content/closure hash changed since promotion) the node id is added to the
+/// returned stale set, so [`build`]'s fold demotes it to `Unknown` and
+/// propagates. Returns `(verdicts, stale)` for [`build`]. Matched by basename
+/// — the workspace stores files flat by basename, so distinct modules that
+/// share a basename would collide (a documented limitation).
+pub fn workspace_verdicts(
+    dag: &DagDocument,
+    proven_basenames: &BTreeSet<String>,
+    stale_basenames: &BTreeSet<String>,
+) -> (BTreeMap<String, Verdict>, BTreeSet<String>) {
+    let mut verdicts = BTreeMap::new();
+    let mut stale = BTreeSet::new();
+    for node in &dag.nodes {
+        let base = node
+            .file
+            .file_name()
+            .and_then(|s| s.to_str())
+            .unwrap_or_default();
+        if proven_basenames.contains(base) {
+            verdicts.insert(node.id.clone(), Verdict::Proven);
+            if stale_basenames.contains(base) {
+                stale.insert(node.id.clone());
+            }
+        }
+    }
+    (verdicts, stale)
+}
+
 /// The set of ids reachable from any root by following adjacency edges.
 fn reachable(roots: &[String], adj: &BTreeMap<String, Vec<(String, Junct)>>) -> BTreeSet<String> {
     let mut seen: BTreeSet<String> = BTreeSet::new();
@@ -592,4 +623,62 @@ mod tests {
             assert!(v["edges"][0].get(k).is_some(), "reason edge missing `{k}`");
         }
     }
+
+    // ── M3 follow-on: workspace-fed verdicts + staleness ─────────────────
+    fn two_node_dag() -> crate::dag::DagDocument {
+        use crate::dag::{DagDocument, DagNode, LintSummary};
+        use crate::graph::Edge;
+        use std::path::PathBuf;
+        let mk = |id: &str, file: &str| DagNode {
+            id: id.to_string(),
+            file: PathBuf::from(file),
+            status: "clean",
+            lint: LintSummary::default(),
+            headlines: vec![],
+        };
+        DagDocument {
+            version: "0.1",
+            include_root: PathBuf::from("/r"),
+            entry_modules: vec![PathBuf::from("/r/All.agda")],
+            generated_at: "t".to_string(),
+            nodes: vec![mk("All", "All.agda"), mk("Good", "Good.agda")],
+            edges: vec![Edge {
+                from: "All".to_string(),
+                to: "Good".to_string(),
+                kind: "imports",
+            }],
+            blocked: vec![],
+        }
+    }
+
+    #[test]
+    fn workspace_proven_lights_the_cone_and_stale_demotes() {
+        use crate::prover::Agda;
+        let dag = two_node_dag();
+        let proven: BTreeSet<String> = ["Good.agda".to_string()].into_iter().collect();
+
+        // Fresh proven: Good → Proven; All (not proven) → not set.
+        let (v, s) = workspace_verdicts(&dag, &proven, &BTreeSet::new());
+        assert_eq!(v.get("Good"), Some(&Verdict::Proven));
+        assert!(!v.contains_key("All"));
+        assert!(s.is_empty());
+        let doc = build(dag.clone(), &Agda, &v, &s);
+        let eff =
+            |d: &ReasonDocument, id: &str| d.nodes.iter().find(|n| n.id == id).unwrap().effective;
+        assert_eq!(eff(&doc, "Good"), Verdict::Proven);
+        assert_eq!(eff(&doc, "All"), Verdict::Unknown); // not proven itself
+
+        // Stale proven: Good is proven-but-stale → demoted to Unknown, and it
+        // drags its importer All down too.
+        let stale: BTreeSet<String> = ["Good.agda".to_string()].into_iter().collect();
+        let (v2, s2) = workspace_verdicts(&dag, &proven, &stale);
+        assert!(s2.contains("Good"));
+        let doc2 = build(dag, &Agda, &v2, &s2);
+        assert_eq!(
+            eff(&doc2, "Good"),
+            Verdict::Unknown,
+            "stale proven → unknown"
+        );
+        assert_eq!(eff(&doc2, "All"), Verdict::Unknown);
+    }
 }