Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
9 changes: 9 additions & 0 deletions .claude/blackboard.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,12 @@
## 2026-10-27 — NaN / presence bijection + SQL NULL=NaN predicates

- **Decision (operator):** on a float lane, presence IS NaN, held as a bijection: `presence bit i == 0 ⇔ values[i] is NaN` (predicate `x != x`, never a bit pattern, so wasm NaN canonicalization cannot break it). Missing and arithmetic NaN are deliberately merged. Integer lanes keep the presence plane as the only carrier. Supersedes the premise audit's Q1/Q2 split for float lanes (`.claude/plans/nan-exclusion-mindmap-scratch.md`).
- **Shipped (`simd_masking_ops.rs`, re-exported from `ndarray::simd`):** `not_nan_{f64,f32}_to_mask` (lane → mask, ordered `simd_eq` against itself), `nan_where_clear_{f64,f32}` (mask → lane, NaN under clear bits, cost ∝ clear bits), `presence_nan_mismatches_{f64,f32}` (witness, `popcount(presence XOR derived)` over live rows, no allocation), `{lt,le,gt,ge,eq,ne}_{f64,f32}_to_mask` (SQL TRUE plane: a NaN row never matches, `<>` included; a NaN threshold matches nothing), `mask_not_under(pred, presence)` = `presence & !pred` (SQL NOT, the FALSE plane). `F64Mask8::to_bitmask` added on AVX-512, AVX2/AVX, NEON, wasm and scalar (nightly had it).
- **Finding from the unit test:** `presence` for NOT must be the PREDICATE's presence (AND of its operands'), empty for a NULL literal. With the column's plane, `NOT (x > NULL)` reported every present row FALSE. Documented on `mask_not_under`.
- **Parity:** groups `0x13xx` (bijection: both directions, witness, round trip) and `0x139xx–0x13Cxx` (6 ops × 9 thresholds × 12 lengths, f64 and f32, plus the FALSE plane) against a bit-pattern reference (NaN by exponent/mantissa, order by sign-magnitude key, `-0 == +0`); no float compare in the reference. Arms green: native AVX-512, v3 AVX2, wasm, wasm-scalar, wasm-relaxed, neon-qemu, avx-qemu, v2-qemu, nightly.
- **Disable runs (each restored), all red:** f64 packer tail mask dropped (0x1301); `x == x` replaced by `x < inf` (0x1304); `nan_where_clear` skips the partial chunk (0x1322); witness counts dead bits (0x1341); SQL NULL-row gate dropped (0x13915, `<>`); NULL-literal threshold not refused (0x13905); NOT as a bare complement (0x13b00).
- **Not done:** the masked float fold (`n, mean, M2`, fixed order) and bit-identical float output across backends; three-valued AND/OR of two nullable predicates (TRUE/FALSE planes combine as `Ta & Tb` / `Fa | Fb` and dually; no primitive needed beyond mask_and/or, but no test either); GROUP BY over float keys (NaN != NaN, key on presence).

## 2026-10-27 — wasm `mul_add` certification audit (#378): relaxed-SIMD, proof obligations, X11

- **Relaxed SIMD, tested:** no source path selects on `relaxed-simd` (only the `simd_wasm.rs` module note mentions it). The parity wasm built with `+simd128` and with `+simd128,+relaxed-simd` has a byte-identical code section (621,383 bytes); only the `name` and `target_features` custom sections differ. Byte scan of the code section for relaxed-SIMD opcodes (`0xFD`, sub-opcode `0x100..0x113`): 0 hits; a control calling `f64x2_relaxed_madd` scans to 1 hit. The relaxed build passes under node 22. New arm `scripts/masking-parity.sh wasm-relaxed` and a CI step in `realization/wasm + scalar × wasm32`, as a guard against a relaxed path appearing later. What it establishes: the shipped arithmetic is the same under both flags for this compiler; it does not test an engine executing relaxed instructions, since none are emitted.
Expand Down
50 changes: 48 additions & 2 deletions .claude/plans/nan-exclusion-mindmap-scratch.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
# NaN exclusion for masked statistics: scratch mindmap

