ArghDA M3: Flying-Logic reasoning graph — demote-only verdict propagation

The headline capability of the epic. A new `src/reason/` layer that *wraps*
(does not replace) the DAG: the `DagDocument` is embedded verbatim, and on
top go a per-node `Verdict`, `And`/`Or` edge juncts, and a memoised,
cycle-safe, DEMOTE-ONLY propagation fold.

The honesty invariant, enforced end-to-end: a node's effective verdict can
only be LOWERED by its dependencies, never manufactured. Lint-clean + no
typecheck = `Unknown`, never green. Only `Proven` is green;
`Admitted`/`Postulated` are amber. And because the fold is demote-only over
`And` import edges, structural amber INFECTS downstream — anything that
transitively imports a `postulate` (or `missing-safe`/escape-hatch) module
is itself capped, visible before any prover runs. `Or` groups are forgiving
(one green route keeps a goal up). Import cycles degrade to `Error` and
terminate. Staleness (closure-hash-changed proven → `Unknown`) is applied
pre-fold so it propagates. `wired` marks the CRT-root-reachable cone.

- `src/reason/mod.rs`: `Junct`, `ReasonNode` (self_verdict/effective/
  verdict_evidence/soundness/wired), `ReasonEdge`, `ReasonDocument`
  (version "0.1", embedded `dag`, `crt_roots`); rank/demote/promote lattice;
  lint→verdict caps; the propagation fold.
- `arghda reason <path> [--check]`: `--check` runs the backend per node for
  REAL exit-code verdicts (honest); default is structure+lint derived.
- Tests: 9 unit (demote, downstream amber infection, Or forgiveness, cycle
  termination, wiring, clean-but-unchecked→Unknown) + 6 integration. Total
  suite 81 green; clippy -D warnings, fmt, SPDX clean.
