diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 1ad83e795..ae8ca70d0 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -47,7 +47,7 @@ | D-id | Deliverable | Status | Owner / gate | | --- | --- | --- | --- | | D-DRISA-1-LAB | sealed DR frame as a local register file over borrowed SoA | Measured: 13/13 tests, 6 disables red, 0 allocations/query, +0.04–0.6 µs revalidation; [entry](entries/2026-11-04-d-drisa-1-register-proof.md) | this session; lab crate `drisa-register-probe` | -| D-DRISA-3-LAB | k-of-n / Kleene / Bag on the shipped carry words | In stacked PR | this session; ndarray / Quack owners | +| D-DRISA-3-LAB | k-of-n / Kleene / Bag on the shipped carry words | Measured: semantics exact (19/19, 7 disables red); 1.5–4.8× slower than native words in all 8 shapes; [entry](entries/2026-11-04-d-drisa-3-alu-semantics.md) | this session; ndarray / Quack owners | | D-DRISA-M1 | layout witness on the canonical SoA | Proposed | SoA / DR owner | | D-DRISA-M2 | global id → tile index, or co-addressed selections | Proposed | EXO-46 | | D-DRISA-M3 | result-register lifetime across calls | Proposed | result owner | diff --git a/.claude/board/entries/2026-11-04-d-drisa-3-alu-semantics.md b/.claude/board/entries/2026-11-04-d-drisa-3-alu-semantics.md new file mode 100644 index 000000000..8db9e9845 --- /dev/null +++ b/.claude/board/entries/2026-11-04-d-drisa-3-alu-semantics.md @@ -0,0 +1,36 @@ +# D-DRISA-3: the shipped carry words express threshold, Kleene and Bag exactly, and lose to native words in every shape + +**Status:** MEASURED-LAB. Owner: this session (EXO-153 stage 3). Probe: `crates/drisa-register-probe/src/alu.rs`, `tests/integration/alu.rs`, `examples/alu_bench.rs`. Uses only `ndarray::simd::{half_add_mask, full_add_mask, U8x64}`; no `U24x5` or `Abacus` import, no new word, no public type. Follows P3-5 (#1954). + +## What was tested + +Rows are DR-aligned mask planes (one bit per row, tail past `n_rows` zero, a presence plane for absent rows). Three instruction shapes, each against a per-row scalar oracle that shares nothing with the planes: + +- **k-of-n**, two-valued: n ∈ {1, 2, 4, 5, 16, 24}, k ∈ {0, 1, ⌈n/2⌉, n, n+1}; zero, full, alternating, one-hot and random inputs; 100, 4,096 and 65,573 rows (450 cells). The carry arm and a `U8x64` byte-counter arm both equal the oracle on every row. +- **Kleene k-of-n**: an input may be UNKNOWN. TRUE iff the TRUE count reaches k; FALSE iff TRUE + UNKNOWN does not; UNKNOWN otherwise. More than 1,000 UNKNOWN results in the fixture, none turned into FALSE before the terminal. +- **Bag**: each input contributes a 2-bit multiplicity per row; the SUM is compared. The Bag threshold and the support count disagree on at least 4 of 8 k values over the same inputs. + +Boundary twins hold exactly: k = 1 is OR, k = n is AND, k = 0 is exactly the present rows (an absent row is never TRUE), k > n is empty; the middle k is neither OR nor AND. A presence plane with stray bits past `n_rows` never reaches a result. 3-of-5 equals its 10-term Boolean expansion. + +19/19 tests in the crate (6 ALU tests). **Disable runs** (commit first, asserted anchor, `git checkout`): comparator drops its greater-than term → 5 red; presence ignored → 3 red; Kleene UNKNOWN overlaps TRUE → 1 red; Bag high bit at weight 1 → 1 red; carry kept in the same column → 4 red; tail not cleared → 1 red (only after the dirty-presence test was added: before it, presence already zeroed the tail and the guard was not load-bearing). + +## Cost (ns per 64-row word, 65,573 rows, median of 31, 3 processes) + +| instruction | carry words | native | carry / native | +|---|---|---|---| +| 2-of-2 vs native AND | 6.93–7.00 | 1.46 | 4.8× | +| 3-of-5 vs 10-term Boolean expansion | 12.69–12.72 | 3.79–3.81 | 3.3–3.4× | +| 3-of-5 vs `U8x64` counters | 12.69–12.72 | 5.68–5.84 | 2.2× | +| 8-of-16 vs `U8x64` | 39.7–40.4 | 13.8 | 2.9× | +| 12-of-24 vs `U8x64` | 55.5–55.8 | 19.7–20.1 | 2.8× | +| Kleene 4-of-8 vs two `U8x64` counters | 39.8–40.4 | 23.0–26.3 | 1.5–1.7× | +| Kleene 12-of-24 vs two `U8x64` | 131.6–132.7 | 76.6–77.6 | 1.7× | +| Bag sum ≥ 8 of 5 × 2-bit vs `U8x64` | 24.8–25.2 | 7.9–8.0 | 3.1–3.2× | + +One host with AVX-512 and no VNNI, default x86-64 target; the facade backend selected was not recorded. A branchless ripple (no early exit) was tried and was not faster. + +## Reading + +The carry words are a correct and complete arithmetic vocabulary for these shapes: threshold, three-valued threshold and weighted sums all lower to them, with the boundary cases exact. They are not a competitive ALU on this host: each call works on one `u64` (64 rows), and byte counters on the same facade do 64 rows per vector add. That cause is HYPOTHESIS; no wide carry word exists to test it. + +**Abakus contribution, as measured:** the semantics and the oracle, not the speed. The proposed ruling (memo D-DRISA-M6) is to lower these instructions to byte counters by default and keep the carry formulation as the reference. Not measured: counts above 255, folds that keep the planes for later arithmetic, other ISA tiers. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 34a97efdb..b4a3364b0 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ 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. -574 entries, 2026-08-06 .. 2026-11-04. +575 entries, 2026-08-06 .. 2026-11-04. | date | entry id | finding | file | |---|---|---|---| +| 2026-11-04 | `D-DRISA-3` | | [2026-11-04-d-drisa-3-alu-semantics.md](2026-11-04-d-drisa-3-alu-semantics.md) | | 2026-11-04 | `D-DRISA-1` | | [2026-11-04-d-drisa-1-register-proof.md](2026-11-04-d-drisa-1-register-proof.md) | | 2026-11-04 | `D-DRISA-0` | | [2026-11-04-d-drisa-0-remote-register-contract.md](2026-11-04-d-drisa-0-remote-register-contract.md) | | 2026-11-03 | `D-XLOG-META-WIRE-P0` | | [2026-11-03-d-xlog-meta-wire-p0.md](2026-11-03-d-xlog-meta-wire-p0.md) | diff --git a/.claude/plans/d-drisa-decision-memos-v1.md b/.claude/plans/d-drisa-decision-memos-v1.md index cd51b0507..afbb1f7af 100644 --- a/.claude/plans/d-drisa-decision-memos-v1.md +++ b/.claude/plans/d-drisa-decision-memos-v1.md @@ -79,5 +79,5 @@ ## Checklist - [x] D-DRISA-1 local register proof (`entries/2026-11-04-d-drisa-1-register-proof.md`) -- [ ] D-DRISA-3 ALU semantics (stacked PR) +- [x] D-DRISA-3 ALU semantics (`entries/2026-11-04-d-drisa-3-alu-semantics.md`) - [ ] Owner rulings M1–M7 diff --git a/crates/drisa-register-probe/Cargo.toml b/crates/drisa-register-probe/Cargo.toml index bcb2248c4..71376e2e7 100644 --- a/crates/drisa-register-probe/Cargo.toml +++ b/crates/drisa-register-probe/Cargo.toml @@ -19,3 +19,6 @@ description = "D-DRISA-1 lab: does a sealed DR frame bind typed register operand lance-graph-dt64 = { path = "../lance-graph-dt64" } lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } lance-graph-contract = { path = "../lance-graph-contract" } +# D-DRISA-3: the two shipped carry words and `U8x64`, from the same ndarray +# coordinate mask-risc uses, so the graph keeps one ndarray package. +ndarray = { git = "https://github.com/AdaWorldAPI/ndarray", branch = "master", default-features = false, features = ["std"] } diff --git a/crates/drisa-register-probe/examples/alu_bench.rs b/crates/drisa-register-probe/examples/alu_bench.rs new file mode 100644 index 000000000..8032cb58e --- /dev/null +++ b/crates/drisa-register-probe/examples/alu_bench.rs @@ -0,0 +1,202 @@ +//! D-DRISA-3 bench: the ALU instructions over 65,536 + 37 DR-aligned rows, +//! carry words against native baselines on the same facade. Median of 31 +//! runs, ns per 64-row word. Answers are checked equal before timing. +//! +//! Run: cargo run --release --manifest-path crates/drisa-register-probe/Cargo.toml --example alu_bench + +use std::hint::black_box; +use std::time::Instant; + +use drisa_register_probe::alu::{bag_at_least, kofn, kofn_bytes, kofn_kleene, three_of_five_sop}; +use ndarray::simd::U8x64; + +const ROWS: usize = 65_536 + 37; + +fn rng(mut z: u64) -> impl FnMut() -> u64 { + move || { + z = z.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut x = z; + x = (x ^ (x >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + x = (x ^ (x >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + x ^ (x >> 31) + } +} + +fn masks(n: usize, seed: u64) -> Vec> { + let mut r = rng(seed); + let words = ROWS.div_ceil(64); + (0..n).map(|_| (0..words).map(|_| r()).collect()).collect() +} + +fn time(mut f: impl FnMut() -> T) -> f64 { + let mut v: Vec = (0..31) + .map(|_| { + let t = Instant::now(); + black_box(f()); + t.elapsed().as_nanos() as f64 / ROWS.div_ceil(64) as f64 + }) + .collect(); + v.sort_by(|a, b| a.partial_cmp(b).unwrap()); + v[15] +} + +/// Kleene k-of-n with two byte counters (TRUE, and TRUE-or-UNKNOWN). +fn kleene_bytes(t: &[&[u64]], u: &[&[u64]], k: usize, presence: &[u64]) -> (Vec, Vec) { + let (zero, one) = (U8x64::splat(0), U8x64::splat(1)); + let km1 = U8x64::splat((k - 1) as u8); + let words = ROWS.div_ceil(64); + let mut yes = Vec::with_capacity(words); + let mut unk = Vec::with_capacity(words); + for w in 0..words { + let (mut ct, mut cp) = (zero, zero); + for (ti, ui) in t.iter().zip(u) { + ct = ct.saturating_add(U8x64::mask_blend(ti[w], zero, one)); + cp = cp.saturating_add(U8x64::mask_blend(ti[w] | ui[w], zero, one)); + } + let live = presence[w] + & if w == words - 1 { + (1u64 << (ROWS % 64)) - 1 + } else { + !0 + }; + let sure = ct.cmpgt_mask(km1) & live; + yes.push(sure); + unk.push(cp.cmpgt_mask(km1) & live & !sure); + } + (yes, unk) +} + +/// Bag sum with one byte counter: multiplicity lo + 2·hi. +fn bag_bytes(lo: &[&[u64]], hi: &[&[u64]], k: usize, presence: &[u64]) -> Vec { + let (zero, one, two) = (U8x64::splat(0), U8x64::splat(1), U8x64::splat(2)); + let km1 = U8x64::splat((k - 1) as u8); + let words = ROWS.div_ceil(64); + (0..words) + .map(|w| { + let mut c = zero; + for (l, h) in lo.iter().zip(hi) { + c = c.saturating_add(U8x64::mask_blend(l[w], zero, one)); + c = c.saturating_add(U8x64::mask_blend(h[w], zero, two)); + } + let live = presence[w] + & if w == words - 1 { + (1u64 << (ROWS % 64)) - 1 + } else { + !0 + }; + c.cmpgt_mask(km1) & live + }) + .collect() +} + +fn main() { + let words = ROWS.div_ceil(64); + let mut presence = vec![!0u64; words]; + presence[words - 1] = (1u64 << (ROWS % 64)) - 1; + println!("D-DRISA-3: {ROWS} rows, ns per 64-row word, median of 31"); + println!( + "{:<34} {:>10} {:>10} {:>10}", + "instruction", "carry", "native", "carry/native" + ); + + // A7 negative control: a 2-input AND. + let m2 = masks(2, 1); + let r2: Vec<&[u64]> = m2.iter().map(|v| v.as_slice()).collect(); + let and = |p: &[u64]| -> Vec { (0..words).map(|w| r2[0][w] & r2[1][w] & p[w]).collect() }; + assert_eq!(kofn(&r2, 2, &presence, ROWS), and(&presence)); + let (c, n) = ( + time(|| kofn(&r2, 2, &presence, ROWS)), + time(|| and(&presence)), + ); + println!( + "{:<34} {c:>10.2} {n:>10.2} {:>9.1}x", + "2-of-2 vs native AND", + c / n + ); + + // 3-of-5 vs its 10-term Boolean expansion and vs byte counters. + let m5 = masks(5, 2); + let r5: Vec<&[u64]> = m5.iter().map(|v| v.as_slice()).collect(); + let a5: [&[u64]; 5] = [r5[0], r5[1], r5[2], r5[3], r5[4]]; + assert_eq!( + kofn(&r5, 3, &presence, ROWS), + three_of_five_sop(&a5, &presence, ROWS) + ); + assert_eq!( + kofn(&r5, 3, &presence, ROWS), + kofn_bytes(&r5, 3, &presence, ROWS) + ); + let c = time(|| kofn(&r5, 3, &presence, ROWS)); + let s = time(|| three_of_five_sop(&a5, &presence, ROWS)); + let b = time(|| kofn_bytes(&r5, 3, &presence, ROWS)); + println!( + "{:<34} {c:>10.2} {s:>10.2} {:>9.1}x", + "3-of-5 vs 10-term SOP", + c / s + ); + println!( + "{:<34} {c:>10.2} {b:>10.2} {:>9.1}x", + "3-of-5 vs U8x64 counters", + c / b + ); + + // k-of-n at n = 16 and 24. + for n_in in [16usize, 24] { + let m = masks(n_in, 3 + n_in as u64); + let r: Vec<&[u64]> = m.iter().map(|v| v.as_slice()).collect(); + let k = n_in / 2; + assert_eq!( + kofn(&r, k, &presence, ROWS), + kofn_bytes(&r, k, &presence, ROWS) + ); + let c = time(|| kofn(&r, k, &presence, ROWS)); + let b = time(|| kofn_bytes(&r, k, &presence, ROWS)); + println!( + "{:<34} {c:>10.2} {b:>10.2} {:>9.1}x", + format!("{k}-of-{n_in} vs U8x64 counters"), + c / b + ); + } + + // Kleene k-of-n, two counters each side. + for n_in in [8usize, 24] { + let t = masks(n_in, 10 + n_in as u64); + let mut u = masks(n_in, 20 + n_in as u64); + for (ui, ti) in u.iter_mut().zip(&t) { + for (x, y) in ui.iter_mut().zip(ti) { + *x &= !*y; // UNKNOWN disjoint from TRUE + } + } + let tr: Vec<&[u64]> = t.iter().map(|v| v.as_slice()).collect(); + let ur: Vec<&[u64]> = u.iter().map(|v| v.as_slice()).collect(); + let k = n_in / 2; + assert_eq!( + kofn_kleene(&tr, &ur, k, &presence, ROWS), + kleene_bytes(&tr, &ur, k, &presence) + ); + let c = time(|| kofn_kleene(&tr, &ur, k, &presence, ROWS)); + let b = time(|| kleene_bytes(&tr, &ur, k, &presence)); + println!( + "{:<34} {c:>10.2} {b:>10.2} {:>9.1}x", + format!("Kleene {k}-of-{n_in} vs U8x64"), + c / b + ); + } + + // Bag sum of 5 two-bit multiplicities. + let lo = masks(5, 40); + let hi = masks(5, 41); + let lr: Vec<&[u64]> = lo.iter().map(|v| v.as_slice()).collect(); + let hr: Vec<&[u64]> = hi.iter().map(|v| v.as_slice()).collect(); + assert_eq!( + bag_at_least(&lr, &hr, 8, &presence, ROWS), + bag_bytes(&lr, &hr, 8, &presence) + ); + let c = time(|| bag_at_least(&lr, &hr, 8, &presence, ROWS)); + let b = time(|| bag_bytes(&lr, &hr, 8, &presence)); + println!( + "{:<34} {c:>10.2} {b:>10.2} {:>9.1}x", + "Bag sum>=8 of 5x2-bit vs U8x64", + c / b + ); +} diff --git a/crates/drisa-register-probe/src/alu.rs b/crates/drisa-register-probe/src/alu.rs new file mode 100644 index 000000000..6146d6861 --- /dev/null +++ b/crates/drisa-register-probe/src/alu.rs @@ -0,0 +1,197 @@ +//! D-DRISA-3 (EXO-153): arithmetic over DR-aligned mask planes with the two +//! shipped ndarray carry words only (`half_add_mask`, `full_add_mask`). LAB +//! ONLY: no public type, no new word, no `U24x5` / `Abacus` import. +//! +//! Each `u64` word is one significance column for 64 independent rows. A +//! counter of `b` planes holds a per-row count in `0..2^b`. Three +//! instruction shapes are tested against a per-row scalar oracle: +//! - [`kofn`]: at least `k` of `n` Boolean inputs (two-valued); +//! - [`kofn_kleene`]: the same under Kleene logic, where an input may be +//! UNKNOWN for a row: TRUE iff the TRUE count reaches `k`, FALSE iff even +//! counting every UNKNOWN as true does not, UNKNOWN otherwise; +//! - [`bag_at_least`]: Bag multiplicity, each input contributing a 2-bit +//! multiplicity (0..=3) per row; the per-row SUM is compared, which is not +//! the support count. +//! +//! Every result is ANDed with the population's presence plane: an absent row +//! is never TRUE (nor UNKNOWN), even for `k = 0`, and tail bits past `n_rows` +//! are zero. +//! +//! Baselines for the same instructions: [`kofn_bytes`] (one `U8x64` byte +//! counter per 64 rows on the same facade) and [`three_of_five_sop`] (the +//! sum-of-products Boolean expansion over native mask words). + +use ndarray::simd::{full_add_mask, half_add_mask, U8x64}; + +/// Widest counter: counts up to 255. +pub const MAX_PLANES: usize = 8; + +fn planes_for(max_count: usize) -> usize { + (usize::BITS - max_count.leading_zeros()) as usize +} + +fn tail(n_rows: usize, w: usize) -> u64 { + let rows = n_rows.saturating_sub(w * 64); + if rows >= 64 { + !0 + } else { + (1u64 << rows) - 1 + } +} + +/// Add `x` (weight `2^from`) into a counter of `b` planes. +#[inline(always)] +fn ripple(p: &mut [u64; MAX_PLANES], b: usize, from: usize, mut x: u64) { + let mut j = from; + while x != 0 && j < b { + let (s, c) = half_add_mask(p[j], x); + p[j] = s; + x = c; + j += 1; + } +} + +/// Per row: counter >= `k`. `k` larger than the counter can hold is false. +#[inline(always)] +fn ge_const(p: &[u64; MAX_PLANES], b: usize, k: usize) -> u64 { + if k >= 1 << b { + return 0; + } + let mut eq = !0u64; + let mut gt = 0u64; + for j in (0..b).rev() { + if (k >> j) & 1 == 1 { + eq &= p[j]; + } else { + gt |= eq & p[j]; + } + } + gt | eq +} + +/// Sum of `n` single-bit inputs at word `w`, into `b` planes. +#[inline(always)] +fn count_word(inputs: &[&[u64]], w: usize, b: usize) -> [u64; MAX_PLANES] { + let mut p = [0u64; MAX_PLANES]; + let mut i = 0; + while i + 1 < inputs.len() { + let (s, c) = full_add_mask(p[0], inputs[i][w], inputs[i + 1][w]); + p[0] = s; + ripple(&mut p, b, 1, c); + i += 2; + } + if i < inputs.len() { + ripple(&mut p, b, 0, inputs[i][w]); + } + p +} + +/// At least `k` of the `inputs` hold, per present row. +pub fn kofn(inputs: &[&[u64]], k: usize, presence: &[u64], n_rows: usize) -> Vec { + let b = planes_for(inputs.len()).max(1); + assert!(b <= MAX_PLANES, "n too large for an 8-plane counter"); + (0..n_rows.div_ceil(64)) + .map(|w| { + let p = count_word(inputs, w, b); + ge_const(&p, b, k) & presence[w] & tail(n_rows, w) + }) + .collect() +} + +/// Kleene k-of-n. Input `i` is TRUE where `t[i]` is set, UNKNOWN where `u[i]` +/// is set (the two must be disjoint), FALSE elsewhere. Returns `(true, +/// unknown)` result masks; a present row in neither is FALSE. +pub fn kofn_kleene( + t: &[&[u64]], + u: &[&[u64]], + k: usize, + presence: &[u64], + n_rows: usize, +) -> (Vec, Vec) { + assert_eq!(t.len(), u.len()); + let b = planes_for(t.len()).max(1); + let words = n_rows.div_ceil(64); + let mut yes = Vec::with_capacity(words); + let mut unk = Vec::with_capacity(words); + for w in 0..words { + let pt = count_word(t, w, b); + // "possible": TRUE or UNKNOWN, counted once each. + let mut pp = [0u64; MAX_PLANES]; + for (ti, ui) in t.iter().zip(u) { + ripple(&mut pp, b, 0, ti[w] | ui[w]); + } + let live = presence[w] & tail(n_rows, w); + let sure = ge_const(&pt, b, k) & live; + let could = ge_const(&pp, b, k) & live; + yes.push(sure); + unk.push(could & !sure); + } + (yes, unk) +} + +/// Bag: input `i` contributes multiplicity `lo[i] + 2·hi[i]` (0..=3) per row. +/// True where the per-row SUM reaches `k`. +pub fn bag_at_least( + lo: &[&[u64]], + hi: &[&[u64]], + k: usize, + presence: &[u64], + n_rows: usize, +) -> Vec { + assert_eq!(lo.len(), hi.len()); + let b = planes_for(3 * lo.len()).max(1); + assert!(b <= MAX_PLANES, "sum too large for an 8-plane counter"); + (0..n_rows.div_ceil(64)) + .map(|w| { + let mut p = [0u64; MAX_PLANES]; + for (l, h) in lo.iter().zip(hi) { + ripple(&mut p, b, 0, l[w]); + ripple(&mut p, b, 1, h[w]); + } + ge_const(&p, b, k) & presence[w] & tail(n_rows, w) + }) + .collect() +} + +/// Baseline: the same k-of-n with one `U8x64` byte counter per 64 rows on the +/// ndarray facade. `k = 0` is all present rows; `n < 255`. +pub fn kofn_bytes(inputs: &[&[u64]], k: usize, presence: &[u64], n_rows: usize) -> Vec { + let (zero, one) = (U8x64::splat(0), U8x64::splat(1)); + (0..n_rows.div_ceil(64)) + .map(|w| { + let live = presence[w] & tail(n_rows, w); + if k == 0 { + return live; + } + if k > inputs.len() { + return 0; + } + let mut c = zero; + for m in inputs { + c = c.saturating_add(U8x64::mask_blend(m[w], zero, one)); + } + c.cmpgt_mask(U8x64::splat((k - 1) as u8)) & live + }) + .collect() +} + +/// Baseline: at least 3 of 5 as the 10-term sum of products over native mask +/// words. +pub fn three_of_five_sop(m: &[&[u64]; 5], presence: &[u64], n_rows: usize) -> Vec { + (0..n_rows.div_ceil(64)) + .map(|w| { + let [a, b, c, d, e] = [m[0][w], m[1][w], m[2][w], m[3][w], m[4][w]]; + let r = (a & b & c) + | (a & b & d) + | (a & b & e) + | (a & c & d) + | (a & c & e) + | (a & d & e) + | (b & c & d) + | (b & c & e) + | (b & d & e) + | (c & d & e); + r & presence[w] & tail(n_rows, w) + }) + .collect() +} diff --git a/crates/drisa-register-probe/src/lib.rs b/crates/drisa-register-probe/src/lib.rs index c7cd393d3..5605fde7c 100644 --- a/crates/drisa-register-probe/src/lib.rs +++ b/crates/drisa-register-probe/src/lib.rs @@ -28,6 +28,8 @@ //! on field values, so a value write leaves it valid while a value-dependent //! method must refuse until its value witness is re-taken. +pub mod alu; + use std::sync::atomic::{AtomicU64, Ordering}; use lance_graph_contract::class_view::WideFieldMask; diff --git a/crates/drisa-register-probe/tests/integration/alu.rs b/crates/drisa-register-probe/tests/integration/alu.rs new file mode 100644 index 000000000..0e82e092e --- /dev/null +++ b/crates/drisa-register-probe/tests/integration/alu.rs @@ -0,0 +1,279 @@ +//! D-DRISA-3 falsifiers. The oracle works per row on small integer states and +//! shares nothing with the planes, the carry words or the comparator. + +use drisa_register_probe::alu::{bag_at_least, kofn, kofn_bytes, kofn_kleene, three_of_five_sop}; + +/// Per-row input state: 0 false, 1 true, 2 unknown (Kleene only). +struct Case { + present: Vec, + /// `state[i][row]`. + state: Vec>, +} + +fn rng(mut z: u64) -> impl FnMut() -> u64 { + move || { + z = z.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut x = z; + x = (x ^ (x >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + x = (x ^ (x >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + x ^ (x >> 31) + } +} + +#[derive(Clone, Copy, Debug)] +enum Shape { + Zero, + Full, + Alternating, + OneHot, + Random, + RandomKleene, +} + +fn case(n: usize, n_rows: usize, shape: Shape, seed: u64) -> Case { + let mut r = rng(seed); + let present = (0..n_rows).map(|row| row % 13 != 7).collect(); + let state = (0..n) + .map(|i| { + (0..n_rows) + .map(|row| match shape { + Shape::Zero => 0, + Shape::Full => 1, + Shape::Alternating => ((row + i) % 2) as u8, + Shape::OneHot => u8::from(row % n.max(1) == i), + Shape::Random => (r() % 2) as u8, + Shape::RandomKleene => (r() % 3) as u8, + }) + .collect() + }) + .collect(); + Case { present, state } +} + +fn plane(n_rows: usize, f: impl Fn(usize) -> bool) -> Vec { + let mut w = vec![0u64; n_rows.div_ceil(64)]; + for row in 0..n_rows { + if f(row) { + w[row / 64] |= 1 << (row % 64); + } + } + w +} + +fn bit(words: &[u64], row: usize) -> bool { + words[row / 64] >> (row % 64) & 1 == 1 +} + +fn tail_clear(words: &[u64], n_rows: usize) -> bool { + (n_rows..words.len() * 64).all(|row| !bit(words, row)) +} + +const NS: [usize; 6] = [1, 2, 4, 5, 16, 24]; +const ROWS: [usize; 3] = [100, 4096, 65_536 + 37]; + +fn ks(n: usize) -> [usize; 5] { + [0, 1, n.div_ceil(2), n, n + 1] +} + +/// A1/A2: two-valued k-of-n, every n, k and shape, three row counts with +/// tails; carry arm and byte-counter arm both equal the oracle. +#[test] +fn kofn_matches_the_per_row_oracle_everywhere() { + let mut cells = 0; + for shape in [ + Shape::Zero, + Shape::Full, + Shape::Alternating, + Shape::OneHot, + Shape::Random, + ] { + for &n in &NS { + for &rows in &ROWS { + let c = case(n, rows, shape, (n * 7 + rows) as u64); + let presence = plane(rows, |r| c.present[r]); + let ins: Vec> = + c.state.iter().map(|s| plane(rows, |r| s[r] == 1)).collect(); + let refs: Vec<&[u64]> = ins.iter().map(|v| v.as_slice()).collect(); + for k in ks(n) { + let got = kofn(&refs, k, &presence, rows); + let bytes = kofn_bytes(&refs, k, &presence, rows); + for row in 0..rows { + let cnt = c.state.iter().filter(|s| s[row] == 1).count(); + let want = c.present[row] && cnt >= k; + assert_eq!( + bit(&got, row), + want, + "{shape:?} n={n} rows={rows} k={k} row={row}" + ); + assert_eq!( + bit(&bytes, row), + want, + "bytes {shape:?} n={n} k={k} row={row}" + ); + } + assert!(tail_clear(&got, rows) && tail_clear(&bytes, rows)); + cells += 1; + } + } + } + } + assert_eq!(cells, 5 * 6 * 3 * 5); +} + +/// Silence twins: k = 1 is OR, k = n is AND, both under presence; k = 0 is +/// exactly the present rows (absent rows never become true); k > n is empty. +#[test] +fn boundary_ks_are_or_and_presence_and_empty() { + for &n in &NS { + let rows = 65_536 + 37; + let c = case(n, rows, Shape::Random, 99 + n as u64); + let presence = plane(rows, |r| c.present[r]); + let ins: Vec> = c.state.iter().map(|s| plane(rows, |r| s[r] == 1)).collect(); + let refs: Vec<&[u64]> = ins.iter().map(|v| v.as_slice()).collect(); + let or: Vec = (0..presence.len()) + .map(|w| refs.iter().fold(0, |a, m| a | m[w]) & presence[w]) + .collect(); + let and: Vec = (0..presence.len()) + .map(|w| refs.iter().fold(!0, |a, m| a & m[w]) & presence[w]) + .collect(); + assert_eq!(kofn(&refs, 1, &presence, rows), or); + assert_eq!(kofn(&refs, n, &presence, rows), and); + assert_eq!(kofn(&refs, 0, &presence, rows), presence); + assert!(kofn(&refs, n + 1, &presence, rows).iter().all(|&w| w == 0)); + // Anti-vacuity: the middle k is neither the OR nor the AND. + if n >= 4 { + let mid = kofn(&refs, n.div_ceil(2), &presence, rows); + assert!(mid != or && mid != and, "n={n}"); + } + } +} + +/// A5: Kleene. TRUE iff the TRUE count reaches k; FALSE iff TRUE + UNKNOWN +/// does not; UNKNOWN otherwise. UNKNOWN is never turned into FALSE before the +/// terminal, and an absent row is neither TRUE nor UNKNOWN. +#[test] +fn kleene_kofn_keeps_unknown_and_matches_the_oracle() { + let mut unknowns = 0; + for &n in &NS { + for &rows in &ROWS { + let c = case(n, rows, Shape::RandomKleene, (n * 31 + rows) as u64); + let presence = plane(rows, |r| c.present[r]); + let t: Vec> = c.state.iter().map(|s| plane(rows, |r| s[r] == 1)).collect(); + let u: Vec> = c.state.iter().map(|s| plane(rows, |r| s[r] == 2)).collect(); + let tr: Vec<&[u64]> = t.iter().map(|v| v.as_slice()).collect(); + let ur: Vec<&[u64]> = u.iter().map(|v| v.as_slice()).collect(); + for k in ks(n) { + let (yes, unk) = kofn_kleene(&tr, &ur, k, &presence, rows); + for row in 0..rows { + let ct = c.state.iter().filter(|s| s[row] == 1).count(); + let cu = c.state.iter().filter(|s| s[row] == 2).count(); + let (want_t, want_u) = if !c.present[row] { + (false, false) + } else if ct >= k { + (true, false) + } else if ct + cu >= k { + (false, true) + } else { + (false, false) + }; + assert_eq!( + (bit(&yes, row), bit(&unk, row)), + (want_t, want_u), + "n={n} k={k} row={row}" + ); + unknowns += usize::from(want_u); + } + assert!(tail_clear(&yes, rows) && tail_clear(&unk, rows)); + } + } + } + assert!( + unknowns > 1000, + "the fixture must produce UNKNOWN results: {unknowns}" + ); +} + +/// A6: Bag multiplicity is not support. Same support (every input present at +/// least once), different sums: the Bag threshold separates them, the support +/// count cannot. +#[test] +fn bag_sums_differ_from_support_counts() { + let rows = 4096 + 5; + let mut r = rng(5); + let n = 5; + // multiplicity m[i][row] in 0..=3 + let m: Vec> = (0..n) + .map(|_| (0..rows).map(|_| (r() % 4) as u8).collect()) + .collect(); + let present: Vec = (0..rows).map(|row| row % 11 != 3).collect(); + let presence = plane(rows, |row| present[row]); + let lo: Vec> = m + .iter() + .map(|v| plane(rows, |row| v[row] & 1 == 1)) + .collect(); + let hi: Vec> = m + .iter() + .map(|v| plane(rows, |row| v[row] & 2 == 2)) + .collect(); + let support: Vec> = m.iter().map(|v| plane(rows, |row| v[row] > 0)).collect(); + let lr: Vec<&[u64]> = lo.iter().map(|v| v.as_slice()).collect(); + let hr: Vec<&[u64]> = hi.iter().map(|v| v.as_slice()).collect(); + let sr: Vec<&[u64]> = support.iter().map(|v| v.as_slice()).collect(); + let mut differ = 0; + for k in [0, 1, 3, 5, 8, 12, 15, 16] { + let bag = bag_at_least(&lr, &hr, k, &presence, rows); + let sup = kofn(&sr, k, &presence, rows); + for row in 0..rows { + let sum: usize = m.iter().map(|v| usize::from(v[row])).sum(); + assert_eq!(bit(&bag, row), present[row] && sum >= k, "k={k} row={row}"); + } + differ += usize::from(bag != sup); + assert!(tail_clear(&bag, rows)); + } + assert!( + differ >= 4, + "Bag and support must disagree on several k: {differ}" + ); +} + +/// A7 negative control: 3-of-5 by carry words equals the 10-term native +/// sum of products (the timing comparison is in the bench, not asserted). +#[test] +fn three_of_five_matches_its_boolean_expansion() { + let rows = 65_536 + 37; + let c = case(5, rows, Shape::Random, 77); + let presence = plane(rows, |r| c.present[r]); + let ins: Vec> = c.state.iter().map(|s| plane(rows, |r| s[r] == 1)).collect(); + let refs: Vec<&[u64]> = ins.iter().map(|v| v.as_slice()).collect(); + let arr: [&[u64]; 5] = [refs[0], refs[1], refs[2], refs[3], refs[4]]; + assert_eq!( + kofn(&refs, 3, &presence, rows), + three_of_five_sop(&arr, &presence, rows) + ); +} + +/// A presence plane whose tail word carries stray bits past `n_rows` (a +/// caller that did not clear it) must not leak them into any result. +#[test] +fn a_dirty_presence_tail_never_reaches_the_result() { + let rows = 4096 + 37; + let c = case(5, rows, Shape::Full, 3); + let mut presence = plane(rows, |r| c.present[r]); + *presence.last_mut().unwrap() |= !((1u64 << (rows % 64)) - 1); + let ins: Vec> = c.state.iter().map(|s| plane(rows, |r| s[r] == 1)).collect(); + let refs: Vec<&[u64]> = ins.iter().map(|v| v.as_slice()).collect(); + for k in [0, 1, 3, 5] { + assert!( + tail_clear(&kofn(&refs, k, &presence, rows), rows), + "kofn k={k}" + ); + assert!( + tail_clear(&kofn_bytes(&refs, k, &presence, rows), rows), + "bytes k={k}" + ); + } + let none = vec![0u64; presence.len()]; + let unknown: Vec<&[u64]> = vec![none.as_slice(); refs.len()]; + let (yes, unk) = kofn_kleene(&refs, &unknown, 0, &presence, rows); + assert!(tail_clear(&yes, rows) && tail_clear(&unk, rows)); +} diff --git a/crates/drisa-register-probe/tests/integration/main.rs b/crates/drisa-register-probe/tests/integration/main.rs index f862bee24..28c0e18ec 100644 --- a/crates/drisa-register-probe/tests/integration/main.rs +++ b/crates/drisa-register-probe/tests/integration/main.rs @@ -1 +1,2 @@ +pub mod alu; pub mod register;