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
3 changes: 2 additions & 1 deletion .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@

| D-id | Deliverable | Status | Gate |
|---|---|---|---|
| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 11 Clingo goldens exact; holdings lens with Set/Bag projection; 6 disable runs | In PR | lab only |
| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 11 Clingo goldens exact; holdings lens with Set/Bag projection; 6 disable runs | Shipped (#1873) | lab only |
| D-MIST-NATIVE-1a | HHTL16 Register128 rows replace the name interner: world/proposition/rule nodes as 512-byte rows (16 Morton8x8 columns, identity + up to 15 addresses), classid per population on `RegisterLanes`, accessibility derived from world rows, every compose through `bind_dr64` + `relcomp::Chain`; no String in solved state (compile-time guard); 18 tests + 2 compile_fail doctests; 7 disable runs | In PR | lab only |
| D-MIST-NATIVE-1 | `lance-graph-mistaber`: onnx-shaped ALIAS/INLINE/REFUSE facade (plan §3) | Queued | production home for `compose` (plan Q1) |
| D-MIST-NATIVE-2 | lineage origins into `SupportLedger` (`EvidenceSourceId`, `TextAttested`) | Queued | after D-MIST-NATIVE-1 |
| D-MIST-NATIVE-3 | axes past 64 (worlds, propositions, rules) | Queued | refused today |
Expand Down
12 changes: 12 additions & 0 deletions .claude/board/entries/2026-10-30-d-mist-native-1a-hhtl16-rows.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# 2026-10-30 — D-MIST-NATIVE-1a: HHTL16 Register128 rows replace the name interner

**Status:** LAB, measured by tests. Plan: `.claude/plans/d-mistaber-native-v1.md` §9.

- The Kripke probe holds no String in its solved state. World, proposition and rule nodes are 512-byte rows in the HHTL16 format: Register0/Register1, 16 Morton8x8 columns, column 0 the identity, columns 1..=15 addresses.
- The classid is per population, on `RegisterLanes`; the row bytes carry none.
- Accessibility is derived from world rows, and a 16th parent is refused.
- `holds ∘ children` goes through `bind_dr64` and `relcomp::Chain`.
- 11 goldens exact; 18 tests and 2 `compile_fail` doctests; 7 disable runs red.
- Known limit: the binding is a typing guard, so swapping `Chain` for raw `compose` turns nothing red. Only the mistyped-signature disable (D4) shows the path is live.

STATUS: measured | OUTCOME: Mistaber nodes as HHTL16 rows, no Strings, typed DR64 binding | OPEN: whether the row key also carries the address; real concept ids from the OGAR codebook.
3 changes: 2 additions & 1 deletion .claude/board/entries/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,14 +25,15 @@ 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.

512 entries, 2026-08-06 .. 2026-10-30.
513 entries, 2026-08-06 .. 2026-10-30.

| date | entry id | finding | file |
|---|---|---|---|
| 2026-10-30 | `D-XLOG-NATIVE-0` | | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) |
| 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) |
| 2026-10-30 | `D-TRACT-SHAPE-1` | | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) |
| 2026-10-30 | `D-TRACT-HARVEST-0` | | [2026-10-30-d-tract-harvest-0-native-algebra-bridge.md](2026-10-30-d-tract-harvest-0-native-algebra-bridge.md) |
| 2026-10-30 | `D-MIST-NATIVE-1a` | | [2026-10-30-d-mist-native-1a-hhtl16-rows.md](2026-10-30-d-mist-native-1a-hhtl16-rows.md) |
| 2026-10-30 | `D-MIST-NATIVE-0` | | [2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md](2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md) |
| 2026-10-30 | `D-LITHO` | | [2026-10-30-d-litho-photolithography-contract.md](2026-10-30-d-litho-photolithography-contract.md) |
| 2026-10-30 | `D-LITHO-1` | | [2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md](2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md) |
Expand Down
39 changes: 38 additions & 1 deletion .claude/plans/d-mistaber-native-v1.md
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ A lens row is one (mode, source rule), or one (mode) with empty rule fields when

