feat: finish the v0.1 engine — dag, check, state machine, event stream

Implements the spec's first-sprint items 4/5/6 (arghda-spec.adoc) plus a
soundness lint, all verified with the real Agda toolchain (2.6.3) and
dogfooded against the echo-types corpus.

New capabilities
- `graph` module: the Agda import graph is now first-class (nodes + typed
  `imports` edges, deterministic/sorted output). Lifted out of the
  `orphan-module` rule, which had computed the edges and thrown them away;
  the rule now reuses it.
- `dag` command: emits the dependency-DAG JSON contract a visual layer
  consumes — nodes with lint-derived status (clean/warn/blocked), import
  edges, and a `blocked` list (self-blocked by rule + prerequisite-blocked
  by an unclean import).
- Workspace state machine: `transition`/`state_of` move files between the
  four triage states, validated against the spec's transition table, each
  move appended to `.arghda/events.jsonl`. CLI: `claim`, `promote`,
  `reject`, `requeue`, `invalidate`, `events`.
- `check` command: runs Agda on a file and combines the typecheck verdict
  with the lint report (`proven-eligible` / `rejected` / `agda-unavailable`).
  Degrades gracefully when `agda` is not on PATH.
- `event` module: typed append-only JSONL event log + reader.
- `agda` module: typecheck invocation with graceful NotFound handling.
- `timestamp` module: dependency-free RFC 3339 UTC (keeps the build
  hermetic against the committed lockfile).
- New lint rule `unjustified-postulate` (hard-block): a `postulate` opener
  with no adjacent `-- JUSTIFY:` comment.

Verification
- cargo fmt/clippy(-D warnings)/build/test all clean; 20 tests
  (11 unit + 9 integration: dag, transitions, smoke).
- `check` exercised against real Agda: clean file -> proven-eligible;
  typechecking file missing --safe -> rejected by lint; type error ->
  rejected by agda (exit 42); JSON output verified.
- `dag`/`scan` dogfooded on echo-types (193 modules): 903 import edges;
  `scan` independently rediscovers the orphan the 2026-06-16 trust audit
  found by hand (VarianceGate.agda) and the files outside the
  --safe --without-K kernel cone (Fidelity.agda, the cubical island, the
  postulated shadow).

Deferred (next slice): remaining lint rules, content-hash invalidation of
`proven`, the Groove service manifest, and the `.machine_readable/` RSR
retrofit.

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

Author: claude

README.md

@@ -12,12 +12,29 @@ record.
 - `Workspace` struct with four-state dir layout (`inbox`, `working`,
   `proven`, `rejected`)
 - Filesystem watcher (`notify`-based)
-- Two linter rules:
+- Linter rules:
   - `missing-safe-pragma` — file lacks `{-# OPTIONS --safe --without-K #-}`
   - `orphan-module` — `.agda` file not imported from `All.agda`
