feat(graph): multi-root reachability for orphan detection

The orphan rule previously computed reachability from a single entry
module, so on a corpus with several CI roots it over-reported: every
module reachable only from a non-`All.agda` root looked orphaned. The
echo-types dogfood made this concrete — 38 orphan hits, most of them
false.

Changes
- `graph::discover_roots` auto-discovers CI roots (`All.agda`/`Smoke.agda`
  at any depth); `graph::reachable_from_roots` unions reachability across
  them.
- `LintContext.entry_module: &Path` -> `entry_modules: &[PathBuf]`; the
  orphan rule flags a module only if it is unreachable from *every* root
  and is not itself a root.
- `scan` and `dag` share `resolve_roots_and_rules`: explicit `--entry`
  (now repeatable) wins, else auto-discover; if no roots are found the
  orphan rule is dropped (with a note) rather than flagging everything.
- `dag` document now carries `entry_modules` (the roots it used).

Verification
- cargo fmt/clippy(-D warnings)/test clean; 21 tests (added a graph unit
  test proving union reachability: Used via All + Other via Smoke are
  reachable, Orphan via neither is not).
- Re-dogfooded on echo-types (193 modules, 5 discovered roots): orphan
  reports drop 38 -> 17 genuine orphans (the experimental/echo-additive
  tree incl. VarianceGate.agda, plus standalone scratch files); the
  `dag` clean count rises 155 -> 176. postulate/pragma hits unchanged.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs

Author: claude

README.md

@@ -14,7 +14,10 @@ record.
 - Filesystem watcher (`notify`-based)
 - Linter rules:
   - `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}`
-  - `orphan-module` — `.agda` file not imported from `All.agda`
+  - `orphan-module` — `.agda` file not reachable from any CI root (roots
+    are auto-discovered as `All.agda`/`Smoke.agda`, or passed via `--entry`;
+    reachability is the *union*, so a module verified from any root is not
+    an orphan)
   - `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` comment
 - Workspace state machine — transitions are file moves, each logged to
   `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`,
@@ -28,9 +31,14 @@ record.
   `reject`, `requeue`, `invalidate`, `events`, `watch`
 
 Dogfooded against the echo-types corpus (193 modules): `dag` emits the
-903-edge import graph; `scan` flags the known real orphan
-(`experimental/echo-additive/VarianceGate.agda`) and the files deliberately
-outside the `--safe --without-K` kernel cone.
+903-edge import graph; multi-root discovery (5 roots: `All.agda`,
+`Smoke.agda`, `Ordinal/Buchholz/Smoke.agda`, `characteristic/All.agda`,
+`examples/All.agda`) narrows orphan reports from 38 to the 17 genuine
+orphans — the `experimental/echo-additive/` tree (including
+`VarianceGate.agda`, the orphan the 2026-06-16 trust audit found by hand)
+plus standalone scratch files. `scan` also flags the files deliberately
+outside the `--safe --without-K` kernel cone (`Fidelity.agda`, the cubical
+island, the postulated shadow).
 
 Not yet: the remaining lint rules (`missing-without-k`, `unpinned-headline`,
 `unused-import`, `tab-mix`), content-hash invalidation of `proven`, the

src/dag.rs

