From 7edff4ae01e88d4c0720cddb45003f8d2913e447 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 6 Nov 2026 08:08:38 +0000 Subject: [PATCH] plan: D-LANESOCK DR x DT64 property-to-lane socket and joint version witness Normative spec for binding ClassId + SchemaRev + field position to a source-owned lane and its coordinate space (LaneSource), and for a joint witness that checks the DT64 class route and the DR source frame as an explicit pair (LaneBinding). Lists every refusal, including CoordinateSpace for a lane whose row order differs from the selection mask's. No store, clock, index or writer is added; admissions unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMMJzKZrYnckXRC8x2U --- .claude/board/INTEGRATION_PLANS.md | 5 + .claude/board/STATUS_BOARD.md | 7 ++ .../d-lanesock-dr-dt64-lane-socket-v1.md | 95 +++++++++++++++++++ 3 files changed, 107 insertions(+) create mode 100644 .claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 85df23b6d..3a3623658 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,8 @@ +## 2026-11-06 — D-LANESOCK: DR × DT64 property-to-lane socket and joint version witness → `.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md` + +**Status:** NORMATIVE SPEC (D-LANESOCK-0); implementation D-LANESOCK-1 is a separate draft PR. **Board:** [STATUS_BOARD](STATUS_BOARD.md) D-LANESOCK. Follows #1964/#1965 and OGAR#371. +**Confidence:** every type and refusal is mapped onto existing `BindStore`, `FrameStore`, `RouteLog`, `ClassView` and `WideFieldMask` APIs; nothing measured yet. + ## 2026-11-04 — D-DRIVER-ZC-0: virtual access driver instead of 17,000 per-call copy audits **Status:** PROPOSED / DOCS ONLY. [Master](../plans/d-driver-zc-virtual-bus-contract-v1.md) · [staged PR charter](../plans/d-driver-zc-staged-pr-charter-v1.md) · [47 falsifiers](../plans/d-driver-zc-falsifier-matrix-v1.md) · [board entry](entries/2026-11-04-d-driver-zc-0-virtual-bus-contract.md) · [STATUS_BOARD](STATUS_BOARD.md) D-DRIVER-ZC · [EXO-154](https://linear.app/exo-red/issue/EXO-154) / [EXO-153](https://linear.app/exo-red/issue/EXO-153) / [EXO-50](https://linear.app/exo-red/issue/EXO-50). **Architecture move:** apply ndarray SIMD polyfill's facade-and-parity law to a single local/foreign/data-owner *address-access membrane*. Five virtual XX/XY/XZ/YY/ZZ lenses share one witnessed canonical SoA address; typed ClassView and Quack/mask-risc/ndarray execute without default copied values/row reconstruction. BIND→PROJECT→STREAM→EXECUTE→RELEASE; strict local borrow vs disk ingress vs remote message distinction; no new ISA/ALU/hash index or driver runtime. Co-addressed selections and once-per-frame routing first; foreign hops remain EXO-46/89/151/140-gated; D4/S-INGRESS and oracle-lifetime owners open. A 47-case matrix separates semantic results, representation bytes, reachability enforcement and end-to-end economics. #1953/#1955/#1956 already merged; the 8 ZC stages are independent, only ZC-0 documented now. "Thinking Hard Drive" is a proposed restricted theorem schema, not an assertion that disks perform computation or every query takes O(1). **Explicit defer:** no cognitive-shader-driver/Ladybug/P64/StreamDTO/BusDTO/PerturbationDTO stack investigation or consolidation during this PR. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 2558e5ca2..ab8027124 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,10 @@ +## D-LANESOCK — DR × DT64 property-to-lane socket (2026-11-06) + +| D-id | Deliverable | State | +| --- | --- | --- | +| D-LANESOCK-0 | normative spec: socket, joint version witness, refusals | In PR | +| D-LANESOCK-1 | `LaneSource` + `BindStore::bind_lanes` + falsifiers in lance-graph-dt64 and the dir-sim lab | Queued | + ## D-CGMM — Lazy Codegraph fact/demand + MeTTa class-method scratch (2026-11-04) **Implementation detail update (2026-11-04):** [Source→native blueprint](../plans/d-cgmm-implementation-blueprint-v1.md), [EXO gate ledger](../plans/d-cgmm-exo-gates-v1.md) and [fixed independent fixtures](../plans/d-cgmm-executable-fixtures-v1.md) refine the eight future stages. All executable fixtures are **NOT_RUN**, with expected pure COUNT=2 and tenant-A Set=3/Bag=4. The only authorized artifact is docs in draft PR #1958; owners of EXO-121/152/46/140/95/108/73 remain open gates. diff --git a/.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md b/.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md new file mode 100644 index 000000000..8a9f0e761 --- /dev/null +++ b/.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md @@ -0,0 +1,95 @@ +# D-LANESOCK — DR × DT64 property-to-lane socket and joint version witness + +**Status:** NORMATIVE SPEC (D-LANESOCK-0). Implementation D-LANESOCK-1 is a separate draft PR. +**Date:** 2026-11-06. +**Follows:** #1964 / #1965 (hybrid ordinal chain; batch selection over OGAR Ruler planes), AdaWorldAPI/OGAR#371. + +## 0. Ownership (unchanged) + +| Layer | Owns | Never owns | +|---|---|---| +| SoA64K | the canonical lanes and their values | a second lane universe | +| DR (`lance_graph_dt64::dr`) | positions, `RouteLog`, `FrameStore`/`Frame`, `MapTable`, `Guards` | values, method meaning | +| DT64 (`BindStore`) | `ClassSchema`/`SchemaRev`, method bindings, `MethodRef` admission, the route log it keeps | values, physical lane addresses | +| `ClassView` | the field basis (`FieldRef` order) and labels | a physical address | +| `WideFieldMask` | which properties are requested | a row-survivor bit | +| Quack → mask-RISC → ndarray | admitted execution over borrowed lanes | identity, routing, schema | +| Source owner (dir-sim, SAP adapter, ...) | which of its lanes holds which property, in whose row order | DT64 schema | + +The socket adds no store, no clock, no index and no writer. + +## 1. Gap this closes + +1. Nothing maps `(classid, SchemaRev, field position)` to a source-owned lane and the coordinate space that lane is in. +2. `BindStore` owns a private `RouteLog` with its own clock; `FrameStore` has another. Nothing relates a class route to a source frame, and nothing may assume they are one clock. + +## 2. The socket (implemented by the source owner) + +```rust +/// Whose row order a lane is in. +pub struct CoordSpace { pub population: u64, pub coordinates: u64 } + +/// A source-owned lane: address, row order, and the reader scope it serves. +/// No value. +pub struct LaneAddr { pub space: CoordSpace, pub lane: u16, pub scope: Scope } + +pub trait LaneSource { + type Lane<'a> where Self: 'a; // the borrowed lane (e.g. mask-RISC LaneRef) + fn lane_of(&self, class: u32, rev: SchemaRev, field: u8, frame: &Frame) -> Option; + fn borrow(&self, addr: &LaneAddr) -> Option>; +} +``` + +`None` from `lane_of` is UNBOUND and is refused, never read as empty. `borrow` hands out the source's own lane; it never copies, reorders or allocates a lane. + +## 3. The joint witness (DT64) + +```rust +pub struct RouteAt { pub position: u16, pub version: RouteVersion } + +BindStore::bind_lanes(view, frames, source, LaneRequest { + route: RouteAt, rev: SchemaRev, fields: &WideFieldMask, + frame: &Frame, scope: Scope, selection: CoordSpace, +}) -> Result + +LaneBinding::check(&self, store, view, frames, source) -> Result<(), LaneRefusal> // hot, no allocation +LaneBinding::lane(&self, store, view, frames, source, field) -> Result, LaneRefusal> +``` + +`LaneBinding` carries the class, `SchemaRev`, `RouteAt`, the sealed `Frame`, the reader `Scope`, the selection `CoordSpace` and one `LaneAddr` per requested field. It holds no value. + +**Versions are a pair, never a merged clock.** The route is checked against `BindStore`'s own log (`routed_at(current_version, position)` must still be the bound class). The frame is checked against the `FrameStore` that issued it. Each refuses on its own. Sharing a `VersionClock` remains an owner's construction choice and is not required. + +## 4. Refusals (exhaustive) + +| Condition | Refusal | +|---|---| +| unknown class, unrouted position, future version, schema revision or field basis changed | `LaneRefusal::Bind(Refusal::…)` (existing) | +| class re-routed since the bind | `RouteChanged { position, bound, now }` | +| foreign, stale (source / map / coordinates) or re-sealed frame | `Frame(FrameRefusal::…)` (existing) | +| requested field outside the class basis | `FieldNotInBasis { class, field }` | +| source declares no lane for the field | `Unbound { class, field }` | +| lane row order ≠ selection row order | `CoordinateSpace { field, selection, lane }` | +| lane scope ≠ reader scope | `Scope { field, reader, lane }` | +| source's mapping changed since the bind | `MappingChanged { field }` | +| source no longer holds the lane | `Vanished { field }` | + +`CoordinateSpace` is the guard that stops an AD-slot row mask reading an Entra-order lane. No mapping is admitted today to lift it; when one is, it is named here and owned by DR, not by the socket. + +## 5. Consumers + +- **PSCustomObject-shaped projection.** Row mask (Quack `Agg::Rows`) × `WideFieldMask` × `LaneBinding::lane` per field; labels from `ClassView`. No row object. +- **XVERWEIS.** A DT64 `MethodRef`, admitted by `BindStore::admit`; its `reads` must be inside the binding's fields. The method pointer is not the coordinate; the coordinate is not the value. Across coordinate spaces it refuses (`CoordinateSpace`) until a gather is admitted. +- **Quack masked selection and typed folds.** `QueryPlanes.lanes` filled from `LaneBinding::lane`; `Filter`/`Agg` as today. + +## 6. Admissions unchanged + +Gather ban, ADMISSION B, NotASide, OP-14, DRISA M1/M2, D4/S-INGRESS. The socket is read-side only. + +## 7. Falsifiers (D-LANESOCK-1) + +1. Two properties resolved through one `ClassView` basis; one `WideFieldMask` selects both. +2. DR routes the class under a witnessed frame. +3. A DT64-admitted method drives one Quack fold over a borrowed lane; the same binding drives a second operation on the other lane. +4. Independent scalar oracle parity; zero hot allocations. +5. Each refusal in §4 fires on a realistic input, and a disabled guard turns its test red.