Skip to content
Merged
4 changes: 2 additions & 2 deletions .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -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, a BindStore plan item (Litho is a mental model, folded into the bind store plan as D-DT64-6 Amendment A) | Queued | O5 (taken by this session) |
| D-DT64-7-5 | the versioned global → local table, a BindStore plan item (plan §1e; Litho is a mental model, folded into the bind store plan as D-DT64-6 Amendment A) | 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)

Expand All @@ -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 |
Expand Down
Original file line number Diff line number Diff line change
@@ -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.
15 changes: 15 additions & 0 deletions .claude/board/entries/2026-11-01-maptable-versioned-local-map.md
Original file line number Diff line number Diff line change
@@ -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?
4 changes: 3 additions & 1 deletion .claude/board/entries/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,10 +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.

536 entries, 2026-08-06 .. 2026-10-31.
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) |
Expand Down
37 changes: 37 additions & 0 deletions .claude/plans/d-dt64-7-behaviour-addressing-registration-v1.md
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,43 @@ 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`):**

| 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. 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. |

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
Expand Down
14 changes: 14 additions & 0 deletions .claude/plans/d-dynbag-holographic-bags-v1.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
95 changes: 95 additions & 0 deletions crates/lance-graph-dt64/src/dr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<TileId, LocalMap>,
}

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<TileId, LocalMap>) -> 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<LocalMap>)>,
) {
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]
Expand Down
81 changes: 81 additions & 0 deletions crates/lance-graph-dt64/tests/dr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -159,3 +159,84 @@ 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");
// 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]
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)
);
}
6 changes: 6 additions & 0 deletions crates/xlog-relcomp-probe/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,12 @@ 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" }
# `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" }
Expand Down
Loading
Loading