## 5. Evidence (D-MIST-NATIVE-0)

`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 12 tests.
`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 18 tests + 2 doctests (since §9).

Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, F6-undeclared-child, C-mammal-C2/C4/C6/C6i, E-xlog-plain/override. All are exact, compared as sorted lists, so a duplicate atom would also fail.

Expand Down Expand Up @@ -129,3 +129,40 @@ Contracting V or O over the third axis (OR over `z`) gives the `holds` register
So "the third axis is a relation ordinal" covers L and not V or O. Closing NFR-OP-2 stays the DR owner's decision.

**Size.** Dense, each cube is 32 KiB of bits, 96 KiB for the three. The probe stores only O and L, and only as many slices as there are worlds and rules. V is never stored, because every V slice is one `compose` row read. Nothing here allocates a cube.

## 9. D-MIST-NATIVE-1a: HHTL16 rows replace the name interner (2026-10-30)

**Status:** LAB, in PR. The probe holds no names in its solved state. Names live only in `src/membrane.rs`, which parses the goldens and renders atoms.

- **Rows** (`src/rows.rs`). World, proposition and rule nodes are 512-byte `NodeRow`s in the HHTL16 opt-in format. `Register0` holds the x bytes and `Register1` the y bytes. Column k is `Morton8x8::from_xy(R0[k], R1[k])`. Column 0 is the node's identity; columns 1..=15 are addresses, which for a world are its parents. Address = first-appearance ordinal + 1, so no two collide and none is unbound.
- **Classid per population.** Each population is bound once: `Activation` → `resolve_for_context(concept, Register128 slab)` → `bind_register128(Two)`. The concept lives on `RegisterLanes::concept()`. The key, edges and value bytes carry no classid. Concepts are lab stand-ins `0x7F11..13`; none is minted.
- **Accessibility is derived** from world rows (`Kb::derive_children`, its only writer). A 16th parent is refused with `TooManyParents { parents }`. Global address → local 0..64 goes through `hhtl16::LocalMap`, which refuses a 65th node, a duplicate or an unmapped address.
- **Binding.** The accessibility register and the three input registers are bound through `bind_dr64`. Every `holds ∘ children` step runs through `relcomp::Chain::new(..).eval(..)`. The fixpoint and lineage algebra are unchanged.
- **No-String guard.** A doc-hidden `AddressOnly` trait plus an exhaustive destructure of `Kb`, `Holdings`, `Mode` and `Population`. A String field fails to compile, and two `compile_fail` doctests show the bound can fire.

**Tests:** 18 tests and 2 doctests. All 11 goldens stay exact. New tests cover:

- rows round-tripping through `get`/`set`;
- a two-parent world deriving the old accessibility;
- the 16th parent being refused;
- the classid being on the lanes and not in the rows;
- `LocalMap` refusals.

**Disable runs** (committed first, each then broken, red, restored):

| # | breakage | red |
|---|---|---|
| D1 | read only parent column 1 | goldens, diamond Set/Bag, two-parent derivation, contraction, classid test |
| D2 | truncate parents instead of refusing | `a_16th_parent_is_refused` (`left: None`) |
| D3 | classid minted into the key | `the_classid_lives_on_the_lanes_not_in_the_rows` |
| D4 | accessibility signature typed Property × Identity | 12 tests (the `Chain` typing refuses `holds ∘ children`) |
| D5 | address without `+1` | round-trip, goldens and 7 others |
| D6 | accessibility orientation reversed | goldens, orientation, contraction and 5 others |
| D7 | a `NameTable` field on `Kb` | compile errors E0063 and E0027 (exhaustive destructure) |

Known limit: replacing `hop` with raw `compose` turns nothing red. The binding is a typing guard, not semantics, and D4 is the only proof that the path is live.

**Open (operator):**

- the row key is all zero, so identity exists only in column 0. Should the key also carry the address?
- a real binding takes concept ids from the OGAR codebook through hotplug.
Loading
Loading