From 039fc8564b58c4daee938a39b5913953dcd9d4b1 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 00:02:39 +0000 Subject: [PATCH 1/4] lab: D-DRISA-1 register-file probe over borrowed SoA planes Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- Cargo.toml | 5 + crates/drisa-register-probe/Cargo.toml | 21 + .../examples/drisa_bench.rs | 172 ++++ crates/drisa-register-probe/src/lib.rs | 747 ++++++++++++++++++ .../tests/integration/main.rs | 1 + .../tests/integration/register.rs | 485 ++++++++++++ 6 files changed, 1431 insertions(+) create mode 100644 crates/drisa-register-probe/Cargo.toml create mode 100644 crates/drisa-register-probe/examples/drisa_bench.rs create mode 100644 crates/drisa-register-probe/src/lib.rs create mode 100644 crates/drisa-register-probe/tests/integration/main.rs create mode 100644 crates/drisa-register-probe/tests/integration/register.rs diff --git a/Cargo.toml b/Cargo.toml index 5671bfc59..595db49ce 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -232,6 +232,11 @@ exclude = [ # lance-graph-dt64 and the contract only. Verify via # `cargo test --manifest-path crates/dt64-admission-probe/Cargo.toml`. "crates/dt64-admission-probe", + # D-DRISA-1 (EXO-153) LAB: a sealed DR frame read as a register file over + # borrowed SoA planes. Own workspace root; path-deps dt64, mask-risc and + # the contract only. Verify via + # `cargo test --manifest-path crates/drisa-register-probe/Cargo.toml`. + "crates/drisa-register-probe", ] resolver = "2" diff --git a/crates/drisa-register-probe/Cargo.toml b/crates/drisa-register-probe/Cargo.toml new file mode 100644 index 000000000..bcb2248c4 --- /dev/null +++ b/crates/drisa-register-probe/Cargo.toml @@ -0,0 +1,21 @@ +# D-DRISA-1 (EXO-153) LAB: a witnessed DR frame read as a logical register +# file over borrowed canonical SoA planes. NOT a workspace member, nothing +# depends on it, no public contract. Verify with +# cargo test --manifest-path crates/drisa-register-probe/Cargo.toml +# cargo run --release --manifest-path crates/drisa-register-probe/Cargo.toml --example drisa_bench +[package] +name = "drisa-register-probe" +version = "0.0.0" +edition = "2021" +publish = false +license = "MIT OR Apache-2.0" +description = "D-DRISA-1 lab: does a sealed DR frame bind typed register operands to borrowed SoA planes, reused across operations without rerouting, copying payload, or answering stale?" + +# Own workspace root, like the other lab probes. +[workspace] + +[dependencies] +# Consumed read-only through their public APIs; none is changed. +lance-graph-dt64 = { path = "../lance-graph-dt64" } +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } +lance-graph-contract = { path = "../lance-graph-contract" } diff --git a/crates/drisa-register-probe/examples/drisa_bench.rs b/crates/drisa-register-probe/examples/drisa_bench.rs new file mode 100644 index 000000000..db71fa169 --- /dev/null +++ b/crates/drisa-register-probe/examples/drisa_bench.rs @@ -0,0 +1,172 @@ +//! D-DRISA-1 bench: the same methods over the same canonical SoA, three ways. +//! +//! - A `direct`: planes assembled by the caller from the SoA and a selection +//! mask it already holds; no register checks. +//! - B `bind each`: every query binds a register file (routes the selection's +//! global ids through the DR maps, checks frame/source/layout/fields), +//! compiles the method and runs it. +//! - C `bind once`: one register file, methods compiled once; each query +//! revalidates (frame, scope, source, layout digests, value witness) and +//! runs. +//! +//! Per query: wall time (µs), heap allocations and global → local lookups. +//! A counting allocator wraps the system one; it counts calls, not bytes. +//! +//! Run: cargo run --release --manifest-path crates/drisa-register-probe/Cargo.toml --example drisa_bench + +use std::alloc::{GlobalAlloc, Layout, System}; +use std::hint::black_box; +use std::sync::atomic::{AtomicU64, Ordering}; +use std::time::Instant; + +use drisa_register_probe::{ + build_soa, build_table, lookups, run_direct, Checks, Fixture, MethodOp, RegisterFile, +}; +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_dt64::dr::{Scope, Width}; +use lance_graph_dt64::ValueDemand; +use lance_graph_mask_risc::Value; + +struct Counting; +static ALLOCS: AtomicU64 = AtomicU64::new(0); +unsafe impl GlobalAlloc for Counting { + unsafe fn alloc(&self, l: Layout) -> *mut u8 { + ALLOCS.fetch_add(1, Ordering::Relaxed); + unsafe { System.alloc(l) } + } + unsafe fn dealloc(&self, p: *mut u8, l: Layout) { + unsafe { System.dealloc(p, l) } + } +} +#[global_allocator] +static GLOBAL: Counting = Counting; + +const FIELDS: usize = 64; +const DEMANDED: [u8; 3] = [5, 17, 42]; +const SCOPE: Scope = Scope { id: 7 }; +const OPS: [MethodOp; 4] = [ + MethodOp::Count, + MethodOp::Exists, + MethodOp::CountWhereGt { field: 17, t: -5 }, + MethodOp::SumWhereGt { + field: 17, + t: -5, + sum: 42, + }, +]; + +fn median(mut v: Vec) -> f64 { + v.sort_by(|a, b| a.partial_cmp(b).unwrap()); + v[v.len() / 2] +} + +fn main() { + println!("D-DRISA-1: same methods, same SoA. Per query (one of 4 methods, round robin), median of 9 trials."); + println!( + "{:<22} {:>4} {:>11} {:>11} {:>11} {:>9} {:>9} {:>9}", + "fixture", "Q", "A direct", "B bind/q", "C bind 1x", "allocs B", "allocs C", "lkup B/q" + ); + for (name, n, width) in [ + ("DR64, 1 tile", 64usize, Width::W64), + ("DR256, 1 tile", 256, Width::W256), + ("DR256, 256 tiles", 65_536, Width::W256), + ] { + let fixture = Fixture::new(n, FIELDS, 31); + let (table, tiles) = build_table(&fixture, width, 1, 77); + let soa = build_soa(&fixture, &table, &tiles, width); + let selection: Vec = fixture.ids().into_iter().step_by(10).collect(); + let auth = WideFieldMask::from_positions(&DEMANDED); + let bind = || { + RegisterFile::bind( + &table, + &table.seal(), + &tiles, + width, + SCOPE, + FIELDS, + &auth, + &DEMANDED, + ValueDemand::Values, + &selection, + &soa, + Checks::ALL, + ) + .unwrap() + }; + let once = bind(); + let compiled: Vec<_> = OPS.iter().map(|&op| once.compile(op).unwrap()).collect(); + let mut scratch: Vec<_> = compiled.iter().map(|c| once.scratch(c).unwrap()).collect(); + let sel_words = once.selection().to_vec(); + // Parity once per fixture: all three arms give the same answers. + for (i, c) in compiled.iter().enumerate() { + let a = run_direct(c.program(), &soa, &sel_words, &DEMANDED, &mut scratch[i]).unwrap(); + let c_ = once.run(&table, &soa, SCOPE, c, &mut scratch[i]).unwrap(); + let fresh = bind(); + let cb = fresh.compile(OPS[i]).unwrap(); + let mut sb = fresh.scratch(&cb).unwrap(); + let b = fresh.run(&table, &soa, SCOPE, &cb, &mut sb).unwrap(); + assert!(a == c_ && b == c_, "{name} {:?}", OPS[i]); + assert!(!matches!(c_, Value::Count(0)), "non-vacuous"); + } + for q in [1usize, 2, 8, 16, 64, 256] { + let (mut ta, mut tb, mut tc) = (vec![], vec![], vec![]); + let (mut ab, mut ac, mut lb) = (0u64, 0u64, 0u64); + for _ in 0..9 { + let t = Instant::now(); + for k in 0..q { + let i = k % OPS.len(); + black_box( + run_direct( + compiled[i].program(), + &soa, + &sel_words, + &DEMANDED, + &mut scratch[i], + ) + .unwrap(), + ); + } + ta.push(t.elapsed().as_nanos() as f64 / q as f64 / 1000.0); + + let l0 = lookups(&table, &tiles); + let a0 = ALLOCS.load(Ordering::Relaxed); + let t = Instant::now(); + for k in 0..q { + let i = k % OPS.len(); + let f = bind(); + let c = f.compile(OPS[i]).unwrap(); + let mut s = f.scratch(&c).unwrap(); + black_box(f.run(&table, &soa, SCOPE, &c, &mut s).unwrap()); + } + let dt = t.elapsed().as_nanos() as f64 / q as f64 / 1000.0; + ab = (ALLOCS.load(Ordering::Relaxed) - a0) / q as u64; + tb.push(dt); + lb = (lookups(&table, &tiles) - l0) / q as u64; + + let a0 = ALLOCS.load(Ordering::Relaxed); + let t = Instant::now(); + for k in 0..q { + let i = k % OPS.len(); + black_box( + once.run(&table, &soa, SCOPE, &compiled[i], &mut scratch[i]) + .unwrap(), + ); + } + let dt = t.elapsed().as_nanos() as f64 / q as f64 / 1000.0; + ac = (ALLOCS.load(Ordering::Relaxed) - a0) / q as u64; + tc.push(dt); + } + println!( + "{name:<22} {q:>4} {:>9.3}µs {:>9.3}µs {:>9.3}µs {ab:>9} {ac:>9} {lb:>9}", + median(ta), + median(tb), + median(tc) + ); + } + println!( + "{name:<22} register file owns {} B (selection register); SoA holds {} B of values", + once.owned_bytes(), + soa.n_rows() * FIELDS * 4 + ); + } +} diff --git a/crates/drisa-register-probe/src/lib.rs b/crates/drisa-register-probe/src/lib.rs new file mode 100644 index 000000000..7c38535e8 --- /dev/null +++ b/crates/drisa-register-probe/src/lib.rs @@ -0,0 +1,747 @@ +//! D-DRISA-1 (EXO-153): a sealed DR frame read as a logical register file over +//! borrowed canonical SoA planes. LAB ONLY: no public contract, no new store, +//! no transport, no change to `dt64`, `mask-risc` or the contract. +//! +//! The question under test is whether a witnessed DR frame can play the role +//! of a register file: typed operands name coordinates (a frame, its tiles, +//! a field position, an identity selection), and are resolved to borrowed +//! slices of the canonical SoA only when an instruction executes. +//! +//! What this crate owns, and nothing more: +//! - [`Soa`]: a stand-in for the canonical owner of the values. It records +//! which source it is, its value revision, and the coordinate assignment +//! its rows are laid out under (the per-tile map digests of the frame it +//! was built from). +//! - [`RegisterFile`]: a DESCRIPTOR. It holds a frame, the tile digests it was +//! bound under, a scope, the demanded field positions, the value revision +//! (only if values were demanded) and one map-only register: the identity +//! selection, routed from global ids once. It holds no reference into the +//! SoA and no copy of any value. +//! - [`MethodOp`]: a typed method over registers, compiled once to an +//! unchanged `mask-risc` [`Program`]. +//! +//! Execution resolves the operands into [`Planes`] that BORROW the SoA's own +//! slices, then calls `lance_graph_mask_risc::execute`. There is no ALU here. +//! +//! The selection register is the one owned buffer (one bit per row). It is a +//! map-only derived value: it depends on the frame and the tile digests, never +//! on field values, so a value write leaves it valid while a value-dependent +//! method must refuse until its value witness is re-taken. + +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_dt64::dr::{ + Frame, FrameRevisions, LocalMap, MapRead, MapTable, Scope, TileId, Width, +}; +use lance_graph_dt64::ValueDemand; +use lance_graph_mask_risc::{ + execute, execute_into, ExecError, Foreign, LaneRef, MaskOp, Operand, Out, Planes, Pred, + Program, Scratch, Terminal, Value, +}; + +/// Every way a register operand can be invalid. A refusal is always typed: +/// no path returns an empty result or zero in place of a refusal. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Refusal { + /// The frame is not the table's current seal. `then` and `now` are the + /// revisions, reported, never used as identity. + StaleFrame { + then: FrameRevisions, + now: FrameRevisions, + }, + /// The table could not read a tile under the frame. + Map(MapRead), + /// The SoA belongs to another source than the frame's. + SourceMismatch { frame: u64, soa: u64 }, + /// The SoA's rows are laid out under a different coordinate assignment + /// than the one the register was bound under (a permuted or foreign map). + CoordinateMismatch { tile: TileId }, + /// The reader's scope is not the one the register was bound for. + ScopeChanged, + /// A field position past the class basis. + UnknownField(u8), + /// A field position the scope does not authorize. + Unauthorized(u8), + /// A method names a field the register file did not bind. + FieldNotBound(u8), + /// A selection names a global id no bound tile holds. + UnmappedIdentity(u64), + /// A selection names a global id twice. + DuplicateIdentity(u64), + /// A value-dependent method, but values were not demanded at bind. + ValuesNotBound, + /// The SoA's values changed since the register took its value witness. + StaleValues { bound: u64, now: u64 }, + /// A method reads the derived register, but none was derived. + NoDerivedRegister, + /// `mask-risc` refused the program. + Exec(ExecError), +} + +/// The canonical owner's values: one row per DR position, tile-major +/// (`row = tile_ordinal * width + local`). Not part of the register file. +#[derive(Debug)] +pub struct Soa { + source: u64, + revision: u64, + width: Width, + layout: Vec<(TileId, u64)>, + n_rows: usize, + presence: Vec, + fields: Vec>, +} + +impl Soa { + pub fn n_rows(&self) -> usize { + self.n_rows + } + + pub fn revision(&self) -> u64 { + self.revision + } + + pub fn field_count(&self) -> usize { + self.fields.len() + } + + /// The address of a field lane: lets a test show the executed planes + /// borrow these exact bytes. + pub fn field_ptr(&self, field: u8) -> *const i32 { + self.fields[usize::from(field)].as_ptr() + } + + pub fn presence_ptr(&self) -> *const u64 { + self.presence.as_ptr() + } + + /// Write one value by row. Any write bumps the value revision. + pub fn write(&mut self, row: usize, field: u8, value: i32) { + self.fields[usize::from(field)][row] = value; + self.revision += 1; + } + + /// The row of `global` under `table`'s current frame, by the same layout + /// rule the SoA was built with. For writes in tests only. + pub fn row_of(&self, table: &MapTable, global: u64) -> Option { + let frame = table.seal(); + let w = self.width.positions(); + for (ordinal, (tile, _)) in self.layout.iter().enumerate() { + let map = table.map(&frame, *tile).ok()?; + if let Ok(local) = map.local(global) { + return Some(ordinal * w + usize::from(local)); + } + } + None + } +} + +/// Independent truth: identities and their values, keyed by global id. The +/// oracle reads only this, never a map, a position or a register. +#[derive(Debug, Clone)] +pub struct Fixture { + /// `(global, present, values)`; absent identities have no row data. + pub rows: Vec<(u64, bool, Vec)>, + pub field_count: usize, +} + +fn splitmix(mut z: u64) -> u64 { + z = z.wrapping_add(0x9E37_79B9_7F4A_7C15); + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) +} + +impl Fixture { + /// `n` identities with pseudo-random ids, ~90% present, values in + /// `-100..100` derived from (id, field). + pub fn new(n: usize, field_count: usize, seed: u64) -> Fixture { + let rows = (0..n) + .map(|i| { + let id = splitmix(seed ^ (i as u64).wrapping_mul(0xA24B_AED4_963E_E407)); + let present = !splitmix(id ^ 0x55).is_multiple_of(10); + let values = (0..field_count) + .map(|f| { + (splitmix(id ^ (f as u64 + 1).wrapping_mul(0x9E37)) % 200) as i32 - 100 + }) + .collect(); + (id, present, values) + }) + .collect(); + Fixture { rows, field_count } + } + + fn get(&self, global: u64) -> Option<&(u64, bool, Vec)> { + self.rows.iter().find(|r| r.0 == global) + } + + /// Oracle: present identities among `selection`. + pub fn count(&self, selection: &[u64]) -> usize { + let index: std::collections::BTreeMap = self + .rows + .iter() + .enumerate() + .map(|(i, r)| (r.0, i)) + .collect(); + selection + .iter() + .filter(|g| index.get(g).is_some_and(|&i| self.rows[i].1)) + .count() + } + + /// Oracle: present identities among `selection` with `field > t`, and the + /// sum of `sum_field` over them. + pub fn where_gt(&self, selection: &[u64], field: u8, t: i32, sum_field: u8) -> (usize, i64) { + let index: std::collections::BTreeMap = self + .rows + .iter() + .enumerate() + .map(|(i, r)| (r.0, i)) + .collect(); + let mut n = 0; + let mut s = 0i64; + for g in selection { + if let Some(&i) = index.get(g) { + let r = &self.rows[i]; + if r.1 && r.2[usize::from(field)] > t { + n += 1; + s += i64::from(r.2[usize::from(sum_field)]); + } + } + } + (n, s) + } + + /// Apply a value write to the truth (mirrors [`Soa::write`]). + pub fn set(&mut self, global: u64, field: u8, value: i32) { + if let Some(r) = self.rows.iter_mut().find(|r| r.0 == global) { + r.2[usize::from(field)] = value; + } + } + + pub fn ids(&self) -> Vec { + self.rows.iter().map(|r| r.0).collect() + } + + #[doc(hidden)] + pub fn present(&self, global: u64) -> bool { + self.get(global).is_some_and(|r| r.1) + } +} + +/// Lay the fixture's identities out over `tiles` tiles of `width`, each tile's +/// local order permuted by `perm_seed`, and append the maps to a fresh table. +pub fn build_table( + fixture: &Fixture, + width: Width, + source: u64, + perm_seed: u64, +) -> (MapTable, Vec) { + let w = width.positions(); + let ids = fixture.ids(); + let mut table = MapTable::new(source, 1); + let mut changes = Vec::new(); + let mut tiles = Vec::new(); + for (t, chunk) in ids.chunks(w).enumerate() { + let mut order: Vec = chunk.to_vec(); + // Fisher-Yates by a seeded stream: the local order is not the id order. + let mut r = perm_seed ^ (t as u64); + for i in (1..order.len()).rev() { + r = splitmix(r); + order.swap(i, (r % (i as u64 + 1)) as usize); + } + let tile = 1000 + t as TileId; + changes.push(( + tile, + Some(LocalMap::prepare(width, &order).expect("fits the tile")), + )); + tiles.push(tile); + } + table.advance(source, 1, changes); + (table, tiles) +} + +/// Build the canonical SoA for `fixture` under `table`'s current frame. +pub fn build_soa(fixture: &Fixture, table: &MapTable, tiles: &[TileId], width: Width) -> Soa { + let frame = table.seal(); + let w = width.positions(); + let n_rows = tiles.len() * w; + let mut presence = vec![0u64; n_rows.div_ceil(64)]; + let mut fields = vec![vec![0i32; n_rows]; fixture.field_count]; + let mut layout = Vec::new(); + for (ordinal, &tile) in tiles.iter().enumerate() { + let map = table.map(&frame, tile).expect("tile in table"); + layout.push((tile, map.digest())); + for (local, &g) in map.globals().iter().enumerate() { + // An id the fixture does not hold is mapped but absent: it has a + // position and no row data. + let Some((_, present, values)) = fixture.get(g) else { + continue; + }; + let row = ordinal * w + local; + if *present { + presence[row / 64] |= 1 << (row % 64); + for (f, v) in values.iter().enumerate() { + fields[f][row] = *v; + } + } + } + } + Soa { + source: table.revisions().source, + revision: 0, + width, + layout, + n_rows, + presence, + fields, + } +} + +/// Global → local lookups served by every tile map of `table` (DR's own +/// counter): the routing cost a register file is meant to pay once. +pub fn lookups(table: &MapTable, tiles: &[TileId]) -> u64 { + let frame = table.seal(); + tiles + .iter() + .filter_map(|&t| table.map(&frame, t).ok()) + .map(|m| m.lookups()) + .sum() +} + +/// Which checks a register file runs. All on by default; a lab disable run +/// switches exactly one off to show the oracle or a refusal test turns red. +#[derive(Debug, Clone, Copy)] +pub struct Checks { + pub frame: bool, + pub coordinates: bool, + pub values: bool, + pub scope: bool, + pub presence: bool, +} + +impl Checks { + pub const ALL: Checks = Checks { + frame: true, + coordinates: true, + values: true, + scope: true, + presence: true, + }; +} + +/// The register file: a descriptor over a sealed frame. See the crate docs. +#[derive(Debug)] +pub struct RegisterFile { + frame: Frame, + width: Width, + tiles: Vec<(TileId, u64)>, + scope: Scope, + source: u64, + /// Demanded field positions; lane `i` of the executed planes is + /// `demanded[i]`. + demanded: Vec, + value_rev: Option, + /// The map-only identity selection register, one bit per row. + selection: Vec, + /// A derived, value-dependent predicate register: `(value revision it was + /// computed at, mask)`. Valid only while the SoA is at that revision. + derived: Option<(u64, Vec)>, + n_rows: usize, + checks: Checks, +} + +/// A typed method over the register file. It names field positions and +/// constants; it never names a row, a value or a reconstructed object. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum MethodOp { + /// How many selected identities are present. + Count, + /// Whether any selected identity is present. + Exists, + /// How many selected, present identities have `field > t`. + CountWhereGt { field: u8, t: i32 }, + /// Σ `sum` over selected, present identities with `field > t`. + SumWhereGt { field: u8, t: i32, sum: u8 }, + /// Count of the derived predicate register (see + /// [`RegisterFile::derive_gt`]): reads no lane, but the register itself + /// was computed from values, so it is value-scoped. + CountDerived, +} + +impl MethodOp { + pub fn demand(self) -> ValueDemand { + match self { + MethodOp::Count | MethodOp::Exists => ValueDemand::MapOnly, + MethodOp::CountWhereGt { .. } + | MethodOp::SumWhereGt { .. } + | MethodOp::CountDerived => ValueDemand::Values, + } + } +} + +/// A method compiled against one register file: an unchanged `mask-risc` +/// program plus the demand it was compiled for. +#[derive(Debug, Clone)] +pub struct Compiled { + program: Program, + demand: ValueDemand, + /// Reads the derived predicate register (plane 2). + derived: bool, +} + +impl RegisterFile { + /// Bind registers under `frame`. + /// + /// `class_fields` is the class basis size, `authorized` the scope's field + /// mask, `demanded` the fields the methods will read. The selection is + /// routed here, once: every id is located in exactly one bound tile. + #[allow(clippy::too_many_arguments)] + pub fn bind( + table: &MapTable, + frame: &Frame, + tiles: &[TileId], + width: Width, + scope: Scope, + class_fields: usize, + authorized: &WideFieldMask, + demanded: &[u8], + demand: ValueDemand, + selection_ids: &[u64], + soa: &Soa, + checks: Checks, + ) -> Result { + current(table, frame)?; + let mut bound = Vec::with_capacity(tiles.len()); + for &tile in tiles { + let map = table.map(frame, tile).map_err(Refusal::Map)?; + bound.push((tile, map.digest())); + } + for &f in demanded { + if usize::from(f) >= class_fields { + return Err(Refusal::UnknownField(f)); + } + if !authorized.has(f) { + return Err(Refusal::Unauthorized(f)); + } + } + let w = width.positions(); + let n_rows = tiles.len() * w; + let mut selection = vec![0u64; n_rows.div_ceil(64)]; + let maps: Vec<_> = tiles + .iter() + .map(|&t| table.map(frame, t).map_err(Refusal::Map)) + .collect::>()?; + for &g in selection_ids { + let mut row = None; + for (ordinal, map) in maps.iter().enumerate() { + if let Ok(local) = map.local(g) { + row = Some(ordinal * w + usize::from(local)); + break; + } + } + let row = row.ok_or(Refusal::UnmappedIdentity(g))?; + let bit = 1u64 << (row % 64); + if selection[row / 64] & bit != 0 { + return Err(Refusal::DuplicateIdentity(g)); + } + selection[row / 64] |= bit; + } + let file = RegisterFile { + frame: frame.clone(), + width, + tiles: bound, + scope, + source: table.revisions().source, + demanded: demanded.to_vec(), + value_rev: None, + selection, + derived: None, + n_rows, + checks, + }; + file.check_soa(soa)?; + Ok(RegisterFile { + value_rev: matches!(demand, ValueDemand::Values).then_some(soa.revision), + ..file + }) + } + + /// Re-take the value witness without re-routing anything: the selection + /// register and the tile digests are kept as they are. + pub fn rebind_values(&mut self, table: &MapTable, soa: &Soa) -> Result<(), Refusal> { + if self.checks.frame { + current(table, &self.frame)?; + } + self.check_soa(soa)?; + self.value_rev = Some(soa.revision); + Ok(()) + } + + fn check_soa(&self, soa: &Soa) -> Result<(), Refusal> { + if soa.source != self.source { + return Err(Refusal::SourceMismatch { + frame: self.source, + soa: soa.source, + }); + } + if self.checks.coordinates { + if soa.width != self.width || soa.layout.len() != self.tiles.len() { + return Err(Refusal::CoordinateMismatch { + tile: self.tiles.first().map_or(0, |t| t.0), + }); + } + for (have, want) in soa.layout.iter().zip(&self.tiles) { + if have != want { + return Err(Refusal::CoordinateMismatch { tile: want.0 }); + } + } + } + Ok(()) + } + + /// Compile a method against this register file: field positions resolve + /// to lane indices once, here. + pub fn compile(&self, op: MethodOp) -> Result { + let lane = |f: u8| -> Result { + self.demanded + .iter() + .position(|&d| d == f) + .map(|i| i as u16) + .ok_or(Refusal::FieldNotBound(f)) + }; + let sel = if self.checks.presence { + MaskOp::And { + a: Operand::Plane(0), + b: Operand::Plane(1), + dst: 0, + } + } else { + // Disable run only: the selection without the presence plane. + MaskOp::Or { + a: Operand::Plane(1), + b: Operand::Plane(1), + dst: 0, + } + }; + let program = match op { + MethodOp::Count => Program::new( + vec![sel], + Terminal::Count { + mask: Operand::Scratch(0), + }, + ), + MethodOp::Exists => Program::new( + vec![sel], + Terminal::Any { + mask: Operand::Scratch(0), + }, + ), + MethodOp::CountWhereGt { field, t } => Program::new( + vec![ + sel, + MaskOp::Pred { + pred: Pred::GtI32 { + lane: lane(field)?, + t, + }, + under: Some(Operand::Scratch(0)), + dst: 1, + }, + ], + Terminal::Count { + mask: Operand::Scratch(1), + }, + ), + MethodOp::CountDerived => Program::new( + vec![], + Terminal::Count { + mask: Operand::Plane(2), + }, + ), + MethodOp::SumWhereGt { field, t, sum } => Program::new( + vec![ + sel, + MaskOp::Pred { + pred: Pred::GtI32 { + lane: lane(field)?, + t, + }, + under: Some(Operand::Scratch(0)), + dst: 1, + }, + ], + Terminal::MaskedSumI32 { + mask: Operand::Scratch(1), + lane: lane(sum)?, + }, + ), + }; + Ok(Compiled { + program, + demand: op.demand(), + derived: matches!(op, MethodOp::CountDerived), + }) + } + + /// A scratch sized for `compiled` over this register file. + pub fn scratch(&self, compiled: &Compiled) -> Result, Refusal> { + Scratch::for_program(&compiled.program, self.n_rows).map_err(Refusal::Exec) + } + + /// Revalidate every register, then hand the operands to `f` as planes + /// that borrow the SoA. Nothing is copied. + pub fn with_planes( + &self, + table: &MapTable, + soa: &Soa, + scope_now: Scope, + demand: ValueDemand, + f: impl FnOnce(&Planes<'_>) -> R, + ) -> Result { + if self.checks.frame { + current(table, &self.frame)?; + } + if self.checks.scope && scope_now != self.scope { + return Err(Refusal::ScopeChanged); + } + self.check_soa(soa)?; + if matches!(demand, ValueDemand::Values) { + let bound = self.value_rev.ok_or(Refusal::ValuesNotBound)?; + if self.checks.values && bound != soa.revision { + return Err(Refusal::StaleValues { + bound, + now: soa.revision, + }); + } + } + // Plane 2 is the derived register when one exists; otherwise the + // selection stands in so every plane spans `n_rows` (no program + // compiled before `derive_gt` names plane 2). + let derived: &[u64] = self.derived.as_ref().map_or(&self.selection, |d| &d.1); + let masks: [&[u64]; 3] = [&soa.presence, &self.selection, derived]; + // Up to four bound lanes, borrowed in place; no Vec on this path. + let mut lanes: [LaneRef<'_>; 4] = [LaneRef::I32(&[]); 4]; + let k = self.demanded.len().min(4); + for (slot, &field) in lanes.iter_mut().zip(&self.demanded) { + *slot = LaneRef::I32(&soa.fields[usize::from(field)]); + } + let planes = Planes { + n_rows: self.n_rows, + masks: &masks, + lanes: &lanes[..k], + }; + Ok(f(&planes)) + } + + /// Execute a compiled method. The only arithmetic is `mask-risc`'s. + pub fn run( + &self, + table: &MapTable, + soa: &Soa, + scope_now: Scope, + compiled: &Compiled, + scratch: &mut Scratch<'_>, + ) -> Result { + if compiled.derived { + let (at, _) = self.derived.as_ref().ok_or(Refusal::NoDerivedRegister)?; + if self.checks.values && *at != soa.revision { + return Err(Refusal::StaleValues { + bound: *at, + now: soa.revision, + }); + } + } + self.with_planes(table, soa, scope_now, compiled.demand, |planes| { + execute(&compiled.program, planes, scratch, None) + })? + .map_err(Refusal::Exec) + } + + /// Compute the derived register `selected ∧ present ∧ field > t` through + /// `mask-risc` (a `Keep` into an owned mask), stamped with the SoA's value + /// revision. Requires values to be bound and current. + pub fn derive_gt( + &mut self, + table: &MapTable, + soa: &Soa, + scope_now: Scope, + field: u8, + t: i32, + ) -> Result<(), Refusal> { + let compiled = self.compile(MethodOp::CountWhereGt { field, t })?; + let program = Program::new( + compiled.program.ops.clone(), + Terminal::Keep { + mask: Operand::Scratch(1), + }, + ); + let mut scratch = Scratch::for_program(&program, self.n_rows).map_err(Refusal::Exec)?; + let mut words = vec![0u64; self.n_rows.div_ceil(64)]; + self.derived = None; + self.with_planes(table, soa, scope_now, ValueDemand::Values, |planes| { + execute_into( + &program, + planes, + &Foreign::NONE, + &mut scratch, + Out::Mask(&mut words), + ) + })? + .map_err(Refusal::Exec)?; + self.derived = Some((soa.revision, words)); + Ok(()) + } + + /// Bytes this register file owns: the selection register and, if + /// derived, the predicate register. Never a field value. + pub fn owned_bytes(&self) -> usize { + self.selection.len() * 8 + self.derived.as_ref().map_or(0, |d| d.1.len() * 8) + } +} + +fn current(table: &MapTable, frame: &Frame) -> Result<(), Refusal> { + let now = table.seal(); + if frame.same_issue(&now) { + Ok(()) + } else { + Err(Refusal::StaleFrame { + then: frame.revisions(), + now: now.revisions(), + }) + } +} + +/// Arm A of the bench: the same programs over planes the caller assembles +/// directly from the SoA and a caller-built selection. No register checks. +pub fn run_direct( + program: &Program, + soa: &Soa, + selection: &[u64], + demanded: &[u8], + scratch: &mut Scratch<'_>, +) -> Result { + let masks: [&[u64]; 2] = [&soa.presence, selection]; + let mut lanes: [LaneRef<'_>; 4] = [LaneRef::I32(&[]); 4]; + let k = demanded.len().min(4); + for (slot, &field) in lanes.iter_mut().zip(demanded) { + *slot = LaneRef::I32(&soa.fields[usize::from(field)]); + } + let planes = Planes { + n_rows: soa.n_rows, + masks: &masks, + lanes: &lanes[..k], + }; + execute(program, &planes, scratch, None) +} + +impl Compiled { + pub fn program(&self) -> &Program { + &self.program + } +} + +impl RegisterFile { + /// The selection register's words (read-only), for arm A of the bench. + pub fn selection(&self) -> &[u64] { + &self.selection + } +} diff --git a/crates/drisa-register-probe/tests/integration/main.rs b/crates/drisa-register-probe/tests/integration/main.rs new file mode 100644 index 000000000..f862bee24 --- /dev/null +++ b/crates/drisa-register-probe/tests/integration/main.rs @@ -0,0 +1 @@ +pub mod register; diff --git a/crates/drisa-register-probe/tests/integration/register.rs b/crates/drisa-register-probe/tests/integration/register.rs new file mode 100644 index 000000000..915497fd4 --- /dev/null +++ b/crates/drisa-register-probe/tests/integration/register.rs @@ -0,0 +1,485 @@ +//! D-DRISA-1 falsifiers. Every refusal test has a success control; every +//! answer is compared with the [`Fixture`] oracle, which reads only global ids +//! and values and never a map, a position or a register. + +use drisa_register_probe::{ + build_soa, build_table, lookups, Checks, Fixture, MethodOp, Refusal, RegisterFile, +}; +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_dt64::dr::{LocalMap, MapTable, Scope, TileId, Width}; +use lance_graph_dt64::ValueDemand; +use lance_graph_mask_risc::{MaskOp, Operand, Program, Scratch, Terminal, Value}; + +const FIELDS: usize = 64; +const DEMANDED: [u8; 3] = [5, 17, 42]; +const SCOPE: Scope = Scope { id: 7 }; + +struct World { + fixture: Fixture, + table: MapTable, + tiles: Vec, + width: Width, + selection: Vec, +} + +fn world(n: usize, width: Width, seed: u64) -> World { + let fixture = Fixture::new(n, FIELDS, seed); + let (table, tiles) = build_table(&fixture, width, 1, seed ^ 0xBEEF); + // Every 10th identity, so the selection includes absent identities too. + let selection: Vec = fixture.ids().into_iter().step_by(10).collect(); + World { + fixture, + table, + tiles, + width, + selection, + } +} + +fn authorized() -> WideFieldMask { + WideFieldMask::from_positions(&DEMANDED) +} + +fn bind( + w: &World, + soa: &drisa_register_probe::Soa, + checks: Checks, +) -> Result { + RegisterFile::bind( + &w.table, + &w.table.seal(), + &w.tiles, + w.width, + SCOPE, + FIELDS, + &authorized(), + &DEMANDED, + ValueDemand::Values, + &w.selection, + soa, + checks, + ) +} + +fn run( + file: &RegisterFile, + w: &World, + soa: &drisa_register_probe::Soa, + op: MethodOp, +) -> Result { + let c = file.compile(op)?; + let mut s = file.scratch(&c)?; + file.run(&w.table, soa, SCOPE, &c, &mut s) +} + +const OPS: [MethodOp; 4] = [ + MethodOp::Count, + MethodOp::Exists, + MethodOp::CountWhereGt { field: 17, t: -5 }, + MethodOp::SumWhereGt { + field: 17, + t: -5, + sum: 42, + }, +]; + +fn expect(w: &World, op: MethodOp) -> Value { + match op { + MethodOp::Count => Value::Count(w.fixture.count(&w.selection)), + MethodOp::Exists => Value::Bool(w.fixture.count(&w.selection) > 0), + MethodOp::CountWhereGt { field, t } => { + Value::Count(w.fixture.where_gt(&w.selection, field, t, field).0) + } + MethodOp::SumWhereGt { field, t, sum } => { + Value::SumI64(w.fixture.where_gt(&w.selection, field, t, sum).1) + } + MethodOp::CountDerived => unreachable!(), + } +} + +/// DR64, DR256 and 256 DR256 tiles: every method equals the oracle. +#[test] +fn every_method_matches_the_oracle_on_dr64_dr256_and_multi_tile() { + for (n, width) in [(64, Width::W64), (256, Width::W256), (65_536, Width::W256)] { + let w = world(n, width, 11); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + for op in OPS { + assert_eq!( + run(&file, &w, &soa, op).unwrap(), + expect(&w, op), + "{width:?} n={n} {op:?}" + ); + } + // Anti-vacuity: the value predicate keeps some and drops some. + let (kept, _) = w.fixture.where_gt(&w.selection, 17, -5, 17); + let present = w.fixture.count(&w.selection); + assert!(kept > 0 && kept < present, "n={n}: {kept} of {present}"); + } +} + +/// The executed planes borrow the SoA's own bytes; the register file owns +/// only the selection bits. +#[test] +fn execution_borrows_the_soa_and_copies_no_value() { + let w = world(65_536, Width::W256, 12); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + file.with_planes(&w.table, &soa, SCOPE, ValueDemand::Values, |p| { + assert_eq!(p.masks[0].as_ptr(), soa.presence_ptr()); + for (lane, &field) in p.lanes.iter().zip(&DEMANDED) { + let lance_graph_mask_risc::LaneRef::I32(v) = lane else { + panic!("i32 lane") + }; + assert_eq!(v.as_ptr(), soa.field_ptr(field), "field {field}"); + } + }) + .unwrap(); + assert_eq!(file.owned_bytes(), soa.n_rows() / 8); +} + +/// Routing happens once, at bind: 256 runs of four different methods add no +/// global → local lookup. +#[test] +fn many_methods_reuse_one_binding_without_rerouting() { + let w = world(65_536, Width::W256, 13); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let before = lookups(&w.table, &w.tiles); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + let after_bind = lookups(&w.table, &w.tiles); + assert!(after_bind - before >= w.selection.len() as u64); + let compiled: Vec<_> = OPS.iter().map(|&op| file.compile(op).unwrap()).collect(); + let mut scratch: Vec<_> = compiled.iter().map(|c| file.scratch(c).unwrap()).collect(); + for _ in 0..256 { + for ((c, s), &op) in compiled.iter().zip(&mut scratch).zip(&OPS) { + assert_eq!( + file.run(&w.table, &soa, SCOPE, c, s).unwrap(), + expect(&w, op) + ); + } + } + assert_eq!( + lookups(&w.table, &w.tiles), + after_bind, + "no routing per run" + ); +} + +/// A frame advance makes the old register file refuse; a fresh bind under +/// the new frame answers once the SoA owner has rebuilt the layout. With the +/// frame check off the old file still answers: the refusal is that check's. +#[test] +fn a_stale_frame_is_refused_and_a_fresh_bind_answers() { + // 200 ids in one DR256 tile, so the tile has room for an extension. + let mut w = world(200, Width::W256, 14); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + let lax = bind( + &w, + &soa, + Checks { + frame: false, + ..Checks::ALL + }, + ) + .unwrap(); + assert!(run(&file, &w, &soa, MethodOp::Count).is_ok()); + let frame = w.table.seal(); + let mut globals = w.table.map(&frame, w.tiles[0]).unwrap().globals().to_vec(); + globals.push(0xDEAD_BEEF); + w.table.advance( + 1, + 1, + vec![( + w.tiles[0], + Some(LocalMap::prepare(Width::W256, &globals).unwrap()), + )], + ); + assert!(matches!( + run(&file, &w, &soa, MethodOp::Count), + Err(Refusal::StaleFrame { .. }) + )); + assert_eq!( + run(&lax, &w, &soa, MethodOp::Count).unwrap(), + expect(&w, MethodOp::Count) + ); + // Under the new frame this SoA's layout digest is the old one: refused + // until its owner rebuilds it. + assert!(matches!( + bind(&w, &soa, Checks::ALL), + Err(Refusal::CoordinateMismatch { .. }) + )); + let rebuilt = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let fresh = bind(&w, &rebuilt, Checks::ALL).unwrap(); + assert_eq!( + run(&fresh, &w, &rebuilt, MethodOp::Count).unwrap(), + expect(&w, MethodOp::Count) + ); +} + +/// A value write: map-only methods keep answering (and stay correct); value +/// methods and the derived register refuse until the value witness is +/// re-taken, which re-routes nothing. +#[test] +fn a_value_write_invalidates_values_but_not_the_map() { + let mut w = world(65_536, Width::W256, 15); + let mut soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let mut file = bind(&w, &soa, Checks::ALL).unwrap(); + file.derive_gt(&w.table, &soa, SCOPE, 17, -5).unwrap(); + let derived_before = w.fixture.where_gt(&w.selection, 17, -5, 17).0; + assert_eq!( + run(&file, &w, &soa, MethodOp::CountDerived).unwrap(), + Value::Count(derived_before) + ); + + // Flip one selected, present identity across the threshold. + let g = *w + .selection + .iter() + .find(|&&g| w.fixture.present(g) && w.fixture.where_gt(&[g], 17, -5, 17).0 == 1) + .unwrap(); + let row = soa.row_of(&w.table, g).unwrap(); + soa.write(row, 17, -50); + w.fixture.set(g, 17, -50); + + assert_eq!( + run(&file, &w, &soa, MethodOp::Count).unwrap(), + expect(&w, MethodOp::Count) + ); + for op in [ + MethodOp::CountWhereGt { field: 17, t: -5 }, + MethodOp::CountDerived, + ] { + assert!( + matches!(run(&file, &w, &soa, op), Err(Refusal::StaleValues { .. })), + "{op:?}" + ); + } + let routed = lookups(&w.table, &w.tiles); + file.rebind_values(&w.table, &soa).unwrap(); + assert_eq!( + lookups(&w.table, &w.tiles), + routed, + "rebinding values routes nothing" + ); + let op = MethodOp::CountWhereGt { field: 17, t: -5 }; + assert_eq!(run(&file, &w, &soa, op).unwrap(), expect(&w, op)); + // The derived register is still the old one: it must refuse, not answer. + assert!(matches!( + run(&file, &w, &soa, MethodOp::CountDerived), + Err(Refusal::StaleValues { .. }) + )); + file.derive_gt(&w.table, &soa, SCOPE, 17, -5).unwrap(); + assert_eq!( + run(&file, &w, &soa, MethodOp::CountDerived).unwrap(), + Value::Count(derived_before - 1) + ); +} + +/// Disable: without the value check, the stale derived register answers, and +/// the answer is wrong. +#[test] +fn disabling_the_value_check_returns_a_wrong_derived_answer() { + let mut w = world(65_536, Width::W256, 16); + let mut soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let mut file = bind( + &w, + &soa, + Checks { + values: false, + ..Checks::ALL + }, + ) + .unwrap(); + file.derive_gt(&w.table, &soa, SCOPE, 17, -5).unwrap(); + let g = *w + .selection + .iter() + .find(|&&g| w.fixture.present(g) && w.fixture.where_gt(&[g], 17, -5, 17).0 == 1) + .unwrap(); + let row = soa.row_of(&w.table, g).unwrap(); + soa.write(row, 17, -50); + w.fixture.set(g, 17, -50); + let truth = w.fixture.where_gt(&w.selection, 17, -5, 17).0; + assert_ne!( + run(&file, &w, &soa, MethodOp::CountDerived).unwrap(), + Value::Count(truth) + ); +} + +/// A SoA of another source is refused; the same SoA under its own table is +/// accepted. +#[test] +fn a_soa_of_another_source_is_refused() { + let w = world(256, Width::W256, 17); + let (other, other_tiles) = build_table(&w.fixture, Width::W256, 2, 17 ^ 0xBEEF); + let foreign = build_soa(&w.fixture, &other, &other_tiles, Width::W256); + assert!(matches!( + bind(&w, &foreign, Checks::ALL), + Err(Refusal::SourceMismatch { frame: 1, soa: 2 }) + )); + let own = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + assert!(bind(&w, &own, Checks::ALL).is_ok()); +} + +/// Same ids, another local order: refused; with the coordinate check off the +/// value answers diverge from the oracle (the permutation is not harmless). +#[test] +fn a_permuted_coordinate_assignment_is_refused_and_would_be_wrong() { + let w = world(65_536, Width::W256, 18); + let (permuted, _) = build_table(&w.fixture, Width::W256, 1, 0x1234); + let soa_other_layout = build_soa(&w.fixture, &permuted, &w.tiles, Width::W256); + assert!(matches!( + bind(&w, &soa_other_layout, Checks::ALL), + Err(Refusal::CoordinateMismatch { .. }) + )); + let lax = bind( + &w, + &soa_other_layout, + Checks { + coordinates: false, + ..Checks::ALL + }, + ) + .unwrap(); + let op = MethodOp::SumWhereGt { + field: 17, + t: -5, + sum: 42, + }; + assert_ne!( + run(&lax, &w, &soa_other_layout, op).unwrap(), + expect(&w, op) + ); +} + +/// Unknown, unauthorized and unbound fields each refuse with their own +/// reason; the authorized demand binds. +#[test] +fn field_refusals_are_typed() { + let w = world(256, Width::W256, 19); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let try_bind = |demanded: &[u8]| { + RegisterFile::bind( + &w.table, + &w.table.seal(), + &w.tiles, + w.width, + SCOPE, + FIELDS, + &authorized(), + demanded, + ValueDemand::Values, + &w.selection, + &soa, + Checks::ALL, + ) + }; + assert!(matches!(try_bind(&[5, 64]), Err(Refusal::UnknownField(64)))); + assert!(matches!(try_bind(&[5, 6]), Err(Refusal::Unauthorized(6)))); + let file = try_bind(&DEMANDED).unwrap(); + assert!(matches!( + file.compile(MethodOp::CountWhereGt { field: 9, t: 0 }), + Err(Refusal::FieldNotBound(9)) + )); + assert!(file + .compile(MethodOp::CountWhereGt { field: 5, t: 0 }) + .is_ok()); +} + +/// Another scope refuses; with the scope check off it would answer. +#[test] +fn another_scope_is_refused() { + let w = world(256, Width::W256, 20); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + let c = file.compile(MethodOp::Count).unwrap(); + let mut s = file.scratch(&c).unwrap(); + assert!(matches!( + file.run(&w.table, &soa, Scope { id: 8 }, &c, &mut s), + Err(Refusal::ScopeChanged) + )); + assert!(file.run(&w.table, &soa, SCOPE, &c, &mut s).is_ok()); + let lax = bind( + &w, + &soa, + Checks { + scope: false, + ..Checks::ALL + }, + ) + .unwrap(); + assert!(lax.run(&w.table, &soa, Scope { id: 8 }, &c, &mut s).is_ok()); +} + +/// A program that reads a scratch slot it never wrote is refused, even when a +/// previous run left a full mask there: scratch carries nothing across runs. +#[test] +fn stale_scratch_is_refused_by_mask_risc() { + let w = world(256, Width::W256, 21); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind(&w, &soa, Checks::ALL).unwrap(); + let c = file + .compile(MethodOp::CountWhereGt { field: 17, t: -5 }) + .unwrap(); + let mut s = file.scratch(&c).unwrap(); + file.run(&w.table, &soa, SCOPE, &c, &mut s).unwrap(); + let reads_stale = Program::new( + vec![MaskOp::And { + a: Operand::Plane(0), + b: Operand::Plane(1), + dst: 0, + }], + Terminal::Count { + mask: Operand::Scratch(1), + }, + ); + let r = file.with_planes(&w.table, &soa, SCOPE, ValueDemand::MapOnly, |p| { + lance_graph_mask_risc::execute(&reads_stale, p, &mut s, None) + }); + assert!(matches!( + r, + Ok(Err( + lance_graph_mask_risc::ExecError::ScratchReadBeforeWrite { slot: 1 } + )) + )); + let _ = Scratch::new(1, 1); +} + +/// Disable: dropping the presence plane counts absent identities. +#[test] +fn disabling_presence_counts_absent_identities() { + let w = world(65_536, Width::W256, 22); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let file = bind( + &w, + &soa, + Checks { + presence: false, + ..Checks::ALL + }, + ) + .unwrap(); + assert_ne!( + run(&file, &w, &soa, MethodOp::Count).unwrap(), + expect(&w, MethodOp::Count) + ); +} + +/// An id no bound tile holds, and an id given twice, are refused at bind. +#[test] +fn selection_refusals_are_typed() { + let mut w = world(256, Width::W256, 23); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + w.selection.push(0x0123); + assert!(matches!( + bind(&w, &soa, Checks::ALL), + Err(Refusal::UnmappedIdentity(0x0123)) + )); + w.selection.pop(); + let first = w.selection[0]; + w.selection.push(first); + assert!( + matches!(bind(&w, &soa, Checks::ALL), Err(Refusal::DuplicateIdentity(g)) if g == first) + ); +} From 2d733eb1918b25f78e9feddb7ec8294df521783c Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 00:11:46 +0000 Subject: [PATCH 2/4] board: D-DRISA-1 register proof entry and D-DRISA decision memos Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/board/INTEGRATION_PLANS.md | 5 ++ .claude/board/STATUS_BOARD.md | 14 ++++ .../2026-11-04-d-drisa-1-register-proof.md | 66 +++++++++++++++ .claude/board/entries/README.md | 3 +- .claude/plans/d-drisa-decision-memos-v1.md | 83 +++++++++++++++++++ 5 files changed, 170 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-11-04-d-drisa-1-register-proof.md create mode 100644 .claude/plans/d-drisa-decision-memos-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 72efec009..257a16a99 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,8 @@ +## 2026-11-04 — D-DRISA decision memos after the local register proof → `.claude/plans/d-drisa-decision-memos-v1.md` + +**Status:** PROPOSED, owned by this session (EXO-153 stages 1 and 3). **Board:** [STATUS_BOARD](STATUS_BOARD.md) D-DRISA-1-LAB, D-DRISA-3-LAB, D-DRISA-M1..M7; [entry](entries/2026-11-04-d-drisa-1-register-proof.md). Architecture: #1953 (D-DRISA-0, a GPT-session plan adopted after review). Seven owner questions the local proof leaves open: a layout witness on the SoA (the first missing connection), a global id → tile index or co-addressed selections, result-register lifetime, source-location receipt, DR → Lance authority, the carry words as ALU, async loopback. +**Confidence:** each memo cites a lab measurement or a source line; no ruling made. + ## 2026-11-03 — D-DRAM-P3: P2 open ends integrated with the D-DRAM-0 falsifier map → `.claude/plans/d-dram-p3-integrated-v1.md` **Status:** PLAN, owned by this session (operator). **Board:** [STATUS_BOARD](STATUS_BOARD.md) D-DRAM-P3-1..8. Credits P2 (#1950) against the pre-registered #1949 gates (L9, L10, C2, C4 measured in the lab; L1/L2/L6/A3/A4 partial). Orders eleven owned items by signal per effort: three need no outside decision (ReadPolicy range count, non-vacuous projection cases, the D-DRAM-1 census). Production and gated items keep their owners; nothing merges automatically. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index e27abdb64..523df3d65 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -24,6 +24,20 @@ | D-DRAM-P3-7 | route once per frame, lab measurement | Queued | this session; production GATED EXO-46 | | D-DRAM-P3-8 | = D-DRAM-4 end-to-end, decision memo | GATED | D4 + S-INGRESS (#1788) | +**D-DRISA lab (2026-11-04): this session executes EXO-153 stages 1 and 3** ([memos](../plans/d-drisa-decision-memos-v1.md); architecture #1953, a GPT-session plan adopted after review). + +| D-id | Deliverable | Status | Owner / gate | +| --- | --- | --- | --- | +| D-DRISA-1-LAB | sealed DR frame as a local register file over borrowed SoA | Measured: 13/13 tests, 6 disables red, 0 allocations/query, +0.04–0.6 µs revalidation; [entry](entries/2026-11-04-d-drisa-1-register-proof.md) | this session; lab crate `drisa-register-probe` | +| D-DRISA-3-LAB | k-of-n / Kleene / Bag on the shipped carry words | In stacked PR | this session; ndarray / Quack owners | +| D-DRISA-M1 | layout witness on the canonical SoA | Proposed | SoA / DR owner | +| D-DRISA-M2 | global id → tile index, or co-addressed selections | Proposed | EXO-46 | +| D-DRISA-M3 | result-register lifetime across calls | Proposed | result owner | +| D-DRISA-M4 | source-location receipt | Deferred | EXO-46/89/151 | +| D-DRISA-M5 | DR → Lance row authority | Unchanged, GATED | D4 / S-INGRESS | +| D-DRISA-M6 | carry words as the default ALU | Proposed: refuse on current evidence | ndarray / Quack owners | +| D-DRISA-M7 | async loopback (stage 2) as a lab | Proposed: after review of stage 1 | runtime / security review | + Verified: ndarray #402 half/full adder words and #390 byte sum shipped, `Abacus` lab-only; DR `LocalMap` is identity-only; H14c/H14d and #1633 selective Lance reads are lab. Unverified: exact operator-mentioned `ndarray::simd::5x24::*` signature. **Borrow/prefetch default; materialized foreign facet only under D-DRF-1 §5 admission.** ## D-DT64-7 — behaviour addressing and registration: Frozen, Learned, Explore over one classid (2026-10-31) diff --git a/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md b/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md new file mode 100644 index 000000000..3c8329192 --- /dev/null +++ b/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md @@ -0,0 +1,66 @@ +# D-DRISA-1: a sealed DR frame works as a local register file over borrowed SoA, once the SoA states its layout + +**Status:** MEASURED-LAB (local, one process). Owner: this session (EXO-153 stage 1). Probe: `crates/drisa-register-probe/` (`src/lib.rs`, `tests/integration/register.rs`, `examples/drisa_bench.rs`), excluded from the workspace. Architecture: #1953 (D-DRISA-0, a plan written by a GPT session, adopted after review). No production change, no transport, no new public type. + +## Census: what the register contract can be built from + +Read at source on `main` `05f03abb4`. + +| Piece | Where | Status | +|---|---|---| +| Sealed frame, compared by issue (not by value) | `dt64::dr::Frame`, `FrameStore::seal/check` (`dr.rs:404`, `:445`) | EXISTING | +| Versioned tile maps, old frames replay their layout | `MapTable::advance/map/map_at` (`dr.rs:871`, `:913`, `:921`) | EXISTING | +| Counted global → local routing; per-tile digest | `LocalMap::local` counts lookups (`:605`), `TileMap::digest` (`:780`) | EXISTING | +| Locate one id across tiles | `MapTable::locate` reads EVERY listed tile (`:955`) | EXISTING; O(tiles) per id by design (ambiguity check) | +| Focus / Scope / Guards | `dr.rs:496`, `:503`, `:509` | EXISTING; `Focus` is a tile revision, not a lease | +| Map vs value lifetime | `dt64::ValueDemand::{MapOnly, Values}` (`lib.rs:189`) | EXISTING, no executor reads it | +| Borrowed operands | `mask-risc` `Planes { masks: &[&[u64]], lanes: &[LaneRef] }`, `Operand::{Plane, Scratch}` (`ir.rs:7`, `:73`) | EXISTING | +| Execution | `mask-risc::execute` / `execute_into` (`exec.rs:763`, `:1343`) over `ndarray::simd` | WIRED | +| Stale scratch refused | `ExecError::ScratchReadBeforeWrite` (`value.rs:128`) | EXISTING; the plan's "StaleSlot" is the R2IL probe's `FoldError::StaleSlot`, not mask-risc | +| A statement of which frame/tile digests a SoA's rows are laid out under | none found in the closed space above | **MISSING** (the lab `Soa` carries it) | +| A global id → tile index | none; `locate` scans tiles | **MISSING**, owner decision (EXO-46) | +| Source-location receipt / lease host | only excluded lab crates (#1951 census) | **BLOCKED** EXO-46/89/151 | +| Cross-call result register lifetime | no owner | **BLOCKED**, owner decision | +| DR → Lance `_rowid` authority | none | **BLOCKED** D4 / S-INGRESS | + +## The proof + +`RegisterFile` is a descriptor: the frame, the tile digests it was bound under, a scope, the demanded field positions, a value witness when values were demanded, and one map-only register (the identity selection, routed from global ids at bind). It holds no reference into the SoA and no value. At execution it re-checks every operand and hands `mask-risc` planes that borrow the SoA's own slices. + +The eight properties of the mission, each with the test that checks it: + +| # | Property | Result | +|---|---|---| +| 1 | Registers name coordinates, not values | `execution_borrows_the_soa_and_copies_no_value`: executed lanes and the presence plane have the SoA's own addresses; the file owns only the selection bits (8 KiB for 65,536 rows) | +| 2 | Methods name typed operands, not rows | `MethodOp` names field positions and constants; compiled once to an unchanged `mask-risc` `Program` | +| 3 | No second ALU | every answer comes from `mask-risc::execute` | +| 4 | One binding serves many methods without rerouting | `many_methods_reuse_one_binding_without_rerouting`: 256 rounds × 4 methods, 0 lookups after bind | +| 5 | Lifetimes tied to frame, layout, scope, source, values | each check has its own refusal and its own red disable (below) | +| 6 | A value write invalidates value-scoped registers, not the map | `a_value_write_invalidates_values_but_not_the_map`: COUNT stays valid and correct; value methods and the derived predicate register refuse; re-taking the value witness routes nothing; the stale derived register still refuses until recomputed | +| 7 | An invalid register refuses, never answers wrong or empty | `Refusal` has a variant per cause; the oracle tests show the lax versions answer wrong | +| 8 | No mandatory payload gather | no lane is copied; the only owned buffers are the selection and the optional derived register (one bit per row each) | + +All methods equal an independent oracle (global id → value, no map or position) on DR64 (1 tile), DR256 (1 tile) and DR256 × 256 tiles (65,536 identities, local order permuted per tile, 10% selection that includes absent identities). 13/13 tests. + +**Disable runs** (commit first, patch with an asserted anchor, `git checkout`): frame check off → 1 red; layout digest compare off → 2 red; value witness off (lanes) → 1 red; value witness off (derived register) → 1 red; scope check off → 1 red; duplicate-identity check off → 1 red. Restored: 13/13. + +## Cost (µs per query, round robin over 4 methods, 3 processes) + +| fixture | A direct planes | C one binding, revalidated per query | allocations per query (C) | +|---|---|---|---| +| DR64, 1 tile | 0.09–0.20 | 0.14–0.25 | 0 | +| DR256, 1 tile | 0.09–0.27 | 0.13–0.32 | 0 | +| DR256 × 256 tiles, Q ≥ 64 | 6.5–6.7 | 6.8–7.1 | 0 | + +Revalidating the register file costs about 0.04–0.6 µs per query over direct planes. Arm B (bind per query) costs 1.2–1.6 µs (DR64) and 3.7–4.3 µs (DR256) per query, 5 allocations and 7 / 26 lookups. At 256 tiles arm B **fails the gate** (above 1,000 µs per query): routing 6,554 ids scans the tile maps one after another, 842,138 lookups per bind, because no global id → tile index exists. That is the cost a binding pays once, and the measured reason the index (or a co-addressed producer) is an owner question. + +## Findings + +1. **The first missing source-level connection is a layout witness on the canonical SoA**: a statement that its rows are laid out under frame version V with tile digests D. Without it a binding cannot prove that the planes it borrows correspond to the frame; with it (the lab `Soa::layout`), a permuted or foreign layout is refused, and turning that check off gives a wrong answer. +2. **Frame currency is policy; correctness rests on the layout digest.** `MapTable::map` answers old frames by replaying their layout, so an old binding over an unchanged SoA still answers correctly (the lax-frame control). After an extension, the old SoA is refused under the new frame by its digest, not by the frame check. +3. **Map and value lifetimes separate cleanly**, exactly as `ValueDemand` declares; no executor reads `ValueDemand` today. +4. **Routing is the only per-query cost a binding removes.** Execution itself is identical (A vs C differ by the checks). + +## Not shown + +Remote or asynchronous execution, network or RDMA zero-copy, Lance I/O, source leases, cross-call result registers (the derived register here lives inside one in-process object; giving it a lifetime across calls is an owner decision). Decision memos: `.claude/plans/d-drisa-decision-memos-v1.md`. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 9a1f6ddf5..a62317d68 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ 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. -570 entries, 2026-08-06 .. 2026-11-03. +571 entries, 2026-08-06 .. 2026-11-04. | date | entry id | finding | file | |---|---|---|---| +| 2026-11-04 | `D-DRISA-1` | | [2026-11-04-d-drisa-1-register-proof.md](2026-11-04-d-drisa-1-register-proof.md) | | 2026-11-03 | `D-XLOG-META-WIRE-P0` | | [2026-11-03-d-xlog-meta-wire-p0.md](2026-11-03-d-xlog-meta-wire-p0.md) | | 2026-11-03 | `D-GRAMMAR-WHEN-1` | | [2026-11-03-d-grammar-when-1.md](2026-11-03-d-grammar-when-1.md) | | 2026-11-03 | `D-GRAMMAR-CONSTRAINTS-0` | | [2026-11-03-d-grammar-constraints-0.md](2026-11-03-d-grammar-constraints-0.md) | diff --git a/.claude/plans/d-drisa-decision-memos-v1.md b/.claude/plans/d-drisa-decision-memos-v1.md new file mode 100644 index 000000000..cd51b0507 --- /dev/null +++ b/.claude/plans/d-drisa-decision-memos-v1.md @@ -0,0 +1,83 @@ +# D-DRISA decision memos: the owner questions the local register proof leaves open + +> **Status:** PROPOSED. Written by this session after D-DRISA-1 (local register proof) and D-DRISA-3 (ALU semantics). Each memo states the question, the source it rests on, a proposed ruling, the falsifier that would decide it, and what follows from approval or refusal. Nothing here is a decision; each needs the named owner. Architecture: #1953 (D-DRISA-0, a plan by a GPT session, adopted after review). Tracking: EXO-153; handoff: EXO-50. + +## D-DRISA-M1: a layout witness on the canonical SoA + +**Question.** May the canonical SoA state which DR frame version and tile digests its rows are laid out under, so a register binding can verify the planes it borrows? + +**Source.** `MapTable` owns layout (`dr.rs:805`); `TileMap::digest` (`:780`); nothing on the SoA side states the layout (D-DRISA-1 census). The lab `Soa::layout` carries `(TileId, digest)` per tile. + +**Proposed ruling.** The SoA owner records `(MapTable identity, RouteVersion, per-tile digest)` when it lays rows out, read-only to consumers. No new map, no copy of ids. + +**Falsifier.** D-DRISA-1 `a_permuted_coordinate_assignment_is_refused_and_would_be_wrong`: same ids, another local order. Refused with the witness; wrong answer without it. + +**Approve:** register binding becomes verifiable without trusting the caller. **Refuse:** every binding must trust that planes and frame agree; a permuted layout answers wrong silently. + +## D-DRISA-M2: a global id → tile index (EXO-46) + +**Question.** Who owns routing a set of global ids to tiles? `MapTable::locate` reads every tile per id. + +**Source.** `dr.rs:955`. D-DRISA-1 arm B at 256 tiles: 842,138 lookups per bind, above 1,000 µs per query (failed gate). + +**Proposed ruling.** Either (a) an index owned by `MapTable`, versioned with it, or (b) no index: callers obtain selections co-addressed (the #1948 C′ form) so routing never happens per query. Not a new hash table outside DR. + +**Falsifier.** The same arm B with the chosen mechanism: lookups per id ≤ 1 and bind under 1,000 µs at 256 tiles, with the D-DRISA-1 oracle unchanged. + +**Approve (a):** binding cost falls to O(ids). **Approve (b):** no new structure; selections must arrive co-addressed. **Refuse both:** register files must be bound once and reused, never per query. + +## D-DRISA-M3: result-register lifetime across calls + +**Question.** May a derived mask (the D-DRISA-1 derived predicate register) outlive one call? + +**Source.** In-program scratch is epoch-safe (`ExecError::ScratchReadBeforeWrite`). The derived register in the lab lives in one in-process object, stamped with the value revision; nothing owns it across calls. + +**Proposed ruling.** A bounded result register keyed by `(frame issue, layout digests, scope, value revision)`, evicted without changing truth, refusing on any mismatch. No global mask store. + +**Falsifier.** D-DRISA-1 `a_value_write_invalidates_values_but_not_the_map` and `disabling_the_value_check_returns_a_wrong_derived_answer`, run across two calls; plus #1953 N9 (reuse on another frame/scope/source must refuse). + +**Approve:** repeated value predicates need not be recomputed. **Refuse:** results are scalars or egress masks only, recomputed per call. + +## D-DRISA-M4: source-location receipt (EXO-46 / EXO-89 / EXO-151) + +**Question.** Who hosts a receipt of resolved canonical locations? + +**Source.** #1951 census: no production lease host; `drf-focus-probe::FocusKey` and `lance-graph-nsl::FocusLease` are excluded lab crates. D-DRISA-1 needed no receipt: within one process the SoA is borrowed directly. + +**Proposed ruling.** Defer. D-DRISA-1 shows a local binding needs a layout witness (M1), not a location receipt. A receipt matters only once the source is not directly borrowable (Lance, remote). + +**Falsifier.** #1953 R8–R16 once a host exists. + +## D-DRISA-M5: DR → Lance row authority (D4 / S-INGRESS) + +**Question.** Unchanged from #1950 and #1951: exactly one attested DR ordinal → `_rowid` seam, with ingress counted. + +**Source.** #1950 `where_lance_arm` (`BLOCKED_D4`); ingress measured as a copy (0.4–5.4 µs for one range, 123,162 µs for 3.26M ranges). + +**Proposed ruling.** No change by this work. D-DRISA-1 adds one input: the layout witness (M1) is the same kind of statement on the Lance side (a frame → fragment/row binding), so M1 and D4 should be designed together. + +## D-DRISA-M6: the Abakus ALU as an instruction family + +**Question.** Should the shipped carry words become the ALU for threshold, Kleene or Bag instructions? + +**Source.** D-DRISA-3: correct on every case (19/19 tests, 7 disables red), but 1.5–4.8× slower than native words on the same facade in all eight measured shapes, including 3-of-5 against its Boolean expansion and Kleene against two byte counters. P3-5 (#1954): 1.7–4.0× slower for plain k-of-n. + +**Proposed ruling.** Refuse as the default ALU on this evidence. Keep the semantics (the tests and the oracle) as the reference; lower k-of-n, Kleene and Bag thresholds to `U8x64` byte counters. Revisit only with a wide carry word (ndarray owner) or a shape byte counters cannot hold (counts above 255). + +**Falsifier.** A carry implementation that beats `U8x64` on any of the eight shapes, with the D-DRISA-3 oracle unchanged. + +## D-DRISA-M7: asynchronous loopback (stage 2) + +**Question.** May stage 2 (in-process queue, deadline, cancel) proceed as a lab? + +**Source.** #1953 charter PR2. D-DRISA-1 gives the descriptor it would carry: frame issue, layout digests, scope, value revision, compiled method. + +**Proposed ruling.** Yes, as a lab, after review of D-DRISA-1. A queued descriptor must re-run the same revalidation at execution, so a source change between admit and run is refused by the existing checks (N1, N4, N12). + +**Falsifier.** #1953 N1–N9 against the D-DRISA-1 refusals. + +## Checklist + +- [x] D-DRISA-1 local register proof (`entries/2026-11-04-d-drisa-1-register-proof.md`) +- [ ] D-DRISA-3 ALU semantics (stacked PR) +- [ ] Owner rulings M1–M7 From 7af6b16e78843002caf3ec4706cae90a4cfe9bb2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 01:08:35 +0000 Subject: [PATCH 3/4] drisa-register-probe: incarnation in value witness, lane schema in Compiled A rebuilt SoA restarted its revision at zero, so a witness taken from the old SoA matched the new one and a stale derived mask answered. The witness is now (incarnation, revision); every build_soa takes a fresh incarnation. A Compiled program carried lane indices but not the schema they were resolved against, so running it on a file with reordered demanded fields predicated on the wrong field. Compiled now records the schema and run refuses a mismatch with Refusal::SchemaMismatch. Two falsifiers with success controls; both Codex findings on #1955. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/drisa-register-probe/src/lib.rs | 64 ++++++++++--- .../tests/integration/register.rs | 96 +++++++++++++++++++ 2 files changed, 147 insertions(+), 13 deletions(-) diff --git a/crates/drisa-register-probe/src/lib.rs b/crates/drisa-register-probe/src/lib.rs index 7c38535e8..c7cd393d3 100644 --- a/crates/drisa-register-probe/src/lib.rs +++ b/crates/drisa-register-probe/src/lib.rs @@ -28,6 +28,8 @@ //! on field values, so a value write leaves it valid while a value-dependent //! method must refuse until its value witness is re-taken. +use std::sync::atomic::{AtomicU64, Ordering}; + use lance_graph_contract::class_view::WideFieldMask; use lance_graph_dt64::dr::{ Frame, FrameRevisions, LocalMap, MapRead, MapTable, Scope, TileId, Width, @@ -69,19 +71,39 @@ pub enum Refusal { DuplicateIdentity(u64), /// A value-dependent method, but values were not demanded at bind. ValuesNotBound, - /// The SoA's values changed since the register took its value witness. - StaleValues { bound: u64, now: u64 }, + /// The SoA's values changed since the register took its value witness, + /// or the SoA is another incarnation (rebuilt) with a restarted revision. + StaleValues { + bound: ValueWitness, + now: ValueWitness, + }, + /// A compiled method was resolved against another register file's lane + /// schema: its lane indices would name different fields here. + SchemaMismatch, /// A method reads the derived register, but none was derived. NoDerivedRegister, /// `mask-risc` refused the program. Exec(ExecError), } +/// The identity of one value state: which SoA incarnation and which revision +/// of it. The revision alone restarts at zero when a SoA is rebuilt, so it +/// cannot tell a rebuilt SoA from the one a witness was taken from. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct ValueWitness { + pub incarnation: u64, + pub revision: u64, +} + +/// Every built SoA gets a fresh incarnation, never reused in a process. +static NEXT_INCARNATION: AtomicU64 = AtomicU64::new(1); + /// The canonical owner's values: one row per DR position, tile-major /// (`row = tile_ordinal * width + local`). Not part of the register file. #[derive(Debug)] pub struct Soa { source: u64, + incarnation: u64, revision: u64, width: Width, layout: Vec<(TileId, u64)>, @@ -99,6 +121,14 @@ impl Soa { self.revision } + /// The value witness a register takes and later compares. + pub fn witness(&self) -> ValueWitness { + ValueWitness { + incarnation: self.incarnation, + revision: self.revision, + } + } + pub fn field_count(&self) -> usize { self.fields.len() } @@ -287,6 +317,7 @@ pub fn build_soa(fixture: &Fixture, table: &MapTable, tiles: &[TileId], width: W } Soa { source: table.revisions().source, + incarnation: NEXT_INCARNATION.fetch_add(1, Ordering::Relaxed), revision: 0, width, layout, @@ -339,12 +370,12 @@ pub struct RegisterFile { /// Demanded field positions; lane `i` of the executed planes is /// `demanded[i]`. demanded: Vec, - value_rev: Option, + value_rev: Option, /// The map-only identity selection register, one bit per row. selection: Vec, - /// A derived, value-dependent predicate register: `(value revision it was - /// computed at, mask)`. Valid only while the SoA is at that revision. - derived: Option<(u64, Vec)>, + /// A derived, value-dependent predicate register: `(value witness it was + /// computed at, mask)`. Valid only while the SoA has that witness. + derived: Option<(ValueWitness, Vec)>, n_rows: usize, checks: Checks, } @@ -386,6 +417,9 @@ pub struct Compiled { demand: ValueDemand, /// Reads the derived predicate register (plane 2). derived: bool, + /// The lane schema (demanded fields, in lane order) the program's lane + /// indices were resolved against. Checked before execution. + schema: Vec, } impl RegisterFile { @@ -460,7 +494,7 @@ impl RegisterFile { }; file.check_soa(soa)?; Ok(RegisterFile { - value_rev: matches!(demand, ValueDemand::Values).then_some(soa.revision), + value_rev: matches!(demand, ValueDemand::Values).then_some(soa.witness()), ..file }) } @@ -472,7 +506,7 @@ impl RegisterFile { current(table, &self.frame)?; } self.check_soa(soa)?; - self.value_rev = Some(soa.revision); + self.value_rev = Some(soa.witness()); Ok(()) } @@ -579,6 +613,7 @@ impl RegisterFile { program, demand: op.demand(), derived: matches!(op, MethodOp::CountDerived), + schema: self.demanded.clone(), }) } @@ -606,10 +641,10 @@ impl RegisterFile { self.check_soa(soa)?; if matches!(demand, ValueDemand::Values) { let bound = self.value_rev.ok_or(Refusal::ValuesNotBound)?; - if self.checks.values && bound != soa.revision { + if self.checks.values && bound != soa.witness() { return Err(Refusal::StaleValues { bound, - now: soa.revision, + now: soa.witness(), }); } } @@ -641,12 +676,15 @@ impl RegisterFile { compiled: &Compiled, scratch: &mut Scratch<'_>, ) -> Result { + if compiled.schema != self.demanded { + return Err(Refusal::SchemaMismatch); + } if compiled.derived { let (at, _) = self.derived.as_ref().ok_or(Refusal::NoDerivedRegister)?; - if self.checks.values && *at != soa.revision { + if self.checks.values && *at != soa.witness() { return Err(Refusal::StaleValues { bound: *at, - now: soa.revision, + now: soa.witness(), }); } } @@ -687,7 +725,7 @@ impl RegisterFile { ) })? .map_err(Refusal::Exec)?; - self.derived = Some((soa.revision, words)); + self.derived = Some((soa.witness(), words)); Ok(()) } diff --git a/crates/drisa-register-probe/tests/integration/register.rs b/crates/drisa-register-probe/tests/integration/register.rs index 915497fd4..464bde5a5 100644 --- a/crates/drisa-register-probe/tests/integration/register.rs +++ b/crates/drisa-register-probe/tests/integration/register.rs @@ -483,3 +483,99 @@ fn selection_refusals_are_typed() { matches!(bind(&w, &soa, Checks::ALL), Err(Refusal::DuplicateIdentity(g)) if g == first) ); } + +/// A rebuilt SoA restarts its revision at zero. Without an incarnation in the +/// witness, a register bound to the old SoA would accept the rebuilt one and +/// answer with a derived mask computed from the old values. (Codex, #1955.) +#[test] +fn a_rebuilt_soa_is_another_value_state_even_at_revision_zero() { + let mut w = world(65_536, Width::W256, 17); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let mut file = bind(&w, &soa, Checks::ALL).unwrap(); + file.derive_gt(&w.table, &soa, SCOPE, 17, -5).unwrap(); + + let g = *w + .selection + .iter() + .find(|&&g| w.fixture.present(g) && w.fixture.where_gt(&[g], 17, -5, 17).0 == 1) + .unwrap(); + w.fixture.set(g, 17, -50); + let rebuilt = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + assert_eq!( + rebuilt.revision(), + soa.revision(), + "fixture: equal revisions" + ); + assert_ne!(rebuilt.witness(), soa.witness()); + + for op in [ + MethodOp::CountWhereGt { field: 17, t: -5 }, + MethodOp::CountDerived, + ] { + assert!( + matches!( + run(&file, &w, &rebuilt, op), + Err(Refusal::StaleValues { .. }) + ), + "{op:?}" + ); + } + // Control: map-only methods still answer; after rebinding, values answer. + assert_eq!( + run(&file, &w, &rebuilt, MethodOp::Count).unwrap(), + expect(&w, MethodOp::Count) + ); + file.rebind_values(&w.table, &rebuilt).unwrap(); + let op = MethodOp::CountWhereGt { field: 17, t: -5 }; + assert_eq!(run(&file, &w, &rebuilt, op).unwrap(), expect(&w, op)); + file.derive_gt(&w.table, &rebuilt, SCOPE, 17, -5).unwrap(); + assert_eq!( + run(&file, &w, &rebuilt, MethodOp::CountDerived).unwrap(), + Value::Count(w.fixture.where_gt(&w.selection, 17, -5, 17).0) + ); +} + +/// A method compiled against one lane schema must not run on a register file +/// whose lanes name other fields. (Codex, #1955.) +#[test] +fn a_method_compiled_for_another_lane_schema_is_refused() { + let w = world(65_536, Width::W256, 18); + let soa = build_soa(&w.fixture, &w.table, &w.tiles, w.width); + let bind_with = |demanded: &[u8]| { + RegisterFile::bind( + &w.table, + &w.table.seal(), + &w.tiles, + w.width, + SCOPE, + FIELDS, + &authorized(), + demanded, + ValueDemand::Values, + &w.selection, + &soa, + Checks::ALL, + ) + .unwrap() + }; + let a = bind_with(&[17, 42]); + let b = bind_with(&[42, 17]); + let op = MethodOp::CountWhereGt { field: 17, t: -5 }; + let c = a.compile(op).unwrap(); + // Anti-vacuity: on these values field 17 and field 42 disagree, so running + // `c` over `b`'s lanes would give a different, wrong count. + let wrong = MethodOp::CountWhereGt { field: 42, t: -5 }; + assert_ne!(expect(&w, op), expect(&w, wrong)); + let mut s = b.scratch(&c).unwrap(); + assert_eq!( + b.run(&w.table, &soa, SCOPE, &c, &mut s), + Err(Refusal::SchemaMismatch) + ); + // Control: the same method on its own file, and recompiled on `b`. + let mut s = a.scratch(&c).unwrap(); + assert_eq!( + a.run(&w.table, &soa, SCOPE, &c, &mut s).unwrap(), + expect(&w, op) + ); + assert_eq!(run(&b, &w, &soa, op).unwrap(), expect(&w, op)); +} From 272eb6a94f893811fd0c3c3c42d0c4cb700d815e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 01:09:46 +0000 Subject: [PATCH 4/4] D-DRISA-1 entry: record the two review fixes Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/board/entries/2026-11-04-d-drisa-1-register-proof.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md b/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md index 3c8329192..25b76cfb6 100644 --- a/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md +++ b/.claude/board/entries/2026-11-04-d-drisa-1-register-proof.md @@ -44,6 +44,8 @@ All methods equal an independent oracle (global id → value, no map or position **Disable runs** (commit first, patch with an asserted anchor, `git checkout`): frame check off → 1 red; layout digest compare off → 2 red; value witness off (lanes) → 1 red; value witness off (derived register) → 1 red; scope check off → 1 red; duplicate-identity check off → 1 red. Restored: 13/13. +**Review fixes (Codex, #1955).** The value witness is now `(incarnation, revision)`: a rebuilt SoA restarted its revision at zero and was accepted against a witness from the old one. `Compiled` now records the lane schema it was resolved against, and `run` refuses `SchemaMismatch` on a file whose lanes name other fields. Two falsifiers with controls; disables: incarnation pinned → 1 red, schema check off → 1 red. 15/15. + ## Cost (µs per query, round robin over 4 methods, 3 processes) | fixture | A direct planes | C one binding, revalidated per query | allocations per query (C) |