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
21 changes: 21 additions & 0 deletions .claude/board/PR_ARC_INVENTORY.md
Original file line number Diff line number Diff line change
@@ -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`.
Expand Down
4 changes: 2 additions & 2 deletions .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -96,5 +96,7 @@ PGHOST=<socket dir> PGPORT=<port> PGUSER=<user> 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.
15 changes: 9 additions & 6 deletions .claude/board/entries/2026-10-21-pg-classview-polyfill-map.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) | — | — |
Expand Down Expand Up @@ -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).
Expand Down
Loading