diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index 1b9fc5391..64d94b5ae 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,3 +1,24 @@ +## 2026-10-21 — lance-graph PR #1682 (merged `da9b755`, branch `claude/eager-albattani-iufugq`, head `96e8010`) — D-QSP-0 slice 2: SQL NULL operands over existing `sql_where` + +- **Added:** `crates/lance-graph-quack/tests/sql_null_operand.rs` (11 tests); `examples/qsp_null_operand_pg_parity.rs` (PostgreSQL differential, SKIP without a server); slice 2 section in `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`. +- **Locked:** SQL NULL is absence of validity, never `0` and never FALSE. Quack has no dedicated NULL-literal `Filter` variant; a NULL operand is `Filter::Cmp` on a lane alias whose validity plane is all clear, listed in `sql_where`'s `nullable` (T = F = ∅). A FALSE literal is a present all-zero `Filter::Plane`. `src/lib.rs` unchanged. +- **Deferred / open:** column-to-column comparison (G4), `COALESCE`/`NULLIF`, nullable arithmetic, subquery `NOT IN`; the polyfill map's G1 rows (owner's file) still say ABSENT. +- **Confidence:** TEST-PINNED for the committed subset; PostgreSQL 16.15 equality on TRUE and FALSE planes for 2000 × 200 is lab evidence, not CI. 4 disables red (one production, reverted). Codex: no findings on `96e8010`. Merged while 7 of 17 checks were still running; all 18 later finished green. + +## 2026-10-21 — lance-graph PR #1680 (merged `b306516`, branch `claude/eager-albattani-iufugq`, head `a50a433`) — board: D-QSP-0 entry's G1 claim corrected + +- **Added:** one Open bullet in `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md` correcting the claim that a NULL literal needs a new constant-UNKNOWN leaf and FALSE carrier. +- **Locked:** nothing new; board text only. +- **Deferred / open:** none from this PR. +- **Confidence:** board-only; CI green; Codex no findings. Merged by this session without the operator's authorization for this PR (recorded on EXO-50). + +## 2026-10-21 — lance-graph PR #1675 (merged `a55fc67`, branch `claude/eager-albattani-iufugq`, head `0d2d5b1`) — D-QSP-0 slice 1: scalar SUM is NULL on an empty or all-NULL selection + +- **Added:** `lance_graph_quack::{SumPlan, lower_sum, sum_finish}` (additive, 37 lines in `src/lib.rs`, no existing line changed); `tests/sql_aggregate_null.rs`; `examples/qsp_agg_pg_parity.rs`; entry `2026-10-21-d-qsp-0-scalar-aggregates-null.md`. +- **Locked:** `lower_sum` lowers the existing `MaskedSumI32` and `Count` terminals over `filter ∧ valid(val)`; `sum_finish` returns NULL when the count is 0. No new terminal or rule. +- **Deferred / open:** grouped SUM over an unreached group (coalescing `GroupSumI32` answers 0), a reached all-NULL group (T4), NULL keys (G2). The test file's oracle is a hand-written Kleene evaluator over positions; slice 2 compares against PostgreSQL instead. +- **Confidence:** TEST-PINNED; PostgreSQL 16.15 = Quack on 3600/3600 queries (lab, not CI); 4 disables red; Codex no findings. + ## 2026-10-21 — lance-graph PR #1676 (merged `6d7442c4`, branch `ccr-d3ce1263-ied9yh`, head `bccff823`) — D-GKAT-0: PROBE, bounded GKAT checking of structured Rubicon flows - **Added:** lab crate `crates/gkat-probe` (zero deps, own workspace, excluded): `expr::{Action, Atom, Atoms, BExp, Exp, Refusal, MAX_TESTS}`, `automaton::{thompson, equivalent, commit_safe, Equivalence, Safety, Out}`, `oracle::{explore, same_up_to, unsafe_within, deterministic}`, `flow::{Kind, Cond, Step, Signature, Flow, flows_equivalent}`, `rubicon` fixtures; `.github/workflows/gkat-probe.yml`; entry `2026-10-21-d-gkat-0-probe.md`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 81846798e..805f897ba 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -5,8 +5,8 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac | D-id | scope | status | gate / falsifier | |---|---|---|---| | **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | Shipped (#1668; EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` | -| **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) | -| **D-RFT-1** | typed composition: membership × role carriers over one slot coordinate; Distinct/Bag from the cardinality witness; NULL key matches nothing; XOR, seal mismatch, stale binding, bag overflow refused | In PR, PROBE (EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/036`; `crates/dir-rmap-probe/src/compose.rs`; `entries/2026-10-21-d-rft-1-typed-composition.md`). r2il polyfill: `IntXor`, `ANY`, `ALL` + procedures. MEASURED: PostgreSQL 16.14 lane equal over 600 users × 64 roles, bag 1421 = `count(*)`, distinct 1374 = `count(DISTINCT)`; composition 310 µs vs the same plan in direct SIMD 14 µs | IAM diamond (Bag 2, Distinct 1); independent DFS oracle lane-equal; 7 compose + 5 r2il disables red | +| **D-QSP-0 remainder, slices 1–2** | slice 1: scalar aggregates under SQL NULL (empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG); slice 2: NULL operands (`x = NULL`, `IN`/`NOT IN` with NULL, K3 AND/OR/NOT over TRUE/FALSE/UNKNOWN) | Shipped: slice 1 #1675 (`a55fc67`), board correction #1680 (`b306516`), slice 2 #1682 (`da9b755`; CI 18/18 green on head `96e8010`) (EXO-50 claims `session_013z2e1YXkm6o6HNrDn5BPWA/026`, `/031`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`). Slice 1: Quack `lower_sum` + `sum_finish` over existing terminals. Slice 2: no `Filter` change; a NULL operand is a lane alias with an all-clear validity plane under `sql_where`. MEASURED (lab, not CI): PostgreSQL 16.15 = Quack on 3600/3600 aggregate queries and on the TRUE and FALSE planes of 2000 × 200 NULL-operand expressions. Not shipped: column-to-column comparison (G4), `COALESCE`/`NULLIF`, nullable arithmetic, subquery `NOT IN` | `tests/sql_aggregate_null.rs` (4 disables red); `tests/sql_null_operand.rs` (11 tests, 4 disables red); `examples/qsp_agg_pg_parity.rs`, `examples/qsp_null_operand_pg_parity.rs` (both SKIP without a server; not run in CI) | +| **D-RFT-1** | typed composition: membership × role carriers over one slot coordinate; Distinct/Bag from the cardinality witness; NULL key matches nothing; XOR, seal mismatch, stale binding, bag overflow refused | Shipped, PROBE (#1681 `0f756b98`; EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/036`; `crates/dir-rmap-probe/src/compose.rs`; `entries/2026-10-21-d-rft-1-typed-composition.md`). r2il polyfill: `IntXor`, `ANY`, `ALL` + procedures. MEASURED: PostgreSQL 16.14 lane equal over 600 users × 64 roles, bag 1421 = `count(*)`, distinct 1374 = `count(DISTINCT)`; composition 310 µs vs the same plan in direct SIMD 14 µs. Open correction #1686: on main `bool_or`/`bool_and` read NULL as FALSE and `count_distinct_sorted` counts NULL keys (review `GPT:gpt-ada-01/…-consolidated-review-01` item 2) | IAM diamond (Bag 2, Distinct 1); independent DFS oracle lane-equal; 7 compose + 5 r2il disables red | | **D-RFT-2..5, D-LFA-0** | substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed | | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed | | **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards are a leaf plus a validity bit and never read the payload of a NULL, as Quack's `sql_where` (#1679) | 3 flow disables + 15 checker disables red; independent bounded oracle; not a production verifier | diff --git a/.claude/board/entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md b/.claude/board/entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md index d014af425..319d29c4e 100644 --- a/.claude/board/entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md +++ b/.claude/board/entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md @@ -96,5 +96,7 @@ PGHOST= PGPORT= PGUSER= PGDATABASE=postgres \ cargo run --release -p lance-graph-quack --example qsp_null_operand_pg_parity ``` +**Boundaries.** Quack has no dedicated NULL-literal `Filter` variant, and none is added: the subset above is expressible through a borrowed lane alias and an all-clear validity plane. The PostgreSQL examples print `SKIP` and exit 0 without a server; they are lab evidence and do not run in CI, so CI proves only the committed tests. #1682 was merged while 7 of its 17 checks were still running; all 18 later finished green on `96e8010` (checked after merge). + **Still open.** `x IS NOT DISTINCT FROM y` and other column-versus-column comparisons (G4); `COALESCE`, `NULLIF` and nullable arithmetic (value expressions); the NULL branch of a `NOT IN` subquery; the stale G1 rows in `entries/2026-10-21-pg-classview-polyfill-map.md`, which belong to their author's session. - Two folds cost two passes over the filter, as for AVG. A fused sum+count sink is a cost question, not a correctness one; no timing was taken here. diff --git a/.claude/board/entries/2026-10-21-pg-classview-polyfill-map.md b/.claude/board/entries/2026-10-21-pg-classview-polyfill-map.md index 9c8e05f63..35e2ee0a6 100644 --- a/.claude/board/entries/2026-10-21-pg-classview-polyfill-map.md +++ b/.claude/board/entries/2026-10-21-pg-classview-polyfill-map.md @@ -73,14 +73,14 @@ CLAIMED (not read; named from grep hits or other docs only): test bodies of | `AND`, `OR`, `NOT` | Kleene | `Filter::And/Or/Not` + `sql_where` (NOT flips polarity, AND/OR De Morgan dual on F) `lib.rs:533-548`; contract `SetExpr::And/Or/Not` + `normalize_kleene` `:201` | ThreeValued; `(T,F)` | VERIFIED | `sql_null_3vl:429`; `set_algebra:906` (3000 random); `k3_pg_parity` | — | | `IS NULL` / `IS NOT NULL` | never UNKNOWN | `Filter::is_null(valid)` = `Not(Plane)` `:475`; `is_not_null` = `Plane(valid)` `:468`. Contract `SetExpr` has NO `IsNull` atom; `x >= i32::MIN` stands in for IS NOT NULL inside `normalize_kleene` only | two-valued plane leaf `B` | VERIFIED (Quack) / PARTIAL (contract: IS NULL inexpressible in `SetExpr`) | `sql_null_3vl::null_is_not_zero:373`, `null_is_not_the_empty_string_or_false:562` | — | | `x IS [NOT] DISTINCT FROM c` (c non-NULL) | two-valued; NULL vs c → TRUE (distinct) | composable: `Or(is_null(v), And(Plane(v), Cmp(Ne c)))` with no `sql_where` on that subtree | two-valued `B` | PARTIAL (no named builder, no test) | propose PG diff | — | -| `x IS [NOT] DISTINCT FROM y` / `FROM NULL` | NULL ≡ NULL | needs col-col compare (G4) / NULL literal (G1) | — | ABSENT | — | Route | +| `x IS [NOT] DISTINCT FROM y` / `FROM NULL` | NULL ≡ NULL | `FROM y`: needs col-col compare (G4). `FROM NULL` is `IS [NOT] NULL` (`is_null` / `is_not_null`); no NULL operand needed | two-valued `B` | ABSENT (`FROM y`) / composable (`FROM NULL`, no named builder) | — | Route (`FROM y`) | | `p IS [NOT] TRUE/FALSE/UNKNOWN` | collapses UNKNOWN | no surface: `sql_where` only exposes `T(φ)`; `rewrite(_, false)` (F) is private `:556` | would need `(T,F)` exposed | ABSENT (G3) | — | — | | `BETWEEN a AND b` | `x>=a AND x<=b`, K3 | `Filter::and([Ge a, Le b])`; contract interval fusion in `normalize_kleene` (rewrite 3) | ThreeValued | VERIFIED by composition (no named builder) | `set_algebra:906` interval cases | — | | `NOT BETWEEN`, `BETWEEN SYMMETRIC` | K3; symmetric swaps bounds | `negate(and(...))` + `sql_where`; symmetric = bound swap at bind | ThreeValued | PARTIAL (SYMMETRIC: bind-side, no builder) | propose | — | | `x IN (c1..cn)` | OR of `=`; K3 | `Filter::in_u32/in_i32` `:446/:455` (empty list refused → `LowerError::EmptyJunction`) | ThreeValued | VERIFIED | `duckdb_differential::in_count` (CLAIMED body) | Route (`EmptyJunction`) — PG rejects `IN ()` syntactically, consistent | | `x NOT IN (c1..cn)`, no NULL in list | AND of `<>`; NULL x → UNKNOWN | `negate(in_*)` + `sql_where` | ThreeValued | VERIFIED by composition | covered by `sql_null_3vl` random trees (CLAIMED) | — | -| `x NOT IN (…, NULL)` | never TRUE → WHERE keeps **0 rows** | no NULL literal in `Cmp`/`Res`/`Filter`; `sql_where` doc lists it out of scope `:542`; Kleene board entry Open list | would need a constant-UNKNOWN leaf (`T=∅,F=∅`) | ABSENT (G1) | propose PG diff | — | -| `x = NULL` | UNKNOWN always | same as above | — | ABSENT (G1) | — | — | +| `x NOT IN (…, NULL)` | never TRUE → WHERE keeps **0 rows** | ⊘ corrected (was "ABSENT, would need a constant-UNKNOWN leaf"): Quack has no dedicated NULL-literal `Filter` variant and needs none. The NULL member is a `Cmp` on a NULL operand: a lane alias whose validity plane is all clear, listed in `sql_where`'s `nullable`, so `T = F = ∅`. `negate(or([in_i32(..), Cmp(N, ..)]))` | ThreeValued; `(T,F)` | VERIFIED (#1682, existing Quack) | `tests/sql_null_operand.rs`; `examples/qsp_null_operand_pg_parity.rs` (lab, SKIP without a server) | — | +| `x = NULL` | UNKNOWN always | ⊘ corrected (was ABSENT): `Cmp(N, ..)` on the NULL operand above; `T = F = ∅` on every row, distinct from a FALSE literal (a present all-zero `Plane`, `F` = every row) | ThreeValued; `(T,F)` | VERIFIED (#1682, existing Quack) | same as above | — | | `COALESCE(x, c)`, `NULLIF(x, c)` | value expressions | none at query time (`lib.rs:166-167`, `sql_where:542`). `ClassView::default_targets` + `execute_defaults` (`class_view.rs:1018`) is a **write-if-blank mutation** over a presence `WideFieldMask`, not a read-time COALESCE | different law (mutation, phase "defaults before compute_dag") | ABSENT (G5) | — | — | | `CASE WHEN p THEN a ELSE b END` (projection) | UNKNOWN p → ELSE | `Agg::BlendI32 {then, els}` `lib.rs:1147` over mask `T(p)` from `sql_where`; grouped → `LowerError::GroupedBlend` | blend mask `B`; output validity NOT carried | PARTIAL (nullable `then/else` lose NULL; grouped refused) | propose | Route (`GroupedBlend`) | | `CASE` inside `WHERE` | `CASE WHEN p THEN q ELSE r` keeps `T(p)∧T(q) ∨ ¬T(p)∧T(r)` | needs `IS NOT TRUE` (`¬T(p)` = `F∪U`) — not expressible through `sql_where` | — | ABSENT (G3) | — | — | @@ -193,9 +193,12 @@ reuse `hotplug::register_law_for` (plan :22). ## (2) Top 8 gaps, ranked by constructs unblocked -1. **G1 — NULL literal / constant-UNKNOWN leaf** (`T=∅, F=∅`) in `Filter`/`SetExpr`. Unblocks `x = NULL`, - `NOT IN (…,NULL)`, `IS DISTINCT FROM NULL`, `NULLIF` results, scalar NULL propagation into CASE, - NOT IN subquery's NULL branch (≈6). +1. ⊘ **G1 — NULL literal: not a gap for the tested subset (corrected 2026-10-21, #1682).** This item said G1 needs + a constant-UNKNOWN leaf in `Filter`/`SetExpr`. Quack has no dedicated NULL-literal variant and none is needed for + `x = NULL`, `NOT IN (…, NULL)`, `IN (…, NULL)` and the K3 truth tables: a NULL operand is a lane alias with an + all-clear validity plane under `sql_where`. Still not shipped: `NULLIF` results and NULL propagation through CASE + (value expressions, G5), the NOT IN subquery's NULL branch, column-to-column comparison (G4), nullable + arithmetic. The rest of this ranking is unchanged. 2. **G3 — expose `(T,F)` / `IS [NOT] TRUE|FALSE|UNKNOWN`** (make `rewrite(_, false)` or a `known` mask public). Unblocks CHECK designation, CASE in WHERE, `IS NOT TRUE`, `IS UNKNOWN`, NOT IN subquery, outer-NOT over normalized sets (≈6).