-- CLI (`arghda`) with subcommands: `init`, `scan`, `watch`
-
-Not yet: `promote`, `reject`, `dag` (v0.1.x).
+  - `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`,
+  `invalidate`)
+- `dag` — emits the dependency-DAG JSON (nodes + import edges + blocked
+  list) for a source tree: the contract a visual layer consumes
+- `check` — runs Agda on a file and combines the typecheck verdict with the
+  lint report (degrades gracefully when `agda` is absent)
+- First-class import graph (the `graph` module, lifted out of the orphan rule)
+- CLI (`arghda`): `init`, `scan`, `check`, `dag`, `claim`, `promote`,
+  `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.
+
+Not yet: the remaining lint rules (`missing-without-k`, `unpinned-headline`,
+`unused-import`, `tab-mix`), content-hash invalidation of `proven`, the
+Groove service manifest, and the `.machine_readable/` RSR retrofit.
 
 ## Build
 

src/agda.rs

@@ -0,0 +1,81 @@
+//! Shelling out to `agda` to typecheck a file.
+//!
+//! ArghDA never proves anything itself — it asks Agda. This module runs
+//! the typechecker and captures the verdict. If `agda` is not on `PATH`
+//! it degrades gracefully (`available: false`) rather than erroring, so
+//! the rest of the engine still works in an Agda-less environment (CI
+//! linting, DAG extraction, triage moves).
+
+use anyhow::Result;
+use serde::Serialize;
+use std::path::Path;
+use std::process::Command;
+
+const TAIL_LINES: usize = 40;
+
+/// Result of a typecheck attempt.
+#[derive(Clone, Debug, Serialize)]
+pub struct AgdaOutcome {
+    /// Whether the `agda` binary was found and executed.
+    pub available: bool,
+    /// Process exit code, if the process ran.
+    pub exit_code: Option<i32>,
+    /// `true` iff agda exited 0.
+    pub ok: bool,
+    /// Last few lines of combined stdout+stderr (for surfacing errors).
+    pub output_tail: String,
+}
+
+impl AgdaOutcome {
+    fn unavailable() -> Self {
+        Self {
+            available: false,
+            exit_code: None,
+            ok: false,
+            output_tail: String::new(),
+        }
+    }
+}
+
+/// Typecheck `file` with `include_root` on the search path
+/// (`agda -i <include_root> <file>`).
+pub fn check_file(file: &Path, include_root: &Path) -> Result<AgdaOutcome> {
+    let output = Command::new("agda")
+        .arg("-i")
+        .arg(include_root)
+        .arg(file)
+        .output();
+
+    match output {
+        Ok(out) => {
+            let mut combined = String::from_utf8_lossy(&out.stdout).into_owned();
+            combined.push_str(&String::from_utf8_lossy(&out.stderr));
+            Ok(AgdaOutcome {
+                available: true,
+                exit_code: out.status.code(),
+                ok: out.status.success(),
+                output_tail: tail(&combined, TAIL_LINES),
+            })
+        }
+        Err(e) if e.kind() == std::io::ErrorKind::NotFound => Ok(AgdaOutcome::unavailable()),
+        Err(e) => Err(e.into()),
+    }
+}
+
+fn tail(s: &str, n: usize) -> String {
+    let lines: Vec<&str> = s.lines().collect();
+    let start = lines.len().saturating_sub(n);
+    lines[start..].join("\n")
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn tail_keeps_last_n_lines() {
+        assert_eq!(tail("a\nb\nc\nd", 2), "c\nd");
+        assert_eq!(tail("only", 5), "only");
+        assert_eq!(tail("", 3), "");
+    }
+}

src/dag.rs

@@ -0,0 +1,151 @@
+//! The DAG document — the JSON contract a visual layer consumes.
+//!
+//! Builds on the import graph (`crate::graph`) plus a lint pass over every
+//! node. The schema follows `docs/arghda-spec.adoc`; `status` is honest
+//! about what the engine knows without a typecheck: it is lint-derived
+//! (`clean` / `warn` / `blocked`), not a claim of `proven`. Triage status
+//! (proven/rejected) attaches when files flow through a workspace and are
+//! checked with Agda.
+
+use crate::diagnostic::Severity;
+use crate::graph::{self, Edge};
+use crate::lint::{run_lints, LintContext, LintRule};
+use crate::timestamp::now_rfc3339;
+use anyhow::Result;
+use serde::Serialize;
+use std::collections::{BTreeMap, BTreeSet};
+use std::path::{Path, PathBuf};
+
+/// Per-node lint summary: the rule names that fired, by severity.
+#[derive(Clone, Debug, Default, Serialize)]
+pub struct LintSummary {
+    pub hard_block: Vec<String>,
+    pub warn: Vec<String>,
+}
+
+/// A DAG node: an in-tree module with its lint-derived status.
+#[derive(Clone, Debug, Serialize)]
+pub struct DagNode {
+    pub id: String,
+    pub file: PathBuf,
+    /// `clean` | `warn` | `blocked` (lint-derived; not a proof claim).
+    pub status: &'static str,
+    pub lint: LintSummary,
+}
+
+/// A module that cannot advance, and why.
+#[derive(Clone, Debug, Serialize)]
+pub struct Blocked {
+    pub node: String,
+    pub blocked_by: Vec<String>,
+    pub reason: String,
+}
+
+/// The full emitted document.
+#[derive(Clone, Debug, Serialize)]
+pub struct DagDocument {
+    pub version: &'static str,
+    pub include_root: PathBuf,
+    pub entry_module: 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.
+pub fn build(
+    include_root: &Path,
+    entry: &Path,
+    rules: &[Box<dyn LintRule>],
+) -> Result<DagDocument> {
+    let graph = graph::build(include_root)?;
+    let ctx = LintContext {
+        include_root,
+        entry_module: entry,
+    };
+
+    let mut nodes = Vec::with_capacity(graph.nodes.len());
+    let mut self_blocked: BTreeMap<String, Vec<String>> = BTreeMap::new();
+
+    for gn in &graph.nodes {
+        let abs = include_root.join(&gn.file);
+        let report = run_lints(&abs, &ctx, rules)?;
+
+        let mut summary = LintSummary::default();
+        for d in &report.diagnostics {
+            match d.severity {
+                Severity::HardBlock => summary.hard_block.push(d.rule.clone()),
+                Severity::Warn => summary.warn.push(d.rule.clone()),
+            }
+        }
+        summary.hard_block.sort();
+        summary.hard_block.dedup();
+        summary.warn.sort();
+        summary.warn.dedup();
+
+        let status = if !summary.hard_block.is_empty() {
+            self_blocked.insert(gn.id.clone(), summary.hard_block.clone());
+            "blocked"
+        } else if !summary.warn.is_empty() {
+            "warn"
+        } else {
+            "clean"
+        };
+
+        nodes.push(DagNode {
+            id: gn.id.clone(),
+            file: gn.file.clone(),
+            status,
+            lint: summary,
+        });
+    }
+
+    let blocked = compute_blocked(&self_blocked, &graph.edges);
+
+    Ok(DagDocument {
+        version: "0.1",
+        include_root: include_root.to_path_buf(),
+        entry_module: entry.to_path_buf(),
+        generated_at: now_rfc3339(),
+        nodes,
+        edges: graph.edges,
+        blocked,
+    })
+}
+
+/// A node is blocked if it hard-blocks on its own (`reason` = the rule
+/// names) or if any module it imports is itself hard-blocked
+/// (`blocked_by` = those prerequisites). Both are surfaced so the visual
+/// layer can colour a node red for its own fault *and* show the upstream
+/// wall it is waiting on.
+fn compute_blocked(self_blocked: &BTreeMap<String, Vec<String>>, edges: &[Edge]) -> Vec<Blocked> {
+    let mut out = Vec::new();
+
+    for (node, rules) in self_blocked {
+        out.push(Blocked {
+            node: node.clone(),
+            blocked_by: Vec::new(),
+            reason: rules.join(", "),
+        });
+    }
+
+    // Group each node's hard-blocked direct prerequisites.
+    let mut deps: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
+    for e in edges {
+        if self_blocked.contains_key(&e.to) {
+            deps.entry(e.from.clone()).or_default().insert(e.to.clone());
+        }
+    }
+    for (node, prereqs) in deps {
+        out.push(Blocked {
+            node,
+            blocked_by: prereqs.into_iter().collect(),
+            reason: "prerequisite not clean".to_string(),
+        });
+    }
+
+    out.sort_by(|a, b| (&a.node, &a.reason).cmp(&(&b.node, &b.reason)));
+    out
+}

src/event.rs

@@ -0,0 +1,111 @@
+//! The triage event stream.
+//!
+//! Every state transition appends one JSON object (one line) to
+//! `<workspace>/.arghda/events.jsonl`. The log is append-only and is the
+//! audit trail a downstream visual layer replays to reconstruct history.
+
+use crate::timestamp::now_rfc3339;
+use crate::workspace::State;
+use anyhow::{Context, Result};
+use serde::{Deserialize, Serialize};
+use std::fs::{self, OpenOptions};
+use std::io::Write;
+use std::path::{Path, PathBuf};
+
+/// What happened. Mirrors the transition table in `arghda-spec.adoc`.
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize, Deserialize)]
+#[serde(rename_all = "kebab-case")]
+pub enum EventKind {
+    Claim,
+    Promote,
+    Reject,
+    Requeue,
+    Invalidate,
+}
+
+/// A single transition record.
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct Event {
+    pub ts: String,
+    pub kind: EventKind,
+    pub file: String,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub from: Option<State>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub to: Option<State>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    pub note: Option<String>,
+}
+
+impl Event {
+    pub fn new(kind: EventKind, file: impl Into<String>) -> Self {
+        Self {
+            ts: now_rfc3339(),
+            kind,
+            file: file.into(),
+            from: None,
+            to: None,
+            note: None,
+        }
+    }
+
+    pub fn with_from(mut self, from: State) -> Self {
+        self.from = Some(from);
+        self
+    }
+
+    pub fn with_to(mut self, to: State) -> Self {
+        self.to = Some(to);
+        self
+    }
+
+    pub fn with_note(mut self, note: Option<String>) -> Self {
+        self.note = note;
+        self
+    }
+}
+
+/// File name of the rolling event log, under `<workspace>/.arghda/`.
+pub const EVENTS_FILE: &str = "events.jsonl";
+
+fn events_path(ws_root: &Path) -> PathBuf {
+    ws_root.join(".arghda").join(EVENTS_FILE)
+}
+
+/// Append one event as a JSON line. Creates `.arghda/` if absent.
+pub fn append(ws_root: impl AsRef<Path>, ev: &Event) -> Result<()> {
+    let ws_root = ws_root.as_ref();
+    let meta = ws_root.join(".arghda");
+    fs::create_dir_all(&meta).with_context(|| format!("creating {}", meta.display()))?;
+    let path = events_path(ws_root);
+    let mut line = serde_json::to_string(ev).context("serialising event")?;
+    line.push('\n');
+    let mut f = OpenOptions::new()
+        .create(true)
+        .append(true)
+        .open(&path)
+        .with_context(|| format!("opening {}", path.display()))?;
+    f.write_all(line.as_bytes())
+        .with_context(|| format!("appending to {}", path.display()))?;
+    Ok(())
+}
+
+/// Read the whole event log in order. Empty if the log does not exist yet.
+pub fn read_all(ws_root: impl AsRef<Path>) -> Result<Vec<Event>> {
+    let path = events_path(ws_root.as_ref());
+    if !path.is_file() {
+        return Ok(Vec::new());
+    }
+    let contents =
+        fs::read_to_string(&path).with_context(|| format!("reading {}", path.display()))?;
+    let mut out = Vec::new();
+    for (i, line) in contents.lines().enumerate() {
+        if line.trim().is_empty() {
+            continue;
+        }
+        let ev: Event = serde_json::from_str(line)
+            .with_context(|| format!("parsing {} line {}", path.display(), i + 1))?;
+        out.push(ev);
+    }
+    Ok(out)
+}