Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
132 changes: 132 additions & 0 deletions .claude/knowledge/dr512-epistemic-pm-invariant.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
# DR512 / Codec9 universal epistemic P × magnitude law

**Operator ruling 2026-10-28.** This is the one DR512 law, not a numerical mode
selected by a consumer. It supersedes the signed-negative-bit reading in the
historical `palette512-signed-magnitude9-experiment-20261027.md` and the
two-plane probe in ndarray #381. This is a proposed lab CI gate, not
permission for BGZ wire migration, Quack source authorization, DR64³ layout,
or DT64 production dispatch.

| Presence P | Magnitude M | Meaning |
|---|---|---|
| 0 | 0 | **-0 / NaN / epistemically NEVER TOUCHED** |
| 0 | 1..255 | negative numeric value -1..-255 |
| 1 | 0 | valid **+0** |
| 1 | 1..255 | positive numeric value +1..+255 |

One u8 magnitude plus **one** presence bit per numeric row:
64 magnitudes + one u64 presence word = 72 bytes per 64 rows;
512 distinct codewords, exactly 511 signed numeric values and one
never-touched code. Numeric polarity P is NOT access control or alpha
write authority. Negative numeric evidence also is not a source-attested
Boolean negation unless such a mapping is established separately.

## The ONLY never-touched WHERE

```text
WHERE (P == 0) AND (M == 0)
```

No additional 8-KiB sentinel mask is required. A consumer can derive a
bitmap ON DEMAND if its vector engine needs one, but absence cannot be
inferred from P alone: P=0,M>0 carries a valid negative value.

## Touched write: normalize zero to +0

A write/calculation already admitted by its source owner obtains a **touched**
numeric value. Encode with `Codec9::encode_touched`. If the quantized
magnitude is zero, emit P=1,M=0 unconditionally. Pre-existing untouched
P=0,M=0 rows are not touched, not claimed and must remain untouched.
This holds especially for -0.49999, -0.4 and -0.0:

- TiesEven: -0.5 rounds to **valid +0**; -0.50001 → -1.
- TiesAway: -0.5 → -1; -0.4 → **valid +0**.
- Explicitly touched NaN/infinity is rejected, not converted into the
never-touched sentinel. Finite out-of-range values saturate at ±255.
- LUT9 preserves an *existing* -0/NaN; when a nonzero negative LUT input
becomes magnitude zero, it emits +0 and never fabricates absence.
- No numerical threshold or range filter `(-0.5,0)` is required.
The determinant is the touched operation and final quantized zero.

## Existing compile-time owner patterns

`Codec9<R, C>` intentionally reuses ndarray
`codec8::{Rounding, TiesEven, TiesAway, Calibration}` and fixes the
other semantic parameters by construction. Asym, Floor and
`NoNaN` must **not** select a second DR512 bit interpretation. Codebook
enums with 512 arbitrary tokens are different from DR512 signed numeric
codes: they must retain their own typed IDs and source mapping. Never
reinterpret `bgz-tensor::WeightPalette` u8 archetypes as signed magnitudes.

## Cross-repo ownership and CI tripwires

1. **ndarray:** `src/hpc/codec9.rs`, `src/simd_stride.rs`,
`examples/palette512_probe.rs`, `examples/sm9_presence_probe.rs`,
`examples/lut9_bench.rs`, `crates/simd-masking-parity/src/lib.rs`.
Exhaustive 512-codeword oracle, negative-zero ceiling test,
backend/shape parity, WHERE 64K geometry.
2. **lance-graph DT64/Quack/DR64:** keep owner-issued source versions,
source authorization, K3 predicates, sparse write/snapshot and alpha
claims distinct. A numerical P=0 is **not** whitelist, permission or
proof that an ontology relationship is absent.
3. **Odoo, OGIT/OGAR and crai:** use pinned source codebook IDs;
guard incomplete registry, unresolved IDs and source-attested WHEN
/ ON / DO. Test 255/256/257 codebooks explicitly.
4. **MedCare:** no physical clinical-route promotion from a numeric
sentinel or unsigned-magnitude sign bit without its independent
compilation, ACL and source evidence.

This document does not grant a merge or production ABI change. Every
subsequent consumer PR must either prove exact P×M parity using the
independent oracle or refuse the integration. Operator-rejected
lance-graph #1812 stays quarantined and is NOT implementation evidence.


## [-a,+b] LUT distance efficiency, independent cold gate

For **valid numeric** DR512 pairs `x`, `y` with identical positive
magnitude step, distance need not use a 512×512 LUT:

```text
same P: abs(m_x - m_y)
opposite P: m_x + m_y
```

The result is `u16` (maximum **510**), **not** `u8`. The
512-codeword space has exactly one forbidden -0 sentinel that must
refuse distance instead of being treated as 0. Unit tests independently
decode all **511² = 261,121** valid numeric pairs and compare distances.