- Dogfood caught + fixed a real wiring bug: the CLI's `discover_roots`
  yields include-root-relative paths, which a stray `include_root.join`
  double-prefixed, leaving every node unwired. Fixed (match the
  orphan-module rule's convention) + regression-tested; the earlier tests
  missed it because they passed absolute paths.
- STATE.a2ml records M3 = 100%.

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

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -43,7 +43,7 @@ milestones = [
   { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes", completion = 80 },
   { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 },
   { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 },
-  { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 0 },
+  { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 },
   { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 },
   { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 0 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 },
@@ -60,6 +60,23 @@ milestones = [
 # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells
 # the script's --verify-only table).
 #
+# M3 landed 2026-07-01: the Flying-Logic reasoning graph (src/reason/) — the
+# headline capability. Wraps DagDocument verbatim (ReasonDocument.dag) + adds a
+# per-node Verdict, And|Or edge juncts, and a memoised, cycle-safe, DEMOTE-ONLY
+# propagation fold: a node's effective verdict can only be LOWERED by deps,
+# never manufactured. Only Proven is green; Admitted/Postulated amber. Honesty
+# rule enforced end-to-end: lint-clean + no typecheck = Unknown (never green).
+# Structural amber (unjustified-postulate → Postulated cap; missing-safe-pragma
+# / escape-hatch → Admitted) INFECTS downstream via And import edges — visible
+# before any prover runs. `arghda reason <path> [--check]` CLI: --check runs the
+# backend per node for REAL exit-code verdicts. Staleness (closure-hash-changed
+# proven → Unknown, pre-fold so it propagates) + wiring (reachable-from-CRT-root)
+# + crt_roots. 81 tests (61 lib + 20 integration; +9 reason unit +6 reason
+# integration), clippy/fmt/SPDX clean. Dogfood: `reason --check` over the
+# wellformed fixture ran real agda → all Proven/wired. A wiring bug (relative
+# discover_roots paths double-joined) was caught BY dogfooding and fixed +
+# regression-tested — the unit tests missed it (they used absolute paths).
+#
 # M1 landed 2026-07-01 as the promised PURE REFACTOR — behaviour unchanged,
 # oracle held: the 64 pre-existing tests (50 lib + 14 integration) all stay
 # green, +2 new Agda-backend tests = 66 passing; clippy -D warnings + fmt +
@@ -87,11 +104,11 @@ milestones = [
 
 [critical-next-actions]
 actions = [
-  "M1 keystone DONE (Backend trait, pure refactor, 66 tests green). Next, in parallel now that the trait is stable:",
-  "Flying-Logic epic M3: src/reason reasoning graph (And|Or juncts + demote-only cycle-safe Verdict propagation over the common Verdict) — independent of new backends, lands the headline capability early.",
+  "M1 (Backend trait) + M3 (reasoning graph) DONE. Next, all unblocked by the stable trait — pick per priority:",
   "Flying-Logic epic M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; believe_me/assert_total/%partial escape-hatches) — Idris2 v0.7.0 is provisioned.",
   "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the Solver kind; SMT-LIB2 -> sat(Refuted)/unsat(Proven)/unknown(Unknown). Both binaries are provisioned.",
   "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden).",
+  "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs) so `arghda reason <workspace>` lights the cone without --check.",
   "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).",
   "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.",
 ]
@@ -102,9 +119,10 @@ 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-M1: 52 lib + 14 integration = 66 tests pass. `dag`/`check` dogfooded
-# via real CLI runs (dag JSON byte-compatible; check ran a real agda typecheck
-# -> proven-eligible). Dogfooded historically against echo-types + agda-unused.
+# post-M3: 61 lib + 20 integration = 81 tests pass. Dogfooded via real CLI
+# runs: `dag` JSON byte-compatible; `check` + `reason --check` ran real agda
+# typechecks (proven-eligible / all-Proven+wired cone). Dogfooded historically
+# against echo-types + agda-unused.
 
 [ecosystem]
 part-of = ["arghda"]

src/lib.rs

@@ -19,6 +19,7 @@ pub mod hash;
 pub mod lint;
 pub mod proven;
 pub mod prover;
+pub mod reason;
 pub mod timestamp;
 pub mod unused;
 pub mod watcher;
@@ -30,4 +31,5 @@ pub use event::{Event, EventKind};
 pub use graph::{build as build_graph, ImportGraph};
 pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig};
 pub use prover::{default_backend, Agda, Backend, BackendKind, Outcome, Verdict};
+pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode};
 pub use workspace::{StaleEntry, State, Workspace};

src/main.rs

@@ -4,8 +4,8 @@
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
-    build_dag, event, run_lints, unused, watcher, Agda, Backend, LintRule, RuleConfig, State,
-    Workspace,
+    build_dag, build_reason, event, run_lints, unused, watcher, Agda, Backend, LintRule,
+    RuleConfig, State, Workspace,
 };
 use clap::{Parser, Subcommand};
 use std::path::{Path, PathBuf};
@@ -83,6 +83,31 @@ enum Cmd {
         #[arg(long)]
         config: Option<PathBuf>,
     },
+    /// Emit the Flying-Logic reasoning graph (JSON) for the tree at PATH:
+    /// the DAG plus a demote-only verdict propagation. Without `--check`,
+    /// clean nodes are honestly `unknown`; postulate/pragma/escape-hatch
+    /// caps still propagate downstream through import edges.
+    Reason {
+        /// Directory containing `.agda` files; treated as the include root.
+        path: PathBuf,
+        /// Root module for orphan detection; repeatable. Defaults to every
+        /// `All.agda`/`Smoke.agda` discovered under PATH.
+        #[arg(long)]
+        entry: Vec<PathBuf>,
+        /// Regex a name must match to count as a pinnable headline
+        /// (`unpinned-headline` rule). Defaults to the spec pattern.
+        #[arg(long)]
+        headline_pattern: Option<String>,
+        /// Path to an `.arghda/config.toml`. Defaults to
+        /// `<PATH>/.arghda/config.toml` if present.
+        #[arg(long)]
+        config: Option<PathBuf>,
+        /// Run the backend on every node to populate REAL prover verdicts
+        /// (honest exit codes). Slower — typechecks each module. Off by
+        /// default, in which case clean nodes are `unknown`.
+        #[arg(long)]
+        check: bool,
+    },
     /// Claim a file: inbox -> working.
     Claim { workspace: PathBuf, file: String },
     /// Promote a file: working -> proven.
@@ -144,6 +169,19 @@ fn main() -> Result<()> {
             headline_pattern.as_deref(),
             config.as_deref(),
         )?,
+        Cmd::Reason {
+            path,
+            entry,
+            headline_pattern,
+            config,
+            check,
+        } => reason(
+            &path,
+            &entry,
+            headline_pattern.as_deref(),
+            config.as_deref(),
+            check,
+        )?,
         Cmd::Claim { workspace, file } => {
             transition(&workspace, &file, State::Inbox, State::Working)?
         }
@@ -354,6 +392,45 @@ fn dag(
     Ok(())
 }
 
+fn reason(
+    include_root: &Path,
+    entry: &[PathBuf],
+    headline_pattern: Option<&str>,
+    config: Option<&Path>,
+    do_check: bool,
+) -> Result<()> {
+    let backend = Agda;
+    let (roots, rules, cfg) =
+        resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?;
+    let dag_doc = build_dag(
+        include_root,
+        &roots,
+        &rules,
+        &cfg.headline_pattern,
+        &backend,
+    )?;
+
+    // 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.
+    let mut verdicts = std::collections::BTreeMap::new();
+    let stale = std::collections::BTreeSet::new();
+    if do_check {
+        for node in &dag_doc.nodes {
+            let file = include_root.join(&node.file);
+            let outcome = backend.check_file(&file, include_root)?;
+            if outcome.available {
+                verdicts.insert(node.id.clone(), outcome.verdict);
+            }
+        }
+    }
+
+    let doc = build_reason(dag_doc, &backend, &verdicts, &stale);
+    println!("{}", serde_json::to_string_pretty(&doc)?);
+    Ok(())
+}
+
 /// Build the lint `RuleConfig` with precedence default < `.arghda/config.toml`
 /// < CLI flag. An explicit `--config` that does not exist is an error; the
 /// default discovery location (`<include_root>/.arghda/config.toml`) is