diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index b6bc9a7..3725dc8 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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 [--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 ` 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"] diff --git a/src/lib.rs b/src/lib.rs index be22bfa..10b8905 100644 --- a/src/lib.rs +++ b/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}; diff --git a/src/main.rs b/src/main.rs index 2a83a58..b202a79 100644 --- a/src/main.rs +++ b/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, }, + /// 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, + /// Regex a name must match to count as a pinnable headline + /// (`unpinned-headline` rule). Defaults to the spec pattern. + #[arg(long)] + headline_pattern: Option, + /// Path to an `.arghda/config.toml`. Defaults to + /// `/.arghda/config.toml` if present. + #[arg(long)] + config: Option, + /// 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 (`/.arghda/config.toml`) is diff --git a/src/reason/mod.rs b/src/reason/mod.rs new file mode 100644 index 0000000..d1fd71f --- /dev/null +++ b/src/reason/mod.rs @@ -0,0 +1,534 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Flying-Logic reasoning graph — arghda's status-propagating layer. +//! +//! This *wraps*, it does not replace, [`crate::dag::DagDocument`]: the DAG +//! (files, lint, headlines, import edges) is embedded verbatim as +//! [`ReasonDocument::dag`], and this module adds the reasoning semantics on +//! top — a per-node [`Verdict`], `And`/`Or` juncts on edges, and a +//! propagation fold that turns the import DAG into a live picture of what is +//! *actually* established. +//! +//! ## The honesty invariant (owner directive) +//! +//! Propagation is **demote-only**: a node's effective verdict can only be +//! *lowered* by its dependencies, never manufactured. Being lint-clean does +//! NOT make a node [`Verdict::Proven`] — only a real prover exit-0 (supplied +//! via the `verdicts` map) does. An unchecked-but-clean node is +//! [`Verdict::Unknown`], honestly. `Admitted`/`Postulated` are amber, never +//! green. This is the same rule the whole tool lives by: never report a +//! result the tool did not return. +//! +//! ## What propagates even without a typecheck +//! +//! Structural facts read straight from source *do* propagate. A module the +//! linter flags with `unjustified-postulate` is capped at `Postulated` +//! (amber); a `missing-safe-pragma` module is capped at `Admitted`; a +//! `believe_me`/`trustMe` escape hatch caps at `Admitted`. And because the +//! fold is demote-only over `And`-edges, that amber **infects downstream**: +//! anything that transitively imports a postulated module is itself capped +//! at `Postulated`. That is the Flying-Logic payoff — visible before a +//! single prover is run. + +use crate::dag::DagDocument; +use crate::prover::{Backend, Verdict}; +use serde::Serialize; +use std::collections::{BTreeMap, BTreeSet}; + +/// How a node's dependencies combine. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] +#[serde(rename_all = "lowercase")] +pub enum Junct { + /// All dependencies are required (the import case): the node is demoted + /// to the *worst* of its `And`-dependencies. + And, + /// Alternative routes to one goal: the node is demoted only to the + /// *best* alternative — one green route keeps it up. + Or, +} + +/// A reasoning edge: a dependency of `from` on `to`, with its junct. +#[derive(Clone, Debug, Serialize)] +pub struct ReasonEdge { + pub from: String, + pub to: String, + pub junct: Junct, + /// The underlying relation (carried from the import graph: `imports`). + pub kind: String, +} + +/// The reasoning overlay for one node. +#[derive(Clone, Debug, Serialize)] +pub struct ReasonNode { + pub id: String, + /// The node's own verdict, before dependency propagation — the supplied + /// prover verdict (if any) demoted by this node's own lint caps. + pub self_verdict: Verdict, + /// The verdict after the demote-only fold over dependencies. + pub effective: Verdict, + /// Why `self_verdict` is what it is (supplied verdict + lint caps + any + /// staleness), human-readable. + pub verdict_evidence: String, + /// Coarse classification of `effective`: `sound` | `amber` | `unproven` + /// | `unsound`. + pub soundness: &'static str, + /// Whether this node is reachable from a CRT root (part of the verified + /// suite). `false` = an orphan; "unwired is not done". + pub wired: bool, +} + +/// The full reasoning document: the DAG plus the reasoning overlay. +#[derive(Clone, Debug, Serialize)] +pub struct ReasonDocument { + /// Reasoning-schema version (distinct from the embedded `dag.version`). + pub version: &'static str, + /// The import/lint DAG, embedded verbatim so existing consumers keep + /// working. + pub dag: DagDocument, + pub nodes: Vec, + pub edges: Vec, + /// The Current Reality Tree roots: the CI entry modules' ids. The + /// "Proven cone" is the set of `wired` nodes whose `effective` is + /// `Proven`, reachable from these. + pub crt_roots: Vec, +} + +/// Greenness rank: higher is better. The demote-fold keeps the lower rank. +/// `Proven` is the sole green; `Admitted`/`Postulated` are amber; +/// `Unknown`/`Unavailable` are not-yet-established; `Refuted`/`Error` are +/// the floor. +fn rank(v: Verdict) -> u8 { + match v { + Verdict::Proven => 6, + Verdict::Admitted => 5, + Verdict::Postulated => 4, + Verdict::Unknown => 3, + Verdict::Unavailable => 2, + Verdict::Refuted => 1, + Verdict::Error => 0, + } +} + +/// Keep the worse (lower-rank) of two verdicts — the demote operator. +fn demote(a: Verdict, b: Verdict) -> Verdict { + if rank(a) <= rank(b) { + a + } else { + b + } +} + +/// Keep the better (higher-rank) of two verdicts — used for `Or` groups. +fn promote(a: Verdict, b: Verdict) -> Verdict { + if rank(a) >= rank(b) { + a + } else { + b + } +} + +/// Coarse soundness bucket for display. +fn soundness_of(v: Verdict) -> &'static str { + match v { + Verdict::Proven => "sound", + Verdict::Admitted | Verdict::Postulated => "amber", + Verdict::Unknown | Verdict::Unavailable => "unproven", + Verdict::Refuted | Verdict::Error => "unsound", + } +} + +/// The amber/error cap a single lint rule imposes on a node's self-verdict, +/// if any. Structural facts read from source: a postulate cannot be more +/// than `Postulated`; a non-`--safe` module or an escape hatch cannot be +/// more than `Admitted`. `orphan-module` is deliberately absent — it affects +/// `wired`, not soundness (an orphan may typecheck perfectly). Rules with no +/// soundness meaning return `None`. +fn lint_cap(rule: &str) -> Option { + match rule { + "unjustified-postulate" => Some(Verdict::Postulated), + "missing-safe-pragma" => Some(Verdict::Admitted), + "escape-hatch" => Some(Verdict::Admitted), + _ => None, + } +} + +/// Derive a node's self-verdict and the evidence string: start from the +/// supplied prover verdict (or `Unknown` if none was run), then demote by +/// every lint cap this node's own diagnostics impose. +fn self_verdict_of( + id: &str, + hard_block: &[String], + warn: &[String], + verdicts: &BTreeMap, +) -> (Verdict, String) { + let mut evidence = Vec::new(); + let mut v = match verdicts.get(id) { + Some(&supplied) => { + evidence.push(format!("prover: {}", verdict_word(supplied))); + supplied + } + None => { + evidence.push("no typecheck run".to_string()); + Verdict::Unknown + } + }; + for rule in hard_block.iter().chain(warn.iter()) { + if let Some(cap) = lint_cap(rule) { + let before = v; + v = demote(v, cap); + if rank(v) < rank(before) { + evidence.push(format!("{rule} → {}", verdict_word(cap))); + } + } + } + (v, evidence.join("; ")) +} + +fn verdict_word(v: Verdict) -> &'static str { + match v { + Verdict::Proven => "proven", + Verdict::Refuted => "refuted", + Verdict::Unknown => "unknown", + Verdict::Admitted => "admitted", + Verdict::Postulated => "postulated", + Verdict::Error => "error", + Verdict::Unavailable => "unavailable", + } +} + +/// DFS colour for cycle-safe propagation. +#[derive(Clone, Copy, PartialEq)] +enum Colour { + White, + Grey, + Black, +} + +/// Build the reasoning document from an already-built [`DagDocument`]. +/// +/// `verdicts` supplies real prover results by module id (from a `check` run +/// or a workspace's `proven/` state); absent ids are `Unknown`. `stale` is +/// the set of ids whose content/closure hash changed since they were proven +/// — a stale `Proven` is demoted to `Unknown`. `backend` maps the DAG's +/// entry-module paths to ids for the CRT roots. +pub fn build( + dag: DagDocument, + backend: &dyn Backend, + verdicts: &BTreeMap, + stale: &BTreeSet, +) -> ReasonDocument { + // CRT roots: the entry modules' ids. `entry_modules` are already full + // paths (from `discover_roots`, which yields include-root-prefixed paths, + // or from `--entry` as given), so they go straight to `module_name_of` + // WITHOUT re-joining include_root — the same convention the orphan-module + // rule uses. (Re-joining double-prefixes a relative entry and breaks the + // id match, leaving every node unwired.) + let crt_roots: Vec = dag + .entry_modules + .iter() + .filter_map(|p| backend.module_name_of(p, &dag.include_root)) + .collect(); + + // Import edges are all conjunctive (you cannot typecheck a module unless + // every import does). `Or` is supported by the model + fold for authored + // graphs, but is never synthesised from imports. + let edges: Vec = dag + .edges + .iter() + .map(|e| ReasonEdge { + from: e.from.clone(), + to: e.to.clone(), + junct: Junct::And, + kind: e.kind.to_string(), + }) + .collect(); + + // Adjacency: id -> [(dep_id, junct)]. + let mut adj: BTreeMap> = BTreeMap::new(); + for e in &edges { + adj.entry(e.from.clone()) + .or_default() + .push((e.to.clone(), e.junct)); + } + + // wired = reachable from any CRT root by following edges. + let wired = reachable(&crt_roots, &adj); + + // Self-verdict per node from its lint summary + supplied verdicts, then + // staleness. A stale proof (content/closure hash changed since it was + // proven) is no longer established: drop it to `Unknown` *before* the + // fold, so the staleness propagates to everything that imports it. + let mut self_verdict: BTreeMap = BTreeMap::new(); + let mut evidence: BTreeMap = BTreeMap::new(); + for n in &dag.nodes { + let (mut v, mut ev) = self_verdict_of(&n.id, &n.lint.hard_block, &n.lint.warn, verdicts); + if stale.contains(&n.id) && v == Verdict::Proven { + v = Verdict::Unknown; + ev.push_str("; stale: closure hash changed"); + } + self_verdict.insert(n.id.clone(), v); + evidence.insert(n.id.clone(), ev); + } + + // Demote-only, cycle-safe, memoised propagation. + let mut colour: BTreeMap = BTreeMap::new(); + let mut effective: BTreeMap = BTreeMap::new(); + let mut cyclic: BTreeSet = BTreeSet::new(); + let ids: Vec = dag.nodes.iter().map(|n| n.id.clone()).collect(); + for id in &ids { + propagate( + id, + &adj, + &self_verdict, + &mut colour, + &mut effective, + &mut cyclic, + ); + } + + // Assemble nodes, applying staleness (a stale `Proven` → `Unknown`) and + // the cycle marker (a node on an import cycle is `Error`/blocked). + let mut nodes = Vec::with_capacity(dag.nodes.len()); + for n in &dag.nodes { + let mut eff = *effective.get(&n.id).unwrap_or(&Verdict::Unknown); + let mut ev = evidence.get(&n.id).cloned().unwrap_or_default(); + if cyclic.contains(&n.id) { + eff = demote(eff, Verdict::Error); + ev.push_str("; import cycle"); + } + nodes.push(ReasonNode { + id: n.id.clone(), + self_verdict: *self_verdict.get(&n.id).unwrap_or(&Verdict::Unknown), + effective: eff, + verdict_evidence: ev, + soundness: soundness_of(eff), + wired: wired.contains(&n.id), + }); + } + + ReasonDocument { + version: "0.1", + dag, + nodes, + edges, + crt_roots, + } +} + +/// The set of ids reachable from any root by following adjacency edges. +fn reachable(roots: &[String], adj: &BTreeMap>) -> BTreeSet { + let mut seen: BTreeSet = BTreeSet::new(); + let mut stack: Vec = roots.to_vec(); + while let Some(id) = stack.pop() { + if !seen.insert(id.clone()) { + continue; + } + if let Some(deps) = adj.get(&id) { + for (dep, _) in deps { + if !seen.contains(dep) { + stack.push(dep.clone()); + } + } + } + } + seen +} + +/// Post-order demote-fold with grey/black colouring for cycle safety. +/// Returns the effective verdict for `id`, memoising in `effective`. Any +/// node that closes a cycle is recorded in `cyclic` and treated as `Error`. +fn propagate( + id: &str, + adj: &BTreeMap>, + self_verdict: &BTreeMap, + colour: &mut BTreeMap, + effective: &mut BTreeMap, + cyclic: &mut BTreeSet, +) -> Verdict { + match colour.get(id).copied().unwrap_or(Colour::White) { + Colour::Black => return *effective.get(id).unwrap_or(&Verdict::Unknown), + // A back-edge to a node still on the stack: a cycle. The importing + // node is blocked; report `Error` for this leg without recursing. + Colour::Grey => { + cyclic.insert(id.to_string()); + return Verdict::Error; + } + Colour::White => {} + } + colour.insert(id.to_string(), Colour::Grey); + + let base = *self_verdict.get(id).unwrap_or(&Verdict::Unknown); + let mut eff = base; + + // Group dependency contributions by junct. + let mut or_best: Option = None; + if let Some(deps) = adj.get(id) { + for (dep, junct) in deps { + let dep_eff = propagate(dep, adj, self_verdict, colour, effective, cyclic); + match junct { + // And: every required dep drags us down to the worst of them. + Junct::And => eff = demote(eff, dep_eff), + // Or: remember the best alternative; applied after the loop. + Junct::Or => { + or_best = Some(match or_best { + Some(b) => promote(b, dep_eff), + None => dep_eff, + }); + } + } + } + } + // Or group: the goal needs at least one route, so it is capped at the + // best available alternative (still demote-only — never above `base`). + if let Some(best) = or_best { + eff = demote(eff, best); + } + + colour.insert(id.to_string(), Colour::Black); + effective.insert(id.to_string(), eff); + eff +} + +#[cfg(test)] +mod tests { + use super::*; + + // Build an adjacency map from (from, to, junct) triples for fold tests. + fn adjacency(edges: &[(&str, &str, Junct)]) -> BTreeMap> { + let mut adj: BTreeMap> = BTreeMap::new(); + for (f, t, j) in edges { + adj.entry(f.to_string()) + .or_default() + .push((t.to_string(), *j)); + } + adj + } + + fn fold( + selfv: &[(&str, Verdict)], + edges: &[(&str, &str, Junct)], + ) -> (BTreeMap, BTreeSet) { + let adj = adjacency(edges); + let sv: BTreeMap = + selfv.iter().map(|(k, v)| (k.to_string(), *v)).collect(); + let mut colour = BTreeMap::new(); + let mut effective = BTreeMap::new(); + let mut cyclic = BTreeSet::new(); + for (id, _) in selfv { + propagate(id, &adj, &sv, &mut colour, &mut effective, &mut cyclic); + } + (effective, cyclic) + } + + #[test] + fn demote_keeps_the_worse() { + assert_eq!( + demote(Verdict::Proven, Verdict::Postulated), + Verdict::Postulated + ); + assert_eq!(demote(Verdict::Unknown, Verdict::Proven), Verdict::Unknown); + assert_eq!(demote(Verdict::Error, Verdict::Refuted), Verdict::Error); + } + + #[test] + fn clean_but_unchecked_is_unknown_not_proven() { + // The core honesty rule: lint-clean + no prover run ⇒ Unknown. + let verdicts = BTreeMap::new(); + let (v, ev) = self_verdict_of("M", &[], &[], &verdicts); + assert_eq!(v, Verdict::Unknown); + assert!(ev.contains("no typecheck run")); + } + + #[test] + fn supplied_proven_is_capped_by_postulate_lint() { + let mut verdicts = BTreeMap::new(); + verdicts.insert("M".to_string(), Verdict::Proven); + let (v, ev) = self_verdict_of("M", &["unjustified-postulate".to_string()], &[], &verdicts); + assert_eq!(v, Verdict::Postulated); + assert!(ev.contains("postulated")); + } + + #[test] + fn orphan_lint_does_not_cap_soundness() { + // orphan-module is a wiring fact, not a soundness one. + let mut verdicts = BTreeMap::new(); + verdicts.insert("M".to_string(), Verdict::Proven); + let (v, _) = self_verdict_of("M", &["orphan-module".to_string()], &[], &verdicts); + assert_eq!(v, Verdict::Proven); + } + + #[test] + fn and_dependency_demotes_downstream() { + // Top imports Mid imports Leaf; Leaf is Postulated (amber). The + // amber infects the whole And-chain: everyone caps at Postulated. + let (eff, _) = fold( + &[ + ("Top", Verdict::Proven), + ("Mid", Verdict::Proven), + ("Leaf", Verdict::Postulated), + ], + &[("Top", "Mid", Junct::And), ("Mid", "Leaf", Junct::And)], + ); + assert_eq!(eff["Leaf"], Verdict::Postulated); + assert_eq!(eff["Mid"], Verdict::Postulated); + assert_eq!(eff["Top"], Verdict::Postulated); + } + + #[test] + fn or_alternative_keeps_a_goal_up() { + // Goal has two Or routes: one Error, one Proven. The best route + // wins, so the goal stays Proven (Or is forgiving). + let (eff, _) = fold( + &[ + ("Goal", Verdict::Proven), + ("RouteA", Verdict::Error), + ("RouteB", Verdict::Proven), + ], + &[("Goal", "RouteA", Junct::Or), ("Goal", "RouteB", Junct::Or)], + ); + assert_eq!(eff["Goal"], Verdict::Proven); + } + + #[test] + fn or_group_caps_at_best_when_no_route_is_green() { + // Both Or routes are amber ⇒ the goal is capped at the best amber. + let (eff, _) = fold( + &[ + ("Goal", Verdict::Proven), + ("RouteA", Verdict::Postulated), + ("RouteB", Verdict::Admitted), + ], + &[("Goal", "RouteA", Junct::Or), ("Goal", "RouteB", Junct::Or)], + ); + // Admitted (rank 5) beats Postulated (rank 4); demote(Proven, Admitted). + assert_eq!(eff["Goal"], Verdict::Admitted); + } + + #[test] + fn cycle_degrades_to_error_and_terminates() { + // A <-> B mutual import (illegal in Agda, but possible transiently). + // The fold must terminate and mark the cycle, not loop forever. + let (eff, cyclic) = fold( + &[("A", Verdict::Proven), ("B", Verdict::Proven)], + &[("A", "B", Junct::And), ("B", "A", Junct::And)], + ); + assert!(!cyclic.is_empty(), "the cycle must be recorded"); + assert_eq!(eff["A"], Verdict::Error); + assert_eq!(eff["B"], Verdict::Error); + } + + #[test] + fn reachable_marks_only_the_root_cone() { + let adj = adjacency(&[ + ("All", "Used", Junct::And), + ("Used", "Deep", Junct::And), + // Orphan is imported by nobody reachable from All. + ]); + let wired = reachable(&["All".to_string()], &adj); + assert!(wired.contains("All")); + assert!(wired.contains("Used")); + assert!(wired.contains("Deep")); + assert!(!wired.contains("Orphan")); + } +} diff --git a/tests/reason.rs b/tests/reason.rs new file mode 100644 index 0000000..8bc1654 --- /dev/null +++ b/tests/reason.rs @@ -0,0 +1,170 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! `reason` document construction over the fixtures — the Flying-Logic +//! reasoning graph built on top of the DAG. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, default_rules, Agda, Verdict}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn fixture(name: &str) -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push(name); + p +} + +fn dag_of(name: &str) -> arghda_core::DagDocument { + let root = fixture(name); + let roots = [root.join("All.agda")]; + build_dag( + &root, + &roots, + &default_rules(), + DEFAULT_HEADLINE_PATTERN, + &Agda, + ) + .unwrap() +} + +fn effective(doc: &arghda_core::ReasonDocument, id: &str) -> Verdict { + doc.nodes.iter().find(|n| n.id == id).unwrap().effective +} + +fn wired(doc: &arghda_core::ReasonDocument, id: &str) -> bool { + doc.nodes.iter().find(|n| n.id == id).unwrap().wired +} + +#[test] +fn no_verdicts_means_clean_nodes_are_unknown_not_proven() { + // The honesty rule end-to-end: without a typecheck, a lint-clean tree is + // all `unknown` — never fabricated green. + let doc = build_reason( + dag_of("wellformed"), + &Agda, + &BTreeMap::new(), + &BTreeSet::new(), + ); + for n in &doc.nodes { + assert_eq!( + n.effective, + Verdict::Unknown, + "node {} should be unknown without a typecheck", + n.id + ); + assert_eq!(n.soundness, "unproven"); + } + assert_eq!(doc.crt_roots, vec!["All".to_string()]); + assert_eq!(doc.version, "0.1"); + // The DAG is embedded verbatim. + assert_eq!(doc.dag.version, "0.1"); +} + +#[test] +fn supplied_proven_lights_up_the_whole_cone() { + let mut verdicts = BTreeMap::new(); + for id in ["All", "Good", "Util"] { + verdicts.insert(id.to_string(), Verdict::Proven); + } + let doc = build_reason(dag_of("wellformed"), &Agda, &verdicts, &BTreeSet::new()); + for id in ["All", "Good", "Util"] { + assert_eq!( + effective(&doc, id), + Verdict::Proven, + "{id} should be proven" + ); + assert!(wired(&doc, id), "{id} should be wired"); + } +} + +#[test] +fn a_postulated_import_infects_its_downstream() { + // The Flying-Logic payoff: Util is only Postulated (amber); All imports + // Util (an And edge), so All's *effective* verdict is dragged down to + // Postulated even though All itself typechecked. Good does not import + // Util, so it stays Proven. + let mut verdicts = BTreeMap::new(); + verdicts.insert("All".to_string(), Verdict::Proven); + verdicts.insert("Good".to_string(), Verdict::Proven); + verdicts.insert("Util".to_string(), Verdict::Postulated); + let doc = build_reason(dag_of("wellformed"), &Agda, &verdicts, &BTreeSet::new()); + + assert_eq!(effective(&doc, "Util"), Verdict::Postulated); + assert_eq!( + effective(&doc, "All"), + Verdict::Postulated, + "amber must propagate up the And import edge" + ); + assert_eq!(effective(&doc, "Good"), Verdict::Proven); + + // Soundness buckets reflect it. + let all = doc.nodes.iter().find(|n| n.id == "All").unwrap(); + assert_eq!(all.soundness, "amber"); +} + +#[test] +fn an_orphan_is_unwired() { + // Orphan is reachable from no CI root: wired = false. All and Used are. + let doc = build_reason(dag_of("orphan"), &Agda, &BTreeMap::new(), &BTreeSet::new()); + assert!(wired(&doc, "All")); + assert!(wired(&doc, "Used")); + assert!(!wired(&doc, "Orphan"), "Orphan must be unwired"); + assert_eq!(doc.crt_roots, vec!["All".to_string()]); +} + +#[test] +fn staleness_demotes_a_proven_node_to_unknown() { + let mut verdicts = BTreeMap::new(); + for id in ["All", "Good", "Util"] { + verdicts.insert(id.to_string(), Verdict::Proven); + } + let mut stale = BTreeSet::new(); + stale.insert("Good".to_string()); + let doc = build_reason(dag_of("wellformed"), &Agda, &verdicts, &stale); + assert_eq!( + effective(&doc, "Good"), + Verdict::Unknown, + "a stale proven node must fall back to unknown" + ); + // Util (not stale) stays proven; All imports Good so All is dragged to + // unknown by the stale prerequisite. + assert_eq!(effective(&doc, "Util"), Verdict::Proven); + assert_eq!(effective(&doc, "All"), Verdict::Unknown); +} + +#[test] +fn crt_roots_and_wiring_survive_discover_roots_relative_paths() { + // Regression: the CLI derives roots via `graph::discover_roots`, which + // yields include-root-PREFIXED relative paths (e.g. + // `/All.agda`), not absolute ones. crt_roots must still resolve + // to the bare module id `All` and the cone must be wired — a bug here + // left every node unwired. (dag_of passes absolute roots, where the + // earlier `include_root.join` was a silent no-op, so it missed this.) + let root = fixture("wellformed"); + let roots = arghda_core::graph::discover_roots(&root); + let dag = build_dag( + &root, + &roots, + &default_rules(), + DEFAULT_HEADLINE_PATTERN, + &Agda, + ) + .unwrap(); + let doc = build_reason(dag, &Agda, &BTreeMap::new(), &BTreeSet::new()); + + assert_eq!( + doc.crt_roots, + vec!["All".to_string()], + "crt_roots must be the bare module id, got {:?}", + doc.crt_roots + ); + for id in ["All", "Good", "Util"] { + assert!( + wired(&doc, id), + "{id} must be wired via discover_roots path" + ); + } +}