From e12a33a2f3f5c9677bad9d81ce6aabc3fc8f2f93 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 23:21:46 +0000 Subject: [PATCH 1/4] D-POF-ANT-0: Position x Order x Law antennas (lab) Six antennas as isolated example + test code, no facade, backend or storage change: A1 position (shared and re-based bases over Perm64), A2 exposure (E2 sign-routed operand reused by the anchor, E3 two fused consumers), A3/A4 order and law (admitted and refused rewrites, each with a negative example), A5 receipt-only meta fold, A6 64x64 field per-cell vs exposure, row-major vs Morton. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMMjKnig6MXTd41Lf2v --- Cargo.toml | 5 + examples/pof_antennas/exposure.rs | 148 +++++ examples/pof_antennas/main.rs | 474 ++++++++++++++++ examples/pof_antennas/meta.rs | 859 +++++++++++++++++++++++++++++ examples/pof_antennas/order_law.rs | 847 ++++++++++++++++++++++++++++ examples/pof_antennas/position.rs | 451 +++++++++++++++ examples/pof_antennas/scale.rs | 167 ++++++ tests/pof_antennas.rs | 145 +++++ 8 files changed, 3096 insertions(+) create mode 100644 examples/pof_antennas/exposure.rs create mode 100644 examples/pof_antennas/main.rs create mode 100644 examples/pof_antennas/meta.rs create mode 100644 examples/pof_antennas/order_law.rs create mode 100644 examples/pof_antennas/position.rs create mode 100644 examples/pof_antennas/scale.rs create mode 100644 tests/pof_antennas.rs diff --git a/Cargo.toml b/Cargo.toml index 01fcd5af..703ce1dd 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -71,6 +71,11 @@ name = "u9_head_to_head" path = "examples/u9_head_to_head/main.rs" required-features = ["std"] +[[example]] +name = "pof_antennas" +path = "examples/pof_antennas/main.rs" +required-features = ["std"] + [[example]] name = "u9_abacus" path = "examples/u9_abacus/main.rs" diff --git a/examples/pof_antennas/exposure.rs b/examples/pof_antennas/exposure.rs new file mode 100644 index 00000000..fed5a5d4 --- /dev/null +++ b/examples/pof_antennas/exposure.rs @@ -0,0 +1,148 @@ +//! A2, the exposure antenna: one prepared input, several output shapes. +//! +//! Fixture: the U9 block of #388 (64 `u8` magnitudes + one polarity plane per +//! operand). One prepared input feeds three output shapes: +//! +//! * masked byte-dot → 16 `i32` accumulators (B, and E5's `low7` half); +//! * masked SAD → 8 `u64` accumulators (E5's anchor); +//! * the exact signed fold → one `i64`. +//! +//! Candidates (E0 and E1 are the existing, unchanged kernels): +//! +//! * E0 = B (`kernels::AccB`), E1 = E5 (`anchor::AccE5`); +//! * E2 ([`AccE2`]): the sign-routed operand is prepared ONCE as two +//! zero-masked vectors `a_pos = a | !negative`, `a_neg = a | negative`. The +//! `low7` dots then run unmasked on them, and the anchor narrows them by the +//! bit-7 plane. Reuse law: `maskz(maskz(a, s), t) == maskz(a, s & t)`, so +//! `sum8(a_pos, top) == sum8(a, !negative & top)` and +//! `dot(a_pos, w) == dot_masked(a, !negative, w)`. Exact; proven per byte in +//! the tests. +//! * E3 ([`AccDual`]): two consumers fused in one pass over the same prepared +//! input: B's exact signed dot (i32 lanes, i64 total) and a second, +//! independent reduction, the sum of `|a|` over the positive-product lanes +//! (u64 lanes). They share the load of `a` and the sign plane; their +//! accumulator types and flush laws stay separate. Compared against the two +//! consumers run as two passes. + +#![allow(dead_code)] + +use crate::anchor::QueryE; +use crate::kernels::{lanes_i64, AccB, Block, B_FLUSH_BLOCKS}; +use ndarray::simd::{I32x16, I8x64, U64x8, U8x64}; + +/// E2: the sign-routed operand prepared once, narrowed for the anchor. +pub struct AccE2 { + low7: [I32x16; 2], + anchor: [U64x8; 2], + blocks: usize, + total: i64, +} + +impl AccE2 { + pub fn new() -> Self { + Self { + low7: [I32x16::splat(0); 2], + anchor: [U64x8::splat(0); 2], + blocks: 0, + total: 0, + } + } + + pub fn flush(&mut self) { + let r = self.low7.map(lanes_i64); + let anchor = self.anchor[0].reduce_sum() as i64 - self.anchor[1].reduce_sum() as i64; + self.total += (r[0] - r[1]) + (anchor << 7); + self.low7 = [I32x16::splat(0); 2]; + self.anchor = [U64x8::splat(0); 2]; + self.blocks = 0; + } + + #[inline(always)] + pub fn mac(&mut self, a: U8x64, negative: u64, low7: I8x64, top: u64) { + let zero = U8x64::splat(0); + // The prepared exposure: `a` routed by sign, once per block. + let a_pos = U8x64::mask_blend(!negative, zero, a); + let a_neg = U8x64::mask_blend(negative, zero, a); + self.low7[0] = self.low7[0].dot4_u8_i8_add(a_pos, low7); + self.low7[1] = self.low7[1].dot4_u8_i8_add(a_neg, low7); + // The anchor narrows the SAME prepared vectors by bit 7. + self.anchor[0] = self.anchor[0].sum8_u8_add_masked(a_pos, top); + self.anchor[1] = self.anchor[1].sum8_u8_add_masked(a_neg, top); + self.blocks += 1; + if self.blocks == B_FLUSH_BLOCKS { + self.flush(); + } + } + + #[inline(always)] + pub fn scan_step(&mut self, x: Block, q: &QueryE) { + self.mac(x.mag, x.positive ^ q.positive, q.low7, q.top); + } + + pub fn finish(mut self) -> i64 { + self.flush(); + self.total + } +} + +/// The second consumer alone: the sum of `|a|` over lanes whose product is +/// positive, in `u64` lanes (never flushed: 8 * 255 per block per lane). +pub struct AccPosMag { + acc: U64x8, +} + +impl AccPosMag { + pub fn new() -> Self { + Self { acc: U64x8::splat(0) } + } + + #[inline(always)] + pub fn mac(&mut self, a: U8x64, negative: u64) { + self.acc = self.acc.sum8_u8_add_masked(a, !negative); + } + + pub fn finish(self) -> u64 { + self.acc.reduce_sum() + } +} + +/// E3: B and the positive-magnitude sum fused in one pass. Each keeps its own +/// accumulator type and reduction law; only the input and the sign plane are +/// shared. +pub struct AccDual { + pub b: AccB, + pub pos_mag: AccPosMag, +} + +impl AccDual { + pub fn new() -> Self { + Self { + b: AccB::new(), + pos_mag: AccPosMag::new(), + } + } + + #[inline(always)] + pub fn mac(&mut self, a: U8x64, negative: u64, low7: I8x64, top: I8x64) { + self.b.mac(a, negative, low7, top); + self.pos_mag.mac(a, negative); + } + + pub fn finish(self) -> (i64, u64) { + (self.b.finish(), self.pos_mag.finish()) + } +} + +/// Scalar oracle for the second consumer. +pub fn pos_mag_oracle(a: &[([u8; 64], u64)], b: &[([u8; 64], u64)]) -> u64 { + let mut t = 0u64; + for ((ma, pa), (_, pb)) in a.iter().zip(b) { + let positive = !(pa ^ pb); + for (i, &m) in ma.iter().enumerate() { + if positive >> i & 1 == 1 { + t += m as u64; + } + } + } + t +} diff --git a/examples/pof_antennas/main.rs b/examples/pof_antennas/main.rs new file mode 100644 index 00000000..9a3bf6cf --- /dev/null +++ b/examples/pof_antennas/main.rs @@ -0,0 +1,474 @@ +//! D-POF-ANT-0: Position × Order × Law, the first antennas. +//! +//! Each antenna is a module with its own exact oracle and falsifiers +//! (`tests/pof_antennas.rs` runs them). This binary times the ones whose cost +//! is a question: A1 (position), A2 (exposure), A4's two assembly pairs and +//! A6 (scale). A3 and A5 are semantic antennas and have no timing. +//! +//! `cargo run --release --example pof_antennas --features std`; +//! the tier is whatever this build compiled (printed in the header). + +#[path = "../u9_abacus/anchor.rs"] +mod anchor; +mod exposure; +#[path = "../u9_head_to_head/kernels.rs"] +mod kernels; +mod meta; +mod order_law; +mod position; +mod scale; + +use anchor::{split_anchor, AccE5, QueryE}; +use exposure::{AccDual, AccE2, AccPosMag}; +use kernels::{check, oracle, prepare_b, AccB, Block, Operand, QueryB}; +use ndarray::hpc::perm::Perm64; +use ndarray::simd::{I8x64, U64x8, U8x64}; +use std::alloc::{GlobalAlloc, Layout, System}; +use std::hint::black_box; +use std::sync::atomic::{AtomicU64, Ordering}; +use std::time::Instant; + +/// Counts allocations and allocated bytes, so A6 reports them measured. +struct Counting; +static ALLOCS: AtomicU64 = AtomicU64::new(0); +static ALLOC_BYTES: AtomicU64 = AtomicU64::new(0); +unsafe impl GlobalAlloc for Counting { + unsafe fn alloc(&self, l: Layout) -> *mut u8 { + ALLOCS.fetch_add(1, Ordering::Relaxed); + ALLOC_BYTES.fetch_add(l.size() as u64, Ordering::Relaxed); + // SAFETY: forwarded unchanged to the system allocator. + unsafe { System.alloc(l) } + } + unsafe fn dealloc(&self, p: *mut u8, l: Layout) { + // SAFETY: forwarded unchanged to the system allocator. + unsafe { System.dealloc(p, l) } + } +} +#[global_allocator] +static GLOBAL: Counting = Counting; + +fn allocs() -> (u64, u64) { + (ALLOCS.load(Ordering::Relaxed), ALLOC_BYTES.load(Ordering::Relaxed)) +} + +fn tier() -> &'static str { + if cfg!(target_feature = "avx512vnni") { + "x86_64 AVX-512 + VNNI" + } else if cfg!(target_feature = "avx512bw") { + "x86_64 AVX-512 (no VNNI)" + } else if cfg!(target_feature = "avx2") { + "x86_64 AVX2" + } else if cfg!(target_arch = "aarch64") { + "aarch64 NEON" + } else { + "other" + } +} + +/// Median of `runs` timings, in ns per `unit`. +fn time(name: &str, units: usize, unit: &str, runs: usize, base: Option, f: &dyn Fn() -> i64) -> f64 { + black_box(f()); + let mut t: Vec = (0..runs) + .map(|_| { + let t0 = Instant::now(); + black_box(f()); + t0.elapsed().as_nanos() as f64 / units as f64 + }) + .collect(); + t.sort_by(f64::total_cmp); + let med = t[runs / 2]; + let rel = base + .map(|b| format!(" {:6.2}x", med / b)) + .unwrap_or_default(); + println!("{name:<62} {med:9.3} ns/{unit}{rel}"); + med +} + +type Raw = ([u8; 64], u64); + +/// Uniform over the 511 numeric U9 values (as in #388). +fn data(blocks: usize, seed: u64) -> (Vec, Vec) { + let mut s = seed; + let mut next = move || { + s = s + .wrapping_mul(6_364_136_223_846_793_005) + .wrapping_add(1_442_695_040_888_963_407); + (s >> 33) as u32 + }; + let mut mk = || { + let mut m = [0u8; 64]; + let mut p = 0u64; + for (i, mi) in m.iter_mut().enumerate() { + let v = (next() % 511) as i32 - 255; + *mi = v.unsigned_abs() as u8; + p |= u64::from(v >= 0) << i; + } + (m, p) + }; + let a = (0..blocks).map(|_| mk()).collect(); + let b = (0..blocks).map(|_| mk()).collect(); + (a, b) +} + +fn perm(seed: u64) -> Perm64 { + let mut idx: [u8; 64] = core::array::from_fn(|i| i as u8); + let mut s = seed | 1; + for i in (1..64).rev() { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + idx.swap(i, (s % (i as u64 + 1)) as usize); + } + Perm64::from_indices(idx).unwrap() +} + +// ---- A1 ------------------------------------------------------------------ + +fn bench_a1(label: &str, n: usize, runs: usize) { + use position::*; + let raw: Vec = (0..n).map(|k| fixture(1, 0x9E37_79B9 ^ k as u64)).collect(); + let prepared: Vec = raw.iter().map(Prepared::new).collect(); + let p = perm(77); + let rebased: Vec = prepared.iter().map(|x| x.rebase(p)).collect(); + for (r, x) in raw.iter().zip(&rebased) { + assert_eq!(x.run(1).unwrap(), oracle(&permute_raw(r, p))); + } + let fold = |r: Results| r.count as i64 ^ r.signed_sum ^ r.select as i64; + let p0 = || { + raw.iter() + .map(|r| fold(p0_separate(r))) + .fold(0, i64::wrapping_add) + }; + let p1 = || { + raw.iter() + .map(|r| fold(Prepared::new(r).run(1).unwrap())) + .fold(0, i64::wrapping_add) + }; + let setup = || { + raw.iter() + .map(|r| { + black_box(Prepared::new(r)); + 0 + }) + .sum() + }; + let p1_exec = || { + prepared + .iter() + .map(|x| fold(x.run(1).unwrap())) + .fold(0, i64::wrapping_add) + }; + let rebase = || { + prepared + .iter() + .map(|x| { + black_box(x.rebase(p)); + 0 + }) + .sum() + }; + let p2_exec = || { + rebased + .iter() + .map(|x| fold(x.run(1).unwrap())) + .fold(0, i64::wrapping_add) + }; + let p2 = || { + raw.iter() + .map(|r| fold(Prepared::new(r).rebase(p).run(1).unwrap())) + .fold(0, i64::wrapping_add) + }; + let lazy = || { + prepared + .iter() + .map(|x| fold(x.run_rebased_lazy(p, 1).unwrap())) + .fold(0, i64::wrapping_add) + }; + let blended = || { + prepared + .iter() + .map(|x| { + black_box(conjugate_mask_blended(&p, x.mask_pred())); + black_box(conjugate_mask_blended(&p, x.mask_positive())); + black_box(conjugate_mask_blended(&p, x.mask_sel())); + 0 + }) + .sum() + }; + let materialize_all = || { + raw.iter() + .map(|r| { + black_box(permute_raw(r, p)); + 0 + }) + .sum() + }; + println!("-- A1 position, {label}: {n} blocks of 64 positions (4 byte planes = 256 B read per block)"); + let b0 = time("P0 separate preparation per operation", n, "block", runs, None, &p0); + time("P1 shared basis: prepare + run", n, "block", runs, Some(b0), &p1); + time(" P1 setup only (4 planes -> 3 masks + magnitudes)", n, "block", runs, Some(b0), &setup); + time(" P1 execution only (prepared basis given)", n, "block", runs, Some(b0), &p1_exec); + time("P2 re-based: prepare + rebase + run", n, "block", runs, Some(b0), &p2); + time(" P2 rebase only (3 conjugate_mask)", n, "block", runs, Some(b0), &rebase); + time(" P2 execution only (re-based basis given)", n, "block", runs, Some(b0), &p2_exec); + time( + "P2-lazy: prepared, run in source, conjugate the select result once", + n, + "block", + runs, + Some(b0), + &lazy, + ); + time( + " rebase only, blended mask expansion (3 x mask_blend + materialize)", + n, + "block", + runs, + Some(b0), + &blended, + ); + time( + " reference: materialize all 4 planes through the map", + n, + "block", + runs, + Some(b0), + &materialize_all, + ); +} + +// ---- A2 ------------------------------------------------------------------ + +fn bench_a2(label: &str, n: usize, runs: usize, seed: u64) { + let (ra, rb) = data(n, seed); + let (ab, bb) = (Operand::new(&ra), Operand::new(&rb)); + let want = oracle(&ra, &rb).unwrap(); + let q = bb.block(0); + let want_scan = oracle(&ra, &vec![rb[0]; n]).unwrap(); + let split: Vec<(u64, I8x64, I8x64)> = ab + .blocks() + .zip(bb.blocks()) + .map(|(a, b)| prepare_b(a, b)) + .collect(); + let anc: Vec<(u64, I8x64, u64)> = ab + .blocks() + .zip(bb.blocks()) + .map(|(a, b)| { + let (l, t) = split_anchor(b.mag); + (a.positive ^ b.positive, l, t) + }) + .collect(); + + let b_e2e = || { + let mut acc = AccB::new(); + for (a, b) in ab.blocks().zip(bb.blocks()) { + check(a, b).unwrap(); + acc.step(a, b); + } + acc.finish() + }; + let e5_e2e = || { + let mut acc = AccE5::new(); + for (a, b) in ab.blocks().zip(bb.blocks()) { + check(a, b).unwrap(); + acc.step(a, b); + } + acc.finish() + }; + let e2_e2e = || { + let mut acc = AccE2::new(); + for (a, b) in ab.blocks().zip(bb.blocks()) { + check(a, b).unwrap(); + let (l, t) = split_anchor(b.mag); + acc.mac(a.mag, a.positive ^ b.positive, l, t); + } + acc.finish() + }; + let b_ari = || asm_b_loop(&ab.mag, &split); + let e5_ari = || asm_e5_loop(&ab.mag, &anc); + let e2_ari = || asm_e2_loop(&ab.mag, &anc); + let b_scan = || { + let qb = QueryB::new(q); + let mut acc = AccB::new(); + for x in ab.blocks() { + check(x, q).unwrap(); + acc.scan_step(x, &qb); + } + acc.finish() + }; + let e5_scan = || { + let qe = QueryE::new(q); + let mut acc = AccE5::new(); + for x in ab.blocks() { + check(x, q).unwrap(); + acc.scan_step(x, &qe); + } + acc.finish() + }; + let e2_scan = || { + let qe = QueryE::new(q); + let mut acc = AccE2::new(); + for x in ab.blocks() { + check(x, q).unwrap(); + acc.scan_step(x, &qe); + } + acc.finish() + }; + let dual_fused = || { + let (t, m) = asm_dual_loop(&ab.mag, &split); + t ^ m as i64 + }; + let dual_separate = || { + let t = asm_b_loop(&ab.mag, &split); + let m = asm_posmag_loop(&ab.mag, &split); + t ^ m as i64 + }; + for (name, f, w) in [ + ("B e2e", &b_e2e as &dyn Fn() -> i64, want), + ("E5 e2e", &e5_e2e, want), + ("E2 e2e", &e2_e2e, want), + ("B ari", &b_ari, want), + ("E5 ari", &e5_ari, want), + ("E2 ari", &e2_ari, want), + ("B scan", &b_scan, want_scan), + ("E5 scan", &e5_scan, want_scan), + ("E2 scan", &e2_scan, want_scan), + ] { + assert_eq!(f(), w, "{name} disagrees with the oracle"); + } + assert_eq!(dual_fused(), dual_separate()); + + println!("-- A2 exposure, {label}: {n} blocks of 64 values per operand"); + let be = time("E0 = B end-to-end", n, "64", runs, None, &b_e2e); + time("E1 = E5 end-to-end (unchanged, #393)", n, "64", runs, Some(be), &e5_e2e); + time("E2 end-to-end: sign-routed operand once, anchor narrows it", n, "64", runs, Some(be), &e2_e2e); + let ba = time("E0 = B arithmetic only", n, "64", runs, None, &b_ari); + time("E1 = E5 arithmetic only", n, "64", runs, Some(ba), &e5_ari); + time("E2 arithmetic only", n, "64", runs, Some(ba), &e2_ari); + let bs = time("E0 = B scan", n, "64", runs, None, &b_scan); + time("E1 = E5 scan", n, "64", runs, Some(bs), &e5_scan); + time("E2 scan", n, "64", runs, Some(bs), &e2_scan); + let sep = time("E3 two consumers, two passes (B + positive-|a| sum)", n, "64", runs, None, &dual_separate); + time("E3 two consumers fused in one pass", n, "64", runs, Some(sep), &dual_fused); +} + +#[inline(never)] +pub fn asm_b_loop(mags: &[U8x64], split: &[(u64, I8x64, I8x64)]) -> i64 { + let mut acc = AccB::new(); + for (a, (ng, l, t)) in mags.iter().zip(split) { + acc.mac(*a, *ng, *l, *t); + } + acc.finish() +} +#[inline(never)] +pub fn asm_e5_loop(mags: &[U8x64], anc: &[(u64, I8x64, u64)]) -> i64 { + let mut acc = AccE5::new(); + for (a, (ng, l, t)) in mags.iter().zip(anc) { + acc.mac(*a, *ng, *l, *t); + } + acc.finish() +} +#[inline(never)] +pub fn asm_e2_loop(mags: &[U8x64], anc: &[(u64, I8x64, u64)]) -> i64 { + let mut acc = AccE2::new(); + for (a, (ng, l, t)) in mags.iter().zip(anc) { + acc.mac(*a, *ng, *l, *t); + } + acc.finish() +} +#[inline(never)] +pub fn asm_dual_loop(mags: &[U8x64], split: &[(u64, I8x64, I8x64)]) -> (i64, u64) { + let mut acc = AccDual::new(); + for (a, (ng, l, t)) in mags.iter().zip(split) { + acc.mac(*a, *ng, *l, *t); + } + acc.finish() +} +#[inline(never)] +pub fn asm_posmag_loop(mags: &[U8x64], split: &[(u64, I8x64, I8x64)]) -> u64 { + let mut acc = AccPosMag::new(); + for (a, (ng, _, _)) in mags.iter().zip(split) { + acc.mac(*a, *ng); + } + acc.finish() +} + +// ---- A4: the obvious optimized expression vs the direct baseline --------- + +/// Count after moving the data through the map (direct baseline). +#[inline(never)] +pub fn asm_count_after_perm(p: &Perm64, a: &[u8; 64]) -> u32 { + p.materialize(a).iter().filter(|&&v| v != 0).count() as u32 +} +/// Count with the map skipped: admitted only because count is invariant. +#[inline(never)] +pub fn asm_count_skipping_perm(_p: &Perm64, a: &[u8; 64]) -> u32 { + U8x64::from_array(*a) + .cmpeq_mask(U8x64::splat(0)) + .count_zeros() +} +/// (a ^ b) & c as two lane operations. +#[inline(never)] +pub fn asm_xor_then_and(a: U64x8, b: U64x8, c: U64x8) -> U64x8 { + (a ^ b) & c +} +/// (a ^ b) & c as one ternary-logic operation (immediate 0x28). +#[inline(never)] +pub fn asm_fused_ternlog(a: U64x8, b: U64x8, c: U64x8) -> U64x8 { + a.ternlog::<0x28>(b, c) +} + +// ---- A6 ------------------------------------------------------------------ + +fn bench_a6(runs: usize) { + use scale::*; + let t = table(0x51_7CC1_B727_220A); + let (a, b) = (0xF0F0_1234_8000_0001u64, 0x0FF0_F00F_5555_AAAAu64); + let (ab, bb) = (bytes_of(a), bytes_of(b)); + let (rm, mo) = (row_major(), morton()); + let want = oracle(&t, a, b); + type Row<'a> = (&'a str, Box (u64, Traffic) + 'a>); + let rows: [Row; 5] = [ + ("per cell, materialized, row-major", Box::new(|| per_cell_materialized(&t, &ab, &bb, &rm))), + ("per cell, materialized, Morton", Box::new(|| per_cell_materialized(&t, &ab, &bb, &mo))), + ("per cell, conjugated mask, row-major", Box::new(|| per_cell_conjugated(&t, a, b, &rm))), + ("per cell, conjugated mask, Morton", Box::new(|| per_cell_conjugated(&t, a, b, &mo))), + ("whole field through the exposure (64x64 u16 kernel)", Box::new(|| whole_field_exposure(&t, a, b))), + ]; + println!("-- A6 scale: 64x64 field (4096 cells), one field-wide count; table working set 8 KiB"); + let mut base = None; + for (name, f) in &rows { + let (got, tr) = f(); + assert_eq!(got, want, "{name}"); + let (n0, b0) = allocs(); + black_box(f()); + let (n1, b1) = allocs(); + let med = time(name, 1, "field", runs, base, &|| f().0 as i64); + base.get_or_insert(med); + println!( + " compositions {}, bytes written {}, allocations {} ({} B)", + tr.compositions, + tr.bytes_written, + n1 - n0, + b1 - b0 + ); + } +} + +fn main() { + println!("tier: {} (target-cpu as compiled)", tier()); + { + // Keep the out-of-line copies in the binary for the disassembly. + let (a, b, c) = (black_box(U64x8::splat(3)), black_box(U64x8::splat(5)), black_box(U64x8::splat(9))); + assert_eq!(asm_xor_then_and(a, b, c).to_array(), asm_fused_ternlog(a, b, c).to_array()); + let p = perm(5); + let blk: [u8; 64] = core::array::from_fn(|i| (i % 3) as u8); + assert_eq!(asm_count_after_perm(&p, &blk), asm_count_skipping_perm(&p, &blk)); + let _: Block; + } + bench_a1("L1-resident", 64, 2001); + bench_a1("streamed", 1 << 18, 9); + bench_a2("L1-resident", 64, 2001, 1); + bench_a2("streamed", 1 << 20, 5, 2); + bench_a6(201); +} diff --git a/examples/pof_antennas/meta.rs b/examples/pof_antennas/meta.rs new file mode 100644 index 00000000..80a068c2 --- /dev/null +++ b/examples/pof_antennas/meta.rs @@ -0,0 +1,859 @@ +#![allow(dead_code)] +//! Scalar oracle for "one fold inspects another fold's receipt". +//! +//! First-level fold: `evaluate` reads a sealed [`World`] (optionally through a +//! speculative [`Thought`]), applies ordered [`Step`]s, then a Kleene +//! [`Method`], and emits a [`Receipt`]. +//! +//! Second-level (meta) fold: `compare`, `may_reuse`, `aggregate`, +//! `which_changed` and `meta_evaluate` take receipts only (plus, for reuse, a +//! version lookup). Their signatures never mention `World`, `Thought` or a fact +//! array, so the meta fold cannot read the underlying facts. +//! +//! Mock typed data only; plain safe std Rust, no global state. + +/// Three-valued (Kleene) truth. `Unknown` is a value, never coerced silently. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Tri { + /// Known true. + True, + /// Known false. + False, + /// Not known either way. + Unknown, +} + +impl Tri { + /// Kleene conjunction: False dominates, then Unknown, then True. + pub fn and(self, o: Tri) -> Tri { + match (self, o) { + (Tri::False, _) | (_, Tri::False) => Tri::False, + (Tri::True, Tri::True) => Tri::True, + _ => Tri::Unknown, + } + } + + /// Kleene disjunction: True dominates, then Unknown, then False. + pub fn or(self, o: Tri) -> Tri { + match (self, o) { + (Tri::True, _) | (_, Tri::True) => Tri::True, + (Tri::False, Tri::False) => Tri::False, + _ => Tri::Unknown, + } + } + + /// Kleene negation; `Unknown` stays `Unknown`. + pub fn not(self) -> Tri { + match self { + Tri::True => Tri::False, + Tri::False => Tri::True, + Tri::Unknown => Tri::Unknown, + } + } + + fn byte(self) -> u8 { + match self { + Tri::False => 0, + Tri::True => 1, + Tri::Unknown => 2, + } + } +} + +/// How `Unknown` is treated when a method runs. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Policy { + /// Unknown stays Unknown. + OpenWorld, + /// Unknown is explicitly mapped to False before the method runs. + ClosedWorld, +} + +impl Policy { + fn dep_id(self) -> u64 { + match self { + Policy::OpenWorld => 0, + Policy::ClosedWorld => 1, + } + } +} + +/// A sealed 64-lane world at one version. There is no `&mut` method. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct World { + /// World identity (stable across versions). + pub id: u32, + /// Monotone version. + pub version: u64, + facts: [Tri; 64], +} + +impl World { + /// Build a world from explicit facts. + pub fn new(id: u32, version: u64, facts: [Tri; 64]) -> World { + World { id, version, facts } + } + + /// Fact at lane `i` (`Unknown` if out of range). + pub fn fact(&self, i: usize) -> Tri { + if i < 64 { + self.facts[i] + } else { + Tri::Unknown + } + } + + /// New world, same id, version + 1, with `changes` applied. + pub fn advance(&self, changes: &[(usize, Tri)]) -> World { + let mut facts = self.facts; + for &(i, t) in changes { + if i < 64 { + facts[i] = t; + } + } + World { + id: self.id, + version: self.version + 1, + facts, + } + } +} + +/// A speculative projection over one world version. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Thought { + /// Branch identity. + pub branch: u32, + /// World version this thought was made against. + pub base_version: u64, + /// Lane overrides. + pub overlay: Vec<(usize, Tri)>, +} + +/// Why a view was refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Stale { + /// The thought's base version is not the world's version. + World { + /// World's current version. + expected: u64, + /// Version the thought was based on. + found: u64, + }, +} + +/// World facts with the thought overlay applied; refuses a stale thought. +pub fn view(w: &World, t: Option<&Thought>) -> Result<[Tri; 64], Stale> { + let mut v = w.facts; + if let Some(t) = t { + if t.base_version != w.version { + return Err(Stale::World { + expected: w.version, + found: t.base_version, + }); + } + for &(i, x) in &t.overlay { + if i < 64 { + v[i] = x; + } + } + } + Ok(v) +} + +/// A Kleene method over a lane set. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Method { + /// Conjunction over the lanes. + AllOf { + /// Method id. + id: u32, + /// Lane bitmask. + lanes: u64, + }, + /// Disjunction over the lanes. + AnyOf { + /// Method id. + id: u32, + /// Lane bitmask. + lanes: u64, + }, + /// At least `k` lanes true. + AtLeast { + /// Method id. + id: u32, + /// Lane bitmask. + lanes: u64, + /// Threshold. + k: u32, + }, +} + +impl Method { + /// Method id. + pub fn id(&self) -> u32 { + match *self { + Method::AllOf { id, .. } | Method::AnyOf { id, .. } | Method::AtLeast { id, .. } => id, + } + } + + /// Lane bitmask. + pub fn lanes(&self) -> u64 { + match *self { + Method::AllOf { lanes, .. } | Method::AnyOf { lanes, .. } | Method::AtLeast { lanes, .. } => lanes, + } + } +} + +/// Run a method over `v` under policy `p` (ClosedWorld coerces Unknown first). +pub fn apply_method(m: &Method, v: &[Tri; 64], p: Policy) -> Tri { + let lane = |i: usize| -> Tri { + let t = v[i]; + if p == Policy::ClosedWorld && t == Tri::Unknown { + Tri::False + } else { + t + } + }; + let selected = (0..64usize).filter(|i| (m.lanes() >> i) & 1 == 1); + match *m { + Method::AllOf { .. } => selected.fold(Tri::True, |a, i| a.and(lane(i))), + Method::AnyOf { .. } => selected.fold(Tri::False, |a, i| a.or(lane(i))), + Method::AtLeast { k, .. } => { + let (mut t, mut u) = (0u32, 0u32); + for i in selected { + match lane(i) { + Tri::True => t += 1, + Tri::Unknown => u += 1, + Tri::False => {} + } + } + if t >= k { + Tri::True + } else if t + u < k { + Tri::False + } else { + Tri::Unknown + } + } + } +} + +/// An ordered effect on the view. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Step { + /// Overwrite a lane. + SetFact(usize, Tri), + /// Negate a lane (Kleene). + NegateFact(usize), +} + +/// Apply steps in order. +pub fn apply_steps(mut v: [Tri; 64], steps: &[Step]) -> [Tri; 64] { + for s in steps { + match *s { + Step::SetFact(i, t) => { + if i < 64 { + v[i] = t; + } + } + Step::NegateFact(i) => { + if i < 64 { + v[i] = v[i].not(); + } + } + } + } + v +} + +/// Order-sensitive FNV-1a over a canonical byte encoding of the step list. +pub fn order_witness(steps: &[Step]) -> u64 { + let mut h: u64 = 0xcbf2_9ce4_8422_2325; + let mut eat = |b: u8| { + h ^= b as u64; + h = h.wrapping_mul(0x0000_0100_0000_01b3); + }; + for s in steps { + let (tag, i, t) = match *s { + Step::SetFact(i, t) => (1u8, i as u8, t.byte()), + Step::NegateFact(i) => (2u8, i as u8, 0u8), + }; + eat(tag); + eat(i); + eat(t); + } + h +} + +/// What a receipt says was consulted. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Evidence { + /// World id. + pub world_id: u32, + /// World version. + pub world_version: u64, + /// Lane mask the method read. + pub lanes_consulted: u64, +} + +/// Kind of dependency a receipt recorded. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum DepKind { + /// A world (id, version). + World, + /// A thought (branch, base_version). + Thought, + /// A method (id, 0). + Method, + /// A policy (0 open / 1 closed, 0). + Policy, + /// A step sequence (order witness, 0). + Steps, +} + +/// One recorded dependency. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Dep { + /// Kind. + pub kind: DepKind, + /// Identity within the kind. + pub id: u64, + /// Version recorded at evaluation time. + pub version: u64, +} + +/// A first-level fold's receipt. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Receipt { + /// Receipt identity. + pub receipt_id: u64, + /// (world id, world version). + pub frame: (u32, u64), + /// Basis identity. + pub basis_id: u64, + /// Thought branch, if any. + pub thought: Option, + /// Method id. + pub method_id: u32, + /// Order witness of the step list. + pub order_witness: u64, + /// Law that produced the result. + pub law: &'static str, + /// Policy that ran. + pub policy: Policy, + /// Result. + pub result: Tri, + /// Evidence consulted. + pub evidence: Evidence, + /// Recorded dependencies. + pub deps: Vec, +} + +/// First-level fold: view, then steps, then method. +pub fn evaluate( + receipt_id: u64, w: &World, t: Option<&Thought>, steps: &[Step], m: &Method, p: Policy, basis_id: u64, +) -> Result { + let v = view(w, t)?; + let v = apply_steps(v, steps); + let result = apply_method(m, &v, p); + let witness = order_witness(steps); + let mut deps = vec![Dep { + kind: DepKind::World, + id: w.id as u64, + version: w.version, + }]; + if let Some(t) = t { + deps.push(Dep { + kind: DepKind::Thought, + id: t.branch as u64, + version: t.base_version, + }); + } + deps.push(Dep { + kind: DepKind::Method, + id: m.id() as u64, + version: 0, + }); + deps.push(Dep { + kind: DepKind::Policy, + id: p.dep_id(), + version: 0, + }); + deps.push(Dep { + kind: DepKind::Steps, + id: witness, + version: 0, + }); + Ok(Receipt { + receipt_id, + frame: (w.id, w.version), + basis_id, + thought: t.map(|t| t.branch), + method_id: m.id(), + order_witness: witness, + law: "kleene-fold", + policy: p, + result, + evidence: Evidence { + world_id: w.id, + world_version: w.version, + lanes_consulted: m.lanes(), + }, + deps, + }) +} + +// --------------------------------------------------------------------------- +// Second-level (meta) fold: receipts only. +// --------------------------------------------------------------------------- + +/// Field-wise difference between two receipts. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Diff { + /// Results differ. + pub result_changed: bool, + /// Thought branches differ. + pub thought_changed: bool, + /// World id/version or lanes consulted differ. + pub evidence_changed: bool, + /// Policy differs. + pub rule_changed: bool, + /// Method id differs. + pub method_changed: bool, + /// Order witness differs. + pub order_changed: bool, +} + +impl Diff { + /// True if any field changed. + pub fn any(&self) -> bool { + self.result_changed + || self.thought_changed + || self.evidence_changed + || self.rule_changed + || self.method_changed + || self.order_changed + } +} + +/// Compare two receipts without touching any world. +pub fn compare(a: &Receipt, b: &Receipt) -> Diff { + Diff { + result_changed: a.result != b.result, + thought_changed: a.thought != b.thought, + evidence_changed: a.evidence != b.evidence, + rule_changed: a.policy != b.policy, + method_changed: a.method_id != b.method_id, + order_changed: a.order_witness != b.order_witness, + } +} + +/// Why a receipt may not be reused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Invalidated { + /// A dependency's current version differs from the recorded one. + StaleDep { + /// Dependency kind. + kind: DepKind, + /// Dependency id. + id: u64, + /// Version recorded in the receipt. + recorded: u64, + /// Version now (`u64::MAX` if the dependency is gone). + current: u64, + }, + /// The requested step order is not the one the receipt ran. + OrderChanged { + /// Witness recorded. + recorded: u64, + /// Witness requested. + requested: u64, + }, +} + +/// Reuse check: every dep version unchanged and the order witness matches. +pub fn may_reuse( + r: &Receipt, current_version: &dyn Fn(&DepKind, u64) -> Option, requested_order: u64, +) -> Result<(), Invalidated> { + for d in &r.deps { + let current = current_version(&d.kind, d.id).unwrap_or(u64::MAX); + if current != d.version { + return Err(Invalidated::StaleDep { + kind: d.kind, + id: d.id, + recorded: d.version, + current, + }); + } + } + if r.order_witness != requested_order { + return Err(Invalidated::OrderChanged { + recorded: r.order_witness, + requested: requested_order, + }); + } + Ok(()) +} + +/// Receipt over receipts: children, union of deps, Kleene AND of results. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct AggregateReceipt { + /// Child receipt ids. + pub children: Vec, + /// De-duplicated union of child deps. + pub deps: Vec, + /// Kleene AND over child results. + pub result: Tri, +} + +/// Aggregate receipts, preserving provenance. +pub fn aggregate(rs: &[Receipt]) -> AggregateReceipt { + let mut deps: Vec = Vec::new(); + for r in rs { + for d in &r.deps { + if !deps.contains(d) { + deps.push(*d); + } + } + } + AggregateReceipt { + children: rs.iter().map(|r| r.receipt_id).collect(), + deps, + result: rs.iter().fold(Tri::True, |a, r| a.and(r.result)), + } +} + +/// Pair receipts by `method_id`; report `(next receipt id, diff)` where any field changed. +pub fn which_changed(prev: &[Receipt], next: &[Receipt]) -> Vec<(u64, Diff)> { + let mut out = Vec::new(); + for n in next { + if let Some(p) = prev.iter().find(|p| p.method_id == n.method_id) { + let d = compare(p, n); + if d.any() { + out.push((n.receipt_id, d)); + } + } + } + out +} + +/// Answers to the meta questions, derived from two receipts alone. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct MetaVerdict { + /// The alt thought branch, if switching thought is what changed the result. + pub thought_changed_result: Option, + /// Evidence consulted differs. + pub evidence_changed: bool, + /// Only the policy differs (same evidence, thought, method and order). + pub only_rule_changed: bool, +} + +/// Meta-evaluate `alt` against `base` from receipts only. +pub fn meta_evaluate(base: &Receipt, alt: &Receipt) -> MetaVerdict { + let d = compare(base, alt); + MetaVerdict { + thought_changed_result: if d.thought_changed && d.result_changed { + alt.thought + } else { + None + }, + evidence_changed: d.evidence_changed, + only_rule_changed: d.rule_changed + && !d.evidence_changed + && !d.thought_changed + && !d.method_changed + && !d.order_changed, + } +} + +// --------------------------------------------------------------------------- +// Fixture +// --------------------------------------------------------------------------- + +/// Mock data for the probe and its tests. +pub struct Fixture { + /// World id 7, version 1. + pub world: World, + /// Branch 1: flips lane 5 (read by `m1`) to True. + pub t1: Thought, + /// Branch 2: changes lane 60, which no method reads. + pub t2: Thought, + /// AllOf over lanes 0..8. + pub m1: Method, + /// AnyOf over lanes 10..16 (lane 12 Unknown). + pub m2: Method, + /// AtLeast 3 over lanes 20..25 (lane 22 Unknown). + pub m3: Method, + /// `[SetFact(3, True), NegateFact(3)]`. + pub steps_fwd: Vec, + /// The reverse order. + pub steps_rev: Vec, + /// Basis identity used by the fixture. + pub basis_id: u64, +} + +fn range_mask(lo: u32, hi: u32) -> u64 { + (lo..hi).fold(0u64, |m, i| m | (1u64 << i)) +} + +/// Build the fixture. +pub fn fixture() -> Fixture { + let mut facts = [Tri::False; 64]; + for (i, f) in facts.iter_mut().enumerate() { + *f = if i % 2 == 0 { Tri::False } else { Tri::True }; + } + for f in facts.iter_mut().take(8) { + *f = Tri::True; + } + facts[5] = Tri::False; + for f in &mut facts[10..16] { + *f = Tri::False; + } + facts[12] = Tri::Unknown; + facts[20] = Tri::True; + facts[21] = Tri::True; + facts[22] = Tri::Unknown; + facts[23] = Tri::False; + facts[24] = Tri::False; + for i in [30usize, 31, 40, 50] { + facts[i] = Tri::Unknown; + } + facts[60] = Tri::False; + Fixture { + world: World::new(7, 1, facts), + t1: Thought { + branch: 1, + base_version: 1, + overlay: vec![(5, Tri::True)], + }, + t2: Thought { + branch: 2, + base_version: 1, + overlay: vec![(60, Tri::True)], + }, + m1: Method::AllOf { + id: 101, + lanes: range_mask(0, 8), + }, + m2: Method::AnyOf { + id: 102, + lanes: range_mask(10, 16), + }, + m3: Method::AtLeast { + id: 103, + lanes: range_mask(20, 25), + k: 3, + }, + steps_fwd: vec![Step::SetFact(3, Tri::True), Step::NegateFact(3)], + steps_rev: vec![Step::NegateFact(3), Step::SetFact(3, Tri::True)], + basis_id: 0xB, + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// Version lookup for a world and optional thought; method/policy/steps are version 0. + fn lookup<'a>(w: &'a World, t: Option<&'a Thought>) -> impl Fn(&DepKind, u64) -> Option + 'a { + move |k, id| match k { + DepKind::World => (id == w.id as u64).then_some(w.version), + DepKind::Thought => t.and_then(|t| (id == t.branch as u64).then_some(t.base_version)), + _ => Some(0), + } + } + + fn open(fx: &Fixture, id: u64, t: Option<&Thought>, m: &Method) -> Receipt { + evaluate(id, &fx.world, t, &[], m, Policy::OpenWorld, fx.basis_id).unwrap() + } + + #[test] + fn which_thought_changed_the_result() { + let fx = fixture(); + let base = open(&fx, 1, None, &fx.m1); + let r1 = open(&fx, 2, Some(&fx.t1), &fx.m1); + let r2 = open(&fx, 3, Some(&fx.t2), &fx.m1); + assert_eq!(base.result, Tri::False); + assert_eq!(r1.result, Tri::True); + assert_eq!(r2.result, base.result); + assert_eq!(meta_evaluate(&base, &r1).thought_changed_result, Some(1)); + assert_eq!(meta_evaluate(&base, &r2).thought_changed_result, None); + let d = compare(&base, &r2); + assert!(d.thought_changed); + assert!(!d.result_changed); + assert_ne!(base, r2); + } + + #[test] + fn stale_receipt_after_source_version_change() { + let fx = fixture(); + let r = open(&fx, 1, None, &fx.m1); + let w2 = fx.world.advance(&[(5, Tri::True)]); + assert_eq!(w2.version, fx.world.version + 1); + assert_eq!(w2.id, fx.world.id); + let ord = r.order_witness; + assert_eq!(may_reuse(&r, &lookup(&fx.world, None), ord), Ok(())); + let e = may_reuse(&r, &lookup(&w2, None), ord); + assert!(matches!( + e, + Err(Invalidated::StaleDep { + kind: DepKind::World, + recorded: 1, + current: 2, + .. + }) + )); + // A vanished dependency is stale with current = u64::MAX. + let gone = |_: &DepKind, _: u64| None; + assert!(matches!(may_reuse(&r, &gone, ord), Err(Invalidated::StaleDep { current: u64::MAX, .. }))); + } + + #[test] + fn policy_change_with_unchanged_evidence() { + let fx = fixture(); + let o = evaluate(1, &fx.world, None, &[], &fx.m2, Policy::OpenWorld, fx.basis_id).unwrap(); + let c = evaluate(2, &fx.world, None, &[], &fx.m2, Policy::ClosedWorld, fx.basis_id).unwrap(); + let d = compare(&o, &c); + assert!(d.rule_changed); + assert!(!d.evidence_changed); + assert!(d.result_changed); + assert_eq!(o.result, Tri::Unknown); + assert_eq!(c.result, Tri::False); + let v = meta_evaluate(&o, &c); + assert!(v.only_rule_changed); + assert!(!v.evidence_changed); + // Anti-vacuity: a different method is not "only rule changed". + let other = evaluate(3, &fx.world, None, &[], &fx.m1, Policy::ClosedWorld, fx.basis_id).unwrap(); + assert!(!meta_evaluate(&o, &other).only_rule_changed); + } + + #[test] + fn unknown_is_not_false() { + let fx = fixture(); + let o = evaluate(1, &fx.world, None, &[], &fx.m2, Policy::OpenWorld, fx.basis_id).unwrap(); + let c = evaluate(2, &fx.world, None, &[], &fx.m2, Policy::ClosedWorld, fx.basis_id).unwrap(); + assert_ne!(o.result, Tri::False); + assert_eq!(o.result, Tri::Unknown); + assert_eq!(o.policy, Policy::OpenWorld); + assert_eq!(c.result, Tri::False); + assert_eq!(c.policy, Policy::ClosedWorld); + // The lane set really contains an Unknown. + assert_eq!(fx.world.fact(12), Tri::Unknown); + assert_ne!(o.deps, c.deps); + // AtLeast: True+Unknown reaches k, so Unknown; closed world drops it to False. + let a = open(&fx, 3, None, &fx.m3); + assert_eq!(a.result, Tri::Unknown); + let ac = evaluate(4, &fx.world, None, &[], &fx.m3, Policy::ClosedWorld, fx.basis_id).unwrap(); + assert_eq!(ac.result, Tri::False); + } + + #[test] + fn method_order_changes_effects() { + let fx = fixture(); + let fwd = apply_steps(*view_all(&fx).as_ref(), &fx.steps_fwd); + let rev = apply_steps(*view_all(&fx).as_ref(), &fx.steps_rev); + assert_eq!(fwd[3], Tri::False); + assert_eq!(rev[3], Tri::True); + let (wf, wr) = (order_witness(&fx.steps_fwd), order_witness(&fx.steps_rev)); + assert_ne!(wf, wr); + let r = evaluate(1, &fx.world, None, &fx.steps_fwd, &fx.m1, Policy::OpenWorld, fx.basis_id).unwrap(); + assert_eq!(r.order_witness, wf); + let lk = lookup(&fx.world, None); + assert_eq!(may_reuse(&r, &lk, wf), Ok(())); + assert_eq!( + may_reuse(&r, &lk, wr), + Err(Invalidated::OrderChanged { + recorded: wf, + requested: wr + }) + ); + let rr = evaluate(2, &fx.world, None, &fx.steps_rev, &fx.m1, Policy::OpenWorld, fx.basis_id).unwrap(); + assert!(compare(&r, &rr).order_changed); + } + + fn view_all(fx: &Fixture) -> Box<[Tri; 64]> { + Box::new(view(&fx.world, None).unwrap()) + } + + fn covers(agg: &AggregateReceipt, rs: &[Receipt]) -> bool { + rs.iter() + .all(|r| agg.children.contains(&r.receipt_id) && r.deps.iter().all(|d| agg.deps.contains(d))) + } + + #[test] + fn provenance_survives_aggregation() { + let fx = fixture(); + let rs = vec![open(&fx, 1, Some(&fx.t1), &fx.m1), open(&fx, 2, None, &fx.m2), open(&fx, 3, None, &fx.m3)]; + let agg = aggregate(&rs); + assert_eq!(agg.children, vec![1, 2, 3]); + assert_eq!(agg.result, Tri::Unknown); + assert!(covers(&agg, &rs)); + for r in &rs { + assert!(agg.deps.contains(&Dep { + kind: DepKind::World, + id: 7, + version: 1 + })); + assert!(agg + .deps + .iter() + .any(|d| d.kind == DepKind::Method && d.id == r.method_id as u64)); + } + // Deduplicated: one World dep despite three children. + assert_eq!(agg.deps.iter().filter(|d| d.kind == DepKind::World).count(), 1); + // Negative: dropping m1's Method dep is detected. + let mut cut = agg.clone(); + let before = cut.deps.len(); + cut.deps + .retain(|d| !(d.kind == DepKind::Method && d.id == rs[0].method_id as u64)); + assert!(cut.deps.len() < before); + assert!(!covers(&cut, &rs)); + } + + #[test] + fn unchanged_dependencies_permit_reuse() { + let fx = fixture(); + let r = open(&fx, 1, Some(&fx.t1), &fx.m1); + assert_eq!(may_reuse(&r, &lookup(&fx.world, Some(&fx.t1)), r.order_witness), Ok(())); + // Anti-vacuity: the same lookup without the thought makes the Thought dep vanish. + assert!(may_reuse(&r, &lookup(&fx.world, None), r.order_witness).is_err()); + let a = open(&fx, 2, Some(&fx.t1), &fx.m1); + assert!(which_changed(std::slice::from_ref(&r), &[a]).is_empty()); + } + + #[test] + fn stale_thought_is_refused() { + let fx = fixture(); + let old = Thought { + branch: 9, + base_version: 0, + overlay: vec![], + }; + let e = evaluate(1, &fx.world, Some(&old), &[], &fx.m1, Policy::OpenWorld, fx.basis_id); + assert_eq!(e, Err(Stale::World { expected: 1, found: 0 })); + assert!(evaluate(2, &fx.world, Some(&fx.t1), &[], &fx.m1, Policy::OpenWorld, fx.basis_id).is_ok()); + } + + #[test] + fn meta_fold_reads_receipts_only() { + let (base, alt, inner_diff, inner_verdict) = { + let fx = fixture(); + let base = open(&fx, 1, None, &fx.m1); + let alt = open(&fx, 2, Some(&fx.t1), &fx.m1); + let d = compare(&base, &alt); + let v = meta_evaluate(&base, &alt); + drop(fx); + (base.clone(), alt.clone(), d, v) + }; + let outer_diff = compare(&base, &alt); + let outer_verdict = meta_evaluate(&base, &alt); + assert_eq!(outer_diff, inner_diff); + assert_eq!(outer_verdict, inner_verdict); + assert!(outer_diff.result_changed); + assert_eq!(outer_verdict.thought_changed_result, Some(1)); + let changed = which_changed(&[base], &[alt]); + assert_eq!(changed.len(), 1); + assert_eq!(changed[0].0, 2); + } +} diff --git a/examples/pof_antennas/order_law.rs b/examples/pof_antennas/order_law.rs new file mode 100644 index 00000000..2881a6b6 --- /dev/null +++ b/examples/pof_antennas/order_law.rs @@ -0,0 +1,847 @@ +//! Order antenna (A3) and law antenna (A4) for the permutation-of-fields probe. +//! +//! Three orders get mixed up whenever a lane-wise operation is reordered: +//! +//! - **traversal order**: the sequence in which lanes are visited. A fold over +//! the multiset of lane values (count, sum) does not care. +//! - **coordinate order**: the basis ([`Perm64`]) through which a block is +//! viewed. Invariant folds and equivariant lane-wise ops do not care; +//! positional ops (prefix scan, index-weighted sum) do. +//! - **effect order**: the order in which writes land on one cell. This is a +//! partial order: only non-commuting pairs must keep their relative order. +//! +//! The A3 half models each of the three and refuses illegal reorders +//! ([`check_reorder`]). The A4 half records the algebraic laws of each +//! operation as plain data ([`LAW_TABLE`]) and shows which laws admit which +//! optimization (skip a permutation, fuse two ops, defer a reduction, carry a +//! result in its basis). Nothing here restates [`PermInvariant`] or +//! [`PermEquivariant`]; the law table is a record, the traits stay the gate. +//! +//! Plain safe Rust. All lane movement goes through [`Perm64`]'s own methods. + +#![allow(dead_code)] + +use ndarray::hpc::perm::{ + combine_in_basis, CountNonzero, InBasis, LaneFold, LaneOp, Perm64, PermEquivariant, PermInvariant, SumLanes, LANES, +}; + +// --------------------------------------------------------------------------- +// A3 — order antenna +// --------------------------------------------------------------------------- + +/// One write on a single `i64` cell. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Effect { + /// Replace the cell with the value. + Set(i64), + /// Add the value to the cell. + Add(i64), + /// Multiply the cell by the value. + Mul(i64), +} + +impl Effect { + /// Apply to one cell with checked arithmetic; `None` on overflow. + pub fn apply(&self, cell: i64) -> Option { + match *self { + Effect::Set(v) => Some(v), + Effect::Add(v) => cell.checked_add(v), + Effect::Mul(v) => cell.checked_mul(v), + } + } +} + +/// Run `effs` in order on a cell starting at `init`. +/// +/// Returns `None` if any step overflows `i64`. Arithmetic is checked, never +/// wrapping, so an overflow is reported instead of being folded into a result. +pub fn run_effects(init: i64, effs: &[Effect]) -> Option { + effs.iter().try_fold(init, |cell, e| e.apply(cell)) +} + +/// Whether two effects can be swapped without changing any final value. +/// +/// The rule: `Add`/`Add` commute, `Mul`/`Mul` commute, `Set(x)`/`Set(y)` +/// commute iff `x == y`. Every mixed pair does not commute: `Set`/`Add`, +/// `Set`/`Mul` and `Add`/`Mul` are all order-sensitive. +pub fn commutes(a: &Effect, b: &Effect) -> bool { + match (a, b) { + (Effect::Add(_), Effect::Add(_)) => true, + (Effect::Mul(_), Effect::Mul(_)) => true, + (Effect::Set(x), Effect::Set(y)) => x == y, + _ => false, + } +} + +/// A reorder was refused: effects `first` and `second` (original indices, +/// `first < second`) do not commute but `order` runs `second` before `first`. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct OrderRefusal { + /// Original index of the effect that must stay first. + pub first: usize, + /// Original index of the effect that must stay second. + pub second: usize, +} + +/// Check a proposed execution order against the effect partial order. +/// +/// `order` is a permutation of `0..effs.len()` giving the new execution order +/// (`order[k]` is the original index run `k`-th). It is legal iff every pair +/// `i < j` with `!commutes(effs[i], effs[j])` keeps `i` before `j`. The first +/// violating pair (lowest `i`, then lowest `j`) is reported. +/// +/// # Panics +/// +/// If `order` is not a permutation of `0..effs.len()`. +pub fn check_reorder(effs: &[Effect], order: &[usize]) -> Result<(), OrderRefusal> { + let n = effs.len(); + assert_eq!(order.len(), n, "order must have one entry per effect"); + let mut pos = vec![usize::MAX; n]; + for (k, &orig) in order.iter().enumerate() { + assert!(orig < n, "order entry {orig} is out of range 0..{n}"); + assert_eq!(pos[orig], usize::MAX, "order is not a permutation: {orig} appears twice"); + pos[orig] = k; + } + for i in 0..n { + for j in (i + 1)..n { + if !commutes(&effs[i], &effs[j]) && pos[i] > pos[j] { + return Err(OrderRefusal { first: i, second: j }); + } + } + } + Ok(()) +} + +/// An immutable 64-lane view with a version. Writers return a new snapshot. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Snapshot { + /// Monotone version; a write produces `version + 1`. + pub version: u64, + /// The lane values. + pub lanes: [u8; 64], +} + +/// Reader 1: number of nonzero lanes (via [`CountNonzero`]). +pub fn read_count(s: &Snapshot) -> u32 { + CountNonzero.fold(&s.lanes) +} + +/// Reader 2: sum of lane values (via [`SumLanes`]). +pub fn read_sum(s: &Snapshot) -> u32 { + SumLanes.fold(&s.lanes) +} + +/// Write one lane into a NEW snapshot with `version + 1`; `s` is unchanged. +/// +/// # Panics +/// +/// If `lane >= 64`. +pub fn write_lane(s: &Snapshot, lane: usize, v: u8) -> Snapshot { + assert!(lane < LANES, "lane {lane} out of range"); + let mut lanes = s.lanes; + lanes[lane] = v; + Snapshot { + version: s.version + 1, + lanes, + } +} + +/// Inclusive prefix sum over lanes: `out[i] = x[0] + ... + x[i]`. +/// +/// The sum wraps mod 256 deliberately: the result is itself a lane value. +/// Output lane `i` reads lanes `0..=i`, so this is NOT [`PermEquivariant`]. +#[derive(Clone, Copy, Debug, Default)] +pub struct PrefixSum; + +impl LaneOp<1> for PrefixSum { + fn apply(&self, [x]: [&[u8; LANES]; 1]) -> [u8; LANES] { + let mut out = [0u8; LANES]; + let mut acc = 0u8; + for (o, &v) in out.iter_mut().zip(x.iter()) { + acc = acc.wrapping_add(v); + *o = acc; + } + out + } +} + +/// Positional fold: `sum of i * lane[i]`. Reads the lane index, so it is NOT +/// [`PermInvariant`]. +#[derive(Clone, Copy, Debug, Default)] +pub struct IndexWeightedSum; + +impl LaneFold for IndexWeightedSum { + type Out = u64; + fn fold(&self, b: &[u8; LANES]) -> u64 { + b.iter() + .enumerate() + .map(|(i, &v)| i as u64 * v as u64) + .sum() + } +} + +/// A small program separating the three orders. +#[derive(Clone, Debug)] +pub struct Program { + /// Coordinate basis through which both operand blocks are viewed. + pub coord_basis: Perm64, + /// Effects run on the cell before the computed count is added. + pub effects: Vec, +} + +/// Count lanes where `(a & b) != 0`, visiting positions in `visit` order, +/// after viewing both blocks through `p.coord_basis`; then feed the count as +/// `Add(count)` appended after `p.effects` into [`run_effects`] from 0. +/// +/// Traversal order (`visit`, any permutation of `0..64`) and coordinate basis +/// do not change the count: both operands share the basis, and a count over +/// the multiset of lanes ignores visit order. Effect order is a separate +/// partial order, checked by [`check_reorder`]. +/// +/// # Panics +/// +/// If `visit` is not a permutation of `0..64`. +pub fn run_lanewise_then_effects(p: &Program, a: &[u8; 64], b: &[u8; 64], visit: &[usize; 64]) -> (u32, Option) { + let mut seen = 0u64; + for &i in visit { + assert!(i < LANES, "visit entry {i} out of range"); + assert_eq!(seen >> i & 1, 0, "visit is not a permutation: {i} twice"); + seen |= 1u64 << i; + } + let am = p.coord_basis.materialize(a); + let bm = p.coord_basis.materialize(b); + let mut count = 0u32; + for &i in visit { + if am[i] & bm[i] != 0 { + count += 1; + } + } + let mut effs = p.effects.clone(); + effs.push(Effect::Add(count as i64)); + (count, run_effects(0, &effs)) +} + +/// Combine two blocks, each viewed through its own basis, with a 2-ary +/// equivariant op. Thin wrapper over [`combine_in_basis`]. +pub fn combine_two>(op: &Op, pa: Perm64, a: &[u8; 64], pb: Perm64, b: &[u8; 64]) -> InBasis { + combine_in_basis(op, [(pa, a), (pb, b)]) +} + +// --------------------------------------------------------------------------- +// A4 — law antenna +// --------------------------------------------------------------------------- + +/// How an operation behaves at the edge of its integer range. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Overflow { + /// Cannot overflow for any admitted input. + None, + /// Wraps modulo the lane width, deliberately. + Wraps, + /// Exact, but only within the stated bound. + ExactWithinBound(&'static str), +} + +/// Algebraic metadata of one operation: a DATA record, not a trait. +#[derive(Clone, Copy, Debug)] +pub struct Laws { + /// Row name (unique). + pub name: &'static str, + /// Input/output shape in words. + pub shape: &'static str, + /// Output lane `i` depends only on input lane `i`. + pub lane_local: bool, + /// `(x op y) op z == x op (y op z)` over the combining step. + pub associative: bool, + /// `x op y == y op x` over the combining step. + pub commutative: bool, + /// Result unchanged when the input is permuted (a reduction). + pub perm_invariant: bool, + /// `op(P x) == P op(x)` for every permutation. + pub perm_equivariant: bool, + /// Writes whose order matters (a partial order on effects). + pub ordered_effects: bool, + /// Result is exact (no rounding, no silent loss). + pub exact: bool, + /// Range behaviour. + pub overflow: Overflow, + /// Must read from one immutable snapshot. + pub needs_snapshot: bool, + /// Needs a coordinate frame (mask or basis) carried alongside the data. + pub needs_frame: bool, +} + +/// One row per operation in the probe. Every field is stated; the tests below +/// check the ones that admit an optimization (skip a permutation, fuse ops, +/// defer a reduction, carry a result in its basis, refuse a reorder). +pub const LAW_TABLE: &[Laws] = &[ + Laws { + name: "count(A AND B)", + shape: "64 u8 x 64 u8 -> u32", + lane_local: false, + associative: true, + commutative: true, + perm_invariant: true, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::None, + needs_snapshot: false, + needs_frame: false, + }, + Laws { + name: "sum of lanes", + shape: "64 u8 -> u32", + lane_local: false, + associative: true, + commutative: true, + perm_invariant: true, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::ExactWithinBound("u32: 64 lanes x 255 per block"), + needs_snapshot: false, + needs_frame: false, + }, + Laws { + name: "masked signed U9 dot (B kernel, i32 lanes flushed every 16384 blocks)", + shape: "64 u8 x 64 i8 -> 16 i32 -> i64", + lane_local: false, + associative: true, + commutative: true, + perm_invariant: true, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::ExactWithinBound("i32 lanes: 16384 blocks x 130560 < i32::MAX"), + needs_snapshot: false, + needs_frame: true, + }, + Laws { + name: "E5 anchor masked byte sum (u64 lanes)", + shape: "64 u8 + u64 mask -> u64", + lane_local: false, + associative: true, + commutative: true, + perm_invariant: true, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::ExactWithinBound("u64 lanes: 255 per byte, no wrap below 2^56 bytes"), + needs_snapshot: false, + needs_frame: true, + }, + Laws { + name: "programmable XOR/AND select (ternlog)", + shape: "3 x 64 u8 -> 64 u8", + lane_local: true, + associative: false, + commutative: false, + perm_invariant: false, + perm_equivariant: true, + ordered_effects: false, + exact: true, + overflow: Overflow::None, + needs_snapshot: false, + needs_frame: false, + }, + Laws { + name: "lane-wise XOR", + shape: "2 x 64 u8 -> 64 u8", + lane_local: true, + associative: true, + commutative: true, + perm_invariant: false, + perm_equivariant: true, + ordered_effects: false, + exact: true, + overflow: Overflow::None, + needs_snapshot: false, + needs_frame: false, + }, + Laws { + name: "index-weighted sum", + shape: "64 u8 -> u64", + lane_local: false, + associative: true, + commutative: true, + perm_invariant: false, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::ExactWithinBound("u64: 63 x 255 x 64 per block"), + needs_snapshot: false, + needs_frame: true, + }, + Laws { + name: "prefix sum", + shape: "64 u8 -> 64 u8", + lane_local: false, + associative: false, + commutative: false, + perm_invariant: false, + perm_equivariant: false, + ordered_effects: false, + exact: false, + overflow: Overflow::Wraps, + needs_snapshot: false, + needs_frame: true, + }, + Laws { + name: "Set/Add/Mul effects on one cell", + shape: "i64 cell x effect list -> Option", + lane_local: false, + associative: false, + commutative: false, + perm_invariant: false, + perm_equivariant: false, + ordered_effects: true, + exact: true, + overflow: Overflow::ExactWithinBound("i64: checked ops, None on overflow"), + needs_snapshot: true, + needs_frame: false, + }, + Laws { + name: "predicate mask conjugated by Perm64", + shape: "u64 lane mask x Perm64 -> u64 lane mask", + lane_local: false, + associative: false, + commutative: false, + perm_invariant: false, + perm_equivariant: false, + ordered_effects: false, + exact: true, + overflow: Overflow::None, + needs_snapshot: false, + needs_frame: true, + }, +]; + +/// Reorder a fold: skip the permutation entirely. +/// +/// Relies on the [`PermInvariant`] law, `fold(P·x) == fold(x)`. The generic +/// bound is the admission: a positional fold such as [`IndexWeightedSum`] +/// does not implement the marker and cannot be passed here. +pub fn fold_skipping_perm(f: &F, _p: Perm64, block: &[u8; 64]) -> F::Out { + f.fold(block) +} + +/// Fuse `(a ^ b) & c` into one ternlog immediate. +/// +/// Relies on the lane-local, per-bit nature of XOR and AND: the fused result +/// is a function of the three input bits alone, so it is a truth table. The +/// immediate convention matches [`LaneTernlog`]: output bit = bit +/// `(a << 2) | (b << 1) | c` of the immediate. +pub fn fuse_xor_then_and_imm() -> u8 { + let mut imm = 0u8; + for a in 0..2u8 { + for b in 0..2u8 { + for c in 0..2u8 { + let sel = (a << 2) | (b << 1) | c; + let out = (a ^ b) & c; + imm |= out << sel; + } + } + } + imm +} + +/// Defer a reduction: accumulate in one `i32` (wrapping) and flush to `i64` +/// every `flush_every` items. +/// +/// Relies on associativity and commutativity of addition plus a bound: exact +/// only while `flush_every * max|product| <= i32::MAX`. Past the bound the +/// `i32` wraps silently. +/// +/// # Panics +/// +/// If `flush_every == 0`. +pub fn deferred_i32_total(products: &[i32], flush_every: usize) -> i64 { + assert!(flush_every > 0, "flush_every must be positive"); + let mut total = 0i64; + let mut acc = 0i32; + let mut n = 0usize; + for &p in products { + acc = acc.wrapping_add(p); + n += 1; + if n == flush_every { + total += acc as i64; + acc = 0; + n = 0; + } + } + total + acc as i64 +} + +/// Reference total: every product widened to `i64` first. Always exact. +pub fn exact_i64_total(products: &[i32]) -> i64 { + products.iter().map(|&p| p as i64).sum() +} + +// --------------------------------------------------------------------------- +// Deterministic test data +// --------------------------------------------------------------------------- + +/// SplitMix64: tiny deterministic generator for fixtures. +#[derive(Clone, Debug)] +pub struct SplitMix64(pub u64); + +impl SplitMix64 { + /// Next 64 random bits. + pub fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + + /// A block where about three lanes in four are random bytes, the rest 0. + pub fn block(&mut self) -> [u8; 64] { + core::array::from_fn(|_| { + if !self.next_u64().is_multiple_of(4) { + (self.next_u64() & 0xff) as u8 + } else { + 0 + } + }) + } + + /// A random permutation of `0..64` as `usize` (Fisher-Yates). + pub fn visit_order(&mut self) -> [usize; 64] { + let mut v: [usize; 64] = core::array::from_fn(|i| i); + for i in (1..64).rev() { + let j = (self.next_u64() % (i as u64 + 1)) as usize; + v.swap(i, j); + } + v + } + + /// A random [`Perm64`]. + pub fn perm(&mut self) -> Perm64 { + let v = self.visit_order(); + let idx: [u8; 64] = core::array::from_fn(|i| v[i] as u8); + Perm64::from_indices(idx).expect("shuffled indices form a permutation") + } +} + +#[cfg(test)] +mod tests { + use super::*; + use ndarray::hpc::perm::{LaneAnd, LaneTernlog, LaneXor}; + + fn bitand(a: &[u8; 64], b: &[u8; 64]) -> [u8; 64] { + LaneAnd.apply([a, b]) + } + + // ----- A3 ----- + + #[test] + fn count_and_is_permutation_invariant() { + let mut rng = SplitMix64(1); + let a = rng.block(); + let b = rng.block(); + let base = bitand(&a, &b); + let nz = CountNonzero.fold(&base); + assert!((10..=54).contains(&nz), "fixture must be non-trivial, got {nz} nonzero lanes"); + for _ in 0..8 { + let p = rng.perm(); + let moved = bitand(&p.materialize(&a), &p.materialize(&b)); + assert_eq!(CountNonzero.fold(&moved), nz); + assert_eq!(CountNonzero.fold(&p.materialize(&base)), nz); + } + } + + #[test] + fn xor_is_permutation_equivariant() { + let mut rng = SplitMix64(2); + let a = rng.block(); + let b = rng.block(); + for _ in 0..6 { + let p = rng.perm(); + let got = combine_two(&LaneXor, p, &a, p, &b).materialize(); + assert_eq!(got, p.materialize(&LaneXor.apply([&a, &b]))); + let q = rng.perm(); + let mixed = combine_two(&LaneXor, p, &a, q, &b).materialize(); + let (pa, qb) = (p.materialize(&a), q.materialize(&b)); + let expected: [u8; 64] = core::array::from_fn(|i| pa[i] ^ qb[i]); + assert_eq!(mixed, expected); + } + } + + #[test] + fn index_weighted_sum_is_not_invariant() { + let mut rng = SplitMix64(3); + let x = rng.block(); + let base = IndexWeightedSum.fold(&x); + assert_eq!(IndexWeightedSum.fold(&Perm64::IDENTITY.materialize(&x)), base); + let perms: Vec = (0..8).map(|_| rng.perm()).collect(); + assert!( + perms + .iter() + .any(|p| IndexWeightedSum.fold(&p.materialize(&x)) != base), + "no random permutation changed the positional fold" + ); + } + + #[test] + fn prefix_sum_is_not_equivariant() { + let mut rng = SplitMix64(4); + let x = rng.block(); + let id = Perm64::IDENTITY; + assert_eq!(id.materialize(&PrefixSum.apply([&x])), PrefixSum.apply([&id.materialize(&x)])); + let perms: Vec = (0..8).map(|_| rng.perm()).collect(); + assert!( + perms + .iter() + .any(|p| p.materialize(&PrefixSum.apply([&x])) != PrefixSum.apply([&p.materialize(&x)])), + "no random permutation separated P*prefix(x) from prefix(P*x)" + ); + } + + #[test] + fn set_then_add_differs_from_add_then_set() { + let fwd = [Effect::Set(1), Effect::Add(1)]; + let rev = [Effect::Add(1), Effect::Set(1)]; + assert_eq!(run_effects(0, &fwd), Some(2)); + assert_eq!(run_effects(0, &rev), Some(1)); + assert_eq!(check_reorder(&fwd, &[1, 0]), Err(OrderRefusal { first: 0, second: 1 })); + assert_eq!(check_reorder(&fwd, &[0, 1]), Ok(())); + } + + #[test] + fn adds_commute_and_reorder_is_allowed() { + let effs = [Effect::Add(2), Effect::Add(3), Effect::Add(5)]; + let orders: [[usize; 3]; 6] = [[0, 1, 2], [0, 2, 1], [1, 0, 2], [1, 2, 0], [2, 0, 1], [2, 1, 0]]; + for o in orders { + assert_eq!(check_reorder(&effs, &o), Ok(()), "order {o:?}"); + let reordered: Vec = o.iter().map(|&i| effs[i]).collect(); + assert_eq!(run_effects(0, &reordered), Some(10)); + } + } + + #[test] + fn mixed_sequence_partial_order() { + let effs = [Effect::Add(1), Effect::Set(10), Effect::Add(2), Effect::Add(3)]; + assert_eq!(run_effects(0, &effs), Some(15)); + // Swapping the last two commuting adds is allowed and keeps the result. + assert_eq!(check_reorder(&effs, &[0, 1, 3, 2]), Ok(())); + assert_eq!(run_effects(0, &[effs[0], effs[1], effs[3], effs[2]]), Some(15)); + // Moving Add(1) after Set(10) is refused, and would change the value. + assert_eq!(check_reorder(&effs, &[1, 0, 2, 3]), Err(OrderRefusal { first: 0, second: 1 })); + assert_eq!(run_effects(0, &[effs[1], effs[0], effs[2], effs[3]]), Some(16)); + // Moving Add(2) before Set(10) is refused too. + assert_eq!(check_reorder(&effs, &[0, 2, 1, 3]), Err(OrderRefusal { first: 1, second: 2 })); + } + + #[test] + fn two_readers_share_a_snapshot() { + let s1 = Snapshot { + version: 7, + lanes: core::array::from_fn(|i| if i % 3 == 0 { i as u8 } else { 0 }), + }; + let (c_first, s_first) = (read_count(&s1), read_sum(&s1)); + let (s_second, c_second) = (read_sum(&s1), read_count(&s1)); + assert_eq!((c_first, s_first), (c_second, s_second)); + assert!(c_first > 0 && s_first > 0); + assert_eq!(s1.lanes[4], 0); + let s2 = write_lane(&s1, 4, 200); + assert_eq!(s2.version, 8); + assert_eq!(s1.version, 7); + assert_eq!((read_count(&s1), read_sum(&s1)), (c_first, s_first)); + assert_eq!(read_count(&s2), c_first + 1); + assert_eq!(read_sum(&s2), s_first + 200); + } + + #[test] + fn sequential_dependency_must_see_first_result() { + let fwd = [Effect::Add(3), Effect::Mul(2)]; + let rev = [Effect::Mul(2), Effect::Add(3)]; + assert_eq!(run_effects(1, &fwd), Some(8)); + assert_eq!(run_effects(1, &rev), Some(5)); + assert_eq!(check_reorder(&fwd, &[1, 0]), Err(OrderRefusal { first: 0, second: 1 })); + } + + #[test] + fn traversal_and_basis_do_not_change_the_count() { + let mut rng = SplitMix64(5); + let a = rng.block(); + let b = rng.block(); + let identity_visit: [usize; 64] = core::array::from_fn(|i| i); + let reversed_visit: [usize; 64] = core::array::from_fn(|i| 63 - i); + let random_visit = rng.visit_order(); + let bases = [Perm64::IDENTITY, rng.perm(), rng.perm()]; + let commuting = vec![Effect::Add(2), Effect::Add(3)]; + + let reference = { + let p = Program { + coord_basis: Perm64::IDENTITY, + effects: commuting.clone(), + }; + run_lanewise_then_effects(&p, &a, &b, &identity_visit) + }; + assert!((10..=54).contains(&reference.0), "anti-vacuity: count {}", reference.0); + assert_eq!(reference.1, Some(reference.0 as i64 + 5)); + + for basis in bases { + for visit in [&identity_visit, &reversed_visit, &random_visit] { + let p = Program { + coord_basis: basis, + effects: commuting.clone(), + }; + assert_eq!(run_lanewise_then_effects(&p, &a, &b, visit), reference); + } + } + + // Non-commuting effects: same count, but the effect order is fixed. + let ordered = vec![Effect::Set(1), Effect::Mul(3)]; + let p = Program { + coord_basis: bases[1], + effects: ordered.clone(), + }; + let (count, result) = run_lanewise_then_effects(&p, &a, &b, &random_visit); + assert_eq!(count, reference.0); + assert_eq!(result, Some(3 + count as i64)); + let full = [ordered[0], ordered[1], Effect::Add(count as i64)]; + assert_eq!(check_reorder(&full, &[1, 0, 2]), Err(OrderRefusal { first: 0, second: 1 })); + assert_ne!( + run_effects(0, &[full[1], full[0], full[2]]), + result, + "the refused order would have changed the value" + ); + } + + // ----- A4 ----- + + #[test] + fn reorder_a_fold_positive_and_negative() { + let mut rng = SplitMix64(6); + let x = rng.block(); + let perms: Vec = (0..8).map(|_| rng.perm()).collect(); + for &p in &perms { + assert_eq!(fold_skipping_perm(&CountNonzero, p, &x), CountNonzero.fold(&p.materialize(&x))); + assert_eq!(fold_skipping_perm(&SumLanes, p, &x), SumLanes.fold(&p.materialize(&x))); + } + // Negative: IndexWeightedSum is not PermInvariant, so it cannot be + // passed to fold_skipping_perm; skipping the permutation would be wrong. + assert!(perms + .iter() + .any(|p| IndexWeightedSum.fold(&x) != IndexWeightedSum.fold(&p.materialize(&x)))); + } + + #[test] + fn fuse_two_ops_positive_and_negative() { + let mut rng = SplitMix64(7); + let (a, b, c) = (rng.block(), rng.block(), rng.block()); + let imm = fuse_xor_then_and_imm(); + let fused = LaneTernlog(imm).apply([&a, &b, &c]); + let staged = LaneAnd.apply([&LaneXor.apply([&a, &b]), &c]); + assert_eq!(fused, staged); + assert_ne!(staged, [0u8; 64], "anti-vacuity: composition must be nonzero"); + + // Negative: treating prefix as lane-local identity is not the same op. + let true_comp = LaneAnd.apply([&PrefixSum.apply([&a]), &b]); + let fake_fused = LaneAnd.apply([&a, &b]); + assert_ne!(true_comp, fake_fused); + } + + #[test] + fn defer_reduction_positive_and_negative() { + let product = 4 * 255 * 128i32; + assert_eq!(product, 130_560); + let bound = (i32::MAX / product) as usize; + assert!((16384..16500).contains(&bound), "bound {bound} should sit just above 16384"); + let items = vec![product; 3 * 16384 + 5]; + assert!(items.len() > bound + 1); + let exact = exact_i64_total(&items); + assert_eq!(exact, product as i64 * items.len() as i64); + // Positive: flushing every 16384 items stays inside the i32 range. + assert_eq!(deferred_i32_total(&items, 16384), exact); + // Boundary: exactly the bound still fits. + assert_eq!(deferred_i32_total(&items, bound), exact); + // Negative: one past the bound wraps. + assert_ne!(deferred_i32_total(&items, bound + 1), exact); + } + + #[test] + fn propagate_compact_result_invariant_vs_equivariant() { + let mut rng = SplitMix64(8); + let a = rng.block(); + let b = rng.block(); + let p = rng.perm(); + assert_ne!(p, Perm64::IDENTITY); + + // Invariant result: no basis needed, equal across bases. + let base = CountNonzero.fold(&bitand(&a, &b)); + for q in [Perm64::IDENTITY, p, rng.perm()] { + let moved = bitand(&q.materialize(&a), &q.materialize(&b)); + assert_eq!(CountNonzero.fold(&moved), base); + } + + // Equivariant result: data alone is in the wrong coordinates. + let r = combine_two(&LaneXor, p, &a, p, &b); + assert_ne!(r.data, r.materialize(), "data without its basis is not the answer"); + let (pa, pb) = (p.materialize(&a), p.materialize(&b)); + let expected: [u8; 64] = core::array::from_fn(|i| pa[i] ^ pb[i]); + assert_eq!(r.materialize(), expected); + } + + #[test] + fn refuse_invalid_composition() { + let bad = [Effect::Set(4), Effect::Add(1)]; + assert!(check_reorder(&bad, &[1, 0]).is_err()); + let ok = [Effect::Add(4), Effect::Add(1)]; + assert_eq!(check_reorder(&ok, &[1, 0]), Ok(())); + assert!(commutes(&Effect::Set(2), &Effect::Set(2))); + assert!(!commutes(&Effect::Set(2), &Effect::Set(3))); + assert!(!commutes(&Effect::Add(2), &Effect::Mul(3))); + } + + #[test] + fn effect_overflow_is_reported_not_wrapped() { + assert_eq!(run_effects(i64::MAX, &[Effect::Add(1)]), None); + assert_eq!(run_effects(i64::MAX, &[Effect::Add(1), Effect::Set(0)]), None); + assert_eq!(run_effects(5, &[Effect::Mul(2)]), Some(10)); + } + + #[test] + #[should_panic(expected = "not a permutation")] + fn check_reorder_rejects_a_non_permutation() { + let effs = [Effect::Add(1), Effect::Add(2)]; + let _ = check_reorder(&effs, &[0, 0]); + } + + #[test] + fn law_table_sanity() { + let mut names: Vec<&str> = LAW_TABLE.iter().map(|r| r.name).collect(); + names.sort_unstable(); + let before = names.len(); + names.dedup(); + assert_eq!(names.len(), before, "row names must be unique"); + assert_eq!(before, 10); + + for r in LAW_TABLE { + if r.perm_invariant { + assert!(!r.lane_local, "{}: an invariant row is a fold, not lane-local", r.name); + assert!(!r.perm_equivariant, "{}: invariant and equivariant are exclusive", r.name); + } + if r.ordered_effects { + assert!(!r.commutative, "{}: ordered effects do not commute", r.name); + } + if r.perm_equivariant { + assert!(r.lane_local, "{}: equivariance needs lane locality", r.name); + } + } + for name in ["prefix sum", "index-weighted sum"] { + let r = LAW_TABLE + .iter() + .find(|r| r.name == name) + .expect("row present"); + assert!(!r.perm_invariant && !r.perm_equivariant, "{name}"); + } + // Both ordering-relevant rows are present and flagged. + assert!(LAW_TABLE.iter().any(|r| r.ordered_effects)); + assert!(LAW_TABLE.iter().any(|r| r.perm_invariant)); + assert!(LAW_TABLE.iter().any(|r| r.perm_equivariant)); + } +} diff --git a/examples/pof_antennas/position.rs b/examples/pof_antennas/position.rs new file mode 100644 index 00000000..b796dd5a --- /dev/null +++ b/examples/pof_antennas/position.rs @@ -0,0 +1,451 @@ +//! A1, the position antenna: one 64-position basis, three operations. +//! +//! The 64 logical positions carry four planes: a magnitude byte, a polarity +//! bit (1 = positive), a predicate bit and an operation-selector bit. Three +//! operations read them: +//! +//! 1. predicate evaluation: `count(pred AND positive)`; +//! 2. masked numeric accumulation: `sum(mag | pred, positive) - sum(mag | pred, +//! negative)`, an exact signed `i64`; +//! 3. programmable XOR/AND selection, per position: +//! `sel ? (pred XOR positive) : (pred AND positive)`. +//! +//! Three ways to run them: +//! +//! * P0 prepares every plane separately for every operation; +//! * P1 prepares the planes once ([`Prepared`]) and runs the operations on +//! the shared basis; +//! * P2 re-bases a prepared basis through a [`Perm64`] ([`Prepared::rebase`]). +//! The masks follow their positions through [`Perm64::conjugate_mask`]; the +//! magnitudes are not moved, because operations 1 and 2 are invariant under +//! a consistent permutation and are evaluated in the source basis. Only +//! operation 3's result is owed in the new basis, and it gets there as a +//! conjugated mask, not as a data move. +//! +//! A prepared basis records the frame it was prepared from; running it +//! against another frame is refused ([`StaleBasis`]). + +#![allow(dead_code)] + +use ndarray::hpc::perm::Perm64; +use ndarray::simd::{U64x8, U8x64}; + +/// One block of 64 positions as raw byte planes, the form P0 starts from. +#[derive(Clone, Copy)] +pub struct RawPlanes { + pub frame: u64, + pub mag: [u8; 64], + /// 1 = positive, 0 = negative. + pub polarity: [u8; 64], + /// 1 = predicate holds. + pub pred: [u8; 64], + /// 1 = XOR, 0 = AND for operation 3. + pub sel: [u8; 64], +} + +/// The three results. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Results { + pub count: u32, + pub signed_sum: i64, + pub select: u64, +} + +/// Bit plane of the lanes whose byte is 1. +#[inline(always)] +fn plane(bytes: &[u8; 64]) -> u64 { + U8x64::from_array(*bytes).cmpeq_mask(U8x64::splat(1)) +} + +#[inline(always)] +fn op_count(pred: u64, positive: u64) -> u32 { + (pred & positive).count_ones() +} + +#[inline(always)] +fn op_signed_sum(mag: U8x64, pred: u64, positive: u64) -> i64 { + let zero = U64x8::splat(0); + let pos = zero.sum8_u8_add_masked(mag, pred & positive).reduce_sum(); + let neg = zero.sum8_u8_add_masked(mag, pred & !positive).reduce_sum(); + pos as i64 - neg as i64 +} + +#[inline(always)] +fn op_select(pred: u64, positive: u64, sel: u64) -> u64 { + (sel & (pred ^ positive)) | (!sel & (pred & positive)) +} + +/// P0: every operation prepares the planes it needs on its own. +#[inline(always)] +pub fn p0_separate(r: &RawPlanes) -> Results { + let count = op_count(plane(&r.pred), plane(&r.polarity)); + let signed_sum = op_signed_sum(U8x64::from_array(r.mag), plane(&r.pred), plane(&r.polarity)); + let select = op_select(plane(&r.pred), plane(&r.polarity), plane(&r.sel)); + Results { + count, + signed_sum, + select, + } +} + +/// A basis prepared once: the bit planes, the magnitudes, the frame they came +/// from and the coordinate map they are seen through. +#[derive(Clone, Copy)] +pub struct Prepared { + pub frame: u64, + /// The map from source positions to this view's positions. + pub basis: Perm64, + mag: U8x64, + positive: u64, + pred: u64, + sel: u64, +} + +/// A prepared basis was run against a frame it was not prepared from. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct StaleBasis { + pub prepared: u64, + pub current: u64, +} + +impl Prepared { + /// P1 preparation: each plane once. + #[inline(always)] + pub fn new(r: &RawPlanes) -> Self { + Self { + frame: r.frame, + basis: Perm64::IDENTITY, + mag: U8x64::from_array(r.mag), + positive: plane(&r.polarity), + pred: plane(&r.pred), + sel: plane(&r.sel), + } + } + + /// Run all three operations on this basis. + #[inline(always)] + pub fn run(&self, current_frame: u64) -> Result { + if current_frame != self.frame { + return Err(StaleBasis { + prepared: self.frame, + current: current_frame, + }); + } + Ok(Results { + count: op_count(self.pred, self.positive), + signed_sum: op_signed_sum(self.mag, self.pred, self.positive), + select: op_select(self.pred, self.positive, self.sel), + }) + } + + /// P2: the same basis seen through `p`. See [`Rebased`]. + #[inline(always)] + pub fn rebase(&self, p: Perm64) -> Rebased { + Rebased { + source: *self, + basis: p, + pred: p.conjugate_mask(self.pred), + positive: p.conjugate_mask(self.positive), + sel: p.conjugate_mask(self.sel), + } + } + + pub fn mask_pred(&self) -> u64 { + self.pred + } + pub fn mask_positive(&self) -> u64 { + self.positive + } + pub fn mask_sel(&self) -> u64 { + self.sel + } + + /// P2-lazy: the same answer as `rebase(p).run(frame)` with ONE mask + /// conjugation instead of three. Licensed by equivariance alone: select + /// is lane-local, so `p∘select(pred, pos, sel) == select(p∘pred, p∘pos, + /// p∘sel)`, and count and the signed sum are invariant, so they need no + /// conjugation at all. The rebase is deferred to the one compact result + /// that carries positions. + #[inline(always)] + pub fn run_rebased_lazy(&self, p: Perm64, current_frame: u64) -> Result { + let src = self.run(current_frame)?; + Ok(Results { + select: p.conjugate_mask(src.select), + ..src + }) + } +} + +/// The same map as [`Perm64::conjugate_mask`], with the mask expanded to +/// bytes by one masked select instead of a 64-lane scalar loop. Uses only the +/// public map API (`materialize`) for the byte move. +#[inline(always)] +pub fn conjugate_mask_blended(p: &Perm64, mask: u64) -> u64 { + let flags = U8x64::mask_blend(mask, U8x64::splat(0), U8x64::splat(0x80)); + U8x64::from_array(p.materialize(&flags.to_array())).movemask() +} + +/// A prepared basis re-based through a permutation. The masks are carried to +/// the new positions; the magnitudes stay in the source basis. +#[derive(Clone, Copy)] +pub struct Rebased { + source: Prepared, + pub basis: Perm64, + pred: u64, + positive: u64, + sel: u64, +} + +impl Rebased { + /// Run the three operations. The invariant ones (count, signed sum) are + /// evaluated in whichever basis holds consistent planes; the equivariant + /// one (select) on the conjugated masks, so its result is in the new + /// basis. No data moves. + #[inline(always)] + pub fn run(&self, current_frame: u64) -> Result { + let src = self.source.run(current_frame)?; + Ok(Results { + count: op_count(self.pred, self.positive), + signed_sum: src.signed_sum, + select: op_select(self.pred, self.positive, self.sel), + }) + } + + /// The deliberate mistake the falsifier checks for: summing the source + /// magnitudes under the RE-BASED masks, i.e. mixing two bases. + pub fn mixed_basis_sum(&self) -> i64 { + op_signed_sum(self.source.mag, self.pred, self.positive) + } + + /// The other deliberate mistake: control bits that did not follow their + /// positions (the selector left in the source basis). + pub fn stale_selector_select(&self) -> u64 { + op_select(self.pred, self.positive, self.source.sel) + } +} + +/// Per-position scalar oracle, independent of the planes above. +pub fn oracle(r: &RawPlanes) -> Results { + let mut count = 0u32; + let mut signed_sum = 0i64; + let mut select = 0u64; + for i in 0..64 { + let pred = r.pred[i] == 1; + let pos = r.polarity[i] == 1; + if pred && pos { + count += 1; + } + if pred { + let m = r.mag[i] as i64; + signed_sum += if pos { m } else { -m }; + } + let bit = if r.sel[i] == 1 { pred ^ pos } else { pred && pos }; + select |= (bit as u64) << i; + } + Results { + count, + signed_sum, + select, + } +} + +/// Deterministic fixture: 64 distinct positions (each magnitude is unique), +/// mixed planes. +pub fn fixture(frame: u64, seed: u64) -> RawPlanes { + let mut s = seed; + let mut next = move || { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + s + }; + let mut mag = [0u8; 64]; + for (i, m) in mag.iter_mut().enumerate() { + // Distinct per position, so a position mix-up changes the sum. + *m = (i as u8).wrapping_mul(3).wrapping_add(17) | 1; + } + let bits = |x: u64| -> [u8; 64] { core::array::from_fn(|i| (x >> i & 1) as u8) }; + RawPlanes { + frame, + mag, + polarity: bits(next()), + pred: bits(next()), + sel: bits(next()), + } +} + +/// The same block with every plane permuted by `p` (the reference for P2). +pub fn permute_raw(r: &RawPlanes, p: Perm64) -> RawPlanes { + RawPlanes { + frame: r.frame, + mag: p.materialize(&r.mag), + polarity: p.materialize(&r.polarity), + pred: p.materialize(&r.pred), + sel: p.materialize(&r.sel), + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn perm(seed: u64) -> Perm64 { + let mut idx: [u8; 64] = core::array::from_fn(|i| i as u8); + let mut s = seed | 1; + for i in (1..64).rev() { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + idx.swap(i, (s % (i as u64 + 1)) as usize); + } + Perm64::from_indices(idx).unwrap() + } + + #[test] + fn p0_p1_and_the_oracle_agree() { + for seed in 1..50u64 { + let r = fixture(3, seed * 0x9E37_79B9); + let want = oracle(&r); + // Anti-vacuity: every operation sees a non-trivial selection. + assert!(want.count > 3 && want.count < 40, "seed {seed}: {want:?}"); + assert_eq!(p0_separate(&r), want); + assert_eq!(Prepared::new(&r).run(3), Ok(want)); + } + } + + /// Re-basing keeps the meaning: invariant results unchanged, the + /// equivariant result carried to the new positions, equal to running the + /// oracle on the physically permuted block. + #[test] + fn rebase_preserves_meaning() { + let r = fixture(3, 0xDEAD_BEEF); + let base = Prepared::new(&r).run(3).unwrap(); + let mut moved_any = false; + for k in 1..12 { + let p = perm(k); + let got = Prepared::new(&r).rebase(p).run(3).unwrap(); + let truth = oracle(&permute_raw(&r, p)); + assert_eq!(got, truth, "perm {k}"); + assert_eq!((got.count, got.signed_sum), (base.count, base.signed_sum)); + assert_eq!(got.select, p.conjugate_mask(base.select)); + moved_any |= got.select != base.select; + } + assert!(moved_any, "no permutation moved the select result: vacuous"); + } + + /// Falsifier: mixing bases (re-based masks over source magnitudes) is + /// detected; position i of one basis is not position i of another. + #[test] + fn mixing_bases_changes_the_result() { + let r = fixture(3, 0x1234_5678); + let truth = oracle(&r).signed_sum; + let wrong = (1..12) + .map(|k| Prepared::new(&r).rebase(perm(k)).mixed_basis_sum()) + .filter(|&s| s != truth) + .count(); + assert!(wrong >= 10, "only {wrong} of 11 permutations exposed the mix-up"); + } + + /// Falsifier: control bits that do not follow their positions give a + /// different select result. + #[test] + fn selector_must_follow_its_positions() { + let r = fixture(3, 0xABCD_0001); + let wrong = (1..12) + .filter(|&k| { + let rb = Prepared::new(&r).rebase(perm(k)); + rb.stale_selector_select() != rb.run(3).unwrap().select + }) + .count(); + assert!(wrong >= 10, "only {wrong} of 11 permutations exposed a stale selector"); + } + + /// Falsifier: a basis prepared from one frame is refused on another. + #[test] + fn a_stale_basis_is_refused() { + let r = fixture(3, 7); + let prep = Prepared::new(&r); + assert_eq!( + prep.run(4), + Err(StaleBasis { + prepared: 3, + current: 4 + }) + ); + assert_eq!( + prep.rebase(perm(5)).run(4).map(|_| ()), + Err(StaleBasis { + prepared: 3, + current: 4 + }) + ); + assert!(prep.run(3).is_ok()); + } + + /// Two domains in different bases: combining them needs the relative + /// map, not the raw slot numbers. + #[test] + fn two_domains_meet_through_the_relative_map() { + let r = fixture(3, 99); + let (p, q) = (perm(21), perm(22)); + // Domain X: predicate seen through p. Domain Y: polarity seen through q. + let x = p.conjugate_mask(plane(&r.pred)); + let y = q.conjugate_mask(plane(&r.polarity)); + // Correct: carry y into p's basis with q.relative_to(p)... expressed + // on masks: back to source with q's inverse, then into p. + let y_in_p = p.conjugate_mask(q.inverse().conjugate_mask(y)); + let truth = p.conjugate_mask(plane(&r.pred) & plane(&r.polarity)); + assert_eq!(x & y_in_p, truth); + // Naive: slot i of y treated as slot i of x. + assert_ne!(x & y, truth); + } + + /// The lazy rebase (one conjugation of the result) equals the eager one + /// (three conjugations of the inputs) for every map tried; and the + /// blended expansion equals `conjugate_mask` bit for bit. + #[test] + fn lazy_rebase_and_blended_conjugation_agree() { + let mut s = 0x9E37_79B9_7F4A_7C15u64; + for k in 1..40 { + let r = fixture(5, k); + let prep = Prepared::new(&r); + let p = perm(k + 100); + assert_eq!(prep.run_rebased_lazy(p, 5).unwrap(), prep.rebase(p).run(5).unwrap()); + assert_eq!( + prep.run_rebased_lazy(p, 6), + Err(StaleBasis { + prepared: 5, + current: 6 + }) + ); + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + for m in [s, !s, 0, u64::MAX, 1 << (k % 64)] { + assert_eq!(conjugate_mask_blended(&p, m), p.conjugate_mask(m)); + } + } + } + + /// Negative: lazy rebase is only licensed for the EQUIVARIANT result. + /// Applying it to an order-dependent result (a prefix count of the + /// selected positions) gives a wrong answer. + #[test] + fn lazy_rebase_is_refused_for_a_positional_result() { + let r = fixture(5, 7); + let prep = Prepared::new(&r); + let src_sel = prep.run(5).unwrap().select; + // Positional result: mask of positions whose prefix popcount is odd. + let prefix_odd = |m: u64| { + (0..64).fold(0u64, |acc, i| acc | (u64::from((m & (u64::MAX >> (63 - i))).count_ones() % 2 == 1) << i)) + }; + let mut differs = false; + for k in 1..12 { + let p = perm(k); + let truth = prefix_odd(prep.rebase(p).run(5).unwrap().select); + let lazy = p.conjugate_mask(prefix_odd(src_sel)); + differs |= truth != lazy; + } + assert!(differs, "a positional result must not commute with the rebase"); + } +} diff --git a/examples/pof_antennas/scale.rs b/examples/pof_antennas/scale.rs new file mode 100644 index 00000000..0e324e63 --- /dev/null +++ b/examples/pof_antennas/scale.rs @@ -0,0 +1,167 @@ +//! A6, one bounded scaling antenna: a 64×64 logical field. +//! +//! The field is the 4096 cells of a [`PermTable12`]; cell `code` is the map +//! `table.for_code(code)`. One question over the whole field: +//! +//! `Σ_cells #{ i : A[i] && B[cell[i]] }` +//! +//! where `A` is a predicate in output coordinates and `B` a predicate that +//! moves with each cell. Four executions, one answer: +//! +//! * per cell, materialized: compose the cell, move `B`'s bytes, count; +//! * per cell, conjugated: compose the cell, carry `B`'s mask through it +//! (`conjugate_mask`), AND, popcount; no data written; +//! * whole field through the existing exposure ([`PermTable12::exposure`]): +//! one 64×64 kernel, one weighted count, no per-cell work; +//! * the two per-cell forms again in Morton order of the 64×64 grid. +//! +//! No dense 64³ (or larger) structure is allocated: the largest object is the +//! 64×64 `u16` exposure (8 KiB). + +#![allow(dead_code)] + +use ndarray::hpc::perm::{Perm64, PermTable12}; + +/// Bytes written by each execution, so traffic is reported, not guessed. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] +pub struct Traffic { + pub compositions: u64, + pub bytes_written: u64, +} + +/// A table with twelve distinct, non-trivial base steps. +pub fn table(seed: u64) -> PermTable12 { + let mut s = seed | 1; + let mut next = move || { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + s + }; + PermTable12::new(core::array::from_fn(|_| { + let mut idx: [u8; 64] = core::array::from_fn(|i| i as u8); + for i in (1..64).rev() { + idx.swap(i, (next() % (i as u64 + 1)) as usize); + } + Perm64::from_indices(idx).unwrap() + })) +} + +/// The cell order of the 64×64 grid. Row-major is `code = y * 64 + x`; +/// Morton interleaves the bits of `x` and `y`. +pub fn row_major() -> Vec { + (0..4096u16).collect() +} + +pub fn morton() -> Vec { + (0..4096u32) + .map(|m| { + let (mut x, mut y) = (0u32, 0u32); + for b in 0..6 { + x |= (m >> (2 * b) & 1) << b; + y |= (m >> (2 * b + 1) & 1) << b; + } + (y * 64 + x) as u16 + }) + .collect() +} + +pub fn per_cell_materialized(t: &PermTable12, a: &[u8; 64], b: &[u8; 64], order: &[u16]) -> (u64, Traffic) { + let mut tr = Traffic::default(); + let mut total = 0u64; + for &code in order { + let p = t.for_code(code); + tr.compositions += 1; + let moved = p.materialize(b); + tr.bytes_written += 64; + total += a + .iter() + .zip(&moved) + .filter(|(x, y)| **x != 0 && **y != 0) + .count() as u64; + } + (total, tr) +} + +pub fn per_cell_conjugated(t: &PermTable12, a: u64, b: u64, order: &[u16]) -> (u64, Traffic) { + let mut tr = Traffic::default(); + let mut total = 0u64; + for &code in order { + let p = t.for_code(code); + tr.compositions += 1; + total += (a & p.conjugate_mask(b)).count_ones() as u64; + } + (total, tr) +} + +pub fn whole_field_exposure(t: &PermTable12, a: u64, b: u64) -> (u64, Traffic) { + let e = t.exposure(); + let total = e.count_where(|i, j| a >> i & 1 == 1 && b >> j & 1 == 1); + // One 64x64 u16 kernel is written once. + ( + total, + Traffic { + compositions: 0, + bytes_written: 64 * 64 * 2, + }, + ) +} + +/// Scalar oracle from the index vectors alone. +pub fn oracle(t: &PermTable12, a: u64, b: u64) -> u64 { + let mut total = 0u64; + for code in 0..4096u16 { + let idx = t.for_code(code).indices(); + for (i, &j) in idx.iter().enumerate() { + if a >> i & 1 == 1 && b >> j & 1 == 1 { + total += 1; + } + } + } + total +} + +pub fn bytes_of(mask: u64) -> [u8; 64] { + core::array::from_fn(|i| (mask >> i & 1) as u8) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn every_execution_agrees_with_the_oracle() { + let t = table(0x51_7CC1_B727_220A); + for (a, b) in [ + (0xF0F0_1234_8000_0001u64, 0x0FF0_F00F_5555_AAAAu64), + (u64::MAX, 0x8000_0000_0000_0001), + (0x0123_4567_89AB_CDEF, 0xFEDC_BA98_7654_3210), + ] { + let want = oracle(&t, a, b); + // Anti-vacuity: the answer depends on the field, not just popcounts. + assert!(want > 0 && want < 4096 * 64); + assert_eq!(per_cell_materialized(&t, &bytes_of(a), &bytes_of(b), &row_major()).0, want); + assert_eq!(per_cell_conjugated(&t, a, b, &row_major()).0, want); + assert_eq!(per_cell_conjugated(&t, a, b, &morton()).0, want); + assert_eq!(whole_field_exposure(&t, a, b).0, want); + } + } + + #[test] + fn morton_visits_every_cell_once() { + let mut m = morton(); + assert_ne!(m, row_major(), "Morton order is a different traversal"); + m.sort_unstable(); + assert_eq!(m, row_major()); + } + + /// The field answer is not a function of the popcounts alone: two `b` + /// with equal popcount give different totals, so the fixture exercises + /// the per-cell routing. + #[test] + fn the_answer_depends_on_positions() { + let t = table(9); + let a = 0x0000_0000_FFFF_FFFFu64; + assert_ne!(oracle(&t, a, 0x0000_0000_0000_FFFF), oracle(&t, a, 0xFFFF_0000_0000_0000)); + } +} diff --git a/tests/pof_antennas.rs b/tests/pof_antennas.rs new file mode 100644 index 00000000..fd6c915d --- /dev/null +++ b/tests/pof_antennas.rs @@ -0,0 +1,145 @@ +#![cfg(feature = "std")] +//! D-POF-ANT-0 antennas: exactness and falsifiers. The A1, A3/A4, A5 and A6 +//! modules carry their own tests; A2 (the arithmetic exposure) is checked here +//! against #388's `i64` oracle and the unchanged B and E5 kernels. + +#[path = "../examples/u9_head_to_head/kernels.rs"] +mod kernels; +#[path = "../examples/u9_abacus/anchor.rs"] +mod anchor; +#[path = "../examples/pof_antennas/exposure.rs"] +mod exposure; +#[path = "../examples/pof_antennas/meta.rs"] +mod meta; +#[path = "../examples/pof_antennas/order_law.rs"] +mod order_law; +#[path = "../examples/pof_antennas/position.rs"] +mod position; +#[path = "../examples/pof_antennas/scale.rs"] +mod scale; + +use anchor::{split_anchor, AccE5, QueryE}; +use exposure::{pos_mag_oracle, AccDual, AccE2, AccPosMag}; +use kernels::{check, oracle, prepare_b, AccB, Block, B_FLUSH_BLOCKS}; +use ndarray::simd::{U64x8, U8x64}; + +type Raw = ([u8; 64], u64); + +fn block(r: &Raw) -> Block { + Block { + mag: U8x64::from_array(r.0), + positive: r.1, + } +} + +fn encode(v: i32) -> (u8, bool) { + (v.unsigned_abs() as u8, v >= 0) +} + +/// E2 end to end and as a scan, E3's two consumers fused and separate, and +/// B and E5 on the same data. +fn run_a2(a: &[Raw], b: &[Raw]) -> ([i64; 4], (i64, u64), (i64, u64)) { + let (mut e2, mut s2, mut bk, mut e5) = (AccE2::new(), AccE2::new(), AccB::new(), AccE5::new()); + let mut dual = AccDual::new(); + let (mut sep_b, mut sep_m) = (AccB::new(), AccPosMag::new()); + for (ra, rb) in a.iter().zip(b) { + let (x, y) = (block(ra), block(rb)); + check(x, y).unwrap(); + let (low7, top) = split_anchor(y.mag); + e2.mac(x.mag, x.positive ^ y.positive, low7, top); + s2.scan_step(x, &QueryE::new(y)); + bk.step(x, y); + e5.step(x, y); + let (neg, l, t) = prepare_b(x, y); + dual.mac(x.mag, neg, l, t); + sep_b.mac(x.mag, neg, l, t); + sep_m.mac(x.mag, neg); + } + ( + [e2.finish(), s2.finish(), bk.finish(), e5.finish()], + dual.finish(), + (sep_b.finish(), sep_m.finish()), + ) +} + +fn check_a2(a: &[Raw], b: &[Raw]) { + let want = oracle(a, b).unwrap(); + let want_m = pos_mag_oracle(a, b); + let (four, dual, sep) = run_a2(a, b); + assert_eq!(four, [want; 4]); + assert_eq!(dual, (want, want_m)); + assert_eq!(sep, (want, want_m)); +} + +#[test] +fn a2_all_511_by_511_pairs_are_exact() { + let mut n = 0usize; + for va in -255..=255i32 { + for vb in -255..=255i32 { + let lane = n % 64; + let (ma, pa) = encode(va); + let (mb, pb) = encode(vb); + let (mut am, mut bm) = ([0u8; 64], [0u8; 64]); + am[lane] = ma; + bm[lane] = mb; + let ap = if pa { u64::MAX } else { !(1u64 << lane) }; + let bp = if pb { u64::MAX } else { !(1u64 << lane) }; + assert_eq!(run_a2(&[(am, ap)], &[(bm, bp)]).0, [i64::from(va) * i64::from(vb); 4], "{va} x {vb}"); + n += 1; + } + } + assert_eq!(n, 511 * 511); +} + +#[test] +fn a2_mixed_blocks_and_worst_case_runs_are_exact() { + let mut s = 0x00DD_BA11_u64; + let mut val = move || { + s = s + .wrapping_mul(6_364_136_223_846_793_005) + .wrapping_add(1_442_695_040_888_963_407); + ((s >> 33) % 511) as i32 - 255 + }; + for blocks in [1usize, 3, 64, 300] { + let mut mk = || { + let mut m = [0u8; 64]; + let mut p = 0u64; + for (i, slot) in m.iter_mut().enumerate() { + let (mi, pi) = encode(val()); + *slot = mi; + p |= u64::from(pi) << i; + } + (m, p) + }; + let a: Vec<_> = (0..blocks).map(|_| mk()).collect(); + let b: Vec<_> = (0..blocks).map(|_| mk()).collect(); + check_a2(&a, &b); + } + let n = 2 * B_FLUSH_BLOCKS + 3; + for (pa, pb) in [(u64::MAX, u64::MAX), (u64::MAX, 0), (0xF0F0_F0F0_0F0F_0F0F, 0x3333_CCCC_5555_AAAA)] { + check_a2(&vec![([255u8; 64], pa); n], &vec![([255u8; 64], pb); n]); + } +} + +/// The reuse law E2 relies on, byte by byte: narrowing a zero-masked vector +/// by a second mask equals masking once by the AND of both masks, and the +/// narrower mask is not the same mask (sign alone keeps more bytes). +#[test] +fn a2_narrowing_law_holds_and_is_not_identity() { + let a = U8x64::from_array(core::array::from_fn(|i| (i as u8).wrapping_mul(37) | 0x81)); + let mut seen_difference = false; + for (s, t) in [ + (0xF0F0_1234_8000_0001u64, 0x0FF0_F00F_5555_AAAAu64), + (u64::MAX, 0x8000_0000_0000_0001), + (0, u64::MAX), + ] { + let zero = U8x64::splat(0); + let a_s = U8x64::mask_blend(s, zero, a); + let narrowed = U64x8::splat(0).sum8_u8_add_masked(a_s, t); + let direct = U64x8::splat(0).sum8_u8_add_masked(a, s & t); + assert_eq!(narrowed.to_array(), direct.to_array()); + let sign_only = U64x8::splat(0).sum8_u8_add_masked(a, s); + seen_difference |= sign_only.to_array() != direct.to_array(); + } + assert!(seen_difference, "sign and sign AND bit7 never differed: vacuous"); +} From 12b1b0e8ca14d69d7d80e5aca9b81f18bc1d30e7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 23:29:54 +0000 Subject: [PATCH 2/4] D-POF-ANT-0: lazy rebase, blended conjugation probe, report Adds P2-lazy (one conjugation of the equivariant result instead of three of its inputs) and a blended mask expansion row to A1, with an exactness test and a negative test for a positional result. Report records the A0 census, per-tier timings and loop bodies, 14 red disable runs, the discovery matrix and the POSITION/ORDER/LAW/EXPOSURE/WITNESS mapping onto existing types. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMMjKnig6MXTd41Lf2v --- .claude/blackboard.md | 20 ++ .claude/knowledge/pof-antennas-probe.md | 409 ++++++++++++++++++++++++ 2 files changed, 429 insertions(+) create mode 100644 .claude/knowledge/pof-antennas-probe.md diff --git a/.claude/blackboard.md b/.claude/blackboard.md index 126356ad..3947e959 100644 --- a/.claude/blackboard.md +++ b/.claude/blackboard.md @@ -3985,3 +3985,23 @@ realizations; wasm/neon parity pass; 6 disable runs red. Verdict: ADOPT-LAB on A sign's zero-masked copy, E5 pays maskz+vpsadbw+vpaddq per sign; 0 spills) and AVX2 (mask built in registers per call, 8 vpshufb + 16 vpmuludq per block). Overall DEFER as B replacement. Closes fruit U1 (blackboard U9 fruit list, #392). + +## D-POF-ANT-0: Position x Order x Law antennas (2026-10-29, branch claude/pof-antennas) + +Lab only: `examples/pof_antennas/*`, `tests/pof_antennas.rs` (41 tests, 7 realizations green, 14 disable runs red), report +`.claude/knowledge/pof-antennas-probe.md`. No facade/backend/storage/trait change; #393 untouched. Findings: sharing a +prepared basis wins without sharing a mask (P1 0.79-0.93x on AVX-512); invariant folds need no carry under a rebase and +an equivariant result needs ONE `conjugate_mask` of the result (P2-lazy 6.3 vs 16.4 ns VNNI); `conjugate_mask` itself costs +4.4 ns because its mask->bytes expansion is a scalar `from_fn` (a `mask_blend` expansion is 5.6x faster on AVX-512, 2.5x +slower on AVX2). E2 (sign-routed operand once, anchor narrows it; lowering drops E5's kandq/kandnq, keeps 4 zero-masked +moves) beats E5 on every AVX-512 row and B on v4 (L1 e2e 4.69 vs 5.11 vs 5.63), still 1.10x B on VNNI, 7x worse on AVX2 +(per-lane mask_blend). E3 two fused consumers 0.6-0.94x on every tier. A6: Exposure field fold tier-independent +(6.1-8.0 us/field), Morton = row-major at 8 KiB. LAW already lives in mask-risc (ternlog commutativity, per-terminal merge +laws, ExtentUnsupported, row bounds) and WITNESS in OrderedLaneWitness; no new trait. + +| # | fruit | size | gate | +|---|---|---|---| +| P1 | `Perm64::conjugate_mask` mask expansion via one masked select on AVX-512, current path on AVX2 | low | perm.rs owner PR; parity on all realizations | +| P2 | E2 as the AVX-512-without-VNNI U9 kernel (joins #393's ADOPT-LAB row) | low | integration owner | +| P3 | AVX2 P1 anomaly: setup+exec 8 ns apart, 42 ns together | low | asm of the combined path | +| P4 | RPR stale cases X1-X9 / #1848 B0 fixture can reuse the A5 scalar oracle | high | lance-graph owners | diff --git a/.claude/knowledge/pof-antennas-probe.md b/.claude/knowledge/pof-antennas-probe.md new file mode 100644 index 00000000..5d314ac2 --- /dev/null +++ b/.claude/knowledge/pof-antennas-probe.md @@ -0,0 +1,409 @@ +# D-POF-ANT-0: Position × Order × Law, the first antennas + +READ BY: savant-architect, simd-savant, vector-synthesis, the Perm64 owner, the +DR/DT owners (lance-graph #1835), the Thought-Git owner (#1848). + +Scope: lab code and docs only. +- Code: `examples/pof_antennas/{position,exposure,order_law,meta,scale,main}.rs` + and `tests/pof_antennas.rs`. +- No facade word, backend, dispatch, storage owner, cache, registry, mask + minting, Thought-Git runtime or public trait was added. +- #393 (E5) is untouched and its verdict stands: E2 below is a new row, not a + revision. +- lance-graph was read at `origin/main` 61720fa (#1848 merged) and not + modified. + +Method: +- The tests are exact oracles plus falsifiers: 41 tests, 14 disable runs, all + red. +- Timings are medians of 2001 runs (L1) or 5–9 runs (streamed). Each tier was + run 3 times; the tables give min–max of the medians. +- Tiers: native = AVX-512 + VNNI; v4 = `config-v4.toml`, AVX-512 without VNNI; + v3 = `config-v3.toml`, AVX2. Every binary prints its tier on the first line. +- Loop bodies come from `#[inline(never)]` copies, disassembled with objdump. + +## The answer in one paragraph + +Sharing a coordinate basis is useful without sharing a mask, but only under +two conditions: + +1. **Invariant results** (counts, sums, the exact U9 dot) need **no** move + under a rebase. +2. **Equivariant results** (lane-local selects) need **one** carry of the + **result**, not one per input. + +Under both, a rebase costs at most one `conjugate_mask`. A rebase is "free" +only if conjugation is cheap. Today it is not: `conjugate_mask` expands the +mask to bytes with a 64-lane scalar loop, which costs about 4.4 ns on +AVX-512. That is more than all three operations together. + +The laws that license reuse are already in the stack: +- ndarray: the markers `PermInvariant` and `PermEquivariant`; +- lance-graph mask-risc: commutativity read from the ternlog table, a merge + law per terminal, `ExtentUnsupported` refusals, and stated row bounds; +- the witnesses `OrderedLaneWitness` and `SealedFacetLane::validate`. + +None of them needs a new trait. The smallest evidence-carrying fold result +has six fields: result, the law it was folded under, basis/frame, order +witness, the dependency versions, and UNKNOWN kept as its own value. + +## A0: census of what already exists + +Classification: IMPLEMENTED (code exists), MEASURED (timed by this probe or a +cited PR), PROPOSED (plan/decision only), MISSING. + +| primitive | file | owner | in → out | position | order | law | frame/version | oracle/tests | cost measured | status | missing | +|---|---|---|---|---|---|---|---|---|---|---|---| +| `Perm64::{then, inverse, relative_to}` | `src/hpc/perm.rs` | ndarray (#336) | map × map → map | a coordinate map | composition order (`then` left to right) | group law | **none**: a map carries no basis id or frame | perm.rs, 24 tests | — | IMPLEMENTED | basis identity; A1 adds the frame outside the map | +| `Perm64::materialize` | perm.rs:283 | ndarray | 64 B → 64 B | the only data move | n/a | equivariant | none | perm.rs | 9.6 ns for 4 planes (VNNI), 57 ns (AVX2) | MEASURED | — | +| `Perm64::conjugate_mask` | perm.rs:265 | ndarray | `u64` → `u64` | carries a mask through the map without moving data | n/a | equivariant | none | perm.rs; A1, A6 | **4.4 ns each** (VNNI/v4), **~60 ns** (AVX2) | MEASURED | the mask→bytes expansion is a scalar `from_fn` | +| `LaneFold` + `PermInvariant` | perm.rs:766 | ndarray | 64 lanes → `Out` | ignored | any | **marker only**, unchecked | none | perm.rs; A4 negative `IndexWeightedSum` | — | IMPLEMENTED | a wrong `impl` is not detected; A3/A4 tests are the guard | +| `LaneOp` + `PermEquivariant` | perm.rs:781 | ndarray | N × 64 → 64 | preserved | any | marker only | none | perm.rs; A4 negative `PrefixSum` | — | IMPLEMENTED | same | +| `InBasis`, `combine_in_basis` | perm.rs:876, 910 | ndarray | two bases → one | relative map | n/a | requires equivariant | basis = the map value | perm.rs; A3 | — | IMPLEMENTED | — | +| `PermTable12`, `Exposure`, `count_where` | perm.rs:338, 957, 1011 | ndarray | 4096 cells → a 64×64 `u16` kernel | the whole field at once | none | invariant counts only | none | perm.rs; A6 | **7.5 µs per field**, 1 allocation (8 KiB) | MEASURED | — | +| `PermChain`, `PermField`, `PermBatch`, `Schedule` | perm.rs | ndarray | — | — | — | — | none | perm.rs | — | IMPLEMENTED, not used here | — | +| mask-RISC masking ops (`eq/lt_*_to_mask`, masked reductions, `ternlog`, `mask_shift_morton`) | `src/simd_masking_ops.rs` | ndarray (#306) | lanes → mask, mask → fold | strided read in place | traversal order free | per-op doc | none | 181 tests | per #306 | IMPLEMENTED | — | +| `U64x8::sum8_u8_add_masked` | `src/simd_avx512.rs:2186` | ndarray (#390) | `U8x64` + keep → 8 × `u64` | vertical | free | exact, 255·8 per lane per call | none | #390, #393 | #393 | MEASURED | — | +| `I32x16::dot4_u8_i8_add(_masked)` | simd_avx512.rs | ndarray | `U8x64` × `I8x64` → 16 × `i32` | vertical | free | exact within the flush bound | none | #388 | #388 | MEASURED | — | +| `U8x64::mask_blend` | simd_avx512.rs, simd_avx2.rs | ndarray | mask × 2 → 1 | lane-local | — | equivariant | — | — | **one `vpblendmb`/`vmovdqu8{z}` on AVX-512; a per-lane loop on AVX2** (A2 E2: 73 vs 10 ns) | MEASURED | AVX2 realization (already on the facet-stride R2 list) | +| `U64x8::ternlog::` | simd_avx512.rs:5851 | ndarray | 3 → 1 | lane-local | — | the immediate is the truth table | — | — | LLVM already fuses `(a^b)&c` to one `vpternlogq` | MEASURED (A4) | — | +| U9 kernels B, E3–E5 | `examples/u9_*` | lab (#388–#393) | 2 × U9 block → `i64` | vertical | free | exact, flushed | none | #388, #389, #393 | #393 | MEASURED | — | +| W1a consumer contract | `.claude/knowledge/vertical-simd-consumer-contract.md` | ndarray | — | — | — | defines saturation/overflow docs | — | — | — | IMPLEMENTED (doc) | — | +| `OrderedLaneWitness`, `SealedFacetLane::{seal, validate, verify}` | lance-graph `lance-graph-contract/src/ordered_lane.rs:51, 193, 264, 294` | lance-graph | keys × version → witness | numeric projection order | **sealed sort order** | O(1) validation, O(n) re-attestation | `LanceVersion`, n_rows, digest, lens | ordered_lane tests | — | IMPLEMENTED | — | +| mask-risc `Program`, `Terminal`, `GroupFold::merge`, `ExtentUnsupported`, `MASKED_SUM_I32_MAX_ROWS`, ternlog commutativity | lance-graph `lance-graph-mask-risc/src/{ir,exec,value}.rs` | lance-graph | planes → terminal | borrowed planes | straight-line ops, one terminal | **merge law per terminal; commutativity read from the table (`exec.rs:427`); partial-extent refusal; stated row bounds** | none | mask-risc tests (e.g. `exec.rs:2460`) | per mask-risc PRs | IMPLEMENTED | — | +| thought-git-probe `BaseRef`, `VersionStore::{seal, commit_cycle}` | lance-graph `thought-git-probe/src/receipt.rs:56, 128, 153` | lab | thoughts × base → commit witness | — | cycle | — | `BaseRef{dataset, branch, version}` | probe tests | — | IMPLEMENTED (lab) | `DurableRef`, `ThoughtCommitId` are PROPOSED (D-CPG); not in crates | +| DR = HHTL16 addressing, DT = `ClassId → schema + methods`, DR #4 method routing | lance-graph `.claude/plans/d-drdt-dr-dt-ownership-amendment-v1.md` (#1835) | lance-graph | — | DR owns coordinate maps | DT owns ordered effects and method identity | — | `FrameStore` (lab) | — | `LocalMap` 1,050 ns cold, 7.7 ns per lookup | PROPOSED (decisions) | bit-matrix column read (#1835 §3) | +| witness-gated reuse; 9 stale cases X1–X9 | lance-graph `.claude/plans/recursive-perspective-rebinding-v1.md` §6 (#1622) | lance-graph | prepared frame → reuse or refuse | — | — | — | `Witness` | the probe implements the refusal; X1–X9 not run | — | PARTIAL | X1–X9 | +| epistemic basin B0–B11 (four spaces kept apart; duplicate roots do not inflate support; UNKNOWN never becomes zero or false) | lance-graph `docs/research/epistemic-awareness/2026-10-29-epistemic-basin-metathought-pr-scratchpad.md` (#1848) | lance-graph | — | — | — | — | — | — | — | PROPOSED | all | + +The Haiku maps behind this table were spot-checked against the source at +their stated lines: `ordered_lane.rs:193` and `:264`, +`simd_avx512.rs:2186`, `simd_masking_ops.rs:6053`, and 10 `perm.rs` items. +Every one matched. + +## A1: position antenna + +Fixture: 64 positions with four byte planes (magnitude, polarity, predicate, +selector), one `Perm64` basis, and a frame number. Three operations: +- `count(pred & positive)`; +- a masked signed sum (`sum8_u8_add_masked` on each side); +- a select `(sel & (pred ^ pos)) | (!sel & (pred & pos))`. + +| ns per block (64 positions) | native L1 | v4 L1 | v3 L1 | native streamed | +|---|---|---|---|---| +| P0 separate preparation per operation | 3.75 – 4.69 | 3.77 – 5.08 | 8.33 – 8.38 | 13.9 – 16.4 | +| P1 shared basis: prepare + run | 3.50 – 4.22 | 3.50 – 4.08 | **42.4 – 42.7** | 10.4 – 12.4 | +| ↳ setup only | 1.77 – 2.73 | 1.70 – 2.53 | 2.78 – 2.81 | 9.7 – 11.4 | +| ↳ execution only | 2.47 – 3.63 | 2.50 – 3.44 | 5.23 – 5.27 | 8.8 – 10.4 | +| P2 eager rebase: prepare + 3 × `conjugate_mask` + run | 16.4 – 17.6 | 15.2 – 17.3 | 246 – 261 | 20.6 – 21.6 | +| ↳ rebase only (3 × `conjugate_mask`) | 13.6 | 13.3 – 15.5 | 179 | 14.6 – 17.0 | +| **P2-lazy: run in source, conjugate the select result once** | **6.34 – 7.05** | 6.36 – 9.03 | 53.4 – 55.9 | 10.4 – 11.3 | +| ↳ 3 × blended conjugation (`mask_blend` + `materialize`) | **2.42 – 2.58** | 4.31 – 8.11 | 453 – 466 | 7.2 – 7.7 | +| reference: materialize all 4 planes | 9.64 – 10.9 | 15.3 – 21.5 | 57.1 – 58.2 | 11.1 – 11.7 | + +Findings: + +- **Sharing the basis is useful without sharing a mask** (PROVEN; WIN on + AVX-512). P1 prepares three masks once and every operation reuses them: 0.93× + of P0 in L1 and 0.79× streamed. That is preparation sharing; no mask is + shared across operations of different domains. +- **A rebase never needs to move the magnitudes** (PROVEN). Count and the + signed sum are permutation-invariant, so the re-based basis evaluates them in + the source basis. The falsifier `mixing_bases_changes_the_result` shows that + re-based masks over unmoved magnitudes give a wrong sum, so "evaluate in + whichever basis is consistent" is load-bearing. +- **Defer the rebase to the one equivariant result** (PROVEN; WIN). Lazy + rebase: `p∘select(a,b,c) == select(p∘a, p∘b, p∘c)` because select is + lane-local. That turns 3 conjugations into 1, so 6.3 ns instead of 16.4 ns + on VNNI. The negative, `lazy_rebase_is_refused_for_a_positional_result`, + shows that the same deferral over a prefix-parity result is wrong. +- **`conjugate_mask` is the cost, not the algebra** (MEASURED; fruit, not + fixed here). Its body expands the mask to bytes with a 64-lane + `core::array::from_fn` (perm.rs:266) before the `permute_bytes`. With the + expansion replaced by one `U8x64::mask_blend`, the same map costs 0.81 ns + per conjugation instead of 4.5 on VNNI (equal bit for bit on 5 masks for each + of 39 maps, 195 pairs). On AVX2 `mask_blend` is a per-lane loop and the blended + form is 2.5× **worse**. So the fix is per tier, and it belongs to `perm.rs`'s + owner, not to this lab. +- **AVX2 P1 anomaly** (OPEN). Setup + execution measured apart cost 8 ns, but + together 42 ns. The array-backed AVX2 `U8x64` in a by-value `Prepared` is the + likely cause. Not root-caused. +- Control bits follow their positions (`selector_must_follow_its_positions`); + a stale frame is refused with both frames named (`a_stale_basis_is_refused`); + two domains meet only through the relative map + (`two_domains_meet_through_the_relative_map`). + +## A2: exposure antenna + +- E0 = B and E1 = E5 are unchanged. +- E2 prepares the sign-routed operand once: `a_pos = maskz(a, !neg)`, + `a_neg = maskz(a, neg)`. The `low7` dots then run unmasked on it, and the + anchor narrows the same vectors by bit 7. +- Reuse law: `maskz(maskz(a, s), t) == maskz(a, s & t)`. It is proven per byte + by `a2_narrowing_law_holds_and_is_not_identity`, and E2 is exact on all + 511 × 511 pairs and on worst-case runs across three flush bounds. + +| ns per 64 values | native L1 | v4 L1 | v3 L1 | native streamed | v4 streamed | +|---|---|---|---|---|---| +| E0 = B end-to-end | **2.89 – 2.91** | 5.63 | **10.0** | 8.2 – 9.8 | 12.3 – 13.2 | +| E1 = E5 end-to-end | 3.52 – 3.53 | 5.11 | 12.5 | 9.1 – 10.7 | 12.0 – 13.1 | +| **E2 end-to-end** | 3.19 | **4.69** | 73.6 – 84.6 | 8.5 – 10.1 | **11.1 – 12.9** | +| B / E5 / E2 arithmetic only | 2.39 / 2.75 / 2.53 | 5.00 / 4.44 / **4.17** | 9.2 / 10.9 / 73.6 | — | — | +| B / E5 / E2 scan | 2.66 / 3.28 / 2.92 | 4.77 / 4.64 / **4.29** | 9.2 / 11.6 / 74.8 | 3.2–5.1 / 3.6–5.6 / 3.5–5.1 | — | +| E3 two consumers, two passes | 3.03 – 3.09 | 5.61 – 5.64 | 11.4 | 24.5 – 28.4 | 33.4 – 39.5 | +| **E3 fused, one pass** | **2.42 – 2.44** (0.79×) | 5.28 (0.94×) | 9.7 – 10.2 (0.87×) | 15.8 – 17.4 (0.6–0.7×) | 22.9 – 23.4 (0.6–0.7×) | + +As in #389/#393, the streamed "arithmetic only" rows read precomputed +operands that are larger than the compact layout, so they measure memory and +are left out. + +Steady-state loop bodies (instructions; no stack operands on any AVX-512 +body): + +| tier | B | E5 | **E2** | E3 fused | positive-|a| alone | +|---|---|---|---|---|---| +| VNNI | 18: 4 `vpdpbusd`, 2 `vmovdqu8{z}` | 23: 2 `vpdpbusd`, 4 `{z}`, 2 `vpsadbw`, 2 `vpaddq`, `kandq`, `kandnq` | **21**: same, **without `kandq`/`kandnq`** | 20: B + 1 `vpsadbw` + 1 `vpaddq`, **still 2 `{z}`** | 9 | +| v4 | 40 | 36 | **34** | 42 | 9 | +| AVX2 | 122, 22 stack operands | 145, 18 | **510, 134** (per-lane `mask_blend`) | 133 | 28 | + +Findings: + +- **E2's reuse is exact, and its lowering removes the mask ALU, not the + moves** (PROVEN, verified in the assembly). LLVM does **not** fold the nested + `maskz` into one masked move: E2 still has 4 zero-masked moves, like E5. What + disappears is E5's `kandq`/`kandnq` (the `s & t` mask), 2 instructions per + block. +- **E2 is the best U9 candidate on AVX-512 without VNNI** (WIN). L1 + end-to-end 4.69 vs E5 5.11 vs B 5.63; arithmetic 4.17; scan 4.29. Every one + of three runs and every row beats E5 and B on that tier. Streamed, the + ranges overlap with E5 (host noise, as in #393). +- **E2 still loses to B on VNNI** (LOSS, 1.10×). It beats E5 there (3.19 vs + 3.53). The cause is unchanged from #393: B's fourth `vpdpbusd` reuses the + sign's zero-masked copy, while the anchor needs a second masked move per + sign. +- **E2 is refused on AVX2** (LOSS, 7×). `U8x64::mask_blend` is a per-lane + loop there. On that tier `sum8_u8_add_masked` builds its keep mask in + registers, so E5 is the better shape. +- **Two consumers fused share the preparation, not the accumulators** (WIN on + every tier). E3 keeps B's `i32` lanes with their flush law and the + positive-|a| sum's `u64` lanes with none. In the VNNI body the second + consumer reuses B's existing zero-masked copy of `a` (still 2 `{z}`) and + adds 2 instructions instead of a 9-instruction loop. The win is 0.79× in L1 + and 0.6–0.7× streamed (one read of `a` instead of two). + +## A3 and A4: order and law + +`order_law.rs`, 18 tests. A3 keeps three orders separate: +- traversal order: no effect on invariant folds; +- coordinate order: the basis; no effect on invariant folds, carried by + equivariant ops; +- effect order: `Set`/`Add`/`Mul` sequences; `x=1; x+=1` ≠ `x+=1; x=1`. + +A3 cases: +- Two readers of one snapshot see the same version. +- A sequential dependency must see the first result. +- `check_reorder` refuses a reorder of two non-commuting effects and names + both. + +A4 checks each licensed optimization against a negative example. Two of +them (reorder and defer) also have disable runs, X7 and X8. + +| optimization | licensed by | negative example | correct | asm vs direct baseline | +|---|---|---|---|---| +| reorder a fold | `PermInvariant` (count, sum, min, max) | `IndexWeightedSum` is a `LaneFold` and not invariant; reordering changes it | PROVEN | count with the map skipped: **3 instructions** (`vptestmb`, `kmovq`, `popcnt`) vs ~200 with `materialize` (VNNI) | +| fuse two lane ops | both `PermEquivariant` and lane-local | `PrefixSum ∘ AND` is not fusable into one lane op | PROVEN | `(a^b)&c` is **already one `vpternlogq` (0x48)** in the direct form; the explicit `ternlog::<0x28>` adds nothing (**TIE**) | +| share coordinate preparation | the same frame and the same basis | a stale frame or a different basis is refused (A1) | PROVEN | A1 P1 vs P0 | +| defer a reduction | associative and commutative, **plus an exact bound** | flushing at bound + 1 = 16,449 blocks overflows `i32`; bound = ⌊i32::MAX / 130,560⌋ = 16,448, computed in the test | PROVEN | #393 (`B_FLUSH_BLOCKS` = 16,384 sits under the bound) | +| propagate a compact result | invariant: no carry; equivariant: one carry of the result | a positional result (prefix parity) cannot be carried after the fact (A1) | PROVEN | A1 P2-lazy | +| refuse an invalid composition | `check_reorder`; mask-risc `ExtentUnsupported` | `Set` across `Add` | PROVEN | — | + +`LAW_TABLE` (10 rows) records shape, lane-locality, associativity, +commutativity, invariance, equivariance, ordered effects, exactness, overflow, +snapshot and frame for every operation used. It is a **lab table**, not a +trait. The equivalent production knowledge already lives in mask-risc: +commutativity read from the ternlog truth table, a merge law per terminal, and +stated row bounds. No new trait restates it. + +## A5: meta-SoA antenna + +`meta.rs`, 9 tests, a pure scalar oracle. The fixture: +- 1 sealed WORLD (id 7, version 1, 64 Kleene facts, 6 UNKNOWN); +- 2 THOUGHT overlays; +- 3 methods (AllOf, AnyOf, AtLeast-3); +- 2 rules (OpenWorld and ClosedWorld); +- 1 meta-evaluation. + +Each `Receipt` records: +- frame/version; +- basis id; +- method id; +- order witness (FNV-1a over the step list); +- policy (the law); +- result and evidence; +- typed dependencies `{kind, id, version}`. + +The meta fold (`meta_evaluate`, `which_changed`, `aggregate`, `may_reuse`) +reads receipts only. `meta_fold_reads_receipts_only` evaluates it after the +world has been dropped. + +| negative case | detected by | disable run | +|---|---|---| +| stale source | `may_reuse` → `StaleDep{kind, id, recorded, current}` | X10 red | +| policy change with unchanged evidence | `compare` → `rule_changed` | X13 red | +| different thoughts treated as the same | `which_thought_changed_the_result` | — | +| UNKNOWN treated as FALSE | `unknown_is_not_false` (only ClosedWorld coerces) | X9 red | +| method order changing the effects | order witness → `OrderChanged` | X11 red | +| provenance lost in aggregation | `aggregate` keeps every child and the deduplicated dependency union | X12 red | + +`aggregate` deduplicates dependencies, so a dependency named twice does not +count twice. That is the receipt-level half of #1848's "duplicate roots do not +inflate support"; the support half (votes) is not modelled. OPEN, it belongs +to #1848 B4. + +## A6: scale antenna + +The field is the 64×64 = 4,096 cells of a `PermTable12`, and one field-wide +question: `Σ #{ i : A[i] ∧ B[cell[i]] }`. No dense 64³ structure is +allocated; the largest object is the 8 KiB exposure kernel. + +| µs per field | native | v4 | v3 | compositions | bytes written | allocations | +|---|---|---|---|---|---|---| +| per cell, materialized, row-major | 51.4 | 54.5 | 165 – 168 | 4,096 | 262,144 | 0 | +| per cell, materialized, Morton | 51.4 | 54.5 | 165 | 4,096 | 262,144 | 0 | +| per cell, conjugated mask, row-major | **5.2 – 5.7** | 9.6 – 11.0 | 1,138 – 1,150 | 4,096 | **0** | 0 | +| per cell, conjugated mask, Morton | 5.2 – 5.8 | 9.6 – 10.6 | 1,132 – 1,143 | 4,096 | 0 | 0 | +| whole field through `Exposure` | 7.6 – 8.0 | **7.5** | **6.1** | 0 | 8,192 | 1 (8,192 B) | + +Findings: +- **Exposure folding is the only tier-independent form** (WIN on v3 by 190×, + TIE on AVX-512). +- **Per-cell conjugation is fastest on VNNI**, at about 1.3 ns per cell, 0 + bytes written. On AVX2 it is the worst, because `conjugate_mask` there is the + scalar expansion plus the array-backed `permute_bytes`. +- **Row-major vs Morton: TIE on every tier.** The table's working set is 8 KiB + and stays in L1, so traversal order does not matter at this size. The + traversal law holds: both orders give the same answer + (`morton_visits_every_cell_once`). +- Cache-miss counters were not available in this container; working set, + bytes written and allocations come from the counting allocator and the + `Traffic` counters. + +## Discovery matrix + +| antenna | reusable substrate | new law found | missing element | correctness | cost | verdict | +|---|---|---|---|---|---|---| +| A1 shared basis | `Perm64`, masking ops | preparation sharing is independent of mask sharing | basis/frame identity is not on `Perm64` | PROVEN | WIN (0.79–0.93×) AVX-512; LOSS v3 (OPEN anomaly) | ADOPT-LAB | +| A1 rebase | `conjugate_mask`, `PermInvariant`/`Equivariant` | invariant: no carry; equivariant: carry the result once | cheap mask→bytes expansion in `conjugate_mask` | PROVEN | P2-lazy WIN 2.6× over eager; eager LOSS vs materialize | ADOPT-LAB (lazy); fruit for the `perm.rs` owner | +| A2 E2 | `mask_blend`, `dot4_u8_i8_add`, `sum8_u8_add_masked` | nested maskz = maskz of the AND; lowering removes the mask ALU, not the moves | AVX2 `mask_blend` | PROVEN | WIN v4; LOSS VNNI vs B (WIN vs E5); LOSS AVX2 | ADOPT-LAB on v4; #393 unchanged | +| A2 E3 | same | two consumers share preparation and keep separate accumulator laws | — | PROVEN | WIN all tiers (0.63–0.94×) | ADOPT-LAB | +| A3 order | `Perm64`, snapshot by value | three orders are independent; effects need a partial order | — | PROVEN | UNMEASURED (semantic) | PROVEN | +| A4 law | markers + mask-risc laws | every admitted rewrite has a counterexample | marker traits are unchecked | PROVEN | count-skip 3 vs ~200 instructions; ternlog fusion TIE (LLVM already does it) | PROVEN | +| A5 meta | mask-risc witnesses, thought-git-probe receipts | a receipt-only second fold is sufficient | `DurableRef`, `ThoughtCommitId` (PROPOSED in D-CPG) | PROVEN (scalar oracle) | UNMEASURED | PARTIAL (support counting OPEN) | +| A6 scale | `PermTable12::exposure` | the field fold is tier-independent; traversal is free at 8 KiB | — | PROVEN | Exposure TIE/WIN; per-cell conj WIN VNNI, LOSS AVX2 | ADOPT-LAB | + +## The distilled contract: already represented, nothing new prescribed + +| element | where it already lives | gap | +|---|---|---| +| **POSITION** | `Perm64` (map), `InBasis` (basis = map value), `conjugate_mask` (masks move without data), `Morton8x8` / HHTL16 (DR addressing, #1835) | a map carries no basis id or frame; the frame comes from WITNESS | +| **ORDER** | `Perm64::then` (composition order); `OrderedLaneWitness` (sealed key order); mask-risc `Program` (straight-line ops, one terminal); DT method schema (ordered effects, #1835) | the effect-order refusal exists only in this lab (`check_reorder`) and in DT's PROPOSED schema | +| **LAW** | `PermInvariant`, `PermEquivariant` (markers); mask-risc `GroupFold::merge`, commutativity from the ternlog table, `ExtentUnsupported`, `MASKED_SUM_I32_MAX_ROWS`; W1a overflow docs | markers are unchecked; exactness bounds are per-PR prose (B_FLUSH_BLOCKS) | +| **EXPOSURE** | `PermTable12::exposure` / `Exposure::count_where` (the field); the prepared operand (A2 E2, E3) | — | +| **WITNESS** | `OrderedLaneWitness` + `SealedFacetLane::validate` (O(1)) / `verify` (O(n)); RPR witness-gated reuse; thought-git-probe `VersionStore::seal` | `DurableRef` / `ThoughtCommitId` PROPOSED; the RPR stale cases X1–X9 not run | + +No new struct or trait is needed: all five elements exist, and they live in +ndarray (POSITION, LAW markers, EXPOSURE) and lance-graph (ORDER, LAW tables, +WITNESS). That split follows the repo rule: ndarray = hardware, lance-graph = +meaning. + +## Q1–Q3 + +**Q1. What can be reused without materialization?** + +1. A **prepared position basis**: the masks built once from byte planes, + shared by every operation that reads them (A1 P1). +2. The **result of an invariant fold** across any rebase or traversal order: + no carry at all (A1, A4, A6). +3. The **result of an equivariant op**, carried once by `conjugate_mask` + instead of carrying its inputs (A1 P2-lazy). +4. A **prepared operand** across consumers with different accumulator types + (A2 E2 within one kernel; A2 E3 across two consumers). +5. A **field of maps** as one 64×64 exposure kernel instead of 4,096 + compositions (A6). +6. A **receipt**: the second fold reads receipts only (A5). + +Materialization was never required. It was only the slowest correct form. + +**Q2. Which laws make that reuse correct?** + +- Permutation invariance licenses skipping or reordering the map for folds. +- Lane-local permutation equivariance licenses carrying one result instead of + its inputs, and fusing lane ops. +- Associativity and commutativity **with a stated exactness bound** license + deferring a reduction (16,448 blocks, not "large"). +- Frame and basis equality license sharing preparation. +- Dependency-version equality and order-witness equality license reusing a + receipt. +- `maskz(maskz(a, s), t) = maskz(a, s & t)` licenses narrowing a prepared + operand. + +Each license has a counterexample in the tests, and removing each one turns a +test red (14 disables). + +**Q3. What is the smallest fold result that still carries its evidence?** + +`(result, law, basis/frame, order witness, dependency versions)`, with UNKNOWN +kept as its own value of `result`: +- Without the law, a policy change with identical evidence is invisible. +- Without the frame, a stale source is reused. +- Without the order witness, reordered effects are reused. +- Without the dependencies, aggregation loses provenance. +- Collapsing UNKNOWN into FALSE changes AnyOf/AtLeast answers. + +A5 has one failing test for each omission. Evidence is optional for +correctness; it is what makes the result explainable, not reusable. + +## Correctness record + +`tests/pof_antennas.rs` + the module tests: 41 tests. They pass on: +- native (AVX-512 VNNI), v4 and v3; +- AVX (qemu SandyBridge) and v2 (qemu Nehalem); +- aarch64 (qemu); +- nightly-simd. + +Clippy `-D warnings` and rustfmt are clean. The facet-stride guard reports +nothing on the added lines; the lab uses `Perm64`'s API for every byte move. + +Disable runs (commit first, patch with an asserted anchor, run, `git +checkout`), each red: + +| id | disable | red tests | +|---|---|---| +| X1 | A1 selector left in the source basis | 3 | +| X2 | A1 stale frame accepted | 2 | +| X3 | A1 lazy rebase drops the result conjugation | 1 | +| X4 | A2 E2 anchor narrows the raw operand | 2 | +| X5 | A2 E2 sign routing inverted | 2 | +| X6 | A2 E3 second consumer reads the wrong sign | 1 | +| X7 | A3 every reorder admitted | 5 | +| X8 | A4 deferred reduction never flushes | 1 | +| X9 | A5 UNKNOWN coerced to FALSE under every policy | 3 | +| X10 | A5 reuse ignores dependency versions | 2 | +| X11 | A5 reuse ignores the order witness | 1 | +| X12 | A5 aggregation drops provenance | 1 | +| X13 | A5 policy not compared | 1 | +| X14 | A6 moving mask not conjugated | 1 | + +## Fruits (not done here) + +1. `Perm64::conjugate_mask`: expand the mask with one masked select on + AVX-512 (5.6× in this probe), keep the current path on AVX2. This changes + production code, so it is owned by `perm.rs` and needs its own PR with + parity tests. +2. E2 as the AVX-512-without-VNNI U9 kernel: it beats E5 there in every row. + It would join #393's ADOPT-LAB row; it is not integrated. +3. The AVX2 `U8x64::mask_blend` per-lane loop (already on the facet-stride + R2 list) is what refuses E2 and the blended conjugation on v3. +4. The AVX2 P1 anomaly (8 ns apart, 42 ns together): OPEN. +5. The lance-graph RPR stale cases X1–X9 and #1848 B0–B11 remain theirs; A5 + is a scalar oracle that a B0 fixture could reuse. From c86d3bf9e7a0a3c919c9c007e417945f1a30da6f Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 23:42:11 +0000 Subject: [PATCH 3/4] pof antennas: checked-overflow commutation and full-width step witness `commutes` admitted Add/Add and Mul/Mul unconditionally, but under `run_effects`' checked semantics a swap can turn an overflow into a value (Add(1), Add(-1) from i64::MAX; Mul(-1), Mul(0) from i64::MIN). Add pairs now commute only without opposite signs, Mul pairs only when equal, one is 1, or both have magnitude >= 2; a brute-force test over boundary values checks every admitted pair. `order_witness` truncated lane indices to u8, so NegateFact(0) and NegateFact(256) shared a witness; it now encodes the full index. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMMjKnig6MXTd41Lf2v --- examples/pof_antennas/meta.rs | 25 +++++++++-- examples/pof_antennas/order_law.rs | 71 +++++++++++++++++++++++++++--- 2 files changed, 86 insertions(+), 10 deletions(-) diff --git a/examples/pof_antennas/meta.rs b/examples/pof_antennas/meta.rs index 80a068c2..8cc40889 100644 --- a/examples/pof_antennas/meta.rs +++ b/examples/pof_antennas/meta.rs @@ -268,6 +268,11 @@ pub fn apply_steps(mut v: [Tri; 64], steps: &[Step]) -> [Tri; 64] { } /// Order-sensitive FNV-1a over a canonical byte encoding of the step list. +/// +/// The lane index is encoded in full (8 bytes): truncating it would give +/// `NegateFact(0)` and `NegateFact(256)` the same witness although only the +/// first one changes a lane. Two out-of-range steps (both no-ops) still get +/// different witnesses; that only refuses a reuse that would have been safe. pub fn order_witness(steps: &[Step]) -> u64 { let mut h: u64 = 0xcbf2_9ce4_8422_2325; let mut eat = |b: u8| { @@ -276,11 +281,13 @@ pub fn order_witness(steps: &[Step]) -> u64 { }; for s in steps { let (tag, i, t) = match *s { - Step::SetFact(i, t) => (1u8, i as u8, t.byte()), - Step::NegateFact(i) => (2u8, i as u8, 0u8), + Step::SetFact(i, t) => (1u8, i as u64, t.byte()), + Step::NegateFact(i) => (2u8, i as u64, 0u8), }; eat(tag); - eat(i); + for b in i.to_le_bytes() { + eat(b); + } eat(t); } h @@ -856,4 +863,16 @@ mod tests { assert_eq!(changed.len(), 1); assert_eq!(changed[0].0, 2); } + + /// A lane index that differs only above the low byte changes the + /// witness, so a receipt for `NegateFact(0)` is not reused for + /// `NegateFact(256)` (which is a no-op and gives a different result). + #[test] + fn witness_keeps_the_full_lane_index() { + let (a, b) = ([Step::NegateFact(0)], [Step::NegateFact(256)]); + assert_ne!(order_witness(&a), order_witness(&b)); + let mut v = [Tri::False; 64]; + v[0] = Tri::True; + assert_ne!(apply_steps(v, &a)[0], apply_steps(v, &b)[0]); + } } diff --git a/examples/pof_antennas/order_law.rs b/examples/pof_antennas/order_law.rs index 2881a6b6..240023e0 100644 --- a/examples/pof_antennas/order_law.rs +++ b/examples/pof_antennas/order_law.rs @@ -59,15 +59,31 @@ pub fn run_effects(init: i64, effs: &[Effect]) -> Option { effs.iter().try_fold(init, |cell, e| e.apply(cell)) } -/// Whether two effects can be swapped without changing any final value. +/// Whether two effects can be swapped without changing the result of +/// [`run_effects`] for ANY starting value, overflow included: a swap must not +/// turn a reported overflow (`None`) into a value or back. /// -/// The rule: `Add`/`Add` commute, `Mul`/`Mul` commute, `Set(x)`/`Set(y)` -/// commute iff `x == y`. Every mixed pair does not commute: `Set`/`Add`, -/// `Set`/`Mul` and `Add`/`Mul` are all order-sensitive. +/// Under checked arithmetic, exact-integer commutativity is not enough: +/// +/// * `Add(a)`/`Add(b)` commute iff `a` and `b` do not have opposite signs. +/// With both `>= 0` (or both `<= 0`) the intermediate lies between the +/// start and the final value, so it overflows only if the final value does. +/// With opposite signs it does not: from `i64::MAX`, `Add(1), Add(-1)` +/// overflows while `Add(-1), Add(1)` returns `i64::MAX`. +/// * `Mul(a)`/`Mul(b)` commute iff `a == b`, either factor is `1`, or both +/// have magnitude `>= 2`. In the last case the intermediate has at most half +/// the final magnitude, so it fits whenever the final value does. A `0` or +/// `-1` factor breaks it: from `i64::MIN`, `Mul(-1), Mul(0)` overflows while +/// `Mul(0), Mul(-1)` returns `0`. +/// * `Set(x)`/`Set(y)` commute iff `x == y`. +/// * Every mixed pair (`Set`/`Add`, `Set`/`Mul`, `Add`/`Mul`) is +/// order-sensitive. pub fn commutes(a: &Effect, b: &Effect) -> bool { - match (a, b) { - (Effect::Add(_), Effect::Add(_)) => true, - (Effect::Mul(_), Effect::Mul(_)) => true, + match (*a, *b) { + (Effect::Add(x), Effect::Add(y)) => !((x < 0 && y > 0) || (x > 0 && y < 0)), + (Effect::Mul(x), Effect::Mul(y)) => { + x == y || x == 1 || y == 1 || (x.unsigned_abs() >= 2 && y.unsigned_abs() >= 2) + } (Effect::Set(x), Effect::Set(y)) => x == y, _ => false, } @@ -620,6 +636,47 @@ mod tests { } } + /// Soundness of `commutes` under checked arithmetic: every admitted pair + /// gives the same `run_effects` result in both orders for every boundary + /// start value, and the overflow counterexamples are refused. + #[test] + fn commutes_is_sound_under_checked_overflow() { + let vals = [i64::MIN, i64::MIN + 1, -(1 << 62), -3, -2, -1, 0, 1, 2, 3, 1 << 62, i64::MAX - 1, i64::MAX]; + let mut effs = Vec::new(); + for &v in &vals { + effs.extend([Effect::Add(v), Effect::Mul(v), Effect::Set(v)]); + } + let (mut admitted, mut refused) = (0, 0); + for a in &effs { + for b in &effs { + if commutes(a, b) { + admitted += 1; + for &x in &vals { + assert_eq!(run_effects(x, &[*a, *b]), run_effects(x, &[*b, *a]), "{a:?} {b:?} from {x}"); + } + } else { + refused += 1; + } + } + } + // Anti-vacuity: both sides are populated. + assert!(admitted > 100 && refused > 100, "admitted {admitted}, refused {refused}"); + // The two counterexamples. + assert_eq!( + check_reorder(&[Effect::Add(1), Effect::Add(-1)], &[1, 0]), + Err(OrderRefusal { first: 0, second: 1 }) + ); + assert_ne!( + run_effects(i64::MAX, &[Effect::Add(1), Effect::Add(-1)]), + run_effects(i64::MAX, &[Effect::Add(-1), Effect::Add(1)]) + ); + assert!(!commutes(&Effect::Mul(-1), &Effect::Mul(0))); + assert_ne!( + run_effects(i64::MIN, &[Effect::Mul(-1), Effect::Mul(0)]), + run_effects(i64::MIN, &[Effect::Mul(0), Effect::Mul(-1)]) + ); + } + #[test] fn mixed_sequence_partial_order() { let effs = [Effect::Add(1), Effect::Set(10), Effect::Add(2), Effect::Add(3)]; From 48b4bf749abfc1a910b3018c59124bcd24ccb366 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 23:42:40 +0000 Subject: [PATCH 4/4] pof antennas report: record the two review fixes and their disable runs Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMMjKnig6MXTd41Lf2v --- .claude/knowledge/pof-antennas-probe.md | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/.claude/knowledge/pof-antennas-probe.md b/.claude/knowledge/pof-antennas-probe.md index 5d314ac2..6448aafd 100644 --- a/.claude/knowledge/pof-antennas-probe.md +++ b/.claude/knowledge/pof-antennas-probe.md @@ -204,6 +204,13 @@ A3 cases: - A sequential dependency must see the first result. - `check_reorder` refuses a reorder of two non-commuting effects and names both. +- Commutation is judged under the checked semantics, not exact integers + (corrected after review). A swap must not turn an overflow into a value: + `Add(1), Add(-1)` from `i64::MAX` overflows, while the reverse returns + `i64::MAX`. So `Add` pairs commute only without opposite signs, and `Mul` + pairs only when equal, when one factor is 1, or when both have magnitude + `>= 2`. `commutes_is_sound_under_checked_overflow` checks every admitted + pair from 13 boundary start values. A4 checks each licensed optimization against a negative example. Two of them (reorder and defer) also have disable runs, X7 and X8. @@ -253,6 +260,7 @@ world has been dropped. | different thoughts treated as the same | `which_thought_changed_the_result` | — | | UNKNOWN treated as FALSE | `unknown_is_not_false` (only ClosedWorld coerces) | X9 red | | method order changing the effects | order witness → `OrderChanged` | X11 red | +| two step lists that differ only above a lane index's low byte | full-width index in the order witness (`witness_keeps_the_full_lane_index`; corrected after review) | Y3 red | | provenance lost in aggregation | `aggregate` keeps every child and the deduplicated dependency union | X12 red | `aggregate` deduplicates dependencies, so a dependency named twice does not @@ -365,7 +373,8 @@ correctness; it is what makes the result explainable, not reusable. ## Correctness record -`tests/pof_antennas.rs` + the module tests: 41 tests. They pass on: +`tests/pof_antennas.rs` + the module tests: 43 tests (41 at first push; +two added with the review fixes, re-run on native, v3 and aarch64). They pass on: - native (AVX-512 VNNI), v4 and v3; - AVX (qemu SandyBridge) and v2 (qemu Nehalem); - aarch64 (qemu); @@ -393,6 +402,9 @@ checkout`), each red: | X12 | A5 aggregation drops provenance | 1 | | X13 | A5 policy not compared | 1 | | X14 | A6 moving mask not conjugated | 1 | +| Y1 | `commutes` admits every `Add`/`Add` pair (review fix) | 1 | +| Y2 | `commutes` admits every `Mul`/`Mul` pair (review fix) | 1 | +| Y3 | order witness truncates the lane index to `u8` (review fix) | 1 | ## Fruits (not done here)