> **Status: SCRATCH, for later examination.** Nothing here is built, measured
> or decided. It maps purposes against the benefits and costs of each option,
> **Status: PARTLY BUILT (2026-10-27).** The NaN / presence bijection is
> shipped: `not_nan_{f64,f32}_to_mask` (lane → mask), `nan_where_clear_{f64,f32}`
> (mask → lane) and `presence_nan_mismatches_{f64,f32}` (the witness), with
> parity group `0x13xx` on every realization. See § "Decision: presence IS NaN"
> at the end. The masked float fold (S2) and float-output determinism are
> still open. The rest of this page is the original scratch: it maps purposes
> against the benefits and costs of each option. It maps purposes against the benefits and costs of each option,
> so a later session can pick a design without re-deriving the trade-offs.
> Context: the follow-up to #378 (wasm `mul_add` rounds once on every
> realization) and lance-graph `D-WFL-DET` (replay determinism).
Expand Down Expand Up @@ -212,3 +217,44 @@ are struck.
**Council status:** halted before Phase 1; nothing was implemented. Q2 alone
is probably too small for a council (two mask primitives and a convention).
Q1 and Q3 are not ndarray's to decide.

## Decision: presence IS NaN (operator, 2026-10-27)

On a float lane the presence bit and NaN are one state with two spellings,
held as a bijection:

```
presence bit i == 0 ⇔ values[i] is NaN (for every live row i)
```

This replaces the premise audit's Q1/Q2 split for float lanes. "Missing" and
"arithmetic produced NaN" are deliberately merged: a fold can read either
spelling and gets the same population, and `n` is the popcount of the plane it
folds, so dilution cannot occur. "Is NaN" is the predicate `x != x`, never a
bit pattern, so backends that do not preserve NaN payloads (wasm) cannot break
it. Integer lanes have no NaN; there the presence plane stays the only carrier.

Shipped primitives (`src/simd_masking_ops.rs`, re-exported from `ndarray::simd`):

| direction | function | cost |
|---|---|---|
| lane → mask | `not_nan_f64_to_mask`, `not_nan_f32_to_mask` | one ordered `simd_eq` per 8 / 16 lanes |
| mask → lane | `nan_where_clear_f64`, `nan_where_clear_f32` | one word per 64 rows plus one store per clear bit |
| witness | `presence_nan_mismatches_f64`, `presence_nan_mismatches_f32` | `popcount(presence XOR derived)` over live rows, no allocation |

`F64Mask8::to_bitmask` was added on the AVX-512, AVX2/AVX, NEON, wasm and
scalar backends (nightly already had it) so the f64 packer reads one
spelling on every arm.

### SQL over a NULL=NaN lane (2026-10-27)

With NULL=NaN the SQL aggregates need no caller clean-up: `COUNT(*)` =
`popcount(filter)`, `COUNT(x)` = `popcount(filter & presence)`, and
`SUM`/`AVG`/`VAR` fold over the same plane, with `n == 0` giving NULL (NaN).
Comparisons are the `{lt,le,gt,ge,eq,ne}_{f64,f32}_to_mask` TRUE planes. NOT
is where IEEE and SQL differ (`!(NaN > 5)` is true, `NOT (NULL > 5)` is
UNKNOWN), so a lowering negates with `mask_not_under(pred, presence)`, where
`presence` is the predicate's presence: the AND of its operands' planes, empty
for a NULL literal. Known differences from PostgreSQL/DuckDB: a stored NaN
value reads back as NULL; GROUP BY and DISTINCT on float keys must key on
presence, since `NaN != NaN`.
4 changes: 4 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,10 @@ required-features = ["std"]
name = "codec8_asm_probe"
required-features = ["std"]

[[example]]
name = "sm9_presence_probe"
required-features = ["std"]

[[example]]
name = "cpu_guard_probe"
required-features = ["std"]
Expand Down
Loading
Loading