diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index ee53bcf..e8aa259 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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)", ] diff --git a/src/config.rs b/src/config.rs index 59d0ef6..f4b7a19 100644 --- a/src/config.rs +++ b/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, } +#[derive(Debug, Default, Deserialize)] +#[serde(deny_unknown_fields)] +struct ProvenTable { + /// Source-tree include root for transitive `proven` closure hashing. + include_root: Option, +} + /// Parse config TOML text into a [`RuleConfig`], overlaying built-in defaults. fn parse(text: &str) -> Result { let file: ConfigFile = toml::from_str(text).context("parsing .arghda/config.toml")?; @@ -69,6 +78,29 @@ pub fn load_from_dir(base: &Path) -> Result { } } +/// The `[proven] include_root` (if any) from `/.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> { + 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")) + ); + } } diff --git a/src/graph.rs b/src/graph.rs index f912a49..a0a7869 100644 --- a/src/graph.rs +++ b/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(); diff --git a/src/proven.rs b/src/proven.rs index 55d2b0e..b99cb7c 100644 --- a/src/proven.rs +++ b/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, pub promoted_at: String, } @@ -67,3 +76,34 @@ pub fn hash_file(path: &Path) -> Result { 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 { + let mut deps: BTreeMap = 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())) +} diff --git a/src/workspace.rs b/src/workspace.rs index 3a0dcd0..4c4c410 100644 --- a/src/workspace.rs +++ b/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> { 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 { diff --git a/tests/proven.rs b/tests/proven.rs index 915d6d6..6aa965c 100644 --- a/tests/proven.rs +++ b/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();