From 34c431611b309ef2c5d0c5e6ec8afcf926416177 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 16:40:19 +0200 Subject: [PATCH 1/2] probe(dr-math): independently audit finite 64x64 observations and counterexamples --- .../POPULATION_EVIDENCE.md | 15 +++ crates/dr-math-binding-probe/src/lib.rs | 3 + .../dr-math-binding-probe/src/population.rs | 95 ++++++++++++++++++ .../dr-math-binding-probe/tests/population.rs | 99 +++++++++++++++++++ 4 files changed, 212 insertions(+) create mode 100644 crates/dr-math-binding-probe/POPULATION_EVIDENCE.md create mode 100644 crates/dr-math-binding-probe/src/population.rs create mode 100644 crates/dr-math-binding-probe/tests/population.rs diff --git a/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md new file mode 100644 index 000000000..27f5286cb --- /dev/null +++ b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md @@ -0,0 +1,15 @@ +# D-DRMC-2 — Population evidence is not proof of universal mathematics + +This stage adds a deliberately small independent **audit/reference** implementation for one 64×64 focus, plus scalar-per-pair differential fixtures. It has zero data storage and does not run in a hot application path. + +`Gamma` (constraints), `R` (proposed relationship), and an optional separate `validity` plane are **independently bound** via Stage 1's structural signatures and witnessed frame. All three must have the same row/column coordinate domains and the same complete supplied witness. `UNKNOWN` is not FALSE. The fixed 4096-pair focus is not the global population, and a DR bit does not encode multiplicity, confidence, observational provenance, or independent data quality. + +`universal_on_focus` merely asserts `eligible > 0 && unknown == 0 && false == 0` over *these supplied bits*. This is a **finite-focus result**, not a generalized theorem, a causal discovery, or source attestation. Caller-supplied bits and revision numbers can be fabricated. In particular, no production method may call this a `CertifiedLaw` until an independently sealed source snapshot, completeness proof, interpretation of the constraints, and independent oracle have been checked. + +Next falsifiers for an actual discovery pipeline: +1. Compare against authoritative source observation IDs and a scalar/SQL/datafrog oracle; measure distinct/bag derivations separately. +2. Add a source seal and valid coverage receipt, distinguish a selected focus from exhaustive whole-population enumeration, and revalidate any learned threshold/rule against a held-out population. +3. For candidate algebraic rewrites, check the statement under formal mathematical assumptions through an independent proof checker. egglog e-graph extraction alone cannot prove it holds in nature. +4. Preserve negative controls: empty sample, unknown observations, one contradicting member, stale revision, changed authorization, out-of-focus true member, cyclic/self-supporting derivations. + +Runtime masks/folds remain Quack/R2IL/mask-risc or the established direct resident SIMD fast path. The `observe_focus` loop is test/reference checking only and not an alternative production evaluator. diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs index b6ca5f3e6..7d9440e48 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/crates/dr-math-binding-probe/src/lib.rs @@ -149,3 +149,6 @@ pub fn bind_dr64<'a>( rows, }) } + +/// Independent 64x64 finite-population reference audit; NEVER a production evaluator. +pub mod population; diff --git a/crates/dr-math-binding-probe/src/population.rs b/crates/dr-math-binding-probe/src/population.rs new file mode 100644 index 000000000..02e009500 --- /dev/null +++ b/crates/dr-math-binding-probe/src/population.rs @@ -0,0 +1,95 @@ +//! D-DRMC-2: deliberately small, independent FINITE POPULATION audit oracle. +//! +//! NOT a physical runtime executor, graph engine, statistical test, proof of +//! causality, or independent authentication of supplied source data. Reads +//! one 64x64 QR focus to find concrete counterexamples before a law is admitted. +//! Hot production folds remain existing Quack/R2IL/mask-risc/native SIMD. +use crate::{BindingWitness, BoundDr64}; + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct PopulationReport { + /// Pairs selected by Gamma within this concrete 64x64 focus. + pub eligible: u32, + /// Eligible positions with an observed TRUE/valid relationship. + pub true_pairs: u32, + /// Eligible positions observed FALSE (counterexamples). + pub false_pairs: u32, + /// Eligible positions without a known TRUE/FALSE observation. + pub unknown_pairs: u32, +} + +impl PopulationReport { + pub const fn checked(self) -> u32 { + self.true_pairs + self.false_pairs + } + /// Finite-focus only: no statement about unobserved people or any theorem + /// over every possible population. + pub fn universal_on_focus(self) -> Result { + if self.eligible == 0 { + return Err(ClaimRefusal::Vacuous); + } + if self.unknown_pairs != 0 { + return Err(ClaimRefusal::Unknown(self.unknown_pairs)); + } + if self.false_pairs != 0 { + return Err(ClaimRefusal::Counterexamples(self.false_pairs)); + } + Ok(self) + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ClaimRefusal { + DifferentAxes, + ChangedWitness, + Vacuous, + Unknown(u32), + Counterexamples(u32), +} + +/// Reference checker over THREE separate boolean planes: +/// 1. Gamma: which DR pairs satisfy candidate constraints; +/// 2. R: which DR pairs satisfy proposed relational law; +/// 3. validity: which R bits are known, None only for explicitly total +/// two-valued observations. UNKNOWN is never treated as FALSE. +/// +/// It compares already bound axes and full supplied witnesses. It does not +/// verify that an underlying source exists or that its relation facts are true. +/// `validity` is a separate *physical* carrier and no SQL-NULL encoding in DR. +pub fn observe_focus( + gamma: &BoundDr64<'_>, + relation: &BoundDr64<'_>, + validity: Option<&BoundDr64<'_>>, + snapshot: BindingWitness, +) -> Result { + let a = (gamma.method.row, gamma.method.column); + if a != (relation.method.row, relation.method.column) + || validity.is_some_and(|v| a != (v.method.row, v.method.column)) + { + return Err(ClaimRefusal::DifferentAxes); + } + if gamma.witness != snapshot || relation.witness != snapshot + || validity.is_some_and(|v| v.witness != snapshot) + { + return Err(ClaimRefusal::ChangedWitness); + } + let mut report = PopulationReport { + eligible: 0, true_pairs: 0, false_pairs: 0, unknown_pairs: 0, + }; + for i in 0..64 { + let focus = gamma.rows[i]; + let known = validity.map_or(u64::MAX, |v| v.rows[i]); + let positive = focus & relation.rows[i] & known; + let negative = focus & !relation.rows[i] & known; + let unknown = focus & !known; + report.eligible += focus.count_ones(); + report.true_pairs += positive.count_ones(); + report.false_pairs += negative.count_ones(); + report.unknown_pairs += unknown.count_ones(); + } + debug_assert_eq!( + report.eligible, + report.true_pairs + report.false_pairs + report.unknown_pairs + ); + Ok(report) +} diff --git a/crates/dr-math-binding-probe/tests/population.rs b/crates/dr-math-binding-probe/tests/population.rs new file mode 100644 index 000000000..9898b83b8 --- /dev/null +++ b/crates/dr-math-binding-probe/tests/population.rs @@ -0,0 +1,99 @@ +use dr_math_binding_probe::{ + bind_dr64, Axis, AxisKind, BindingWitness, BoundDr64, MethodSignature, + population::{observe_focus, ClaimRefusal, PopulationReport}, +}; + +fn w() -> BindingWitness { + BindingWitness { source_revision: 8, relation_map_revision: 1, + coordinate_revision: 2, focus_revision: 3, authorization_scope: 4 } +} +fn sig(method: u16, column: AxisKind) -> MethodSignature { + MethodSignature::presence(7, method, + Axis { class: 7, kind: AxisKind::Identity }, + Axis { class: 7, kind: column }) +} +fn bind<'a>(s: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> { + bind_dr64(s, s, w(), w(), rows).unwrap() +} +fn first_bits() -> [u64; 64] { + let mut rows = [0u64;64]; + rows[1] = (1<<2) | (1<<3) | (1<<4); + rows[5] = 1<<6; + rows +} +#[test] +fn exact_complete_focus_passes_without_causal_claim() { + let selected = first_bits(); + let g = bind(sig(1, AxisKind::Property), &selected); + let r = bind(sig(2, AxisKind::Property), &selected); + let summary = observe_focus(&g, &r, None, w()).unwrap(); + assert_eq!(summary, PopulationReport { eligible: 4, true_pairs: 4, false_pairs: 0, unknown_pairs: 0 }); + assert_eq!(summary.universal_on_focus().unwrap().checked(), 4); +} +#[test] +fn one_concrete_counterexample_refuses_claim() { + let selected = first_bits(); + let mut outcomes = selected; + outcomes[5] = 0; + let g = bind(sig(1, AxisKind::Property), &selected); + let r = bind(sig(2, AxisKind::Property), &outcomes); + assert_eq!(observe_focus(&g, &r, None, w()).unwrap().universal_on_focus(), + Err(ClaimRefusal::Counterexamples(1))); +} +#[test] +fn unknown_is_not_false_or_proof() { + let selected = first_bits(); + let mut known = selected; + known[1] &= !(1<<3); + let g = bind(sig(1, AxisKind::Property), &selected); + let r = bind(sig(2, AxisKind::Property), &selected); + let v = bind(sig(3, AxisKind::Property), &known); + let observed = observe_focus(&g, &r, Some(&v), w()).unwrap(); + assert_eq!((observed.true_pairs,observed.false_pairs,observed.unknown_pairs),(3,0,1)); + assert_eq!(observed.universal_on_focus(), Err(ClaimRefusal::Unknown(1))); +} +#[test] +fn empty_population_is_a_vacuity_not_a_law() { + let empty = [0u64;64]; + let g = bind(sig(1, AxisKind::Property), &empty); + let r = bind(sig(2, AxisKind::Property), &empty); + assert_eq!(observe_focus(&g,&r,None,w()).unwrap().universal_on_focus(), + Err(ClaimRefusal::Vacuous)); +} +#[test] +fn axes_and_snapshot_are_checked_before_reading_bits() { + let selected = first_bits(); + let g = bind(sig(1, AxisKind::Property), &selected); + let wrong = bind(sig(2, AxisKind::Identity), &selected); + assert_eq!(observe_focus(&g,&wrong,None,w()),Err(ClaimRefusal::DifferentAxes)); + let mut stale = w(); + stale.source_revision += 1; + assert_eq!(observe_focus(&g,&g,None,stale),Err(ClaimRefusal::ChangedWitness)); +} +#[test] +fn packed_bit_math_matches_independent_scalar_pair_enumeration() { + let selected = first_bits(); + let mut outcomes = selected; + outcomes[1] &= !(1<<2); + let mut known = selected; + known[1] &= !(1<<4); + let g=bind(sig(1,AxisKind::Property),&selected); + let r=bind(sig(2,AxisKind::Property),&outcomes); + let v=bind(sig(3,AxisKind::Property),&known); + let report=observe_focus(&g,&r,Some(&v),w()).unwrap(); + let mut scalar=[0u32;4]; // eligible, true, false, unknown + for (i, row) in selected.iter().enumerate() { + for j in 0..64 { + if row & (1u64< Date: Thu, 22 Oct 2026 15:17:54 +0000 Subject: [PATCH 2/2] probe(dr-math): refuted beats unknown; non-tautological population fixtures Coresearch D-DRMC items X4 and X17 (operator-chosen), on the stage 1 frame/focus/scope split. - universal_on_focus checks Counterexamples before Unknown. A refuted focus used to report Unknown(n) and hide the counterexample; under certain-answer semantics one observed FALSE refutes the claim. refuted_beats_unknown pins Gamma 0b111, R 0b001, validity 0b011 and its two twins. - The fixtures no longer bind Gamma and R to the same bits ("Gamma subset of R" was Gamma subset of Gamma). R holds pairs outside Gamma, with anti-vacuity asserts; the scalar-enumeration test now also calls universal_on_focus. - observe_focus reads validity from R, requires a two-valued Gamma, and refuses a different frame issue, a stale frame or a different focus. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../POPULATION_EVIDENCE.md | 4 +- .../dr-math-binding-probe/src/population.rs | 65 ++-- .../dr-math-binding-probe/tests/population.rs | 324 ++++++++++++++---- 3 files changed, 298 insertions(+), 95 deletions(-) diff --git a/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md index 27f5286cb..dd5e982c3 100644 --- a/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md +++ b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md @@ -2,9 +2,9 @@ This stage adds a deliberately small independent **audit/reference** implementation for one 64×64 focus, plus scalar-per-pair differential fixtures. It has zero data storage and does not run in a hot application path. -`Gamma` (constraints), `R` (proposed relationship), and an optional separate `validity` plane are **independently bound** via Stage 1's structural signatures and witnessed frame. All three must have the same row/column coordinate domains and the same complete supplied witness. `UNKNOWN` is not FALSE. The fixed 4096-pair focus is not the global population, and a DR bit does not encode multiplicity, confidence, observational provenance, or independent data quality. +`Gamma` (constraints, two-valued) and `R` (proposed relationship) are bound through Stage 1: same row/column coordinate domains, the same issue of the same store-sealed frame (still current), and the same focus. A three-valued `R` carries its own validity bits; there is no separately bound validity plane. `UNKNOWN` is not FALSE, and a counterexample is reported before any unknown pair: one observed FALSE refutes the claim whatever the unknown pairs hold. The fixed 4096-pair focus is not the global population, and a DR bit does not encode multiplicity, confidence, observational provenance, or independent data quality. -`universal_on_focus` merely asserts `eligible > 0 && unknown == 0 && false == 0` over *these supplied bits*. This is a **finite-focus result**, not a generalized theorem, a causal discovery, or source attestation. Caller-supplied bits and revision numbers can be fabricated. In particular, no production method may call this a `CertifiedLaw` until an independently sealed source snapshot, completeness proof, interpretation of the constraints, and independent oracle have been checked. +`universal_on_focus` checks, in order, `eligible > 0`, `false == 0`, `unknown == 0` over *these supplied bits*. This is a **finite-focus result**, not a generalized theorem, a causal discovery, or source attestation. Caller-supplied bits and revision numbers can be fabricated. In particular, no production method may call this a `CertifiedLaw` until an independently sealed source snapshot, completeness proof, interpretation of the constraints, and independent oracle have been checked. Next falsifiers for an actual discovery pipeline: 1. Compare against authoritative source observation IDs and a scalar/SQL/datafrog oracle; measure distinct/bag derivations separately. diff --git a/crates/dr-math-binding-probe/src/population.rs b/crates/dr-math-binding-probe/src/population.rs index 02e009500..f3cfb0240 100644 --- a/crates/dr-math-binding-probe/src/population.rs +++ b/crates/dr-math-binding-probe/src/population.rs @@ -4,7 +4,7 @@ //! causality, or independent authentication of supplied source data. Reads //! one 64x64 QR focus to find concrete counterexamples before a law is admitted. //! Hot production folds remain existing Quack/R2IL/mask-risc/native SIMD. -use crate::{BindingWitness, BoundDr64}; +use crate::{BoundDr64, FrameStore, Truth}; #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct PopulationReport { @@ -25,15 +25,18 @@ impl PopulationReport { /// Finite-focus only: no statement about unobserved people or any theorem /// over every possible population. pub fn universal_on_focus(self) -> Result { + // Refuted beats unknown (certain-answer semantics): one observed + // counterexample refutes the claim whatever the unknown pairs hold, + // so it is reported first and never hidden behind `Unknown`. if self.eligible == 0 { return Err(ClaimRefusal::Vacuous); } - if self.unknown_pairs != 0 { - return Err(ClaimRefusal::Unknown(self.unknown_pairs)); - } if self.false_pairs != 0 { return Err(ClaimRefusal::Counterexamples(self.false_pairs)); } + if self.unknown_pairs != 0 { + return Err(ClaimRefusal::Unknown(self.unknown_pairs)); + } Ok(self) } } @@ -41,44 +44,56 @@ impl PopulationReport { #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum ClaimRefusal { DifferentAxes, - ChangedWitness, + /// The selection is three-valued; Gamma selects or it does not. + SelectionNotTwoValued, + /// Gamma and R were not bound to the same issue of the same frame. + DifferentFrame, + /// The frame they share is no longer the store's current seal. + StaleFrame, + /// Gamma and R read different windows of the frame. + DifferentFocus, Vacuous, Unknown(u32), Counterexamples(u32), } -/// Reference checker over THREE separate boolean planes: -/// 1. Gamma: which DR pairs satisfy candidate constraints; -/// 2. R: which DR pairs satisfy proposed relational law; -/// 3. validity: which R bits are known, None only for explicitly total -/// two-valued observations. UNKNOWN is never treated as FALSE. +/// Reference checker over the selection Gamma and the relation R: +/// 1. Gamma: which DR pairs satisfy the candidate constraints (two-valued); +/// 2. R: which DR pairs satisfy the proposed relational law, with R's own +/// validity bits when R's method is three-valued. UNKNOWN is never FALSE. /// -/// It compares already bound axes and full supplied witnesses. It does not -/// verify that an underlying source exists or that its relation facts are true. -/// `validity` is a separate *physical* carrier and no SQL-NULL encoding in DR. +/// It compares the bound axes, that both operands share one current frame +/// issue and one focus. It does not verify that the source exists or that its +/// relation facts are true. pub fn observe_focus( + store: &FrameStore, gamma: &BoundDr64<'_>, relation: &BoundDr64<'_>, - validity: Option<&BoundDr64<'_>>, - snapshot: BindingWitness, ) -> Result { - let a = (gamma.method.row, gamma.method.column); - if a != (relation.method.row, relation.method.column) - || validity.is_some_and(|v| a != (v.method.row, v.method.column)) - { + if (gamma.method.row, gamma.method.column) != (relation.method.row, relation.method.column) { return Err(ClaimRefusal::DifferentAxes); } - if gamma.witness != snapshot || relation.witness != snapshot - || validity.is_some_and(|v| v.witness != snapshot) - { - return Err(ClaimRefusal::ChangedWitness); + if gamma.method.truth != Truth::TwoValued { + return Err(ClaimRefusal::SelectionNotTwoValued); + } + if !gamma.frame.same_issue(&relation.frame) { + return Err(ClaimRefusal::DifferentFrame); + } + if store.check(&gamma.frame).is_err() { + return Err(ClaimRefusal::StaleFrame); + } + if gamma.focus != relation.focus { + return Err(ClaimRefusal::DifferentFocus); } let mut report = PopulationReport { - eligible: 0, true_pairs: 0, false_pairs: 0, unknown_pairs: 0, + eligible: 0, + true_pairs: 0, + false_pairs: 0, + unknown_pairs: 0, }; for i in 0..64 { let focus = gamma.rows[i]; - let known = validity.map_or(u64::MAX, |v| v.rows[i]); + let known = relation.validity.map_or(u64::MAX, |v| v[i]); let positive = focus & relation.rows[i] & known; let negative = focus & !relation.rows[i] & known; let unknown = focus & !known; diff --git a/crates/dr-math-binding-probe/tests/population.rs b/crates/dr-math-binding-probe/tests/population.rs index 9898b83b8..424e6754b 100644 --- a/crates/dr-math-binding-probe/tests/population.rs +++ b/crates/dr-math-binding-probe/tests/population.rs @@ -1,99 +1,287 @@ use dr_math_binding_probe::{ - bind_dr64, Axis, AxisKind, BindingWitness, BoundDr64, MethodSignature, - population::{observe_focus, ClaimRefusal, PopulationReport}, + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Scope, Truth, bind_dr64, + population::{ClaimRefusal, PopulationReport, observe_focus}, }; -fn w() -> BindingWitness { - BindingWitness { source_revision: 8, relation_map_revision: 1, - coordinate_revision: 2, focus_revision: 3, authorization_scope: 4 } +const FOCUS: Focus = Focus { revision: 3 }; +const SCOPE: Scope = Scope { id: 4 }; + +fn store() -> FrameStore { + FrameStore::new(FrameRevisions { + source: 8, + relation_map: 1, + coordinates: 2, + }) } fn sig(method: u16, column: AxisKind) -> MethodSignature { - MethodSignature::presence(7, method, - Axis { class: 7, kind: AxisKind::Identity }, - Axis { class: 7, kind: column }) + MethodSignature::presence( + 7, + method, + Axis { + class: 7, + kind: AxisKind::Identity, + }, + Axis { + class: 7, + kind: column, + }, + ) +} +fn three_valued(mut s: MethodSignature) -> MethodSignature { + s.truth = Truth::ThreeValued; + s +} +fn bind_at<'a>( + store: &FrameStore, + focus: Focus, + s: MethodSignature, + rows: &'a [u64; 64], + validity: Option<&'a [u64; 64]>, +) -> BoundDr64<'a> { + let at = Guards { + frame: store.seal(), + focus, + scope: SCOPE, + }; + bind_dr64(store, s, s, &at, (focus, SCOPE), Operand { rows, validity }).unwrap() } -fn bind<'a>(s: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> { - bind_dr64(s, s, w(), w(), rows).unwrap() +fn bind<'a>(store: &FrameStore, s: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> { + bind_at(store, FOCUS, s, rows, None) +} +fn gamma_bits() -> [u64; 64] { + let mut rows = [0u64; 64]; + rows[1] = (1 << 2) | (1 << 3); + rows[5] = 1 << 6; + rows } -fn first_bits() -> [u64; 64] { - let mut rows = [0u64;64]; - rows[1] = (1<<2) | (1<<3) | (1<<4); - rows[5] = 1<<6; +/// R holds every Gamma pair AND pairs outside Gamma (bits 4 and 9), so a +/// checker that reads Gamma in place of R, or counts R outside the focus, +/// gives a different answer. +fn relation_bits() -> [u64; 64] { + let mut rows = [0u64; 64]; + rows[1] = (1 << 2) | (1 << 3) | (1 << 4); + rows[5] = (1 << 6) | (1 << 9); rows } + #[test] fn exact_complete_focus_passes_without_causal_claim() { - let selected = first_bits(); - let g = bind(sig(1, AxisKind::Property), &selected); - let r = bind(sig(2, AxisKind::Property), &selected); - let summary = observe_focus(&g, &r, None, w()).unwrap(); - assert_eq!(summary, PopulationReport { eligible: 4, true_pairs: 4, false_pairs: 0, unknown_pairs: 0 }); - assert_eq!(summary.universal_on_focus().unwrap().checked(), 4); + let st = store(); + let (selected, relation) = (gamma_bits(), relation_bits()); + // Anti-vacuity: Gamma and R are different bits, and R reaches outside Gamma. + assert_ne!(selected, relation); + assert!((0..64).any(|i| relation[i] & !selected[i] != 0)); + let g = bind(&st, sig(1, AxisKind::Property), &selected); + let r = bind(&st, sig(2, AxisKind::Property), &relation); + let summary = observe_focus(&st, &g, &r).unwrap(); + assert_eq!( + summary, + PopulationReport { + eligible: 3, + true_pairs: 3, + false_pairs: 0, + unknown_pairs: 0 + } + ); + assert_eq!(summary.universal_on_focus().unwrap().checked(), 3); } + #[test] fn one_concrete_counterexample_refuses_claim() { - let selected = first_bits(); - let mut outcomes = selected; - outcomes[5] = 0; - let g = bind(sig(1, AxisKind::Property), &selected); - let r = bind(sig(2, AxisKind::Property), &outcomes); - assert_eq!(observe_focus(&g, &r, None, w()).unwrap().universal_on_focus(), - Err(ClaimRefusal::Counterexamples(1))); + let st = store(); + let selected = gamma_bits(); + let mut relation = relation_bits(); + relation[5] &= !(1 << 6); + let g = bind(&st, sig(1, AxisKind::Property), &selected); + let r = bind(&st, sig(2, AxisKind::Property), &relation); + assert_eq!( + observe_focus(&st, &g, &r).unwrap().universal_on_focus(), + Err(ClaimRefusal::Counterexamples(1)) + ); } + #[test] fn unknown_is_not_false_or_proof() { - let selected = first_bits(); - let mut known = selected; - known[1] &= !(1<<3); - let g = bind(sig(1, AxisKind::Property), &selected); - let r = bind(sig(2, AxisKind::Property), &selected); - let v = bind(sig(3, AxisKind::Property), &known); - let observed = observe_focus(&g, &r, Some(&v), w()).unwrap(); - assert_eq!((observed.true_pairs,observed.false_pairs,observed.unknown_pairs),(3,0,1)); + let st = store(); + let (selected, relation) = (gamma_bits(), relation_bits()); + let mut known = [u64::MAX; 64]; + known[1] &= !(1 << 3); + let g = bind(&st, sig(1, AxisKind::Property), &selected); + let r = bind_at( + &st, + FOCUS, + three_valued(sig(2, AxisKind::Property)), + &relation, + Some(&known), + ); + let observed = observe_focus(&st, &g, &r).unwrap(); + assert_eq!( + ( + observed.true_pairs, + observed.false_pairs, + observed.unknown_pairs + ), + (2, 0, 1) + ); assert_eq!(observed.universal_on_focus(), Err(ClaimRefusal::Unknown(1))); } + +/// Certain-answer semantics: a refuted claim is refuted whatever the unknown +/// pairs hold, so `Counterexamples` must win over `Unknown`. Gamma 0b111, R +/// 0b001, validity 0b011: one true, one false, one unknown. +#[test] +fn refuted_beats_unknown() { + let st = store(); + let report = |relation: u64, validity: u64| { + let (mut g, mut r, mut v) = ([0u64; 64], [0u64; 64], [0u64; 64]); + g[0] = 0b111; + r[0] = relation; + v[0] = validity; + let gb = bind(&st, sig(1, AxisKind::Property), &g); + let rb = bind_at( + &st, + FOCUS, + three_valued(sig(2, AxisKind::Property)), + &r, + Some(&v), + ); + observe_focus(&st, &gb, &rb).unwrap() + }; + let both = report(0b001, 0b011); + assert_eq!( + (both.true_pairs, both.false_pairs, both.unknown_pairs), + (1, 1, 1) + ); + assert_eq!( + both.universal_on_focus(), + Err(ClaimRefusal::Counterexamples(1)) + ); + // Twins: unknown only, false only. + assert_eq!( + report(0b011, 0b011).universal_on_focus(), + Err(ClaimRefusal::Unknown(1)) + ); + assert_eq!( + report(0b011, 0b111).universal_on_focus(), + Err(ClaimRefusal::Counterexamples(1)) + ); +} + #[test] fn empty_population_is_a_vacuity_not_a_law() { - let empty = [0u64;64]; - let g = bind(sig(1, AxisKind::Property), &empty); - let r = bind(sig(2, AxisKind::Property), &empty); - assert_eq!(observe_focus(&g,&r,None,w()).unwrap().universal_on_focus(), - Err(ClaimRefusal::Vacuous)); + let st = store(); + let empty = [0u64; 64]; + let relation = relation_bits(); + let g = bind(&st, sig(1, AxisKind::Property), &empty); + let r = bind(&st, sig(2, AxisKind::Property), &relation); + assert_eq!( + observe_focus(&st, &g, &r).unwrap().universal_on_focus(), + Err(ClaimRefusal::Vacuous) + ); } + #[test] -fn axes_and_snapshot_are_checked_before_reading_bits() { - let selected = first_bits(); - let g = bind(sig(1, AxisKind::Property), &selected); - let wrong = bind(sig(2, AxisKind::Identity), &selected); - assert_eq!(observe_focus(&g,&wrong,None,w()),Err(ClaimRefusal::DifferentAxes)); - let mut stale = w(); - stale.source_revision += 1; - assert_eq!(observe_focus(&g,&g,None,stale),Err(ClaimRefusal::ChangedWitness)); +fn axes_frame_and_focus_are_checked_before_reading_bits() { + let mut st = store(); + let (selected, relation) = (gamma_bits(), relation_bits()); + let g = bind(&st, sig(1, AxisKind::Property), &selected); + let wrong_axis = bind(&st, sig(2, AxisKind::Identity), &relation); + assert_eq!( + observe_focus(&st, &g, &wrong_axis), + Err(ClaimRefusal::DifferentAxes) + ); + let known = [u64::MAX; 64]; + let k3_gamma = bind_at( + &st, + FOCUS, + three_valued(sig(1, AxisKind::Property)), + &selected, + Some(&known), + ); + let r = bind(&st, sig(2, AxisKind::Property), &relation); + assert_eq!( + observe_focus(&st, &k3_gamma, &r), + Err(ClaimRefusal::SelectionNotTwoValued) + ); + let other_focus = bind_at( + &st, + Focus { revision: 9 }, + sig(2, AxisKind::Property), + &relation, + None, + ); + assert_eq!( + observe_focus(&st, &g, &other_focus), + Err(ClaimRefusal::DifferentFocus) + ); + let other = store(); + let foreign = bind(&other, sig(2, AxisKind::Property), &relation); + assert_eq!( + observe_focus(&st, &g, &foreign), + Err(ClaimRefusal::DifferentFrame) + ); + st.advance(FrameRevisions { + source: 9, + relation_map: 1, + coordinates: 2, + }); + assert_eq!(observe_focus(&st, &g, &r), Err(ClaimRefusal::StaleFrame)); } + #[test] fn packed_bit_math_matches_independent_scalar_pair_enumeration() { - let selected = first_bits(); - let mut outcomes = selected; - outcomes[1] &= !(1<<2); - let mut known = selected; - known[1] &= !(1<<4); - let g=bind(sig(1,AxisKind::Property),&selected); - let r=bind(sig(2,AxisKind::Property),&outcomes); - let v=bind(sig(3,AxisKind::Property),&known); - let report=observe_focus(&g,&r,Some(&v),w()).unwrap(); - let mut scalar=[0u32;4]; // eligible, true, false, unknown + let st = store(); + let selected = gamma_bits(); + let mut relation = relation_bits(); + relation[1] &= !(1 << 2); + let mut known = [u64::MAX; 64]; + known[5] &= !(1 << 6); + let g = bind(&st, sig(1, AxisKind::Property), &selected); + let r = bind_at( + &st, + FOCUS, + three_valued(sig(2, AxisKind::Property)), + &relation, + Some(&known), + ); + let report = observe_focus(&st, &g, &r).unwrap(); + let mut scalar = [0u32; 4]; // eligible, true, false, unknown for (i, row) in selected.iter().enumerate() { for j in 0..64 { - if row & (1u64<