For a separately proposed calibrated asymmetric range [-a,+b], with
negative step a/255 and positive step b/255:

```text
both negative: abs(m_x-m_y) * a/255
both positive: abs(m_x-m_y) * b/255
opposite: m_negative * a/255 + m_positive * b/255
```

The `tests/dr512_epistemic_contract.rs` independent oracle checks the
[-3,+7] case over all 511² valid pairs. **This is a distance-law
analysis, not an approved alternative P×M codec, nor a measured
speedup.** A full pairwise distance table has 512² entries, or **512 KiB**
at u16; even separate same/opposite 256² u16 tables total **256 KiB**.
The arithmetic is a subtract/abs or an add and should be the baseline
before claiming LUT efficiency. Any real SIMD/L1/L2-cache comparison
requires a pinned host/ISA benchmark with end-to-end memory costs.

## CausalEdge64 extension: DEFERRED, do not implement in this PR

Current CausalEdge64 bits 0..23 are THREE 8-bit SPO palette codes;
24..39 are NARS truth, 40..58 Pearl rungs, 59..63 epistemic/reasoning.
If each SPO code were extended from 256 to 512 choices, THREE extra
bits are required per edge (one per S/P/O), not an available 3-bit
space in the existing 64-bit contract. A 3-bit sidecar might be
theoretically sufficient but needs all THREE original palette identities
to be associated with the same pinned source/codebook generation and
the sidecar to be versioned and snapshot-attested with them.
Cross-page splits, stale codebooks, incomplete witnesses and partial
writes must refuse reconstruction. Do NOT steal CausalEdge64 truth,
Pearl or Epi5 bits, alter current codecs, or promote a physical layout.
Evaluate independently, under lance-graph's CausalEdge64/DT64/DR64
owner, only after evidence of correctness and benefit. **DEFERRED**.
22 changes: 22 additions & 0 deletions .github/workflows/ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -472,8 +472,30 @@ jobs:
# mutually exclusive (`compile_error!`).
- run: cargo +nightly doc --no-deps --features approx,serde,rayon

# Canonical DR512 P×M never-touched contract. This must fail loudly on
# an inverted presence bit, a fabricated -0/NaN, a lost negative number,
# or a stale independent SIMD/SM9 reference. No optional/passive gate.
dr512-epistemic-tripwire:
runs-on: ubuntu-latest
name: dr512/epistemic-presence
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@1.99.0
- uses: Swatinem/rust-cache@v2
- name: Exhaustive codeword, distance, sparse-WHERE and negative-ceiling oracles
run: cargo test --test dr512_epistemic_contract
- name: Codec9 independent compile-time and scalar oracles
run: cargo test --lib hpc::codec9::tests
- name: LUT9 and its independent scalar lane oracle
run: cargo test --lib simd_stride::tests::lut9
- name: Legacy Palette512 arithmetic probe must agree on polarity
run: cargo test --example palette512_probe
- name: SM9 presence probe must have only one polarity plane
run: cargo test --example sm9_presence_probe

