D-DRISA-3 (lab): threshold, Kleene and Bag on the shipped carry words (stacked on #1955)

.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 |

.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.

.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) |

.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

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"] }

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<Vec<u64>> {
+    let mut r = rng(seed);
+    let words = ROWS.div_ceil(64);
+    (0..n).map(|_| (0..words).map(|_| r()).collect()).collect()
+}
+
+fn time<T>(mut f: impl FnMut() -> T) -> f64 {
+    let mut v: Vec<f64> = (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<u64>, Vec<u64>) {
+    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<u64> {
+    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<u64> { (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
+    );
+}