Repository navigation
contract: Register128 slab reading + classid-free register rails; bounded power sums end to end (D-LXC-29) #1324
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
58c1c72
contract: Register128 slab reading and two classid-free register rail…
claude e723858
jc: end-to-end Register128 bounded stats test (D-LXC-29)
claude 7654e34
board: D-LXC-29 Register128 + bounded power sums entry, status row, c…
claude 1f9a909
board: give the Register128 entry its own id D-LXC-29-R (entries inde…
claude 0a7fffb
contract: count Register128 rail writes against their tenant
claude 347096d
contract: keep Register0 writes to the counter test only
claude File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
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
86 changes: 86 additions & 0 deletions
86
.claude/board/entries/2026-10-04-register128-bounded-power-sums.md
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,86 @@ | ||
| # 2026-10-04 — Register128: classid-free 128-bit register + bounded power sums as its first consumer (D-LXC-29-R) | ||
|
|
||
| ## DECISION (operator ruling, 2026-10-04) | ||
|
|
||
| - **DECISION:** alternative 2, carried to a live consumer. A slab may declare the physical reading `SlabReading::Register128` (tag 1). Its bytes are 128 raw bits with no classid inside. | ||
| - **SCOPE:** | ||
| - The concept comes from the SPOG context, resolved through `Activation::resolve_for_context` and handed back by `RegisterLanes::concept()`. | ||
| - Facet96 (tag 0) is untouched, and none of its bytes are reused. | ||
| - `TurbovecResidue` is not used. | ||
| - #1323's logical APIs are unchanged. | ||
| - **BASIS:** "classid-free" means not embedded in the payload; it does not mean semantically untyped. | ||
| - **REVISIT WHEN:** a consumer needs more than two rails, or the rails collide with a future tenant. | ||
|
|
||
| ## What landed | ||
|
|
||
| **lance-graph contract (`58c1c72`)** | ||
| - `SlabReading::Register128 = 1`; tags 2, 3, 0x80 and 0xFF still fail closed. | ||
| - `ValueTenant::Register0` and `ValueTenant::Register1`, each 16 bytes: | ||
| - row bytes [252,268) and [268,284), value offsets 220 and 236; | ||
| - appended after `EpisodicBasin` and included in `ValueSchema::Full` only; | ||
| - the `BoardAggregates` reservation re-bases from ordinal 16 to 18. | ||
| - `register128.rs`: | ||
| - `Register128([u8;16])`, read as 4 LE `u32` words; | ||
| - `RegisterRails::{One, Two}`; | ||
| - `RegisterLanes`, which is `Copy`, holds only numbers, and offers `get`/`set` per rail. | ||
| - `ResolvedReading::bind_register128(rails)`: | ||
| - checked once per population; | ||
| - refuses a non-Register128 slab (`NotRegister128`); | ||
| - refuses a schema without the rails (`RegisterRailAbsent`). | ||
| - **`ENVELOPE_LAYOUT_VERSION` is NOT bumped.** Appended tenants are layout-preserving (same precedent as earlier appends), and a bump would make every existing Facet96 slab fail closed. | ||
|
|
||
| **ndarray (`eeb911b`, plus bench)** | ||
| - `BOUNDED_TILE_ROWS = 65,536`, with a compile-time proof that `255² · 2^16 < 2^32`. | ||
| - `masked_group_bounded_power_sums_u8{,_via,_pair}`: | ||
| - register layout `[n, Σx, Σx², reserved]`; | ||
| - word 3 is never read or written. | ||
| - `masked_group_bounded_cross_power_sums_u8{,_via,_pair}`, on two rails: | ||
| - rail0 = `[n, Σx, Σx², ·]`, identical to the univariate register; | ||
| - rail1 = `[Σy, Σy², Σxy, ·]`; | ||
| - so `n` is stored once. | ||
| - All six go through the existing `group_walk`, so lane, via and pair semantics and the drop rules are those of the `i32` kernels. | ||
| - `widen_bounded_{,cross_}power_sums` give the exact `PowerSums` / `CrossPowerSums`. | ||
| - `fold_bounded_{,cross_}power_sums_tiles` cut a population into tiles of at most 2^16 rows and `checked_merge` each tile. A tile is refused whole if any group's merge would overflow. | ||
| - A tile over the bound returns `TileTooLarge` before any write. | ||
|
|
||
| **jc end-to-end (`e723858`)** | ||
| - The context is resolved and both rails bound once. | ||
| - A four-tile population is folded through ndarray. | ||
| - Each tile's registers are stored per group into `NodeRow` rails, then read back, widened and merged. The result equals the wide `i32` path, univariate and bivariate. | ||
| - A Facet96 or undeclared slab never binds. | ||
|
|
||
| ## Proofs (each disable-verified red, then restored) | ||
|
|
||
| | claim | test | disable | | ||
| |---|---|---| | ||
| | rails only for a Register128 slab + Full schema | `register_rails_are_granted_only_to_a_register128_slab` | slab check removed; rail-presence check removed | | ||
| | concept from context, never payload | `a_register_takes_its_concept_from_the_context_never_the_payload` | — | | ||
| | 65,536 × 255 fits exactly | `the_full_bound_at_u8_max_fits_exactly` | — | | ||
| | 65,537 rows refused, nothing written | `one_row_past_the_bound_is_refused_before_any_write` | bound guard removed → red | | ||
| | narrow → widen exact, lane/via/pair | `narrow_then_widen_…`, `bivariate_narrow_then_widen_…` | widen word swapped → red (3 tests) | | ||
| | tiles + checked_merge == whole | `partitioned_tiles_merge_to_the_whole` | merge replaced by overwrite → red | | ||
| | overflowing tile commits nothing | `an_overflowing_merge_commits_nothing_of_the_tile` | check fused into commit loop → red | | ||
|
|
||
| ## MEASURED (AVX-512 host, `avx512f=true`, release, 16 groups, median of 31 runs, ns/row) | ||
|
|
||
| | case | wide i32 | bounded u8 | ratio | | ||
| |---|---|---|---| | ||
| | univariate tile=4096 | 1.448 | 1.094 | 1.32 | | ||
| | bivariate tile=4096 | 3.032 | 1.921 | 1.58 | | ||
| | univariate tile=16384 | 1.445 | 1.095 | 1.32 | | ||
| | bivariate tile=16384 | 3.010 | 1.906 | 1.58 | | ||
| | univariate tile=65536 | 1.432 | 1.095 | 1.31 | | ||
| | bivariate tile=65536 | 3.264 | 1.911 | 1.71 | | ||
| | univariate tiled n=1,048,699 | 1.514 | 1.205 | 1.26 | | ||
| | bivariate tiled n=1,048,699 | 3.477 | 2.133 | 1.63 | | ||
|
|
||
| - These are single-host, single-session numbers. AVX2 and NEON were not measured. | ||
| - Input is 1 byte per lane against 4 for the wide path. | ||
| - The wide path is timed on pre-widened `i32` lanes, so the conversion cost the bounded path avoids is not included. | ||
|
|
||
| ## OPEN | ||
|
|
||
| - **Zero-copy strided writes:** the kernel writes a compact `&mut [[u8;16]]` working set (one register per group). These are stored to rows per group via `RegisterLanes::set`, not strided into `NodeRow` in place. | ||
| - **No production call site yet:** the mask-risc terminal for the bounded fold is not wired. | ||
| - **Declaration storage:** where `SlabDeclaration` lives in the metadata envelope, and the writer that persists it. | ||
| - **Unmeasured tiers:** AVX2, NEON and wasm timings. |
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,204 @@ | ||
| //! D-LXC-29 end to end: a SPOG context resolves a `Register128` slab ONCE, | ||
| //! binds its rails ONCE, and bounded power sums fold tile by tile through | ||
| //! `ndarray::simd` into those rails — then widen losslessly to the exact | ||
| //! `PowerSums` / `CrossPowerSums` the wide `i32` kernels produce. | ||
| //! | ||
| //! jc is the one crate that already sees both sides (ndarray as a dependency, | ||
| //! the contract as a dev-dependency), so the cross-crate proof lives here and | ||
| //! no production crate gains a dependency. | ||
|
|
||
| use lance_graph_contract::canonical_node::{NodeGuid, NodeRow, ReadMode, ValueSchema}; | ||
| use lance_graph_contract::hotplug::{Activation, ActivationDrift, SlabDeclaration, SlabReading}; | ||
| use lance_graph_contract::register128::{Register128, RegisterLanes, RegisterRails}; | ||
| use lance_graph_contract::soa_envelope::ENVELOPE_LAYOUT_VERSION; | ||
| use ndarray::simd::{ | ||
| fold_bounded_cross_power_sums_tiles, fold_bounded_power_sums_tiles, | ||
| masked_group_bounded_cross_power_sums_u8, masked_group_bounded_power_sums_u8, | ||
| masked_group_cross_power_sums_i32, masked_group_power_sums_i32, CrossPowerSums, PowerSums, | ||
| BOUNDED_TILE_ROWS, | ||
| }; | ||
|
|
||
| const CONCEPT: u16 = 0x0901; | ||
| const GROUPS: usize = 7; | ||
|
|
||
| fn activation() -> Activation { | ||
| Activation::new( | ||
| Vec::new(), | ||
| Vec::new(), | ||
| vec![(CONCEPT, ReadMode::PLUG_AND_PLAY_V3)], | ||
| ) | ||
| } | ||
|
|
||
| fn register_slab() -> SlabDeclaration { | ||
| SlabDeclaration { | ||
| reading: SlabReading::Register128, | ||
| value_schema: ValueSchema::Full, | ||
| layout_version: ENVELOPE_LAYOUT_VERSION, | ||
| } | ||
| } | ||
|
|
||
| /// One group-result row, addressed under the context's concept. The key's | ||
| /// identity is the group; the payload carries no classid. | ||
| fn group_row(group: usize) -> NodeRow { | ||
| NodeRow { | ||
| key: NodeGuid::new(u32::from(CONCEPT) << 16, 1, 2, 3, 0x66, group as u32), | ||
| edges: Default::default(), | ||
| value: [0; 480], | ||
| } | ||
| } | ||
|
|
||
| struct Population { | ||
| n: usize, | ||
| mask: Vec<u64>, | ||
| keys: Vec<u32>, | ||
| xs: Vec<u8>, | ||
| ys: Vec<u8>, | ||
| } | ||
|
|
||
| fn population() -> Population { | ||
| let n = 3 * BOUNDED_TILE_ROWS + 777; | ||
| let mut mask = vec![0u64; n.div_ceil(64)]; | ||
| for i in (0..n).filter(|i| i % 11 != 4) { | ||
| mask[i / 64] |= 1 << (i % 64); | ||
| } | ||
| let mut s = 0x9E37_79B9_7F4A_7C15u64; | ||
| let mut next = || { | ||
| s = s | ||
| .wrapping_mul(6364136223846793005) | ||
| .wrapping_add(1442695040888963407); | ||
| (s >> 56) as u8 | ||
| }; | ||
| let xs: Vec<u8> = (0..n).map(|_| next()).collect(); | ||
| let ys: Vec<u8> = (0..n).map(|_| next()).collect(); | ||
| let keys = (0..n as u32) | ||
| .map(|i| (i.wrapping_mul(2_654_435_761) >> 11) % GROUPS as u32) | ||
| .collect(); | ||
| Population { | ||
| n, | ||
| mask, | ||
| keys, | ||
| xs, | ||
| ys, | ||
| } | ||
| } | ||
|
|
||
| /// Resolution and binding run exactly once, before the population loop; the | ||
| /// loop sees only `RegisterLanes` (plain numbers) and byte lanes. | ||
| fn bind() -> RegisterLanes { | ||
| activation() | ||
| .resolve_for_context(CONCEPT, Some(®ister_slab())) | ||
| .expect("context resolves") | ||
| .bind_register128(RegisterRails::Two) | ||
| .expect("Register128 slab grants both rails") | ||
| } | ||
|
|
||
| /// FAILS IF: the tiled bounded fold, stored per tile and per group into the | ||
| /// value-slab rails and read back, does not widen and merge to exactly the | ||
| /// wide `i32` path over the whole population — univariate (rail 0) and | ||
| /// bivariate (rails 0+1) alike. | ||
| #[test] | ||
| fn register_rails_carry_bounded_stats_that_widen_to_the_wide_path() { | ||
| let p = population(); | ||
| let lanes = bind(); | ||
| assert_eq!(lanes.concept(), CONCEPT, "concept comes from the context"); | ||
|
|
||
| // Univariate: one row per (tile, group); the register is written per | ||
| // group, never per input row. | ||
| let mut tile_rows: Vec<Vec<NodeRow>> = Vec::new(); | ||
| let mut regs = [[0u8; 16]; GROUPS]; | ||
| let mut out = [PowerSums::default(); GROUPS]; | ||
| fold_bounded_power_sums_tiles(p.n, &mut regs, &mut out, |t, regs| { | ||
| masked_group_bounded_power_sums_u8( | ||
| &p.mask[t.start / 64..], | ||
| &p.keys[t.clone()], | ||
| &p.xs[t], | ||
| regs, | ||
| )?; | ||
| let rows = (0..GROUPS) | ||
| .map(|g| { | ||
| let mut row = group_row(g); | ||
| assert!(lanes.set(&mut row, 0, Register128(regs[g]))); | ||
| row | ||
| }) | ||
| .collect(); | ||
| tile_rows.push(rows); | ||
| Ok(()) | ||
| }) | ||
| .unwrap(); | ||
| assert_eq!(tile_rows.len(), 4, "three full tiles and one partial"); | ||
|
|
||
| let wx: Vec<i32> = p.xs.iter().map(|&x| i32::from(x)).collect(); | ||
| let wy: Vec<i32> = p.ys.iter().map(|&y| i32::from(y)).collect(); | ||
| let mut want = [PowerSums::default(); GROUPS]; | ||
| masked_group_power_sums_i32(&p.mask, &p.keys, &wx, &mut want); | ||
| assert_eq!(out, want, "tiled driver == whole"); | ||
|
|
||
| // Independently: re-read every stored rail, widen, merge. | ||
| let mut reread = [PowerSums::default(); GROUPS]; | ||
| for rows in &tile_rows { | ||
| for (g, row) in rows.iter().enumerate() { | ||
| let reg = lanes.get(row, 0).unwrap(); | ||
| let w = ndarray::simd::widen_bounded_power_sums(®.0); | ||
| reread[g] = reread[g].checked_merge(w).unwrap(); | ||
| } | ||
| } | ||
| assert_eq!(reread, want, "rails read back == whole"); | ||
| assert!(want.iter().map(|w| w.n).sum::<u64>() > BOUNDED_TILE_ROWS as u64); | ||
| assert!(want.iter().all(|w| w.n > 0), "every group populated"); | ||
|
|
||
| // Bivariate: rail 0 = [n, Σx, Σx², ·], rail 1 = [Σy, Σy², Σxy, ·]. | ||
| let (mut r0, mut r1) = ([[0u8; 16]; GROUPS], [[0u8; 16]; GROUPS]); | ||
| let mut cross = [CrossPowerSums::default(); GROUPS]; | ||
| let mut stored: Vec<NodeRow> = Vec::new(); | ||
| fold_bounded_cross_power_sums_tiles(p.n, &mut r0, &mut r1, &mut cross, |t, a, b| { | ||
| masked_group_bounded_cross_power_sums_u8( | ||
| &p.mask[t.start / 64..], | ||
| &p.keys[t.clone()], | ||
| &p.xs[t.clone()], | ||
| &p.ys[t], | ||
| a, | ||
| b, | ||
| )?; | ||
| for g in 0..GROUPS { | ||
| let mut row = group_row(g); | ||
| assert!(lanes.set(&mut row, 0, Register128(a[g]))); | ||
| assert!(lanes.set(&mut row, 1, Register128(b[g]))); | ||
| stored.push(row); | ||
| } | ||
| Ok(()) | ||
| }) | ||
| .unwrap(); | ||
| let mut want_cross = [CrossPowerSums::default(); GROUPS]; | ||
| masked_group_cross_power_sums_i32(&p.mask, &p.keys, &wx, &wy, &mut want_cross); | ||
| assert_eq!(cross, want_cross, "bivariate tiled driver == whole"); | ||
|
|
||
| let mut reread = [CrossPowerSums::default(); GROUPS]; | ||
| for (k, row) in stored.iter().enumerate() { | ||
| let (a, b) = (lanes.get(row, 0).unwrap(), lanes.get(row, 1).unwrap()); | ||
| let g = k % GROUPS; | ||
| let w = ndarray::simd::widen_bounded_cross_power_sums(&a.0, &b.0); | ||
| reread[g] = reread[g].checked_merge(w).unwrap(); | ||
| } | ||
| assert_eq!(reread, want_cross, "bivariate rails read back == whole"); | ||
| } | ||
|
|
||
| /// FAILS IF: a population whose slab declares Facet96 (or nothing) can be | ||
| /// bound as registers. The fold never runs on such a slab. | ||
| #[test] | ||
| fn a_facet96_slab_is_never_bound_as_registers() { | ||
| let a = activation(); | ||
| let facet = SlabDeclaration { | ||
| reading: SlabReading::Facet96, | ||
| ..register_slab() | ||
| }; | ||
| for slab in [Some(&facet), None] { | ||
| let r = a.resolve_for_context(CONCEPT, slab).unwrap(); | ||
| assert!(matches!( | ||
| r.bind_register128(RegisterRails::One), | ||
| Err(ActivationDrift::NotRegister128 { | ||
| concept: CONCEPT, | ||
| .. | ||
| }) | ||
| )); | ||
| } | ||
| } | ||
Oops, something went wrong.
Oops, something went wrong.
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.
Uh oh!
There was an error while loading. Please reload this page.