From e5ac9caa76a719bbc0724dc1846e5d529696e8c7 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 01:51:05 +0000 Subject: [PATCH 1/3] 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/3] 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/3] =?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. |