diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 9367774c6..f4c8e51a0 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -34,6 +34,7 @@ Plan: `.claude/plans/2026-10-06-global-sudoku-replayable-orchestration-v1.md`. O | **D-GSO-5** | P5: first recipe quartet over existing primitives | Shipped (#1355) | `cognitive-shader-driver/examples/recipe_quartet_probe.rs`: four `match`-arm recipes over `Quorum::observe`, `Quad8::fold_product`, `Morton8x8` + `PalettePerturbation::hop`, `GadamerRevision::revise` (verdict left `NotRun`: removing the new roots is tautological, so the counterfactual moves to P7); a thread-local counting allocator shows zero allocations per recipe (no instruction vector); `ProbeRecipe` is its own type, not a shipped `recipes` ID; ordinal meanings not canonized; no Pearl projection (P7) and no selector (P6); 7 tests, 6 disable runs red | | **D-GSO-6** | P6: deterministic, versioned recipe selector | Shipped (#1358, #1362, #1365); `observations_pending` + `frontier_bounded` wired, `new_encounter` → `revision_pending`: In PR | `cognitive-shader-driver/examples/recipe_selector_probe.rs`: `SelectorPolicy::select(state)` is a pure `const fn` over a declared 4-fact `EpistemicState`; V1 = §11 order (fold, bound, local, revise), rests only on the settled state; V2 swaps two steps (differs on 2 of 16 states); a recorded `Selection` (policy + state) replays under its own policy; every cycle rests in one step per open condition and replays identically; the version covers selection only, not recipe implementations (§13 digest open); 5 tests, 5 disable runs red. Follow-up: `new_encounter` is derived from the world (revising would still change a horizon mask; equals `revise` changing it on a 2-bit universe; rootless revisions included) and the `Revision` recipe writes `GadamerRevision`'s `delta.resulting`; dropping that write never rests; `unresolved_tension` cannot drive `local_disagreement` (never cleared); the other three facts are still stand-ins; 14 tests, 10 disable runs red. Follow-up 2: `local_disagreement` = `unresolved_tension \ interrogated`, where `interrogated` is the coverage `MooreInterrogation` writes (tension itself never cleared); a revision adding a new contradiction reopens it; dropping the interrogation write never rests; `observations_pending` and `frontier_bounded` remain stand-ins; 17 tests, 15 disable runs red. Follow-up 3: `new_encounter` renamed `revision_pending` (revising would change the horizon); `observations_pending` = arrived verdicts > verdicts the `Quorum` counted (silence included; `speaking()` would never rest on a silent source); dropping the fold write never rests; coverage stays per tension bit (new evidence on a covered bit does not reopen); `frontier_bounded` = a recorded `Quad8::fold_product` frontier exists for the current candidate space (a changed space reopens it; an empty frontier is bounded); no stand-in fact remains in the wired cycle; 25 tests, 25 disable runs red | | **D-GSO-7** | P7: reasoning-band earning and downgrade | Shipped (#1360) | `cognitive-shader-driver/examples/reasoning_band_probe.rs`: `ReasoningBand` (bits 61..63) read only via `band_reading::project_band`; earned one rung per executed passing proof under the shipped Pearl `CausalMask` (SO majority → Association, PO intervention trial passed → Causal, SPO removal attack passed → Counterfactual), outcomes executed from trial data and never supplied, no skipping, `NotRun` never raises; failed test, contradicting `Quorum` (minority caps at Association, majority drops to Surface) and `simpsons_paradox_risk` lower it; replay gives the same edge bits; unreadable provenance / undeclared / band-absent refuse; ladder and thresholds are policy pins; 7 tests, 10 disable runs red | +| **D-GSO-7a** | P7a: the reasoning band as a relational certification (supersedes the meaning of D-GSO-7's rungs; #1360 unchanged) | In PR | `cognitive-shader-driver/examples/relational_certification_probe.rs`: a reading declared per class over bits 61..63 (`0 Open, 1 Associated, 2 Related, 3 Contributes, 4 CausalCandidate, 5 Causes`, 6..7 refuse; a class declared under the historical reading refuses the same bits); contracts are integer folds over unit masks + `causal_audit::SupportLedger` (2 distinct sources; the robustness mask only refutes; `Causes` = 2 distinct `InterventionBacked` sources + executed randomized arms); `entails` is an explicit table equal to `code >=` on 0..=5 only; repetition, observational effect size, the inference mantissa and confounded observational data never raise or demote past their contract; exhaustive 2,500-model family: 0 chain violations with scoped association, 10 with marginal (Simpson); sibling specificity and removal (overdetermination) are shown not to be rungs; only receipts recorded at or before the model's seal count, so a later receipt cannot change an earlier seal's replay; 13 tests, 12 disable runs red | | **D-GSO-8** | P8: seal boundary | Shipped (#1363) | `lance-graph-planner/examples/seal_boundary_probe.rs`: internal events change only working rows; a declared `Boundary` event freezes the changed rows with the shipped `DetachedCycleBatch::freeze` into a local ledger (no `WalSink`); an unchanged boundary writes nothing; replaying the persisted events from each prior seal reproduces the next seal exactly (frame, landings, image, hash); wrong base, dropped event and swapped order each change the seal; tie limit handled by plan option 1: the key is the event's own durable unique `seq`, a tied batch is refused, and a test shows on the real `freeze` that tied keys make the seal arrival-dependent; 6 tests, 5 disable runs red. Follow-up: `apply` refuses a `seq` not greater than the last (a reuse on one row or across seals escaped `first_tie`), `resume_after` restores the top persisted key; 7 tests, 2 more disable runs red | ## D-PLX — Population-law cross-check (2026-10-03) diff --git a/.claude/board/entries/2026-10-06-reasoning-band-as-relational-certification.md b/.claude/board/entries/2026-10-06-reasoning-band-as-relational-certification.md new file mode 100644 index 000000000..33d2a5c95 --- /dev/null +++ b/.claude/board/entries/2026-10-06-reasoning-band-as-relational-certification.md @@ -0,0 +1,44 @@ +# 2026-10-06 — D-GSO-7a: the reasoning band as a relational certification + +## MEASURED + +`crates/cognitive-shader-driver/examples/relational_certification_probe.rs`: +13 tests, 12 disable runs red. Supersedes the **meaning** of D-GSO-7's rungs; +`#1360`'s probe and its board row are unchanged. + +- **Inventory before the change.** `ReasoningBand` has no production writer + (`with_reasoning_band` is called only in tests and examples). No class + outside examples declares `BandPresence::Present`, so every production read + refuses. The one library reader, `dismech_counterfactual::EdgeRole`, copies + the band without deciding on it. The one raw ordinal comparison is + `reasoning_band_probe.rs`'s `cap()`, which ranks `Perspective` / `Meta` / + `Transcendent` above `Counterfactual`. +- **Reading, declared per class.** Bits 61..63 = + `0 Open, 1 Associated, 2 Related, 3 Contributes, 4 CausalCandidate, 5 Causes`; + 6 and 7 refuse. `ReasoningBand` is used only as the 3-bit carrier. A class + declared under the historical reading refuses the same bits. Working names. +- **Order.** `entails` is an explicit table and equals `code >=` on 0..=5. + Historical `Meta` (6) and `Transcendent` (7) do not satisfy `Causes`. +- **Chain vs partial order.** Exhaustive family of 2,500 two-stratum models: + 0 implication violations with `Associated` existential over the declared + populations; 10 with marginal association (Contributes without it; Simpson). + Certified per code `[1100, 144, 610, 259, 387, 0]`. +- `Causes` holds against a confounded observational population when the + randomized arms certify it, and entails the lower contracts in the trial + population. #1360's confounding cap would demote it. +- Sibling specificity is not a rung: A and an equally effective sibling give + `Causes` while A is not discriminative against the sibling. +- Only receipts recorded at or before the model's seal count, so a later + receipt cannot change what an earlier seal replays to (codex review). +- Removal is not the causal test: under Y = A or B, removing A from a unit with + B leaves Y while the population trial certifies `Causes`. + +## OPEN + +- Whether the reading becomes a `band_reading` lens (contract change), and the + final names. +- `CausalCandidate` carries ordering only. +- Scoped association is only sound if strata are declared before the data + are read; nothing enforces that yet. +- The robustness mask is an input; no CLAM/CHAODA mask has been run on real data. +- Sibling and overdetermination tests are existence witnesses, not guards. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index dfa385e84..7081a13e3 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ 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. -229 entries, 2026-08-06 .. 2026-10-06. +230 entries, 2026-08-06 .. 2026-10-06. | date | entry id | finding | file | |---|---|---|---| @@ -34,6 +34,7 @@ exactly one of them, never both. | 2026-10-06 | `D-GSO-6` | | [2026-10-06-selector-revision-wired.md](2026-10-06-selector-revision-wired.md) | | 2026-10-06 | `selector-observations-wired` | | [2026-10-06-selector-observations-wired.md](2026-10-06-selector-observations-wired.md) | | 2026-10-06 | `selector-local-disagreement-wired` | | [2026-10-06-selector-local-disagreement-wired.md](2026-10-06-selector-local-disagreement-wired.md) | +| 2026-10-06 | `D-GSO-7a` | | [2026-10-06-reasoning-band-as-relational-certification.md](2026-10-06-reasoning-band-as-relational-certification.md) | | 2026-10-06 | `quack-r2il-one-evaluator-round4` | | [2026-10-06-quack-r2il-one-evaluator-round4.md](2026-10-06-quack-r2il-one-evaluator-round4.md) | | 2026-10-06 | `D-MORTON-0` | | [2026-10-06-morton8x8-checked-address.md](2026-10-06-morton8x8-checked-address.md) | | 2026-10-06 | `diff-plateau-as-expression-round5` | | [2026-10-06-diff-plateau-as-expression-round5.md](2026-10-06-diff-plateau-as-expression-round5.md) | diff --git a/crates/cognitive-shader-driver/Cargo.toml b/crates/cognitive-shader-driver/Cargo.toml index d2b67cf60..2f75f83e8 100644 --- a/crates/cognitive-shader-driver/Cargo.toml +++ b/crates/cognitive-shader-driver/Cargo.toml @@ -97,6 +97,11 @@ test = true name = "reasoning_band_probe" test = true +# D-GSO-7a relational-certification probe; tests run under `cargo test`. +[[example]] +name = "relational_certification_probe" +test = true + [dependencies] lance-graph-contract = { path = "../lance-graph-contract" } # Read-only ontology registry (Phase 7, v4 plan). default-features = false so the diff --git a/crates/cognitive-shader-driver/examples/README.md b/crates/cognitive-shader-driver/examples/README.md index 7a0f13679..22918c340 100644 --- a/crates/cognitive-shader-driver/examples/README.md +++ b/crates/cognitive-shader-driver/examples/README.md @@ -177,6 +177,27 @@ events replay to the same edge bits. The ladder and thresholds are policy pins. cargo run -p cognitive-shader-driver --example reasoning_band_probe ``` +## relational_certification_probe.rs + +D-GSO-7a (P7a). Replaces the meaning of the band rungs from `reasoning_band_probe` +(#1360, which stays as shipped). Under a reading declared per class, bits 61..63 +hold the strongest relational statement the sealed model may assert: +`0 Open, 1 Associated, 2 Related, 3 Contributes, 4 CausalCandidate, 5 Causes`; +6 and 7 are reserved and refuse. Each contract is an integer fold over unit +masks and a `SupportLedger`: association needs two distinct sources, the +robustness mask can only refute, `Contributes` is a stable effect in every +declared stratum, and `Causes` needs two distinct `InterventionBacked` sources +plus executed randomized arms. No observational effect reaches `Causes`, the +inference mantissa does not move the band, and the historical `Meta` / +`Transcendent` codes do not satisfy `Causes`. An exhaustive family of 2,500 +small models shows the chain is monotone when association is scoped to the +declared populations, and not when it is marginal (Simpson). Names and +thresholds are policy pins. + +```bash +cargo run -p cognitive-shader-driver --example relational_certification_probe +``` + ## ewa_anisotropic_probe.rs D-CTX-3. Anisotropic EWA: the footprint is each virtual surfel's normalised diff --git a/crates/cognitive-shader-driver/examples/relational_certification_probe.rs b/crates/cognitive-shader-driver/examples/relational_certification_probe.rs new file mode 100644 index 000000000..4a3ac3753 --- /dev/null +++ b/crates/cognitive-shader-driver/examples/relational_certification_probe.rs @@ -0,0 +1,1029 @@ +//! D-GSO-7a (P7a): the reasoning band as a relational certification. +//! +//! Supersedes the semantics of D-GSO-7 (`reasoning_band_probe.rs`, #1360) +//! without editing it. #1360 stays as shipped: a probe of how a band is earned +//! and lowered. What this probe replaces is the meaning of the rungs. +//! +//! # The claim under test +//! +//! Bits 61..63 hold the strongest relational statement the sealed model is +//! allowed to assert. They do not hold confidence, effect size, the reasoning +//! operation, or how much work the path took. Under one declared reading the +//! raw codes are: +//! +//! | code | contract | obligation (all integer folds over unit masks) | +//! |---|---|---| +//! | 0 | `Open` | none | +//! | 1 | `Associated` | A raises Y in some declared population, ≥ 2 distinct sources | +//! | 2 | `Related` | the association holds in a declared population **and** after the robustness mask | +//! | 3 | `Contributes` | in **every** declared stratum A does not lower Y, before and after the robustness mask, and raises it in at least one | +//! | 4 | `CausalCandidate` | `Contributes`, and exposure precedes outcome on every co-occurring unit | +//! | 5 | `Causes` | ≥ 2 distinct `InterventionBacked` sources **and** the executed randomized arms show the treated rate higher | +//! | 6, 7 | reserved | refuse | +//! +//! The names are working names. The obligations are the content, and the +//! thresholds (2 sources, the rate comparison) are policy pins. +//! +//! # What was measured, not assumed +//! +//! - **Ordinal comparison is legal on codes 0..=5 only.** `entails` is an +//! explicit table; a test proves it equals `code >= code` on the six +//! contracts. Codes 6 and 7 are not contracts, so they satisfy nothing. +//! - **The chain is monotone only with scoped association.** If `Associated` +//! means the marginal association, an exhaustive family of small models finds +//! relations that satisfy `Contributes` but not `Associated` (Simpson's +//! reversal). Measured counts are printed by `main`. With `Associated` +//! existential over the declared populations (the universe plus the declared +//! strata, fixed before the data are read), the family has no violation. +//! - **`Causes` entails the lower contracts in the population that certified +//! it**: the randomized arms. It does not entail them in the observational +//! population, and a confounded observational population does not demote an +//! intervention-certified relation (#1360's confounding cap would). +//! - **Sibling specificity is not a rung.** A and its sibling can both cause Y +//! equally; comparing A against siblings then fails while `Causes` holds. So +//! "discriminative against siblings" cannot sit below `Causes` in a chain; it +//! is a statistic beside the band. +//! - **Removal is not the causal path.** Under overdetermination (Y = A or B) +//! removing A from a unit with B leaves Y unchanged, while the population +//! trial still certifies `Causes`. +//! +//! # Reused, unchanged +//! +//! `CausalEdge64` bits 61..63 via `with_reasoning_band` / `reasoning_band`, +//! read through `band_reading::BandDeclarations::project_band`; the +//! `ReasoningBand` enum is used only as the 3-bit carrier, its historical names +//! carry no meaning here. Provenance is `causal_audit::SupportLedger` / +//! `SupportReceipt` / `SupportBasis` / `EvidenceSourceId`. Seals are +//! `scheduler::DatasetVersion`. +//! +//! # Not decided here +//! +//! - Whether the reading becomes a `band_reading` lens. Here the reading is +//! probe-local and keyed by class: a class declared under the historical +//! reading refuses, even for the same bits. +//! - `CausalCandidate`'s obligations beyond ordering. They are deliberately +//! thin until real data exist. +//! - The robustness mask's source. It is an input (in practice an anomaly +//! detector such as ndarray's CLAM/CHAODA). It can only refute: a mask can +//! never create an association that the full population lacks. +//! - No stored rows are written. +//! +//! Run: `cargo run -p cognitive-shader-driver --example relational_certification_probe` +//! Tests: `cargo test -p cognitive-shader-driver --example relational_certification_probe` + +use causal_edge::edge::CausalEdge64; +use causal_edge::layout::ReasoningBand; +use lance_graph_contract::band_reading::{ + BandDeclarations, BandPresence, BandReadError, BandReading, EdgeProvenance, +}; +use lance_graph_contract::causal_audit::{ + EvidenceSourceId, SupportBasis, SupportLedger, SupportReceipt, +}; +use lance_graph_contract::class_view::ClassId; +use lance_graph_contract::rail_geometry::RailAxis; +use lance_graph_contract::scheduler::DatasetVersion; + +// ── The declared reading ────────────────────────────────────────────────── + +/// A class whose edges carry the certification reading. +const CERT_CLASS: ClassId = 0x0902; +/// A class that declares a band under the historical reading. +const LEGACY_CLASS: ClassId = 0x0901; +const RAIL: RailAxis = RailAxis::Taxonomy; +/// Classes declared under the certification reading. The bits cannot say which +/// reading wrote them, so the class does. +const CERTIFICATION_CLASSES: &[ClassId] = &[CERT_CLASS]; + +/// The certified relational contract. Working names; the obligations in the +/// module table are the content. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Contract { + Open, + Associated, + Related, + Contributes, + CausalCandidate, + Causes, +} + +impl Contract { + const ALL: [Contract; 6] = [ + Contract::Open, + Contract::Associated, + Contract::Related, + Contract::Contributes, + Contract::CausalCandidate, + Contract::Causes, + ]; + + const fn code(self) -> u8 { + match self { + Contract::Open => 0, + Contract::Associated => 1, + Contract::Related => 2, + Contract::Contributes => 3, + Contract::CausalCandidate => 4, + Contract::Causes => 5, + } + } + + fn from_code(raw: u8) -> Result { + Ok(match raw { + 0 => Contract::Open, + 1 => Contract::Associated, + 2 => Contract::Related, + 3 => Contract::Contributes, + 4 => Contract::CausalCandidate, + 5 => Contract::Causes, + other => return Err(Refusal::Reserved(other)), + }) + } + + /// Does holding `self` license asserting `required`? An explicit table, + /// never a comparison of codes. + const fn entails(self, required: Contract) -> bool { + use Contract::*; + matches!( + (self, required), + (_, Open) + | (Associated, Associated) + | (Related, Associated | Related) + | (Contributes, Associated | Related | Contributes) + | ( + CausalCandidate, + Associated | Related | Contributes | CausalCandidate + ) + | (Causes, _) + ) + } +} + +/// Why a band could not be read. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Refusal { + /// The class is not declared under the certification reading. + NotCertificationClass, + /// A reserved code (6 or 7). + Reserved(u8), + /// The contract refused (undeclared, band absent, untrusted provenance). + Band(BandReadError), +} + +fn declarations() -> BandDeclarations { + let mut d = BandDeclarations::new(); + for class in [CERT_CLASS, LEGACY_CLASS] { + d.declare( + class, + RAIL, + BandReading { + band: BandPresence::Present, + ..BandReading::ZERO_FALLBACK + }, + ); + } + d +} + +/// Read the certified contract off an edge. +fn read( + decl: &BandDeclarations, + class: ClassId, + edge: CausalEdge64, + provenance: EdgeProvenance, +) -> Result { + if !CERTIFICATION_CLASSES.contains(&class) { + return Err(Refusal::NotCertificationClass); + } + let raw = decl + .project_band(class, RAIL, edge.reasoning_band().to_bits_3(), provenance) + .map_err(Refusal::Band)?; + Contract::from_code(raw) +} + +/// Does the band on the edge license `required`? Reserved codes refuse. +fn satisfies( + decl: &BandDeclarations, + class: ClassId, + edge: CausalEdge64, + required: Contract, +) -> Result { + Ok(read(decl, class, edge, EdgeProvenance::V2Stamped)?.entails(required)) +} + +/// Write a contract into bits 61..63. Only those bits move. +fn stamp(edge: CausalEdge64, contract: Contract) -> CausalEdge64 { + edge.with_reasoning_band(ReasoningBand::from_bits_3(contract.code())) +} + +// ── The sealed model and its satisfaction folds ─────────────────────────── + +/// Why a proposition could not be decided in the model. Not a third truth +/// value: the model lacks what the decision needs. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum NotGrounded { + EmptyArm, + TooFewSources, + NoIdentificationDesign, + NoDeclaredStratum, +} + +/// Satisfied (`Ok(true)`), refuted (`Ok(false)`), or not grounded. +type Sat = Result; + +const OBSERVATION: &[SupportBasis] = &[SupportBasis::DirectlyObserved, SupportBasis::TextAttested]; +const INTERVENTION: &[SupportBasis] = &[SupportBasis::InterventionBacked]; +/// Distinct sources a contract needs. Policy pin. +const MIN_SOURCES: usize = 2; + +/// A satisfaction fold over a sealed model. +type Evaluator = fn(&Model) -> Sat; + +/// One sealed model: unit masks over at most 64 units. +#[derive(Debug, Clone)] +struct Model { + seal: DatasetVersion, + universe: u64, + exposed: u64, + outcome: u64, + /// The declared comparison partition, fixed before the data are read. + strata: [u64; 4], + /// Units whose exposure precedes their outcome. + ordered: u64, + /// Units the robustness mask keeps. + clean: u64, + /// Randomized identification design. + trial: u64, + assigned: u64, + ledger: SupportLedger, + /// Which bases count as this model's evidence for the association + /// contracts. + bases: &'static [SupportBasis], +} + +fn count(m: u64) -> u64 { + u64::from(m.count_ones()) +} + +/// rate(Y | a) compared with rate(Y | b) by cross-multiplication. +fn compare(outcome: u64, a: u64, b: u64, strict: bool) -> Sat { + let (na, nb) = (count(a), count(b)); + if na == 0 || nb == 0 { + return Err(NotGrounded::EmptyArm); + } + let (lhs, rhs) = (count(outcome & a) * nb, count(outcome & b) * na); + Ok(if strict { lhs > rhs } else { lhs >= rhs }) +} + +/// Distinct sources among `bases`, counting only receipts recorded at or +/// before `seal`: a sealed model is certified from the evidence it held, so a +/// later receipt cannot change what an earlier seal replays to. +fn distinct_sources(ledger: &SupportLedger, bases: &[SupportBasis], seal: DatasetVersion) -> usize { + let mut seen: Vec = Vec::new(); + for r in ledger + .receipts() + .iter() + .filter(|r| r.at <= seal && bases.contains(&r.basis)) + { + if !seen.contains(&r.source) { + seen.push(r.source); + } + } + seen.len() +} + +/// Existential fold: satisfied if any grounded case is, refuted if every +/// grounded case is, not grounded if none is. +fn any(results: impl Iterator) -> Sat { + let mut grounded = false; + let mut first_err = NotGrounded::EmptyArm; + for r in results { + match r { + Ok(true) => return Ok(true), + Ok(false) => grounded = true, + Err(e) => first_err = e, + } + } + if grounded { + Ok(false) + } else { + Err(first_err) + } +} + +impl Model { + fn sourced(&self) -> Result<(), NotGrounded> { + if distinct_sources(&self.ledger, self.bases, self.seal) >= MIN_SOURCES { + Ok(()) + } else { + Err(NotGrounded::TooFewSources) + } + } + + fn assoc_in(&self, p: u64) -> Sat { + compare(self.outcome, p & self.exposed, p & !self.exposed, true) + } + + fn declared(&self) -> impl Iterator + '_ { + core::iter::once(self.universe).chain( + self.strata + .iter() + .filter(|s| **s != 0) + .map(move |s| s & self.universe), + ) + } + + fn associated(&self) -> Sat { + self.sourced()?; + any(self.declared().map(|p| self.assoc_in(p))) + } + + /// The marginal variant, kept to measure where the chain breaks. + fn associated_marginal(&self) -> Sat { + self.sourced()?; + self.assoc_in(self.universe) + } + + /// The robustness mask can only refute: the association must hold in the + /// full population and after the mask. + fn related(&self) -> Sat { + self.sourced()?; + any(self.declared().map(|p| { + let full = self.assoc_in(p)?; + let kept = self.assoc_in(p & self.clean)?; + Ok(full && kept) + })) + } + + fn contributes(&self) -> Sat { + self.sourced()?; + let mut strict = false; + let mut any_stratum = false; + for s in self.strata.iter().filter(|s| **s != 0) { + any_stratum = true; + let s = s & self.universe; + let (a, b) = (s & self.exposed, s & !self.exposed); + let (ka, kb) = (a & self.clean, b & self.clean); + if !compare(self.outcome, a, b, false)? || !compare(self.outcome, ka, kb, false)? { + return Ok(false); + } + strict |= compare(self.outcome, a, b, true)? && compare(self.outcome, ka, kb, true)?; + } + if !any_stratum { + return Err(NotGrounded::NoDeclaredStratum); + } + Ok(strict) + } + + fn causal_candidate(&self) -> Sat { + if !self.contributes()? { + return Ok(false); + } + let co = self.universe & self.exposed & self.outcome; + Ok(co & !self.ordered == 0) + } + + fn causes(&self) -> Sat { + match distinct_sources(&self.ledger, INTERVENTION, self.seal) { + 0 => return Err(NotGrounded::NoIdentificationDesign), + n if n < MIN_SOURCES => return Err(NotGrounded::TooFewSources), + _ => {} + } + compare( + self.outcome, + self.trial & self.assigned, + self.trial & !self.assigned, + true, + ) + } + + /// The randomized arms read as a population of their own. + fn trial_view(&self) -> Model { + Model { + universe: self.trial, + exposed: self.assigned, + strata: [self.trial, 0, 0, 0], + ordered: self.trial, + bases: INTERVENTION, + ..self.clone() + } + } + + /// The strongest contract the model satisfies. + fn certify(&self) -> Contract { + if self.causes() == Ok(true) { + return Contract::Causes; + } + let rungs: [(Contract, Evaluator); 4] = [ + (Contract::CausalCandidate, Model::causal_candidate), + (Contract::Contributes, Model::contributes), + (Contract::Related, Model::related), + (Contract::Associated, Model::associated), + ]; + rungs + .iter() + .find(|(_, f)| f(self) == Ok(true)) + .map_or(Contract::Open, |(c, _)| *c) + } +} + +// ── Fixture builder ─────────────────────────────────────────────────────── + +struct Builder { + next: u32, + m: Model, +} + +impl Builder { + fn new() -> Self { + Builder { + next: 0, + m: Model { + seal: DatasetVersion(1), + universe: 0, + exposed: 0, + outcome: 0, + strata: [0; 4], + ordered: 0, + clean: u64::MAX, + trial: 0, + assigned: 0, + ledger: SupportLedger::new(), + bases: OBSERVATION, + }, + } + } + + fn units(&mut self, n: u32, hits: u32) -> (u64, u64) { + assert!(hits <= n && self.next + n <= 64, "fixture exceeds 64 units"); + let mut all = 0; + let mut hit = 0; + for i in 0..n { + let bit = 1u64 << (self.next + i); + all |= bit; + if i < hits { + hit |= bit; + } + } + self.next += n; + self.m.outcome |= hit; + (all, hit) + } + + /// Observational cell: `n` units in `stratum`, `hits` with the outcome. + fn cell(&mut self, stratum: usize, exposed: bool, n: u32, hits: u32) -> (u64, u64) { + let (all, hit) = self.units(n, hits); + self.m.universe |= all; + self.m.strata[stratum] |= all; + self.m.ordered |= all; + if exposed { + self.m.exposed |= all; + } + (all, hit) + } + + fn arm(&mut self, assigned: bool, n: u32, hits: u32) -> (u64, u64) { + let (all, hit) = self.units(n, hits); + self.m.trial |= all; + if assigned { + self.m.assigned |= all; + } + (all, hit) + } + + fn sources(&mut self, basis: SupportBasis, ids: &[u64]) -> &mut Self { + let at = self.m.seal; + self.sources_at(basis, ids, at) + } + + fn sources_at(&mut self, basis: SupportBasis, ids: &[u64], at: DatasetVersion) -> &mut Self { + for id in ids { + self.m.ledger.record(SupportReceipt { + basis, + source: EvidenceSourceId(*id), + at, + strength: 128, + }); + } + self + } + + fn build(&self) -> Model { + self.m.clone() + } +} + +/// A robust single-stratum association: 4/5 exposed vs 1/5 unexposed. +fn robust_association() -> Builder { + let mut b = Builder::new(); + b.cell(0, true, 5, 4); + b.cell(0, false, 5, 1); + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + b +} + +/// Within each stratum A raises Y; pooled, A lowers it (Simpson). +fn simpson_population() -> Builder { + let mut b = Builder::new(); + // stratum 0: mostly exposed, low base rate + b.cell(0, true, 8, 2); // 0.25 + b.cell(0, false, 2, 0); // 0.00 + // stratum 1: mostly unexposed, high base rate + b.cell(1, true, 2, 2); // 1.00 + b.cell(1, false, 8, 6); // 0.75 + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + b +} + +/// A positive randomized trial with two independent intervention sources. +fn add_positive_trial(b: &mut Builder) { + b.arm(true, 6, 5); + b.arm(false, 6, 1); + b.sources(SupportBasis::InterventionBacked, &[10, 11]); +} + +fn main() { + let decl = declarations(); + let mut with_trial = robust_association(); + add_positive_trial(&mut with_trial); + let mut simpson_trial = simpson_population(); + add_positive_trial(&mut simpson_trial); + let fixtures: [(&str, Model); 4] = [ + ( + "robust association, observational", + robust_association().build(), + ), + ( + "Simpson population, observational", + simpson_population().build(), + ), + ("robust association + randomized trial", with_trial.build()), + ( + "Simpson population + randomized trial", + simpson_trial.build(), + ), + ]; + println!("relational certification over bits 61..63 (declared reading)"); + let codebook: Vec = Contract::ALL + .iter() + .map(|c| format!("{}={c:?}", c.code())) + .collect(); + println!(" codebook: {} (6, 7 reserved)", codebook.join(", ")); + for (name, m) in &fixtures { + let c = m.certify(); + let edge = stamp(CausalEdge64::ZERO, c); + let back = read(&decl, CERT_CLASS, edge, EdgeProvenance::V2Stamped); + println!( + " {name:<40} -> {c:?} (code {}, marginal association {:?}, read back {back:?})", + c.code(), + m.associated_marginal() + ); + } + let t = fixtures[3].1.trial_view(); + println!( + " Simpson + trial, read in the trial population: associated {:?}, contributes {:?}", + t.associated(), + t.contributes() + ); + let meta = CausalEdge64::ZERO.with_reasoning_band(ReasoningBand::Meta); + println!( + " historical Meta bits asked to satisfy Causes: {:?}", + satisfies(&decl, CERT_CLASS, meta, Contract::Causes) + ); + let census = monotonicity_census(); + println!( + "monotonicity over {} models: scoped violations {}, marginal violations {} (Contributes without marginal association); certified per code {:?}", + census.models, census.scoped_violations, census.marginal_violations, census.reached + ); +} + +/// Exhaustive family: two strata, two cells each, n ∈ {1, 2}, every hit count, +/// two robustness masks (keep all, drop the first exposed outcome unit) and two +/// orderings (all ordered, that unit's outcome not preceded by exposure). +struct Census { + models: usize, + scoped_violations: usize, + marginal_violations: usize, + /// How many models certify each code. + reached: [usize; 6], +} + +fn monotonicity_census() -> Census { + let options: Vec<(u32, u32)> = (1..=2u32) + .flat_map(|n| (0..=n).map(move |h| (n, h))) + .collect(); + let mut c = Census { + models: 0, + scoped_violations: 0, + marginal_violations: 0, + reached: [0; 6], + }; + for &a0 in &options { + for &b0 in &options { + for &a1 in &options { + for &b1 in &options { + for (drop, unordered) in + [(false, false), (true, false), (false, true), (true, true)] + { + let mut b = Builder::new(); + let (_, hit) = b.cell(0, true, a0.0, a0.1); + b.cell(0, false, b0.0, b0.1); + b.cell(1, true, a1.0, a1.1); + b.cell(1, false, b1.0, b1.1); + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + if drop && hit != 0 { + b.m.clean &= !(hit.isolate_lowest_one()); + } + if unordered && hit != 0 { + b.m.ordered &= !(hit.isolate_lowest_one()); + } + let m = b.build(); + c.models += 1; + c.reached[m.certify().code() as usize] += 1; + let holds = |s: Sat| s == Ok(true); + let (cc, co, re, asc) = ( + holds(m.causal_candidate()), + holds(m.contributes()), + holds(m.related()), + holds(m.associated()), + ); + if (cc && !co) || (co && !re) || (re && !asc) { + c.scoped_violations += 1; + } + if co && !holds(m.associated_marginal()) { + c.marginal_violations += 1; + } + } + } + } + } + } + c +} + +#[cfg(test)] +mod tests { + use super::*; + use causal_edge::layout::SPARE_MASK; + + /// P7a.1 + P7a.8: the reading is declared per class; reserved codes and + /// historically-declared classes refuse; the bits alone decide nothing. + #[test] + fn the_reading_is_declared_and_reserved_codes_refuse() { + let decl = declarations(); + for c in Contract::ALL { + let edge = stamp(CausalEdge64::ZERO, c); + assert_eq!( + read(&decl, CERT_CLASS, edge, EdgeProvenance::V2Stamped), + Ok(c) + ); + // Same bits, historical reading: refused. + assert_eq!( + read(&decl, LEGACY_CLASS, edge, EdgeProvenance::V2Stamped), + Err(Refusal::NotCertificationClass) + ); + } + for raw in [6u8, 7] { + let edge = CausalEdge64::ZERO.with_reasoning_band(ReasoningBand::from_bits_3(raw)); + assert_eq!( + read(&decl, CERT_CLASS, edge, EdgeProvenance::V2Stamped), + Err(Refusal::Reserved(raw)) + ); + } + let edge = stamp(CausalEdge64::ZERO, Contract::Causes); + assert!(matches!( + read(&decl, CERT_CLASS, edge, EdgeProvenance::Unknown), + Err(Refusal::Band(_)) + )); + } + + /// The `>=` reading is legal on the six contracts and only there. The old + /// `Meta` (6) and `Transcendent` (7) codes are numerically above `Causes` + /// and must not satisfy it. + #[test] + fn ordinal_order_is_legal_only_on_the_declared_prefix() { + for a in Contract::ALL { + for b in Contract::ALL { + assert_eq!(a.entails(b), a.code() >= b.code(), "{a:?} vs {b:?}"); + } + } + let decl = declarations(); + for historical in [ReasoningBand::Meta, ReasoningBand::Transcendent] { + let edge = CausalEdge64::ZERO.with_reasoning_band(historical); + assert!(historical.to_bits_3() > Contract::Causes.code()); + assert!(satisfies(&decl, CERT_CLASS, edge, Contract::Causes).is_err()); + assert!(satisfies(&decl, CERT_CLASS, edge, Contract::Open).is_err()); + } + } + + /// P7a.2: one source repeated a thousand times is one source. + #[test] + fn repetition_alone_cannot_climb() { + let mut once = Builder::new(); + once.cell(0, true, 5, 4); + once.cell(0, false, 5, 1); + let mut many = Builder::new(); + many.cell(0, true, 5, 4); + many.cell(0, false, 5, 1); + once.sources(SupportBasis::DirectlyObserved, &[7]); + for _ in 0..1000 { + many.sources(SupportBasis::DirectlyObserved, &[7]); + } + let (once, many) = (once.build(), many.build()); + assert_eq!(many.associated(), Err(NotGrounded::TooFewSources)); + assert_eq!(once.certify(), Contract::Open); + assert_eq!(many.certify(), once.certify()); + // One genuinely independent source changes it. + let mut two = Builder::new(); + two.cell(0, true, 5, 4); + two.cell(0, false, 5, 1); + two.sources(SupportBasis::DirectlyObserved, &[7, 8]); + assert!(two.build().certify().entails(Contract::Associated)); + // The same holds for identification: 1000 receipts, one lab. + let mut lab = robust_association(); + lab.arm(true, 6, 5); + lab.arm(false, 6, 1); + for _ in 0..1000 { + lab.sources(SupportBasis::InterventionBacked, &[10]); + } + assert_eq!(lab.build().causes(), Err(NotGrounded::TooFewSources)); + assert_ne!(lab.build().certify(), Contract::Causes); + } + + /// P7a.3: `Related` comes from population masks. An association carried by + /// anomalous units stops at `Associated`; one that appears only after the + /// mask is not created by it. + #[test] + fn related_comes_from_population_masking_and_masks_only_refute() { + assert!(robust_association().build().related() == Ok(true)); + + // Outlier-driven: the exposed hits are exactly the anomalous units. + let mut b = Builder::new(); + let (_, hits) = b.cell(0, true, 6, 3); + b.cell(0, false, 6, 1); + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + b.m.clean &= !hits; + let outlier = b.build(); + assert_eq!(outlier.associated(), Ok(true)); + assert_eq!(outlier.related(), Ok(false)); + assert_eq!(outlier.certify(), Contract::Associated); + + // Hidden-by-anomaly: no association until the unexposed hits are + // masked. The mask does not raise it. + let mut h = Builder::new(); + h.cell(0, true, 4, 2); + let (_, hidden) = h.cell(0, false, 4, 3); + h.sources(SupportBasis::DirectlyObserved, &[1, 2]); + h.m.clean &= !hidden; + let hidden = h.build(); + assert_eq!(hidden.assoc_in(hidden.universe & hidden.clean), Ok(true)); + assert_eq!(hidden.related(), Ok(false)); + assert_eq!(hidden.certify(), Contract::Open); + } + + /// P7a.4 + P7a.5: a stable conditional effect certifies `Contributes` / + /// `CausalCandidate`; no observational effect, however large, reaches + /// `Causes`. + #[test] + fn observational_effect_stops_below_causes() { + let mut big = Builder::new(); + big.cell(0, true, 10, 10); + big.cell(0, false, 10, 0); + big.cell(1, true, 10, 10); + big.cell(1, false, 10, 0); + big.sources(SupportBasis::DirectlyObserved, &[1, 2, 3, 4, 5]); + big.sources(SupportBasis::CrossEnvironmentInvariant, &[6, 7]); + let mut m = big.build(); + assert_eq!(m.certify(), Contract::CausalCandidate); + assert_eq!(m.causes(), Err(NotGrounded::NoIdentificationDesign)); + // Ordering violated on one co-occurring unit: Contributes, not candidate. + let co = m.exposed & m.outcome; + m.ordered &= !(co.isolate_lowest_one()); + assert_eq!(m.certify(), Contract::Contributes); + } + + /// P7a.6: `Causes` needs both attested identification and executed arms. + /// Withdrawing a source at the next seal lowers the band; nothing sticks. + #[test] + fn causes_requires_identification_and_executed_arms() { + let mut no_receipts = robust_association(); + no_receipts.arm(true, 6, 5); + no_receipts.arm(false, 6, 1); + assert_eq!( + no_receipts.build().causes(), + Err(NotGrounded::NoIdentificationDesign) + ); + + let mut no_arms = robust_association(); + no_arms.sources(SupportBasis::InterventionBacked, &[10, 11]); + assert_eq!(no_arms.build().causes(), Err(NotGrounded::EmptyArm)); + + let mut null_trial = robust_association(); + null_trial.arm(true, 6, 2); + null_trial.arm(false, 6, 2); + null_trial.sources(SupportBasis::InterventionBacked, &[10, 11]); + assert_eq!(null_trial.build().causes(), Ok(false)); + assert_eq!(null_trial.build().certify(), Contract::CausalCandidate); + + let mut full = robust_association(); + add_positive_trial(&mut full); + let sealed = full.build(); + assert_eq!(sealed.certify(), Contract::Causes); + + let mut next = sealed.clone(); + next.seal = DatasetVersion(2); + assert_eq!(next.ledger.withdraw_source(EvidenceSourceId(11)), 1); + assert_ne!(next.certify(), Contract::Causes); + } + + /// P7a.7: running a counterfactual changes nothing it was not asked to + /// write. The mantissa survives stamping, the band does not depend on it, + /// and evaluating an alternate world leaves the sealed model's + /// certification as it was. + #[test] + fn a_counterfactual_operation_does_not_move_the_band() { + let decl = declarations(); + let mut b = robust_association(); + add_positive_trial(&mut b); + let m = b.build(); + let certified = m.certify(); + for mantissa in -8i8..=7 { + let edge = CausalEdge64::ZERO.with_inference_mantissa(mantissa); + let stamped = stamp(edge, certified); + assert_eq!(stamped.inference_mantissa(), mantissa); + assert_eq!( + (stamped.0 ^ edge.0) & !SPARE_MASK, + 0, + "only bits 61..63 move" + ); + assert_eq!( + read(&decl, CERT_CLASS, stamped, EdgeProvenance::V2Stamped), + Ok(certified) + ); + } + // Alternate world do(not A): exposure removed everywhere. + let mut world = m.clone(); + world.exposed = 0; + world.assigned = 0; + assert_eq!(world.certify(), Contract::Open); + assert_eq!(m.certify(), certified); + } + + /// The five-state chain is monotone with association scoped to the declared + /// populations, and is not with the marginal reading. + #[test] + fn the_chain_is_monotone_only_under_scoped_association() { + let c = monotonicity_census(); + assert_eq!(c.models, 2500); + assert_eq!(c.scoped_violations, 0); + assert!( + c.marginal_violations > 0, + "the family must contain a Simpson case" + ); + // Not vacuous: the family reaches every observational contract, and + // no observational model reaches `Causes`. + for code in 0..5 { + assert!( + c.reached[code] > 0, + "code {code} never certified: {:?}", + c.reached + ); + } + assert_eq!(c.reached[5], 0); + } + + /// Simpson: marginal association is negative, every stratum positive. The + /// observational chain certifies `CausalCandidate` through the declared + /// strata; a trial certifies `Causes`, and the confounded observational + /// population does not demote it. `Causes` entails the lower contracts in + /// the trial population. + #[test] + fn confounding_does_not_demote_an_intervention_certified_relation() { + let obs = simpson_population().build(); + assert_eq!(obs.associated_marginal(), Ok(false)); + assert_eq!(obs.contributes(), Ok(true)); + assert_eq!(obs.certify(), Contract::CausalCandidate); + + let mut b = simpson_population(); + add_positive_trial(&mut b); + let m = b.build(); + assert_eq!(m.certify(), Contract::Causes); + let t = m.trial_view(); + for (rung, sat) in [ + (Contract::Associated, t.associated()), + (Contract::Related, t.related()), + (Contract::Contributes, t.contributes()), + (Contract::CausalCandidate, t.causal_candidate()), + ] { + assert_eq!( + sat, + Ok(true), + "{rung:?} must hold in the certifying population" + ); + } + } + + /// Overdetermination: Y = A or B. Removing A from a unit with B leaves Y, + /// yet the randomized population certifies `Causes`. Necessity is not the + /// causal test. + #[test] + fn overdetermination_removal_says_dispensable_population_says_causes() { + let mut b = Builder::new(); + let (a_and_b, _) = b.arm(true, 3, 3); // A and B -> Y + b.arm(true, 3, 3); // A only -> Y + let (b_only, _) = b.arm(false, 3, 3); // B only -> Y + b.arm(false, 3, 0); // neither -> no Y + b.sources(SupportBasis::InterventionBacked, &[10, 11]); + let with_b = a_and_b | b_only; + let m = b.build(); + // Removal diagnostic on one unit with A and B: Y = A or B still holds. + let unit = a_and_b.isolate_lowest_one(); + assert_ne!( + unit & with_b, + 0, + "removing A leaves Y: A is dispensable here" + ); + assert_eq!(m.causes(), Ok(true)); + assert_eq!(m.certify(), Contract::Causes); + } + + /// Specificity against siblings is orthogonal to `Causes`: A and its + /// sibling are equally effective, so A is not discriminative against the + /// sibling population while `Causes` holds. It cannot be a rung below. + #[test] + fn sibling_specificity_is_not_a_rung() { + let mut b = robust_association(); + let (a_arm, _) = b.arm(true, 6, 5); + let (sib_arm, _) = b.arm(false, 6, 5); // the sibling treatment + b.arm(false, 6, 1); // untreated control + b.sources(SupportBasis::InterventionBacked, &[10, 11]); + let mut m = b.build(); + m.trial &= !sib_arm; // the identification design compares A with untreated + assert_eq!(m.certify(), Contract::Causes); + assert_eq!(compare(m.outcome, a_arm, sib_arm, true), Ok(false)); + } + + /// Receipts recorded after the model's seal do not count: certification + /// replays from the evidence the seal held, whatever the ledger holds now. + #[test] + fn receipts_after_the_seal_do_not_count() { + let mut b = Builder::new(); + b.cell(0, true, 5, 4); + b.cell(0, false, 5, 1); + b.sources(SupportBasis::DirectlyObserved, &[1]); + b.sources_at(SupportBasis::DirectlyObserved, &[2], DatasetVersion(2)); + b.arm(true, 6, 5); + b.arm(false, 6, 1); + b.sources_at( + SupportBasis::InterventionBacked, + &[10, 11], + DatasetVersion(2), + ); + let sealed = b.build(); + assert_eq!(sealed.seal, DatasetVersion(1)); + assert_eq!(sealed.associated(), Err(NotGrounded::TooFewSources)); + assert_eq!(sealed.causes(), Err(NotGrounded::NoIdentificationDesign)); + assert_eq!(sealed.certify(), Contract::Open); + // The same ledger read at the later seal does count them. + let later = Model { + seal: DatasetVersion(2), + ..sealed.clone() + }; + assert_eq!(later.certify(), Contract::Causes); + assert_eq!( + sealed.certify(), + Contract::Open, + "replay of the earlier seal is unchanged" + ); + } + + /// The same seal certifies to the same bits on replay. + #[test] + fn replay_gives_the_same_bits() { + let decl = declarations(); + let seals = [ + robust_association().build(), + simpson_population().build(), + { + let mut b = simpson_population(); + add_positive_trial(&mut b); + b.build() + }, + ]; + let run = || -> Vec { + seals + .iter() + .map(|m| stamp(CausalEdge64::ZERO, m.certify()).0) + .collect() + }; + assert_eq!(run(), run()); + for bits in run() { + assert!(read( + &decl, + CERT_CLASS, + CausalEdge64(bits), + EdgeProvenance::V2Stamped + ) + .is_ok()); + } + } +}