diff --git a/.claude/board/AGENT_LOG.md b/.claude/board/AGENT_LOG.md index d0e50a981..c9f16a8b8 100644 --- a/.claude/board/AGENT_LOG.md +++ b/.claude/board/AGENT_LOG.md @@ -1,3 +1,8 @@ +## 2026-10-15 — D-HOLO H14b result count: one census run + +- Card `census-counter` (run as a general-purpose agent on Haiku with the card's rules pasted), the H14b table of `h14b_run1.txt`, lines 59–94: k <= 4 cells, cells above 1.25× B on full-row and session read, min/max per density, F3 and byte comparisons. +- Ledger: every count matched the orchestrator's independent awk run (9 failing cells, same cells and ratios); 0 wrong, 0 missed. One cosmetic defect: its echo labels were shell-expanded; the counting commands were unaffected. About 396k subagent tokens. No conclusion came from the card. + ## 2026-10-15 — ledger-correction batch: two Haiku harvest runs - Card `harvest-scout` over ndarray `src/hpc/*cascade*` + blackboard (O20): hits at `cascade.rs:270-276`, `:813`, blackboard `:84-90` read and confirmed; 0 wrong, 0 missed. Earlier in the session the doc scout returned counts without hits (one miss on that kind of task). diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 33d9af721..2b3c9299d 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -42,7 +42,8 @@ Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own work | **D-HOLO-H9** | Relational emptiness decided symbolically (empty operand, disjoint domains, contradictory constraints) vs by fold | Queued (pre-registered, not run) | zero false empties; fraction decided symbolically reported | | **D-HOLO-H11** | Stacked logic: a chain of NAL polyfill bricks at depth 1–8 composed before one evaluation | Queued (pre-registered, not run; after H6b) | answers no single brick gives, == oracle; cost below d separate runs at d = 4; no confidence inflation, gate disable must inflate | | **D-HOLO-H12** | Semantic map of inference functions across OpenNARS, ONA, the NAL polyfill (and a MeTTa NAL if pinnable) | Queued (pre-registered, not run) | last system adds zero nodes in both orders; polyfill gaps named; differences classified as distinction or defect | -| **D-HOLO-H14** | Per classid x thought x 64k tile: full 512-byte row writes vs a connected lane delta (row key + lane mask + changed lanes in one record), and per-(thought, lane) tables indexed directly by the row address (`Lane_l[index]`, no traversal; presence masks folded, materialization charged only at a terminal); session thought masks and thought lane masks kept as separate levels | Measured 2026-10-15 (v4, one class): C folds 10–256× faster than B on F1/F2; C merge-on-read 2.8–6.1× slower than B; C default and B default both not met; returned to the operator with the crossover; H14b (positional per-row lane mask for C) open | == dense reference; C default iff at k <= 4 its fold queries are >= 2x faster than B, its reads with terminal materialization <= 1.25x B and bytes <= B; else B default iff read and session read <= 1.25x A and bytes <= 0.5x A; mixed result returns to the operator | +| **D-HOLO-H14** | Per classid x thought x 64k tile: full 512-byte row writes vs a connected lane delta (row key + lane mask + changed lanes in one record), and per-(thought, lane) tables indexed directly by the row address (`Lane_l[index]`, no traversal; presence masks folded, materialization charged only at a terminal); session thought masks and thought lane masks kept as separate levels | Measured 2026-10-15 (v4, one class): C folds 10–256× faster than B on F1/F2; C merge-on-read 2.8–6.1× slower than B; C default and B default both not met; returned to the operator with the crossover; H14b measured (row D-HOLO-H14b) | == dense reference; C default iff at k <= 4 its fold queries are >= 2x faster than B, its reads with terminal materialization <= 1.25x B and bytes <= B; else B default iff read and session read <= 1.25x A and bytes <= 0.5x A; mixed result returns to the operator | +| **D-HOLO-H14b** | C plus one positional u32 lane mask per row per thought (`Mask[i]`), so merge-on-read reads only the tables the mask names; folds unchanged | Measured 2026-10-15 (v4, one class, entry 2026-10-15-d-holo-h14b-lane-mask): prediction falsified in 9 of 18 cells at k <= 4 (all 1 % cells pass, failures at 10 % and 100 % dirty); bytes <= B everywhere; M faster than C on full-row read in 35 of 36 cells; M beats B on F3 in all 12 cells at 1 % dirty; M default not met. WITHDRAWN 2026-10-15 as a layout candidate (category error: M transposes C's presence planes into a row index; H14/H14b measured row reconstruction, not C's primary operation); numbers kept; follow-up D-HOLO-H14c | M default iff at k <= 4 on every cell its full-row and session read <= 1.25x B and bytes <= B; folds equal C (tested) | | **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | Shipped #1546 `c21bd165` (11 tests, 11 disable runs red; four comparisons on one lane 8 → 2 ops; 70/2,000 small descriptions refused as written, all run rewritten) | == row oracle over 400 generated descriptions × 5 measures | | **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | Queued (maintainer decision) | relalg tests pass unchanged against the contract IR | | **D-RA-3** | Datalog rules as algebra values; names are labels resolved through the label codebook, never strings in a rule | Queued (after D-RA-2) | codebook-built rules == hand-written `Rel`; unknown label refused at resolution | diff --git a/.claude/board/entries/2026-10-15-d-holo-h14b-lane-mask.md b/.claude/board/entries/2026-10-15-d-holo-h14b-lane-mask.md new file mode 100644 index 000000000..4d4e84f8d --- /dev/null +++ b/.claude/board/entries/2026-10-15-d-holo-h14b-lane-mask.md @@ -0,0 +1,28 @@ +# D-HOLO-H14b — inverted fold plus a positional lane mask per row (v4, 2026-10-15) + +**Status:** MEASURED. Plan: `.claude/plans/d-holo-address-indexed-algebra-v1.md` (H14b, pre-registered before the run, results). +**Probe:** `crates/lance-graph-mask-risc/examples/holo_lane_storage_probe.rs` (arm M); `tier: v4 (avx512f)`; A, B, C and M timed in one run on one host; one class. + +- Prediction (M's full-row and session read <= 1.25× B at k <= 4): + FALSIFIED in 9 of 18 cells. At 1 % dirty all 6 cells pass (full-row + 0.94–1.14× B, session 0.93–1.13×); failures at 10 % dirty (up to 1.40 / + 1.87×) and 100 % dirty (up to 1.63 / 5.85×). M's bytes to the writer are + at most B's in every cell, by construction rather than measurement (B was + charged a `starts` offset per dirty row that M was not; under the same + accounting they are equal). M default not met; returns to the operator. +- The mask fixed most of C's merge cost: M's full-row read is faster than C's + in 35 of 36 cells (C/M 0.98–3.69×). +- F3 (fold, then build the named rows): M beats B in all 12 cells at 1 % + dirty and in 18 of 36 overall; M beats C in 33 of 36. + +**OPEN:** why M loses at higher density (HYPOTHESIS: a row's k lanes sit in k +tables, B's in one record); C's and M's seal at 1 % dirty is page-fault +bound; 16 classes untimed. + +**Withdrawal note (2026-10-15, before merge).** M is withdrawn as a candidate +default layout for thought-first C, and the density-based A/B/C/M switch is +withdrawn. H14 and H14b mostly measured whole-row reconstruction, which is not +C's primary operation; `Mask[i]` transposes what C's per-lane presence planes +already hold into a row-oriented index. The numbers above stand; their reading +as a verdict on C does not. M remains an experimental row-oriented acceleration +structure. Follow-up: D-HOLO-H14c. Full note: the plan's "H14b withdrawal note". diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 0fc798c6a..88fc7a74f 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,13 +25,14 @@ 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. -343 entries, 2026-08-06 .. 2026-10-15. +344 entries, 2026-08-06 .. 2026-10-15. | date | entry id | finding | file | |---|---|---|---| | 2026-10-15 | `ledger-correction-wire-contract` | | [2026-10-15-ledger-correction-wire-contract.md](2026-10-15-ledger-correction-wire-contract.md) | | 2026-10-15 | `givens-layer` | | [2026-10-15-givens-layer.md](2026-10-15-givens-layer.md) | | 2026-10-15 | `D-WAL` | `LanceCycleWriter` vs the lancedb 0.40 MemWAL write path (measured) | [2026-10-15-d-wal-shootout.md](2026-10-15-d-wal-shootout.md) | +| 2026-10-15 | `D-HOLO-H14b` | | [2026-10-15-d-holo-h14b-lane-mask.md](2026-10-15-d-holo-h14b-lane-mask.md) | | 2026-10-15 | `D-HOLO-H14` | | [2026-10-15-d-holo-h14-lane-storage.md](2026-10-15-d-holo-h14-lane-storage.md) | | 2026-10-14 | `revision-layer-invariants` | | [2026-10-14-revision-layer-invariants.md](2026-10-14-revision-layer-invariants.md) | | 2026-10-14 | `D-MTP-0` | where Hyperon/MeTTa attaches to the masking-algebra polyfill | [2026-10-14-metta-polyfill-map.md](2026-10-14-metta-polyfill-map.md) | diff --git a/.claude/plans/d-holo-address-indexed-algebra-v1.md b/.claude/plans/d-holo-address-indexed-algebra-v1.md index 7ced213d8..1c94bc2b6 100644 --- a/.claude/plans/d-holo-address-indexed-algebra-v1.md +++ b/.claude/plans/d-holo-address-indexed-algebra-v1.md @@ -1083,3 +1083,127 @@ What the numbers point at (HYPOTHESIS, not measured here): - C's seal at 1 % dirty is page faults: the positional tables are zeroed lazily, so each scattered dirty row touches a fresh page. At 100 % dirty the same seal costs 32–222 ns. Persisted bytes are unaffected. + +## Next falsifier: H14b — C with a positional lane mask per row (PRE-REGISTERED 2026-10-15, NOT RUN) + +Approved by the operator 2026-10-15 ("go ahead with H14b"). + +**Arm M.** C's per-(thought, lane) tables and presence masks, unchanged, plus +one `u32` per row per thought held positionally: `Mask[i]` names the lanes row +i changed in that thought (0 for a clean row). The address stays the register: +no index, no traversal. Folds are C's folds (the same presence masks). +Merge-on-read reads `Mask[i]` and then position i of only the tables it names, +instead of probing every touched table. + +Resident cost added per thought: 4 bytes per row (256 KiB per 64k tile). +Bytes handed to the writer: per dirty row its key, its lane mask and the +changed lanes (8 + 16k); per-lane positions follow from the masks. + +**Prediction.** At k <= 4, on every (dirty, thoughts) cell of the H14 grid, +M's full-row read and M's session read are each at most 1.25× B's. Falsified +if any such cell exceeds 1.25×. + +**Decision rule.** M becomes the default for a dirty tile if, at k <= 4 on +every cell: the prediction holds; M's bytes to the writer are at most B's; +and C's fold advantage (at least 2× B on F1 and F2) carries over, which holds +by construction because M folds C's masks (checked by test, not re-timed). If +the prediction fails, the result returns to the operator with the cells that +failed and the F3 crossover between M and B. + +Also reported, not part of the rule: seal per dirty row, F3 per emitted row +for M against A, B and C. + +**Comparisons are within one run.** A, B, C and M are timed in the same run on +the same host with the tier printed. The H14 numbers (another host) are not +compared against. + +**Tests before any timing.** +- M reads the dense reference on every row (k = 1, 4, 31). +- M's `Mask[r]` equals B's lane mask for every row r. +- M's merge probes exactly `popcount(Mask[r])` tables for row r, and C's + merge probes every touched table; the fixture must have more touched tables + than k, or the test proves nothing. +- M's F1, F2 and F3 equal C's. + +**Disable runs.** M's merge iterating the touched tables instead of `Mask[r]` +must turn the probe test red. A mask that drops one lane must turn the +reference test red. + +### H14b results (v4, 2026-10-15): the prediction fails above 1 % dirty; M is C's read fixed, not B's + +Run: `cargo run --release -p lance-graph-mask-risc --example +holo_lane_storage_probe`; the program printed `tier: v4 (avx512f)`. A, B, C +and M were timed in the same run on the same host (a different host from the +H14 run, so the two runs are not compared). One class. 11 tests pass; the two +pre-registered disable runs turned their tests red (M's merge over every +touched table; a mask that drops a lane). + +**Rule at k <= 4 (18 cells).** +- Prediction (M's full-row and session read each <= 1.25× B): **FALSIFIED** + in 9 of 18 cells. All 6 cells at 1 % dirty pass (full-row 0.94–1.14× B, + session 0.93–1.13×). The failures are at 10 % dirty (T = 8 k = 4: 1.40 / + 1.34; T = 64: session 1.34–1.87) and at 100 % dirty (full-row up to 1.63×, + session up to 5.85×). +- M's bytes to the writer <= B's: true in every cell, but by construction, + not as a measurement. Both arms carry the same values; B was also charged a + 4-byte `starts` offset per dirty row that M was not, although both can + derive per-lane positions from the masks. Under the same accounting the two + are equal, so this part of the rule carried no evidence (review of #1569). +- Folds: M uses C's presence masks; tested equal, not re-timed. +- M default: **not met.** Returns to the operator. + +**What M did change.** Against C in the same run, M's full-row read is +0.98–3.69× as fast (C/M): faster in 35 of 36 cells, from 297.4 vs 209.8 ns +(T = 1, 1 %, k = 1) to 1,129 vs 306 ns (T = 64, 1 %, k = 1); the one cell +where C is faster is T = 1, 100 %, k = 31 (1,299 vs 1,320 ns). On F3 (fold, +then build the rows the fold names), M beats C in 33 of 36 cells and B in +18 of 36. At 1 % dirty M is the cheapest arm in 10 of 12 cells (M 84–184 ns +per emitted row, B 175–1,260, C 123–241); C is cheaper at k = 31 for 1 and 8 +thoughts. + +**Where M loses (HYPOTHESIS, not measured).** B keeps a row's changed lanes +next to each other in one record, so a row read is one index lookup and one +or two cache lines. M keeps lane l of row i in table l at position i, so a +row with k changed lanes is k cache lines in k tables. That costs little when +few rows are dirty and grows with density; the session read at 8–64 thoughts +also walks up to T × k tables at once. A test would be to time the read +against k at fixed density and count cache misses per row. + +**Crossover.** At 1 % dirty, M matches B on reads (within 1.25× in all 6 +cells at k <= 4) and beats B on F3 in all 12 cells; at 10 % and above, B's +reads are faster. M's seal at 1 % dirty is still the +page-fault cost of C's positional tables (6.5–15 µs per dirty row at one +thought). + +### H14b withdrawal note (2026-10-15): M withdrawn as a layout candidate; the numbers stand, their reading as a verdict on C does not + +DECISION (operator, 2026-10-15: "I think M is a categorical error"). SCOPE: the +default-layout question for thought-first C. BASIS: below. REVISIT WHEN: a +consumer is shown that genuinely needs whole-row reconstruction as its primary +operation. + +1. **M is withdrawn as a candidate default layout for C.** It stays in the probe + as an experimental, row-oriented acceleration structure. It is not a + prerequisite for Cartesian operand addressing. +2. **The density-based A/B/C/M layout switch proposed after H14b is withdrawn.** +3. **H14 and H14b mostly measured whole-row reconstruction** (full-row read, + session read, F3 materialization). That is not C's primary operation. In C a + thought program names the lane tables it needs, and each is read at the shared + address: `Thought(t)[Table(a)[i] : Table(b)[i]]`. No row is assembled unless a + named terminal asks for one. +4. **What M adds is a transposition, not new information.** `Mask[i]` restates, + row by row, what C's per-(thought, lane) presence planes already hold column + by column: bit l of `Mask[i]` equals bit i of `P_{t,l}`. Storing it again, + per row, reintroduces row-first discovery ("which lanes does this row have?") + in front of positional access. +5. **Two facts are distinct.** The thought knows which lanes its program + *requests*; it does not need to know which lanes are *populated* at a row. + C answers the second question with the presence bit of each requested table, + one test per requested lane, never by scanning the touched tables. +6. **The measurements are not invalid.** Every number above stands as measured. + What is withdrawn is their interpretation as a verdict on whether C works. + The open hypothesis from H14 ("the merge probes every touched table") is + itself an artifact of the full-row question: a query-shaped read probes only + the tables its program selects. +7. The follow-up falsifier is **H14c** (thought-first positional reads, Hamming + presence, Lance 13 masked I/O), run on its own branch and PR. diff --git a/crates/lance-graph-mask-risc/examples/holo_lane_storage_probe.rs b/crates/lance-graph-mask-risc/examples/holo_lane_storage_probe.rs index 87bfbbf11..f3751c66f 100644 --- a/crates/lance-graph-mask-risc/examples/holo_lane_storage_probe.rs +++ b/crates/lance-graph-mask-risc/examples/holo_lane_storage_probe.rs @@ -247,6 +247,8 @@ struct ArmC { thread_local! { static VALUE_READS: std::cell::Cell = const { std::cell::Cell::new(0) }; static MERGES: std::cell::Cell = const { std::cell::Cell::new(0) }; + /// Lane tables a merge looks into, present or not. + static PROBES: std::cell::Cell = const { std::cell::Cell::new(0) }; } impl ArmC { @@ -287,6 +289,8 @@ impl ArmC { self.touched.len() * (WORDS * 8 + N * LANE) } fn value(&self, l: usize, r: usize) -> Option<&Val> { + #[cfg(test)] + PROBES.with(|c| c.set(c.get() + 1)); let p = self.planes[l].as_ref()?; if p.present[r / 64] >> (r % 64) & 1 == 0 { return None; @@ -322,6 +326,64 @@ impl ArmC { } } +// ---------------------------------------------------------------- M (H14b) + +/// C plus one lane mask per row, held positionally: `mask[i]` names the +/// lanes row i changed. The merge reads only the tables the mask names. +/// +/// Withdrawn as a layout candidate (2026-10-15): `mask[i]` restates, per row, +/// what C's presence planes already hold per lane. Kept as an experimental +/// row-oriented acceleration for whole-row reconstruction only; see the plan's +/// "H14b withdrawal note" and D-HOLO-H14c. +struct ArmM { + c: ArmC, + mask: Vec, +} + +impl ArmM { + fn seal(w: &Writes) -> Self { + let mut mask = vec![0u32; N]; + for (&r, &m) in w.rows.iter().zip(&w.masks) { + mask[r as usize] = m; + } + ArmM { + c: ArmC::seal(w), + mask, + } + } + /// Bytes handed to the writer: per dirty row key + mask + changed lanes. + /// + /// This omits the per-row value offset that `ArmB::bytes` charges, though + /// both can derive it from the masks, so `bm <= bb` below holds by + /// construction (`bm == bb - 4 * dirty rows`); it is not a measurement. + fn bytes(&self) -> usize { + self.mask + .iter() + .filter(|&&m| m != 0) + .map(|m| 8 + LANE * m.count_ones() as usize) + .sum() + } + fn resident(&self) -> usize { + self.c.resident() + 4 * N + } + fn read(&self, base: &[Row], r: usize) -> Row { + #[cfg(test)] + MERGES.with(|c| c.set(c.get() + 1)); + let mut out = base[r]; + for l in BitIter(self.mask[r]) { + #[cfg(test)] + PROBES.with(|c| c.set(c.get() + 1)); + // The mask names the lane, so the plane exists and holds row r. + let v = &self.c.planes[l] + .as_ref() + .expect("masked lane has a table") + .values[r]; + out[l * LANE..(l + 1) * LANE].copy_from_slice(v); + } + out + } +} + fn popcount(words: &[u64]) -> u64 { words.iter().map(|w| u64::from(w.count_ones())).sum() } @@ -366,6 +428,27 @@ fn f2_c(arms: &[ArmC], l: usize, a0: usize, acc: &mut [u64], tmp: &mut [u64]) -> } popcount(acc) } +fn f2_m(arms: &[ArmM], l: usize, a0: usize, acc: &mut [u64], tmp: &mut [u64]) -> u64 { + let (w0, w1) = (a0 / 64, (a0 + APERTURE) / 64); + acc.fill(0); + for m in arms { + if let Some(p) = &m.c.planes[l] { + mask_or(acc, &p.present[w0..w1], tmp); + acc.copy_from_slice(tmp); + } + } + popcount(acc) +} +/// F3 on M: C's fold, then M's merge on the rows the fold names. +fn f3_m(m: &ArmM, base: &[Row], a0: usize, acc: &mut [u64], out: &mut Vec) { + m.c.fold_lanes(&F1_LANES, a0, acc); + out.clear(); + for (wi, &w) in acc.iter().enumerate() { + for b in BitIter64(w) { + out.push(m.read(base, a0 + wi * 64 + b)); + } + } +} /// F3 on C: fold first, then merge-on-read only the rows the fold names. fn f3_c(c: &ArmC, base: &[Row], a0: usize, acc: &mut [u64], out: &mut Vec) { c.fold_lanes(&F1_LANES, a0, acc); @@ -429,7 +512,9 @@ fn time(mut f: F) -> f64 { } fn main() { - println!("D-HOLO H14: full row (A) vs connected delta (B) vs inverted fold (C)"); + println!( + "D-HOLO H14/H14b: full row (A), connected delta (B), inverted fold (C), C + positional lane mask (M)" + ); println!("tier: {}", tier()); println!("rows per tile {N}; aperture {APERTURE}; timings ns, median of 11\n"); let base = base(); @@ -443,6 +528,10 @@ fn main() { let mut c_rule = true; let mut c_fold_wins = true; let mut c_read_ok = true; + let mut m_read_ok = true; + let mut m_bytes_ok = true; + let mut m_fail: Vec = Vec::new(); + let mut mrows: Vec = Vec::new(); let mut acc = vec![0u64; APERTURE / 64]; let mut tmp = vec![0u64; APERTURE / 64]; let mut out: Vec = Vec::with_capacity(APERTURE); @@ -455,6 +544,8 @@ fn main() { let a: Vec = ws.iter().map(|w| ArmA::seal(&base, w)).collect(); let b: Vec = ws.iter().map(ArmB::seal).collect(); let c: Vec = ws.iter().map(ArmC::seal).collect(); + let m: Vec = ws.iter().map(ArmM::seal).collect(); + let bm: usize = m.iter().map(ArmM::bytes).sum(); let (ba, bb): (usize, usize) = ( a.iter().map(ArmA::bytes).sum(), b.iter().map(ArmB::bytes).sum(), @@ -475,6 +566,9 @@ fn main() { let sc = time(|| { black_box(ArmC::seal(black_box(&ws[0]))); }) / d0; + let sm = time(|| { + black_box(ArmM::seal(black_box(&ws[0]))); + }) / d0; // Full-row read: 65,536 random (thought, row) pairs. let probe: Vec<(u16, u32)> = (0..N as u64) @@ -499,6 +593,11 @@ fn main() { black_box(c[t as usize].read(&base, r as usize)); } }) / per; + let rm = time(|| { + for &(t, r) in &probe { + black_box(m[t as usize].read(&base, r as usize)); + } + }) / per; // Session read: every thought of the session over one aperture. let a0 = 8 * APERTURE; @@ -525,6 +624,13 @@ fn main() { } } }) / sper; + let qm = time(|| { + for r in a0..a0 + APERTURE { + for &t in &thoughts { + black_box(m[t].read(&base, r)); + } + } + }) / sper; // F1 / F2 / F3, ns per aperture row (F3 per emitted row). let ap = APERTURE as f64; @@ -565,6 +671,10 @@ fn main() { f3_c(&c[0], &base, black_box(a0), &mut acc, &mut out); black_box(&out); }) / emitted; + let f3m = time(|| { + f3_m(&m[0], &base, black_box(a0), &mut acc, &mut out); + black_box(&out); + }) / emitted; if k <= 4 { let b_ok = rb <= 1.25 * ra && qb <= 1.25 * qa && bb as f64 <= 0.5 * ba as f64; @@ -575,7 +685,24 @@ fn main() { c_rule &= c_ok; c_fold_wins &= folds; c_read_ok &= reads; + let m_reads = rm <= 1.25 * rb && qm <= 1.25 * qb; + m_read_ok &= m_reads; + m_bytes_ok &= bm <= bb; + if !m_reads { + m_fail.push(format!( + "T {t_n} {label} k {k}: read M/B {:.2}, session M/B {:.2}", + rm / rb, + qm / qb + )); + } } + mrows.push(format!( + "{t_n:>3} {label:>5} {k:>3} | {:>9} {:>9} | {sm:>7.1} | {rb:>7.2} {rm:>7.2} {:>5.2} | {qb:>7.2} {qm:>7.2} {:>5.2} | {f3b:>6.1} {f3c:>6.1} {f3m:>6.1}", + bb >> 10, + bm >> 10, + rm / rb, + qm / qb + )); let _ = dirty; println!( "{t_n:>3} {label:>5} {k:>3} | {:>9} {:>9} {:>9} {:>10} | {sa:>6.1} {sb:>6.1} {sc:>6.1} | {ra:>6.2} {rb:>6.2} {rcn:>6.2} | {qa:>6.2} {qb:>6.2} {qc:>6.2} | {f1a:>7.3} {f1b:>7.3} {f1c:>7.3} | {f2a:>7.3} {f2b:>7.3} {f2c:>7.3} | {f3a:>6.1} {f3b:>6.1} {f3c:>6.1}", @@ -599,6 +726,37 @@ fn main() { " B default over A: {}", if b_rule { "HOLDS" } else { "not met" } ); + + println!("\nH14b: M (C + positional lane mask) against B, same run"); + println!( + "{:>3} {:>5} {:>3} | {:>9} {:>9} | {:>7} | {:>7} {:>7} {:>5} | {:>7} {:>7} {:>5} | {:>6} {:>6} {:>6}", + "T", "dirty", "k", "B KiB", "M KiB", "sealM", "readB", "readM", "M/B", "sessB", "sessM", "M/B", + "F3 B", "F3 C", "F3 M" + ); + for row in &mrows { + println!("{row}"); + } + println!("rule at k <= 4, every (dirty, thoughts) cell:"); + println!( + " M full-row and session read <= 1.25x B: {}", + if m_read_ok { "HOLDS" } else { "FALSIFIED" } + ); + for f in &m_fail { + println!(" {f}"); + } + println!( + " M bytes to the writer <= B (by construction, see ArmM::bytes): {}", + if m_bytes_ok { "yes" } else { "no" } + ); + println!(" M folds are C's folds (tested equal, not re-timed)"); + println!( + " M default: {}", + if m_read_ok && m_bytes_ok { + "HOLDS" + } else { + "not met" + } + ); } #[cfg(test)] @@ -643,6 +801,81 @@ mod tests { } } + #[test] + fn m_reads_the_dense_reference() { + for k in [1, 4, 31] { + let (base, ws) = fixture(2, 1_000, k); + for w in &ws { + let d = dense(&base, w); + let m = ArmM::seal(w); + for (r, want) in d.iter().enumerate() { + assert_eq!(&m.read(&base, r), want, "M row {r} k {k}"); + } + } + } + } + + #[test] + fn m_mask_is_b_lane_mask_at_every_row() { + let (_, ws) = fixture(2, 1_000, 4); + for w in &ws { + let (b, m) = (ArmB::seal(w), ArmM::seal(w)); + for r in 0..N { + assert_eq!(m.mask[r], b.mask(r), "row {r}"); + } + } + } + + #[test] + fn m_merge_probes_only_the_tables_its_mask_names() { + let (base, ws) = fixture(1, 1_000, 4); + let (c, m) = (ArmC::seal(&ws[0]), ArmM::seal(&ws[0])); + assert!( + c.touched.len() > 4, + "fixture must touch more tables than k, or this proves nothing" + ); + let mut dirty_seen = 0; + for r in 0..N { + PROBES.with(|p| p.set(0)); + let _ = m.read(&base, r); + assert_eq!( + PROBES.with(|p| p.get()), + u64::from(m.mask[r].count_ones()), + "M row {r}" + ); + if m.mask[r] != 0 && dirty_seen < 50 { + dirty_seen += 1; + PROBES.with(|p| p.set(0)); + let _ = c.read(&base, r); + assert_eq!( + PROBES.with(|p| p.get()), + c.touched.len() as u64, + "C row {r}" + ); + } + } + assert_eq!(dirty_seen, 50, "fixture has dirty rows"); + } + + #[test] + fn m_folds_and_terminal_equal_c() { + let (base, ws) = fixture(3, 1_000, 4); + let c: Vec = ws.iter().map(ArmC::seal).collect(); + let m: Vec = ws.iter().map(ArmM::seal).collect(); + let mc: Vec<&ArmC> = m.iter().map(|x| &x.c).collect(); + let (mut acc, mut tmp) = (vec![0u64; APERTURE / 64], vec![0u64; APERTURE / 64]); + for a0 in [0, 3 * APERTURE, N - APERTURE] { + let want1 = f1_c(&c[0], a0, &mut acc); + assert_eq!(f1_c(mc[0], a0, &mut acc), want1); + let want2 = f2_c(&c, 5, a0, &mut acc, &mut tmp); + assert_eq!(f2_m(&m, 5, a0, &mut acc, &mut tmp), want2); + let (mut oc, mut om) = (Vec::new(), Vec::new()); + f3_c(&c[0], &base, a0, &mut acc, &mut oc); + f3_m(&m[0], &base, a0, &mut acc, &mut om); + assert_eq!(oc, om); + } + } + #[test] fn the_session_mask_names_exactly_the_writing_thoughts() { let b = base();