@@ -46,24 +46,25 @@ pub struct Blocked {
 pub struct DagDocument {
     pub version: &'static str,
     pub include_root: PathBuf,
-    pub entry_module: PathBuf,
+    pub entry_modules: Vec<PathBuf>,
     pub generated_at: String,
     pub nodes: Vec<DagNode>,
     pub edges: Vec<Edge>,
     pub blocked: Vec<Blocked>,
 }
 
 /// Build the DAG document for the source tree at `include_root`, using
-/// `entry` for the orphan-reachability rule and `rules` as the lint pack.
+/// `entry_modules` (the union of CI roots) for the orphan-reachability rule
+/// and `rules` as the lint pack.
 pub fn build(
     include_root: &Path,
-    entry: &Path,
+    entry_modules: &[PathBuf],
     rules: &[Box<dyn LintRule>],
 ) -> Result<DagDocument> {
     let graph = graph::build(include_root)?;
     let ctx = LintContext {
         include_root,
-        entry_module: entry,
+        entry_modules,
     };
 
     let mut nodes = Vec::with_capacity(graph.nodes.len());
@@ -107,7 +108,7 @@ pub fn build(
     Ok(DagDocument {
         version: "0.1",
         include_root: include_root.to_path_buf(),
-        entry_module: entry.to_path_buf(),
+        entry_modules: entry_modules.to_vec(),
         generated_at: now_rfc3339(),
         nodes,
         edges: graph.edges,

src/graph.rs

@@ -113,6 +113,44 @@ pub fn transitive_imports(entry: &Path, include_root: &Path) -> Result<HashSet<S
     Ok(reachable)
 }
 
+/// Union of the modules reachable from each root in `roots`. A module
+/// verified from *any* CI entry point counts as reachable.
+pub fn reachable_from_roots(roots: &[PathBuf], include_root: &Path) -> Result<HashSet<String>> {
+    let mut all = HashSet::new();
+    for root in roots {
+        for m in transitive_imports(root, include_root)? {
+            all.insert(m);
+        }
+    }
+    Ok(all)
+}
+
+/// Discover conventional CI root modules under `include_root`: every file
+/// named `All.agda` or `Smoke.agda`, at any depth. These are the entry
+/// points an estate `--safe --without-K` workspace registers its verified
+/// suite from (e.g. echo-types has `All.agda`, `Smoke.agda`,
+/// `characteristic/All.agda`, `examples/All.agda`, `tutorial/All.agda`).
+pub fn discover_roots(include_root: &Path) -> Vec<PathBuf> {
+    let mut roots = Vec::new();
+    for entry in WalkDir::new(include_root)
+        .into_iter()
+        .filter_map(|e| e.ok())
+    {
+        let path = entry.path();
+        if path.extension().and_then(|s| s.to_str()) != Some("agda") {
+            continue;
+        }
+        if matches!(
+            path.file_name().and_then(|s| s.to_str()),
+            Some("All.agda") | Some("Smoke.agda")
+        ) {
+            roots.push(path.to_path_buf());
+        }
+    }
+    roots.sort();
+    roots
+}
+
 /// A node in the import graph: a `.agda` source file and its module name.
 #[derive(Clone, Debug, Serialize)]
 pub struct GraphNode {
@@ -221,4 +259,35 @@ mod tests {
         assert!(imports.contains(&"Baz".to_string()));
         assert!(!imports.iter().any(|i| i.contains("Ignored")));
     }
+
+    #[test]
+    fn discover_and_reach_over_multiple_roots() {
+        let tmp = tempfile::tempdir().unwrap();
+        let r = tmp.path();
+        std::fs::write(r.join("All.agda"), "module All where\nopen import Used\n").unwrap();
+        std::fs::write(
+            r.join("Smoke.agda"),
+            "module Smoke where\nopen import Other\n",
+        )
+        .unwrap();
+        std::fs::write(r.join("Used.agda"), "module Used where\n").unwrap();
+        std::fs::write(r.join("Other.agda"), "module Other where\n").unwrap();
+        std::fs::write(r.join("Orphan.agda"), "module Orphan where\n").unwrap();
+
+        let roots = discover_roots(r);
+        let names: Vec<String> = roots
+            .iter()
+            .map(|p| p.file_name().unwrap().to_str().unwrap().to_string())
+            .collect();
+        assert_eq!(roots.len(), 2, "discovers All.agda + Smoke.agda: {names:?}");
+        assert!(names.contains(&"All.agda".to_string()));
+        assert!(names.contains(&"Smoke.agda".to_string()));
+
+        // Reachability is the UNION: Used (via All) and Other (via Smoke)
+        // are both reachable; Orphan (via neither) is not.
+        let reachable = reachable_from_roots(&roots, r).unwrap();
+        assert!(reachable.contains("Used"));
+        assert!(reachable.contains("Other"));
+        assert!(!reachable.contains("Orphan"));
+    }
 }

src/lint/mod.rs

@@ -1,6 +1,6 @@
 use crate::diagnostic::LintReport;
 use anyhow::Result;
-use std::path::Path;
+use std::path::{Path, PathBuf};
 
 pub mod orphan_module;
 pub mod postulate;
@@ -12,8 +12,10 @@ pub struct LintContext<'a> {
     /// Agda include root; `.agda` files' module names are computed
     /// relative to this path.
     pub include_root: &'a Path,
-    /// Path to the `All.agda` (or equivalent) entry module.
-    pub entry_module: &'a Path,
+    /// The root modules (e.g. `All.agda`, `Smoke.agda`). Reachability is
+    /// computed from the *union* of these, so a module verified from any
+    /// CI entry point is not an orphan.
+    pub entry_modules: &'a [PathBuf],
 }
 
 pub trait LintRule: Send + Sync {

src/lint/orphan_module.rs

@@ -1,6 +1,6 @@
 use super::{LintContext, LintRule};
 use crate::diagnostic::{Diagnostic, LintReport, Severity};
-use crate::graph::{module_name_of, transitive_imports};
+use crate::graph::{module_name_of, reachable_from_roots};
 use anyhow::{Context, Result};
 use std::path::Path;
 
@@ -16,28 +16,27 @@ impl LintRule for OrphanModule {
             return Ok(()); // file sits outside include_root; nothing to say
         };
 
-        // The entry module itself is never an orphan of itself.
-        if Some(module.as_str()) == module_name_of(ctx.entry_module, ctx.include_root).as_deref() {
+        // A root module is never an orphan of itself.
+        let is_root = ctx
+            .entry_modules
+            .iter()
+            .any(|root| module_name_of(root, ctx.include_root).as_deref() == Some(module.as_str()));
+        if is_root {
             return Ok(());
         }
 
-        let reachable =
-            transitive_imports(ctx.entry_module, ctx.include_root).with_context(|| {
-                format!(
-                    "computing transitive imports from {}",
-                    ctx.entry_module.display()
-                )
-            })?;
+        let reachable = reachable_from_roots(ctx.entry_modules, ctx.include_root)
+            .context("computing reachability from root modules")?;
 
         if !reachable.contains(&module) {
             report.push(Diagnostic {
                 rule: self.name().to_string(),
                 severity: Severity::HardBlock,
                 file: file.to_path_buf(),
                 message: format!(
-                    "module `{}` is not reachable via imports from `{}`",
+                    "module `{}` is not reachable via imports from any of the {} root module(s)",
                     module,
-                    ctx.entry_module.display()
+                    ctx.entry_modules.len()
                 ),
                 line: None,
             });

src/lint/postulate.rs

@@ -73,9 +73,10 @@ mod tests {
     fn lint_str(body: &str) -> LintReport {
         let tmp = tempfile::NamedTempFile::new().unwrap();
         std::fs::write(tmp.path(), body).unwrap();
+        let roots = [tmp.path().to_path_buf()];
         let ctx = LintContext {
             include_root: tmp.path().parent().unwrap(),
-            entry_module: tmp.path(),
+            entry_modules: &roots,
         };
         let rules: Vec<Box<dyn LintRule>> = vec![Box::new(UnjustifiedPostulate)];
         run_lints(tmp.path(), &ctx, &rules).unwrap()