Repository navigation
dt64: D-LANESOCK-1 property-to-lane socket and joint route/frame witness - #1967
Merged
Merged
Conversation
…CK-1) LaneSource is implemented by a source owner: it maps (classid, SchemaRev, field position) to a LaneAddr (lane, coordinate space, reader scope) and lends its own lane. BindStore::bind_lanes resolves the class at a route, checks the basis and the frame, and takes one lane per requested field into a LaneBinding that holds addresses only. LaneBinding::check revalidates route (against the store's current version), frame, basis and mapping without allocating. Refuses: schema/basis/route errors, a re-route, foreign or stale frames, fields outside the basis, unbound fields, a lane in another row order than the selection (CoordinateSpace), another reader scope, a changed mapping and a vanished lane. dir-sim lab: two AD-owned property lanes bound through one ClassView basis, folded with Quack under the Ruler-plane selection (oracle parity), an Entra-order lane refused under the AD selection, reorder refusal, and zero hot allocations at 64K slots. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMJzKZrYnckXRC8x2U
…me the socket alone The scan oracle is quadratic at 64K slots; its parity stays pinned at 300 slots across three seeds. Reports check+borrow separately from the fold. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMJzKZrYnckXRC8x2U
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMJzKZrYnckXRC8x2U
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
|
AdaWorldAPI
marked this pull request as ready for review
November 6, 2026 08:55
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
AdaWorldAPI
pushed a commit
that referenced
this pull request
Nov 6, 2026
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMJzKZrYnckXRC8x2U
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Implements D-LANESOCK-1 from the merged spec (#1966,
.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md). The code lives inlance-graph-dt64(src/lane.rs). The crate still depends only on the zero-dependency contract crate.LaneSource, implemented by the source owner.(classid, SchemaRev, field position)to aLaneAddr: the lane, itsCoordSpace(whose row order the lane is in) and the readerScopeit serves.type Lane<'a>), for example mask-RISCLaneRef. dt64 never names mask-RISC.BindStore::bind_lanes(cold), producing aLaneBindingthat holds addresses only.FrameStore.SchemaRev, then takes one lane per field of theWideFieldMask.LaneBinding::check/lane(hot, no allocation). They re-check route, frame, basis and mapping, then borrow the lane.BindStore's own log, the frame against theFrameStorethat issued it. No merged clock is introduced.Refusals: the existing
RefusalandFrameRefusalarms, plus:RouteChanged,FieldNotInBasis,Unbound;CoordinateSpace: a lane in another row order than the selection;Scope,MappingChanged,Vanished,NotBound.Not changed: no store, clock, GUID index, writer or per-row DTO. The Gather ban, ADMISSION B, NotASide, OP-14, DRISA M1/M2 and D4/S-INGRESS are untouched. Cross-space reads refuse; no mapping is admitted.
Proof
lance-graph-dt64/tests/lane_socket.rs(8 tests):ClassViewbasis are bound and borrowed;ptr::eqshows the lanes are the source's own slices, not copies;CoordinateSpacerefusal, and that the same field binds under its own row order;SchemaRevand a changed basis;MapChanged);dir-sim lab,
tests/ordinal_chain_lab.rs(4 new tests, 19 total):WideFieldMask. Over three seeds:MethodRef(itsreadsnames the lane) drivesAgg::SumI32;confirmed ∧ cost > 150→Agg::Count;CoordinateSpace.CoordinatesChanged), and a rebind under the new frame works.Disable runs (committed first, each guard removed, then restored); each turns its named test red:
check;check;Measured (release, 64K slots; reported, not gated)
SumI32over a 64Ki32laneChecks run
cargo clippy -p lance-graph-dt64 --all-targets -- -D warnings: clean.cargo test -p lance-graph-dt64: all green.-D warnings): clean. Lab tests: 19/19. fmt: clean.Board
STATUS_BOARD.md: D-LANESOCK-0 Shipped (plan: D-LANESOCK — DR × DT64 property-to-lane socket and joint version witness #1966), D-LANESOCK-1 In PR.LATEST_STATE.mdcontract-inventory line is added after merge, per that file's convention.Generated by Claude Code