From f61876d96cdaa0c33ef37f8b3f04a5692b48c52a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 10:39:19 +0000 Subject: [PATCH] ArghDA M3 follow-on: workspace-fed verdicts + staleness in `reason` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Flying-Logic reasoning graph can now source REAL prover verdicts from a four-state workspace's `proven/` state without re-running any tool, and demote a stale-proven node back to unknown — honest by construction, never fabricated. - `reason::workspace_verdicts(dag, proven, stale)` — pure mapping: a node whose file basename is in the workspace's `proven/` set → Proven; if that same file is stale (content/closure hash changed since promotion) it is added to the stale set, so the existing demote-only fold lowers it to Unknown. Matched by file basename (documented collision caveat). Re-exported from lib.rs. - `arghda reason --workspace `: reads the proven + stale-proven basename sets off the workspace (Workspace::list / stale_proven) and feeds them in. `--check` stays authoritative — a fresh typecheck overrides the workspace verdict and clears staleness for that node. - Evidence strings are honest: "prover: proven" for a fresh promotion, "prover: proven; stale: closure hash changed" for a demoted stale one. Verification: `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo test` (130 pass, +1 reason unit), `check-spdx.sh` all green. Dogfooded end-to-end: fresh proven leaf → effective proven, un-proven root → unknown; editing the proven file on disk → node demoted to unknown with the stale evidence string. Completes the refinement follow-ons bucket (M4 .ipkg roots, M6 axiom audit, M3 workspace verdicts). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/6a2/STATE.a2ml | 23 +++++++-- src/lib.rs | 4 +- src/main.rs | 38 ++++++++++++-- src/reason/mod.rs | 89 ++++++++++++++++++++++++++++++++ 4 files changed, 145 insertions(+), 9 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f7cc55b..32de7ba 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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 --workspace +# `: 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 ` 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 diff --git a/src/lib.rs b/src/lib.rs index dbed3ab..0def871 100644 --- a/src/lib.rs +++ b/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}; diff --git a/src/main.rs b/src/main.rs index 4c222ee..dd9daa4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -151,6 +151,12 @@ enum Cmd { /// `echidna[=]`. #[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, }, /// 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,12 +577,29 @@ 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 = 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 = + 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 { @@ -580,6 +607,7 @@ fn reason( 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 } } } diff --git a/src/reason/mod.rs b/src/reason/mod.rs index 3ce724e..8154e86 100644 --- a/src/reason/mod.rs +++ b/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, + stale_basenames: &BTreeSet, +) -> (BTreeMap, BTreeSet) { + 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>) -> BTreeSet { let mut seen: BTreeSet = 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 = ["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 = ["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); + } }