diff --git a/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md new file mode 100644 index 000000000..e8f92ee76 --- /dev/null +++ b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md @@ -0,0 +1,42 @@ +# D-EPI-COT-C3 (first slice): tactics run only on grounded, Epi5-eligible markers + +**Status:** TEST-PINNED. Code: +- `crates/lance-graph-planner/src/nars/warrant.rs` +- `epistemic_state5::RecipeRule` +- `certification::CertificationModel::measured_only` + +Plan: `docs/research/epistemic-cot/c3-plan.md` §8. + +## Decision + +- **SCOPE:** a planner tactic (RCR 4, TR 6, CAS 8) runs only on `Marker`s. A marker is three things together: + - the ledger's pooled truth and roots; + - bits 59..63 projected through `Epi5Declarations`; + - a thought slot and generation. + + Each premise must satisfy the recipe's `RecipeRule`. The rule's requires/forbids are policy pins: Associated for 4/6/7/8, and no intermediate-known for RCR. +- **Judgments** carry the tactic's truth, the proof's roots, the thought, and `Unknown × Open`. A term-logic step earns no certification. The only promotion is `pearl::reason` + `revise` over executed trial arms (pinned in the same test). +- **`measured_only`:** an unmeasured outcome is excluded, not read as negative. That includes trial arms, which `causes` reads without the universe. + +## Evidence + +- 9 new tests. 9 disables, each red. +- One disable (trial arms unrestricted) was green on the first fixture: every control unit was measured. An unmeasured-control fixture was added before recording. +- Planner lib 485 pass; contract lib 1561 pass. +- Clippy `--lib --tests` reports the same 8 sites as main `694b243bd`. + +## Open + +- Effect size, sample size, uncertainty and multiple comparisons are still unreported by `CertificationModel`. +- Missing-at-random is assumed. +- ASC and CR are not run through `fire`. +- The lab affordance law still has its own rule type. +- C3b and C3c wait on the bits 50..52 order decision and the TFLite location. + +## Addendum, same day: ledger → `pearl::hydrate` + +- `nars::mediator::hydrate_from_ledger` connects the ledger's grounded deductions of `A → Y` through `B` to the unchanged `pearl::hydrate`. It returns derivations, roots, the `Hydration` result, the edge and the mediated-path sensitivity. +- The ledger never creates a chain, and a path the chain does not witness leaves the edge unchanged. A chain-only path has no ledger receipt and is refused. +- `Law::Deduction` admits `Impl` in an explicit step: never closure, and `Rel` never composes. +- 5 tests; 5 disables red. The first grounding disable did not bind (no proofs exist without evidence); it was replaced before recording. +- Maturation order for new declared readings is `7 = Staunen … 0 = Wisdom`. The TFLite kernels are in ndarray. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 6f379afec..a6f8e64ef 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,13 +25,14 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -497 entries, 2026-08-06 .. 2026-10-28. +498 entries, 2026-08-06 .. 2026-10-28. | date | entry id | finding | file | |---|---|---|---| | 2026-10-28 | `thought-layers-nan-skip` | | [2026-10-28-thought-layers-nan-skip.md](2026-10-28-thought-layers-nan-skip.md) | | 2026-10-28 | `lane-layout-from-classview` | | [2026-10-28-lane-layout-from-classview.md](2026-10-28-lane-layout-from-classview.md) | | 2026-10-28 | `D-SAG-6-1` | | [2026-10-28-d-sag-6-1-audit-reference-ledger.md](2026-10-28-d-sag-6-1-audit-reference-ledger.md) | +| 2026-10-28 | `D-EPI-COT-C3` | | [2026-10-28-d-epi-cot-c3-warrant.md](2026-10-28-d-epi-cot-c3-warrant.md) | | 2026-10-28 | `D-EPI-COT` | | [2026-10-28-d-epi-cot-c0-c2.md](2026-10-28-d-epi-cot-c0-c2.md) | | 2026-10-28 | `D-DT64-6` | | [2026-10-28-d-dt64-6-routing-bindstore-behavior.md](2026-10-28-d-dt64-6-routing-bindstore-behavior.md) | | 2026-10-28 | `D-DT64-6-1a` | | [2026-10-28-d-dt64-6-ogit-predicates-impl.md](2026-10-28-d-dt64-6-ogit-predicates-impl.md) | diff --git a/crates/lance-graph-contract/src/certification.rs b/crates/lance-graph-contract/src/certification.rs index 0d5014cac..5c2672011 100644 --- a/crates/lance-graph-contract/src/certification.rs +++ b/crates/lance-graph-contract/src/certification.rs @@ -289,6 +289,35 @@ impl CertificationModel { ) } + /// The model restricted to the units whose outcome was measured. + /// + /// `outcome` is a positive mask: a unit outside it reads as a known + /// negative. A unit whose outcome is UNKNOWN must not read that way, so + /// before certifying, every mask (population, strata, ordering, + /// robustness, and the trial arms, which `causes` reads without the + /// universe) is intersected with `measured`. An arm left with no measured + /// unit refuses as [`NotGrounded::EmptyArm`] rather than deciding. + #[must_use] + pub fn measured_only(&self, measured: &M) -> Self { + let keep = |m: &M| m.intersection(measured); + CertificationModel { + universe: keep(&self.universe), + exposed: keep(&self.exposed), + outcome: keep(&self.outcome), + strata: [ + keep(&self.strata[0]), + keep(&self.strata[1]), + keep(&self.strata[2]), + keep(&self.strata[3]), + ], + ordered: keep(&self.ordered), + clean: keep(&self.clean), + trial: keep(&self.trial), + assigned: keep(&self.assigned), + ..self.clone() + } + } + /// The randomized arms read as a population of their own. pub fn trial_view(&self) -> CertificationModel { CertificationModel { @@ -458,6 +487,58 @@ impl ModelBuilder { mod tests { use super::*; + /// Unmeasured outcomes are not negatives. Treated arm: 4 units with the + /// outcome, 4 whose outcome was never measured. Control arm: 3 of 8. + /// Reading the unmeasured units as negatives gives 4/8 against 3/8, so + /// `causes` holds; restricted to measured units it is 4/4 against 3/8. + /// The second fixture moves the gap the other way: 2 of 8 treated + /// measured positive, 6 unmeasured; as negatives 2/8 < 3/8 refutes, as + /// unknown 2/2 > 3/8 holds. + #[test] + fn unmeasured_outcomes_are_not_read_as_negatives() { + let build = |treated_hits: u32, treated_unknown: u32| { + let mut b = ModelBuilder::new(); + b.sources(SupportBasis::InterventionBacked, &[1, 2]); + let (t_known, _) = b.arm(true, treated_hits, treated_hits); + let (t_unknown, _) = b.arm(true, treated_unknown, 0); + let (c, _) = b.arm(false, 8, 3); + let measured = t_known.union(&c); + assert!(!t_unknown.is_empty() && !t_unknown.intersects(&measured)); + (b.build(), measured) + }; + + let (m, measured) = build(2, 6); + assert_eq!(m.causes(), Ok(false), "unknowns read as negatives refute"); + assert_eq!(m.measured_only(&measured).causes(), Ok(true)); + + let (m, measured) = build(4, 4); + assert_eq!(m.causes(), Ok(true)); + assert_eq!(m.measured_only(&measured).causes(), Ok(true)); + + // Unknowns in the control arm: treated 1 of 4 measured, control 3 of + // 8 measured plus 8 unmeasured. Read as negatives the control rate + // is 3/16 and treated (1/4) looks higher; restricted it is 3/8 and + // treated is lower. + let mut b = ModelBuilder::new(); + b.sources(SupportBasis::InterventionBacked, &[1, 2]); + let (t, _) = b.arm(true, 4, 1); + let (c_known, _) = b.arm(false, 8, 3); + let (c_unknown, _) = b.arm(false, 8, 0); + let m = b.build(); + let measured = t.union(&c_known); + assert!(!c_unknown.intersects(&measured)); + assert_eq!(m.causes(), Ok(true), "unknown controls read as negatives"); + assert_eq!(m.measured_only(&measured).causes(), Ok(false)); + + // An arm with no measured unit refuses instead of deciding. + let (m, _) = build(2, 6); + let control_only = m.trial.difference(&m.assigned); + assert_eq!( + m.measured_only(&control_only).causes(), + Err(NotGrounded::EmptyArm) + ); + } + /// Every fold of a model, so two models can be compared fold by fold. fn folds(m: &CertificationModel) -> [Sat; 6] { [ diff --git a/crates/lance-graph-contract/src/epistemic_state5.rs b/crates/lance-graph-contract/src/epistemic_state5.rs index 06e7ab0ee..3d4f3d842 100644 --- a/crates/lance-graph-contract/src/epistemic_state5.rs +++ b/crates/lance-graph-contract/src/epistemic_state5.rs @@ -306,6 +306,59 @@ pub const fn facts_population(required: Facts) -> Population { population } +/// A recipe's epistemic obligations: the facts a state must assert +/// (`requires`) and must not assert (`forbids`) for the recipe to be eligible +/// on an edge in that state. +/// +/// This is the affordance law's rule, moved from the D-GSO-AFF-0 lab +/// (`cognitive-shader-driver/examples/shared/affordance_law.rs`) so a +/// production consumer can read it. Eligibility is a read-only derivation from +/// declared facts: it does not authorize execution, does not say a +/// conclusion is true, and never writes an edge. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)] +pub struct RecipeRule { + /// Facts every eligible state asserts. + pub requires: Facts, + /// Facts no eligible state asserts. + pub forbids: Facts, +} + +impl RecipeRule { + /// A rule with these obligations. + #[must_use] + pub const fn new(requires: Facts, forbids: Facts) -> Self { + Self { requires, forbids } + } + + /// Whether a state asserting `facts` satisfies the rule. + #[must_use] + pub const fn holds(self, facts: Facts) -> bool { + facts & self.requires == self.requires && facts & self.forbids == 0 + } + + /// Whether `state` satisfies the rule. + #[must_use] + pub const fn admits(self, state: EpistemicState5) -> bool { + self.holds(state.facts()) + } + + /// The V1 codes on which the rule holds. Reserved codes never appear. + #[must_use] + pub const fn population(self) -> Population { + let mut population = 0; + let mut raw = 0; + while raw < CODES { + if let Some(facts) = COMPILED_FACTS_V1[raw] { + if self.holds(facts) { + population |= 1 << raw; + } + } + raw += 1; + } + population + } +} + /// A reading generation. V1 is the 2 × 3 product above. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)] pub enum Epi5Gen { @@ -540,6 +593,39 @@ mod tests { EpistemicState5::new(Epi5Gen::V1, t, c).raw() } + /// A rule's population is exactly the meaningful codes it admits, and + /// `forbids` removes codes `requires` alone would keep. + #[test] + fn a_recipe_rule_population_matches_its_per_state_check() { + let rule = RecipeRule::new(ASSOCIATED, INTERMEDIATE_KNOWN); + let mut expected = 0; + for raw in 0u8..32 { + if let Ok(s) = EpistemicState5::decode(Epi5Gen::V1, raw) { + if rule.admits(s) { + expected |= 1 << raw; + } + } + } + assert_eq!(rule.population(), expected); + assert_eq!( + RecipeRule::new(ASSOCIATED, 0).population() & !rule.population(), + facts_population(ASSOCIATED | INTERMEDIATE_KNOWN), + "forbids removes exactly the states that assert the forbidden fact" + ); + assert!(!rule.admits(EpistemicState5::new( + Epi5Gen::V1, + T::IndirectKnown, + C::Causes + ))); + assert!(rule.admits(EpistemicState5::new( + Epi5Gen::V1, + T::IndirectUnknown, + C::Causes + ))); + assert!(!rule.admits(EpistemicState5::new(Epi5Gen::V1, T::Direct, C::Open))); + assert_eq!(rule.population() >> 24, 0, "reserved codes never admitted"); + } + /// The layout is the product: `raw5 = t | c << 2`, 24 meaningful, 8 /// reserved, and decode inverts it on every code. #[test] diff --git a/crates/lance-graph-planner/src/nars/mediator.rs b/crates/lance-graph-planner/src/nars/mediator.rs new file mode 100644 index 000000000..f22682c22 --- /dev/null +++ b/crates/lance-graph-planner/src/nars/mediator.rs @@ -0,0 +1,353 @@ +//! `mediator`: the seam from the derivation ledger to `pearl::hydrate` +//! (D-EPI-COT C3a). +//! +//! The ledger (#1840) can hold a grounded deduction `A → Y` through a +//! mediator `B`. That is a reasoning result, not a source-attested chain. +//! [`hydrate_from_ledger`] hands the step to the existing topology gate, +//! [`crate::pearl::hydrate`], and leaves the decision there: +//! +//! - the ledger supplies the receipt: which derivations go through `B`, their +//! source roots, and what removing them does to `A → Y`; +//! - the sealed chain decides the topology. `IndirectUnknown` becomes +//! `IndirectKnown` only when both `A → B` and `B → Y` are bindings in the +//! sealed chain. A ledger path whose links are not in the chain changes +//! nothing; +//! - certification never moves here. +//! +//! The adapter refuses when the ledger has no grounded path through `B`, so a +//! hydration it reports always has a ledger receipt behind it. It reads only +//! the subject and object of each chain step, as `pearl::hydrate` does; the +//! step's `u8` tag is not a predicate (the withdrawn #1572 guard). + +use std::collections::BTreeSet; + +use causal_edge::edge::CausalEdge64; +use lance_graph_contract::epistemic_state5::Epi5ReadError; + +use super::belief::CStmt; +use super::support::{ + Ablation, DerivationId, DerivationLedger, Law, Refusal, Sensitivity, SourceId, +}; +use crate::chain_replay::ChainStep; +use crate::pearl::{hydrate, Hydration, Reading}; + +/// What the ledger and the sealed chain said about `A → Y` through `B`. +#[derive(Debug, Clone, PartialEq)] +pub struct MediatorReceipt { + /// Grounded deductions of `A → Y` through `B`. + pub derivations: Vec, + /// Source roots of the proofs through them. + pub roots: BTreeSet, + /// What `pearl::hydrate` found in the sealed chain. + pub hydration: Hydration, + /// The edge after `pearl::hydrate`. + pub edge: CausalEdge64, + /// `A → Y` with and without the derivations through `B`. + pub mediated: Sensitivity, +} + +/// Why no receipt was produced. +#[derive(Debug, Clone, PartialEq)] +pub enum MediatorRefusal { + /// A term does not fit the edge's 8-bit index. + TermRange(u16), + /// The edge is not the relation `A → Y`. + EdgeMismatch, + /// The ledger has no grounded deduction of `A → Y` through `B`. + NoLedgerPath, + /// The ledger refused to evaluate. + Ledger(Refusal), + /// The edge's bits 59..63 do not project. + Epi5(Epi5ReadError), +} + +fn idx(term: u16) -> Result { + u8::try_from(term).map_err(|_| MediatorRefusal::TermRange(term)) +} + +/// Hand a ledger path `A → B → Y` to `pearl::hydrate` for the edge `A → Y`. +/// +/// # Errors +/// A [`MediatorRefusal`]. +pub fn hydrate_from_ledger( + ledger: &DerivationLedger, + edge: CausalEdge64, + target: CStmt, + mediator: u16, + sealed: &[ChainStep], + reading: Reading<'_>, +) -> Result { + let (a, b, y) = (idx(target.s)?, idx(mediator)?, idx(target.p)?); + if edge.s_idx() != a || edge.o_idx() != y { + return Err(MediatorRefusal::EdgeMismatch); + } + + let first = CStmt { + s: target.s, + cop: target.cop, + p: mediator, + }; + let second = CStmt { + s: mediator, + cop: target.cop, + p: target.p, + }; + let through: Vec = ledger + .derivations() + .iter() + .enumerate() + .filter(|(_, d)| { + d.law == Law::Deduction + && d.conclusion == target + && (d.premises == [first, second] || d.premises == [second, first]) + }) + .map(|(i, _)| DerivationId(i as u32)) + .collect(); + + let proofs = ledger + .proofs(target, &Ablation::none()) + .map_err(MediatorRefusal::Ledger)?; + let mut derivations = Vec::new(); + let mut roots = BTreeSet::new(); + for id in through { + if let Some(p) = proofs.iter().find(|p| p.uses.contains(&id)) { + derivations.push(id); + roots.extend(p.roots.iter().copied()); + } + } + if derivations.is_empty() { + return Err(MediatorRefusal::NoLedgerPath); + } + + let (edge, hydration) = + hydrate(edge, (a, b, y), sealed, reading).map_err(MediatorRefusal::Epi5)?; + let mediated = ledger + .sensitivity(target, &Ablation::derivations(&derivations)) + .map_err(MediatorRefusal::Ledger)?; + Ok(MediatorReceipt { + derivations, + roots, + hydration, + edge, + mediated, + }) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::nars::belief::Copula; + use crate::nars::support::ChainId; + use crate::nars::truth::TruthValue; + use causal_edge::edge::InferenceType; + use causal_edge::{CausalMask, PlasticityState}; + use lance_graph_contract::band_reading::EdgeProvenance; + use lance_graph_contract::class_view::ClassId; + use lance_graph_contract::epistemic_state5::{ + Certification3, Epi5Declarations, Epi5Gen, Epi5Reading, EpistemicState5, Topology2, + }; + use lance_graph_contract::rail_geometry::RailAxis; + + const CLASS: ClassId = 0x0902; + const RAIL: RailAxis = RailAxis::Taxonomy; + const A: u16 = 10; + const B: u16 = 20; + const C: u16 = 25; + const Y: u16 = 30; + + fn imp(s: u16, p: u16) -> CStmt { + CStmt { + s, + cop: Copula::Impl, + p, + } + } + + fn decls() -> Epi5Declarations { + let mut d = Epi5Declarations::new(); + d.declare( + CLASS, + RAIL, + Epi5Reading { + generation: Epi5Gen::V1, + }, + ); + d + } + + fn reading(d: &Epi5Declarations) -> Reading<'_> { + Reading { + declarations: d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + } + } + + fn edge(s: u16, o: u16, t: Topology2, c: Certification3) -> CausalEdge64 { + CausalEdge64::pack( + s as u8, + 0x91, + o as u8, + 200, + 200, + CausalMask::SO, + causal_edge::Orientation::from_code(0b101), + InferenceType::Deduction, + PlasticityState::S_HOT, + 0, + ) + .with_epistemic_raw5(EpistemicState5::new(Epi5Gen::V1, t, c).raw()) + } + + fn state(e: CausalEdge64) -> (Topology2, Certification3) { + let s = EpistemicState5::decode(Epi5Gen::V1, e.epistemic_raw5()).unwrap(); + (s.topology(), s.certification()) + } + + /// `A → B` from source 1, `B → Y` from source 2, and their deduction. + fn ledger_through(m: u16) -> DerivationLedger { + let mut l = DerivationLedger::new(); + l.observe(imp(A, m), TruthValue::new(0.9, 0.9), 1); + l.observe(imp(m, Y), TruthValue::new(0.9, 0.9), 2); + l.derive( + ChainId(1), + Law::Deduction, + [imp(m, Y), imp(A, m)], + imp(A, Y), + ) + .unwrap(); + l + } + + /// Sealed steps; the `u8` tag is deliberately not the predicate. + fn sealed(links: &[(u16, u16)]) -> Vec { + links + .iter() + .map(|&(s, o)| { + ( + 0xFF, + edge(s, o, Topology2::Direct, Certification3::Associated), + ) + }) + .collect() + } + + fn query() -> CausalEdge64 { + edge(A, Y, Topology2::IndirectUnknown, Certification3::Causes) + } + + /// Ledger and chain agree: `IndirectUnknown × Causes` (raw5 22) becomes + /// `IndirectKnown × Causes` (raw5 21), with the ledger's roots, and the + /// mediated path carries the conclusion. + #[test] + fn a_ledger_path_witnessed_by_the_chain_hydrates() { + let d = decls(); + let l = ledger_through(B); + let r = hydrate_from_ledger( + &l, + query(), + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d), + ) + .unwrap(); + assert_eq!(r.hydration, Hydration::Hydrated); + assert_eq!( + state(r.edge), + (Topology2::IndirectKnown, Certification3::Causes) + ); + assert_eq!(r.edge.epistemic_raw5(), 21); + assert_eq!(r.roots, [1, 2].into_iter().collect()); + assert!(!r.mediated.survives(), "the only path goes through B"); + } + + /// A ledger path whose links are not both in the sealed chain does not + /// hydrate: the edge keeps raw5 22. + #[test] + fn a_ledger_path_alone_does_not_hydrate() { + let d = decls(); + let l = ledger_through(B); + for links in [&[(A, B)][..], &[][..]] { + let r = hydrate_from_ledger(&l, query(), imp(A, Y), B, &sealed(links), reading(&d)) + .unwrap(); + assert_ne!(r.hydration, Hydration::Hydrated); + assert_eq!(r.edge, query()); + } + } + + /// No grounded ledger path through `B`: refused, even when the chain has + /// both links. Covers no derivation, a derivation through another + /// mediator, and a derivation whose premise has no evidence. + #[test] + fn the_adapter_needs_a_grounded_ledger_path_through_the_mediator() { + let d = decls(); + let chain = sealed(&[(A, B), (B, Y)]); + let run = |l: &DerivationLedger| { + hydrate_from_ledger(l, query(), imp(A, Y), B, &chain, reading(&d)) + }; + + assert_eq!( + run(&DerivationLedger::new()), + Err(MediatorRefusal::NoLedgerPath) + ); + assert_eq!(run(&ledger_through(C)), Err(MediatorRefusal::NoLedgerPath)); + + let mut ungrounded = DerivationLedger::new(); + ungrounded.observe(imp(B, Y), TruthValue::new(0.9, 0.9), 2); + ungrounded + .derive( + ChainId(1), + Law::Deduction, + [imp(B, Y), imp(A, B)], + imp(A, Y), + ) + .unwrap(); + assert_eq!(run(&ungrounded), Err(MediatorRefusal::NoLedgerPath)); + } + + /// With an independent direct observation of `A → Y`, removing the + /// mediated path leaves the conclusion: the path through `B` is not + /// individually necessary, though it still hydrates. + #[test] + fn a_redundant_mediated_path_is_not_reported_as_necessary() { + let d = decls(); + let mut l = ledger_through(B); + l.observe(imp(A, Y), TruthValue::new(0.8, 0.9), 3); + let r = hydrate_from_ledger( + &l, + query(), + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d), + ) + .unwrap(); + assert_eq!(r.hydration, Hydration::Hydrated); + assert!(r.mediated.survives()); + assert_eq!(r.mediated.after.unwrap().roots, [3].into_iter().collect()); + } + + #[test] + fn the_edge_must_be_the_target_relation() { + let d = decls(); + let l = ledger_through(B); + let other = edge(A, B, Topology2::IndirectUnknown, Certification3::Causes); + assert_eq!( + hydrate_from_ledger( + &l, + other, + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d) + ), + Err(MediatorRefusal::EdgeMismatch) + ); + assert_eq!( + hydrate_from_ledger(&l, query(), imp(A, Y), 300, &[], reading(&d)), + Err(MediatorRefusal::TermRange(300)) + ); + } +} diff --git a/crates/lance-graph-planner/src/nars/mod.rs b/crates/lance-graph-planner/src/nars/mod.rs index 4e6b8393e..3259a432d 100644 --- a/crates/lance-graph-planner/src/nars/mod.rs +++ b/crates/lance-graph-planner/src/nars/mod.rs @@ -15,6 +15,7 @@ pub mod ghost_prior; pub mod inference; pub mod insight; pub mod insights; +pub mod mediator; pub mod meta_basin; pub mod reach_out; pub mod regulate; @@ -23,6 +24,7 @@ pub mod support; pub mod tactic_select; pub mod tactics; pub mod truth; +pub mod warrant; pub use basin_resonance::{rank_basins, Basin, BasinKind, ResonanceConfig}; pub use belief::{Belief, BeliefArena, CStmt, Copula, ReviseOutcome, Stamp}; diff --git a/crates/lance-graph-planner/src/nars/support.rs b/crates/lance-graph-planner/src/nars/support.rs index e3036f10d..aeb789ab7 100644 --- a/crates/lance-graph-planner/src/nars/support.rs +++ b/crates/lance-graph-planner/src/nars/support.rs @@ -103,6 +103,17 @@ pub enum Refusal { Pool, } +/// Whether an explicit deduction step may chain two statements of `cop`. +/// +/// Wider than [`Copula::transits`], which governs blanket closure: `Impl` is +/// never closed transitively, but an admitted step may chain it, as the +/// copula's own documentation requires ("causal chaining goes through explicit +/// tactics"). The step earns NARS truth only; it certifies no cause. `Rel` +/// never composes. +fn composes(cop: Copula) -> bool { + matches!(cop, Copula::Inh | Copula::Sim | Copula::Impl) +} + /// The NARS law a derivation applies, as [`TruthValue`] implements it. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Law { @@ -136,7 +147,7 @@ impl Law { let [a, b] = premises; let drawn = match self { Law::Deduction => { - if a.cop != b.cop || !a.cop.transits() { + if a.cop != b.cop || !composes(a.cop) { return None; } if a.s == b.p { @@ -1109,6 +1120,16 @@ mod tests { assert!(l .derive(A, Law::Deduction, [rel(1, 2), rel(2, 3)], rel(1, 3)) .is_err()); + // An explicit implication step chains, though closure never would. + let imp = |s, p| CStmt { + s, + cop: Copula::Impl, + p, + }; + let mut chained = DerivationLedger::new(); + assert!(chained + .derive(A, Law::Deduction, [imp(1, 2), imp(2, 3)], imp(1, 3)) + .is_ok()); assert!(l.derivations().is_empty()); assert!(l.grounded_since(0).unwrap().is_empty()); assert!(l diff --git a/crates/lance-graph-planner/src/nars/warrant.rs b/crates/lance-graph-planner/src/nars/warrant.rs new file mode 100644 index 000000000..a80ca1937 --- /dev/null +++ b/crates/lance-graph-planner/src/nars/warrant.rs @@ -0,0 +1,725 @@ +//! `warrant`: which planner tactic may run on which grounded statements, and +//! what it may conclude (D-EPI-COT C3). +//! +//! A tactic runs only on [`Marker`]s. A marker is a statement whose evidence +//! comes from the [`DerivationLedger`] (truth and source roots) and whose +//! bits 59..63 project under a declared reading to an [`EpistemicState5`]. +//! [`fire`] checks every premise against the tactic's [`RecipeRule`], runs the +//! planner's own tactic function over the markers, admits each candidate into +//! the ledger, and returns [`Judgment`]s. +//! +//! # What a judgment may claim +//! +//! - **Truth:** the truth of the ledger proof through the new derivation, +//! returned with that proof's roots. It equals the tactic's own truth +//! unless a premise's evidence depends on the conclusion itself: the +//! ledger's cycle guard drops that evidence from the proof, and the +//! judgment reports what the proof actually rests on. +//! - **Roots:** the source roots of the proof through the new derivation, +//! which are the union of the premises' roots. A thought that replays the +//! same premises adds no root. +//! - **Epistemic state:** always `Unknown × Open`. A term-logic step earns no +//! certification and fixes no topology. Certification rises only through +//! `crate::pearl::reason` + `revise` (executed trial arms for `Causes`), and +//! topology only through `crate::pearl::hydrate`. Two `Causes` premises do +//! not make their deduction a cause: causation is not transitive in general. +//! - **Breadcrumb:** the [`ThoughtRef`] the step ran in (the 53..58 slot and +//! its generation). The operation is not written into the result. +//! +//! # The tactic law (policy pins) +//! +//! | recipe | tactic | requires | forbids | +//! |---|---|---|---| +//! | 4 | RCR abduction | `ASSOCIATED` | `INTERMEDIATE_KNOWN` | +//! | 6 | TR analogy | `ASSOCIATED` | — | +//! | 7 | ASC self-critique | `ASSOCIATED` | — | +//! | 8 | CAS induction / deduction | `ASSOCIATED` | — | +//! | 11 | CR revision | — | — | +//! +//! - DECISION: a Datapath tactic composes statements that have at least been +//! associated from independent sources; an `Open` statement has nothing to +//! compose. +//! - DECISION: RCR does not abduce a middle term for a relation whose mediator +//! is already known (the lab rule `HYDRATE_INTERMEDIATE` forbids the same). +//! - SCOPE: [`fire`] runs the Datapath tactics (4, 6, 8). ASC and CR are +//! revisions; in the ledger they are new observations, pooled by +//! [`DerivationLedger::pooled`]. +//! - BASIS: none measured; these are the smallest rules that make the +//! eligibility boundary testable. +//! - REVISIT WHEN: a tactic produces a measured wrong conclusion that a +//! stricter rule would have refused, or refuses a step a fixture needs. + +use std::collections::BTreeSet; + +use lance_graph_contract::band_reading::EdgeProvenance; +use lance_graph_contract::class_view::ClassId; +use lance_graph_contract::epistemic_state5::{ + fact, Certification3, Epi5Declarations, Epi5Gen, Epi5ReadError, EpistemicState5, RecipeRule, + Topology2, +}; +use lance_graph_contract::rail_geometry::RailAxis; + +use super::belief::{BeliefArena, CStmt, Stamp}; +use super::support::{ + Ablation, ChainId, DerivationId, DerivationLedger, NotAFigure, Refusal, SourceId, +}; +use super::tactics::{ + cas_abstract, rcr_abduce, tr_diverge, Throttle, ASC_ID, CAS_ID, CR_ID, RCR_ID, TR_ID, +}; +use super::truth::TruthValue; + +/// The thought a step ran in: the CE64 bits 53..58 slot (0 = WORLD) and the +/// slot's generation, so a reused slot is not mistaken for the old thought. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct ThoughtRef { + /// Slot `0..=63`. + pub slot: u8, + /// Generation of the slot. + pub generation: u32, +} + +/// Highest thought slot (six bits). +pub const MAX_SLOT: u8 = 63; + +/// The tactic law: a rule per recipe id. Recipes outside the table have no +/// rule and are never eligible. +#[must_use] +pub const fn tactic_rule(recipe: u8) -> Option { + match recipe { + RCR_ID => Some(RecipeRule::new(fact::ASSOCIATED, fact::INTERMEDIATE_KNOWN)), + TR_ID | ASC_ID | CAS_ID => Some(RecipeRule::new(fact::ASSOCIATED, 0)), + CR_ID => Some(RecipeRule::new(0, 0)), + _ => None, + } +} + +/// Where a statement's bits 59..63 came from and how they are declared. +#[derive(Clone, Copy)] +pub struct Declared<'a> { + /// The declarations. + pub declarations: &'a Epi5Declarations, + /// The statement's class. + pub class: ClassId, + /// The rail the class declared the reading on. + pub rail: RailAxis, + /// Where the bits came from. + pub provenance: EdgeProvenance, + /// The raw bits 59..63. + pub raw5: u8, +} + +/// A statement grounded in the ledger with a declared epistemic state. +/// Built only by [`Marker::ground`]. +#[derive(Debug, Clone, PartialEq)] +pub struct Marker { + stmt: CStmt, + truth: TruthValue, + roots: BTreeSet, + state: EpistemicState5, + thought: ThoughtRef, +} + +/// Why no marker was built. +#[derive(Debug, Clone, PartialEq)] +pub enum MarkerRefusal { + /// The ledger has no evidence for the statement. + NoEvidence(CStmt), + /// The ledger refused to evaluate. + Ledger(Refusal), + /// Bits 59..63 do not project under the declaration. + Epi5(Epi5ReadError), + /// The slot does not fit in six bits. + Slot(u8), +} + +impl Marker { + /// Ground `stmt`: truth and roots from the ledger's pooled evidence, + /// the state from the declared projection. + /// + /// # Errors + /// A [`MarkerRefusal`]. + pub fn ground( + ledger: &DerivationLedger, + stmt: CStmt, + declared: Declared<'_>, + thought: ThoughtRef, + ) -> Result { + if thought.slot > MAX_SLOT { + return Err(MarkerRefusal::Slot(thought.slot)); + } + let state = declared + .declarations + .project_state5( + declared.class, + declared.rail, + Epi5Gen::V1, + declared.raw5, + declared.provenance, + ) + .map_err(MarkerRefusal::Epi5)?; + let pooled = ledger + .pooled(stmt, &Ablation::none()) + .map_err(MarkerRefusal::Ledger)? + .ok_or(MarkerRefusal::NoEvidence(stmt))?; + Ok(Self { + stmt, + truth: pooled.truth, + roots: pooled.roots, + state, + thought, + }) + } + + /// The statement. + #[must_use] + pub fn stmt(&self) -> CStmt { + self.stmt + } + /// Its pooled truth when grounded. + #[must_use] + pub fn truth(&self) -> TruthValue { + self.truth + } + /// Its source roots when grounded. + #[must_use] + pub fn roots(&self) -> &BTreeSet { + &self.roots + } + /// Its declared epistemic state. + #[must_use] + pub fn state(&self) -> EpistemicState5 { + self.state + } + /// The thought it was grounded in. + #[must_use] + pub fn thought(&self) -> ThoughtRef { + self.thought + } +} + +/// A Datapath tactic step. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Step { + /// RCR: abduction over every shared predicate (recipe 4). + Rcr, + /// TR: analogy from a focus statement (recipe 6). + Tr(CStmt), + /// CAS: induction and deduction around a focus subject (recipe 8). + Cas(u16), +} + +impl Step { + /// The recipe id the step implements. + #[must_use] + pub fn recipe(self) -> u8 { + match self { + Step::Rcr => RCR_ID, + Step::Tr(_) => TR_ID, + Step::Cas(_) => CAS_ID, + } + } +} + +/// What a step concluded. +#[derive(Debug, Clone, PartialEq)] +pub struct Judgment { + /// The conclusion. + pub stmt: CStmt, + /// The truth of the proof through [`Self::derivation`]. + pub truth: TruthValue, + /// The derivation admitted into the ledger. + pub derivation: DerivationId, + /// Roots of the proof through that derivation. + pub roots: BTreeSet, + /// The thought the step ran in. + pub thought: ThoughtRef, + /// Always `Unknown × Open`: see the module documentation. + pub state: EpistemicState5, +} + +/// Why a step did not run, or stopped. +#[derive(Debug, Clone, PartialEq)] +pub enum FireRefusal { + /// No markers. + NoPremises, + /// Two markers name the same statement. + DuplicatePremise(CStmt), + /// The recipe has no rule. + NoRule(u8), + /// A premise's state does not satisfy the rule. + Ineligible { + /// The premise. + stmt: CStmt, + /// Its state. + state: EpistemicState5, + /// The recipe. + recipe: u8, + }, + /// A premise's ledger evidence changed after its marker was built. + Stale(CStmt), + /// The ledger refused. + Ledger(Refusal), + /// The ledger refused a candidate's figure. + Figure(NotAFigure), + /// No proof uses the admitted derivation. + NoProof(CStmt), +} + +/// The state every judgment carries. +pub const JUDGMENT_STATE: EpistemicState5 = + EpistemicState5::new(Epi5Gen::V1, Topology2::Unknown, Certification3::Open); + +/// Run `step` over `markers` in `chain`, as thought `thought`. +/// +/// Refuses before anything is admitted when a premise is ineligible or stale. +/// +/// # Errors +/// A [`FireRefusal`]. +pub fn fire( + ledger: &mut DerivationLedger, + chain: ChainId, + thought: ThoughtRef, + step: Step, + markers: &[Marker], +) -> Result, FireRefusal> { + if markers.is_empty() { + return Err(FireRefusal::NoPremises); + } + let recipe = step.recipe(); + let rule = tactic_rule(recipe).ok_or(FireRefusal::NoRule(recipe))?; + let mut arena = BeliefArena::new(); + let mut seen: Vec = Vec::new(); + for m in markers { + if seen.contains(&m.stmt) { + return Err(FireRefusal::DuplicatePremise(m.stmt)); + } + seen.push(m.stmt); + if !rule.admits(m.state) { + return Err(FireRefusal::Ineligible { + stmt: m.stmt, + state: m.state, + recipe, + }); + } + let now = ledger + .pooled(m.stmt, &Ablation::none()) + .map_err(FireRefusal::Ledger)?; + if now.as_ref().map(|p| (p.truth, &p.roots)) != Some((m.truth, &m.roots)) { + return Err(FireRefusal::Stale(m.stmt)); + } + let stamp = m + .roots + .iter() + .fold(Stamp(0), |s, &r| s.union(Stamp::source(r))); + arena.observe(m.stmt, m.truth, stamp); + } + + let throttle = Throttle::permissive(); + let frontier = match step { + Step::Rcr => rcr_abduce(&arena, &throttle), + Step::Tr(focus) => tr_diverge(&arena, focus), + Step::Cas(subject) => cas_abstract(&arena, subject, &throttle), + }; + + let mut out = Vec::with_capacity(frontier.candidates.len()); + for c in &frontier.candidates { + let derivation = ledger + .admit(chain, &arena, c) + .map_err(FireRefusal::Figure)?; + let proof = ledger + .proofs(c.stmt, &Ablation::none()) + .map_err(FireRefusal::Ledger)? + .into_iter() + .find(|p| p.uses.contains(&derivation)) + .ok_or(FireRefusal::NoProof(c.stmt))?; + out.push(Judgment { + stmt: c.stmt, + truth: proof.truth, + derivation, + roots: proof.roots, + thought, + state: JUDGMENT_STATE, + }); + } + Ok(out) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::nars::belief::Copula; + use crate::pearl::{reason, revise, Edit, Evidence, Reading}; + use causal_edge::edge::{CausalEdge64, InferenceType}; + use causal_edge::{CausalMask, PlasticityState}; + use lance_graph_contract::causal_audit::SupportBasis; + use lance_graph_contract::certification::ModelBuilder; + use lance_graph_contract::epistemic_state5::Epi5Reading; + + const CLASS: ClassId = 0x0902; + const RAIL: RailAxis = RailAxis::Taxonomy; + const THOUGHT: ThoughtRef = ThoughtRef { + slot: 1, + generation: 1, + }; + + fn inh(s: u16, p: u16) -> CStmt { + CStmt { + s, + cop: Copula::Inh, + p, + } + } + + fn decls() -> Epi5Declarations { + let mut d = Epi5Declarations::new(); + d.declare( + CLASS, + RAIL, + Epi5Reading { + generation: Epi5Gen::V1, + }, + ); + d + } + + fn raw(t: Topology2, c: Certification3) -> u8 { + EpistemicState5::new(Epi5Gen::V1, t, c).raw() + } + + fn declared(d: &Epi5Declarations, raw5: u8) -> Declared<'_> { + Declared { + declarations: d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + raw5, + } + } + + /// `1 → 9` from source 1 and `2 → 9` from source 2: a shared predicate. + fn ledger() -> DerivationLedger { + let mut l = DerivationLedger::new(); + l.observe(inh(1, 9), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(2, 9), TruthValue::new(0.8, 0.9), 2); + l + } + + fn markers(l: &DerivationLedger, d: &Epi5Declarations, raw5: u8) -> Vec { + [inh(1, 9), inh(2, 9)] + .into_iter() + .map(|s| Marker::ground(l, s, declared(d, raw5), THOUGHT).expect("grounded")) + .collect() + } + + /// The acceptance path: RCR runs on two grounded markers, its candidates + /// enter the ledger, and each judgment carries the tactic's truth, the + /// union of the premises' roots, the thought, and `Unknown × Open`. + #[test] + fn a_tactic_consumes_grounded_markers_and_keeps_their_roots() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).expect("eligible"); + + assert_eq!(js.len(), 2, "1→2 and 2→1"); + assert_eq!(l.derivations().len(), 2); + let both: BTreeSet = [1, 2].into_iter().collect(); + for j in &js { + assert_eq!(j.roots, both); + assert_eq!(j.thought, THOUGHT); + assert_eq!(j.state, JUDGMENT_STATE); + let pooled = l.pooled(j.stmt, &Ablation::none()).unwrap().unwrap(); + assert_eq!(pooled.truth, j.truth, "the ledger agrees with the tactic"); + } + let (rule, obs) = (TruthValue::new(0.8, 0.9), TruthValue::new(0.9, 0.9)); + let j12 = js.iter().find(|j| j.stmt == inh(1, 2)).expect("1→2"); + assert_eq!(j12.truth, rule.abduction(&obs)); + } + + /// Eligibility follows the declared facts only: `Open` refuses, the same + /// topology at `Associated` runs; for RCR a known mediator refuses where + /// an unknown one runs, while CAS takes both. A refusal admits nothing. + #[test] + fn eligibility_follows_the_declared_facts() { + let d = decls(); + let cases = [ + (Step::Rcr, Topology2::Direct, Certification3::Open, false), + ( + Step::Rcr, + Topology2::Direct, + Certification3::Associated, + true, + ), + ( + Step::Rcr, + Topology2::IndirectKnown, + Certification3::Associated, + false, + ), + ( + Step::Rcr, + Topology2::IndirectUnknown, + Certification3::Associated, + true, + ), + ( + Step::Cas(1), + Topology2::IndirectKnown, + Certification3::Associated, + true, + ), + ( + Step::Cas(1), + Topology2::Unknown, + Certification3::Open, + false, + ), + ]; + for (step, t, c, ok) in cases { + let mut l = ledger(); + let ms = markers(&l, &d, raw(t, c)); + let r = fire(&mut l, ChainId(1), THOUGHT, step, &ms); + match (ok, r) { + (true, Ok(_)) => {} + (false, Err(FireRefusal::Ineligible { recipe, .. })) => { + assert_eq!(recipe, step.recipe()); + assert!(l.derivations().is_empty(), "a refusal admits nothing"); + } + (_, other) => panic!("{step:?} on {t:?} × {c:?}: {other:?}"), + } + } + } + + /// No evidence, an undeclared class, untrusted provenance or an + /// out-of-range slot: no marker. + #[test] + fn a_marker_needs_evidence_and_a_declared_reading() { + let d = decls(); + let l = ledger(); + let ok = raw(Topology2::Direct, Certification3::Associated); + assert_eq!( + Marker::ground(&l, inh(3, 9), declared(&d, ok), THOUGHT), + Err(MarkerRefusal::NoEvidence(inh(3, 9))) + ); + let mut undeclared = declared(&d, ok); + undeclared.class = 0x0903; + assert_eq!( + Marker::ground(&l, inh(1, 9), undeclared, THOUGHT), + Err(MarkerRefusal::Epi5(Epi5ReadError::UndeclaredClass(0x0903))) + ); + let mut legacy = declared(&d, ok); + legacy.provenance = EdgeProvenance::V1Legacy; + assert!(matches!( + Marker::ground(&l, inh(1, 9), legacy, THOUGHT), + Err(MarkerRefusal::Epi5(Epi5ReadError::UnknownProvenance(_))) + )); + let far = ThoughtRef { + slot: 64, + generation: 0, + }; + assert_eq!( + Marker::ground(&l, inh(1, 9), declared(&d, ok), far), + Err(MarkerRefusal::Slot(64)) + ); + } + + /// Premises at `Causes` do not make a judgment a cause: every eligible + /// premise state yields `Unknown × Open`. The only promotion is an + /// executed trial through `pearl`: observation alone leaves the edge + /// `Open`, and the trial arms raise it. + #[test] + fn a_judgment_is_never_promoted_by_its_premises() { + let d = decls(); + let rule = tactic_rule(RCR_ID).unwrap(); + for t in Topology2::ALL { + for c in Certification3::ALL { + let state = EpistemicState5::new(Epi5Gen::V1, t, c); + if !rule.admits(state) { + continue; + } + let mut l = ledger(); + let ms = markers(&l, &d, state.raw()); + for j in fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap() { + assert_eq!(j.state, JUDGMENT_STATE, "premises at {t:?} × {c:?}"); + } + } + } + + let edge = CausalEdge64::pack( + 1, + 0x91, + 2, + 200, + 200, + CausalMask::PO, + causal_edge::Orientation::from_code(0b101), + InferenceType::Deduction, + PlasticityState::S_HOT, + 0, + ) + .with_epistemic_raw5(JUDGMENT_STATE.raw()); + let reading = Reading { + declarations: &d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + }; + let mut b = ModelBuilder::new(); + b.cell(0, true, 5, 4); + b.cell(0, false, 5, 1); + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + let observed = b.build(); + let m = reason( + edge, + &Evidence { + model: &observed, + chain: None, + }, + Edit::None, + ); + let after = revise(&m, reading).unwrap(); + assert_eq!(after.epistemic_raw5(), JUDGMENT_STATE.raw()); + + b.arm(true, 6, 5); + b.arm(false, 6, 1); + b.sources(SupportBasis::InterventionBacked, &[10, 11]); + let trial = b.build(); + let m = reason( + edge, + &Evidence { + model: &trial, + chain: None, + }, + Edit::None, + ); + let after = revise(&m, reading).unwrap(); + assert_eq!( + EpistemicState5::decode(Epi5Gen::V1, after.epistemic_raw5()) + .unwrap() + .certification(), + Certification3::Causes + ); + } + + /// A premise whose pooled evidence runs through the conclusion: `1 → 9` + /// is observed weakly and also derived through `1 → 2`. RCR then + /// proposes `1 → 2` from `1 → 9` and `2 → 9`. The admitted proof cannot + /// use the derivation through `1 → 2` (it would support itself), so the + /// judgment carries the proof's weaker truth and its roots, not the + /// snapshot truth. + #[test] + fn a_judgment_reports_the_truth_its_roots_support() { + let d = decls(); + let mut l = DerivationLedger::new(); + l.observe(inh(1, 2), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(2, 9), TruthValue::new(0.9, 0.9), 2); + l.observe(inh(1, 9), TruthValue::new(0.1, 0.1), 3); + l.derive( + ChainId(0), + crate::nars::support::Law::Deduction, + [inh(1, 2), inh(2, 9)], + inh(1, 9), + ) + .unwrap(); + let st = raw(Topology2::Direct, Certification3::Associated); + let ms: Vec = [inh(1, 9), inh(2, 9)] + .into_iter() + .map(|s| Marker::ground(&l, s, declared(&d, st), THOUGHT).unwrap()) + .collect(); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap(); + let j = js.iter().find(|j| j.stmt == inh(1, 2)).expect("1→2"); + let snapshot = ms[1].truth().abduction(&ms[0].truth()); + assert!(j.truth.confidence < snapshot.confidence / 10.0); + let proof = l + .proofs(inh(1, 2), &Ablation::none()) + .unwrap() + .into_iter() + .find(|p| p.uses.contains(&j.derivation)) + .unwrap(); + assert_eq!(j.truth, proof.truth); + assert_eq!(j.roots, proof.roots); + assert!( + !j.roots.contains(&1), + "the conclusion's own source is not a root" + ); + } + + /// The same step in 63 thoughts admits 63 derivations, and the + /// conclusion's pooled truth and roots stay those of one. + #[test] + fn replaying_a_step_in_many_thoughts_adds_no_evidence() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + let once = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap(); + let target = once[0].stmt; + let first = l.pooled(target, &Ablation::none()).unwrap().unwrap(); + for slot in 2..=MAX_SLOT { + let t = ThoughtRef { + slot, + generation: 1, + }; + fire(&mut l, ChainId(u32::from(slot)), t, Step::Rcr, &ms).unwrap(); + } + assert_eq!(l.derivations().len(), 2 * 63); + let after = l.pooled(target, &Ablation::none()).unwrap().unwrap(); + assert_eq!(after.truth, first.truth); + assert_eq!(after.roots, first.roots); + } + + /// A marker built before its statement's evidence changed is refused, + /// and nothing is admitted. + #[test] + fn a_stale_marker_is_refused() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + l.observe(inh(1, 9), TruthValue::new(0.1, 0.9), 3); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms), + Err(FireRefusal::Stale(inh(1, 9))) + ); + assert!(l.derivations().is_empty()); + } + + /// CAS on a focus subject admits induction and deduction, each a valid + /// figure, with the tactic's truth. + #[test] + fn cas_deduction_runs_on_grounded_markers() { + let d = decls(); + let mut l = DerivationLedger::new(); + l.observe(inh(1, 5), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(5, 7), TruthValue::new(0.8, 0.9), 2); + let st = raw(Topology2::Direct, Certification3::Associated); + let ms: Vec = [inh(1, 5), inh(5, 7)] + .into_iter() + .map(|s| Marker::ground(&l, s, declared(&d, st), THOUGHT).unwrap()) + .collect(); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Cas(1), &ms).unwrap(); + let ded = js + .iter() + .find(|j| j.stmt == inh(1, 7)) + .expect("1→7 by deduction"); + assert_eq!( + ded.truth, + TruthValue::new(0.8, 0.9).deduction(&TruthValue::new(0.9, 0.9)) + ); + assert_eq!(ded.roots, [1, 2].into_iter().collect()); + } + + #[test] + fn a_duplicate_premise_is_refused() { + let d = decls(); + let mut l = ledger(); + let mut ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + ms.push(ms[0].clone()); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms), + Err(FireRefusal::DuplicatePremise(inh(1, 9))) + ); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &[]), + Err(FireRefusal::NoPremises) + ); + } +} diff --git a/docs/research/epistemic-cot/c3-plan.md b/docs/research/epistemic-cot/c3-plan.md index ce2e4c04d..1e5d513e1 100644 --- a/docs/research/epistemic-cot/c3-plan.md +++ b/docs/research/epistemic-cot/c3-plan.md @@ -1,7 +1,7 @@ # D-EPI-COT C3 — plan: Epi5 bridge, scenting, numerical learning -Status: PLAN. Nothing here is implemented. C1/C2 (`nars::support`) is unchanged -by this document. +Status: PLAN, with the first C3 slice delivered (§8). C1/C2 (`nars::support`) +is unchanged. C3 has three parts, in this order: @@ -169,3 +169,161 @@ The learned output is a ranking. It is never passed in as an observation. 2. Whether the `learn` gate's behaviour on `deepnsm-v2` edges is a live defect, which depends on whether those edges ever reach `learn`. 3. Where the TFLite kernels live (§5). + +## 8. Delivered: first C3 slice + +Source pins: lance-graph main `694b243bd`, ndarray master `2cbe131`. + +### Owner and overlap map + +| file | owner contract | change | +|---|---|---| +| `lance-graph-contract/src/epistemic_state5.rs` | D-EPI-CANON-0 | adds `RecipeRule` (additive) | +| `lance-graph-contract/src/certification.rs` | P7a #1369 / D-PEARL-PROD-0 | adds `CertificationModel::measured_only` (additive) | +| `lance-graph-planner/src/nars/warrant.rs` | D-EPI-COT (new) | new module | +| `lance-graph-planner/src/pearl.rs` | D-PEARL-PROD-0 | unchanged; still the only writer of bits 59..63 | +| `cognitive-shader-driver/examples/shared/affordance_law.rs` | D-GSO-AFF-0 | unchanged; still uses its own rule type (follow-up) | + +EXO-50, read to its latest message (08:45Z): no open message claims these +files. Numeric admission stays with EXO-152. + +### What runs + +- **`RecipeRule`** (contract): `requires` / `forbids` over declared facts, a + per-state check and the V1 population. This moves the lab law's rule into the + contract. The lab still has its own copy; switching it over is a follow-up. +- **`CertificationModel::measured_only`** (contract): units whose outcome + was not measured are excluded from every mask, including the trial arms, + instead of being read as negatives. An arm left with no measured unit + refuses with `EmptyArm`. +- **`nars::warrant`** (planner): + - **`Marker::ground`** builds a marker from three things: the ledger's + pooled truth and roots, the bits 59..63 projected through + `Epi5Declarations`, and the thought slot and generation. It refuses + with `NoEvidence`, an `Epi5` read error, or `Slot`. + - **`tactic_rule`** gives the eligibility rule for recipes 4, 6, 7, 8 + and 11. These are policy pins, documented in the module. + - **`fire`**: + 1. checks every premise against its rule; + 2. refuses a stale or duplicate marker; + 3. runs the planner's own RCR, TR or CAS function; + 4. admits each candidate through `DerivationLedger::admit`. + + Each judgment carries the tactic's truth, the roots of the proof through + the new derivation, the thought, and `Unknown × Open`. + +### Falsifiers + +Each is disable-verified: the named disable turns its test red. + +| falsifier | test | disable | +|---|---|---| +| acceptance path, roots preserved | `a_tactic_consumes_grounded_markers_and_keeps_their_roots` | — | +| eligibility follows declared facts | `eligibility_follows_the_declared_facts` | skip the rule check; drop RCR's `forbids` | +| no marker without evidence or declaration | `a_marker_needs_evidence_and_a_declared_reading` | skip the slot check | +| no promotion from premises; only trial arms promote | `a_judgment_is_never_promoted_by_its_premises` | judgment takes a premise's state | +| replayed thoughts add no evidence | `replaying_a_step_in_many_thoughts_adds_no_evidence` | — (ledger L7) | +| stale marker refused | `a_stale_marker_is_refused` | skip the staleness check | +| duplicate premise refused | `a_duplicate_premise_is_refused` | skip the duplicate check | +| UNKNOWN is not negative | `unmeasured_outcomes_are_not_read_as_negatives` | trial arms not restricted (red only after adding unmeasured control units) | +| rule population | `a_recipe_rule_population_matches_its_per_state_check` | `holds` ignores `forbids` | + +L1–L5 are already pinned by `pearl.rs` tests; this slice does not duplicate +them: + +- L1: `f1_observation_alone_never_promotes_to_causes`. +- L2 and L3: `cui_bono_script_moves_the_state_only_where_evidence_earned_it`, + which ends at `IndirectKnown × Causes`. +- L4: `hydration_only_promotes_the_edge_whose_path_it_is` and + `f5_a_proposed_beneficiary_is_not_evidence`. +- L5: `f7_one_at_a_time_removal_is_not_the_definition_of_causality`, the + overdetermined trial. + +### Clippy + +`cargo clippy -p lance-graph-planner --lib --tests -D warnings` reports the +same 8 sites on main `694b243bd` as on this branch: +`nested_bands.rs` 601/978/1025, `cache/nars_engine.rs:1413` and +`tests/moore_nars16_probe.rs`. `--lib` alone is clean. + +### Still open + +- **Statistics:** effect size, sample-size bounds, uncertainty, and + multiple-comparison correction across the up to five populations + `associated` tries. Today `CertificationModel` reports none of these, and + nothing here asserts more than it reports. +- **Missingness:** missing-at-random is assumed by `measured_only`; it is + not tested. +- **ASC and CR (7, 11)** are not run through `fire`. They are revisions, + and the ledger already pools them. +- **The lab affordance law** still has its own rule type. +- **C3b and C3c,** which wait on the decisions in §7. + +## 9. Ledger → `pearl::hydrate` seam + +**Existing:** `planner::pearl::{reason, revise, hydrate}` (#1390/#1391) already +writes bits 59..63. `hydrate` moves `IndirectUnknown` to `IndirectKnown` when +both bindings `A → B` and `B → Y` are in the sealed chain. None of the files +named `hydrate.rs` is that gate: + +- `deepnsm-v2/src/hydrate.rs` addresses parsed triples to their verse; +- `lance-graph/src/graph/hydrate.rs` loads bgz7 vectors into Lance; +- `bgz-tensor/src/hydrate.rs` is a download binary. + +**Added:** `nars::mediator::hydrate_from_ledger`. + +1. It finds the ledger's grounded deductions of `A → Y` through `B`. +2. It hands the path to the unchanged `pearl::hydrate`. +3. It returns a receipt: derivation ids, source roots, the `Hydration` + result, the edge after `hydrate`, and `A → Y`'s sensitivity with the + mediated derivations removed. + +What each side is allowed to do: + +- **The ledger never creates a chain.** A ledger path whose links are not + both in the sealed chain leaves the edge unchanged. +- **The adapter refuses a chain-only path.** If the ledger has no grounded + path through `B`, there is no receipt. +- **Only subject and object are read** from each chain step. The step tag is + not a predicate; that was the #1572 guard, which was withdrawn. + +To record causal mediator paths, `Law::Deduction` now admits `Impl` in an +explicit step: + +- `Copula::transits` still keeps `Impl` out of blanket closure, and `Rel` + still never composes. +- The step earns NARS truth only. It certifies nothing. + +| falsifier | test | disable | +|---|---|---| +| chain-witnessed ledger path hydrates (raw5 22 → 21) with roots | `a_ledger_path_witnessed_by_the_chain_hydrates` | — | +| ledger path alone does not hydrate | `a_ledger_path_alone_does_not_hydrate` | — (`pearl::hydrate` owns it) | +| grounded path through B required | `the_adapter_needs_a_grounded_ledger_path_through_the_mediator` | accept ungrounded derivations; accept any mediator | +| redundant mediated path not reported as necessary | `a_redundant_mediated_path_is_not_reported_as_necessary` | — | +| edge must be the target | `the_edge_must_be_the_target_relation` | skip the edge check | +| `Impl` chains, `Rel` never | `l8_an_invalid_figure_is_not_admitted` | `Rel` composes; `Impl` refused | + +**One disable did not bind on its first form.** Falling back to "any proof" +changed nothing, because without evidence there are no proofs at all. +Accepting derivations without a proof does bind, and that is the form +recorded. + +**Maturation (operator, 2026-10-28):** `7 = Staunen … 0 = Wisdom` (the #1494 +order) is the order for new, explicitly declared maturation readings. + +- Wisdom stays revisable: an independently witnessed contradiction reopens + it. +- No existing class is reinterpreted. `deepnsm-v2` keeps its opposite + `novelty_wisdom` order. +- Before any production write, four things must be settled: the reading, + its provenance, a migration, and the `CausalEdge64::learn` collision. +- Until then, maturation stays transient and fail-closed. + +**TFLite (operator, 2026-10-28):** the kernels are in `AdaWorldAPI/ndarray`: + +- `src/simd_fixedpoint.rs`: TFLite fixed-point arithmetic; +- `src/simd_stride.rs`: `lut9`; +- `src/hpc/codec9.rs`: Palette512. + +`AdaWorldAPI/tflite-micro` is the reference, and lance-graph #1800 has the +softmax oracle. No `lance-graph-tflite` crate. No training kernel exists yet.