feat(proven): transitive-import closure hashing + cycle-safety regression

.machine_readable/6a2/STATE.a2ml

@@ -27,7 +27,7 @@ milestones = [
   { name = "State machine (claim/promote/reject/requeue/invalidate) + events.jsonl", completion = 100 },
   { name = "`check` command (Agda typecheck + lint verdict)", completion = 100 },
   { name = "Multi-root reachability (union of discovered CI roots)", completion = 100 },
-  { name = "Content-hash invalidation of proven (file-level; transitive imports deferred)", completion = 75 },
+  { name = "Content-hash invalidation of proven (file-level + transitive-import closure via [proven] include_root)", completion = 100 },
   { name = "Operator config (.arghda/config.toml + --headline-pattern + --config)", completion = 100 },
   { name = "RSR / standards alignment (.machine_readable, README.adoc, EXPLAINME, LICENSE, .well-known)", completion = 100 },
   { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 },
@@ -40,8 +40,8 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "Template-applicability: rsr-profile.a2ml declares preset rust-cli (landed); estate policy + gate model + reference checker filed in hyperpolymath/standards#391. Follow-up: wire scripts/check-rsr-profile.sh into CI once standards#391 lands.",
-  "Extend content-hash invalidation to cover transitive imports (needs include-root tracking)",
+  "Template-applicability: rsr-profile.a2ml declares capabilities (landed); estate policy + gate model + reference checker landed in hyperpolymath/standards#391 + #392 (pure capability-gating). Follow-up: wire the standards rsr-profile check into CI.",
+  "Transitive-import closure hashing landed (workspace [proven] include_root); follow-up: also expose it as a --include-root CLI flag on promote/stale.",
   "Serve /.well-known/groove for PanLL discovery (Groove protocol)",
   "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
 ]

src/config.rs

@@ -21,7 +21,7 @@
 use crate::lint::RuleConfig;
 use anyhow::{Context, Result};
 use serde::Deserialize;
-use std::path::Path;
+use std::path::{Path, PathBuf};
 
 /// Conventional config location, relative to a source tree or workspace root.
 pub const CONFIG_REL_PATH: &str = ".arghda/config.toml";
@@ -33,6 +33,8 @@ pub const CONFIG_REL_PATH: &str = ".arghda/config.toml";
 struct ConfigFile {
     #[serde(default)]
     lint: LintTable,
+    #[serde(default)]
+    proven: ProvenTable,
 }
 
 #[derive(Debug, Default, Deserialize)]
@@ -42,6 +44,13 @@ struct LintTable {
     headline_pattern: Option<String>,
 }
 
+#[derive(Debug, Default, Deserialize)]
+#[serde(deny_unknown_fields)]
+struct ProvenTable {
+    /// Source-tree include root for transitive `proven` closure hashing.
+    include_root: Option<String>,
+}
+
 /// Parse config TOML text into a [`RuleConfig`], overlaying built-in defaults.
 fn parse(text: &str) -> Result<RuleConfig> {
     let file: ConfigFile = toml::from_str(text).context("parsing .arghda/config.toml")?;
@@ -69,6 +78,29 @@ pub fn load_from_dir(base: &Path) -> Result<RuleConfig> {
     }
 }
 
+/// The `[proven] include_root` (if any) from `<base>/.arghda/config.toml`,
+/// resolved relative to `base` when given as a relative path. This is the
+/// source tree against which a promoted file's transitive-import closure is
+/// hashed for staleness; `None` means own-bytes hashing only.
+pub fn proven_include_root(base: &Path) -> Result<Option<PathBuf>> {
+    let candidate = base.join(CONFIG_REL_PATH);
+    if !candidate.is_file() {
+        return Ok(None);
+    }
+    let text = std::fs::read_to_string(&candidate)
+        .with_context(|| format!("reading config {}", candidate.display()))?;
+    let file: ConfigFile =
+        toml::from_str(&text).with_context(|| format!("parsing config {}", candidate.display()))?;
+    Ok(file.proven.include_root.map(|p| {
+        let p = PathBuf::from(p);
+        if p.is_absolute() {
+            p
+        } else {
+            base.join(p)
+        }
+    }))
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -122,4 +154,42 @@ mod tests {
         let cfg = load_from_dir(dir.path()).unwrap();
         assert_eq!(cfg.headline_pattern, "^[A-Z].*$");
     }
+
+    #[test]
+    fn proven_include_root_absent_is_none() {
+        let dir = tempfile::tempdir().unwrap();
+        assert!(proven_include_root(dir.path()).unwrap().is_none());
+        // A [lint]-only config also yields no include root.
+        std::fs::create_dir_all(dir.path().join(".arghda")).unwrap();
+        std::fs::write(dir.path().join(CONFIG_REL_PATH), "[lint]\n").unwrap();
+        assert!(proven_include_root(dir.path()).unwrap().is_none());
+    }
+
+    #[test]
+    fn proven_include_root_resolves_absolute_and_relative() {
+        let dir = tempfile::tempdir().unwrap();
+        std::fs::create_dir_all(dir.path().join(".arghda")).unwrap();
+
+        // Relative is resolved against the workspace base.
+        std::fs::write(
+            dir.path().join(CONFIG_REL_PATH),
+            "[proven]\ninclude_root = \"src\"\n",
+        )
+        .unwrap();
+        assert_eq!(
+            proven_include_root(dir.path()).unwrap(),
+            Some(dir.path().join("src"))
+        );
+
+        // Absolute is taken as-is.
+        std::fs::write(
+            dir.path().join(CONFIG_REL_PATH),
+            "[proven]\ninclude_root = \"/abs/tree\"\n",
+        )
+        .unwrap();
+        assert_eq!(
+            proven_include_root(dir.path()).unwrap(),
+            Some(std::path::PathBuf::from("/abs/tree"))
+        );
+    }
 }

