From 11949939338b449bda2c131cc83cb77fe7e03cd7 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:39:21 +0000 Subject: [PATCH 1/7] probe(dr-math): D-DRCA-2 DR256::WHERE x DR#3 projection with guarded reuse A three-valued global WHERE selection (Quack Draft::bind + Filter::sql_where, mask-risc Keep over 65,536 addresses) is projected into one table's 64-slot frame through the counted LocalMap, re-admitted against every guard on each read, and folded over the bound DR#3 register. The library module takes the TRUE and FALSE Keep masks as borrowed words and depends on neither engine. Twelve tests against a source-ID scalar oracle: in/out-of-frame selection, equal ordinals of two tables, YZ rotation, NULL/UNKNOWN never FALSE, source, scope/focus, FK target, reseal/coordinate, owner/codebook/criteria/schema changes, empty and full selections, the stale detached-Keep shape, and zero allocations in projection, admission and folds. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .github/workflows/dr-math-binding-probe.yml | 4 + crates/dr-math-binding-probe/Cargo.toml | 5 + crates/dr-math-binding-probe/src/hhtl16.rs | 17 + crates/dr-math-binding-probe/src/lib.rs | 5 + crates/dr-math-binding-probe/src/where_dr3.rs | 295 ++++ .../tests/dr256_where_dr3.rs | 1309 +++++++++++++++++ 6 files changed, 1635 insertions(+) create mode 100644 crates/dr-math-binding-probe/src/where_dr3.rs create mode 100644 crates/dr-math-binding-probe/tests/dr256_where_dr3.rs diff --git a/.github/workflows/dr-math-binding-probe.yml b/.github/workflows/dr-math-binding-probe.yml index b5cc18156..8d1dce0ac 100644 --- a/.github/workflows/dr-math-binding-probe.yml +++ b/.github/workflows/dr-math-binding-probe.yml @@ -8,6 +8,8 @@ on: - "crates/dr-math-binding-probe/**" - "crates/lance-graph-contract/**" - "crates/lance-graph-act-r/**" + - "crates/lance-graph-quack/**" + - "crates/lance-graph-mask-risc/**" - ".github/workflows/dr-math-binding-probe.yml" - "rust-toolchain.toml" push: @@ -16,6 +18,8 @@ on: - "crates/dr-math-binding-probe/**" - "crates/lance-graph-contract/**" - "crates/lance-graph-act-r/**" + - "crates/lance-graph-quack/**" + - "crates/lance-graph-mask-risc/**" - ".github/workflows/dr-math-binding-probe.yml" - "rust-toolchain.toml" workflow_dispatch: diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index daaa6aed8..7237dbcf1 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/crates/dr-math-binding-probe/Cargo.toml @@ -20,3 +20,8 @@ sha2 = "0.10" [dev-dependencies] lance-graph-act-r = { path = "../lance-graph-act-r" } +# D-DRCA-2 (tests/dr256_where_dr3.rs, examples/dr256_where_stages.rs): the +# real WHERE path. Quack binds and lowers, mask-risc executes the `Keep` +# terminal; the library itself never names either. +lance-graph-quack = { path = "../lance-graph-quack" } +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } diff --git a/crates/dr-math-binding-probe/src/hhtl16.rs b/crates/dr-math-binding-probe/src/hhtl16.rs index af37aef03..792811e09 100644 --- a/crates/dr-math-binding-probe/src/hhtl16.rs +++ b/crates/dr-math-binding-probe/src/hhtl16.rs @@ -128,6 +128,23 @@ impl LocalMap { pub fn lookups(&self) -> u64 { self.lookups.get() } + + /// FNV-1a over the local → global table, in local order. A frame states + /// which coordinate assignment it was sealed under by carrying this value + /// as its `coordinates` revision, so a selection projected through one + /// assignment cannot be read under another (D-DRCA-2). A digest, not an + /// identity: two maps over the same ids in the same order are the same + /// assignment. + pub fn digest(&self) -> u64 { + let mut h: u64 = 0xcbf2_9ce4_8422_2325; + for &g in &self.globals { + for b in g.to_le_bytes() { + h ^= u64::from(b); + h = h.wrapping_mul(0x0000_0100_0000_01b3); + } + } + h + } } /// The HHTL16 Cartesian address of cell `(x, y)` of a 64 × 64 register. diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs index cbd81d7bb..b1cb70372 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/crates/dr-math-binding-probe/src/lib.rs @@ -285,3 +285,8 @@ pub mod hhtl16; /// Associativity of Boolean relation composition: typing, law admission, /// egglog proof, lowering check and the first certificate. pub mod relcomp; + +/// D-DRCA-2: a global WHERE selection (65,536 addresses, three-valued) +/// projected into one table's 64-slot frame and read over DR#3, with every +/// reuse re-admitted against its guards. +pub mod where_dr3; diff --git a/crates/dr-math-binding-probe/src/where_dr3.rs b/crates/dr-math-binding-probe/src/where_dr3.rs new file mode 100644 index 000000000..af9ba92eb --- /dev/null +++ b/crates/dr-math-binding-probe/src/where_dr3.rs @@ -0,0 +1,295 @@ +//! D-DRCA-2: `DR256::WHERE` × DR#3, lab only. +//! +//! The invariant under test: +//! +//! ```text +//! global selection → optional amortized global→local mapping +//! → HHTL16 Cartesian projection → native fold +//! ``` +//! +//! # What this module does not do +//! +//! It evaluates no predicate. The global selection is the output of Quack's +//! existing WHERE (`Query { filter, agg: Agg::Rows }` → mask-risc `Keep`), +//! handed in as two borrowed 8 KiB masks: the rows where the criteria are +//! TRUE and the rows where they are FALSE (`Filter::sql_where` of the +//! criteria and of their negation). A row in neither is UNKNOWN. This +//! module has no Quack or mask-risc dependency; the tests and the stage +//! example wire the real engine to it. +//! +//! It stores nothing. A [`LocalSelection`] is a caller-owned value, the +//! projection of one selection into one frame, with the guards it was made +//! under. There is no cache, map of selections or persistent mask store. +//! +//! # The three steps +//! +//! 1. **Global → local** ([`project`]): for each local ordinal `l` of the +//! table's [`LocalMap`], test bit `global(l)` of the TRUE and FALSE masks. +//! The work is `map.len()` probes, never a pass over 65,536 rows, and a +//! selected identity outside the frame is not promoted into it. The frame +//! must carry `map.digest()` as its `coordinates` revision, so a selection +//! cannot be projected through one assignment and read under another. +//! 2. **Admission** ([`LocalSelection::admit`]): every read re-checks the +//! global source seal (owner, source revision, codebook, address space), +//! the local frame, the focus, the scope, the identity axis, the DR +//! method and the criteria. Any mismatch refuses; nothing is silently +//! reused. The only way to read is through the [`Admitted`] it returns. +//! 3. **Fold** ([`selected_count`], [`selected_column`], +//! [`selected_column_k3`], [`selected_cell`]): the selection is a `u64` +//! over the identity axis, ANDed into reads of the borrowed rows. No +//! Cartesian product is built and no row is copied. +//! +//! # Three-valued semantics +//! +//! WHERE keeps TRUE only. UNKNOWN is carried separately +//! ([`Admitted::unknown`]) and is never folded into FALSE: the complement of a +//! selection is its FALSE set, not "every slot not TRUE". +use crate::hhtl16::{self, LocalMap, MapRefusal}; +use crate::relcomp::Rows; +use crate::{Axis, BoundDr64, Focus, Frame, FrameStore, Guards, MethodSignature, Refusal, Scope}; + +/// Addresses in one DR256 global population. +pub const GLOBAL: usize = 65_536; +/// `u64` words in one global mask (8 KiB). +pub const GLOBAL_WORDS: usize = GLOBAL / 64; + +/// What the global selection was bound under, besides the source seal: the +/// identity of the criteria (a caller-supplied digest of the bound query). +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Criteria { + pub id: u64, +} + +/// Why a projection was refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ProjectRefusal { + /// A global mask that is not exactly [`GLOBAL_WORDS`] words. + WrongWidth, + /// A local slot whose global id lies outside the 65,536 addresses. + OutOfUniverse, + /// The local frame was not sealed under this map's coordinate assignment. + MapNotFrame, + /// A row that is both TRUE and FALSE: not a three-valued selection. + NotThreeValued, + /// The global source seal is not current. + Global(Refusal), + /// The local frame is not current. + Local(Refusal), +} + +/// Why a reuse was refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ReuseRefusal { + /// The global source moved: another owner (`ForeignFrame`), new data + /// (`SourceChanged`), a new codebook (`MapChanged`), a new address space + /// (`CoordinatesChanged`) or a reseal. + Global(Refusal), + /// The local frame moved, the same five ways. + Local(Refusal), + /// The register was bound under a different frame issue. + DifferentFrame, + /// The register's row axis is not the axis the selection was projected + /// onto (equal local ordinals of two tables). + AxisMismatch, + /// The register's DR method is not the one the selection was made for. + SchemaChanged, + FocusChanged, + ScopeChanged, + CriteriaChanged, +} + +/// One global selection projected into one table's frame. Caller-owned; +/// readable only through [`LocalSelection::admit`]. +#[derive(Clone, Debug)] +pub struct LocalSelection { + truth: u64, + falsity: u64, + slots: u64, + axis: Axis, + method: MethodSignature, + global: Frame, + local: Frame, + focus: Focus, + scope: Scope, + criteria: Criteria, + probes: u32, +} + +/// The selection, after every guard held. No public constructor. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Admitted { + truth: u64, + falsity: u64, + slots: u64, +} + +impl Admitted { + /// Identities where the criteria are TRUE: what WHERE keeps. + pub fn truth(&self) -> u64 { + self.truth + } + /// Identities where the criteria are FALSE. + pub fn falsity(&self) -> u64 { + self.falsity + } + /// Identities where the criteria are UNKNOWN. Never part of FALSE. + pub fn unknown(&self) -> u64 { + self.slots & !(self.truth | self.falsity) + } + /// The occupied local slots of the frame. + pub fn slots(&self) -> u64 { + self.slots + } +} + +fn bit(mask: &[u64], g: u64) -> bool { + (mask[(g >> 6) as usize] >> (g & 63)) & 1 == 1 +} + +/// What one global selection is projected under. +#[derive(Clone, Copy, Debug)] +pub struct Under<'a> { + /// The owner of the 65,536-address source, and its seal. + pub global_store: &'a FrameStore, + pub global: &'a Frame, + /// The owner of the DR frame, and the guards of the target register. + pub local_store: &'a FrameStore, + pub guards: &'a Guards, + /// The identity axis and DR method the selection is for. + pub axis: Axis, + pub method: MethodSignature, + pub criteria: Criteria, +} + +/// Project a three-valued global selection into one table's frame. +/// +/// `truth` and `falsity` are the `Keep` outputs of WHERE for the criteria and +/// for their negation. Work: `map.len()` probes into each mask. +pub fn project( + map: &LocalMap, + truth: &[u64], + falsity: &[u64], + under: Under<'_>, +) -> Result { + if truth.len() != GLOBAL_WORDS || falsity.len() != GLOBAL_WORDS { + return Err(ProjectRefusal::WrongWidth); + } + under + .global_store + .check(under.global) + .map_err(ProjectRefusal::Global)?; + under + .local_store + .check(&under.guards.frame) + .map_err(ProjectRefusal::Local)?; + if under.guards.frame.revisions().coordinates != map.digest() { + return Err(ProjectRefusal::MapNotFrame); + } + let (mut t, mut f, mut slots) = (0u64, 0u64, 0u64); + for l in 0..map.len() as u8 { + let g = map.global(l).ok_or(ProjectRefusal::OutOfUniverse)?; + if g >= GLOBAL as u64 { + return Err(ProjectRefusal::OutOfUniverse); + } + let (bt, bf) = (bit(truth, g), bit(falsity, g)); + if bt && bf { + return Err(ProjectRefusal::NotThreeValued); + } + t |= u64::from(bt) << l; + f |= u64::from(bf) << l; + slots |= 1 << l; + } + Ok(LocalSelection { + truth: t, + falsity: f, + slots, + axis: under.axis, + method: under.method, + global: under.global.clone(), + local: under.guards.frame.clone(), + focus: under.guards.focus, + scope: under.guards.scope, + criteria: under.criteria, + probes: map.len() as u32, + }) +} + +impl LocalSelection { + /// Mask probes the projection made (the global → local work). + pub fn probes(&self) -> u32 { + self.probes + } + + /// Re-check every guard against the register about to be read. + pub fn admit( + &self, + global_store: &FrameStore, + local_store: &FrameStore, + register: &BoundDr64<'_>, + criteria: Criteria, + ) -> Result { + global_store + .check(&self.global) + .map_err(ReuseRefusal::Global)?; + local_store + .check(&self.local) + .map_err(ReuseRefusal::Local)?; + if !register.frame.same_issue(&self.local) { + return Err(ReuseRefusal::DifferentFrame); + } + if register.method.row != self.axis { + return Err(ReuseRefusal::AxisMismatch); + } + if register.method != self.method { + return Err(ReuseRefusal::SchemaChanged); + } + if register.focus != self.focus { + return Err(ReuseRefusal::FocusChanged); + } + if register.scope != self.scope { + return Err(ReuseRefusal::ScopeChanged); + } + if criteria != self.criteria { + return Err(ReuseRefusal::CriteriaChanged); + } + Ok(Admitted { + truth: self.truth, + falsity: self.falsity, + slots: self.slots, + }) + } +} + +/// Identity × Property cells over the selected identities: Σ over set bits +/// `x` of `sel` of `popcount(rows[x])`. +pub fn selected_count(rows: &Rows, sel: u64) -> u32 { + let (mut s, mut n) = (sel, 0u32); + while s != 0 { + let x = s.trailing_zeros() as usize; + n += rows[x].count_ones(); + s &= s - 1; + } + n +} + +/// The selected identities holding property `y`: one column read, ANDed. +pub fn selected_column(rows: &Rows, sel: u64, y: u8) -> Option { + hhtl16::column(rows, y).map(|c| c & sel) +} + +/// Three-valued column `y` over the selected identities: (known TRUE, known +/// FALSE, UNKNOWN). A two-valued register has no UNKNOWN. +pub fn selected_column_k3(r: &BoundDr64<'_>, sel: u64, y: u8) -> Option<(u64, u64, u64)> { + let col = hhtl16::column(r.rows, y)?; + let known = match r.validity { + Some(_) => hhtl16::column_validity(r, y)?, + None => u64::MAX, + }; + Some((col & known & sel, !col & known & sel, !known & sel)) +} + +/// One cell `(x, y)`, read only if `x` is selected. +pub fn selected_cell(rows: &Rows, sel: u64, x: u8, y: u8) -> Result { + let code = hhtl16::address(x, y)?; + Ok((sel >> x) & 1 == 1 && hhtl16::cell(rows, code)?) +} diff --git a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs new file mode 100644 index 000000000..f01994131 --- /dev/null +++ b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs @@ -0,0 +1,1309 @@ +//! D-DRCA-2: `DR256::WHERE` × DR#3. +//! +//! Global selection (Quack WHERE over 65,536 addresses, mask-risc `Keep`) +//! → global→local projection through a [`LocalMap`] → HHTL16 Cartesian read +//! of a bound DR64 register → fold. +//! +//! # The oracle +//! +//! `Source` holds the rows as plain Rust values: `class: u32`, `sel: +//! Option` (`None` = NULL), `live: bool`, indexed by global address. +//! The oracle answers every question from `Source`, the fact arrays and the +//! frame's source-order id list. It shares no code with Quack, mask-risc, +//! `hhtl16` or `where_dr3`: local positions are `position()` in the id list, +//! three-valued verdicts are a `match` on `Option`. +//! +//! The engine side encodes the same `Source` into resident lanes and planes +//! (a value lane plus a validity plane per nullable column) and asks Quack. +use std::alloc::{GlobalAlloc, Layout, System}; +use std::cell::Cell; + +use dr_math_binding_probe::hhtl16::{self, LocalMap, address, cell, cell_rotated}; +use dr_math_binding_probe::relcomp::{Chain, ComposeRefusal, RelExpr, Rows}; +use dr_math_binding_probe::where_dr3::{ + self, Criteria, GLOBAL, GLOBAL_WORDS, LocalSelection, ProjectRefusal, ReuseRefusal, Under, + project, selected_cell, selected_column, selected_column_k3, selected_count, +}; +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, Frame, FrameRevisions, FrameStore, Guards, MethodSignature, + Operand, Population, Refusal, Scope, Truth, bind_dr64, +}; +use lance_graph_mask_risc::{Foreign, LaneRef, Out, Planes, Scratch, execute_into, words_for}; +use lance_graph_quack::bind::{Binder, BoundField, FieldKind, TableId, table}; +use lance_graph_quack::{Agg, Cmp, Col, Filter, Mask, Query, lower}; + +// ── allocation counter ──────────────────────────────────────────────────── + +struct Counting; +thread_local! { + static ALLOCS: Cell = const { Cell::new(0) }; +} +fn allocs() -> u64 { + ALLOCS.with(Cell::get) +} +// SAFETY: forwards to `System` unchanged; only counts calls. +unsafe impl GlobalAlloc for Counting { + unsafe fn alloc(&self, l: Layout) -> *mut u8 { + ALLOCS.with(|c| c.set(c.get() + 1)); + // SAFETY: same contract as the caller's. + unsafe { System.alloc(l) } + } + unsafe fn dealloc(&self, p: *mut u8, l: Layout) { + // SAFETY: same contract as the caller's. + unsafe { System.dealloc(p, l) } + } +} +#[global_allocator] +static GLOBAL_ALLOC: Counting = Counting; + +// ── the source, as plain values ─────────────────────────────────────────── + +const EMP: u32 = 21; +const DEPT: u32 = 22; +const OTHER: u32 = 9; +const EMP_CLASS: u16 = 21; +const DEPT_CLASS: u16 = 22; + +#[derive(Clone, Copy, Debug)] +struct Row { + class: u32, + sel: Option, + live: bool, +} + +struct Rng(u64); +impl Rng { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + fn below(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +fn source(rng: &mut Rng) -> Vec { + (0..GLOBAL) + .map(|_| { + let class = match rng.below(10) { + 0..=4 => EMP, + 5..=7 => DEPT, + _ => OTHER, + }; + let sel = (rng.below(7) != 0).then(|| rng.below(3) as i32); + Row { + class, + sel, + live: rng.below(20) != 0, + } + }) + .collect() +} + +/// The oracle's three-valued verdict of `class = 'employee' AND sel = want`. +/// `None`: not in the live population (neither TRUE nor FALSE). +fn verdict(r: &Row, want: i32) -> Option> { + if !r.live { + return None; + } + Some(if r.class != EMP { + Some(false) + } else { + r.sel.map(|v| v == want) + }) +} + +// ── the engine side: resident encoding + Quack ──────────────────────────── + +/// Planes: 0 = live, 1 = validity of `sel`, 2 = every address. Lanes: 0 = +/// class code (`U32`), 1 = `sel` (`I32`; payload at NULL rows is 1, so an +/// engine that reads NULL payloads keeps them). +struct Resident { + planes: [Vec; 3], + class: Vec, + sel: Vec, +} +const LIVE: Mask = Mask(0); +const VSEL: Mask = Mask(1); +const ALL: Mask = Mask(2); +const CLASS: Col = Col(0); +const SEL: Col = Col(1); + +fn resident(src: &[Row], codebook: &Codebook) -> Resident { + let mut planes: [Vec; 3] = std::array::from_fn(|_| vec![0u64; GLOBAL_WORDS]); + let (mut class, mut sel) = (vec![0u32; GLOBAL], vec![1i32; GLOBAL]); + for (g, r) in src.iter().enumerate() { + let set = |p: &mut Vec| p[g / 64] |= 1 << (g % 64); + if r.live { + set(&mut planes[0]); + } + if let Some(v) = r.sel { + set(&mut planes[1]); + sel[g] = v; + } + set(&mut planes[2]); + class[g] = codebook.encode(r.class); + } + Resident { planes, class, sel } +} + +/// The consumer codebook: which `U32` code the class `employee` carries. +#[derive(Clone, Copy)] +struct Codebook { + shift: u32, +} +impl Codebook { + fn encode(&self, class: u32) -> u32 { + class + self.shift + } +} +impl Binder for Codebook { + fn table(&self, name: &str) -> Option { + (name == "node").then_some(TableId(0)) + } + fn live(&self, _t: TableId) -> Mask { + LIVE + } + fn field(&self, _t: TableId, name: &str) -> Option { + match name { + "class" => Some(BoundField { + col: CLASS, + kind: FieldKind::Code, + validity: None, + }), + "sel" => Some(BoundField { + col: SEL, + kind: FieldKind::I32, + validity: Some(VSEL), + }), + _ => None, + } + } + fn code(&self, _t: TableId, _f: Col, literal: &str) -> Option { + (literal == "employee").then_some(self.encode(EMP)) + } +} + +/// `Keep` of one filter through mask-risc. +fn keep(res: &Resident, filter: Filter) -> Vec { + let q = Query { + filter, + agg: Agg::Rows, + }; + let prog = lower(&q).expect("lowers"); + let masks: Vec<&[u64]> = res.planes.iter().map(Vec::as_slice).collect(); + let lanes = [LaneRef::U32(&res.class), LaneRef::I32(&res.sel)]; + let pl = Planes { + n_rows: GLOBAL, + masks: &masks, + lanes: &lanes, + }; + let mut out = vec![0u64; words_for(GLOBAL)]; + let mut s = Scratch::for_program(&prog, GLOBAL).expect("carves"); + execute_into(&prog, &pl, &Foreign::NONE, &mut s, Out::Mask(&mut out)).expect("runs"); + out +} + +/// TRUE and FALSE masks of `class = 'employee' AND sel = want` (K3). The TRUE +/// mask comes from Quack's own `Draft::bind`; the FALSE mask from the same +/// leaves under `NOT`, both through `Filter::sql_where`. +fn where_k3(res: &Resident, cb: &Codebook, want: i32) -> (Vec, Vec) { + let bound = table("node") + .where_eq("class", "employee") + .where_eq("sel", want) + .bind(cb) + .expect("binds"); + let raw = Filter::and([ + Filter::Cmp(CLASS, Cmp::EqU32(cb.encode(EMP))), + Filter::Cmp(SEL, Cmp::EqI32(want)), + ]); + let nullable = [(SEL, VSEL)]; + let t_direct = Filter::and([Filter::plane(LIVE), raw.clone()]).sql_where(&nullable); + let f = Filter::and([Filter::plane(LIVE), Filter::negate(raw)]).sql_where(&nullable); + let t = keep(res, bound.filter); + assert_eq!( + t, + keep(res, t_direct), + "Draft::bind and the hand-built filter must agree" + ); + (t, keep(res, f)) +} + +fn bit(m: &[u64], g: u64) -> bool { + (m[(g >> 6) as usize] >> (g & 63)) & 1 == 1 +} + +// ── frames, facts and registers ─────────────────────────────────────────── + +struct World { + src: Vec, + emp_ids: Vec, + dept_ids: Vec, + skills: Vec, + sites: Vec, + has_skill: Vec<(u64, u64)>, + certified: Vec<(u64, u64, Option)>, + works_in: Vec<(u64, u64)>, + located_at: Vec<(u64, u64)>, +} + +/// 64 live employees and 64 live departments in shuffled source order, with +/// TRUE, FALSE and UNKNOWN employees all present (asserted by the tests). +fn world(seed: u64) -> World { + let mut rng = Rng(seed); + let src = source(&mut rng); + let pick = |rng: &mut Rng, class: u32| -> Vec { + let mut out = Vec::new(); + while out.len() < 64 { + let g = rng.below(GLOBAL as u64); + let r = src[g as usize]; + if r.live && r.class == class && !out.contains(&g) { + out.push(g); + } + } + out + }; + let emp_ids = pick(&mut rng, EMP); + let dept_ids = pick(&mut rng, DEPT); + let skills: Vec = (0..40).map(|i| 900_000 + i).collect(); + let sites: Vec = (0..16).map(|i| 800_000 + i).collect(); + let (mut has_skill, mut certified, mut works_in, mut located_at) = + (Vec::new(), Vec::new(), Vec::new(), Vec::new()); + for &e in &emp_ids { + for _ in 0..rng.below(5) { + let s = skills[rng.below(skills.len() as u64) as usize]; + if !has_skill.contains(&(e, s)) { + has_skill.push((e, s)); + let c = match rng.below(3) { + 0 => Some(true), + 1 => Some(false), + _ => None, + }; + certified.push((e, s, c)); + } + } + works_in.push((e, dept_ids[rng.below(64) as usize])); + } + for &d in &dept_ids { + for _ in 0..1 + rng.below(2) { + let t = sites[rng.below(16) as usize]; + if !located_at.contains(&(d, t)) { + located_at.push((d, t)); + } + } + } + World { + src, + emp_ids, + dept_ids, + skills, + sites, + has_skill, + certified, + works_in, + located_at, + } +} + +fn pos(ids: &[u64], g: u64) -> u8 { + ids.iter().position(|&x| x == g).unwrap() as u8 +} + +struct Maps { + emp: LocalMap, + dept: LocalMap, + skill: LocalMap, + site: LocalMap, +} +fn maps(w: &World) -> Maps { + Maps { + emp: LocalMap::prepare(&w.emp_ids).unwrap(), + dept: LocalMap::prepare(&w.dept_ids).unwrap(), + skill: LocalMap::prepare(&w.skills).unwrap(), + site: LocalMap::prepare(&w.sites).unwrap(), + } +} + +/// Registers are built from the oracle's positions, not through the map, so +/// a wrong map cannot make a register agree with itself. +fn plane(facts: &[(u64, u64)], rows: &[u64], cols: &[u64]) -> Rows { + let mut r = [0u64; 64]; + for &(a, b) in facts { + r[pos(rows, a) as usize] |= 1 << pos(cols, b); + } + r +} +fn certified_planes(w: &World) -> (Rows, Rows) { + let (mut val, mut known) = ([0u64; 64], [0u64; 64]); + for &(e, s, c) in &w.certified { + let (x, y) = (pos(&w.emp_ids, e), pos(&w.skills, s)); + if let Some(v) = c { + known[x as usize] |= 1 << y; + if v { + val[x as usize] |= 1 << y; + } + } + } + (val, known) +} + +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 7 }; +const CRITERIA: Criteria = Criteria { id: 0xC1 }; + +fn axis(class: u16, kind: AxisKind) -> Axis { + Axis { class, kind } +} +fn emp_id() -> Axis { + axis(EMP_CLASS, AxisKind::Identity) +} +fn sig(ord: u16, row: Axis, col: Axis) -> MethodSignature { + MethodSignature::presence(row.class, ord, row, col) +} +fn has_skill_sig() -> MethodSignature { + sig(1, emp_id(), axis(EMP_CLASS, AxisKind::Property)) +} +fn certified_sig() -> MethodSignature { + MethodSignature { + truth: Truth::ThreeValued, + ..sig(2, emp_id(), axis(EMP_CLASS, AxisKind::Property)) + } +} +fn works_in_sig() -> MethodSignature { + sig(3, emp_id(), axis(DEPT_CLASS, AxisKind::Identity)) +} +fn located_at_sig() -> MethodSignature { + sig( + 4, + axis(DEPT_CLASS, AxisKind::Identity), + axis(DEPT_CLASS, AxisKind::Property), + ) +} +fn dept_attr_sig() -> MethodSignature { + sig( + 5, + axis(DEPT_CLASS, AxisKind::Identity), + axis(DEPT_CLASS, AxisKind::Property), + ) +} + +/// The global source's owner. `relation_map` is the codebook revision. +fn global_store(cb: &Codebook) -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: u64::from(cb.shift), + coordinates: 1, + }) +} +/// The DR frame's owner, sealed under one map's coordinate assignment. +fn local_store(map: &LocalMap) -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: map.digest(), + }) +} +fn guards(st: &FrameStore, focus: Focus, scope: Scope) -> Guards { + Guards { + frame: st.seal(), + focus, + scope, + } +} +fn bind<'a>( + st: &FrameStore, + g: &Guards, + m: MethodSignature, + rows: &'a Rows, + validity: Option<&'a Rows>, +) -> BoundDr64<'a> { + bind_dr64(st, m, m, g, (g.focus, g.scope), Operand { rows, validity }).unwrap() +} + +#[allow(clippy::too_many_arguments)] +fn select( + map: &LocalMap, + t: &[u64], + f: &[u64], + gst: &FrameStore, + gseal: &Frame, + lst: &FrameStore, + g: &Guards, + axis: Axis, + method: MethodSignature, +) -> Result { + project( + map, + t, + f, + Under { + global_store: gst, + global: gseal, + local_store: lst, + guards: g, + axis, + method, + criteria: CRITERIA, + }, + ) +} + +/// The oracle's in-frame (TRUE, FALSE, UNKNOWN) words for `ids`. +fn oracle_local(src: &[Row], ids: &[u64], want: i32) -> (u64, u64, u64) { + let (mut t, mut f, mut u) = (0u64, 0u64, 0u64); + for (l, &g) in ids.iter().enumerate() { + match verdict(&src[g as usize], want) { + Some(Some(true)) => t |= 1 << l, + Some(Some(false)) => f |= 1 << l, + Some(None) => u |= 1 << l, + None => panic!("frame ids are live by construction"), + } + } + (t, f, u) +} + +const SEED: u64 = 0xD0CA_0002; +const WANT: i32 = 1; + +// ── 1. global selection inside and outside the frame ────────────────────── + +#[test] +fn global_selection_is_exact_and_only_frame_identities_are_projected() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + // Whole-mask comparison against the oracle, every one of 65,536 addresses. + let (mut gt, mut gf, mut gu) = (0u32, 0u32, 0u32); + for (g, r) in w.src.iter().enumerate() { + let g64 = g as u64; + let v = verdict(r, WANT); + assert_eq!(bit(&t, g64), v == Some(Some(true)), "TRUE at {g}"); + assert_eq!(bit(&f, g64), v == Some(Some(false)), "FALSE at {g}"); + gt += u32::from(v == Some(Some(true))); + gf += u32::from(v == Some(Some(false))); + gu += u32::from(v == Some(None)); + } + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + let (ot, of, ou) = oracle_local(&w.src, &w.emp_ids, WANT); + assert_eq!((a.truth(), a.falsity(), a.unknown()), (ot, of, ou)); + assert_eq!(a.slots(), u64::MAX); + // Anti-vacuity: all three verdicts occur in the frame, and the global + // selection reaches far beyond it. Projection work is the frame, not the + // universe. + assert!(ot != 0 && of != 0 && ou != 0, "t={ot:x} f={of:x} u={ou:x}"); + assert!(gt > 1000 && gf > 1000 && gu > 1000); + assert!(gt > ot.count_ones() * 10); + assert_eq!(sel.probes(), 64); + assert_eq!(m.emp.lookups(), 0, "projection never searches the map"); +} + +// ── 2. two tables, equal local ordinals ─────────────────────────────────── + +#[test] +fn equal_local_ordinals_of_two_tables_never_alias() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let gst = global_store(&cb); + let seal = gst.seal(); + let (lemp, ldept) = (local_store(&m.emp), local_store(&m.dept)); + let (ge, gd) = (guards(&lemp, FOCUS, SCOPE), guards(&ldept, FOCUS, SCOPE)); + let se = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lemp, + &ge, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let dept_axis = axis(DEPT_CLASS, AxisKind::Identity); + let sd = select( + &m.dept, + &t, + &f, + &gst, + &seal, + &ldept, + &gd, + dept_axis, + dept_attr_sig(), + ) + .unwrap(); + let re = plane(&w.has_skill, &w.emp_ids, &w.skills); + let rd = plane(&w.located_at, &w.dept_ids, &w.sites); + let be = bind(&lemp, &ge, has_skill_sig(), &re, None); + let bd = bind(&ldept, &gd, dept_attr_sig(), &rd, None); + let ae = se.admit(&gst, &lemp, &be, CRITERIA).unwrap(); + let ad = sd.admit(&gst, &ldept, &bd, CRITERIA).unwrap(); + // The employee selection occupies ordinals the department frame also has; + // projected through the department map it selects no department (every + // department is FALSE for `class = 'employee'`, never UNKNOWN). + assert_ne!(ae.truth() & ad.slots(), 0); + assert_eq!(ad.truth(), 0); + assert_eq!(ad.falsity(), ad.slots()); + // An employee selection cannot be read against a department-row register, + // even when that register sits in the very frame the selection was made in. + let bd_in_emp = bind(&lemp, &ge, dept_attr_sig(), &rd, None); + assert_eq!( + se.admit(&gst, &lemp, &bd_in_emp, CRITERIA), + Err(ReuseRefusal::AxisMismatch) + ); + // Nor against a register of the other frame. + assert_eq!( + se.admit(&gst, &lemp, &bd, CRITERIA), + Err(ReuseRefusal::DifferentFrame) + ); +} + +// ── 3. reads under the selection, both orientations and YZ rotation ─────── + +#[test] +fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + let selected = |e: u64| verdict(&w.src[e as usize], WANT) == Some(Some(true)); + let holds = |e: u64, s: u64| w.has_skill.contains(&(e, s)); + let (mut cells, mut selected_facts, mut rotated_hits) = (0u32, 0u32, 0u32); + for &e in &w.emp_ids { + let x = pos(&w.emp_ids, e); + for (y, &s) in w.skills.iter().enumerate() { + let y = y as u8; + let want = selected(e) && holds(e, s); + assert_eq!(selected_cell(b.rows, a.truth(), x, y).unwrap(), want); + // YZ rotation: the rotated address (y, x) reads the same fact, and + // the selection still applies to the identity coordinate. + let rot = + (a.truth() >> x) & 1 == 1 && cell_rotated(b.rows, address(y, x).unwrap()).unwrap(); + assert_eq!(rot, want, "rotated ({y}, {x})"); + rotated_hits += u32::from(rot); + cells += u32::from(want); + } + } + for (y, &s) in w.skills.iter().enumerate() { + let col = selected_column(b.rows, a.truth(), y as u8).unwrap(); + let expect = w + .emp_ids + .iter() + .filter(|&&e| selected(e) && holds(e, s)) + .fold(0u64, |acc, &e| acc | 1 << pos(&w.emp_ids, e)); + assert_eq!(col, expect, "column {s}"); + } + selected_facts += w.has_skill.iter().filter(|&&(e, _)| selected(e)).count() as u32; + assert_eq!(selected_count(b.rows, a.truth()), selected_facts); + assert_eq!(cells, selected_facts); + assert_eq!(rotated_hits, cells); + // Anti-vacuity: the selection removes facts, and keeps some. + assert!(selected_facts > 0 && (selected_facts as usize) < w.has_skill.len()); + // The fixture is not symmetric, so an identity "rotation" cannot pass. + assert!((0..64u8).any(|x| { + (0..64u8).any(|y| { + cell(&r, address(x, y).unwrap()).unwrap() != cell(&r, address(y, x).unwrap()).unwrap() + }) + })); +} + +// ── 4. NULL / UNKNOWN: never FALSE ──────────────────────────────────────── + +#[test] +fn unknown_stays_unknown_in_selection_negation_and_property() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + certified_sig(), + ) + .unwrap(); + let (val, known) = certified_planes(&w); + let b = bind(&lst, &g, certified_sig(), &val, Some(&known)); + let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + // NOT(selection) is FALSE, not "every slot not TRUE". + assert_ne!(a.unknown(), 0); + assert_eq!(a.falsity() & a.unknown(), 0); + assert_ne!(a.falsity(), a.slots() & !a.truth()); + // The NULL rows' payload is 1 = WANT, so an engine reading payloads at + // NULL would have kept them: none is TRUE. + for &e in &w.emp_ids { + if w.src[e as usize].sel.is_none() { + assert_eq!((a.truth() >> pos(&w.emp_ids, e)) & 1, 0); + } + } + // Three-valued property over the selected identities, column by column. + let (mut u_cells, mut f_cells) = (0u32, 0u32); + for (y, &s) in w.skills.iter().enumerate() { + let (ct, cf, cu) = selected_column_k3(&b, a.truth(), y as u8).unwrap(); + let (mut et, mut ef, mut eu) = (0u64, 0u64, 0u64); + for &e in &w.emp_ids { + if verdict(&w.src[e as usize], WANT) != Some(Some(true)) { + continue; + } + let bitpos = 1u64 << pos(&w.emp_ids, e); + match w.certified.iter().find(|c| c.0 == e && c.1 == s) { + Some((_, _, Some(true))) => et |= bitpos, + Some((_, _, Some(false))) => ef |= bitpos, + // No fact, or a fact with unknown certification: UNKNOWN. + _ => eu |= bitpos, + } + } + assert_eq!((ct, cf, cu), (et, ef, eu), "certified column {s}"); + u_cells += cu.count_ones(); + f_cells += cf.count_ones(); + } + assert!(u_cells > 0 && f_cells > 0); +} + +// ── 5. source change after WHERE: refuse, then rebind ───────────────────── + +#[test] +fn source_change_after_where_refuses_reuse_and_rebind_matches() { + let mut w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (mut gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + let before = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + // Flip `sel` on every selected frame employee: none is TRUE any more. + for &e in &w.emp_ids { + if verdict(&w.src[e as usize], WANT) == Some(Some(true)) { + w.src[e as usize].sel = Some(0); + } + } + gst.advance(FrameRevisions { + source: 2, + ..gst.revisions() + }); + assert_eq!( + sel.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::Global(Refusal::SourceChanged)) + ); + // Rebind: WHERE again, project again, under the new seal. + let res2 = resident(&w.src, &cb); + let (t2, f2) = where_k3(&res2, &cb, WANT); + let seal2 = gst.seal(); + let sel2 = select( + &m.emp, + &t2, + &f2, + &gst, + &seal2, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let after = sel2.admit(&gst, &lst, &b, CRITERIA).unwrap(); + assert_eq!(after.truth(), 0); + assert_eq!( + (after.truth(), after.falsity(), after.unknown()), + oracle_local(&w.src, &w.emp_ids, WANT) + ); + // The silent alternative: the old projection would still answer. + assert_ne!( + selected_count(b.rows, before.truth()), + selected_count(b.rows, after.truth()) + ); +} + +// ── 6. ACL / scope and focus with identical coordinates ─────────────────── + +#[test] +fn scope_or_focus_change_refuses_with_identical_coordinates() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + // Same frame issue, same coordinate numbers, same register bytes. + let g_scope = Guards { + scope: Scope { id: 8 }, + ..g.clone() + }; + let b_scope = bind(&lst, &g_scope, has_skill_sig(), &r, None); + assert_eq!( + sel.admit(&gst, &lst, &b_scope, CRITERIA), + Err(ReuseRefusal::ScopeChanged) + ); + let g_focus = Guards { + focus: Focus { revision: 2 }, + ..g.clone() + }; + let b_focus = bind(&lst, &g_focus, has_skill_sig(), &r, None); + assert_eq!( + sel.admit(&gst, &lst, &b_focus, CRITERIA), + Err(ReuseRefusal::FocusChanged) + ); + // Silence twin: the unchanged register admits. + let b = bind(&lst, &g, has_skill_sig(), &r, None); + assert!(sel.admit(&gst, &lst, &b, CRITERIA).is_ok()); +} + +// ── 7. witnessed FK: selected employees' sites; FK change refuses ───────── + +#[test] +fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { + let mut w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let gst = global_store(&cb); + // One frame over both tables; its coordinates name the employee map, the + // axis the selection is projected onto. + let both = FrameRevisions { + source: 1, + relation_map: 1, + coordinates: m.emp.digest(), + }; + let mut lst = FrameStore::new(both); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + works_in_sig(), + ) + .unwrap(); + let rw = plane(&w.works_in, &w.emp_ids, &w.dept_ids); + let rl = plane(&w.located_at, &w.dept_ids, &w.sites); + let bw = bind(&lst, &g, works_in_sig(), &rw, None); + let bl = bind(&lst, &g, located_at_sig(), &rl, None); + let a = sel.admit(&gst, &lst, &bw, CRITERIA).unwrap(); + let chain = Chain::new(&lst, vec![bw.clone(), bl.clone()]).unwrap(); + let (es, _) = chain + .eval(&RelExpr::comp(RelExpr::Leaf(0), RelExpr::Leaf(1))) + .unwrap(); + let selected = |e: u64| verdict(&w.src[e as usize], WANT) == Some(Some(true)); + let at_site = |w: &World, e: u64, s: u64| { + w.works_in + .iter() + .any(|&(a, d)| a == e && w.located_at.contains(&(d, s))) + }; + let mut hits = 0u32; + for &e in &w.emp_ids { + for &s in &w.sites { + let got = selected_cell(&es, a.truth(), pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); + assert_eq!(got, selected(e) && at_site(&w, e, s), "({e}, {s})"); + hits += u32::from(got); + } + } + assert!(hits > 0); + drop(chain); + // The referenced property changes: one department moves to a new site. + let (d0, _) = w.located_at[0]; + w.located_at.retain(|&(d, _)| d != d0); + w.located_at.push((d0, w.sites[15])); + lst.advance(FrameRevisions { source: 2, ..both }); + assert_eq!( + sel.admit(&gst, &lst, &bw, CRITERIA), + Err(ReuseRefusal::Local(Refusal::SourceChanged)) + ); + assert_eq!( + Chain::new(&lst, vec![bw.clone(), bl.clone()]).err(), + Some(ComposeRefusal::StaleFrame) + ); + // Rebind both registers and the selection under the new seal. + let g2 = guards(&lst, FOCUS, SCOPE); + let rl2 = plane(&w.located_at, &w.dept_ids, &w.sites); + let bw2 = bind(&lst, &g2, works_in_sig(), &rw, None); + let bl2 = bind(&lst, &g2, located_at_sig(), &rl2, None); + let sel2 = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g2, + emp_id(), + works_in_sig(), + ) + .unwrap(); + let a2 = sel2.admit(&gst, &lst, &bw2, CRITERIA).unwrap(); + let chain2 = Chain::new(&lst, vec![bw2, bl2]).unwrap(); + let (es2, _) = chain2 + .eval(&RelExpr::comp(RelExpr::Leaf(0), RelExpr::Leaf(1))) + .unwrap(); + for &e in &w.emp_ids { + for &s in &w.sites { + let got = + selected_cell(&es2, a2.truth(), pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); + assert_eq!(got, selected(e) && at_site(&w, e, s)); + } + } + let _ = m.site.len() + m.skill.len(); +} + +// ── 8. reseal and coordinate changes ────────────────────────────────────── + +#[test] +fn reseal_and_coordinate_changes_refuse() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let gst = global_store(&cb); + let seal = gst.seal(); + let mut lst = local_store(&m.emp); + let g = guards(&lst, FOCUS, SCOPE); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + let before = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + // Reseal at the same numbers. + lst.advance(lst.revisions()); + assert_eq!( + sel.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::Local(Refusal::FrameResealed)) + ); + // A new coordinate assignment: the same ids in another order. + let mut reordered = w.emp_ids.clone(); + reordered.reverse(); + let map2 = LocalMap::prepare(&reordered).unwrap(); + assert_ne!(map2.digest(), m.emp.digest()); + lst.advance(FrameRevisions { + coordinates: map2.digest(), + ..lst.revisions() + }); + assert_eq!( + sel.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::Local(Refusal::CoordinatesChanged)) + ); + // Projecting through the old map under the new frame is refused. + let g2 = guards(&lst, FOCUS, SCOPE); + assert_eq!( + select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g2, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::MapNotFrame) + ); + // Through the new map it projects, with the bits moved to the new + // ordinals. + let sel2 = select( + &map2, + &t, + &f, + &gst, + &seal, + &lst, + &g2, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r2 = plane(&w.has_skill, &reordered, &w.skills); + let b2 = bind(&lst, &g2, has_skill_sig(), &r2, None); + let a2 = sel2.admit(&gst, &lst, &b2, CRITERIA).unwrap(); + assert_eq!(a2.truth(), oracle_local(&w.src, &reordered, WANT).0); + assert_eq!( + selected_count(b2.rows, a2.truth()), + selected_count(&r, before.truth()) + ); +} + +// ── 9. owner, codebook, criteria, schema ────────────────────────────────── + +#[test] +fn foreign_owner_codebook_criteria_and_schema_refuse() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let mut gst = global_store(&cb); + let lst = local_store(&m.emp); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + // Another owner at identical numbers. + let other = global_store(&cb); + assert_eq!( + sel.admit(&other, &lst, &b, CRITERIA), + Err(ReuseRefusal::Global(Refusal::ForeignFrame)) + ); + // Other criteria. + assert_eq!( + sel.admit(&gst, &lst, &b, Criteria { id: 0xC2 }), + Err(ReuseRefusal::CriteriaChanged) + ); + // Another DR method over the same axis (DT schema moved). + let other_method = sig(9, emp_id(), axis(EMP_CLASS, AxisKind::Property)); + let b_schema = bind(&lst, &g, other_method, &r, None); + assert_eq!( + sel.admit(&gst, &lst, &b_schema, CRITERIA), + Err(ReuseRefusal::SchemaChanged) + ); + // A new codebook: `employee` is re-encoded. The old projection refuses; + // the stale binding, run silently, keeps nobody. + let cb2 = Codebook { shift: 100 }; + gst.advance(FrameRevisions { + relation_map: u64::from(cb2.shift), + ..gst.revisions() + }); + assert_eq!( + sel.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::Global(Refusal::MapChanged)) + ); + let res2 = resident(&w.src, &cb2); + let (t_stale, _) = where_k3(&res2, &cb, WANT); + let (t_fresh, f_fresh) = where_k3(&res2, &cb2, WANT); + assert_eq!(t_fresh, t); + assert!(t_stale.iter().all(|&x| x == 0)); + let seal2 = gst.seal(); + let sel2 = select( + &m.emp, + &t_fresh, + &f_fresh, + &gst, + &seal2, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + assert!(sel2.admit(&gst, &lst, &b, CRITERIA).is_ok()); +} + +// ── 10. empty and full selections ───────────────────────────────────────── + +#[test] +fn empty_and_full_global_selections_are_exact() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + // Empty: no row has sel = 99. Every frame employee is FALSE or UNKNOWN. + let (t0, f0) = where_k3(&res, &cb, 99); + assert!(t0.iter().all(|&x| x == 0)); + let s0 = select( + &m.emp, + &t0, + &f0, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let a0 = s0.admit(&gst, &lst, &b, CRITERIA).unwrap(); + assert_eq!( + (a0.truth(), a0.falsity(), a0.unknown()), + oracle_local(&w.src, &w.emp_ids, 99) + ); + assert_eq!(selected_count(b.rows, a0.truth()), 0); + // Full: the every-address plane. All 65,536 TRUE, every slot selected. + let full = keep(&res, Filter::plane(ALL)); + let none = vec![0u64; GLOBAL_WORDS]; + assert_eq!( + full.iter().map(|w| w.count_ones()).sum::(), + GLOBAL as u32 + ); + let s1 = select( + &m.emp, + &full, + &none, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let a1 = s1.admit(&gst, &lst, &b, CRITERIA).unwrap(); + assert_eq!((a1.truth(), a1.falsity(), a1.unknown()), (u64::MAX, 0, 0)); + assert_eq!( + selected_count(b.rows, a1.truth()) as usize, + w.has_skill.len() + ); + // Malformed inputs are refused, not read. + assert_eq!( + select( + &m.emp, + &full[..10], + &none, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::WrongWidth) + ); + assert_eq!( + select( + &m.emp, + &full, + &full, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::NotThreeValued) + ); + let far = LocalMap::prepare(&[GLOBAL as u64]).unwrap(); + let lfar = local_store(&far); + let gfar = guards(&lfar, FOCUS, SCOPE); + assert_eq!( + select( + &far, + &full, + &none, + &gst, + &seal, + &lfar, + &gfar, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::OutOfUniverse) + ); +} + +// ── 11. #1792's shape: a detached Keep reused after a criteria input moved ─ + +#[test] +fn stale_keep_negative_control_is_refused_not_answered() { + let mut w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + // The detached Keep: kept outside any guard, then the criteria input + // (`sel`) changes on half the selected rows of the whole universe. + let detached = t.clone(); + let mut moved = 0u32; + for (g, r) in w.src.iter_mut().enumerate() { + if bit(&t, g as u64) && g % 2 == 0 { + r.sel = Some(2); + moved += 1; + } + } + let res2 = resident(&w.src, &cb); + let (fresh, _) = where_k3(&res2, &cb, WANT); + let pop = |m: &[u64]| m.iter().map(|x| x.count_ones()).sum::(); + // Unguarded, the detached mask answers silently with the old population. + assert_eq!(pop(&detached) - pop(&fresh), moved); + assert!(moved > 100); + // Guarded: the same mask, projected under the old seal, is refused once + // the owner records the change. + let m = maps(&w); + let (mut gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let sel = select( + &m.emp, + &detached, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + gst.advance(FrameRevisions { + source: 2, + ..gst.revisions() + }); + assert_eq!( + sel.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::Global(Refusal::SourceChanged)) + ); + // Projecting the detached mask under the NEW seal is not detected: the + // seal attests the caller's claim, not the mask's provenance. Recorded + // as the open limitation, asserted so a fix flips this test. + let seal2 = gst.seal(); + assert!( + select( + &m.emp, + &detached, + &f, + &gst, + &seal2, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .is_ok() + ); +} + +// ── 12. allocation: projection, admission and folds allocate nothing ────── + +#[test] +fn projection_admission_and_folds_do_not_allocate() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (gst, lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + let before = allocs(); + let sel = select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig(), + ) + .unwrap(); + let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + let mut acc = selected_count(b.rows, a.truth()); + for y in 0..40u8 { + acc ^= selected_column(b.rows, a.truth(), y).unwrap().count_ones(); + } + assert_eq!(allocs(), before, "acc={acc}"); + let _ = hhtl16::LOCAL + where_dr3::GLOBAL; + let _ = Population::Distinct; +} From dbc6fb78543e892d646507a22842ab176378ebb8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:41:32 +0000 Subject: [PATCH 2/7] probe(dr-math): D-DRCA-2 cover the projection-time seal checks The first disable pass showed both seal checks inside project() were not load-bearing: no test projected under a stale global seal, a foreign owner's seal, or a resealed local frame. This test does, with a silence twin. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../tests/dr256_where_dr3.rs | 83 +++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs index f01994131..44f5f54bb 100644 --- a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs +++ b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs @@ -1307,3 +1307,86 @@ fn projection_admission_and_folds_do_not_allocate() { let _ = hhtl16::LOCAL + where_dr3::GLOBAL; let _ = Population::Distinct; } + +// ── 13. a projection under a stale seal is refused before any read ──────── + +#[test] +fn projection_under_a_stale_global_seal_or_local_frame_is_refused() { + let w = world(SEED); + let cb = Codebook { shift: 0 }; + let res = resident(&w.src, &cb); + let (t, f) = where_k3(&res, &cb, WANT); + let m = maps(&w); + let (mut gst, mut lst) = (global_store(&cb), local_store(&m.emp)); + let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); + // Silence twin: current seals project. + assert!( + select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .is_ok() + ); + // The global owner moved between WHERE and projection. + gst.advance(FrameRevisions { + source: 2, + ..gst.revisions() + }); + assert_eq!( + select( + &m.emp, + &t, + &f, + &gst, + &seal, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::Global(Refusal::SourceChanged)) + ); + // Another owner's seal at identical numbers. + let other = global_store(&cb); + let seal_now = gst.seal(); + assert_eq!( + select( + &m.emp, + &t, + &f, + &other, + &seal_now, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::Global(Refusal::ForeignFrame)) + ); + // The local frame moved. + lst.advance(lst.revisions()); + assert_eq!( + select( + &m.emp, + &t, + &f, + &gst, + &seal_now, + &lst, + &g, + emp_id(), + has_skill_sig() + ) + .err(), + Some(ProjectRefusal::Local(Refusal::FrameResealed)) + ); +} From e05938aada7947b58c03234e1ba92a300d7feecf Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:44:50 +0000 Subject: [PATCH 3/7] probe(dr-math): D-DRCA-2 stage costs, README section and board entry examples/dr256_where_stages.rs measures every stage separately (cold preparation, bind, lower, WHERE TRUE+FALSE Keep, projection, admission, warm read, rotated read, folds) and the reuse of one projected selection over N = 1, 2, 4, 8, 64 compatible reads against fresh evaluation and rebind-after-invalidation. Totals above 1,000 us are printed as failed gates without a ratio. Warm reuse pays from N = 2. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../2026-10-28-d-drca-2-dr256-where-dr3.md | 16 + .claude/board/entries/README.md | 3 +- crates/dr-math-binding-probe/README.md | 71 ++ .../examples/dr256_where_stages.rs | 868 ++++++++++++++++++ 4 files changed, 957 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md create mode 100644 crates/dr-math-binding-probe/examples/dr256_where_stages.rs diff --git a/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md new file mode 100644 index 000000000..7c91b0d1d --- /dev/null +++ b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md @@ -0,0 +1,16 @@ +# D-DRCA-2: DR256::WHERE × DR#3 + +**Status:** MEASURED, lab only. Code: `crates/dr-math-binding-probe/src/where_dr3.rs`, test `tests/dr256_where_dr3.rs`, costs `examples/dr256_where_stages.rs`; results in the crate README, section D-DRCA-2. Builds on D-DRCA-1 (`hhtl16`, #1834). Contract: `.claude/plans/d-drdt-dr-dt-ownership-amendment-v1.md` (#1835). + +## Result + +- A three-valued global WHERE (Quack `Draft::bind` + `Filter::sql_where`, mask-risc `Keep`, 65,536 addresses) projects into a 64-slot DR frame by `map.len()` probes through the counted `LocalMap`. No new predicate evaluator, routing engine or mask store. +- Every read is re-admitted against owner, source, codebook, frame, register frame, axis, DR method, focus, scope and criteria; each refusal is pinned by a test against an independent source-ID oracle. +- UNKNOWN stays apart from FALSE in the selection, its negation and a three-valued property column. +- Projection, admission and folds allocate nothing. Warm read 71–90 ns; fresh read 44–73 µs (WHERE dominates). Warm reuse breaks even at N = 1 and pays from N = 2 (1.96–2.03×), 8.1–8.4× at N = 8; at N = 64 fresh and rebind exceed 1,000 µs (failed gate), warm stays at 46 µs. +- Sixteen disable runs each turn a test red. The first pass found the projection-time seal checks unpinned; a test was added. +- The #1792 control still reproduces (`reused R2 1032 vs fresh 31`). + +## Open + +A detached `Keep` projected under a NEW seal is accepted: the seal attests the caller's claim, not mask provenance (needs a producer-side frame on Quack's bound query, D-NFR S5). `Criteria` is caller-supplied. The FALSE set costs a second WHERE program. One 64-slot frame per table; no DR256 resident register; no scattered-mask reuse. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 9bad0e3cd..241691706 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. -492 entries, 2026-08-06 .. 2026-10-28. +493 entries, 2026-08-06 .. 2026-10-28. | date | entry id | finding | file | |---|---|---|---| | 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-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) | +| 2026-10-28 | `D-DRCA-2` | | [2026-10-28-d-drca-2-dr256-where-dr3.md](2026-10-28-d-drca-2-dr256-where-dr3.md) | | 2026-10-28 | `D-DRCA-1` | | [2026-10-28-d-drca-1-hhtl16-dr-projection.md](2026-10-28-d-drca-1-hhtl16-dr-projection.md) | | 2026-10-27 | `harvest-integration-composite-key-and-simd-scope` | | [2026-10-27-harvest-integration-composite-key-and-simd-scope.md](2026-10-27-harvest-integration-composite-key-and-simd-scope.md) | | 2026-10-26 | `D-ONNX-INTAKE-0` | | [2026-10-26-onnx-frontend-intake-bakeoff.md](2026-10-26-onnx-frontend-intake-bakeoff.md) | diff --git a/crates/dr-math-binding-probe/README.md b/crates/dr-math-binding-probe/README.md index 3b4d3c313..1b7cd34ac 100644 --- a/crates/dr-math-binding-probe/README.md +++ b/crates/dr-math-binding-probe/README.md @@ -65,3 +65,74 @@ Disable runs, each turning its named test red and restored from the commit: iden Warm reads made 0 global→local lookups. Single host, single run; reported, not gates. **Not done:** DR256::WHERE selection over 65,536 addresses and the stay / rebind / masked-read choice; focus larger than 64; any SIMD kernel (the column read is a scalar per-row gather, the largest warm cost after the folds); a real source owner, ACL or ClassView registry; DT method semantics (DR #4 handoff, amendment plan). + +## D-DRCA-2: DR256::WHERE × DR#3 (`where_dr3`) + +Lab test of the composition `global selection → optional amortized global→local mapping → HHTL16 Cartesian projection → native fold`. Module `src/where_dr3.rs`, test `tests/dr256_where_dr3.rs`, costs `examples/dr256_where_stages.rs`. + +- **WHERE is Quack's.** `table("node").where_eq("class", "employee").where_eq("sel", 1).bind(..)` (`Draft::bind`, three-valued through `Filter::sql_where`), lowered and executed by mask-risc's `Keep` terminal over 65,536 addresses. The FALSE set is the same leaves under `NOT`, also through `sql_where`. A row in neither is UNKNOWN. The module evaluates no predicate and depends on neither engine: it takes the two `Keep` masks as borrowed words. +- **Global → local.** `project` tests bit `global(l)` of both masks for each local slot of the table's `LocalMap`: `map.len()` probes, never a pass over the universe, no map search. A selected identity outside the frame is not projected. The frame must carry `LocalMap::digest()` as its `coordinates` revision, so a selection cannot be projected through one coordinate assignment and read under another. +- **Admission.** Every read goes through `LocalSelection::admit`, which re-checks the global source seal (owner, source revision, codebook, address space), the local frame, register frame identity, identity axis, DR method, focus, scope and criteria. The only readable form is the `Admitted` it returns. A `LocalSelection` is a caller-owned value; there is no store or cache. +- **Folds.** The selection is a `u64` over the identity axis, ANDed into reads of the borrowed rows (`selected_count`, `selected_column`, `selected_column_k3`, `selected_cell`). No Cartesian product, no copied row. +- **K3.** WHERE keeps TRUE. UNKNOWN is carried separately and never folded into FALSE; the negation of a selection is its FALSE set. + +Oracle: the source is plain Rust values per global address (`class`, `sel: Option`, `live`). Verdicts are a `match` on `Option`, local positions are `position()` in the frame's source-order id list, and registers are built from those positions, not through the map. It shares no code with Quack, mask-risc, `hhtl16` or `where_dr3`. NULL rows carry the payload the predicate tests for, so an engine that read NULL payloads would keep them. + +Thirteen tests against that oracle: + +- the global selection, whole mask over all 65,536 addresses, and its in-frame TRUE / FALSE / UNKNOWN (all three non-empty; most selected identities lie outside the frame); +- equal local ordinals of two tables: the employee selection projected through the department map selects no department, and reading it against a department-row register is refused (`AxisMismatch`, `DifferentFrame`); +- selected Identity × Property cell by cell, by column and by count, and the same relationships through the YZ rotation; +- UNKNOWN: kept apart from FALSE in the selection, in its negation and in a three-valued property column; +- a source change after WHERE (refused, then rebound to the oracle); +- a scope or focus change with identical coordinates (refused; the unchanged register admits); +- selected employees' sites through a witnessed FK (`Chain`), then a changed referenced property (refused, rebound); +- a reseal at equal numbers and a new coordinate assignment (refused; the old map is refused under the new frame, and the new map projects to the new ordinals); +- a foreign owner at equal numbers, other criteria, another DR method, and a new codebook (refused; the stale binding run silently keeps nobody); +- empty and full selections, plus malformed widths, TRUE ∧ FALSE overlap and an id outside the universe; +- the #1792 shape: a detached `Keep` reused after its criteria input changed answers silently with the old population; projected under the old seal it is refused; +- projection under a stale global seal, a foreign owner's seal or a resealed local frame; +- projection, admission and folds allocate nothing. + +Disable runs, each restored from the commit and each turning at least one test red: the two projection-time seal checks, `MapNotFrame`, the TRUE ∧ FALSE check, TRUE/FALSE swapped, the eight admission guards (global, local, frame issue, axis, method, focus, scope, criteria), UNKNOWN computed as "not TRUE", the three-valued column reporting UNKNOWN as FALSE, and `selected_count` ignoring the selection. The first pass found the two projection-time seal checks covered by no test; the projection test above was added for them and both now go red. + +The original #1792 control is unchanged and still reproduces: `cargo run --release --example p2_quack_where -- --controls` in `crates/drf-focus-probe` prints `reused R2 1032 vs fresh 31`. + +`cargo run --release --example dr256_where_stages` on a 4-vCPU shared Xeon @ 2.10 GHz (avx512f), median of 21 runs, two runs. Per-op rows below are batched over 40–256 calls where a single call is below timer resolution. + +| stage | run 1 | run 2 | allocs | +|---|---|---|---| +| cold: encode 65,536 source rows into planes and lanes (fixture) | 409 µs | — | 5 | +| cold: `LocalMap::prepare` (64 ids) | 642 ns | — | 3 | +| cold: `FrameStore::new` + seal | 786 ns | — | 2 | +| `Draft::bind` | 308 ns | — | 10 | +| `lower` | 318 ns | — | 7 | +| WHERE TRUE + FALSE `Keep`, 65,536 rows (lowered once) | 42.2 µs | 70.5 µs | 0 | +| `project` (64 probes) | 1,023 ns | 1,028 ns | 0 | +| `admit` | 65.8 ns | 80.1 ns | 0 | +| warm read (`admit` + `selected_count`) | 70.7 ns | 89.9 ns | 0 | +| rotated cell read, selection applied | 10.7 ns | 9.6 ns | 0 | +| `selected_count` | 13.2 ns | 30.3 ns | 0 | +| `selected_column` | 15.0 ns | 16.6 ns | 0 | +| end-to-end fresh read | 44.3 µs | 73.3 µs | 0 | + +Totals for N compatible reads (µs; fresh = WHERE + project + admit + read each time; warm = WHERE + project once, then admit + read; rebind = the owner advances before every read, the old selection is refused, then WHERE + project + admit + read): + +| N | fresh | warm | rebind | fresh / warm | +|---|---|---|---|---| +| 1 | 41.6 / 72.3 | 42.9 / 70.2 | 42.1 / 70.3 | 0.97 / 1.03 | +| 2 | 85.9 / 142.4 | 43.8 / 70.0 | 86.5 / 140.8 | 1.96 / 2.03 | +| 4 | 173.0 / 281.9 | 41.9 / 69.8 | 168.9 / 289.2 | 4.13 / 4.04 | +| 8 | 347.9 / 586.3 | 43.0 / 69.7 | 340.5 / 589.6 | 8.10 / 8.41 | +| 64 | exceeds 1,000 µs (failed gate) | 45.9 / 45.6 | exceeds 1,000 µs (failed gate) | — | + +Warm reuse breaks even at N = 1 and pays from N = 2. At N = 64 only warm reuse stays inside the fold budget. Rebind costs the same as fresh: invalidation is a cheap refusal followed by the full work. Absolute numbers move by up to 1.7× between runs on this shared host; only ratios within a run are used. These are microbenchmarks, reported, not gates. + +**Open limitations.** + +- **The seal attests the caller's claim, not the mask's provenance.** A detached `Keep` projected under a new seal after its source changed is accepted (pinned by the #1792-shape test, so a fix turns it red). Closing this needs the producer to bind a mask to the seal it was computed under; Quack's bound `Query` has no frame today (D-NFR S5). +- `Criteria` is a caller-supplied id; Quack exposes no digest of a bound query. +- The global codebook revision rides in `FrameRevisions::relation_map`; the owner, ACL and scope are the lab `FrameStore`, `Scope { id }` equality. +- The FALSE set costs a second WHERE program. A terminal producing both K3 masks in one pass is not built. +- One 64-slot frame per table; no larger focus, no DR256 resident register, no reuse of a scattered (`ScatterOrU32`) mask. +- `project` is 64 scalar probes (~1 µs); admission (~65–80 ns) is not broken down. diff --git a/crates/dr-math-binding-probe/examples/dr256_where_stages.rs b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs new file mode 100644 index 000000000..52eb537f0 --- /dev/null +++ b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs @@ -0,0 +1,868 @@ +//! D-DRCA-2 stage costs: `DR256::WHERE` × DR#3, each stage of the global +//! selection → local projection → fold path measured on its own, then the +//! cost of reusing one projected selection across N compatible reads. +//! +//! `cargo run --release --example dr256_where_stages` +//! +//! Lab only. Reported, not gated. Every number is the median of 21 timed +//! runs. Stages that are too small to time alone (admission, a fold, one +//! rotated read) are batched inside one call and reported per operation. +//! +//! The fixture (`world`) is built outside every timed region. Cold +//! preparation (encoding 65,536 rows into planes and lanes, the `LocalMap`, +//! the frame stores) is timed separately and is a once-per-frame cost; it is +//! reported, not part of any warm row. +//! +//! The reuse table compares three strategies for N compatible reads of one +//! selection: re-evaluating everything each time (fresh), evaluating once +//! and re-admitting (warm), and re-evaluating after the global owner moved +//! its source revision before every read (rebind-after-invalidation). The +//! answer of every strategy is asserted equal to an oracle count taken from +//! the world's facts. +use std::alloc::{GlobalAlloc, Layout, System}; +use std::cell::Cell; +use std::hint::black_box; +use std::time::Instant; + +use dr_math_binding_probe::hhtl16::{LocalMap, address, cell_rotated}; +use dr_math_binding_probe::relcomp::Rows; +use dr_math_binding_probe::where_dr3::{ + Criteria, GLOBAL, GLOBAL_WORDS, LocalSelection, ReuseRefusal, Under, project, selected_column, + selected_count, +}; +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, Frame, FrameRevisions, FrameStore, Guards, MethodSignature, + Operand, Refusal, Scope, bind_dr64, +}; +use lance_graph_mask_risc::{ + Foreign, LaneRef, Out, Planes, Program, Scratch, execute_into, words_for, +}; +use lance_graph_quack::bind::{Binder, BoundField, FieldKind, TableId, table}; +use lance_graph_quack::{Agg, Cmp, Col, Filter, Mask, Query, lower}; + +// ── allocation counter ──────────────────────────────────────────────────── + +struct Counting; +thread_local! { + static ALLOCS: Cell = const { Cell::new(0) }; +} +fn allocs() -> u64 { + ALLOCS.with(Cell::get) +} +// SAFETY: forwards to `System` unchanged; only counts calls. +unsafe impl GlobalAlloc for Counting { + unsafe fn alloc(&self, l: Layout) -> *mut u8 { + ALLOCS.with(|c| c.set(c.get() + 1)); + // SAFETY: same contract as the caller's. + unsafe { System.alloc(l) } + } + unsafe fn dealloc(&self, p: *mut u8, l: Layout) { + // SAFETY: same contract as the caller's. + unsafe { System.dealloc(p, l) } + } +} +#[global_allocator] +static GLOBAL_ALLOC: Counting = Counting; + +// ── timing ──────────────────────────────────────────────────────────────── + +const RUNS: usize = 21; + +/// Median ns per op of `f` (which performs `ops` operations per call) and the +/// allocations of one untimed call. Returns the first call's result so the +/// caller can fold it into a printed checksum. +fn measure(name: &str, ops: u64, mut f: impl FnMut() -> u64) -> u64 { + let a0 = allocs(); + let first = black_box(f()); + let per_call_allocs = allocs() - a0; + let mut t: Vec = (0..RUNS) + .map(|_| { + let s = Instant::now(); + black_box(f()); + s.elapsed().as_nanos() as f64 / ops as f64 + }) + .collect(); + t.sort_by(f64::total_cmp); + println!( + "{name:<44} {ops:>6} ops {:>12.1} ns/op {per_call_allocs:>5} allocs/call", + t[RUNS / 2] + ); + first +} + +/// Median ns of one call of `f`. +fn median_ns(mut f: impl FnMut() -> u64, sink: &mut u64) -> f64 { + *sink ^= black_box(f()); + let mut t: Vec = (0..RUNS) + .map(|_| { + let s = Instant::now(); + *sink ^= black_box(f()); + s.elapsed().as_nanos() as f64 + }) + .collect(); + t.sort_by(f64::total_cmp); + t[RUNS / 2] +} + +// ── the source, as plain values ─────────────────────────────────────────── + +const EMP: u32 = 21; +const DEPT: u32 = 22; +const OTHER: u32 = 9; +const EMP_CLASS: u16 = 21; + +#[derive(Clone, Copy, Debug)] +struct Row { + class: u32, + sel: Option, + live: bool, +} + +struct Rng(u64); +impl Rng { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + fn below(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +fn source(rng: &mut Rng) -> Vec { + (0..GLOBAL) + .map(|_| { + let class = match rng.below(10) { + 0..=4 => EMP, + 5..=7 => DEPT, + _ => OTHER, + }; + let sel = (rng.below(7) != 0).then(|| rng.below(3) as i32); + Row { + class, + sel, + live: rng.below(20) != 0, + } + }) + .collect() +} + +/// The oracle's three-valued verdict of `class = 'employee' AND sel = want`. +/// `None`: not in the live population (neither TRUE nor FALSE). +fn verdict(r: &Row, want: i32) -> Option> { + if !r.live { + return None; + } + Some(if r.class != EMP { + Some(false) + } else { + r.sel.map(|v| v == want) + }) +} + +// ── the engine side: resident encoding + Quack ──────────────────────────── + +/// Planes: 0 = live, 1 = validity of `sel`, 2 = every address. Lanes: 0 = +/// class code (`U32`), 1 = `sel` (`I32`; payload at NULL rows is 1). +struct Resident { + planes: [Vec; 3], + class: Vec, + sel: Vec, +} +const LIVE: Mask = Mask(0); +const VSEL: Mask = Mask(1); +const CLASS: Col = Col(0); +const SEL: Col = Col(1); + +fn resident(src: &[Row], codebook: &Codebook) -> Resident { + let mut planes: [Vec; 3] = std::array::from_fn(|_| vec![0u64; GLOBAL_WORDS]); + let (mut class, mut sel) = (vec![0u32; GLOBAL], vec![1i32; GLOBAL]); + for (g, r) in src.iter().enumerate() { + let set = |p: &mut Vec| p[g / 64] |= 1 << (g % 64); + if r.live { + set(&mut planes[0]); + } + if let Some(v) = r.sel { + set(&mut planes[1]); + sel[g] = v; + } + set(&mut planes[2]); + class[g] = codebook.encode(r.class); + } + Resident { planes, class, sel } +} + +/// The consumer codebook: which `U32` code the class `employee` carries. +#[derive(Clone, Copy)] +struct Codebook { + shift: u32, +} +impl Codebook { + fn encode(&self, class: u32) -> u32 { + class + self.shift + } +} +impl Binder for Codebook { + fn table(&self, name: &str) -> Option { + (name == "node").then_some(TableId(0)) + } + fn live(&self, _t: TableId) -> Mask { + LIVE + } + fn field(&self, _t: TableId, name: &str) -> Option { + match name { + "class" => Some(BoundField { + col: CLASS, + kind: FieldKind::Code, + validity: None, + }), + "sel" => Some(BoundField { + col: SEL, + kind: FieldKind::I32, + validity: Some(VSEL), + }), + _ => None, + } + } + fn code(&self, _t: TableId, _f: Col, literal: &str) -> Option { + (literal == "employee").then_some(self.encode(EMP)) + } +} + +// ── frames, facts and registers ─────────────────────────────────────────── + +// Kept field for field identical to the test's fixture, so `world(SEED)` +// draws the same random sequence; the example reads only some fields. +#[allow(dead_code)] +struct World { + src: Vec, + emp_ids: Vec, + dept_ids: Vec, + skills: Vec, + sites: Vec, + has_skill: Vec<(u64, u64)>, + certified: Vec<(u64, u64, Option)>, + works_in: Vec<(u64, u64)>, + located_at: Vec<(u64, u64)>, +} + +/// 64 live employees and 64 live departments in shuffled source order, with +/// TRUE, FALSE and UNKNOWN employees all present. +fn world(seed: u64) -> World { + let mut rng = Rng(seed); + let src = source(&mut rng); + let pick = |rng: &mut Rng, class: u32| -> Vec { + let mut out = Vec::new(); + while out.len() < 64 { + let g = rng.below(GLOBAL as u64); + let r = src[g as usize]; + if r.live && r.class == class && !out.contains(&g) { + out.push(g); + } + } + out + }; + let emp_ids = pick(&mut rng, EMP); + let dept_ids = pick(&mut rng, DEPT); + let skills: Vec = (0..40).map(|i| 900_000 + i).collect(); + let sites: Vec = (0..16).map(|i| 800_000 + i).collect(); + let (mut has_skill, mut certified, mut works_in, mut located_at) = + (Vec::new(), Vec::new(), Vec::new(), Vec::new()); + for &e in &emp_ids { + for _ in 0..rng.below(5) { + let s = skills[rng.below(skills.len() as u64) as usize]; + if !has_skill.contains(&(e, s)) { + has_skill.push((e, s)); + let c = match rng.below(3) { + 0 => Some(true), + 1 => Some(false), + _ => None, + }; + certified.push((e, s, c)); + } + } + works_in.push((e, dept_ids[rng.below(64) as usize])); + } + for &d in &dept_ids { + for _ in 0..1 + rng.below(2) { + let t = sites[rng.below(16) as usize]; + if !located_at.contains(&(d, t)) { + located_at.push((d, t)); + } + } + } + World { + src, + emp_ids, + dept_ids, + skills, + sites, + has_skill, + certified, + works_in, + located_at, + } +} + +fn pos(ids: &[u64], g: u64) -> u8 { + ids.iter().position(|&x| x == g).unwrap() as u8 +} + +/// Registers are built from the oracle's positions, not through the map. +fn plane(facts: &[(u64, u64)], rows: &[u64], cols: &[u64]) -> Rows { + let mut r = [0u64; 64]; + for &(a, b) in facts { + r[pos(rows, a) as usize] |= 1 << pos(cols, b); + } + r +} + +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 7 }; +const CRITERIA: Criteria = Criteria { id: 0xC1 }; + +fn axis(class: u16, kind: AxisKind) -> Axis { + Axis { class, kind } +} +fn emp_id() -> Axis { + axis(EMP_CLASS, AxisKind::Identity) +} +fn sig(ord: u16, row: Axis, col: Axis) -> MethodSignature { + MethodSignature::presence(row.class, ord, row, col) +} +fn has_skill_sig() -> MethodSignature { + sig(1, emp_id(), axis(EMP_CLASS, AxisKind::Property)) +} + +/// The global source's owner. `relation_map` is the codebook revision. +fn global_store(cb: &Codebook) -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: u64::from(cb.shift), + coordinates: 1, + }) +} +/// The DR frame's owner, sealed under one map's coordinate assignment. +fn local_store(map: &LocalMap) -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: map.digest(), + }) +} +fn guards(st: &FrameStore, focus: Focus, scope: Scope) -> Guards { + Guards { + frame: st.seal(), + focus, + scope, + } +} +fn bind<'a>( + st: &FrameStore, + g: &Guards, + m: MethodSignature, + rows: &'a Rows, + validity: Option<&'a Rows>, +) -> BoundDr64<'a> { + bind_dr64(st, m, m, g, (g.focus, g.scope), Operand { rows, validity }).unwrap() +} + +const SEED: u64 = 0xD0CA_0002; + +/// The fold budget for one batch (workspace rule: ns per op, µs per batch, +/// never milliseconds). +const GATE_NS: f64 = 1_000_000.0; +fn gated(ns: f64) -> String { + if ns > GATE_NS { + "> 1,000 (FAIL)".to_string() + } else { + format!("{:.1}", ns / 1_000.0) + } +} +const WANT: i32 = 1; + +// ── WHERE: lowered once, executed many times ────────────────────────────── + +/// One lowered `Keep` program and its scratch, built once. +struct Kept { + prog: Program, + scratch: Scratch<'static>, +} +impl Kept { + fn new(filter: Filter) -> Kept { + let q = Query { + filter, + agg: Agg::Rows, + }; + let prog = lower(&q).expect("lowers"); + let scratch = Scratch::for_program(&prog, GLOBAL).expect("carves"); + Kept { prog, scratch } + } + /// Execute into the caller's preallocated output; allocation-free. + fn run(&mut self, inp: &Inputs<'_>, out: &mut [u64]) { + let pl = Planes { + n_rows: GLOBAL, + masks: &inp.masks, + lanes: &inp.lanes, + }; + execute_into( + &self.prog, + &pl, + &Foreign::NONE, + &mut self.scratch, + Out::Mask(out), + ) + .expect("runs"); + } +} + +/// The borrowed resident inputs of the engine. +struct Inputs<'a> { + masks: Vec<&'a [u64]>, + lanes: [LaneRef<'a>; 2], +} + +/// The TRUE and FALSE Keep programs of `class = 'employee' AND sel = WANT` +/// and their reusable output buffers. +struct Eng { + kt: Kept, + kf: Kept, + ot: Vec, + of: Vec, +} +impl Eng { + fn where_true(&mut self, inp: &Inputs<'_>) { + self.kt.run(inp, &mut self.ot); + } + fn where_false(&mut self, inp: &Inputs<'_>) { + self.kf.run(inp, &mut self.of); + } + fn where_both(&mut self, inp: &Inputs<'_>) { + self.where_true(inp); + self.where_false(inp); + } +} + +/// The TRUE-side filter as Quack's own bind makes it, and the FALSE-side +/// filter built from the same leaves under NOT (`Filter::sql_where`). +fn filters(cb: &Codebook) -> (Filter, Filter) { + let bound = table("node") + .where_eq("class", "employee") + .where_eq("sel", WANT) + .bind(cb) + .expect("binds"); + let raw = Filter::and([ + Filter::Cmp(CLASS, Cmp::EqU32(cb.encode(EMP))), + Filter::Cmp(SEL, Cmp::EqI32(WANT)), + ]); + let nullable = [(SEL, VSEL)]; + let f = Filter::and([Filter::plane(LIVE), Filter::negate(raw)]).sql_where(&nullable); + (bound.filter, f) +} + +fn proj( + map: &LocalMap, + eng: &Eng, + gst: &FrameStore, + seal: &Frame, + lst: &FrameStore, + g: &Guards, +) -> LocalSelection { + project( + map, + &eng.ot, + &eng.of, + Under { + global_store: gst, + global: seal, + local_store: lst, + guards: g, + axis: emp_id(), + method: has_skill_sig(), + criteria: CRITERIA, + }, + ) + .unwrap() +} + +// ── the three reuse strategies ──────────────────────────────────────────── + +/// One full read: WHERE TRUE+FALSE, project, admit, count. +#[allow(clippy::too_many_arguments)] +fn fresh_read( + eng: &mut Eng, + inp: &Inputs<'_>, + map: &LocalMap, + gst: &FrameStore, + seal: &Frame, + lst: &FrameStore, + g: &Guards, + b: &BoundDr64<'_>, +) -> u64 { + eng.where_both(inp); + let sel = proj(map, eng, gst, seal, lst, g); + let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); + u64::from(selected_count(b.rows, a.truth())) +} + +#[allow(clippy::too_many_arguments)] +fn total_fresh( + n: usize, + eng: &mut Eng, + inp: &Inputs<'_>, + map: &LocalMap, + gst: &FrameStore, + seal: &Frame, + lst: &FrameStore, + g: &Guards, + b: &BoundDr64<'_>, +) -> u64 { + (0..n) + .map(|_| fresh_read(eng, inp, map, gst, seal, lst, g, b)) + .sum() +} + +#[allow(clippy::too_many_arguments)] +fn total_warm( + n: usize, + eng: &mut Eng, + inp: &Inputs<'_>, + map: &LocalMap, + gst: &FrameStore, + seal: &Frame, + lst: &FrameStore, + g: &Guards, + b: &BoundDr64<'_>, +) -> u64 { + eng.where_both(inp); + let sel = proj(map, eng, gst, seal, lst, g); + let mut acc = 0u64; + for _ in 0..n { + let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); + acc += u64::from(selected_count(b.rows, black_box(a.truth()))); + } + acc +} + +/// Before every read the global owner advances its source revision (same +/// data). The previous selection must be refused; WHERE, projection and +/// admission are then redone under the new seal. +#[allow(clippy::too_many_arguments)] +fn total_rebind( + n: usize, + eng: &mut Eng, + inp: &Inputs<'_>, + map: &LocalMap, + gst: &mut FrameStore, + lst: &FrameStore, + g: &Guards, + b: &BoundDr64<'_>, + prev: &mut LocalSelection, +) -> u64 { + let mut acc = 0u64; + for _ in 0..n { + let cur = gst.revisions(); + gst.advance(FrameRevisions { + source: cur.source + 1, + ..cur + }); + assert_eq!( + prev.admit(gst, lst, b, CRITERIA), + Err(ReuseRefusal::Global(Refusal::SourceChanged)), + "the old selection must be refused after the source moved" + ); + let seal = gst.seal(); + eng.where_both(inp); + let sel = proj(map, eng, gst, &seal, lst, g); + let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); + acc += u64::from(selected_count(b.rows, a.truth())); + *prev = sel; + } + acc +} + +fn cpu_model() -> String { + std::fs::read_to_string("/proc/cpuinfo") + .ok() + .and_then(|s| { + s.lines() + .find(|l| l.starts_with("model name")) + .and_then(|l| l.split(':').nth(1)) + .map(|m| m.trim().to_string()) + }) + .unwrap_or_else(|| "unknown (/proc/cpuinfo unreadable)".to_string()) +} + +fn main() { + println!( + "cpu: {} | avx512f: {} | runs per row: {RUNS}", + cpu_model(), + cfg!(target_feature = "avx512f") + ); + println!(); + + let mut sink = 0u64; + let cb = Codebook { shift: 0 }; + let w = world(SEED); + let res = resident(&w.src, &cb); + + // ── cold preparation (once per frame; not part of any warm row) ────── + println!("== cold preparation (once per frame; reported, not gated) =="); + sink ^= measure("resident: encode 65,536 rows", 1, || { + let r = resident(black_box(&w.src), black_box(&cb)); + r.planes[0][0] ^ u64::from(r.class[1]) + }); + sink ^= measure("LocalMap::prepare (64 ids)", 1, || { + LocalMap::prepare(black_box(&w.emp_ids)).unwrap().len() as u64 + }); + let emp = LocalMap::prepare(&w.emp_ids).unwrap(); + sink ^= measure("FrameStore::new + seal (local)", 1, || { + let st = local_store(black_box(&emp)); + guards(&st, FOCUS, SCOPE).frame.revisions().coordinates + }); + + // ── bind + lower ───────────────────────────────────────────────────── + println!(); + println!("== bind + lower =="); + sink ^= measure("quack: table().where_eq x2 .bind()", 1, || { + let bound = table("node") + .where_eq("class", "employee") + .where_eq("sel", WANT) + .bind(black_box(&cb)) + .expect("binds"); + black_box(bound); + 1 + }); + let (ftrue, ffalse) = filters(&cb); + let q_true = Query { + filter: ftrue.clone(), + agg: Agg::Rows, + }; + sink ^= measure("quack: lower(&query)", 1, || { + black_box(lower(black_box(&q_true)).expect("lowers")); + 1 + }); + + // ── engine state: lowered once, scratch and outputs preallocated ───── + let masks: Vec<&[u64]> = res.planes.iter().map(Vec::as_slice).collect(); + let inp = Inputs { + masks, + lanes: [LaneRef::U32(&res.class), LaneRef::I32(&res.sel)], + }; + let mut eng = Eng { + kt: Kept::new(ftrue), + kf: Kept::new(ffalse), + ot: vec![0u64; words_for(GLOBAL)], + of: vec![0u64; words_for(GLOBAL)], + }; + + // ── WHERE evaluation ───────────────────────────────────────────────── + println!(); + println!("== WHERE evaluation (program lowered once; execute_into only) =="); + sink ^= measure("WHERE TRUE Keep (65,536 rows)", 1, || { + eng.where_true(black_box(&inp)); + eng.ot[0] ^ eng.ot[GLOBAL_WORDS - 1] + }); + sink ^= measure("WHERE FALSE Keep (65,536 rows)", 1, || { + eng.where_false(black_box(&inp)); + eng.of[0] ^ eng.of[GLOBAL_WORDS - 1] + }); + sink ^= measure("WHERE TRUE + FALSE", 1, || { + eng.where_both(black_box(&inp)); + eng.ot[0] ^ eng.of[GLOBAL_WORDS - 1] + }); + eng.where_both(&inp); + + // ── frames, register, selection ────────────────────────────────────── + let gst = global_store(&cb); + let lst = local_store(&emp); + let seal = gst.seal(); + let g = guards(&lst, FOCUS, SCOPE); + let r = plane(&w.has_skill, &w.emp_ids, &w.skills); + let b = bind(&lst, &g, has_skill_sig(), &r, None); + + // ── global -> local, admission, reads ──────────────────────────────── + println!(); + println!("== global -> local, admission, warm reads =="); + sink ^= measure("project: global->local (64 probes)", 1, || { + let sel = proj( + black_box(&emp), + black_box(&eng), + black_box(&gst), + black_box(&seal), + black_box(&lst), + black_box(&g), + ); + u64::from(sel.probes()) + }); + let sel = proj(&emp, &eng, &gst, &seal, &lst, &g); + const BATCH: u64 = 256; + sink ^= measure("admit: LocalSelection::admit", BATCH, || { + let mut acc = 0u64; + for _ in 0..BATCH { + let a = black_box(&sel) + .admit(black_box(&gst), black_box(&lst), black_box(&b), CRITERIA) + .unwrap(); + acc ^= black_box(a.truth()); + } + acc + }); + sink ^= measure("warm read: admit + selected_count", BATCH, || { + let mut acc = 0u64; + for _ in 0..BATCH { + let a = black_box(&sel) + .admit(black_box(&gst), black_box(&lst), black_box(&b), CRITERIA) + .unwrap(); + acc += u64::from(selected_count(black_box(b.rows), black_box(a.truth()))); + } + acc + }); + let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); + assert_ne!(a.truth(), 0, "the fixture must select some identity"); + let x = a.truth().trailing_zeros() as u8; + sink ^= measure("rotation: cell_rotated via address(y, x)", 64, || { + let mut acc = 0u64; + for y in 0..64u8 { + let code = address(black_box(y), black_box(x)).unwrap(); + acc += u64::from(cell_rotated(black_box(b.rows), code).unwrap()); + } + acc + }); + sink ^= measure("fold: selected_count", BATCH, || { + let mut acc = 0u64; + for _ in 0..BATCH { + acc += u64::from(selected_count(black_box(b.rows), black_box(a.truth()))); + } + acc + }); + sink ^= measure("fold: selected_column (one column)", 40, || { + let mut acc = 0u64; + for y in 0..40u8 { + acc ^= selected_column(black_box(b.rows), black_box(a.truth()), black_box(y)).unwrap(); + } + acc + }); + sink ^= measure("end-to-end fresh read", 1, || { + fresh_read( + &mut eng, + black_box(&inp), + black_box(&emp), + &gst, + &seal, + &lst, + &g, + &b, + ) + }); + + // ── oracle ─────────────────────────────────────────────────────────── + let oracle = w + .has_skill + .iter() + .filter(|&&(e, _)| verdict(&w.src[e as usize], WANT) == Some(Some(true))) + .count() as u64; + assert!(oracle > 0, "the oracle must select some fact"); + assert!( + (oracle as usize) < w.has_skill.len(), + "the selection must remove some fact" + ); + let fresh1 = fresh_read(&mut eng, &inp, &emp, &gst, &seal, &lst, &g, &b); + let warm1 = total_warm(1, &mut eng, &inp, &emp, &gst, &seal, &lst, &g, &b); + assert_eq!(fresh1, oracle, "fresh answer equals the oracle"); + assert_eq!(warm1, oracle, "warm answer equals the oracle"); + + // ── reuse table ────────────────────────────────────────────────────── + println!(); + println!("== reuse: total µs for N compatible reads (median of {RUNS}) =="); + println!(" a total above 1,000 µs is a failed gate: printed as such, no ratio drawn from it"); + println!( + "{:>3} {:>16} {:>16} {:>16} {:>12} {:>10}", + "N", "fresh µs", "warm µs", "rebind µs", "fresh/warm", "warm GATE_NS || t_warm > GATE_NS { + ("-".to_string(), "-".to_string()) + } else { + ( + format!("{:.2}x", t_fresh / t_warm), + (t_warm < t_fresh).to_string(), + ) + }; + println!( + "{n:>3} {:>16} {:>16} {:>16} {ratio:>12} {cmp:>10}", + gated(t_fresh), + gated(t_warm), + gated(t_rebind) + ); + } + + println!(); + println!("checksum (anti-DCE): {sink:#018x}"); + println!( + "note: microbenchmarks on a shared machine, reported, not gated. Ratios within one run \ + are the meaningful quantity; absolute ns move with the host. Cold preparation is a \ + once-per-frame cost and is not part of any warm row. The rebind column asserts the old \ + selection is refused (a cheap early-out) inside the timed total." + ); +} From f9957b0661e7ebd86783513b99b5b57690252169 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:49:04 +0000 Subject: [PATCH 4/7] probe(dr-math): D-DRCA-2 Boolean folds refuse three-valued registers The same defect Codex found in hhtl16::cooccurrence (#1834) applied to selected_count, selected_column and selected_cell: they read payload bits as presence and accepted rows of a three-valued register. Admitted now records whether the register it was admitted against is two-valued and distinct, the folds take the Admitted instead of a bare word and return None otherwise. selected_column_k3 reads validity and serves both. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../examples/dr256_where_stages.rs | 12 ++-- crates/dr-math-binding-probe/src/where_dr3.rs | 56 ++++++++++++++----- .../tests/dr256_where_dr3.rs | 34 ++++++----- 3 files changed, 67 insertions(+), 35 deletions(-) diff --git a/crates/dr-math-binding-probe/examples/dr256_where_stages.rs b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs index 52eb537f0..3ed766785 100644 --- a/crates/dr-math-binding-probe/examples/dr256_where_stages.rs +++ b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs @@ -505,7 +505,7 @@ fn fresh_read( eng.where_both(inp); let sel = proj(map, eng, gst, seal, lst, g); let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); - u64::from(selected_count(b.rows, a.truth())) + u64::from(selected_count(b.rows, &a).unwrap()) } #[allow(clippy::too_many_arguments)] @@ -542,7 +542,7 @@ fn total_warm( let mut acc = 0u64; for _ in 0..n { let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); - acc += u64::from(selected_count(b.rows, black_box(a.truth()))); + acc += u64::from(selected_count(b.rows, black_box(&a)).unwrap()); } acc } @@ -578,7 +578,7 @@ fn total_rebind( eng.where_both(inp); let sel = proj(map, eng, gst, &seal, lst, g); let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); - acc += u64::from(selected_count(b.rows, a.truth())); + acc += u64::from(selected_count(b.rows, &a).unwrap()); *prev = sel; } acc @@ -716,7 +716,7 @@ fn main() { let a = black_box(&sel) .admit(black_box(&gst), black_box(&lst), black_box(&b), CRITERIA) .unwrap(); - acc += u64::from(selected_count(black_box(b.rows), black_box(a.truth()))); + acc += u64::from(selected_count(black_box(b.rows), black_box(&a)).unwrap()); } acc }); @@ -734,14 +734,14 @@ fn main() { sink ^= measure("fold: selected_count", BATCH, || { let mut acc = 0u64; for _ in 0..BATCH { - acc += u64::from(selected_count(black_box(b.rows), black_box(a.truth()))); + acc += u64::from(selected_count(black_box(b.rows), black_box(&a)).unwrap()); } acc }); sink ^= measure("fold: selected_column (one column)", 40, || { let mut acc = 0u64; for y in 0..40u8 { - acc ^= selected_column(black_box(b.rows), black_box(a.truth()), black_box(y)).unwrap(); + acc ^= selected_column(black_box(b.rows), black_box(&a), black_box(y)).unwrap(); } acc }); diff --git a/crates/dr-math-binding-probe/src/where_dr3.rs b/crates/dr-math-binding-probe/src/where_dr3.rs index af9ba92eb..57447de02 100644 --- a/crates/dr-math-binding-probe/src/where_dr3.rs +++ b/crates/dr-math-binding-probe/src/where_dr3.rs @@ -37,16 +37,21 @@ //! 3. **Fold** ([`selected_count`], [`selected_column`], //! [`selected_column_k3`], [`selected_cell`]): the selection is a `u64` //! over the identity axis, ANDed into reads of the borrowed rows. No -//! Cartesian product is built and no row is copied. +//! Cartesian product is built and no row is copied. The Boolean folds +//! refuse a three-valued or bag register; [`selected_column_k3`] reads +//! validity and serves both. //! //! # Three-valued semantics //! //! WHERE keeps TRUE only. UNKNOWN is carried separately //! ([`Admitted::unknown`]) and is never folded into FALSE: the complement of a //! selection is its FALSE set, not "every slot not TRUE". -use crate::hhtl16::{self, LocalMap, MapRefusal}; +use crate::hhtl16::{self, LocalMap}; use crate::relcomp::Rows; -use crate::{Axis, BoundDr64, Focus, Frame, FrameStore, Guards, MethodSignature, Refusal, Scope}; +use crate::{ + Axis, BoundDr64, Focus, Frame, FrameStore, Guards, MethodSignature, Population, Refusal, Scope, + Truth, +}; /// Addresses in one DR256 global population. pub const GLOBAL: usize = 65_536; @@ -121,6 +126,9 @@ pub struct Admitted { truth: u64, falsity: u64, slots: u64, + /// The register admitted against is two-valued and distinct, so the + /// Boolean folds may read its payload bits as presence. + boolean: bool, } impl Admitted { @@ -256,30 +264,46 @@ impl LocalSelection { truth: self.truth, falsity: self.falsity, slots: self.slots, + boolean: register.method.truth == Truth::TwoValued + && register.method.population == Population::Distinct, }) } } +// The Boolean folds below read payload bits as presence. They refuse (return +// `None`) when the selection was admitted against a three-valued or bag +// register, where a payload bit under an UNKNOWN cell would count as present +// and a zero-filled one as absent: the rule `hhtl16::cooccurrence` and +// `relcomp::Chain::new` apply. `rows` must be the admitted register's rows or +// a Boolean derivation of them (a `Chain` composition). + /// Identity × Property cells over the selected identities: Σ over set bits -/// `x` of `sel` of `popcount(rows[x])`. -pub fn selected_count(rows: &Rows, sel: u64) -> u32 { - let (mut s, mut n) = (sel, 0u32); +/// `x` of the TRUE selection of `popcount(rows[x])`. +pub fn selected_count(rows: &Rows, a: &Admitted) -> Option { + if !a.boolean { + return None; + } + let (mut s, mut n) = (a.truth, 0u32); while s != 0 { let x = s.trailing_zeros() as usize; n += rows[x].count_ones(); s &= s - 1; } - n + Some(n) } /// The selected identities holding property `y`: one column read, ANDed. -pub fn selected_column(rows: &Rows, sel: u64, y: u8) -> Option { - hhtl16::column(rows, y).map(|c| c & sel) +pub fn selected_column(rows: &Rows, a: &Admitted, y: u8) -> Option { + if !a.boolean { + return None; + } + hhtl16::column(rows, y).map(|c| c & a.truth) } /// Three-valued column `y` over the selected identities: (known TRUE, known /// FALSE, UNKNOWN). A two-valued register has no UNKNOWN. -pub fn selected_column_k3(r: &BoundDr64<'_>, sel: u64, y: u8) -> Option<(u64, u64, u64)> { +pub fn selected_column_k3(r: &BoundDr64<'_>, a: &Admitted, y: u8) -> Option<(u64, u64, u64)> { + let sel = a.truth; let col = hhtl16::column(r.rows, y)?; let known = match r.validity { Some(_) => hhtl16::column_validity(r, y)?, @@ -288,8 +312,12 @@ pub fn selected_column_k3(r: &BoundDr64<'_>, sel: u64, y: u8) -> Option<(u64, u6 Some((col & known & sel, !col & known & sel, !known & sel)) } -/// One cell `(x, y)`, read only if `x` is selected. -pub fn selected_cell(rows: &Rows, sel: u64, x: u8, y: u8) -> Result { - let code = hhtl16::address(x, y)?; - Ok((sel >> x) & 1 == 1 && hhtl16::cell(rows, code)?) +/// One cell `(x, y)`, read only if `x` is selected. `None` outside the +/// register or for a non-Boolean admission. +pub fn selected_cell(rows: &Rows, a: &Admitted, x: u8, y: u8) -> Option { + if !a.boolean { + return None; + } + let code = hhtl16::address(x, y).ok()?; + Some((a.truth >> x) & 1 == 1 && hhtl16::cell(rows, code).ok()?) } diff --git a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs index 44f5f54bb..093b05aa5 100644 --- a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs +++ b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs @@ -616,7 +616,7 @@ fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { for (y, &s) in w.skills.iter().enumerate() { let y = y as u8; let want = selected(e) && holds(e, s); - assert_eq!(selected_cell(b.rows, a.truth(), x, y).unwrap(), want); + assert_eq!(selected_cell(b.rows, &a, x, y).unwrap(), want); // YZ rotation: the rotated address (y, x) reads the same fact, and // the selection still applies to the identity coordinate. let rot = @@ -627,7 +627,7 @@ fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { } } for (y, &s) in w.skills.iter().enumerate() { - let col = selected_column(b.rows, a.truth(), y as u8).unwrap(); + let col = selected_column(b.rows, &a, y as u8).unwrap(); let expect = w .emp_ids .iter() @@ -636,7 +636,7 @@ fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { assert_eq!(col, expect, "column {s}"); } selected_facts += w.has_skill.iter().filter(|&&(e, _)| selected(e)).count() as u32; - assert_eq!(selected_count(b.rows, a.truth()), selected_facts); + assert_eq!(selected_count(b.rows, &a).unwrap(), selected_facts); assert_eq!(cells, selected_facts); assert_eq!(rotated_hits, cells); // Anti-vacuity: the selection removes facts, and keeps some. @@ -689,7 +689,7 @@ fn unknown_stays_unknown_in_selection_negation_and_property() { // Three-valued property over the selected identities, column by column. let (mut u_cells, mut f_cells) = (0u32, 0u32); for (y, &s) in w.skills.iter().enumerate() { - let (ct, cf, cu) = selected_column_k3(&b, a.truth(), y as u8).unwrap(); + let (ct, cf, cu) = selected_column_k3(&b, &a, y as u8).unwrap(); let (mut et, mut ef, mut eu) = (0u64, 0u64, 0u64); for &e in &w.emp_ids { if verdict(&w.src[e as usize], WANT) != Some(Some(true)) { @@ -708,6 +708,11 @@ fn unknown_stays_unknown_in_selection_negation_and_property() { f_cells += cf.count_ones(); } assert!(u_cells > 0 && f_cells > 0); + // The Boolean folds read payload bits as presence, so they refuse a + // selection admitted against this three-valued register. + assert_eq!(selected_count(b.rows, &a), None); + assert_eq!(selected_column(b.rows, &a, 0), None); + assert_eq!(selected_cell(b.rows, &a, 0, 0), None); } // ── 5. source change after WHERE: refuse, then rebind ───────────────────── @@ -774,8 +779,8 @@ fn source_change_after_where_refuses_reuse_and_rebind_matches() { ); // The silent alternative: the old projection would still answer. assert_ne!( - selected_count(b.rows, before.truth()), - selected_count(b.rows, after.truth()) + selected_count(b.rows, &before).unwrap(), + selected_count(b.rows, &after).unwrap() ); } @@ -876,7 +881,7 @@ fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { let mut hits = 0u32; for &e in &w.emp_ids { for &s in &w.sites { - let got = selected_cell(&es, a.truth(), pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); + let got = selected_cell(&es, &a, pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); assert_eq!(got, selected(e) && at_site(&w, e, s), "({e}, {s})"); hits += u32::from(got); } @@ -920,8 +925,7 @@ fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { .unwrap(); for &e in &w.emp_ids { for &s in &w.sites { - let got = - selected_cell(&es2, a2.truth(), pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); + let got = selected_cell(&es2, &a2, pos(&w.emp_ids, e), pos(&w.sites, s)).unwrap(); assert_eq!(got, selected(e) && at_site(&w, e, s)); } } @@ -1011,8 +1015,8 @@ fn reseal_and_coordinate_changes_refuse() { let a2 = sel2.admit(&gst, &lst, &b2, CRITERIA).unwrap(); assert_eq!(a2.truth(), oracle_local(&w.src, &reordered, WANT).0); assert_eq!( - selected_count(b2.rows, a2.truth()), - selected_count(&r, before.truth()) + selected_count(b2.rows, &a2).unwrap(), + selected_count(&r, &before).unwrap() ); } @@ -1124,7 +1128,7 @@ fn empty_and_full_global_selections_are_exact() { (a0.truth(), a0.falsity(), a0.unknown()), oracle_local(&w.src, &w.emp_ids, 99) ); - assert_eq!(selected_count(b.rows, a0.truth()), 0); + assert_eq!(selected_count(b.rows, &a0).unwrap(), 0); // Full: the every-address plane. All 65,536 TRUE, every slot selected. let full = keep(&res, Filter::plane(ALL)); let none = vec![0u64; GLOBAL_WORDS]; @@ -1147,7 +1151,7 @@ fn empty_and_full_global_selections_are_exact() { let a1 = s1.admit(&gst, &lst, &b, CRITERIA).unwrap(); assert_eq!((a1.truth(), a1.falsity(), a1.unknown()), (u64::MAX, 0, 0)); assert_eq!( - selected_count(b.rows, a1.truth()) as usize, + selected_count(b.rows, &a1).unwrap() as usize, w.has_skill.len() ); // Malformed inputs are refused, not read. @@ -1299,9 +1303,9 @@ fn projection_admission_and_folds_do_not_allocate() { ) .unwrap(); let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); - let mut acc = selected_count(b.rows, a.truth()); + let mut acc = selected_count(b.rows, &a).unwrap(); for y in 0..40u8 { - acc ^= selected_column(b.rows, a.truth(), y).unwrap().count_ones(); + acc ^= selected_column(b.rows, &a, y).unwrap().count_ones(); } assert_eq!(allocs(), before, "acc={acc}"); let _ = hhtl16::LOCAL + where_dr3::GLOBAL; From cbc7930fa892228fd594e33acd8055e329b350e6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 08:50:18 +0000 Subject: [PATCH 5/7] docs(dr-math): D-DRCA-2 README and board entry for the Boolean-fold refusal Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md | 2 +- crates/dr-math-binding-probe/README.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md index 7c91b0d1d..6a4890e6c 100644 --- a/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md +++ b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md @@ -8,7 +8,7 @@ - Every read is re-admitted against owner, source, codebook, frame, register frame, axis, DR method, focus, scope and criteria; each refusal is pinned by a test against an independent source-ID oracle. - UNKNOWN stays apart from FALSE in the selection, its negation and a three-valued property column. - Projection, admission and folds allocate nothing. Warm read 71–90 ns; fresh read 44–73 µs (WHERE dominates). Warm reuse breaks even at N = 1 and pays from N = 2 (1.96–2.03×), 8.1–8.4× at N = 8; at N = 64 fresh and rebind exceed 1,000 µs (failed gate), warm stays at 46 µs. -- Sixteen disable runs each turn a test red. The first pass found the projection-time seal checks unpinned; a test was added. +- Seventeen disable runs each turn a test red (the Boolean folds refuse a three-valued register, the Codex #1834 finding applied here). The first pass found the projection-time seal checks unpinned; a test was added. - The #1792 control still reproduces (`reused R2 1032 vs fresh 31`). ## Open diff --git a/crates/dr-math-binding-probe/README.md b/crates/dr-math-binding-probe/README.md index 1b7cd34ac..0a914eb29 100644 --- a/crates/dr-math-binding-probe/README.md +++ b/crates/dr-math-binding-probe/README.md @@ -74,7 +74,7 @@ Lab test of the composition `global selection → optional amortized global→lo - **Global → local.** `project` tests bit `global(l)` of both masks for each local slot of the table's `LocalMap`: `map.len()` probes, never a pass over the universe, no map search. A selected identity outside the frame is not projected. The frame must carry `LocalMap::digest()` as its `coordinates` revision, so a selection cannot be projected through one coordinate assignment and read under another. - **Admission.** Every read goes through `LocalSelection::admit`, which re-checks the global source seal (owner, source revision, codebook, address space), the local frame, register frame identity, identity axis, DR method, focus, scope and criteria. The only readable form is the `Admitted` it returns. A `LocalSelection` is a caller-owned value; there is no store or cache. - **Folds.** The selection is a `u64` over the identity axis, ANDed into reads of the borrowed rows (`selected_count`, `selected_column`, `selected_column_k3`, `selected_cell`). No Cartesian product, no copied row. -- **K3.** WHERE keeps TRUE. UNKNOWN is carried separately and never folded into FALSE; the negation of a selection is its FALSE set. +- **K3.** WHERE keeps TRUE. UNKNOWN is carried separately and never folded into FALSE; the negation of a selection is its FALSE set. The Boolean folds read payload bits as presence, so they refuse a selection admitted against a three-valued or bag register (the rule `hhtl16::cooccurrence` and `relcomp::Chain::new` apply); `selected_column_k3` reads validity and serves both. Oracle: the source is plain Rust values per global address (`class`, `sel: Option`, `live`). Verdicts are a `match` on `Option`, local positions are `position()` in the frame's source-order id list, and registers are built from those positions, not through the map. It shares no code with Quack, mask-risc, `hhtl16` or `where_dr3`. NULL rows carry the payload the predicate tests for, so an engine that read NULL payloads would keep them. @@ -83,7 +83,7 @@ Thirteen tests against that oracle: - the global selection, whole mask over all 65,536 addresses, and its in-frame TRUE / FALSE / UNKNOWN (all three non-empty; most selected identities lie outside the frame); - equal local ordinals of two tables: the employee selection projected through the department map selects no department, and reading it against a department-row register is refused (`AxisMismatch`, `DifferentFrame`); - selected Identity × Property cell by cell, by column and by count, and the same relationships through the YZ rotation; -- UNKNOWN: kept apart from FALSE in the selection, in its negation and in a three-valued property column; +- UNKNOWN: kept apart from FALSE in the selection, in its negation and in a three-valued property column, and the Boolean folds refuse that three-valued register; - a source change after WHERE (refused, then rebound to the oracle); - a scope or focus change with identical coordinates (refused; the unchanged register admits); - selected employees' sites through a witnessed FK (`Chain`), then a changed referenced property (refused, rebound); @@ -94,7 +94,7 @@ Thirteen tests against that oracle: - projection under a stale global seal, a foreign owner's seal or a resealed local frame; - projection, admission and folds allocate nothing. -Disable runs, each restored from the commit and each turning at least one test red: the two projection-time seal checks, `MapNotFrame`, the TRUE ∧ FALSE check, TRUE/FALSE swapped, the eight admission guards (global, local, frame issue, axis, method, focus, scope, criteria), UNKNOWN computed as "not TRUE", the three-valued column reporting UNKNOWN as FALSE, and `selected_count` ignoring the selection. The first pass found the two projection-time seal checks covered by no test; the projection test above was added for them and both now go red. +Disable runs, each restored from the commit and each turning at least one test red: the two projection-time seal checks, `MapNotFrame`, the TRUE ∧ FALSE check, TRUE/FALSE swapped, the eight admission guards (global, local, frame issue, axis, method, focus, scope, criteria), UNKNOWN computed as "not TRUE", the three-valued column reporting UNKNOWN as FALSE, `selected_count` ignoring the selection, and the Boolean folds accepting a three-valued register. The first pass found the two projection-time seal checks covered by no test; the projection test above was added for them and both now go red. The original #1792 control is unchanged and still reproduces: `cargo run --release --example p2_quack_where -- --controls` in `crates/drf-focus-probe` prints `reused R2 1032 vs fresh 31`. From 5151a76c0b9b97ed52d4af55a485bf9ea426ab45 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 09:04:13 +0000 Subject: [PATCH 6/7] probe(dr-math): D-DRCA-2 single WHERE; UNKNOWN is undecided, not FALSE Semantic correction. Epistemic absence ($null, NaN, SQL NULL, an unset validity bit, K3 UNKNOWN) is one logical value: no TRUE/FALSE judgment. The projection no longer takes a second FALSE mask as a truth representation. It takes Quack's one WHERE Keep (TRUE rows, three-valued through sql_where); Admitted exposes TRUE only and no complement, because the complement of a selection reads UNKNOWN as FALSE. A negation is its own WHERE over the negated criteria, so NOT UNKNOWN stays UNKNOWN; reusing one selection as the other is refused (CriteriaChanged). The three-valued property read returns the register's own value + validity form, with value masked by validity so a stale payload under an UNKNOWN cell is never TRUE. No Epi5 state is derived from absence. The stage example drops the second WHERE program. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../examples/dr256_where_stages.rs | 57 +-- crates/dr-math-binding-probe/src/where_dr3.rs | 82 ++-- .../tests/dr256_where_dr3.rs | 402 +++++++----------- 3 files changed, 201 insertions(+), 340 deletions(-) diff --git a/crates/dr-math-binding-probe/examples/dr256_where_stages.rs b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs index 3ed766785..1dfda8cdc 100644 --- a/crates/dr-math-binding-probe/examples/dr256_where_stages.rs +++ b/crates/dr-math-binding-probe/examples/dr256_where_stages.rs @@ -38,7 +38,7 @@ use lance_graph_mask_risc::{ Foreign, LaneRef, Out, Planes, Program, Scratch, execute_into, words_for, }; use lance_graph_quack::bind::{Binder, BoundField, FieldKind, TableId, table}; -use lance_graph_quack::{Agg, Cmp, Col, Filter, Mask, Query, lower}; +use lance_graph_quack::{Agg, Col, Filter, Mask, Query, lower}; // ── allocation counter ──────────────────────────────────────────────────── @@ -425,42 +425,26 @@ struct Inputs<'a> { lanes: [LaneRef<'a>; 2], } -/// The TRUE and FALSE Keep programs of `class = 'employee' AND sel = WANT` -/// and their reusable output buffers. +/// The one WHERE `Keep` program of `class = 'employee' AND sel = WANT` and its +/// reusable output buffer. struct Eng { kt: Kept, - kf: Kept, ot: Vec, - of: Vec, } impl Eng { fn where_true(&mut self, inp: &Inputs<'_>) { self.kt.run(inp, &mut self.ot); } - fn where_false(&mut self, inp: &Inputs<'_>) { - self.kf.run(inp, &mut self.of); - } - fn where_both(&mut self, inp: &Inputs<'_>) { - self.where_true(inp); - self.where_false(inp); - } } -/// The TRUE-side filter as Quack's own bind makes it, and the FALSE-side -/// filter built from the same leaves under NOT (`Filter::sql_where`). -fn filters(cb: &Codebook) -> (Filter, Filter) { - let bound = table("node") +/// The WHERE filter as Quack's own bind makes it (three-valued over `sel`). +fn filter(cb: &Codebook) -> Filter { + table("node") .where_eq("class", "employee") .where_eq("sel", WANT) .bind(cb) - .expect("binds"); - let raw = Filter::and([ - Filter::Cmp(CLASS, Cmp::EqU32(cb.encode(EMP))), - Filter::Cmp(SEL, Cmp::EqI32(WANT)), - ]); - let nullable = [(SEL, VSEL)]; - let f = Filter::and([Filter::plane(LIVE), Filter::negate(raw)]).sql_where(&nullable); - (bound.filter, f) + .expect("binds") + .filter } fn proj( @@ -474,7 +458,6 @@ fn proj( project( map, &eng.ot, - &eng.of, Under { global_store: gst, global: seal, @@ -490,7 +473,7 @@ fn proj( // ── the three reuse strategies ──────────────────────────────────────────── -/// One full read: WHERE TRUE+FALSE, project, admit, count. +/// One full read: WHERE, project, admit, count. #[allow(clippy::too_many_arguments)] fn fresh_read( eng: &mut Eng, @@ -502,7 +485,7 @@ fn fresh_read( g: &Guards, b: &BoundDr64<'_>, ) -> u64 { - eng.where_both(inp); + eng.where_true(inp); let sel = proj(map, eng, gst, seal, lst, g); let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); u64::from(selected_count(b.rows, &a).unwrap()) @@ -537,7 +520,7 @@ fn total_warm( g: &Guards, b: &BoundDr64<'_>, ) -> u64 { - eng.where_both(inp); + eng.where_true(inp); let sel = proj(map, eng, gst, seal, lst, g); let mut acc = 0u64; for _ in 0..n { @@ -575,7 +558,7 @@ fn total_rebind( "the old selection must be refused after the source moved" ); let seal = gst.seal(); - eng.where_both(inp); + eng.where_true(inp); let sel = proj(map, eng, gst, &seal, lst, g); let a = sel.admit(gst, lst, b, CRITERIA).unwrap(); acc += u64::from(selected_count(b.rows, &a).unwrap()); @@ -636,7 +619,7 @@ fn main() { black_box(bound); 1 }); - let (ftrue, ffalse) = filters(&cb); + let ftrue = filter(&cb); let q_true = Query { filter: ftrue.clone(), agg: Agg::Rows, @@ -654,27 +637,17 @@ fn main() { }; let mut eng = Eng { kt: Kept::new(ftrue), - kf: Kept::new(ffalse), ot: vec![0u64; words_for(GLOBAL)], - of: vec![0u64; words_for(GLOBAL)], }; // ── WHERE evaluation ───────────────────────────────────────────────── println!(); println!("== WHERE evaluation (program lowered once; execute_into only) =="); - sink ^= measure("WHERE TRUE Keep (65,536 rows)", 1, || { + sink ^= measure("WHERE Keep (65,536 rows)", 1, || { eng.where_true(black_box(&inp)); eng.ot[0] ^ eng.ot[GLOBAL_WORDS - 1] }); - sink ^= measure("WHERE FALSE Keep (65,536 rows)", 1, || { - eng.where_false(black_box(&inp)); - eng.of[0] ^ eng.of[GLOBAL_WORDS - 1] - }); - sink ^= measure("WHERE TRUE + FALSE", 1, || { - eng.where_both(black_box(&inp)); - eng.ot[0] ^ eng.of[GLOBAL_WORDS - 1] - }); - eng.where_both(&inp); + eng.where_true(&inp); // ── frames, register, selection ────────────────────────────────────── let gst = global_store(&cb); diff --git a/crates/dr-math-binding-probe/src/where_dr3.rs b/crates/dr-math-binding-probe/src/where_dr3.rs index 57447de02..87931760e 100644 --- a/crates/dr-math-binding-probe/src/where_dr3.rs +++ b/crates/dr-math-binding-probe/src/where_dr3.rs @@ -10,12 +10,11 @@ //! # What this module does not do //! //! It evaluates no predicate. The global selection is the output of Quack's -//! existing WHERE (`Query { filter, agg: Agg::Rows }` → mask-risc `Keep`), -//! handed in as two borrowed 8 KiB masks: the rows where the criteria are -//! TRUE and the rows where they are FALSE (`Filter::sql_where` of the -//! criteria and of their negation). A row in neither is UNKNOWN. This -//! module has no Quack or mask-risc dependency; the tests and the stage -//! example wire the real engine to it. +//! existing typed WHERE (`Query { filter, agg: Agg::Rows }` → mask-risc +//! `Keep`, three-valued through `Filter::sql_where`), handed in as one +//! borrowed 8 KiB mask: the rows where the criteria are TRUE. This module +//! has no Quack or mask-risc dependency; the tests and the stage example +//! wire the real engine to it. //! //! It stores nothing. A [`LocalSelection`] is a caller-owned value, the //! projection of one selection into one frame, with the guards it was made @@ -24,7 +23,7 @@ //! # The three steps //! //! 1. **Global → local** ([`project`]): for each local ordinal `l` of the -//! table's [`LocalMap`], test bit `global(l)` of the TRUE and FALSE masks. +//! table's [`LocalMap`], test bit `global(l)` of the WHERE mask. //! The work is `map.len()` probes, never a pass over 65,536 rows, and a //! selected identity outside the frame is not promoted into it. The frame //! must carry `map.digest()` as its `coordinates` revision, so a selection @@ -39,13 +38,25 @@ //! over the identity axis, ANDed into reads of the borrowed rows. No //! Cartesian product is built and no row is copied. The Boolean folds //! refuse a three-valued or bag register; [`selected_column_k3`] reads -//! validity and serves both. +//! value and validity and serves both. //! -//! # Three-valued semantics +//! # Epistemic absence //! -//! WHERE keeps TRUE only. UNKNOWN is carried separately -//! ([`Admitted::unknown`]) and is never folded into FALSE: the complement of a -//! selection is its FALSE set, not "every slot not TRUE". +//! `$null`, NaN, SQL NULL, an unset Arrow validity bit and K3 UNKNOWN are one +//! logical value here: no TRUE/FALSE judgment has been established. It says +//! nothing about whether the entity or relationship exists, and it carries no +//! finer epistemic state (that is CausalEdge64 Epi5, under its own evidence +//! contract, and is not derived from absence alone). +//! +//! - WHERE selects TRUE. A slot that is not selected is FALSE **or** UNKNOWN; +//! [`Admitted`] gives no complement, because the complement of a selection +//! would read UNKNOWN as FALSE. +//! - `NOT UNKNOWN` is UNKNOWN. A negated selection is a second WHERE over the +//! negated criteria, evaluated by Quack's typed three-valued `sql_where`, +//! never the complement of the first. +//! - A three-valued property keeps the existing value + validity +//! representation (Arrow-style, `BoundDr64::validity`); no separate FALSE +//! mask is introduced. use crate::hhtl16::{self, LocalMap}; use crate::relcomp::Rows; use crate::{ @@ -74,8 +85,6 @@ pub enum ProjectRefusal { OutOfUniverse, /// The local frame was not sealed under this map's coordinate assignment. MapNotFrame, - /// A row that is both TRUE and FALSE: not a three-valued selection. - NotThreeValued, /// The global source seal is not current. Global(Refusal), /// The local frame is not current. @@ -108,7 +117,6 @@ pub enum ReuseRefusal { #[derive(Clone, Debug)] pub struct LocalSelection { truth: u64, - falsity: u64, slots: u64, axis: Axis, method: MethodSignature, @@ -124,7 +132,6 @@ pub struct LocalSelection { #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct Admitted { truth: u64, - falsity: u64, slots: u64, /// The register admitted against is two-valued and distinct, so the /// Boolean folds may read its payload bits as presence. @@ -132,18 +139,11 @@ pub struct Admitted { } impl Admitted { - /// Identities where the criteria are TRUE: what WHERE keeps. + /// Identities where the criteria are TRUE: what WHERE keeps. The other + /// occupied slots are FALSE or UNKNOWN, and this type does not say which. pub fn truth(&self) -> u64 { self.truth } - /// Identities where the criteria are FALSE. - pub fn falsity(&self) -> u64 { - self.falsity - } - /// Identities where the criteria are UNKNOWN. Never part of FALSE. - pub fn unknown(&self) -> u64 { - self.slots & !(self.truth | self.falsity) - } /// The occupied local slots of the frame. pub fn slots(&self) -> u64 { self.slots @@ -169,17 +169,16 @@ pub struct Under<'a> { pub criteria: Criteria, } -/// Project a three-valued global selection into one table's frame. +/// Project a global WHERE selection into one table's frame. /// -/// `truth` and `falsity` are the `Keep` outputs of WHERE for the criteria and -/// for their negation. Work: `map.len()` probes into each mask. +/// `truth` is the `Keep` output of WHERE: the rows where the criteria are +/// TRUE. Work: `map.len()` probes into it. pub fn project( map: &LocalMap, truth: &[u64], - falsity: &[u64], under: Under<'_>, ) -> Result { - if truth.len() != GLOBAL_WORDS || falsity.len() != GLOBAL_WORDS { + if truth.len() != GLOBAL_WORDS { return Err(ProjectRefusal::WrongWidth); } under @@ -193,23 +192,17 @@ pub fn project( if under.guards.frame.revisions().coordinates != map.digest() { return Err(ProjectRefusal::MapNotFrame); } - let (mut t, mut f, mut slots) = (0u64, 0u64, 0u64); + let (mut t, mut slots) = (0u64, 0u64); for l in 0..map.len() as u8 { let g = map.global(l).ok_or(ProjectRefusal::OutOfUniverse)?; if g >= GLOBAL as u64 { return Err(ProjectRefusal::OutOfUniverse); } - let (bt, bf) = (bit(truth, g), bit(falsity, g)); - if bt && bf { - return Err(ProjectRefusal::NotThreeValued); - } - t |= u64::from(bt) << l; - f |= u64::from(bf) << l; + t |= u64::from(bit(truth, g)) << l; slots |= 1 << l; } Ok(LocalSelection { truth: t, - falsity: f, slots, axis: under.axis, method: under.method, @@ -262,7 +255,6 @@ impl LocalSelection { } Ok(Admitted { truth: self.truth, - falsity: self.falsity, slots: self.slots, boolean: register.method.truth == Truth::TwoValued && register.method.population == Population::Distinct, @@ -300,16 +292,20 @@ pub fn selected_column(rows: &Rows, a: &Admitted, y: u8) -> Option { hhtl16::column(rows, y).map(|c| c & a.truth) } -/// Three-valued column `y` over the selected identities: (known TRUE, known -/// FALSE, UNKNOWN). A two-valued register has no UNKNOWN. -pub fn selected_column_k3(r: &BoundDr64<'_>, a: &Admitted, y: u8) -> Option<(u64, u64, u64)> { +/// Column `y` over the selected identities in the register's own +/// representation: `(value, validity)`, both restricted to the selection. +/// A selected identity whose validity bit is clear is UNKNOWN, whatever its +/// value bit holds; the value bit is masked by validity so a stale payload +/// under an UNKNOWN cell is never returned as TRUE. A two-valued register is +/// valid at every selected identity. +pub fn selected_column_k3(r: &BoundDr64<'_>, a: &Admitted, y: u8) -> Option<(u64, u64)> { let sel = a.truth; let col = hhtl16::column(r.rows, y)?; let known = match r.validity { Some(_) => hhtl16::column_validity(r, y)?, None => u64::MAX, }; - Some((col & known & sel, !col & known & sel, !known & sel)) + Some((col & known & sel, known & sel)) } /// One cell `(x, y)`, read only if `x` is selected. `None` outside the diff --git a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs index 093b05aa5..08ce249fb 100644 --- a/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs +++ b/crates/dr-math-binding-probe/tests/dr256_where_dr3.rs @@ -207,10 +207,10 @@ fn keep(res: &Resident, filter: Filter) -> Vec { out } -/// TRUE and FALSE masks of `class = 'employee' AND sel = want` (K3). The TRUE -/// mask comes from Quack's own `Draft::bind`; the FALSE mask from the same -/// leaves under `NOT`, both through `Filter::sql_where`. -fn where_k3(res: &Resident, cb: &Codebook, want: i32) -> (Vec, Vec) { +/// WHERE `class = 'employee' AND sel = want`: the TRUE rows, through Quack's +/// own `Draft::bind` (three-valued over the nullable `sel`), checked against +/// the same filter built by hand. +fn where_k3(res: &Resident, cb: &Codebook, want: i32) -> Vec { let bound = table("node") .where_eq("class", "employee") .where_eq("sel", want) @@ -221,15 +221,28 @@ fn where_k3(res: &Resident, cb: &Codebook, want: i32) -> (Vec, Vec) { Filter::Cmp(SEL, Cmp::EqI32(want)), ]); let nullable = [(SEL, VSEL)]; - let t_direct = Filter::and([Filter::plane(LIVE), raw.clone()]).sql_where(&nullable); - let f = Filter::and([Filter::plane(LIVE), Filter::negate(raw)]).sql_where(&nullable); + let t_direct = Filter::and([Filter::plane(LIVE), raw]).sql_where(&nullable); let t = keep(res, bound.filter); assert_eq!( t, keep(res, t_direct), "Draft::bind and the hand-built filter must agree" ); - (t, keep(res, f)) + t +} + +/// WHERE `NOT (class = 'employee' AND sel = want)`: a second WHERE, evaluated +/// by the same three-valued `sql_where`. `NOT UNKNOWN` stays UNKNOWN, so a +/// NULL row is kept by neither this nor [`where_k3`]. +fn where_not(res: &Resident, cb: &Codebook, want: i32) -> Vec { + let raw = Filter::and([ + Filter::Cmp(CLASS, Cmp::EqU32(cb.encode(EMP))), + Filter::Cmp(SEL, Cmp::EqI32(want)), + ]); + keep( + res, + Filter::and([Filter::plane(LIVE), Filter::negate(raw)]).sql_where(&[(SEL, VSEL)]), + ) } fn bit(m: &[u64], g: u64) -> bool { @@ -427,7 +440,6 @@ fn bind<'a>( fn select( map: &LocalMap, t: &[u64], - f: &[u64], gst: &FrameStore, gseal: &Frame, lst: &FrameStore, @@ -438,7 +450,6 @@ fn select( project( map, t, - f, Under { global_store: gst, global: gseal, @@ -475,14 +486,13 @@ fn global_selection_is_exact_and_only_frame_identities_are_projected() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); // Whole-mask comparison against the oracle, every one of 65,536 addresses. let (mut gt, mut gf, mut gu) = (0u32, 0u32, 0u32); for (g, r) in w.src.iter().enumerate() { let g64 = g as u64; let v = verdict(r, WANT); assert_eq!(bit(&t, g64), v == Some(Some(true)), "TRUE at {g}"); - assert_eq!(bit(&f, g64), v == Some(Some(false)), "FALSE at {g}"); gt += u32::from(v == Some(Some(true))); gf += u32::from(v == Some(Some(false))); gu += u32::from(v == Some(None)); @@ -490,23 +500,14 @@ fn global_selection_is_exact_and_only_frame_identities_are_projected() { let m = maps(&w); let (gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); let (ot, of, ou) = oracle_local(&w.src, &w.emp_ids, WANT); - assert_eq!((a.truth(), a.falsity(), a.unknown()), (ot, of, ou)); + assert_eq!(a.truth(), ot); + // Neither a FALSE nor an UNKNOWN identity is selected. + assert_eq!(a.truth() & (of | ou), 0); assert_eq!(a.slots(), u64::MAX); // Anti-vacuity: all three verdicts occur in the frame, and the global // selection reaches far beyond it. Projection work is the frame, not the @@ -525,7 +526,7 @@ fn equal_local_ordinals_of_two_tables_never_alias() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let gst = global_store(&cb); let seal = gst.seal(); @@ -534,7 +535,6 @@ fn equal_local_ordinals_of_two_tables_never_alias() { let se = select( &m.emp, &t, - &f, &gst, &seal, &lemp, @@ -547,7 +547,6 @@ fn equal_local_ordinals_of_two_tables_never_alias() { let sd = select( &m.dept, &t, - &f, &gst, &seal, &ldept, @@ -563,11 +562,9 @@ fn equal_local_ordinals_of_two_tables_never_alias() { let ae = se.admit(&gst, &lemp, &be, CRITERIA).unwrap(); let ad = sd.admit(&gst, &ldept, &bd, CRITERIA).unwrap(); // The employee selection occupies ordinals the department frame also has; - // projected through the department map it selects no department (every - // department is FALSE for `class = 'employee'`, never UNKNOWN). + // projected through the department map it selects no department. assert_ne!(ae.truth() & ad.slots(), 0); assert_eq!(ad.truth(), 0); - assert_eq!(ad.falsity(), ad.slots()); // An employee selection cannot be read against a department-row register, // even when that register sits in the very frame the selection was made in. let bd_in_emp = bind(&lemp, &ge, dept_attr_sig(), &rd, None); @@ -589,22 +586,11 @@ fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let (gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); @@ -649,65 +635,116 @@ fn selected_identity_by_property_matches_the_oracle_and_survives_rotation() { })); } -// ── 4. NULL / UNKNOWN: never FALSE ──────────────────────────────────────── +// ── 4. NULL / UNKNOWN: NOT UNKNOWN is UNKNOWN ───────────────────────────── + +const NOT_CRITERIA: Criteria = Criteria { id: 0xC1_0001 }; #[test] -fn unknown_stays_unknown_in_selection_negation_and_property() { +fn unknown_is_neither_selected_nor_negated_and_never_read_as_false() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); + // The negation is its own WHERE through Quack's three-valued sql_where. + let tn = where_not(&res, &cb, WANT); + // Globally: the negated WHERE keeps exactly the oracle's FALSE rows, and + // a NULL row is kept by neither WHERE. + let mut gap = 0u32; + for (g, r) in w.src.iter().enumerate() { + let (g64, v) = (g as u64, verdict(r, WANT)); + assert_eq!(bit(&tn, g64), v == Some(Some(false)), "NOT at {g}"); + if v == Some(None) { + assert!(!bit(&t, g64) && !bit(&tn, g64), "UNKNOWN at {g}"); + gap += 1; + } + } + assert!(gap > 1000); let m = maps(&w); let (gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - certified_sig(), - ) - .unwrap(); let (val, known) = certified_planes(&w); let b = bind(&lst, &g, certified_sig(), &val, Some(&known)); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), certified_sig()).unwrap(); let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); - // NOT(selection) is FALSE, not "every slot not TRUE". - assert_ne!(a.unknown(), 0); - assert_eq!(a.falsity() & a.unknown(), 0); - assert_ne!(a.falsity(), a.slots() & !a.truth()); + let under = |criteria| Under { + global_store: &gst, + global: &seal, + local_store: &lst, + guards: &g, + axis: emp_id(), + method: certified_sig(), + criteria, + }; + let neg = project(&m.emp, &tn, under(NOT_CRITERIA)).unwrap(); + let an = neg.admit(&gst, &lst, &b, NOT_CRITERIA).unwrap(); + // A selection is not reusable as its own negation. + assert_eq!( + neg.admit(&gst, &lst, &b, CRITERIA), + Err(ReuseRefusal::CriteriaChanged) + ); + // In the frame: the UNKNOWN slots are in neither selection, so the + // complement of a selection is not its negation. + let (ot, of, ou) = oracle_local(&w.src, &w.emp_ids, WANT); + assert_eq!((a.truth(), an.truth()), (ot, of)); + assert_eq!(a.truth() & an.truth(), 0); + assert_eq!(a.slots() & !(a.truth() | an.truth()), ou); + assert_ne!(ou, 0); + assert_ne!(a.slots() & !a.truth(), an.truth()); // The NULL rows' payload is 1 = WANT, so an engine reading payloads at - // NULL would have kept them: none is TRUE. + // NULL would have kept them: none is selected by either WHERE. for &e in &w.emp_ids { if w.src[e as usize].sel.is_none() { - assert_eq!((a.truth() >> pos(&w.emp_ids, e)) & 1, 0); + let x = pos(&w.emp_ids, e); + assert_eq!((a.truth() | an.truth()) >> x & 1, 0); } } - // Three-valued property over the selected identities, column by column. - let (mut u_cells, mut f_cells) = (0u32, 0u32); - for (y, &s) in w.skills.iter().enumerate() { - let (ct, cf, cu) = selected_column_k3(&b, &a, y as u8).unwrap(); - let (mut et, mut ef, mut eu) = (0u64, 0u64, 0u64); - for &e in &w.emp_ids { - if verdict(&w.src[e as usize], WANT) != Some(Some(true)) { - continue; - } - let bitpos = 1u64 << pos(&w.emp_ids, e); - match w.certified.iter().find(|c| c.0 == e && c.1 == s) { - Some((_, _, Some(true))) => et |= bitpos, - Some((_, _, Some(false))) => ef |= bitpos, - // No fact, or a fact with unknown certification: UNKNOWN. - _ => eu |= bitpos, + // Three-valued property over the selected identities, in the register's + // own value + validity form. + let check = |b: &BoundDr64<'_>| { + let (mut u_cells, mut f_cells) = (0u32, 0u32); + for (y, &s) in w.skills.iter().enumerate() { + let (cv, ck) = selected_column_k3(b, &a, y as u8).unwrap(); + let (mut et, mut ef, mut eu) = (0u64, 0u64, 0u64); + for &e in &w.emp_ids { + if verdict(&w.src[e as usize], WANT) != Some(Some(true)) { + continue; + } + let bitpos = 1u64 << pos(&w.emp_ids, e); + match w.certified.iter().find(|c| c.0 == e && c.1 == s) { + Some((_, _, Some(true))) => et |= bitpos, + Some((_, _, Some(false))) => ef |= bitpos, + // No fact, or a fact with unknown certification: UNKNOWN. + _ => eu |= bitpos, + } } + assert_eq!(cv, et, "TRUE, certified column {s}"); + assert_eq!(ck & !cv, ef, "FALSE, certified column {s}"); + assert_eq!(a.truth() & !ck, eu, "UNKNOWN, certified column {s}"); + u_cells += (a.truth() & !ck).count_ones(); + f_cells += (ck & !cv).count_ones(); } - assert_eq!((ct, cf, cu), (et, ef, eu), "certified column {s}"); - u_cells += cu.count_ones(); - f_cells += cf.count_ones(); - } - assert!(u_cells > 0 && f_cells > 0); + assert!(u_cells > 0 && f_cells > 0); + }; + check(&b); + // A stale payload bit under an UNKNOWN cell of a selected identity is + // never returned as TRUE. + let (x, y) = w + .emp_ids + .iter() + .filter(|&&e| verdict(&w.src[e as usize], WANT) == Some(Some(true))) + .flat_map(|&e| w.skills.iter().map(move |&s| (e, s))) + .find(|&(e, s)| { + !matches!( + w.certified.iter().find(|c| c.0 == e && c.1 == s), + Some((_, _, Some(_))) + ) + }) + .map(|(e, s)| (pos(&w.emp_ids, e), pos(&w.skills, s))) + .unwrap(); + let mut dirty = val; + dirty[x as usize] |= 1 << y; + let bd = bind(&lst, &g, certified_sig(), &dirty, Some(&known)); + check(&bd); // The Boolean folds read payload bits as presence, so they refuse a // selection admitted against this three-valued register. assert_eq!(selected_count(b.rows, &a), None); @@ -722,22 +759,11 @@ fn source_change_after_where_refuses_reuse_and_rebind_matches() { let mut w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let (mut gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); let before = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); @@ -757,12 +783,11 @@ fn source_change_after_where_refuses_reuse_and_rebind_matches() { ); // Rebind: WHERE again, project again, under the new seal. let res2 = resident(&w.src, &cb); - let (t2, f2) = where_k3(&res2, &cb, WANT); + let t2 = where_k3(&res2, &cb, WANT); let seal2 = gst.seal(); let sel2 = select( &m.emp, &t2, - &f2, &gst, &seal2, &lst, @@ -773,10 +798,7 @@ fn source_change_after_where_refuses_reuse_and_rebind_matches() { .unwrap(); let after = sel2.admit(&gst, &lst, &b, CRITERIA).unwrap(); assert_eq!(after.truth(), 0); - assert_eq!( - (after.truth(), after.falsity(), after.unknown()), - oracle_local(&w.src, &w.emp_ids, WANT) - ); + assert_eq!(after.truth(), oracle_local(&w.src, &w.emp_ids, WANT).0); // The silent alternative: the old projection would still answer. assert_ne!( selected_count(b.rows, &before).unwrap(), @@ -791,22 +813,11 @@ fn scope_or_focus_change_refuses_with_identical_coordinates() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let (gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); // Same frame issue, same coordinate numbers, same register bytes. let g_scope = Guards { @@ -839,7 +850,7 @@ fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { let mut w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let gst = global_store(&cb); // One frame over both tables; its coordinates name the employee map, the @@ -851,18 +862,7 @@ fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { }; let mut lst = FrameStore::new(both); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - works_in_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), works_in_sig()).unwrap(); let rw = plane(&w.works_in, &w.emp_ids, &w.dept_ids); let rl = plane(&w.located_at, &w.dept_ids, &w.sites); let bw = bind(&lst, &g, works_in_sig(), &rw, None); @@ -906,18 +906,7 @@ fn fk_projection_over_selection_matches_and_a_changed_reference_refuses() { let rl2 = plane(&w.located_at, &w.dept_ids, &w.sites); let bw2 = bind(&lst, &g2, works_in_sig(), &rw, None); let bl2 = bind(&lst, &g2, located_at_sig(), &rl2, None); - let sel2 = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g2, - emp_id(), - works_in_sig(), - ) - .unwrap(); + let sel2 = select(&m.emp, &t, &gst, &seal, &lst, &g2, emp_id(), works_in_sig()).unwrap(); let a2 = sel2.admit(&gst, &lst, &bw2, CRITERIA).unwrap(); let chain2 = Chain::new(&lst, vec![bw2, bl2]).unwrap(); let (es2, _) = chain2 @@ -939,24 +928,13 @@ fn reseal_and_coordinate_changes_refuse() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let gst = global_store(&cb); let seal = gst.seal(); let mut lst = local_store(&m.emp); let g = guards(&lst, FOCUS, SCOPE); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); let before = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); @@ -985,7 +963,6 @@ fn reseal_and_coordinate_changes_refuse() { select( &m.emp, &t, - &f, &gst, &seal, &lst, @@ -998,18 +975,7 @@ fn reseal_and_coordinate_changes_refuse() { ); // Through the new map it projects, with the bits moved to the new // ordinals. - let sel2 = select( - &map2, - &t, - &f, - &gst, - &seal, - &lst, - &g2, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel2 = select(&map2, &t, &gst, &seal, &lst, &g2, emp_id(), has_skill_sig()).unwrap(); let r2 = plane(&w.has_skill, &reordered, &w.skills); let b2 = bind(&lst, &g2, has_skill_sig(), &r2, None); let a2 = sel2.admit(&gst, &lst, &b2, CRITERIA).unwrap(); @@ -1027,23 +993,12 @@ fn foreign_owner_codebook_criteria_and_schema_refuse() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let mut gst = global_store(&cb); let lst = local_store(&m.emp); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); // Another owner at identical numbers. @@ -1076,15 +1031,14 @@ fn foreign_owner_codebook_criteria_and_schema_refuse() { Err(ReuseRefusal::Global(Refusal::MapChanged)) ); let res2 = resident(&w.src, &cb2); - let (t_stale, _) = where_k3(&res2, &cb, WANT); - let (t_fresh, f_fresh) = where_k3(&res2, &cb2, WANT); + let t_stale = where_k3(&res2, &cb, WANT); + let t_fresh = where_k3(&res2, &cb2, WANT); assert_eq!(t_fresh, t); assert!(t_stale.iter().all(|&x| x == 0)); let seal2 = gst.seal(); let sel2 = select( &m.emp, &t_fresh, - &f_fresh, &gst, &seal2, &lst, @@ -1109,12 +1063,11 @@ fn empty_and_full_global_selections_are_exact() { let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); // Empty: no row has sel = 99. Every frame employee is FALSE or UNKNOWN. - let (t0, f0) = where_k3(&res, &cb, 99); + let t0 = where_k3(&res, &cb, 99); assert!(t0.iter().all(|&x| x == 0)); let s0 = select( &m.emp, &t0, - &f0, &gst, &seal, &lst, @@ -1124,14 +1077,10 @@ fn empty_and_full_global_selections_are_exact() { ) .unwrap(); let a0 = s0.admit(&gst, &lst, &b, CRITERIA).unwrap(); - assert_eq!( - (a0.truth(), a0.falsity(), a0.unknown()), - oracle_local(&w.src, &w.emp_ids, 99) - ); + assert_eq!(a0.truth(), oracle_local(&w.src, &w.emp_ids, 99).0); assert_eq!(selected_count(b.rows, &a0).unwrap(), 0); // Full: the every-address plane. All 65,536 TRUE, every slot selected. let full = keep(&res, Filter::plane(ALL)); - let none = vec![0u64; GLOBAL_WORDS]; assert_eq!( full.iter().map(|w| w.count_ones()).sum::(), GLOBAL as u32 @@ -1139,7 +1088,6 @@ fn empty_and_full_global_selections_are_exact() { let s1 = select( &m.emp, &full, - &none, &gst, &seal, &lst, @@ -1149,7 +1097,7 @@ fn empty_and_full_global_selections_are_exact() { ) .unwrap(); let a1 = s1.admit(&gst, &lst, &b, CRITERIA).unwrap(); - assert_eq!((a1.truth(), a1.falsity(), a1.unknown()), (u64::MAX, 0, 0)); + assert_eq!(a1.truth(), u64::MAX); assert_eq!( selected_count(b.rows, &a1).unwrap() as usize, w.has_skill.len() @@ -1159,7 +1107,6 @@ fn empty_and_full_global_selections_are_exact() { select( &m.emp, &full[..10], - &none, &gst, &seal, &lst, @@ -1170,21 +1117,6 @@ fn empty_and_full_global_selections_are_exact() { .err(), Some(ProjectRefusal::WrongWidth) ); - assert_eq!( - select( - &m.emp, - &full, - &full, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig() - ) - .err(), - Some(ProjectRefusal::NotThreeValued) - ); let far = LocalMap::prepare(&[GLOBAL as u64]).unwrap(); let lfar = local_store(&far); let gfar = guards(&lfar, FOCUS, SCOPE); @@ -1192,7 +1124,6 @@ fn empty_and_full_global_selections_are_exact() { select( &far, &full, - &none, &gst, &seal, &lfar, @@ -1212,7 +1143,7 @@ fn stale_keep_negative_control_is_refused_not_answered() { let mut w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); // The detached Keep: kept outside any guard, then the criteria input // (`sel`) changes on half the selected rows of the whole universe. let detached = t.clone(); @@ -1224,7 +1155,7 @@ fn stale_keep_negative_control_is_refused_not_answered() { } } let res2 = resident(&w.src, &cb); - let (fresh, _) = where_k3(&res2, &cb, WANT); + let fresh = where_k3(&res2, &cb, WANT); let pop = |m: &[u64]| m.iter().map(|x| x.count_ones()).sum::(); // Unguarded, the detached mask answers silently with the old population. assert_eq!(pop(&detached) - pop(&fresh), moved); @@ -1237,7 +1168,6 @@ fn stale_keep_negative_control_is_refused_not_answered() { let sel = select( &m.emp, &detached, - &f, &gst, &seal, &lst, @@ -1264,7 +1194,6 @@ fn stale_keep_negative_control_is_refused_not_answered() { select( &m.emp, &detached, - &f, &gst, &seal2, &lst, @@ -1283,25 +1212,14 @@ fn projection_admission_and_folds_do_not_allocate() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let (gst, lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); let r = plane(&w.has_skill, &w.emp_ids, &w.skills); let b = bind(&lst, &g, has_skill_sig(), &r, None); let before = allocs(); - let sel = select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig(), - ) - .unwrap(); + let sel = select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).unwrap(); let a = sel.admit(&gst, &lst, &b, CRITERIA).unwrap(); let mut acc = selected_count(b.rows, &a).unwrap(); for y in 0..40u8 { @@ -1319,43 +1237,19 @@ fn projection_under_a_stale_global_seal_or_local_frame_is_refused() { let w = world(SEED); let cb = Codebook { shift: 0 }; let res = resident(&w.src, &cb); - let (t, f) = where_k3(&res, &cb, WANT); + let t = where_k3(&res, &cb, WANT); let m = maps(&w); let (mut gst, mut lst) = (global_store(&cb), local_store(&m.emp)); let (seal, g) = (gst.seal(), guards(&lst, FOCUS, SCOPE)); // Silence twin: current seals project. - assert!( - select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig() - ) - .is_ok() - ); + assert!(select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).is_ok()); // The global owner moved between WHERE and projection. gst.advance(FrameRevisions { source: 2, ..gst.revisions() }); assert_eq!( - select( - &m.emp, - &t, - &f, - &gst, - &seal, - &lst, - &g, - emp_id(), - has_skill_sig() - ) - .err(), + select(&m.emp, &t, &gst, &seal, &lst, &g, emp_id(), has_skill_sig()).err(), Some(ProjectRefusal::Global(Refusal::SourceChanged)) ); // Another owner's seal at identical numbers. @@ -1365,7 +1259,6 @@ fn projection_under_a_stale_global_seal_or_local_frame_is_refused() { select( &m.emp, &t, - &f, &other, &seal_now, &lst, @@ -1382,7 +1275,6 @@ fn projection_under_a_stale_global_seal_or_local_frame_is_refused() { select( &m.emp, &t, - &f, &gst, &seal_now, &lst, From 433e7dfd91c1316a6798f60a39c39c412b98e574 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 09:08:30 +0000 Subject: [PATCH 7/7] docs(dr-math): D-DRCA-2 epistemic-absence semantics and re-measured single WHERE README section and board entry rewritten for the single-WHERE contract: UNKNOWN ($null, NaN, NULL, unset validity) is one undecided value, never read as FALSE, no complement offered, negation is its own WHERE, no Epi5 derived from absence. Measured back to back against the previous two-program path on the same fixture: the fresh read halves (41.5-43.2 us to 20.6 us); reuse still pays from N = 2. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../2026-10-28-d-drca-2-dr256-where-dr3.md | 13 ++-- crates/dr-math-binding-probe/README.md | 65 +++++++++---------- 2 files changed, 38 insertions(+), 40 deletions(-) diff --git a/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md index 6a4890e6c..0a416c52f 100644 --- a/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md +++ b/.claude/board/entries/2026-10-28-d-drca-2-dr256-where-dr3.md @@ -4,13 +4,12 @@ ## Result -- A three-valued global WHERE (Quack `Draft::bind` + `Filter::sql_where`, mask-risc `Keep`, 65,536 addresses) projects into a 64-slot DR frame by `map.len()` probes through the counted `LocalMap`. No new predicate evaluator, routing engine or mask store. -- Every read is re-admitted against owner, source, codebook, frame, register frame, axis, DR method, focus, scope and criteria; each refusal is pinned by a test against an independent source-ID oracle. -- UNKNOWN stays apart from FALSE in the selection, its negation and a three-valued property column. -- Projection, admission and folds allocate nothing. Warm read 71–90 ns; fresh read 44–73 µs (WHERE dominates). Warm reuse breaks even at N = 1 and pays from N = 2 (1.96–2.03×), 8.1–8.4× at N = 8; at N = 64 fresh and rebind exceed 1,000 µs (failed gate), warm stays at 46 µs. -- Seventeen disable runs each turn a test red (the Boolean folds refuse a three-valued register, the Codex #1834 finding applied here). The first pass found the projection-time seal checks unpinned; a test was added. -- The #1792 control still reproduces (`reused R2 1032 vs fresh 31`). +- One Quack WHERE (`Draft::bind` + `Filter::sql_where`, mask-risc `Keep`, 65,536 addresses) projects into a 64-slot DR frame by `map.len()` probes through the counted `LocalMap`. No new predicate evaluator, routing engine, mask store or epistemic sidecar. +- Epistemic absence (`$null`, NaN, SQL NULL, unset validity, K3 UNKNOWN) is one logical value. WHERE selects TRUE; the unselected slots are FALSE or UNKNOWN and no complement is offered. A negation is its own WHERE, so `NOT UNKNOWN` stays UNKNOWN. A three-valued property keeps value + validity. No Epi5 state is derived from absence. +- Every read is re-admitted against owner, source, codebook, frame, register frame, axis, DR method (the ClassId-bound `MethodSignature`), focus, scope and criteria; each refusal is pinned by a test against an independent source-ID oracle. +- Projection, admission and folds allocate nothing. Measured back to back on the same fixture, the single WHERE halves the fresh read (41.5–43.2 µs → 20.6 µs). Warm reuse pays from N = 2 (2.0×), 7.9–8.0× at N = 8; at N = 64 fresh and rebind exceed 1,000 µs (failed gate), warm stays at 24–25 µs. +- Sixteen disable runs each turn a test red. The #1792 control still reproduces (`reused R2 1032 vs fresh 31`). ## Open -A detached `Keep` projected under a NEW seal is accepted: the seal attests the caller's claim, not mask provenance (needs a producer-side frame on Quack's bound query, D-NFR S5). `Criteria` is caller-supplied. The FALSE set costs a second WHERE program. One 64-slot frame per table; no DR256 resident register; no scattered-mask reuse. +A detached `Keep` projected under a NEW seal is accepted: the seal attests the caller's claim, not mask provenance (independent gate, D-NFR S5: a producer-side frame on Quack's bound query). `Criteria` is caller-supplied. One 64-slot frame per table; no DR256 resident register; no scattered-mask reuse. diff --git a/crates/dr-math-binding-probe/README.md b/crates/dr-math-binding-probe/README.md index 0a914eb29..b5fddf871 100644 --- a/crates/dr-math-binding-probe/README.md +++ b/crates/dr-math-binding-probe/README.md @@ -70,69 +70,68 @@ Warm reads made 0 global→local lookups. Single host, single run; reported, not Lab test of the composition `global selection → optional amortized global→local mapping → HHTL16 Cartesian projection → native fold`. Module `src/where_dr3.rs`, test `tests/dr256_where_dr3.rs`, costs `examples/dr256_where_stages.rs`. -- **WHERE is Quack's.** `table("node").where_eq("class", "employee").where_eq("sel", 1).bind(..)` (`Draft::bind`, three-valued through `Filter::sql_where`), lowered and executed by mask-risc's `Keep` terminal over 65,536 addresses. The FALSE set is the same leaves under `NOT`, also through `sql_where`. A row in neither is UNKNOWN. The module evaluates no predicate and depends on neither engine: it takes the two `Keep` masks as borrowed words. -- **Global → local.** `project` tests bit `global(l)` of both masks for each local slot of the table's `LocalMap`: `map.len()` probes, never a pass over the universe, no map search. A selected identity outside the frame is not projected. The frame must carry `LocalMap::digest()` as its `coordinates` revision, so a selection cannot be projected through one coordinate assignment and read under another. +- **WHERE is Quack's, once.** `table("node").where_eq("class", "employee").where_eq("sel", 1).bind(..)` (`Draft::bind`, three-valued through `Filter::sql_where`), lowered and executed by mask-risc's `Keep` terminal over 65,536 addresses. Its output, the rows where the criteria are TRUE, is the only selection input. The module evaluates no predicate and depends on neither engine. +- **DT is the existing ClassId-bound schema.** The register's `MethodSignature` (owner `ClassId`, axes, truth, population) is what a selection is projected for and re-admitted against. +- **Global → local.** `project` tests bit `global(l)` of the WHERE mask for each local slot of the table's `LocalMap`: `map.len()` probes, never a pass over the universe, no map search. A selected identity outside the frame is not projected. The frame must carry `LocalMap::digest()` as its `coordinates` revision, so a selection cannot be projected through one coordinate assignment and read under another. - **Admission.** Every read goes through `LocalSelection::admit`, which re-checks the global source seal (owner, source revision, codebook, address space), the local frame, register frame identity, identity axis, DR method, focus, scope and criteria. The only readable form is the `Admitted` it returns. A `LocalSelection` is a caller-owned value; there is no store or cache. - **Folds.** The selection is a `u64` over the identity axis, ANDed into reads of the borrowed rows (`selected_count`, `selected_column`, `selected_column_k3`, `selected_cell`). No Cartesian product, no copied row. -- **K3.** WHERE keeps TRUE. UNKNOWN is carried separately and never folded into FALSE; the negation of a selection is its FALSE set. The Boolean folds read payload bits as presence, so they refuse a selection admitted against a three-valued or bag register (the rule `hhtl16::cooccurrence` and `relcomp::Chain::new` apply); `selected_column_k3` reads validity and serves both. + +**Epistemic absence.** `$null`, NaN, SQL NULL, an unset Arrow validity bit and K3 UNKNOWN are one logical value: no TRUE/FALSE judgment has been established. It does not say the entity or relationship does not exist, and no finer epistemic state (CausalEdge64 Epi5, under its own evidence contract) is derived from it. Consequences here: + +- WHERE selects TRUE. A slot that is not selected is FALSE **or** UNKNOWN, and `Admitted` offers no complement, because the complement of a selection would read UNKNOWN as FALSE. +- `NOT UNKNOWN` is UNKNOWN. A negated selection is a second WHERE over the negated criteria through the same `sql_where`, with its own criteria identity; reusing one selection as the other is refused. +- A three-valued property keeps the register's own value + validity form (`BoundDr64::validity`). `selected_column_k3` returns `(value, validity)` over the selection, with the value masked by validity, so a stale payload under an UNKNOWN cell is never TRUE. The Boolean folds read payload bits as presence and refuse a three-valued or bag register (the rule `hhtl16::cooccurrence` and `relcomp::Chain::new` apply). +- Physical encodings (Quack validity planes, Arrow bitmaps, NaN payloads) are adapter concerns; none adds a semantic category. Oracle: the source is plain Rust values per global address (`class`, `sel: Option`, `live`). Verdicts are a `match` on `Option`, local positions are `position()` in the frame's source-order id list, and registers are built from those positions, not through the map. It shares no code with Quack, mask-risc, `hhtl16` or `where_dr3`. NULL rows carry the payload the predicate tests for, so an engine that read NULL payloads would keep them. Thirteen tests against that oracle: -- the global selection, whole mask over all 65,536 addresses, and its in-frame TRUE / FALSE / UNKNOWN (all three non-empty; most selected identities lie outside the frame); +- the global WHERE, whole mask over all 65,536 addresses, and its in-frame selection (TRUE, FALSE and UNKNOWN all occur in the frame; neither FALSE nor UNKNOWN is selected; most selected identities lie outside the frame); - equal local ordinals of two tables: the employee selection projected through the department map selects no department, and reading it against a department-row register is refused (`AxisMismatch`, `DifferentFrame`); - selected Identity × Property cell by cell, by column and by count, and the same relationships through the YZ rotation; -- UNKNOWN: kept apart from FALSE in the selection, in its negation and in a three-valued property column, and the Boolean folds refuse that three-valued register; +- UNKNOWN: the negated WHERE keeps exactly the oracle's FALSE rows, a NULL row is kept by neither WHERE (globally and in the frame), the complement of a selection differs from its negation, one selection is refused as the other, the three-valued column matches the oracle in value + validity form including with a stale payload under an UNKNOWN cell, and the Boolean folds refuse that register; - a source change after WHERE (refused, then rebound to the oracle); - a scope or focus change with identical coordinates (refused; the unchanged register admits); - selected employees' sites through a witnessed FK (`Chain`), then a changed referenced property (refused, rebound); - a reseal at equal numbers and a new coordinate assignment (refused; the old map is refused under the new frame, and the new map projects to the new ordinals); - a foreign owner at equal numbers, other criteria, another DR method, and a new codebook (refused; the stale binding run silently keeps nobody); -- empty and full selections, plus malformed widths, TRUE ∧ FALSE overlap and an id outside the universe; +- empty and full selections, plus a malformed width and an id outside the universe; - the #1792 shape: a detached `Keep` reused after its criteria input changed answers silently with the old population; projected under the old seal it is refused; - projection under a stale global seal, a foreign owner's seal or a resealed local frame; - projection, admission and folds allocate nothing. -Disable runs, each restored from the commit and each turning at least one test red: the two projection-time seal checks, `MapNotFrame`, the TRUE ∧ FALSE check, TRUE/FALSE swapped, the eight admission guards (global, local, frame issue, axis, method, focus, scope, criteria), UNKNOWN computed as "not TRUE", the three-valued column reporting UNKNOWN as FALSE, `selected_count` ignoring the selection, and the Boolean folds accepting a three-valued register. The first pass found the two projection-time seal checks covered by no test; the projection test above was added for them and both now go red. +Sixteen disable runs, each restored from the commit and each turning at least one test red: the two projection-time seal checks, `MapNotFrame`, the complement projected as the selection, the eight admission guards (global, local, frame issue, axis, method, focus, scope, criteria), the three-valued column reporting UNKNOWN as known, its value not masked by validity, `selected_count` ignoring the selection, and the Boolean folds accepting a three-valued register. The original #1792 control is unchanged and still reproduces: `cargo run --release --example p2_quack_where -- --controls` in `crates/drf-focus-probe` prints `reused R2 1032 vs fresh 31`. -`cargo run --release --example dr256_where_stages` on a 4-vCPU shared Xeon @ 2.10 GHz (avx512f), median of 21 runs, two runs. Per-op rows below are batched over 40–256 calls where a single call is below timer resolution. +`cargo run --release --example dr256_where_stages` on a 4-vCPU shared Xeon @ 2.10 GHz (avx512f), median of 21 runs. The single-WHERE path was measured back to back against the previous two-program path (TRUE and FALSE `Keep`, commit `cbc7930`) on the same fixture, alternating old/new three times; the two quiet pairs are shown (the third pair was disturbed by host load in both arms). -| stage | run 1 | run 2 | allocs | +| stage | previous (two WHERE programs) | single WHERE | allocs | |---|---|---|---| -| cold: encode 65,536 source rows into planes and lanes (fixture) | 409 µs | — | 5 | -| cold: `LocalMap::prepare` (64 ids) | 642 ns | — | 3 | -| cold: `FrameStore::new` + seal | 786 ns | — | 2 | -| `Draft::bind` | 308 ns | — | 10 | -| `lower` | 318 ns | — | 7 | -| WHERE TRUE + FALSE `Keep`, 65,536 rows (lowered once) | 42.2 µs | 70.5 µs | 0 | -| `project` (64 probes) | 1,023 ns | 1,028 ns | 0 | -| `admit` | 65.8 ns | 80.1 ns | 0 | -| warm read (`admit` + `selected_count`) | 70.7 ns | 89.9 ns | 0 | -| rotated cell read, selection applied | 10.7 ns | 9.6 ns | 0 | -| `selected_count` | 13.2 ns | 30.3 ns | 0 | -| `selected_column` | 15.0 ns | 16.6 ns | 0 | -| end-to-end fresh read | 44.3 µs | 73.3 µs | 0 | - -Totals for N compatible reads (µs; fresh = WHERE + project + admit + read each time; warm = WHERE + project once, then admit + read; rebind = the owner advances before every read, the old selection is refused, then WHERE + project + admit + read): +| WHERE `Keep`, 65,536 rows | 41.7 / 40.2 µs | 20.1 / 20.0 µs | 0 | +| end-to-end fresh read | 43.2 / 41.5 µs | 20.6 / 20.6 µs | 0 | +| warm total, N = 8 | 42.9 / 42.4 µs | 21.4 / 21.0 µs | 0 | + +Other stages of the single-WHERE path (two runs): `Draft::bind` 465–513 ns (10 allocs), `lower` 472–482 ns (7 allocs), `project` 912–926 ns, `admit` 76–82 ns, warm read 84–91 ns, `selected_count` 14–16 ns, all 0 allocs. Cold: `LocalMap::prepare` 891–963 ns (3 allocs); encoding the 65,536-row fixture into planes and lanes ~600 µs (fixture, once). + +Totals for N compatible reads, single WHERE (µs, quiet pairs; fresh = WHERE + project + admit + read each time; warm = WHERE + project once, then admit + read; rebind = the owner advances before every read, the old selection is refused, then WHERE + project + admit + read): | N | fresh | warm | rebind | fresh / warm | |---|---|---|---|---| -| 1 | 41.6 / 72.3 | 42.9 / 70.2 | 42.1 / 70.3 | 0.97 / 1.03 | -| 2 | 85.9 / 142.4 | 43.8 / 70.0 | 86.5 / 140.8 | 1.96 / 2.03 | -| 4 | 173.0 / 281.9 | 41.9 / 69.8 | 168.9 / 289.2 | 4.13 / 4.04 | -| 8 | 347.9 / 586.3 | 43.0 / 69.7 | 340.5 / 589.6 | 8.10 / 8.41 | -| 64 | exceeds 1,000 µs (failed gate) | 45.9 / 45.6 | exceeds 1,000 µs (failed gate) | — | +| 1 | 20.7 / 21.1 | 20.6 / 20.7 | 20.8 / 21.1 | 1.00 / 1.02 | +| 2 | 42.4 / 42.4 | 21.1 / 20.6 | 41.3 / 41.2 | 2.01 / 2.05 | +| 4 | 83.2 / 80.1 | 21.0 / 20.1 | 85.7 / 81.7 | 3.96 / 3.99 | +| 8 | 170.8 / 165.1 | 21.4 / 21.0 | 169.4 / 168.6 | 7.96 / 7.86 | +| 64 | exceeds 1,000 µs (failed gate) | 25.2 / 24.1 | exceeds 1,000 µs (failed gate) | — | -Warm reuse breaks even at N = 1 and pays from N = 2. At N = 64 only warm reuse stays inside the fold budget. Rebind costs the same as fresh: invalidation is a cheap refusal followed by the full work. Absolute numbers move by up to 1.7× between runs on this shared host; only ratios within a run are used. These are microbenchmarks, reported, not gates. +One WHERE halves the fresh read. Warm reuse breaks even at N = 1 and pays from N = 2; at N = 64 only warm reuse stays inside the fold budget. Rebind costs the same as fresh. Microbenchmarks, reported, not gates. **Open limitations.** -- **The seal attests the caller's claim, not the mask's provenance.** A detached `Keep` projected under a new seal after its source changed is accepted (pinned by the #1792-shape test, so a fix turns it red). Closing this needs the producer to bind a mask to the seal it was computed under; Quack's bound `Query` has no frame today (D-NFR S5). +- **The seal attests the caller's claim, not the mask's provenance** (independent gate, D-NFR S5). A detached `Keep` projected under a new seal after its source changed is accepted (pinned by the #1792-shape test, so a fix turns it red). Closing it needs the producer to bind a mask to the seal it was computed under; Quack's bound `Query` has no frame today. - `Criteria` is a caller-supplied id; Quack exposes no digest of a bound query. - The global codebook revision rides in `FrameRevisions::relation_map`; the owner, ACL and scope are the lab `FrameStore`, `Scope { id }` equality. -- The FALSE set costs a second WHERE program. A terminal producing both K3 masks in one pass is not built. +- A negated selection costs its own WHERE, which is the price of `NOT UNKNOWN` staying UNKNOWN. - One 64-slot frame per table; no larger focus, no DR256 resident register, no reuse of a scattered (`ScatterOrU32`) mask. -- `project` is 64 scalar probes (~1 µs); admission (~65–80 ns) is not broken down. +- `project` is 64 scalar probes (~1 µs); admission (~76–82 ns) is not broken down.