Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .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 Down
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?
3 changes: 2 additions & 1 deletion .claude/board/entries/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
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
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)
);
}
Loading