src/graph.rs

@@ -263,6 +263,20 @@ mod tests {
         assert!(!imports.iter().any(|i| i.contains("Ignored")));
     }
 
+    #[test]
+    fn transitive_imports_terminates_on_a_cycle() {
+        // A <-> B mutual import is illegal in Agda, but a half-written file
+        // under active edit in `working/` can transiently produce one. The
+        // `reachable` visited-set must stop the walk from looping forever.
+        let tmp = tempfile::tempdir().unwrap();
+        let r = tmp.path();
+        std::fs::write(r.join("A.agda"), "module A where\nopen import B\n").unwrap();
+        std::fs::write(r.join("B.agda"), "module B where\nopen import A\n").unwrap();
+        let reach = transitive_imports(&r.join("A.agda"), r).unwrap();
+        assert!(reach.contains("A"));
+        assert!(reach.contains("B"));
+    }
+
     #[test]
     fn discover_and_reach_over_multiple_roots() {
         let tmp = tempfile::tempdir().unwrap();

src/proven.rs

@@ -9,10 +9,12 @@
 //! can be sent back to `inbox` — the `proven -> inbox` invalidation from
 //! `docs/arghda-spec.adoc`.
 //!
-//! v1 hashes the file content only. Hashing a file *plus its transitive
-//! imports* (the spec's full form) needs the workspace to know the source
-//! tree's include root, which the flat triage layout does not yet carry;
-//! that is a documented follow-on.
+//! [`hash_file`] hashes the file's own bytes. [`closure_hash`] additionally
+//! folds in every transitive import that resolves inside a source-tree
+//! include root — the spec's full form, so a promoted file goes stale when a
+//! proof *under* it changes, not only when it is edited. The include root is
+//! a workspace property (`[proven] include_root` in `.arghda/config.toml`);
+//! when it is unset, only own-bytes hashing applies.
 
 use crate::hash::sha256_hex;
 use anyhow::{Context, Result};
@@ -26,7 +28,14 @@ pub const HASHES_FILE: &str = "hashes.json";
 /// What was recorded when a file entered `proven`.
 #[derive(Clone, Debug, Serialize, Deserialize)]
 pub struct ProvenRecord {
+    /// SHA-256 of the file's own bytes.
     pub sha256: String,
+    /// SHA-256 of the file *and its transitive-import closure*, recorded when
+    /// a source-tree include root was known at promotion. `None` for files
+    /// promoted without one (own-bytes checking only); absent in older
+    /// manifests, which still load.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub closure_sha256: Option<String>,
     pub promoted_at: String,
 }
 
@@ -67,3 +76,34 @@ pub fn hash_file(path: &Path) -> Result<String> {
     let bytes = fs::read(path).with_context(|| format!("reading {}", path.display()))?;
     Ok(sha256_hex(&bytes))
 }
+
+/// SHA-256 over `file`'s own bytes plus the bytes of every transitive import
+/// that resolves to a file inside `include_root`, in deterministic module
+/// order. This is the spec's full `proven` invalidation form: a promoted file
+/// is stale not only when it is edited, but when any proof it depends on is.
+///
+/// `file` may live outside `include_root` (the usual case — it has been moved
+/// into the triage `proven/` dir); its imports are still resolved against the
+/// source tree at `include_root`. Imports that do not resolve in-tree (stdlib
+/// / external) are skipped, exactly as the import graph omits them.
+pub fn closure_hash(file: &Path, include_root: &Path) -> Result<String> {
+    let mut deps: BTreeMap<String, String> = BTreeMap::new();
+    for module in crate::graph::transitive_imports(file, include_root)? {
+        let path = crate::graph::module_to_path(&module, include_root);
+        if path.is_file() {
+            deps.insert(module, hash_file(&path)?);
+        }
+    }
+    // Entry's own hash first, then sorted `module\0hash` lines: deterministic,
+    // and sensitive to a dependency being added, removed, or edited.
+    let mut buf = String::with_capacity(72 * (deps.len() + 1));
+    buf.push_str(&hash_file(file)?);
+    buf.push('\n');
+    for (module, hash) in &deps {
+        buf.push_str(module);
+        buf.push('\0');
+        buf.push_str(hash);
+        buf.push('\n');
+    }
+    Ok(sha256_hex(buf.as_bytes()))
+}

src/workspace.rs

@@ -128,13 +128,20 @@ impl Workspace {
 
         // Maintain the proven content-hash manifest: record on entry to
         // `proven`, drop on exit. This is what lets `stale_proven` detect a
-        // file edited after promotion.
+        // file edited after promotion. When the workspace declares a source
+        // tree (`[proven] include_root`), also record the transitive-import
+        // closure hash so an edit to a *dependency* invalidates the file too.
         if to == State::Proven {
             let mut manifest = proven::load(&self.root)?;
+            let closure_sha256 = match crate::config::proven_include_root(&self.root)? {
+                Some(root) => Some(proven::closure_hash(&dst, &root)?),
+                None => None,
+            };
             manifest.entries.insert(
                 file_name.to_string(),
                 ProvenRecord {
                     sha256: proven::hash_file(&dst)?,
+                    closure_sha256,
                     promoted_at: ev.ts.clone(),
                 },
             );
@@ -156,6 +163,7 @@ impl Workspace {
     /// for `proven -> inbox` invalidation.
     pub fn stale_proven(&self) -> Result<Vec<StaleEntry>> {
         let manifest = proven::load(&self.root)?;
+        let include_root = crate::config::proven_include_root(&self.root)?;
         let mut out = Vec::new();
         for path in self.list(State::Proven)? {
             let Some(name) = path.file_name().and_then(|s| s.to_str()) else {
@@ -165,7 +173,15 @@ impl Workspace {
             let reason = match manifest.entries.get(name) {
                 None => Some("no recorded hash"),
                 Some(rec) if rec.sha256 != current => Some("content changed since promotion"),
-                Some(_) => None,
+                // Own bytes match: if a closure hash was recorded and the
+                // source tree is still known, a mismatch now means a
+                // transitive import changed under the file.
+                Some(rec) => match (&rec.closure_sha256, &include_root) {
+                    (Some(stored), Some(root)) if proven::closure_hash(&path, root)? != *stored => {
+                        Some("a transitive import changed since promotion")
+                    }
+                    _ => None,
+                },
             };
             if let Some(reason) = reason {
                 out.push(StaleEntry {

tests/proven.rs

@@ -63,6 +63,48 @@ fn invalidate_returns_to_inbox_and_drops_the_hash() {
     assert!(!manifest.entries.contains_key("Bar.agda"));
 }
 
+#[test]
+fn editing_a_transitive_import_makes_a_proven_file_stale() {
+    let tmp = tempfile::tempdir().unwrap();
+    let ws = Workspace::init(tmp.path()).unwrap();
+
+    // A source tree (separate from the triage dirs) holding the dependency.
+    let src = tmp.path().join("src");
+    fs::create_dir_all(&src).unwrap();
+    fs::write(src.join("Dep.agda"), "module Dep where\nx = Set\n").unwrap();
+
+    // Point the workspace at that source tree for closure hashing.
+    fs::write(
+        tmp.path().join(".arghda").join("config.toml"),
+        format!("[proven]\ninclude_root = \"{}\"\n", src.display()),
+    )
+    .unwrap();
+
+    // A file that depends on Dep, promoted to proven.
+    fs::write(
+        ws.state_dir(State::Working).join("Main.agda"),
+        "module Main where\nopen import Dep\n",
+    )
+    .unwrap();
+    ws.transition("Main.agda", State::Working, State::Proven, None)
+        .unwrap();
+
+    // Promotion recorded a closure hash, and nothing is stale yet.
+    let manifest = proven::load(tmp.path()).unwrap();
+    assert!(manifest.entries["Main.agda"].closure_sha256.is_some());
+    assert!(ws.stale_proven().unwrap().is_empty());
+
+    // Edit the DEPENDENCY, not the proven file itself -> stale via closure.
+    fs::write(src.join("Dep.agda"), "module Dep where\nx = Set\ny = Set\n").unwrap();
+    let stale = ws.stale_proven().unwrap();
+    assert_eq!(stale.len(), 1);
+    assert_eq!(stale[0].file, "Main.agda");
+    assert_eq!(
+        stale[0].reason,
+        "a transitive import changed since promotion"
+    );
+}
+
 #[test]
 fn proven_file_without_a_record_is_stale() {
     let tmp = tempfile::tempdir().unwrap();