From e5ac9caa76a719bbc0724dc1846e5d529696e8c7 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 01:51:05 +0000 Subject: [PATCH 1/7] dr: MapTable, the versioned global -> local table (D-DT64-7 O5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A LocalMap is now read only under the frame it was sealed under; the coordinates revision is derived from the held maps (tile id + map digest), not passed in. Stored selections (D7') wait on O4. Design: plan §1e. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- ...-7-behaviour-addressing-registration-v1.md | 35 +++++++ crates/lance-graph-dt64/src/dr.rs | 95 +++++++++++++++++++ crates/lance-graph-dt64/tests/dr.rs | 78 +++++++++++++++ 3 files changed, 208 insertions(+) diff --git a/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md b/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md index 7ae1c3c18..e2ceb78fb 100644 --- a/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md +++ b/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md @@ -116,6 +116,41 @@ Preserved throughout: the `0xC401` name-bound reading, the `FnIndex` opcode cont --- +### 1e. O5 design: the versioned global → local table (2026-11-01) + +O5 is a BindStore plan item (D-DT64-6 Amendment A). Litho is the mental model it came from, not a component. + +**What exists (VERIFIED-IN-CODE, `lance-graph-dt64/src/dr.rs`):** + +| Piece | What it does | +|---|---| +| `LocalMap::prepare(width, globals)` | One tile's global → local table, at most 64 or 256 entries. Duplicates and overflow are refused. | +| Row shape | One row per local position: `globals[local]`. `local()` reads global → local (counted), `global()` reads local → global. Ids only, never values. | +| `LocalMap::digest` | FNV-1a over the local-order table. Its doc says a frame carries this value as its `coordinates` revision. | +| `FrameStore` | `seal` / `advance` / `check`. A stale frame is refused and names the revision that moved (`CoordinatesChanged` for a new map). | + +So "versions = frame revisions" already works as a mechanism. **The gap:** nothing ties a `LocalMap` to the frame it was sealed under. +- A caller can keep a map after `advance` and read through it with no refusal. +- `coordinates` is whatever number the caller passes, not the digest of the maps in use. + +**Proposal (WORKING-MODEL), in `dr`, additive. No existing signature changes:** + +1. **`MapTable`.** It owns one `FrameStore` and the `LocalMap` of each tile, keyed by `TileId` (a `u32` the caller names). Insert and replace go through `MapTable::advance(changes)`. That sets `coordinates` to a digest over every tile's `(TileId, LocalMap::digest)` in tile order, and leaves `source` and `relation_map` as passed. Tiles are inserted only through `advance`, so the revision always matches the maps actually held. +2. **Reads take the frame.** `MapTable::map(&Frame, tile) -> Result<&LocalMap, MapRead>`. `MapRead` is either `Stale(FrameRefusal)` or `NoSuchTile`. Old frames are refused, so a map cannot outlive its frame. This is `Pop`'s `Stale` rule (F7) applied to coordinates. +3. **Where it sits.** DR owns the frame, so the table lives in `dr`, beside `FrameStore`. The BindStore keeps reading frames through `Guards`, exactly as `prepare` does now. A BindStore field holding the table is the alternative; it would make the store own DR state, which §3 assigns to DR. +4. **Not in this item: stored selections (D7').** Storing a `WideFieldMask` over a tile's local positions, keyed to the frame, depends on O4: whether one `0xF###` value names one stored selection or one position in a wider basis. It is added once O4 is decided, as a sibling read with the same `Stale` refusal. + +**Falsifiers (test-first):** + +| Id | Falsifier | +|---|---| +| T1 | A map read under a frame sealed before `advance` is refused with `Stale(CoordinatesChanged)`, and read under the new seal it succeeds. Twin: an `advance` that changes nothing in a tile still re-seals, so the old frame gets `Stale(FrameResealed)`. | +| T2 | `coordinates` is a function of the held maps. The same maps in the same tiles give the same revision. Reordering one tile's globals changes it. Swapping two tiles' maps changes it, because the `TileId` is in the digest. | +| T3 | A frame from another `MapTable` is refused with `Stale(ForeignFrame)`, even at equal revisions. | +| T4 | Backward compatibility: existing `LocalMap` / `FrameStore` callers (`tests/dr.rs`, `xlog-relcomp-probe` `litho.rs` and `gate_b.rs`) are unchanged and green. | + +Each falsifier gets a disable run: drop the frame check in `map`, and drop the `TileId` from the digest. + ## 2. The classid, both sides ```text diff --git a/crates/lance-graph-dt64/src/dr.rs b/crates/lance-graph-dt64/src/dr.rs index 062a0d652..0c46caa69 100644 --- a/crates/lance-graph-dt64/src/dr.rs +++ b/crates/lance-graph-dt64/src/dr.rs @@ -506,6 +506,101 @@ impl LocalMap { } } +/// A tile's name in a [`MapTable`], chosen by the caller. +pub type TileId = u32; + +/// Why a [`MapTable`] read was refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum MapRead { + /// The frame is not the table's current seal. + Stale(FrameRefusal), + /// The current frame holds no map for this tile. + NoSuchTile(TileId), +} + +/// The versioned global → local table (D-DT64-7 O5): every tile's +/// [`LocalMap`] under one [`FrameStore`]. Maps change only through +/// [`MapTable::advance`], which sets the `coordinates` revision from the maps +/// it holds, and a map is read only under the frame it was sealed under. +#[derive(Debug)] +pub struct MapTable { + frames: FrameStore, + tiles: BTreeMap, +} + +impl MapTable { + /// An empty table at the given source and relation-map revisions. + pub fn new(source: u64, relation_map: u64) -> Self { + let tiles = BTreeMap::new(); + let coordinates = Self::coordinates(&tiles); + Self { + frames: FrameStore::new(FrameRevisions { + source, + relation_map, + coordinates, + }), + tiles, + } + } + + /// FNV-1a over `(tile, map digest)` in tile order. + fn coordinates(tiles: &BTreeMap) -> u64 { + let mut h: u64 = 0xcbf2_9ce4_8422_2325; + for (tile, map) in tiles { + let bytes = tile + .to_le_bytes() + .into_iter() + .chain(map.digest().to_le_bytes()); + for b in bytes { + h ^= u64::from(b); + h = h.wrapping_mul(0x0000_0100_0000_01b3); + } + } + h + } + + /// Insert (`Some`), replace (`Some`) or remove (`None`) tile maps, then + /// re-seal. Every frame sealed before is stale afterwards, even when + /// nothing changed. + pub fn advance( + &mut self, + source: u64, + relation_map: u64, + changes: Vec<(TileId, Option)>, + ) { + for (tile, map) in changes { + match map { + Some(m) => { + self.tiles.insert(tile, m); + } + None => { + self.tiles.remove(&tile); + } + } + } + self.frames.advance(FrameRevisions { + source, + relation_map, + coordinates: Self::coordinates(&self.tiles), + }); + } + + /// Seal the current frame. + pub fn seal(&self) -> Frame { + self.frames.seal() + } + + pub fn revisions(&self) -> FrameRevisions { + self.frames.revisions() + } + + /// The map of `tile`, if `frame` is the current seal. + pub fn map(&self, frame: &Frame, tile: TileId) -> Result<&LocalMap, MapRead> { + self.frames.check(frame).map_err(MapRead::Stale)?; + self.tiles.get(&tile).ok_or(MapRead::NoSuchTile(tile)) + } +} + /// The HHTL16 Cartesian address of cell `(x, y)` of one tile of `width`: the /// contract's [`Morton8x8`] code, `x` the row coordinate, `y` the column. #[inline] diff --git a/crates/lance-graph-dt64/tests/dr.rs b/crates/lance-graph-dt64/tests/dr.rs index c3242af74..ca67b4341 100644 --- a/crates/lance-graph-dt64/tests/dr.rs +++ b/crates/lance-graph-dt64/tests/dr.rs @@ -159,3 +159,81 @@ fn dr_does_not_depend_on_the_binding_side() { ); assert!(!src.contains("super::"), "dr.rs must not name its parent"); } + +// ------------------------------------------- MapTable (D-DT64-7 O5, §1e) + +use lance_graph_dt64::dr::{MapRead, MapTable}; + +fn map(ids: &[u64]) -> LocalMap { + LocalMap::prepare(Width::W64, ids).unwrap() +} + +#[test] +fn a_map_is_read_only_under_the_frame_it_was_sealed_under() { + let mut t = MapTable::new(7, 11); + t.advance(7, 11, vec![(1, Some(map(&[10, 20, 30])))]); + let old = t.seal(); + assert_eq!(t.map(&old, 1).unwrap().local(20), Ok(1)); + t.advance(7, 11, vec![(1, Some(map(&[30, 20, 10])))]); + assert_eq!( + t.map(&old, 1).unwrap_err(), + MapRead::Stale(FrameRefusal::CoordinatesChanged) + ); + let now = t.seal(); + assert_eq!(t.map(&now, 1).unwrap().local(30), Ok(0)); + assert_eq!(t.map(&now, 2).unwrap_err(), MapRead::NoSuchTile(2)); +} + +#[test] +fn an_advance_that_changes_nothing_still_reseals() { + let mut t = MapTable::new(7, 11); + t.advance(7, 11, vec![(1, Some(map(&[10, 20])))]); + let old = t.seal(); + let before = t.revisions(); + t.advance(7, 11, vec![]); + assert_eq!(t.revisions(), before, "nothing moved"); + assert_eq!( + t.map(&old, 1).unwrap_err(), + MapRead::Stale(FrameRefusal::FrameResealed) + ); +} + +#[test] +fn the_coordinates_revision_is_a_function_of_the_held_maps() { + let at = |tiles: Vec<(u32, &[u64])>| { + let mut t = MapTable::new(7, 11); + t.advance( + 7, + 11, + tiles.into_iter().map(|(k, v)| (k, Some(map(v)))).collect(), + ); + t.revisions().coordinates + }; + let base = at(vec![(1, &[10, 20]), (2, &[30, 40])]); + assert_eq!(base, at(vec![(1, &[10, 20]), (2, &[30, 40])]), "same maps"); + assert_ne!(base, at(vec![(1, &[20, 10]), (2, &[30, 40])]), "reordered"); + assert_ne!( + base, + at(vec![(1, &[30, 40]), (2, &[10, 20])]), + "tiles swapped" + ); + assert_ne!(base, at(vec![(1, &[10, 20])]), "tile removed"); +} + +#[test] +fn a_removed_tile_is_gone_and_another_tables_frame_is_foreign() { + let mut a = MapTable::new(7, 11); + a.advance(7, 11, vec![(1, Some(map(&[10]))), (2, Some(map(&[20])))]); + a.advance(7, 11, vec![(2, None)]); + let f = a.seal(); + assert!(a.map(&f, 1).is_ok()); + assert_eq!(a.map(&f, 2).unwrap_err(), MapRead::NoSuchTile(2)); + + let mut b = MapTable::new(7, 11); + b.advance(7, 11, vec![(1, Some(map(&[10])))]); + assert_eq!(a.revisions(), b.revisions(), "equal numbers"); + assert_eq!( + a.map(&b.seal(), 1).unwrap_err(), + MapRead::Stale(FrameRefusal::ForeignFrame) + ); +} From 37d05254ddb7d1caa07e650df2cf4c1fab5f1e42 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 01:51:30 +0000 Subject: [PATCH 2/7] dr: pin the tile id in the MapTable coordinates digest (renamed tile) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/lance-graph-dt64/tests/dr.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/crates/lance-graph-dt64/tests/dr.rs b/crates/lance-graph-dt64/tests/dr.rs index ca67b4341..0e1da49fb 100644 --- a/crates/lance-graph-dt64/tests/dr.rs +++ b/crates/lance-graph-dt64/tests/dr.rs @@ -218,6 +218,9 @@ fn the_coordinates_revision_is_a_function_of_the_held_maps() { "tiles swapped" ); assert_ne!(base, at(vec![(1, &[10, 20])]), "tile removed"); + // Same maps in the same order under another tile name: only the tile id + // in the digest tells these apart. + assert_ne!(base, at(vec![(1, &[10, 20]), (3, &[30, 40])]), "tile renamed"); } #[test] From 3b2477625d91c11eb33a2f49451cd10d0fe5e035 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 01:52:16 +0000 Subject: [PATCH 3/7] =?UTF-8?q?board:=20D-DT64-7-5=20MapTable=20entry,=20s?= =?UTF-8?q?tatus,=20plan=20=C2=A71e=20status?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/board/STATUS_BOARD.md | 2 +- .../2026-11-01-maptable-versioned-local-map.md | 15 +++++++++++++++ .claude/board/entries/README.md | 3 ++- ...dt64-7-behaviour-addressing-registration-v1.md | 4 +++- 4 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 .claude/board/entries/2026-11-01-maptable-versioned-local-map.md diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index a7dbc06e2..26b4fc820 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -15,7 +15,7 @@ Plan: `.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md`. Docs onl | D-DT64-7-L1 | full-classid basis for behaviour lenses (contract `ClassView` accessor) | Queued | after L4 | | D-DT64-7-L5 | consumer `ClassView` + immutable basis witness at registration | Queued | after L1 | | D-DT64-7-L2 | host composition of DT64 and OGAR authorities + views, with activation checks (L3) | Queued | after L5 | -| D-DT64-7-5 | the versioned global → local selection table (D-LITHO Q5) | Queued | O5 (DR/DT owner) | +| D-DT64-7-5 | the versioned global → local table, a BindStore plan item (plan §1e) | Core in PR: `dr::MapTable`; stored selections (D7') wait on O4 | O4 for the selection half | ## D-MIST-NATIVE — Mistaber's Kripke holdings over the DR64 relation register (2026-10-30) diff --git a/.claude/board/entries/2026-11-01-maptable-versioned-local-map.md b/.claude/board/entries/2026-11-01-maptable-versioned-local-map.md new file mode 100644 index 000000000..811685322 --- /dev/null +++ b/.claude/board/entries/2026-11-01-maptable-versioned-local-map.md @@ -0,0 +1,15 @@ +# D-DT64-7-5: `dr::MapTable`, the versioned global → local table + +**Date 2026-11-01 · ID D-DT64-7-5 · Status IN PR · Plan `.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md` §1e** + +`LocalMap` and `FrameStore` existed, and `LocalMap::digest` was documented as the frame's `coordinates` revision, but nothing tied a map to its frame. `MapTable` holds every tile's `LocalMap` under one `FrameStore`: + +- `advance` derives `coordinates` from the held `(tile id, map digest)` pairs. +- `map(&Frame, tile)` refuses a stale or foreign frame (`MapRead::Stale`), and a missing tile (`NoSuchTile`). +- Existing `LocalMap` and `FrameStore` callers are unchanged: `tests/dr.rs` and `xlog-relcomp-probe` stay green. + +**Disable runs:** +- Dropping the frame check turns 3 tests red. +- Dropping the tile id from the digest turns `tile renamed` red. The first version of the test used only a swap case, which stayed green without the tile id because order alone changes the digest. + +**OPEN:** stored selections (D7'), which need O4: does one `0xF###` value name one stored selection, or a position in a wider basis? diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 0e62185b8..6dc00710f 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. -536 entries, 2026-08-06 .. 2026-10-31. +537 entries, 2026-08-06 .. 2026-11-01. | date | entry id | finding | file | |---|---|---|---| +| 2026-11-01 | `D-DT64-7-5` | | [2026-11-01-maptable-versioned-local-map.md](2026-11-01-maptable-versioned-local-map.md) | | 2026-10-31 | `x2-dt64-admission-policy` | | [2026-10-31-x2-dt64-admission-policy.md](2026-10-31-x2-dt64-admission-policy.md) | | 2026-10-31 | `r1-r2il-binding-reading` | | [2026-10-31-r1-r2il-binding-reading.md](2026-10-31-r1-r2il-binding-reading.md) | | 2026-10-31 | `r1-native-prepared-successor` | | [2026-10-31-r1-native-prepared-successor.md](2026-10-31-r1-native-prepared-successor.md) | diff --git a/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md b/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md index e2ceb78fb..88201948f 100644 --- a/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md +++ b/.claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md @@ -118,6 +118,8 @@ Preserved throughout: the `0xC401` name-bound reading, the `FnIndex` opcode cont ### 1e. O5 design: the versioned global → local table (2026-11-01) +**Status:** core shipped (`dr::MapTable`, T1–T4 green, both disable runs red). Stored selections wait on O4. + O5 is a BindStore plan item (D-DT64-6 Amendment A). Litho is the mental model it came from, not a component. **What exists (VERIFIED-IN-CODE, `lance-graph-dt64/src/dr.rs`):** @@ -145,7 +147,7 @@ So "versions = frame revisions" already works as a mechanism. **The gap:** nothi | Id | Falsifier | |---|---| | T1 | A map read under a frame sealed before `advance` is refused with `Stale(CoordinatesChanged)`, and read under the new seal it succeeds. Twin: an `advance` that changes nothing in a tile still re-seals, so the old frame gets `Stale(FrameResealed)`. | -| T2 | `coordinates` is a function of the held maps. The same maps in the same tiles give the same revision. Reordering one tile's globals changes it. Swapping two tiles' maps changes it, because the `TileId` is in the digest. | +| T2 | `coordinates` is a function of the held maps. The same maps in the same tiles give the same revision. Reordering one tile's globals changes it. Swapping two tiles' maps changes it. Renaming a tile with the same map in the same position changes it; this case alone tests that the `TileId` is in the digest (a disable run showed the swap case passes without it). | | T3 | A frame from another `MapTable` is refused with `Stale(ForeignFrame)`, even at equal revisions. | | T4 | Backward compatibility: existing `LocalMap` / `FrameStore` callers (`tests/dr.rs`, `xlog-relcomp-probe` `litho.rs` and `gate_b.rs`) are unchanged and green. | From 11c48a2343294281c6a229d7591155d77191d62e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 02:02:48 +0000 Subject: [PATCH 4/7] xlog probe: run support and bag count through Quack -> mask-risc (D-DYNBAG-0, step 1) support = ScatterOrU32 per side + mask_and; bag count = GroupReduce Count per side + checked_binary_i64 (TRACKED, MISSING-3). No ndarray fold word left in native.rs. Public API unchanged; gate_b / litho stay the oracles. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/Cargo.toml | 4 + crates/xlog-relcomp-probe/src/native.rs | 163 ++++++++++++++++-------- 2 files changed, 116 insertions(+), 51 deletions(-) diff --git a/crates/xlog-relcomp-probe/Cargo.toml b/crates/xlog-relcomp-probe/Cargo.toml index 283d2b1a2..cca9d5fe7 100644 --- a/crates/xlog-relcomp-probe/Cargo.toml +++ b/crates/xlog-relcomp-probe/Cargo.toml @@ -22,6 +22,10 @@ dr-math-binding-probe = { path = "../dr-math-binding-probe" } ndarray = { git = "https://github.com/AdaWorldAPI/ndarray", branch = "master", default-features = false, features = ["std"] } # DR's global -> local map for the answer axis (lance_graph_dt64::dr::LocalMap). lance-graph-dt64 = { path = "../lance-graph-dt64" } +# D-DYNBAG-0: the description (Quack) and its one evaluator (mask-risc). +# Folds run there, never as direct ndarray::simd calls from this crate. +lance-graph-quack = { path = "../lance-graph-quack" } +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } # XLOG's CUDA-free compiler crates, pinned to one upstream commit # (MIT OR Apache-2.0; notices in the upstream repository). xlog-core = { git = "https://github.com/BrainyBlaze/xlog", rev = "bff6da663308190148c5ce58a715d86525b62e67" } diff --git a/crates/xlog-relcomp-probe/src/native.rs b/crates/xlog-relcomp-probe/src/native.rs index b1ff8f791..4c734c533 100644 --- a/crates/xlog-relcomp-probe/src/native.rs +++ b/crates/xlog-relcomp-probe/src/native.rs @@ -1,36 +1,44 @@ -//! The admitted chain query and its bag count, computed on the -//! `ndarray::simd` polyfill. +//! The admitted chain query and its bag count, described in Quack and +//! evaluated by mask-risc (D-DYNBAG-0, plan `d-dynbag-holographic-bags-v1.md` +//! §17). //! //! This is the execution path of the probe. The DR64 register path //! (`propagate`, over `dr-math-binding-probe::relcomp`) stays as a //! differential cross-check: it answers support only, and it is limited to //! one 64-slot tile. //! -//! Every step is one `ndarray::simd` function, with no loop over rows of our -//! own: +//! Each side of `q(Y) :- r(X, Y), s(Y, Z)` is one table with two `u32` lanes +//! (the free end, the Y end as a local position) and one resident plane (its +//! live rows). Each answer is one Quack `Query`, lowered to one mask-risc +//! `Program` and run by `execute_into`: //! -//! | step | function | -//! |---|---| -//! | a bound end (`X == x`, `Z == z`) | `eq_u32_to_mask` | -//! | the other relation's ends projected onto Y | `mask_scatter_or_u32` (result only) | -//! | forward ∧ backward | `mask_and` | -//! | rows per Y, on each side | `masked_group_count_u32` | -//! | derivations per Y = left count × right count | `checked_binary_i64(Mul)` | +//! | step | Quack | mask-risc terminal | +//! |---|---|---| +//! | a bound end (`X == x`, `Z == z`), or every row | `Filter::cmp(free, EqU32)` / `Filter::plane(live)` | the program's mask | +//! | Y with a partner on one side (support) | `Agg::ScatterOrU32 { fk: y }` | `ScatterOrU32`, the demanded result | +//! | rows per Y on one side (bag count) | `Agg::GroupReduce { Local(y), Count }` | `GroupReduce`, `Out::I64` sized to the Y map | +//! +//! Two calls remain on `ndarray::simd` directly, and neither is a fold: +//! - `mask_and` (forward ∧ backward) is an elementwise alias shared with +//! `lance-graph-onnx` (Amendment C of `d-xlog-native-v1.md`). +//! - `checked_binary_i64(Mul)` (left count × right count per Y) is TRACKED: +//! mask-risc has no elementwise combine of two `i64` sinks yet (§17.5 +//! MISSING-3). A product past `i64` is refused, never wrapped. //! //! The Y domain is DR's: a `lance_graph_dt64::dr::LocalMap` (global id → //! local position), prepared by the caller and never derived here. A Y id the -//! map does not hold is refused. A product past `i64` is refused, never -//! wrapped. +//! map does not hold is refused. //! -//! The only Rust loops here relabel inputs and outputs. They build the key -//! columns from the tuples (one local lookup per row) and decode the answer -//! bits back to ids. Neither is a computation over the population. +//! The only Rust loops here relabel inputs and outputs: they build the key +//! lanes from the tuples (one local lookup per row), the live plane, and decode +//! the answer bits back to ids. None is a computation over the population. use lance_graph_dt64::dr::{LocalMap, MapRefusal}; -use ndarray::simd::{ - I64ArithError, I64Op, checked_binary_i64, eq_u32_to_mask, mask_and, mask_scatter_or_u32, - masked_group_count_u32, +use lance_graph_mask_risc::{ExecError, Foreign, LaneRef, Out, Planes, Scratch, execute_into}; +use lance_graph_quack::{ + Agg, Cmp, Col, Filter, GroupAddr, GroupAgg, LowerError, Mask, Query, lower, }; +use ndarray::simd::{I64ArithError, I64Op, checked_binary_i64, mask_and}; use xlog_core::AggOp; use xlog_ir::{ProjectExpr, RirNode}; @@ -43,6 +51,10 @@ pub enum NativeRefusal { Domain(MapRefusal), /// A per-Y derivation count past `i64`. Count(I64ArithError), + /// Quack refused to lower the description. + Lower(LowerError), + /// mask-risc refused to run the program. + Exec(ExecError), } /// The masks over the Y domain, one bit per local position. @@ -56,10 +68,19 @@ pub struct Support { pub answer: Vec, } -/// One relation's columns: the free end and the Y end as local positions. +/// The free end of a side's rows. +const FREE: Col = Col(0); +/// The Y end of a side's rows, as a local position in DR's map. +const Y: Col = Col(1); +/// The side's live rows. +const LIVE: Mask = Mask(0); + +/// One relation's lanes: the free end and the Y end as local positions, and +/// its live-rows plane. struct Side { free: Vec, y_local: Vec, + live: Vec, } fn side( @@ -73,33 +94,24 @@ fn side( .map(|t| mid.local(u64::from(y_of(t))).map(u32::from)) .collect::>() .map_err(NativeRefusal::Domain)?; + let n = tuples.len(); + let live = (0..n.div_ceil(64)) + .map(|i| { + let rows = (n - i * 64).min(64); + if rows == 64 { + u64::MAX + } else { + (1u64 << rows) - 1 + } + }) + .collect(); Ok(Side { free: tuples.iter().map(free_of).collect(), y_local, + live, }) } -/// The selected rows of one side: all of them, or those whose free end -/// equals the bound. -fn rows(side: &Side, bound: Option) -> Vec { - let n = side.free.len(); - let mut words = vec![0u64; n.div_ceil(64)]; - match bound { - Some(v) => eq_u32_to_mask(&side.free, v, &mut words), - None => { - for (i, w) in words.iter_mut().enumerate() { - let live = (n - i * 64).min(64); - *w = if live == 64 { - u64::MAX - } else { - (1u64 << live) - 1 - }; - } - } - } - words -} - fn sides( left: &[(u32, u32)], right: &[(u32, u32)], @@ -112,6 +124,60 @@ fn sides( )) } +/// The rows of one side the query reads: those whose free end equals the +/// bound, or every live row. +fn selected(bound: Option) -> Filter { + match bound { + Some(v) => Filter::cmp(FREE, Cmp::EqU32(v)), + None => Filter::plane(LIVE), + } +} + +/// Describe, lower and run one query over one side. +fn run(side: &Side, query: &Query, out: Out<'_>) -> Result<(), NativeRefusal> { + let n = side.free.len(); + let masks: [&[u64]; 1] = [&side.live]; + let lanes = [LaneRef::U32(&side.free), LaneRef::U32(&side.y_local)]; + let planes = Planes { + n_rows: n, + masks: &masks, + lanes: &lanes, + }; + let program = lower(query).map_err(NativeRefusal::Lower)?; + let mut scratch = Scratch::for_program(&program, n).map_err(NativeRefusal::Exec)?; + execute_into(&program, &planes, &Foreign::NONE, &mut scratch, out) + .map_err(NativeRefusal::Exec)?; + Ok(()) +} + +/// The Y a side reaches: `ScatterOrU32` over the Y lane, the demanded result. +fn reached(side: &Side, bound: Option, n_y: usize) -> Result, NativeRefusal> { + let mut words = vec![0u64; n_y.div_ceil(64)]; + let query = Query { + filter: selected(bound), + agg: Agg::ScatterOrU32 { + fk: Y, + out_rows: n_y as u32, + }, + }; + run(side, &query, Out::Mask(&mut words))?; + Ok(words) +} + +/// Rows per Y on one side: `GroupReduce` keyed by the Y lane, `Count`. +fn degrees(side: &Side, bound: Option, n_y: usize) -> Result, NativeRefusal> { + let mut counts = vec![0i64; n_y]; + let query = Query { + filter: selected(bound), + agg: Agg::GroupReduce { + key: GroupAddr::Local(Y), + agg: GroupAgg::Count, + }, + }; + run(side, &query, Out::I64(&mut counts))?; + Ok(counts) +} + /// The support of `q(Y) :- r(X, Y), s(Y, Z)` (with optional bounds on X and /// Z) over DR's Y map. pub fn support( @@ -122,12 +188,9 @@ pub fn support( ) -> Result { let (l, r) = sides(left, right, mid)?; let n = mid.len(); - let words = n.div_ceil(64); - let mut forward = vec![0u64; words]; - let mut backward = vec![0u64; words]; - mask_scatter_or_u32(&rows(&l, q.left_bound), &l.y_local, &mut forward, n); - mask_scatter_or_u32(&rows(&r, q.right_bound), &r.y_local, &mut backward, n); - let mut answer = vec![0u64; words]; + let forward = reached(&l, q.left_bound, n)?; + let backward = reached(&r, q.right_bound, n)?; + let mut answer = vec![0u64; forward.len()]; mask_and(&forward, &backward, &mut answer); Ok(Support { forward, @@ -147,10 +210,8 @@ pub fn bag_count( ) -> Result, NativeRefusal> { let (l, r) = sides(left, right, mid)?; let n = mid.len(); - let mut per_left = vec![0i64; n]; - let mut per_right = vec![0i64; n]; - masked_group_count_u32(&rows(&l, q.left_bound), &l.y_local, &mut per_left); - masked_group_count_u32(&rows(&r, q.right_bound), &r.y_local, &mut per_right); + let per_left = degrees(&l, q.left_bound, n)?; + let per_right = degrees(&r, q.right_bound, n)?; let mut out = vec![0i64; n]; checked_binary_i64(I64Op::Mul, &per_left, &per_right, &mut out) .map_err(NativeRefusal::Count)?; From bf56e76c5ee4e18f0f88431d9d6fc803bba05255 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 02:06:45 +0000 Subject: [PATCH 5/7] xlog probe: the admitted MethodBinding drives the bag count (D-DYNBAG-0, step 2) bag_count_admitted runs only from an admitted Bag method whose words the caller reads (MISSING-1, probe-local) and from DR's Y map read under the caller's MapTable frame; a stale frame, an unread word, a Distinct method, or a retracted route (no binding) leaves nothing to run. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/Cargo.toml | 2 + crates/xlog-relcomp-probe/src/native.rs | 63 +++++++- .../xlog-relcomp-probe/tests/dto_binding.rs | 134 ++++++++++++++++++ 3 files changed, 198 insertions(+), 1 deletion(-) diff --git a/crates/xlog-relcomp-probe/Cargo.toml b/crates/xlog-relcomp-probe/Cargo.toml index cca9d5fe7..d8618fe6a 100644 --- a/crates/xlog-relcomp-probe/Cargo.toml +++ b/crates/xlog-relcomp-probe/Cargo.toml @@ -26,6 +26,8 @@ lance-graph-dt64 = { path = "../lance-graph-dt64" } # Folds run there, never as direct ndarray::simd calls from this crate. lance-graph-quack = { path = "../lance-graph-quack" } lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } +# `Population`, read off the admitted `MethodBinding` (D-DYNBAG-0 step 2). +lance-graph-contract = { path = "../lance-graph-contract" } # XLOG's CUDA-free compiler crates, pinned to one upstream commit # (MIT OR Apache-2.0; notices in the upstream repository). xlog-core = { git = "https://github.com/BrainyBlaze/xlog", rev = "bff6da663308190148c5ce58a715d86525b62e67" } diff --git a/crates/xlog-relcomp-probe/src/native.rs b/crates/xlog-relcomp-probe/src/native.rs index 4c734c533..2b0a053c4 100644 --- a/crates/xlog-relcomp-probe/src/native.rs +++ b/crates/xlog-relcomp-probe/src/native.rs @@ -33,7 +33,9 @@ //! lanes from the tuples (one local lookup per row), the live plane, and decode //! the answer bits back to ids. None is a computation over the population. -use lance_graph_dt64::dr::{LocalMap, MapRefusal}; +use lance_graph_contract::set_rules::Population; +use lance_graph_dt64::dr::{Frame, LocalMap, MapRead, MapRefusal, MapTable, TileId}; +use lance_graph_dt64::{AlgebraRef, MethodBinding}; use lance_graph_mask_risc::{ExecError, Foreign, LaneRef, Out, Planes, Scratch, execute_into}; use lance_graph_quack::{ Agg, Cmp, Col, Filter, GroupAddr, GroupAgg, LowerError, Mask, Query, lower, @@ -218,6 +220,65 @@ pub fn bag_count( Ok(out) } +/// The operation a polyfill word stands for, as this probe reads it. The +/// bind store names words by position only; which Quack description a word +/// lowers to is MISSING-1 (plan §17.5), so the caller supplies the reading +/// and any word without one is refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Word { + /// `GroupReduce { Local(y), Count }` over one side. + GroupCount, + /// The checked i64 product of the two per-Y counts (TRACKED, MISSING-3). + MulI64, +} + +/// Why an admitted method was not run. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum BoundRefusal { + /// The method is not a bag count: support is never offered as a count. + NotBag, + /// The method names a word the caller gave no reading for. + UnknownWord(AlgebraRef), + /// The method's steps are not the two-sided count this path computes. + Shape, + /// DR's Y map is not readable under the given frame. + Map(MapRead), + /// The computation itself refused. + Native(NativeRefusal), +} + +/// Run an admitted bag-count method. Execution starts from the +/// `MethodBinding` the bind store admitted, and from DR's Y map read under the +/// caller's frame: no admitted method, or a stale frame, and nothing runs. +/// +/// The method must be `Population::Bag` and its steps must read, in order, +/// [`Word::GroupCount`], [`Word::GroupCount`], [`Word::MulI64`]. +#[allow(clippy::too_many_arguments)] +pub fn bag_count_admitted( + method: &MethodBinding, + words: impl Fn(AlgebraRef) -> Option, + table: &MapTable, + frame: &Frame, + tile: TileId, + q: &ChainQuery, + left: &[(u32, u32)], + right: &[(u32, u32)], +) -> Result, BoundRefusal> { + if method.population != Population::Bag { + return Err(BoundRefusal::NotBag); + } + let steps = method + .effects + .iter() + .map(|e| words(e.algebra).ok_or(BoundRefusal::UnknownWord(e.algebra))) + .collect::, _>>()?; + if steps != [Word::GroupCount, Word::GroupCount, Word::MulI64] { + return Err(BoundRefusal::Shape); + } + let mid = table.map(frame, tile).map_err(BoundRefusal::Map)?; + bag_count(q, left, right, mid).map_err(BoundRefusal::Native) +} + /// Global ids of the set bits of `mask`, in local order. pub fn ids(mid: &LocalMap, mask: &[u64]) -> Vec { (0..mid.len()) diff --git a/crates/xlog-relcomp-probe/tests/dto_binding.rs b/crates/xlog-relcomp-probe/tests/dto_binding.rs index bbaaef9cc..d33082af5 100644 --- a/crates/xlog-relcomp-probe/tests/dto_binding.rs +++ b/crates/xlog-relcomp-probe/tests/dto_binding.rs @@ -418,3 +418,137 @@ fn executing_the_admitted_bag_method_is_refused_in_the_lab_register() { assert_eq!(e.err(), Some(lab::Refusal::BagNeedsMultiplicity)); assert_eq!(rr.len(), SLOTS); } + +// ---------------- D-DYNBAG-0 step 2: the admitted method drives execution + +use lance_graph_dt64::dr::{LocalMap, MapRead, MapTable, Width}; +use xlog_relcomp_probe::ChainQuery; +use xlog_relcomp_probe::native::{BoundRefusal, Word, bag_count_admitted, nonzero}; + +/// MISSING-1, probe-local: the polyfill words this lens names, read as the +/// Quack / tracked operations they stand for. Any other word is refused. +fn word_of(a: AlgebraRef) -> Option { + match a { + GROUP_COUNT => Some(Word::GroupCount), + MUL_I64 => Some(Word::MulI64), + _ => None, + } +} + +const Y_TILE: u32 = 11; + +fn y_table(r: &[(u32, u32)], s: &[(u32, u32)]) -> MapTable { + let ys: Vec = answer_ids(r, s).into_iter().map(u64::from).collect(); + let mut t = MapTable::new(1, 1); + t.advance( + 1, + 1, + vec![(Y_TILE, Some(LocalMap::prepare(Width::W64, &ys).unwrap()))], + ); + t +} + +/// XLOG compiles the fixture; `admit` accepts rule `q`'s body. +fn chain() -> ChainQuery { + let plan = xlog_logic::Compiler::new().compile(MULT).unwrap(); + let body = &plan + .rules_by_scc + .iter() + .flatten() + .find(|r| r.head == "q") + .unwrap() + .body; + xlog_relcomp_probe::admit(body).unwrap() +} + +#[test] +fn the_admitted_method_drives_the_count() { + let (r, s) = fixture(); + let views = Views::new(); + let mut store = bind_store(); + let frames = FrameStore::new(revisions(1)); + let routed = route(&mut store, &frames, answer_ids(&r, &s)); + let b = bind(&store, &frames, &views, &routed).unwrap(); + let table = y_table(&r, &s); + let frame = table.seal(); + let counts = + bag_count_admitted(b.method, word_of, &table, &frame, Y_TILE, &chain(), &r, &s).unwrap(); + let map = table.map(&frame, Y_TILE).unwrap(); + let got: Vec<(u64, i64)> = nonzero(map, &counts); + let want: Vec<(u64, i64)> = b + .expected + .iter() + .map(|(g, c)| (u64::from(g.identity_v2()), *c as i64)) + .collect(); + assert_eq!(got, want, "the binding's expected values, per Y"); +} + +#[test] +fn a_retracted_route_leaves_nothing_to_run() { + let (r, s) = fixture(); + let views = Views::new(); + let mut store = bind_store(); + let frames = FrameStore::new(revisions(1)); + let mut routed = route(&mut store, &frames, answer_ids(&r, &s)); + routed.version = store.retract(7); + // No binding, so no MethodBinding to hand to the executor. + assert!(bind(&store, &frames, &views, &routed).is_err()); +} + +#[test] +fn a_stale_map_frame_is_refused_before_anything_runs() { + let (r, s) = fixture(); + let views = Views::new(); + let mut store = bind_store(); + let frames = FrameStore::new(revisions(1)); + let routed = route(&mut store, &frames, answer_ids(&r, &s)); + let b = bind(&store, &frames, &views, &routed).unwrap(); + let mut table = y_table(&r, &s); + let old = table.seal(); + table.advance(1, 1, vec![]); + assert_eq!( + bag_count_admitted(b.method, word_of, &table, &old, Y_TILE, &chain(), &r, &s), + Err(BoundRefusal::Map(MapRead::Stale( + FrameRefusal::FrameResealed + ))) + ); +} + +#[test] +fn a_method_naming_an_unread_word_is_refused() { + let (r, s) = fixture(); + let views = Views::new(); + let mut store = bind_store(); + let frames = FrameStore::new(revisions(1)); + let routed = route(&mut store, &frames, answer_ids(&r, &s)); + let b = bind(&store, &frames, &views, &routed).unwrap(); + let table = y_table(&r, &s); + let frame = table.seal(); + let only_count = |a: AlgebraRef| (a == GROUP_COUNT).then_some(Word::GroupCount); + assert_eq!( + bag_count_admitted( + b.method, + only_count, + &table, + &frame, + Y_TILE, + &chain(), + &r, + &s + ), + Err(BoundRefusal::UnknownWord(MUL_I64)) + ); +} + +#[test] +fn a_distinct_method_is_not_run_as_a_bag_count() { + let (r, s) = fixture(); + let table = y_table(&r, &s); + let frame = table.seal(); + let mut m = xlog_count(); + m.population = Population::Distinct; + assert_eq!( + bag_count_admitted(&m, word_of, &table, &frame, Y_TILE, &chain(), &r, &s), + Err(BoundRefusal::NotBag) + ); +} From 927f1e86789cf0712859378d5c1f7aed298aa874 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 02:07:57 +0000 Subject: [PATCH 6/7] xlog probe: Intake, Y looked up once under a MapTable frame (D-DYNBAG-0 gate 3) Queries read the intake's lanes and re-check its frame; no lookup after intake (MISSING-5 test). bag_count_admitted now runs over an Intake. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/src/native.rs | 83 +++++++++++++++---- .../xlog-relcomp-probe/tests/dto_binding.rs | 78 ++++++++++------- 2 files changed, 116 insertions(+), 45 deletions(-) diff --git a/crates/xlog-relcomp-probe/src/native.rs b/crates/xlog-relcomp-probe/src/native.rs index 2b0a053c4..07a7f0202 100644 --- a/crates/xlog-relcomp-probe/src/native.rs +++ b/crates/xlog-relcomp-probe/src/native.rs @@ -189,9 +189,12 @@ pub fn support( mid: &LocalMap, ) -> Result { let (l, r) = sides(left, right, mid)?; - let n = mid.len(); - let forward = reached(&l, q.left_bound, n)?; - let backward = reached(&r, q.right_bound, n)?; + support_of(&l, &r, q, mid.len()) +} + +fn support_of(l: &Side, r: &Side, q: &ChainQuery, n: usize) -> Result { + let forward = reached(l, q.left_bound, n)?; + let backward = reached(r, q.right_bound, n)?; let mut answer = vec![0u64; forward.len()]; mask_and(&forward, &backward, &mut answer); Ok(Support { @@ -211,15 +214,68 @@ pub fn bag_count( mid: &LocalMap, ) -> Result, NativeRefusal> { let (l, r) = sides(left, right, mid)?; - let n = mid.len(); - let per_left = degrees(&l, q.left_bound, n)?; - let per_right = degrees(&r, q.right_bound, n)?; + bag_count_of(&l, &r, q, mid.len()) +} + +fn bag_count_of(l: &Side, r: &Side, q: &ChainQuery, n: usize) -> Result, NativeRefusal> { + let per_left = degrees(l, q.left_bound, n)?; + let per_right = degrees(r, q.right_bound, n)?; let mut out = vec![0i64; n]; checked_binary_i64(I64Op::Mul, &per_left, &per_right, &mut out) .map_err(NativeRefusal::Count)?; Ok(out) } +/// Both sides' lanes, built once from the tuples under one `MapTable` frame +/// (plan §17.6 gates 2 and 3). Every query re-checks that frame and reads the +/// lanes; none looks a Y up again. +pub struct Intake { + frame: Frame, + tile: TileId, + n_y: usize, + left: Side, + right: Side, +} + +impl Intake { + /// The one intake: each tuple's Y looked up once in the tile's map, read + /// under `frame`. + pub fn new( + table: &MapTable, + frame: &Frame, + tile: TileId, + left: &[(u32, u32)], + right: &[(u32, u32)], + ) -> Result { + let mid = table.map(frame, tile).map_err(BoundRefusal::Map)?; + let (l, r) = sides(left, right, mid).map_err(BoundRefusal::Native)?; + Ok(Self { + frame: frame.clone(), + tile, + n_y: mid.len(), + left: l, + right: r, + }) + } + + /// The Y map the lanes were built against, if its frame is still current. + pub fn map<'t>(&self, table: &'t MapTable) -> Result<&'t LocalMap, BoundRefusal> { + table.map(&self.frame, self.tile).map_err(BoundRefusal::Map) + } + + /// [`support`] over the intake's lanes. + pub fn support(&self, table: &MapTable, q: &ChainQuery) -> Result { + self.map(table)?; + support_of(&self.left, &self.right, q, self.n_y).map_err(BoundRefusal::Native) + } + + /// [`bag_count`] over the intake's lanes. + pub fn bag_count(&self, table: &MapTable, q: &ChainQuery) -> Result, BoundRefusal> { + self.map(table)?; + bag_count_of(&self.left, &self.right, q, self.n_y).map_err(BoundRefusal::Native) + } +} + /// The operation a polyfill word stands for, as this probe reads it. The /// bind store names words by position only; which Quack description a word /// lowers to is MISSING-1 (plan §17.5), so the caller supplies the reading @@ -247,22 +303,18 @@ pub enum BoundRefusal { Native(NativeRefusal), } -/// Run an admitted bag-count method. Execution starts from the -/// `MethodBinding` the bind store admitted, and from DR's Y map read under the -/// caller's frame: no admitted method, or a stale frame, and nothing runs. +/// Run an admitted bag-count method over an [`Intake`]. Execution starts from +/// the `MethodBinding` the bind store admitted, and the intake re-checks its +/// `MapTable` frame: no admitted method, or a stale frame, and nothing runs. /// /// The method must be `Population::Bag` and its steps must read, in order, /// [`Word::GroupCount`], [`Word::GroupCount`], [`Word::MulI64`]. -#[allow(clippy::too_many_arguments)] pub fn bag_count_admitted( method: &MethodBinding, words: impl Fn(AlgebraRef) -> Option, + intake: &Intake, table: &MapTable, - frame: &Frame, - tile: TileId, q: &ChainQuery, - left: &[(u32, u32)], - right: &[(u32, u32)], ) -> Result, BoundRefusal> { if method.population != Population::Bag { return Err(BoundRefusal::NotBag); @@ -275,8 +327,7 @@ pub fn bag_count_admitted( if steps != [Word::GroupCount, Word::GroupCount, Word::MulI64] { return Err(BoundRefusal::Shape); } - let mid = table.map(frame, tile).map_err(BoundRefusal::Map)?; - bag_count(q, left, right, mid).map_err(BoundRefusal::Native) + intake.bag_count(table, q) } /// Global ids of the set bits of `mask`, in local order. diff --git a/crates/xlog-relcomp-probe/tests/dto_binding.rs b/crates/xlog-relcomp-probe/tests/dto_binding.rs index d33082af5..726be5291 100644 --- a/crates/xlog-relcomp-probe/tests/dto_binding.rs +++ b/crates/xlog-relcomp-probe/tests/dto_binding.rs @@ -423,7 +423,7 @@ fn executing_the_admitted_bag_method_is_refused_in_the_lab_register() { use lance_graph_dt64::dr::{LocalMap, MapRead, MapTable, Width}; use xlog_relcomp_probe::ChainQuery; -use xlog_relcomp_probe::native::{BoundRefusal, Word, bag_count_admitted, nonzero}; +use xlog_relcomp_probe::native::{BoundRefusal, Intake, Word, bag_count_admitted, nonzero}; /// MISSING-1, probe-local: the polyfill words this lens names, read as the /// Quack / tracked operations they stand for. Any other word is refused. @@ -461,6 +461,13 @@ fn chain() -> ChainQuery { xlog_relcomp_probe::admit(body).unwrap() } +fn admitted<'s>(store: &'s mut BindStore, r: &[(u32, u32)], s: &[(u32, u32)]) -> &'s MethodBinding { + let views = Views::new(); + let frames = FrameStore::new(revisions(1)); + let routed = route(store, &frames, answer_ids(r, s)); + bind(store, &frames, &views, &routed).unwrap().method +} + #[test] fn the_admitted_method_drives_the_count() { let (r, s) = fixture(); @@ -470,11 +477,9 @@ fn the_admitted_method_drives_the_count() { let routed = route(&mut store, &frames, answer_ids(&r, &s)); let b = bind(&store, &frames, &views, &routed).unwrap(); let table = y_table(&r, &s); - let frame = table.seal(); - let counts = - bag_count_admitted(b.method, word_of, &table, &frame, Y_TILE, &chain(), &r, &s).unwrap(); - let map = table.map(&frame, Y_TILE).unwrap(); - let got: Vec<(u64, i64)> = nonzero(map, &counts); + let intake = Intake::new(&table, &table.seal(), Y_TILE, &r, &s).unwrap(); + let counts = bag_count_admitted(b.method, word_of, &intake, &table, &chain()).unwrap(); + let got: Vec<(u64, i64)> = nonzero(intake.map(&table).unwrap(), &counts); let want: Vec<(u64, i64)> = b .expected .iter() @@ -498,44 +503,59 @@ fn a_retracted_route_leaves_nothing_to_run() { #[test] fn a_stale_map_frame_is_refused_before_anything_runs() { let (r, s) = fixture(); - let views = Views::new(); let mut store = bind_store(); - let frames = FrameStore::new(revisions(1)); - let routed = route(&mut store, &frames, answer_ids(&r, &s)); - let b = bind(&store, &frames, &views, &routed).unwrap(); + let method = admitted(&mut store, &r, &s).clone(); let mut table = y_table(&r, &s); let old = table.seal(); + let intake = Intake::new(&table, &old, Y_TILE, &r, &s).unwrap(); table.advance(1, 1, vec![]); + let stale = Err(BoundRefusal::Map(MapRead::Stale( + FrameRefusal::FrameResealed, + ))); + assert_eq!( + bag_count_admitted(&method, word_of, &intake, &table, &chain()), + stale + ); + assert_eq!(intake.support(&table, &chain()).err(), stale.err()); assert_eq!( - bag_count_admitted(b.method, word_of, &table, &old, Y_TILE, &chain(), &r, &s), - Err(BoundRefusal::Map(MapRead::Stale( + Intake::new(&table, &old, Y_TILE, &r, &s).err(), + Some(BoundRefusal::Map(MapRead::Stale( FrameRefusal::FrameResealed ))) ); } +/// Gate 3 (MISSING-5): Y is looked up once per tuple at intake; queries read +/// the lanes and look nothing up again. #[test] -fn a_method_naming_an_unread_word_is_refused() { +fn queries_after_intake_do_not_look_y_up_again() { let (r, s) = fixture(); - let views = Views::new(); let mut store = bind_store(); - let frames = FrameStore::new(revisions(1)); - let routed = route(&mut store, &frames, answer_ids(&r, &s)); - let b = bind(&store, &frames, &views, &routed).unwrap(); + let method = admitted(&mut store, &r, &s).clone(); let table = y_table(&r, &s); let frame = table.seal(); + let lookups = || table.map(&frame, Y_TILE).unwrap().lookups(); + let before = lookups(); + let intake = Intake::new(&table, &frame, Y_TILE, &r, &s).unwrap(); + let at_intake = lookups(); + assert_eq!(at_intake - before, (r.len() + s.len()) as u64); + for _ in 0..10 { + bag_count_admitted(&method, word_of, &intake, &table, &chain()).unwrap(); + intake.support(&table, &chain()).unwrap(); + } + assert_eq!(lookups(), at_intake, "no lookup after intake"); +} + +#[test] +fn a_method_naming_an_unread_word_is_refused() { + let (r, s) = fixture(); + let mut store = bind_store(); + let method = admitted(&mut store, &r, &s).clone(); + let table = y_table(&r, &s); + let intake = Intake::new(&table, &table.seal(), Y_TILE, &r, &s).unwrap(); let only_count = |a: AlgebraRef| (a == GROUP_COUNT).then_some(Word::GroupCount); assert_eq!( - bag_count_admitted( - b.method, - only_count, - &table, - &frame, - Y_TILE, - &chain(), - &r, - &s - ), + bag_count_admitted(&method, only_count, &intake, &table, &chain()), Err(BoundRefusal::UnknownWord(MUL_I64)) ); } @@ -544,11 +564,11 @@ fn a_method_naming_an_unread_word_is_refused() { fn a_distinct_method_is_not_run_as_a_bag_count() { let (r, s) = fixture(); let table = y_table(&r, &s); - let frame = table.seal(); + let intake = Intake::new(&table, &table.seal(), Y_TILE, &r, &s).unwrap(); let mut m = xlog_count(); m.population = Population::Distinct; assert_eq!( - bag_count_admitted(&m, word_of, &table, &frame, Y_TILE, &chain(), &r, &s), + bag_count_admitted(&m, word_of, &intake, &table, &chain()), Err(BoundRefusal::NotBag) ); } From dc2099bb480368db521f850238fa1284a40fe543 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 02:09:26 +0000 Subject: [PATCH 7/7] =?UTF-8?q?D-DYNBAG-0:=20gate=206=20pinned;=20plan=20?= =?UTF-8?q?=C2=A717.7=20status,=20board=20entry,=20STATUS=20row?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/board/STATUS_BOARD.md | 2 +- ...1-dynbag-0-xlog-through-quack-mask-risc.md | 26 +++++++++++++++++++ .claude/board/entries/README.md | 3 ++- .claude/plans/d-dynbag-holographic-bags-v1.md | 14 ++++++++++ .../xlog-relcomp-probe/tests/dto_binding.rs | 22 ++++++++++++++++ 5 files changed, 65 insertions(+), 2 deletions(-) create mode 100644 .claude/board/entries/2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 46b673056..bdad85730 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -37,7 +37,7 @@ Plan: `.claude/plans/d-dynbag-holographic-bags-v1.md`. Plan only. | D-id | Deliverable | Status | Gate | |---|---|---|---| -| D-DYNBAG-0 | PR #1884 layering fix: XLOG intake as lanes, support + bag count via Quack → mask-risc, fold oracles, cost columns | Queued | operator go-ahead | +| D-DYNBAG-0 | PR #1884 layering fix: XLOG intake as lanes, support + bag count via Quack → mask-risc, fold oracles, cost columns | In PR: gates 1–7 (plan §17.7); cost columns not done | operator go-ahead (given 2026-11-01) | | D-DYNBAG-1 | ℕ-compose probe: `matmul_i8_to_i32` over two DR64² tiles for `p(X, Z)`; B projection = `relcomp::compose` | Queued | D-DYNBAG-0 | | D-DYNBAG-2 | semiring parameter K (B, ℕ) in relalg `Rel` + Quack surface; typed refusal per (op, K) | Queued | D-DYNBAG-1 | | D-DYNBAG-3 | missing ℕ words backend-first (i64 masked select, min, truncated minus, compare-to-mask, masked sum; maybe bit-packed product) | Queued | D-DYNBAG-2 | diff --git a/.claude/board/entries/2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md b/.claude/board/entries/2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md new file mode 100644 index 000000000..c0c66615c --- /dev/null +++ b/.claude/board/entries/2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md @@ -0,0 +1,26 @@ +# D-DYNBAG-0: the XLOG probe runs through Quack → mask-risc, gated by the bind store + +**Date 2026-11-01 · ID D-DYNBAG-0 · Status IN PR · Plan `.claude/plans/d-dynbag-holographic-bags-v1.md` §17.7 · Crate `crates/xlog-relcomp-probe`** + +- `native.rs` describes each side as a Quack `Query` and runs it with mask-risc `execute_into`: + - support: `ScatterOrU32`, then `mask_and`; + - bag count: `GroupReduce { Local(y), Count }`, then a checked product. +- No `ndarray::simd` fold word is called from the probe. Two direct calls remain, and neither is a fold: `mask_and`, an elementwise alias, and `checked_binary_i64`, TRACKED as MISSING-3. +- `native::Intake` looks Y up once under a `dr::MapTable` frame (#1905). Each query re-checks that frame and performs no further lookup (MISSING-5). +- `bag_count_admitted` runs only from an admitted `Population::Bag` `MethodBinding`, with each word read by the caller (MISSING-1, probe-local). +- Refused: + - a retracted route (it produces no binding); + - a stale frame; + - a word the caller gave no reading for; + - a `Distinct` method; + - `p(X, Z)` (MISSING-6). +- Disable runs, all red: + - Count swapped for Max; + - backward dropped; + - population check removed; + - frame check removed; + - unread word accepted; + - intake frame not re-checked; + - one lookup per query. + +**OPEN:** the cost columns, MISSING-1/2/3/4 in their owner crates, and `crates/lance-graph-xlog` (D-XLOG-NATIVE-4), whose dependencies Amendment C now sets as Quack + mask-risc rather than ndarray only. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 6dc00710f..5cfc663be 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,11 +25,12 @@ 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. -537 entries, 2026-08-06 .. 2026-11-01. +538 entries, 2026-08-06 .. 2026-11-01. | date | entry id | finding | file | |---|---|---|---| | 2026-11-01 | `D-DT64-7-5` | | [2026-11-01-maptable-versioned-local-map.md](2026-11-01-maptable-versioned-local-map.md) | +| 2026-11-01 | `D-DYNBAG-0` | | [2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md](2026-11-01-dynbag-0-xlog-through-quack-mask-risc.md) | | 2026-10-31 | `x2-dt64-admission-policy` | | [2026-10-31-x2-dt64-admission-policy.md](2026-10-31-x2-dt64-admission-policy.md) | | 2026-10-31 | `r1-r2il-binding-reading` | | [2026-10-31-r1-r2il-binding-reading.md](2026-10-31-r1-r2il-binding-reading.md) | | 2026-10-31 | `r1-native-prepared-successor` | | [2026-10-31-r1-native-prepared-successor.md](2026-10-31-r1-native-prepared-successor.md) | diff --git a/.claude/plans/d-dynbag-holographic-bags-v1.md b/.claude/plans/d-dynbag-holographic-bags-v1.md index f3a46961f..d128c34a2 100644 --- a/.claude/plans/d-dynbag-holographic-bags-v1.md +++ b/.claude/plans/d-dynbag-holographic-bags-v1.md @@ -537,6 +537,20 @@ XLOG compile ─► RIR ─► admit / admit_count **REVISIT WHEN:** MISSING-3 or MISSING-4 lands in its owner crate; the TRACKED call is then deleted. +### 17.7 Status (2026-11-01, branch `ccr-85acaff0-oszq40-dynbag0`, on #1905) + +| gate | state | where | +|---|---|---| +| 1 compile → admit → bind → Quack → `lower` → `execute_into` → addressed result | met; a retracted route yields no `MethodBinding`, so nothing runs | `tests/dto_binding.rs` `the_admitted_method_drives_the_count`, `a_retracted_route_leaves_nothing_to_run` | +| 2 no owned tuples after intake | met: `native::Intake` holds `u32` lanes and a live plane; queries read only those | `src/native.rs` | +| 3 no global → local lookup per query (MISSING-5) | met via `dr::MapTable` (#1905): the intake looks Y up once under a sealed frame; each query re-checks the frame | `queries_after_intake_do_not_look_y_up_again`, `a_stale_map_frame_is_refused_before_anything_runs` | +| 4 support and multiplicity distinct | met: support = `ScatterOrU32` ×2 + `mask_and`; bag = `GroupReduce Count` ×2 + checked product; a `Distinct` method is refused as a bag count | `gate_b`, `litho`, `a_distinct_method_is_not_run_as_a_bag_count` | +| 5 disable runs | all red: Count swapped (litho 3 red), backward dropped (gate_b 5 red), population check, frame check, unread word, intake frame re-check, lookup per query (1 red each) | — | +| 6 `q(Y)` never answers `p(X, Z)` (MISSING-6) | met: `admit` and `admit_count` both refuse a `p(X, Z)` body (behaviour that already held, now pinned) | `p_x_z_is_refused_not_answered_by_q_y` | +| 7 no `ndarray::simd` fold word in `native.rs` | met: only `mask_and` (elementwise alias) and `checked_binary_i64` (TRACKED, MISSING-3) | `src/native.rs` module doc | + +MISSING-1 stays probe-local: the caller reads each `AlgebraRef` word as a `native::Word`, and any word without a reading is refused (`BoundRefusal::UnknownWord`). + --- ## 18. Cross-frontend projection crosswalk (2026-10-31, before coding) diff --git a/crates/xlog-relcomp-probe/tests/dto_binding.rs b/crates/xlog-relcomp-probe/tests/dto_binding.rs index 726be5291..9d6e38c66 100644 --- a/crates/xlog-relcomp-probe/tests/dto_binding.rs +++ b/crates/xlog-relcomp-probe/tests/dto_binding.rs @@ -572,3 +572,25 @@ fn a_distinct_method_is_not_run_as_a_bag_count() { Err(BoundRefusal::NotBag) ); } + +/// Gate 6 (MISSING-6): a rule that keeps both ends, `p(X, Z)`, is refused at +/// admission. The per-Y support or count is never offered as its answer. +#[test] +fn p_x_z_is_refused_not_answered_by_q_y() { + let src = MULT.replace( + "q(Y) :- r(X, Y), s(Y, Z).\n?- q(Y).", + "pred p(u32, u32).\np(X, Z) :- r(X, Y), s(Y, Z).\n?- p(X, Z).", + ); + assert_ne!(src, MULT, "the fixture was rewritten"); + let plan = xlog_logic::Compiler::new().compile(&src).unwrap(); + let body = &plan + .rules_by_scc + .iter() + .flatten() + .find(|r| r.head == "p") + .unwrap() + .body; + let refused = xlog_relcomp_probe::admit(body); + assert!(refused.is_err(), "p(X, Z) admitted: {refused:?}"); + assert!(xlog_relcomp_probe::native::admit_count(body).is_err()); +}