conclusion:
needs:
- dr512-epistemic-tripwire
- clippy
- format
- nostd
Expand Down
20 changes: 14 additions & 6 deletions crates/simd-masking-parity/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2651,6 +2651,14 @@ fn oracle_fma_f64(a: f64, b: f64, c: f64) -> f64 {
// the output sign plane bit by bit; it never calls the primitive.

fn check_lut9() -> Result<(), u32> {
// Canonical P×M four-way truth table, independent of random parity.
let identity: [u8; 256] = core::array::from_fn(|i| i as u8);
let mut actual = [0u8; 4];
let mut actual_presence = [u64::MAX];
lut9(&[0, 0, 255, 255], &[0b1010], &identity, &mut actual, &mut actual_presence);
if actual != [0, 0, 255, 255] || actual_presence != [0b1010] {
return Err(0x1430);
}
let mut rng = SplitMix64(0x1400_0000_0001);
// A random table with some zero entries away from index 0, so a sign bit
// must be cleared at nonzero magnitudes too, and every quarter differs.
Expand All @@ -2670,14 +2678,14 @@ fn check_lut9() -> Result<(), u32> {
let mags: Vec<u8> = (0..n)
.map(|i| if pass == 0 { stride(i) } else { rng.next() as u8 })
.collect();
let mut signs: Vec<u64> = (0..words).map(|_| rng.next()).collect();
let mut presences: Vec<u64> = (0..words).map(|_| rng.next()).collect();
if words > 0 && !n.is_multiple_of(64) {
// Junk sign bits past the last row must not reach the output.
signs[words - 1] |= u64::MAX << (n % 64);
presences[words - 1] |= u64::MAX << (n % 64);
}
let mut out = vec![0xAAu8; n + 3];
let mut out_signs = vec![u64::MAX; words + 1];
lut9(&mags, &signs, &table, &mut out, &mut out_signs);
let mut out_presences = vec![u64::MAX; words + 1];
lut9(&mags, &presences, &table, &mut out, &mut out_presences);
for i in 0..n {
if out[i] != table[mags[i] as usize] {
return Err(0x1400 | (pass << 7) | case);
Expand All @@ -2687,9 +2695,9 @@ fn check_lut9() -> Result<(), u32> {
return Err(0x1410 | (pass << 7) | case);
}
let want = reference_mask(n, words + 1, |i| {
(signs[i / 64] >> (i % 64)) & 1 == 1 && (table[mags[i] as usize] != 0 || mags[i] == 0)
((presences[i / 64] >> (i % 64)) & 1 == 1) || (table[mags[i] as usize] == 0 && mags[i] != 0)
});
if out_signs != want {
if out_presences != want {
return Err(0x1420 | (pass << 7) | case);
}
}
Expand Down
32 changes: 16 additions & 16 deletions examples/lut9_bench.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
//! * `i8 table`: the i8 `Sym` form, one 255-entry table indexed by the
//! signed code (`table[c + 127]`), no sign plane;
//! * `u8 table + sign`: the scalar form of what `lut9` computes, a
//! 256-entry lookup plus the sign plane cleared where a nonzero input
//! 256-entry lookup plus the epistemic presence bit set where a touched negative input
//! gives 0;
//! * `lut9`: the SIMD primitive.
//!
Expand Down Expand Up @@ -40,7 +40,7 @@ fn main() {
s
};
let mags: Vec<u8> = (0..N).map(|_| next() as u8).collect();
let signs: Vec<u64> = (0..N / 64).map(|_| next()).collect();
let presences: Vec<u64> = (0..N / 64).map(|_| next()).collect();
let codes: Vec<i8> = (0..N)
.map(|_| ((next() % 255) as i16 - 127) as i8)
.collect();
Expand All @@ -57,25 +57,25 @@ fn main() {

// Correctness first: the SIMD output must equal the scalar form.
let mut out_simd = vec![0u8; N];
let mut signs_simd = vec![0u64; N / 64];
lut9(&mags, &signs, &table, &mut out_simd, &mut signs_simd);
let mut presences_simd = vec![0u64; N / 64];
lut9(&mags, &presences, &table, &mut out_simd, &mut presences_simd);
let mut out_scalar = vec![0u8; N];
let mut signs_scalar = vec![0u64; N / 64];
let scalar = |out: &mut [u8], out_signs: &mut [u64]| {
let mut presences_scalar = vec![0u64; N / 64];
let scalar = |out: &mut [u8], out_presences: &mut [u64]| {
let rows = mags.as_chunks::<64>().0.iter();
for (w, (chunk, o)) in rows.zip(out.as_chunks_mut::<64>().0).enumerate() {
let mut nonzero = 0u64;
let mut became_positive_zero = 0u64;
for (k, (&m, d)) in chunk.iter().zip(o.iter_mut()).enumerate() {
*d = table[m as usize];
// Keep the sign where the result is nonzero or the input is -0.
nonzero |= u64::from(*d != 0 || m == 0) << k;
// P=0,M>0 rounded to zero becomes valid +0. Pre-existing -0 persists.
became_positive_zero |= u64::from(*d == 0 && m != 0) << k;
}
out_signs[w] = signs[w] & nonzero;
out_presences[w] = presences[w] | became_positive_zero;
}
};
scalar(&mut out_scalar, &mut signs_scalar);
scalar(&mut out_scalar, &mut presences_scalar);
assert_eq!(out_simd, out_scalar, "magnitudes differ");
assert_eq!(signs_simd, signs_scalar, "sign planes differ");
assert_eq!(presences_simd, presences_scalar, "sign planes differ");

let mut out_i8 = vec![0i8; N];
let t_i8 = best(|| {
Expand All @@ -85,12 +85,12 @@ fn main() {
black_box(&out_i8);
});
let t_scalar = best(|| {
scalar(&mut out_scalar, &mut signs_scalar);
black_box((&out_scalar, &signs_scalar));
scalar(&mut out_scalar, &mut presences_scalar);
black_box((&out_scalar, &presences_scalar));
});
let t_simd = best(|| {
lut9(black_box(&mags), black_box(&signs), &table, &mut out_simd, &mut signs_simd);
black_box((&out_simd, &signs_simd));
lut9(black_box(&mags), black_box(&presences), &table, &mut out_simd, &mut presences_simd);
black_box((&out_simd, &presences_simd));
});

println!(
Expand Down
Loading
Loading