diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index d53378083..d9bf9ee8a 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,11 @@ +## 2026-10-21 — D-RFT-0 / D-QSP-0: Kleene form of set normalization (in PR) + +- **Contract:** `set_algebra::{Logic, normalize_kleene, normalize_with}` added; `normalize` unchanged (two-valued). `set_rules::SetNormalize` under `Truth::ThreeValued` now applies the Kleene form instead of refusing (its `CATALOGUE` entry has no refusals). Example `k3_pg_parity` (PostgreSQL differential, skips without a server). Entries `entries/2026-10-21-d-rft-0-kleene-normalization.md` and `entries/2026-10-21-d-rft-d-lfa-0-assessment.md` (docs-only D-RFT-1..5 sequence, D-LFA-0 census). + +### Current Contract Inventory — net delta (`set_algebra.rs`, `set_rules.rs`) + +- `set_algebra::Logic { TwoValued, Kleene }`, `normalize_kleene`, `normalize_with` added. No type removed; `normalize`'s output is unchanged. + ## 2026-10-21 — main after #1659 (merged `1c161533`) - **On main:** #1659 (zero-copy joins in mork-pathmap-probe / crepe-plan-probe; ClassView × DR IAM probe; hypothesis-atomization guardrails; coresearch exploration map). Contract inventory: unchanged (lab crates and board only). One FAILED GATE carried: no-pruning arms at n = 50 000. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 81360e227..63761e72f 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,12 @@ +## D-RFT / D-QSP — ClassView × Quack semantic substrate (2026-10-21) + +Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`; docs, not yet on main). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | In PR (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-RFT-1..5, D-LFA-0** | composition, 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-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20) Plan: `.claude/plans/d-relalg-unified-v1.md`. Decisions recorded there: ADMISSION = B, D-RA-2 = A. Acceptance for U1 and U2 is measured row traversals, materializations and total cost with the result set and version semantics unchanged; operator counts alone do not suffice. diff --git a/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md b/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md new file mode 100644 index 000000000..8dca5aee8 --- /dev/null +++ b/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md @@ -0,0 +1,117 @@ +# 2026-10-21 — Co-research: mapping and foresight for D-QSP / D-RFT / D-LFA + +**Status:** EXPLORATION MAP. Nothing in it is adopted; the operator decides. Inputs: five scouts (code, internal prior art, literature, systems, concepts), a 20-row crosswalk, and three co-architects (bridge, firewall and fit, falsifier). Plans: #1667 (`d-qsp-…`, `d-rft-…`, `d-lfa-…`, not on main). Companion entries from the same run: `2026-10-21-pg-classview-polyfill-map.md` and `2026-10-21-eval-egglog-datafrog-ascent.md`. + +## Question + +Which steps in the three plans lack a semantic contract, a named oracle, a named failure mode, or an inside surface by file and line? Which failures will the plans predictably hit, judging by how established systems and the literature solved the same problems? + +## The main finding + +Three outside sources found the same defect independently: **one carrier or one equality used for two strata.** The brief seeded the search terms, so "independently" is weaker than it sounds. + +| Reused for two strata | Where it breaks | +|---|---| +| K3 `=` used as the grouping equality | `GROUP BY`, `DISTINCT` and set operations treat NULLs as one group (`IS NOT DISTINCT FROM`) | +| A mask fold's zero used as the aggregate | An empty or all-NULL `SUM` is NULL in PostgreSQL, not 0 | +| A count carrier under recursion | A cycle keeps itself alive after its last external support is deleted | + +Inside, four conventions carry four strata and share nothing: +- Quack `sql_where`: K3, WHERE only; +- `JoinExec::bag_count`: bag count; +- `Pop`: distinct, 256 slots; +- `set_rules::Population`: a flag that the caller declares rather than computes. + +## Reconciled D-RFT IDs (proposed) + +The plan owns the IDs. Within the plan, the prose wins over the table. The #1668 assessment supplies fixtures and inside surfaces, but never moves an ID. No renumbering is needed. + +Order: 0 (landed) → 1 → {2, 3} → 4 → 5. + +| ID | Contract | Change from today | +|---|---|---| +| D-RFT-0 | `normalize_kleene` keeps the TRUE rows. It applies at the WHERE terminal only, and NOT over its output is refused. | Adds the WHERE-terminal rule. | +| D-RFT-1 | One composition over a shared `JoinDomain` declares its stratum (Distinct or Bag(ℕ)) and its key equality. A NULL key matches nothing. No value-directed foreign gather. | All three documents already agree. | +| D-RFT-2 | The law-licensed rule catalogue. The first new rule is the substitution chain under `Arith`. egglog is an optional offline proof oracle only. | The plan table's "egglog path" becomes a sub-clause. | +| D-RFT-3 | Recursion is Distinct only. The closure equals datafrog's, with one `Iteration` per stratum. The 257th slot is refused. A recursive bag is refused. | Adds the bag refusal and the stratification refusal. | +| D-RFT-4 | Every route gives the same answer, in the Distinct stratum only. Slot generation and binding witness are linked: a rebind invalidates every holder. | The plan table's "think / counterfactual / proposal" row moves to D-LFA-1/2. | +| D-RFT-5 | Replay equals from-scratch. It covers (a) frontier invalidation, with the carrier named per stratum, and (b) thought-git replay from a D-TGB-4 receipt. | Makes the receipt prerequisite explicit. | + +## Exploration map + +### ADOPT-NOW (documentation only; no code) + +| # | Idea | Plan step | +|---|---|---| +| A1 | Adopt the reconciled D-RFT ID table above. This gates any EXO-50 claim of D-RFT-2/4/5. | all D-RFT | +| A2 | Each step declares **stratum / carrier / equality** in the plan text and doc comments. This is a declaration, never a shared type. Promote it to a type only when a failing test shows two crates must exchange it at run time. | all D-QSP, D-RFT | +| A3 | Name a second equality, NotDistinct, used by `GROUP BY`, `DISTINCT`, set operations and recursive `UNION`. It is distinct from K3 `=`. | D-QSP-1/2/4 | +| A4 | `normalize_kleene` is WHERE-terminal. NOT over its result is refused. A (T,F) pair, if ever wanted, is a separate step, because adding it reopens D-RFT-0. | D-RFT-0, D-QSP-0 | +| A5 | `NOT IN`, `NOT EXISTS` and `EXCEPT` are three distinct parity rows. Rewriting one into another is known to be unsound on nullable columns. | D-QSP-2, D-RFT-1 | +| A6 | Recursive strata are Distinct only, unless a convergence proof exists. A recursion limit is a typed refusal, never a truncated answer. | D-RFT-3, D-QSP-4 | +| A7 | DuckDB is never a second correctness oracle. It is compared only on the shared stratum, after a declared dialect-normalization list. A PostgreSQL error is a typed refusal. | D-QSP-3/5 | +| A8 | Four "commit" events stay distinct: Rubicon intention, `KanbanColumn::Commit`, MUL authorization and the seal. Verbs permitted per column form a relation, which does not exist yet. `WaitForInput` is an external pause, not deliberation (this corrects #1668's assessment). | D-LFA-1/2 | + +### PROBE (named, pre-registered, unrun) + +All probes compare counts or scalar folds. + +| Probe | Tests | Kill condition | +|---|---|---| +| P-NOTIN-TRIPLE | R={1,NULL}, S={NULL}: `NOT IN` 0, `NOT EXISTS` 2, `EXCEPT` 1 | PostgreSQL disagrees with 0/2/1 | +| P-NULLGROUP | NULL keys form one group under NotDistinct | PostgreSQL splits them | +| P-EMPTYSUM | Empty or all-NULL `SUM` is NULL. Ungrouped empty input gives 1 row; grouped empty input gives 0 rows. Real-zero `SUM` stays 0. | A real zero comes out NULL (over-correction) | +| P-EXCEPTALL | Multiplicity is max(m−n, 0). On a Boolean route the answer is a semantic refusal. | `EXCEPT ALL` is admitted without a count carrier | +| P-KLEENE-NOT | `NOT(normalize_kleene(x<5 AND NOT x<5))` on {3, NULL} keeps 2 rows; PostgreSQL keeps 1 | The composition is not refused | +| P-MUTUAL-SUPPORT | Two facts support each other. Delete the external seed and both clear. The twin with a second seed keeps both. | `Pop::repair` gives 0. That would contradict the predicted defect; the prediction is a conjecture. **Run first.** | +| P-BAGREC-CYCLE | A recursive bag over a cycle is refused; the Distinct arm equals the closure | A count is returned | +| P-STRAT-NEG | `A←¬B, B←¬A` is refused | It is accepted. Check that PostgreSQL rejects it before relying on it. | +| P-STALE-RESUME | A source moved, or interrupts were reordered, and resume refuses | Resume answers | +| P-ABA-MODDEL | Modify on one side and delete on the other is a named refusal | It resolves silently | +| P-REFUSAL-KIND | A RouteRefusal is retried on another route. A SemanticRefusal is never retried. | A semantic refusal is retried | +| P-TLP-COUNT | The counts for P, NOT P and P IS NULL sum to the table's row count | The sum differs | + +Bridge findings worth a probe: +- `JoinExec::bag_count` sums `u64` without an overflow check (`mork-pathmap-probe/src/join.rs:653-659`). The contract should be exact below a stated row bound and refused above it. +- Grouping NULL keys can reuse the `(Col, Mask)` validity operand that `sql_where` already takes. No new carrier type is needed. + +### PARK + +- A ℤ-diff bag frontier (differential-dataflow shaped). Nothing implements it; drop it from the strata list until a consumer needs it. +- Semiring provenance polynomials (ℕ[X], Why(X)). They are an analysis lens only and must never be stored. They also collide with the 32-source cap. +- A (T,F)-pair `normalize_kleene` for CHECK constraints (D = {T, U}). +- sqllogictest as the case format. It is usable only with `rowsort` and a multiplicity check, never `valuesort`. + +### SKIP + +- A differential-dataflow engine. +- Dolt / lakeFS three-way merge vocabulary. Thought-git has one writer. +- LangGraph as the stale-resume oracle. It does not refuse a stale resume. +- NARS revision as a semiring or lattice merge. It is not idempotent. +- One merged provenance type: lineage, replay receipt and EpistemicState5 stay separate. + +## Anchors the council found at risk + +- **Quack `Filter::Semijoin` is a value-directed foreign gather** (`lance-graph-quack/src/lib.rs:152, 366-391`, lowering to `MaskOp::Gather`). ADMISSION B lists it as pending call-site classification. No `NOT IN`, `EXCEPT` or anti-join lowering may build on it until that classification lands. +- **Oracle scope.** `CLAUDE.md` already rules that answers are compared by folds, "for tests and oracles too". So every oracle inside the workspace is bound. Some existing oracles walk decoded rows: + - `k3_pg_parity`'s Kleene reference evaluator; + - the K3 unit tests in `set_algebra` / `set_rules`; + - `join_probe.rs`; + - `walk_mask.rs:361-372`. + + Only external processes (a PostgreSQL server, Soufflé) remain genuinely open. +- **D-LFA work before a pause.** `graph-flow` re-runs a node from its start on resume. Any Task that does work before a pause point conflicts with A6/A10 unless that work is pure compute. + +## Open (operator) + +1. Does "oracles compare by folds" admit a reference engine that holds tuples internally, if the comparison itself is fold against fold? This decides datafrog's role and the reference evaluators listed above. +2. Adopt the reconciled D-RFT table (A1) before anyone claims D-RFT-2/4/5 on EXO-50? +3. Who classifies `Semijoin` under ADMISSION B? + +## Not searched + +- The `Pop` tile body was not read in full; whether a tile carries counts is CLAIMED. +- The z8run-lance stale predicate is not on disk. +- From the systems scout: the original sqllogictest page, the lakeFS documentation, and the Roaring bitmaps papers. +- Primary sources not obtained: the Gupta–Mumick–Subrahmanian (1993) original and the Geerts–Poggi m-semiring papers. +- No probe was run. diff --git a/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md b/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md new file mode 100644 index 000000000..2533e7376 --- /dev/null +++ b/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md @@ -0,0 +1,70 @@ +# 2026-10-21 — D-RFT-0 / D-QSP-0: set normalization under SQL NULL (Kleene form) + +**Status:** MEASURED, TEST-PINNED. Plans: D-RFT-0 and D-QSP-0 in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`; not yet on main). Claim: EXO-50 `session_01G22yT6htkcdyXsihxxXdrg/031`. + +## The defect + +`contract::set_algebra::normalize` is two-valued. Two of its rewrites assume a row is either in a set or in its complement: + +- a union that covers a whole lane becomes `All`. This covers interval unions, `x≠a ∨ x≠b`, `x≠a ∨ (interval ∋ a)`, and on `U32` lanes `≠a ∨ ≠b` and `≠a ∨ =a`; +- a conjunct whose interval covers the whole lane is dropped. + +On a NULL row both turn UNKNOWN into TRUE. PostgreSQL 16.14: `SELECT count(*) FROM (VALUES (1),(NULL)) v(x) WHERE x<5 OR x>=5` is 1, but `All` is 2. + +Because of this, `set_rules::SetNormalize` refused every rewrite under `Truth::ThreeValued`. That refusal was correct but blanket: it also gave up De Morgan, flattening, absorption and interval fusion, all of which keep the TRUE rows. + +Not affected: +- Quack `Filter::sql_where`, whose T/F polarity encoding is correct and is pinned by `tests/sql_null_3vl.rs`; +- relalg, whose lanes carry no NULL (its two-valued `normalize` is unchanged; 8 suites pass). + +## The fix (precise, not blanket) + +`normalize_kleene(e)` (and `normalize_with(e, Logic::{TwoValued, Kleene})`) runs the same rewrites with the lane-cover cases replaced: + +- a covered `I32` lane becomes `x >= i32::MIN`, which is TRUE exactly on the non-NULL rows. No new vocabulary is needed; it is an existing `Res`; +- a covered `U32` lane keeps its atoms, because no single `U32` atom is TRUE exactly on non-NULL rows; +- the whole-lane atom is emitted only where no `!=` already names the lane. Every `!=` is FALSE on NULL rows anyway, so the atom would be redundant. This keeps the leaf count from growing. + +Why the rest is sound: De Morgan and the negated comparison are Kleene equivalences. After negation normal form no negation sits above a junction, so any rewrite that keeps a subterm's TRUE rows keeps the whole expression's TRUE rows (e.g. `p ∧ ¬p → Empty`). A `Sym` is two-valued by contract, so its complement rule stays. + +`SetNormalize` under `ThreeValued` now applies the Kleene form. Its catalogue entry has no refusals. The `Complement` and `RelationalDifference` guards are unchanged and still refuse under `ThreeValued`. + +## Evidence + +| what | result | +|---|---| +| contract `set_algebra`: Kleene evaluator, 3000 random expressions with NULL lanes | TRUE rows identical, idempotent; > half rewritten; two-valued form wrong on > 30 of the same inputs | +| contract `set_algebra`: the six lane covers one at a time, rows `[3, NULL]` | Kleene keeps 1 row in 2; two-valued keeps both | +| contract `set_rules`: 600 random measures over NULL tables, all rules, three-valued | answer = Kleene oracle; `SetNormalize` fired > 300 times; two-valued normalization alone wrong on > 5 | +| example `k3_pg_parity`, PostgreSQL 16.14, 2000 expressions × 200 rows | as written = Kleene oracle = `normalize_kleene` on 2000/2000 (1537 rewritten); two-valued `normalize` wrong on 474 | +| contract suite | 1549 + 1 passed; clippy `-D warnings` clean (Rust 1.99.0) | + +Disable runs, each red on its named test: +- D1 (I32 cover → `All`): 3 red; +- D2 (no whole-lane atom): 4 red; +- D3 (U32 cover → `All`): 2 red; +- D4 (`SetNormalize` uses the two-valued form): 2 red; +- D5 (whole-lane atom also beside `!=`): green at first, a size guard only. Pinned by `normalize_kleene_never_grows_leaf_count`, then red. + +Re-pinned: `experiment_e_null_refuses_set_normalization` → `experiment_e_null_normalizes_in_the_kleene_form` (rewrite applied, count 2 kept). The complement experiment now isolates `Complement` with `rewrite_with`. + +## Reproduce + +```text +cargo +1.99.0 test --release -p lance-graph-contract --lib set_ +PGHOST= PGPORT= PGUSER= PGDATABASE=postgres \ + cargo +1.99.0 run --release -p lance-graph-contract --example k3_pg_parity +``` + +Without a server the example prints `SKIP` and exits 0. + +## Open + +- **`Sym` is assumed two-valued** under `Truth::ThreeValued`. A consumer that binds a `Sym` to a nullable predicate must not take this path. That is a contract statement, not a check. +- **Out of scope (D-QSP-0 remainder):** + - a NULL literal (`x = NULL`, `NOT IN (…, NULL)`); + - `COALESCE` / `NULLIF`; + - nullable arithmetic; + - empty / all-NULL `SUM` (the `SumFamily::Sym` path exists; no PostgreSQL differential yet); + - `COUNT(expr)` vs `COUNT(*)`. +- **Not done:** a PostgreSQL arm in CI. The example is a lab instrument only. diff --git a/.claude/board/entries/2026-10-21-d-rft-d-lfa-0-assessment.md b/.claude/board/entries/2026-10-21-d-rft-d-lfa-0-assessment.md new file mode 100644 index 000000000..690dd7c26 --- /dev/null +++ b/.claude/board/entries/2026-10-21-d-rft-d-lfa-0-assessment.md @@ -0,0 +1,81 @@ +# 2026-10-21 — D-RFT-1..5 sequence, D-LFA-0 census, physical-shape proof plan + +**Status:** PROPOSAL, documentation only. Nothing here is measured or admitted. Plans: #1667 (`d-rft-…`, `d-lfa-…`, `d-qsp-…`; not on main). The IDs below are #1667's; no new D-ids are minted. Sources: four read-only scout maps (relalg / Quack / R2IL / `mork-pathmap-probe::join` / `dir-rmap-probe::pop`; thought-git-probe / ACT-R / kanban / `cycle_driver`; rs-graph-llm `graph-flow` + `graph-flow-lance`). Each claim names the file it rests on. + +## D-RFT-1..5: the smallest falsifiable sequence + +The kickoff's six asks map onto #1667's five IDs as follows (asks in brackets). + +| # | ask | existing parts (verified) | missing | falsifier | +|---|---|---|---|---| +| D-RFT-1 | [1] typed composition without foreign gather | Quack `Filter::Semijoin` (EXISTS, distinct, `Gather` over a resident foreign plane; NULL fk → FALSE); `mork-pathmap-probe` `JoinDomain` + `JoinExec::bag_count` (`Σ_y Π |side_i at y|`, no enumeration); `dir-rmap-probe::Pop` (distinct, witness-bound, 256-slot register) | one composition `R ∘ S` over a shared domain that declares its law (Distinct / Bag) and NULL key handling, and answers both with the same coordinates. Today the three live in three crates with three conventions | IAM diamond (u ∈ g1, g2; both grant r): Distinct = 1, Bag = 2, XOR = 0 must be refused as a law; a NULL key matches nothing. PostgreSQL arm: `count(*)` vs `count(DISTINCT …)` over the same join (reuse `k3_pg_parity`'s pattern) | +| D-RFT-2 | [2] substitution through numeric method coordinates | `set_rules::Arith` guards (Exact / Wrapping / Checked / IEEE) already refuse rewrites that change overflow or rounding | a rule `a = k·b, b = m·c ⇒ a = k·m·c` in the same catalogue, guarded by `Arith` | substitution fixture `a=2b, b=2c, z=2a ⇒ z=8c` holds under Exact; refused under Checked (overflow at the boundary) and IEEE; an e-graph is not needed for this step | +| D-RFT-3 | [6] datafrog parity, bounded recursion | `dir-rmap-probe` Warshall closure in a 256 tile (refuses > 256); D-TGB-10 keeps recursion on `datafrog` | a bounded-recursion fixture run by both, same answers and the same stop | nested groups with a cycle and a diamond: closure equal to `datafrog`; the 257th group refused, never truncated | +| D-RFT-4 | [3] a 64-thought frontier sharing versioned bindings | `thought-git-probe::SlotPool` (63 live slots + givens; generation-checked `Slot`, `Stale`); `Pop` witness (`Refusal::Stale`) | slot generation and binding witness are two separate staleness checks with no link | 63 thoughts each hold a population over ONE register version. A rebind invalidates all 63 at once; a freed slot's handle is `Stale`. Disable: drop the witness check → a stale population answers | +| D-RFT-5 | [4] replay after changed premises, [5] multi-support deletion | `oracle::next_version` (from-scratch), `Pop::repair` (re-derives, never clears; second path kept, test-pinned in #1666) | repair as a thought-git verb checked against `next_version` | add / delete / cycle / diamond / ABA: incremental = from-scratch on every fixture. CausalEdge64 59..63 (EpistemicState5) is not touched and not used as scratch | + +Order: 1 → 2 and 3 in parallel → 4 → 5. D-RFT-0 (K3) is the prerequisite and is the implementation PR this entry ships with. + +Not assumed: NARS revision as a semiring. Epistemic certification (59..63), causal provenance (receipt, D-TGB-4) and hypothetical results (live slots) stay three separate things. + +## D-LFA-0: copy-versus-reuse census (rs-graph-llm → `lance-graph-flow`) + +| part | where | verdict | why | +|---|---|---|---| +| `Task`, `TaskResult`, `NextAction{Continue, ContinueAndExecute, GoTo, GoBack, End, WaitForInput}` | `graph-flow/src/task.rs` | REUSE | the step vocabulary; no state of its own | +| `GraphBuilder`, `Graph::execute_session`, `ExecutionStatus{Paused, WaitingForInput, Completed, Error}` | `graph.rs` | REUSE | it does not call storage itself (`graph.rs:121`) | +| `FlowRunner::run` (load → execute → save) | `runner.rs:378-393` | REUSE as a driver | it is a driver, not the write owner | +| `Context` = `DashMap` + chat history | `context.rs:390-394` | REUSE, handles only | `graph-flow-lance` already enforces that the only data key is `MATERIALIZED_KEY` | +| `SessionStorage{save, get, delete}` (InMemory, Postgres, Kanban, Surreal) | `storage*.rs` | REUSE the trait; DO NOT reuse `KanbanSessionStorage::{moves, replay}` as truth | a second replay store would compete with the thought-git receipt (D-TGB-4) | +| `LanceTask{source, filter, measure, rotate, execute, materialize}` | `graph-flow-lance/src/tasks.rs` | COPY the pattern | the crate path-depends on z8run checkouts that lance-graph does not have | +| `Envelope{handle, generation, source}`, fail closed on a newer source generation | `z8run-lance` via `graph-flow-lance/src/lib.rs:12-29` | REUSE the rule | the same witness discipline as `Pop` / `Qr` | + +**Rubicon mapping** (`kanban.rs:102-110`: Planning → {CognitiveWork, Prune}; CognitiveWork → Evaluation; Evaluation → {Commit, Plan, Prune}; Plan → Planning): +- *think*: `CognitiveWork`; +- *counterfactual*: an `Evaluation → Plan → Planning` loop over a live slot; +- *do*: `Evaluation → Commit`. + +Four things stay distinct: +- *commitment*: crossing into `CognitiveWork`; +- *proposal*: a `KanbanMove` cast into the supervisor's `BatchWriter`; +- *authorization*: the MUL gate in `cycle_driver::shade_owner` / `run_cognitive_work_gated`; +- *persistence*: `seal_cycle` → one `DatasetVersion`. + +A flow's `End` never writes. + +**API sketch** (not a frozen ABI; no third executor): + +```text +lance-graph-flow + task per ClassView method ordinal → LanceTask-shaped plan handle in Context + NextAction::WaitForInput = deliberation before the Rubicon + ProposeTask (terminal) → KanbanMove intent to BatchWriter; returns a handle + resume → Envelope generation checked; stale → Error, no answer +``` + +**Falsifier proposal:** a flow that ends with a `Commit` proposal leaves the Lance dataset version unchanged until `cycle_driver` seals it. Resuming after the source generation moved fails closed. Disable: let the task write directly → the version moves before the seal. + +## Physical-shape proof plan (unmeasured) + +Fixture: #1666's `dir-rmap-probe` (65k users, 254 security groups). Shapes: +- direct ordinal (`KEEP_DIRECT`); +- sparse runs (`Runs`); +- DR32×128 (512 B); +- DR64×64 (512 B); +- DR256×256 (8 KiB). + +Equal answers are required, including: +- snapshot invalidation (`Stale`); +- the 257th coordinate (`TooLarge`); +- nesting and cycles; +- independent support paths (repair keeps the second path). + +Costs are measured and reported separately: cold bind, first touch, repeated fold, cache, prepare, prefetch, invalidation and materialization. A millisecond stage is reported as FAILED GATE, never hidden in an amortized per-user number. A faster shape that changes one answer is rejected. Known from #1666: the prepare stage is millisecond-scale (FAILED GATE); with GUID-ordered positions a team focus touches 69 of 254 tiles, so tile locality needs a Dn128 ordering first. + +## Open + +- **Owners:** + - D-RFT-1..5 and D-LFA-1..3 are unclaimed; + - EXO-119 (positional lens) and EXO-114 (order witness) are unassigned; + - ADMISSION B still forbids value-directed foreign gather at PREPARE. Whether Quack's `Semijoin` `Gather` over a resident plane counts is not decided here. +- **egglog:** only an offline proof candidate (#1667). Not needed for D-RFT-2's first step. diff --git a/.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md b/.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md new file mode 100644 index 000000000..1169ee8cd --- /dev/null +++ b/.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md @@ -0,0 +1,292 @@ +# egglog, datafrog and Ascent as complements to `lance-graph-relalg` — evaluation (2026-10-21) + +**Status:** OPEN. This is an exploration map, not a ratification. Nothing in it is measured, and no code was written. The scope is a complement to `lance-graph-relalg`; replacing it is not on the table. + +**Evidence grades.** Claims about our own tree are marked `VERIFIED-IN-CODE`, with `file:line`. Claims from outside use these grades: + +- **READ-IN-FULL:** read completely. +- **SECTION-READ:** the named sections were read. +- **ABSTRACT-ONLY:** only the abstract was read. +- **SECONDHAND:** taken from a summary or a third party. + +Three sources gave the outside evidence: +- the source trees of the three AdaWorldAPI forks; +- the text of the CC'22 Ascent paper; +- the text of the PLDI'23 egglog paper (arXiv 2304.04332). + +The OOPSLA'23 BYODS paper was **not read**: the ACM DL returned HTTP 403. Every BYODS claim below therefore rests on the fork's `BYODS.MD` (READ-IN-FULL) and its trait sources. + +## 0. What relalg is today (the thing being complemented) + +- **The IR.** `Rel` is `All`, `Empty`, `Plane`, `Atom`, `And`, `Or` or `Not` over ONE table. It holds no strings and no rows (`crates/lance-graph-relalg/src/ir.rs:46-62`). `Measure` is `Count`, `Sum`, `Min`, `Max` or `Keep` (`ir.rs:98-110`). VERIFIED-IN-CODE. +- **Normalization.** `normalize` converts to the contract's `SetExpr` and delegates to `set_algebra::normalize` (`src/normalize.rs:23-25`). `symbolic` asks `set_rules::rewrite` under `Semantics::exact(n_rows)` whether the measure folds to a constant (`normalize.rs:40-58`). VERIFIED-IN-CODE. +- **Lowering.** Lowering emits R2IL calls over `FoldDialect`, giving one mask-risc program per fold (`src/lower.rs:104-149`). `lower_rel` never loops over rows (`lower.rs:178-194`). VERIFIED-IN-CODE. +- **`set_rules`.** + - It has 8 guarded rules (`lance-graph-contract/src/set_rules.rs:236-310`). + - `Semantics` carries `{universe, arith, truth, sums, population}` (`:74-81`). + - The driver accepts only a strict decrease in size (`:379`). + - `SetNormalize` uses `normalize_kleene` under `Truth::ThreeValued` (`:444-447`). + - The independent oracle is a test-only Kleene evaluator over a materialized table (`:616-768`). + + All VERIFIED-IN-CODE. +- **Not built.** Joins (D-RA-3/4) and recursion (`μ`, D-MTP-3) do not exist. `join_body::is_alpha_acyclic` only classifies the shape of a join body (`src/join_body.rs:21`). VERIFIED-IN-CODE. This is the gap a complement could cover. +- **Prior rulings that bind this evaluation:** + - **X14 (egglog).** egglog is SKIP as a bind- or query-time planner. It is allowed only for offline normal-form generation (`entries/2026-10-21-coresearch-classview-algebra-polyfill.md:127-130`). + - **datafrog is a SET oracle.** `entries/2026-10-16-coresearch-wcoj-leapfrog.md:83-84`. + - **D-CMR-8.** Equality saturation is "justified only if a bounded local rewriter measurably commits to worse forms" (`plans/d-cmr-concept-chain-normalization-v1.md:174-177, 220`). + - **D-RFT-2.** egglog may be only an offline proof or normal-form oracle (`lg-1667/.claude/plans/d-rft-…-v1.md:18`). + - **D-RFT-3.** datafrog is the recursion reference (`:19`). NARS revision is not presumed to be a semiring. + - **D-TGB-10.** The folded rules are checked against datafrog, and recursion stays on datafrog until D-MTP-3 (`plans/thought-git-basics-v1.md:247-248, 168`). + - **CLAUDE.md P0 (2026-10-21).** No millisecond results. No tuple decoding, *including in oracles*: answers are compared by folds. mask-risc is the reference fold algebra. Use AdaWorldAPI forks only. + +## 1. Fork status, licence, build cost + +| | fork / checkout | version | licence | form | dependency weight | already used in the tree | +|---|---|---|---|---|---|---| +| **datafrog** | AdaWorldAPI/datafrog (`~/.cargo/git/checkouts/datafrog-…/edd7cfc`) | 2.0.1 | Apache-2.0/MIT (`Cargo.toml`) | plain runtime library, about 2 kLOC, **zero dependencies** (dev: proptest) | negligible | dev-dependency of `lance-graph-metta` (`Cargo.toml:20`) and `crepe-plan-probe` (`Cargo.toml:44`) | +| **Ascent** | AdaWorldAPI/ascent (`~/.cargo/git/checkouts/ascent-…/f3634e3`, fork PR #1, edition 2024, toolchain 1.99.0) | 0.8.1 | MIT | **proc macro** (`ascent!`, `ascent_run!`, `ascent_par!`) plus runtime | runtime: hashbrown, rustc-hash, boxcar, cfg-if; the default feature `par` adds dashmap and rayon. Macro: syn, quote, itertools, **petgraph 0.8**, derive-syn-parse | dev-dependency of `crepe-plan-probe` (`Cargo.toml:46`), the second oracle in `examples/walk_mask.rs:92-151` | +| **egglog** | AdaWorldAPI/egglog (`(AdaWorldAPI fork) egglog`, origin AdaWorldAPI/egglog, HEAD `4b5686b`) | 3.0.0 | MIT | runtime library plus a CLI (default feature `bin`) | **heavy**: 8 workspace crates; core-relations brings crossbeam, dashmap, bumpalo, rand, num, fixedbitset; the main crate brings im-rc, indexmap, csv, serde_json, egraph-serialize, ordered-float. Toolchain pin is **1.91.0** against the workspace's 1.99 | not a dependency anywhere | + +Licences: all three are permissive. Code is borrowed from none of them; only concepts are, as below. + +**AdaWorldAPI forks: all three exist**, so the forks-only P0 rule can be satisfied. Each must be wired by `git` or `path` with `branch = "master"`, never from crates.io. + +## 2. What each engine actually does (first-hand) + +### datafrog + +**Data model.** +- `Relation { pub elements: Vec }` holds a sorted, deduplicated `Vec` (`relation.rs:15-17`). `from_vec` sorts and then deduplicates (`:78-80`). It is a **set of owned tuples**. READ-IN-FULL. +- `Variable` keeps `stable`, `recent` and `to_add` relations. `changed()` merges these and, for a distinct variable, removes tuples already in `stable` using a gallop (`variable.rs:339-395`). This is semi-naive evaluation driven by the caller's `while iteration.changed()` loop (`iteration.rs`). READ-IN-FULL. +- `variable_indistinct` exists. It is documented as having *no termination guarantee*, so it does not support bag semantics. + +**Operators.** +- `from_join` (sort-merge join on key; `join.rs:12-137`, `gallop` at `:137`). +- `from_antijoin`, whose **right input must be a fixed `Relation`** (`variable.rs:194-201`). Negation is therefore expressible only against a stratum the caller has already completed; the caller stratifies by hand. +- `from_map`. +- `from_leapjoin`: one dynamic source plus fixed `Leapers` (`extend_with` / `extend_anti` / `filter_*`). The smallest proposer proposes and the others intersect (`treefrog.rs:6-45`). The result is collected into a `Vec` and turned into a `Relation`. + +**Not present:** aggregation, lattices, NULL, multiplicities. + +### Ascent + +**Evaluation** (CC'22 §4, SECTION-READ): +- the rule dependence graph is split into SCCs, evaluated in topological order; +- each dynamic relation is split into delta, total and new for semi-naive evaluation; +- indices are selected from the join columns; +- rules compile to **nested loops over hash indices, binding one tuple at a time** (the paper's generated-code listing for `tc`); +- clauses may be reordered when grounding allows. + +**Storage.** The default provider stores a relation as `Vec<$field_types>`, plus index fields (`ascent/src/rel.rs` macro `rel!`). READ (the macro). + +**Lattices** (CC'22 §3.1, SECTION-READ; trait `ascent_base/src/lattice.rs:17-41`): +- In a `lattice` relation, the last column must implement `Lattice` (`meet`/`join`). +- Its meaning is a partial map from the non-lattice columns to the lattice column. Conflicting facts are joined. +- **Correctness presumes a true join-semilattice:** idempotent, commutative and associative. +- `Dual` flips the order, which is how shortest paths are written. + +**Negation and aggregation.** +- Stratified negation and aggregation are built in. +- Aggregators are library functions: `sum`, `min`, `max`, `count`, `mean`, plus user-defined ones (README; CC'22 §3.2). +- Aggregation runs over the set of matching tuples. + +**BYODS** (`BYODS.MD` READ-IN-FULL; `ascent/src/rel_index_read.rs:11-30`): +- A relation can be backed by a provider: `#[ds(provider)]` macros `rel_ind_common!` / `rel_ind!`. +- A provider implements `RelIndexRead::index_get(key) -> Option>`, `RelIndexReadAll::iter_all`, `RelIndexWrite` and `RelIndexMerge`. +- **Only the storage and the index are replaced.** The rule body is still Ascent's generated nested-loop join, which binds per value and writes head tuples one at a time. + +**Parallelism.** `ascent_par!` runs on rayon. + +### egglog + +Paper: PLDI'23 §1 and §3-4 SECTION-READ. Source tree read in part. + +**Model.** Datalog over functions with a functional dependency, plus a union-find, rebuilding (congruence) and extraction. + +**`:merge` resolves conflicting outputs.** The source states that it "must be monotonic … must define a lattice … If values are merged in different orders, they should still result in the same output" (`src/ast/mod.rs:742-748`; the paper's lines on `:merge` and lattices). + +**Rule bodies have no negation.** `GenericFact` is only `Eq | Fact` (`egglog-ast/src/generic_ast.rs:35-38`). READ. + +**Rewrites.** `rewrite` / `birewrite` take `:when` guards and `:subsume` (`src/ast/mod.rs:845-891`). + +**Schedules.** Rulesets run under `saturate`, `repeat` or `seq` (`:383-386`). + +**Proofs.** There is a `prove` command (`:944`) and a term encoding with proof tracking (`src/proofs/`, `proof_encoding.md` read §1). + +**Extraction.** Extraction uses a default or custom cost model (`src/lib.md`, READ-IN-FULL). + +**Other sorts.** A `multiset` sort exists as a *value* sort (`src/sort/multiset.rs`, existence only). Relations themselves are sets. + +**Semantics.** egglog is defined by an inflationary immediate-consequence operator. Semi-naive evaluation is proven equivalent (Theorem 4.1). Non-monotone `:merge` is allowed but its result is order-dependent (paper §4). + +### Shared property that decides role (c) + +**All three materialize owned tuples:** +- datafrog keeps `Vec` in every `Relation` and `Variable`; +- Ascent keeps `Vec` plus index maps, and emits head tuples per binding even under BYODS; +- egglog keeps tables of rows and e-classes. + +Under the P0 rule a tuple violates four things: zero copy, folding, natural order and time. All three engines therefore fall outside the substrate's runtime by construction. That is a property of each engine's data model, not a tuning matter. + +## 3. Per-stratum semantics + +| stratum | datafrog | Ascent | egglog | the substrate today | +|---|---|---|---|---| +| **Boolean / Distinct** | yes: sets by construction | yes: set union for relations (CC'22 §3.1) | yes: unit-valued functions | yes: masks; `Population::Distinct` | +| **Bag / ℕ** | **no.** `from_vec` dedups; `variable_indistinct` gives up termination. A bag needs an explicit multiplicity or witness column (the X17 proposal) | **not natively.** `count`/`sum` aggregate over a *set* of tuples, so a bag needs a witness column too; Σ multiplicity is then expressible with `agg sum` | **no** for relations. `multiset` is a value sort, not relation semantics | partly: `Population::Bag` refusals (`set_rules.rs:463-466, 580-582, 596-598`); join fan-out is not built | +| **K3 NULL** | no | no native support. It could be encoded with `Option` or a 3-element lattice, but the information order and the truth order differ, which invites error | no | **already has an independent oracle:** the Kleene `set_at` evaluator (`set_rules.rs:633-675`) and `normalize_kleene`. None of the three engines adds anything here | +| **Recursion + stratified negation** | **yes, by hand:** antijoin against a completed `Relation`; the caller orders the strata | **yes, built in:** SCC strata, with negation and aggregation across strata | **no negation** in bodies | not built (D-MTP-3); the `walk_mask` lab shows the mask form `new &= !walk; walk |= new` | +| **Lattice-valued** (min-plus, intervals) | no | **yes:** `lattice` plus `Dual` gives shortest paths directly (CC'22 §3.1) | **yes:** `:merge (min old new)` (`tests/interval.egg` style) | min-plus: OPEN (probe P2 in the polyfill entry) | +| **NARS truth (revision)** | n/a | **disqualified while revision is not idempotent.** A lattice join requires `x ⊔ x = x`. Revising the same evidence twice raises confidence, which is exactly the "duplicate proof becomes new evidence" error D-RFT-5 forbids | **same:** `:merge` must be order-independent and monotone; otherwise behaviour is undefined (`ast/mod.rs:742-748`) | NARS is a finisher only (D-CMH-1); the semiring claim is OPEN (P6) | + +Consequence for NARS: neither engine can be the evaluator or the oracle for revision. Their own documented preconditions are the same question probe P6 already asks (associativity, commutativity, idempotence on a quantized grid). A property test answers it, and no engine is needed for that. + +## 4. Role by role + +### Role (a) — offline proof / normal-form generator for `set_rules` + +**egglog fits this role, and only egglog does.** It has: +- guarded rewrites (`:when`); +- per-stratum rulesets: one ruleset per `Semantics` stratum, e.g. a two-valued Boolean algebra ruleset and a Kleene ruleset that leaves out complement and excluded-middle; +- `saturate` schedules; +- cost-based extraction; +- `prove`. + +The prior ruling (X14) and D-CMR-8 fix how it may be used: **offline, against a closed enumeration of small terms, never on a bind or query path, and never as a dependency of `lance-graph-contract` or relalg.** Its output is evidence about the catalogue. That output can be: +- a counterexample showing the local rewriter commits to a larger form; +- a proof that an admitted rule follows from the stratum's axioms; +- a missed rule that is a *candidate* for the catalogue, admitted only through the normal `set_rules` path with its guard and the Kleene oracle. + +It is never a rule source in its own right. + +- **datafrog: SKIP.** It has no equality, no union-find and no rewriting. +- **Ascent: SKIP.** It has no congruence closure. The BYODS `eqrel` provider gives an equivalence relation but not congruence or extraction. egglog is the purpose-built tool, and duplicating it in Ascent buys nothing. + +### Role (b) — independent test oracle for D-RFT-3 recursion and D-TGB-10 + +- **datafrog stays the SET oracle.** + - It is already designated (D-TGB-10, D-RFT-3, the WCOJ map) and already a dev-dependency in two crates. + - It has zero dependencies and fits monotone closure and leapjoin. + - It covers Boolean/Distinct recursion. Stratified negation is possible against completed strata. + - The one change the 2026-10-21 P0 rule forces is in **how the comparison is made**, not in the engine. Current probes compare tuples: + - `lance-graph-metta/examples/join_probe.rs:14` compares sorted pair vectors; + - `crepe-plan-probe/examples/walk_mask.rs:361-372` compares `BTreeSet`s, decoded from the mask planes; + - `walk_mask` also prints an "ascent ms" column (`:399`), which is a no-ms violation as written. + - The rule demands fold against fold. The substrate side produces terminals only (`Count`, plus a fold such as `Sum` over an id-hash lane, or several independent hash lanes). The oracle side computes the same folds over its own result relation. The substrate never decodes a row. +- **Ascent: a second oracle, only for strata datafrog cannot express without hand work.** These are: + - **aggregation inside recursion**, e.g. "count landed facts per source" (D-TGB-8); + - **stratified negation with automatic stratification**, e.g. "branches with no anomaly"; + - **min-plus lattices**: `Dual` shortest path is the natural oracle for P2 (hop distance from iterated Boolean frontier masks). + + datafrog can reach the first two only by hand-ordered antijoins plus external counting, and the third only by enumerating every bounded length. +- **egglog: SKIP.** It has no negation and no aggregation, and its relations are sets. Nothing in D-RFT-3 or D-TGB-10 needs equality saturation. D-RFT-2's substitution step explicitly does not need an e-graph (assessment entry, `:64`). + +### Role (c) — runtime evaluator + +**SKIP for all three.** Four reasons: +- every one materializes owned tuples (§2); +- every one would be a second executor of set operations, which "Polyfill, never legacy" forbids (`thought-git-basics-v1.md:174`); +- mask-risc is the reference fold algebra (P0); +- the measured oracle runs are in ms (datafrog `join_10000` 0.51–0.62 ms; PeTTa and Hyperon much slower: `thought-git-basics-v1.md:62`), which is a failed gate on any runtime path. + +**The one route worth naming, and why it fails: an Ascent BYODS provider over resident mask planes.** +- What works: `index_get` could yield the set bit positions of a plane, read in place. That makes it zero-copy with respect to the storage. +- What does not: the generated join is still a nested loop binding one value at a time, and it writes head tuples through `RelIndexWrite`. That is enumeration where a fold belongs. +- Count, exists and sum would still be per-binding loops, not one compare producing one mask. + +BYODS changes how a relation is stored. It does not change the execution model, and the execution model is what the P0 rule rejects. This stays SKIP, with the stated reason, unless the operator re-scopes. It is listed because the open item in `thought-git-basics-v1.md:174` ("whether a polyfill-backed BYODS relation fits ascent's interface is unchecked") now has a first-hand answer: **the interface fits, but the execution model does not.** + +### Concepts worth borrowing (no code, no dependency) + +- **Ascent's SCC + delta/total/new split** is the shape of relalg `μ` (D-MTP-3) in mask form: + - `delta` becomes a frontier plane; + - `total |= delta`; + - `new &= !total`; + - the fixpoint is reached when `new` is all zero. + + `walk_mask` already does this in a lab. Strata follow from the rule dependence SCCs, as `compute_dag_topo_order` already does for computed properties. +- **egglog's ruleset-per-schedule** maps onto `set_rules`: one enabled-rule set per `Semantics` stratum, which `rewrite_with(enabled)` already supports (`set_rules.rs:343-364`). + +## 5. Probes (pre-registered; nothing run) + +Every probe lives in a lab crate with its own workspace root, beside `crepe-plan-probe`. No probe reports a timing as a result; offline tools report counts only. + +**P-E1 — egglog offline normal-form search (D-CMR-8 / D-RFT-2).** +- **Setup.** + - Enumerate every `SetExpr` over the leaves {Sym0, Sym1, Res(lane 0 > 0)} built with `And`, `Or` and `Not`, up to 7 set nodes. + - Write two egglog rulesets: + - a two-valued Boolean algebra; + - a Kleene ruleset: no complement, no excluded middle, absorption kept, De Morgan kept. + - Saturate each ruleset under a node budget and extract with cost = `set_nodes` (`set_rules.rs:128`). + - Compare against `set_algebra::normalize_with(e, logic)`. +- **Assertions.** + - Every egglog-equal pair agrees with the Kleene `set_at` oracle on random NULL tables. This makes the oracle independent of egglog. + - Report how many terms egglog extracts strictly smaller than the local normalizer does. +- **Kill.** Zero strict improvements over the whole enumeration closes D-CMR-8 and moves egglog to PARK for good. +- **Disable (can-fire).** Drop the absorption rule from the egglog ruleset: known absorption terms must then come out larger than `normalize`'s. +- **Silent twin.** Under the Kleene ruleset, `check (= (Or A (Not A)) All)` must fail. + +**P-E2 — egglog proofs of the catalogue (optional, after P-E1).** +- For each `set_rules` rule that rests on a set identity (`RelationalDifference`'s set side, `SetNormalize`), `prove` the identity from the stratum's axioms only. +- **Kill.** A catalogue rule that cannot be proven from the stratum's axioms is a finding against the rule or the axiom encoding. Either way it is reported, not patched in egglog. + +**P-D1 — datafrog fold-vs-fold oracle (D-TGB-10 / D-RFT-3).** +- **Fixture.** Nested groups with a cycle and a diamond, 256 groups or fewer; a 257th group must be refused. +- **Substrate side.** Closure by iterated Boolean frontier masks, ending in `Count` plus k independent hash-sum terminals over the kept mask. Which terminal carries the hash is OPEN; `Measure::Sum(lane)` over an `I32` hash lane exists (`ir.rs:103`). +- **Oracle side.** datafrog closure, then the same folds computed over its relation. +- **Assertion.** The folds are equal. No `Vec` or set of pairs exists on the substrate side. +- **Disable.** Drop the cycle edge on the substrate side only: the folds must differ. +- **Silent twin.** The diamond counts once (Distinct), not twice. +- **Kill.** A constructed wrong answer of equal count (swap two members) is not detected with k = 2. Then raise k; if the probe still fails at k = 4, fold comparison is insufficient for this fixture, and that goes to the operator. + +**P-A1 — Ascent as the negation and aggregation oracle (D-TGB-8 rules).** +- **Rules.** "Branches with no anomaly" (negation) and "landed facts per source" (`agg count`). Each is written once in Ascent and once in datafrog with hand-ordered antijoins. +- **Comparison.** Both are compared to the substrate's folds, fold against fold. +- **Kill.** If every D-TGB-8 rule is reproduced in datafrog with hand stratification at no greater fixture complexity, Ascent goes to PARK and stays out of the dev-dependency set. +- **Disable.** Put the negated relation in the same stratum (datafrog side: antijoin against a still-growing relation). The answers must diverge, which shows that stratification is load-bearing. + +**P-A2 — Ascent lattice as the min-plus oracle (feeds P2).** +- **Oracle.** `lattice sp(u32, u32, Dual)` gives shortest hop counts. +- **Substrate.** The first level at which iterated Boolean frontier masks reach a node. +- **Assertion.** Equal per (source, target), compared as a fold: Σ distance and Count over reached pairs. +- **Disable.** Replace `Dual` with `u32` (that is, max): the two must disagree. +- **Kill.** Any disagreement on the dir-sim nest. + +**P-N — NARS lattice admissibility (already P6; no engine).** +- Check idempotence, commutativity and associativity of revision on a quantized grid. +- **Prediction.** Idempotence fails. That failure disqualifies both an Ascent `lattice` and an egglog `:merge` for NARS, and the probe records it. + +## 6. Recommendation matrix + +| role \ engine | egglog | datafrog | Ascent | +|---|---|---|---| +| (a) offline proof / normal-form generator for `set_rules` | **PROBE** (P-E1, then P-E2): lab crate only, never linked into the contract or relalg, counts only | SKIP | SKIP | +| (b) independent test oracle, D-RFT-3 / D-TGB-10 | SKIP (no negation or aggregation; no need for equality) | **ADOPT-NOW** as the SET oracle (already adopted). **ADOPT-NOW** (test infrastructure): switch probe comparisons to fold against fold (P-D1) | **PROBE** (P-A1 negation and aggregation, P-A2 min-plus lattice) only for strata datafrog cannot express without hand work | +| (c) runtime evaluator | SKIP | SKIP | SKIP (BYODS keeps the tuple-at-a-time join; reason recorded) | +| concept borrowing | PARK (rulesets per stratum already exist as `rewrite_with(enabled)`) | — | **PARK** (SCC + delta/total → relalg `μ` in mask form) until D-MTP-3 is scheduled | +| NARS stratum | SKIP (`:merge` precondition) | n/a | SKIP (`Lattice` precondition) unless P-N unexpectedly passes | +| K3 stratum | SKIP | SKIP | SKIP (the in-tree Kleene oracle already covers it) | +| Bag stratum | SKIP | PARK (X17 multiplicity column) | PARK (`agg sum` over a witness column) | + +For the Bag stratum, one of datafrog and Ascent should carry it, not both; see Q4. + +## 7. Open operator questions + +1. **The scope of "oracles compare by folds."** datafrog, Ascent and egglog all hold tuples internally. Is an external, test-only engine acceptable when the *comparison* is fold against fold, so that the substrate never decodes and the oracle computes the same folds over its own relation? Or does the P0 rule exclude tuple-native oracles altogether? If they are excluded, then all of role (b) goes, and the only oracle left is the materialized-table evaluator style already in `set_rules` tests, which also builds a table. +2. **The existing violations.** `walk_mask.rs` prints an "ascent ms" column and compares `BTreeSet` tuples. `join_probe.rs` compares sorted pair vectors. Should these be rewritten under P-D1, or banner-marked as pre-ruling labs? +3. **egglog's footprint.** It is a heavy dependency tree, and its fork pins toolchain 1.91.0 while the workspace uses 1.99. Is an isolated lab crate with its own workspace acceptable for P-E1? Or does D-CMR-8 stay a paper exercise until the local rewriter shows a measured loss? +4. **crepe or Ascent.** `crepe-plan-probe` already depends on both. Which one owns the negation and aggregation oracle slot? crepe also owns the rule-as-data front end (`crepe_plan!`), which Ascent's macro does not expose. +5. **The Bag stratum (D-RFT-1).** Should it be carried by datafrog plus a multiplicity column (X17), or by Ascent `agg sum` over a witness column? +6. **The hash terminal for P-D1.** Is a hash-sum over an `I32` id lane through the existing `Measure::Sum` acceptable as a fold fingerprint? Or should mask-risc gain a dedicated order-independent fingerprint terminal? A new terminal needs an insufficiency proof first. + +## Not read / not searched + +- The OOPSLA'23 BYODS paper: HTTP 403. A web search attributed it to a different author list, which is unverified, so it is not relied on. +- egglog-experimental, which may add negation. +- The Ascent paper's §5 numbers (they are not needed for roles a–c). +- The egglog paper's §5–6. +- The crepe source. +- Soufflé. +- Whether mask-risc already has a fingerprint-style terminal. + +`STATUS: open | OUTCOME: evaluation map; datafrog stays the SET oracle with fold comparison; Ascent gets a narrow oracle probe; egglog gets offline probes only; all three SKIP at runtime | OPEN: Q1–Q6` 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 new file mode 100644 index 000000000..9c8e05f63 --- /dev/null +++ b/.claude/board/entries/2026-10-21-pg-classview-polyfill-map.md @@ -0,0 +1,262 @@ +# PostgreSQL API → ClassView polyfill map (draft, 2026-10-21) + +**Status:** WORKING-MODEL / DRAFT. Read-only survey of the tree at #1668 (and the D-QSP plan in +#1667). Nothing here is built, ratified or a parity claim. PostgreSQL is the semantic +oracle; DuckDB the performance comparator (D-QSP plan :7). No SQL engine, ORM, planner or interpreter +is proposed: each row says which **existing** polyfill surface expresses a PG construct, under which +declared law, or that it is ABSENT. + +Stack: `ClassView (method + law) → Quack Binding (coordinates + witnesses) → optional DR (physical +mapping) → relalg/R2IL → mask-RISC`. + +## Sources read first-hand (file:line), and what was NOT read + +READ (full regions): +- `lance-graph-contract/src/set_algebra.rs:1-260` (module laws, `Cmp:81`, `Res:93`, `SetExpr:125`, + `Logic:185`, `normalize:195`, `normalize_kleene:201`, `normalize_with:206`); test names + `normalize_kleene_keeps_the_true_rows_under_null:906`, `normalize_kleene_never_grows_leaf_count:1015`. +- `lance-graph-contract/src/set_rules.rs:1-340` (`Arith:34`, `Truth:49`, `SumFamily:58`, + `Population:67`, `Semantics:74`, `Measure:107`, `Rule:184`, `Refusal:205`, `CATALOGUE:236`); test + names `experiment_e_*:1123-1513`. +- `lance-graph-contract/src/set_program.rs:1-120, 235-262` (`SetProgram:49`, `share:245`). +- `lance-graph-contract/src/class_view.rs:700-1060, 1380-1428` (`ComputeEdge:730`, + `execute_compute_dag:962`, `execute_defaults:1018`, `trait ClassView:1049`, `compute_dag:1403`, + `default_targets:1420`). Locations only for `FieldMask:70`, `WideFieldMask:243`. +- `lance-graph-quack/src/lib.rs:1-168, 210-300, 330-760, 1064-1095, 1124-1885` (`Cmp:218`, + `Filter:340`, `in_u32:446`, `in_i32:455`, `is_not_null:468`, `is_null:475`, `sql_where:549`, + `LowerError:1066`, `Agg:1127`, `GroupAddr:1235`, `GroupAgg:1263`, `Query:1301`, `GroupBy:1314`, + `AvgPlan:1510`, `lower_avg:1522`, `lower_group_avg:1573`, `avg_finish:1611`, `HavingCmp:1618`, + `GroupHaving:1654`, `lower_group_having:1688`, `GroupHavingPlan::finish:1787`, + `normalize_group_sink:1858`). +- `lance-graph-quack/src/bind.rs:1-420` (`BoundField:77`, `validity:87`, `Binder:92`, `Op:137`, + `BindError::UnknownValue:224`, `Draft::bind:288`). +- `lance-graph-mask-risc/src/ir.rs:286-560` (`Terminal:288`, `GroupKey:490`, `GroupFold:510`, + `GROUP_SUM_SYM_MAX_ROWS:697`, `MASKED_SUM_I32_MAX_ROWS:705`); `value.rs` `ExecError::SumRowBound:151`, + `LaneNotOrdered:181` (located). +- `lance-graph-relalg/src/{lib.rs, ir.rs, join_body.rs}` full; `lower.rs:1-80`; `program.rs:1-60`. +- `lance-graph-r2il/src/lib.rs:1-60` (module doc incl. implemented/refused calls) + `FoldError` variants. +- `dir-rmap-probe/src/pop.rs:1-60`, `qr.rs:1-30`, `prep.rs:95-112` (`Refusal`). +- `lance-graph-contract/examples/k3_pg_parity.rs` (full), board entry + `2026-10-21-d-rft-0-kleene-normalization.md` (full), `2026-10-20-six-decisions.md:1-60` (ADMISSION B), + D-QSP plan (full). + +CLAIMED (not read; named from grep hits or other docs only): test bodies of +`lance-graph-quack/tests/sql_null_3vl.rs` (names only, plus lines 669-784 headers), +`tests/duckdb_differential.rs` (fn names only), `mask-risc/tests/distinct.rs` (fn names only), +`relalg/src/normalize.rs` bodies, `relalg/src/lower.rs` past line 80, all of `exec.rs`, `fuse.rs`, +`graph_hop.rs`, `gremlin_parity.rs`, `spofc_cycle.rs`, the remaining 2,000+ lines of `class_view.rs` +(FieldMask/WideFieldMask methods, rail/facet readings), and the Linear/EXO tickets. + +## Legend + +- **Carrier**: `B` = Boolean row mask (`u64` words); `(T,F)` = Quack's polarity pair (T/F masks, U = + neither) — note: the code uses **(T, F)**, not (T, U), `lib.rs:533-548`; `ℕ` = count; `Σ0` = coalescing + sum (empty → 0); `Σsym` = sentinel sum (empty → `SYM_EMPTY_I64` marker); `seed` = MIN/MAX seed + `i64::MAX/MIN` as empty-marker; `K-mask` = K-bit group presence mask. +- **Semantics vector** = `set_rules::Semantics { universe, arith, truth, sums, population }` (`:74`). +- **Refusal type**: `Sem` = semantic refusal (the rewrite/answer would change meaning: + `set_rules::Refusal` `:205`); `Route` = route/binding/physical refusal (shape not admitted: Quack + `LowerError :1066`, `BindError`, mask-risc `ExecError::{LaneNotOrdered,SumRowBound}`, r2il + `FoldError`, DR `prep::Refusal{Stale,OutOfFocus,TooLarge,Duplicate}`). **Neither name exists as a type** + (`RouteRefusal`/`SemanticRefusal` grep: 0 hits in crates/) — see gap G6. +- Status: **VERIFIED-IN-CODE** (surface exists and its doc/test states this exact semantics), + **PARTIAL** (gap named), **ABSENT**. + +## Stratum 1 — K3 predicates (D-QSP-0) + +| PG construct | PG semantics (exact, NULL) | Polyfill surface | Declared law / carrier | Status | Oracle / test | Refusal | +|---|---|---|---|---|---|---| +| `x = c`, `<>`, `<`, `<=`, `>`, `>=` (int4 col vs const) | UNKNOWN if `x` NULL | Quack `Filter::Cmp(col, Cmp::{Eq,Ne,Lt,Le,Gt,Ge}I32)` `lib.rs:218`; NULL via `sql_where` `:549` (leaf `T=valid∧leaf`, `F=valid∧¬leaf`); contract `Res::I32` `set_algebra.rs:93` | `Truth::ThreeValued`; carrier `(T,F)` → WHERE takes `T` | VERIFIED | `sql_null_3vl::where_is_sql_three_valued_on_the_required_cases:274`, `random_trees_agree_with_the_oracle_both_lowerings:429`; `k3_pg_parity` (PG 16.14, 2000 exprs) | — | +| `x = c`, `<>` on coded/text col (u32 code) | same | `Cmp::EqU32/NeU32` `lib.rs:233`; `Res::U32` `set_algebra.rs:97`; text literal → code via `Binder::code` `bind.rs:92` | ThreeValued; `(T,F)`; codebook must be frozen per version (ADMISSION B) | VERIFIED (=,<>) | same; `k3_pg_parity` covers `u0` | `BindError::UnknownValue` (Route) — see trap T9 | +| `<`,`>` on text / u32 order | collation order | none: Quack u32 has only `=,<>`, ternary match; r2il `IntLess` → `NoUnsignedLaneCompare` (`r2il lib.rs` doc) | — | ABSENT | propose PG diff with `COLLATE "C"` | Route (`FoldError::NoUnsignedLaneCompare`) | +| `x op y` (column vs column) | UNKNOWN if either NULL | none: `Cmp` takes a scalar only (`lib.rs:212-216`); r2il `IntSub` lane-lane → `LaneVersusLane` | — | ABSENT (G4) | propose `WHERE a0 < a1` diff | Route | +| `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 | +| `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) | — | — | +| `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) | — | — | + +## Stratum 1b — WHERE collapse vs CHECK + +| PG construct | PG semantics | Surface | Law | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `WHERE φ` | keep rows where φ is TRUE (designated value TRUE) | `Filter::sql_where` `:549` returns `T(φ)`; measures count TRUE rows (`set_rules::Truth::ThreeValued` doc `:49-56`) | `(T,F)` → `T` | VERIFIED | `sql_null_3vl`, `k3_pg_parity` | — | +| `CHECK (φ)` / `FILTER`-free constraint test | passes on TRUE **or UNKNOWN** (= `¬F(φ)`) | expressible: `Filter::negate(Filter::negate(φ).sql_where(n))` = `¬T(¬φ)` = `¬F(φ)`; no named API; `normalize_kleene` may NOT be used (it preserves only the TRUE set) | `(T,F)` → `¬F` | PARTIAL (G3; no test) | propose: `SELECT count(*) FILTER (WHERE (φ) IS NOT FALSE)` diff | — | + +## Stratum 2 — aggregates (D-QSP-1) + +| PG construct | PG semantics | Surface | Law / carrier | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `COUNT(*)` | rows passing WHERE; empty → 0 | `Agg::Count` → `Terminal::Count` `ir.rs:290`; relalg `Measure::Count`; contract `Measure::Count` `set_rules.rs:111` | `ℕ` | VERIFIED | `duckdb_differential::sel_count_posted` etc. (CLAIMED bodies) | — | +| `COUNT(x)` | non-NULL x only | caller ANDs `Plane(valid(x))` into filter (`sql_where` doc `:543-544`; `AvgPlan` doc `:1500-1505`) | `ℕ` over `T ∧ valid` | VERIFIED (convention, not a type) | `sql_null_3vl::aggregates_keep_their_null_conventions:483` | — | +| `COUNT(DISTINCT x)` | distinct non-NULL values | `Agg::CountDistinctOrderedU32` `:1170` → `Terminal::CountKeyRunsU32` `ir.rs:401`; key lane must be KEY-ORDERED, enforced; unordered → refused (no seen-set fallback; `ScatterCountU32` held) | `ℕ`; NULLs excluded only if caller gates `valid(x)` | PARTIAL (ordered lanes only; doc at `:1159` links a non-existent `Agg::CountDistinctU32`) | `mask-risc/tests/distinct.rs::on_a_lane_in_key_order_…`, `a_lane_out_of_key_order_is_refused_…` | Route (`ExecError::LaneNotOrdered`) | +| `SUM(x)`, non-empty | Σ non-NULL; int4 → bigint | `Agg::SumI32` → `MaskedSumI32` (i64, exact up to `2^32` rows) `ir.rs:298` | `Arith::Exact`, `Σ0` | VERIFIED (with `valid(x)` gate) | `duckdb_differential::sum_posted` (CLAIMED) | Route (`SumRowBound` past `2^32`) | +| `SUM(x)` empty / all-NULL | **NULL** | scalar: `MaskedSumI32` returns 0 → **wrong** unless paired with a count (`avg_finish`-style `count==0 → NULL`); grouped: `GroupAgg::SumI32 → GroupFold::SumSymI32` `lib.rs:1290-1294`, `ir.rs:525` keeps empty distinct from 0; contract `SumFamily::Sym` `set_rules.rs:58` | scalar `Σ0` (wrong carrier); grouped `Σsym` + `K-mask` via `normalize_group_sink` `:1858` | PARTIAL (G7: no scalar NULL-preserving SUM) | Kleene entry "Open": no PG differential for empty SUM yet | Sem (`Refusal::SymFamily` blocks unsound rewrites) | +| `AVG(x)` | Σ/count non-NULL; empty → NULL | `lower_avg` `:1522` (two programs) + `avg_finish` `:1611` (`count==0 → None`) | `Σ0 / ℕ`; numeric vs f64 divergence | PARTIAL (PG `avg(int)` is `numeric`, here `f64`; D-QSP-3) | propose | — | +| `MIN(x)`/`MAX(x)` empty/all-NULL | NULL | scalar `MaskedMinI32/MaxI32` → `None` if empty `ir.rs:300`; relalg `Answer::Min(Option)` `lower.rs:31`; r2il pushes seed `i64::MAX/MIN` (r2il doc) | `seed` as NULL marker | VERIFIED (Quack/relalg) / trap in r2il (T7) | `duckdb_differential::min_posted_cc3` (CLAIMED) | — | +| `agg(x) FILTER (WHERE p)` | per-aggregate row filter, K3 on p | one `Query` per aggregate (each with its own `filter`) — the `AvgPlan` pattern; `GroupHaving` forces ONE shared filter for all aggs `:1656-1667` | `T(p)` per program | PARTIAL (scalar OK; grouped multi-agg with different FILTERs ABSENT) | `k3_pg_parity` uses `count(*) FILTER (WHERE …)` as its PG probe | — | +| `HAVING` | group predicate over aggregates; NULL agg → UNKNOWN → dropped | `GroupHaving` / `lower_group_having` `:1688` + `GroupHavingPlan::finish` `:1787` (unreached group never emitted; `HavingCmp` vs i64 const; conjunction only) | `K-mask` (`present`, `keep`) | PARTIAL: conjunction of `agg op const` only; no OR/NOT; no agg-vs-agg; correct NULL only when every agg's NULL ⇔ group unreached (T4) | propose PG diff incl. `HAVING min(x) > 0` with an all-NULL-x group | Route (`HavingAggOutOfRange`, `EmptyGroupUniverse`) | + +## Stratum 3 — grouping / dedup + +| PG construct | PG semantics | Surface | Law | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `GROUP BY k` (non-NULL categorical) | one group per distinct k | `lower_group_by` (K programs) `:1407`, `Agg::GroupReduce{GroupAddr::Local}` `:1201`, `GroupSumI32`; `lower_group_by_auto` `:1885` | key lane `0..K`; keys ≥ K **silently dropped** (zero-fallback) | VERIFIED for dense dictionary keys | `duckdb_differential::run_group*` (CLAIMED) | Route (`EmptyGroupUniverse`) | +| `GROUP BY k` via FK, two-column | | `GroupAddr::Via` / `GroupAddr::Pair` `:1235-1260` | fused; dangling fk dropped | VERIFIED (shape) | CLAIMED | — | +| `GROUP BY k` with NULL keys | all NULLs form **one** group | none: NULL payload is garbage; dropped if ≥K else mis-bucketed; caller must gate `valid(k)` → PG's NULL group lost | needs a reserved NULL code from the binder | ABSENT (G2) | propose PG diff with NULL keys | — | +| `SELECT DISTINCT k` | set of values, NULLs not distinct | `Agg::ScatterOrU32` into a K-domain mask (legal only as the demanded result) / ordered `CountDistinctOrderedU32` for its count | `B` over key domain | PARTIAL (no NULL member; no multi-column DISTINCT) | propose | — | +| "NULLs not distinct" (DISTINCT/GROUP BY/UNION) vs `=` | equality for grouping treats NULL=NULL; `=` does not | no carrier of the NULL group (G2) | — | ABSENT | — | — | + +## Stratum 4 — set operations + +| PG construct | PG semantics | Surface | Law | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `UNION` / `INTERSECT` / `EXCEPT` over **row identity of one table** | dedup; NULLs not distinct | `SetExpr::Or/And`, `Rel::diff` `relalg ir.rs:106`, `Runs::{union,intersect,difference}` `set_algebra.rs:636-675`; DR `Pop::{or,and,and_not}` `pop.rs:58-78` | `Population::Distinct`, `B` | VERIFIED only when both inputs are selections of the SAME population and the projection is the row id | relalg suites (CLAIMED) | Route (`Pop` → `Refusal::Stale` across versions) | +| `UNION` etc. over projected values | dedup on projected tuples | none (row-set ≠ value-set: two rows may project equal) | — | ABSENT | — | — | +| `UNION ALL` | bag sum | count only: `Measure::plus(Count(A), Count(B))` `set_rules.rs:137` | `ℕ`, `Population::Bag` | PARTIAL (counts/sums only; no bag carrier for rows) | propose | Sem (`Refusal::Bag` for range/complement) | +| `INTERSECT ALL` / `EXCEPT ALL` | bag min / monus | none | — | ABSENT (G8) | — | — | + +## Stratum 5 — joins (D-QSP-2) + +All join leaves are under **ADMISSION B**: `Filter::Semijoin`, `Pred::EqU32Via`, `MaskOp::Gather` "need +call-site classification before any removal" (`six-decisions.md:44-46`); no value-directed foreign gather +at PREPARE. + +| PG construct | PG semantics | Surface | Law | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `INNER JOIN` child→parent (n:1, PK) as filter | rows of child with matching parent satisfying p | `Filter::EqU32Via{fk,key,v}` `lib.rs:362`; NULL fk → UNKNOWN (`sql_where` doc `:518-522`); dangling fk → no row | `B`, ThreeValued on fk; PK uniqueness ASSUMED, not witnessed | PARTIAL (no witness that the foreign key lane is a PK; foreign-side NULL "not modelled" `:530`) | `sql_null_3vl::semijoin_over_a_null_fk_is_false_and_eq_via_is_unknown:784` | — | +| `INNER JOIN` aggregate over parent key | `SUM(l.a) GROUP BY p.k` | `Agg::GroupSumViaI32`, `GroupAddr::Via` | fused 2 hops, zero-fallback drops | VERIFIED (shape) | CLAIMED | Route (`SumRowBound`) | +| INNER JOIN fan-out (1:n, n:m) multiplicity | output row per match | none: `ScatterOrU32` is set-valued (union across repeats) `ir.rs:325` | needs bag/ℕ-per-row carrier | ABSENT (G8) | propose | Sem (`Bag`) | +| `LEFT JOIN` | NULL-extended unmatched rows | none (no join output, no NULL extension) | — | ABSENT | — | — | +| `EXISTS` (SEMI) | known TRUE/FALSE; NULL fk → FALSE | `Filter::Semijoin{fk, foreign}` over a RESIDENT foreign plane `:383`; NULL fk gated, `T=valid∧leaf`, `F=¬T` | two-valued `B` | VERIFIED (resident-plane precondition; ADMISSION B pending) | `sql_null_3vl:784` | — | +| `NOT EXISTS` (ANTI) | TRUE for NULL fk | `negate(Semijoin)` + `sql_where` → `F(Semijoin)` = `¬(valid∧leaf)` | `B` | VERIFIED | `sql_null_3vl:784` (doc lines 779-781) | — | +| `x NOT IN (SELECT y …)` | UNKNOWN if x NULL; **no rows at all** if any `y` NULL | none; must NOT be lowered as `negate(Semijoin)` | needs `(T,F)` with "subquery contains NULL" flag | ABSENT (T5) | propose: same fixture, NOT IN vs NOT EXISTS | — | +| NULL join keys | NULL never equals | `EqU32Via` UNKNOWN; `Semijoin` FALSE | as above | VERIFIED (fk side only) | `sql_null_3vl:784` | — | +| general n-ary join bodies | | `relalg::join_body::is_alpha_acyclic` `join_body.rs:21` — a GYO **diagnosis only**, no executor | — | ABSENT (diagnosis exists) | `acyclic/cyclic_bodies_are_recognised` | — | + +## Stratum 6 — recursion (D-QSP-4) + +| PG construct | PG semantics | Surface | Law | Status | Oracle | Refusal | +|---|---|---|---|---|---|---| +| `WITH RECURSIVE … UNION` (reachability) | set fixpoint; terminates on cycles | none general (relalg lib doc: "recursion (μ) … not built" `lib.rs:28-29`). Lab: DR256 Warshall closure of nested groups inside one 256-slot tile `qr.rs:8-14, 351` | set semantics, bounded ≤ 256 slots | PARTIAL-lab (one fixed relation; D-RFT-3 datafrog oracle is the prerequisite) | DR probe tests (CLAIMED); plan D-RFT-3 | Route (`prep::Refusal::TooLarge` > 256 groups — refused, never truncated) | +| `WITH RECURSIVE … UNION ALL` on cycles | does not terminate (PG loops / hits limits) | none | must REFUSE, not answer | ABSENT | — | (needs a refusal) | +| negative dependency / stratification | PG forbids non-monotone recursive refs | none | — | ABSENT | — | Sem (needed) | +| evolving snapshot / support deletion | — | DR `Pop::repair` re-derives from direct groups (multi-support safe) `pop.rs:22-28`; `Refusal::{Stale,OutOfFocus}` | witnessed version | PARTIAL-lab | CLAIMED | Route (`Stale`) | + +## Stratum 7 — scalars (D-QSP-3) — scope marker only + +- Integer: only `i32` lanes compared to constants and `i32→i64` exact sums (`Arith::Exact`, + `MASKED_SUM_I32_MAX_ROWS = 2^32` `ir.rs:705`, refused past it). No arithmetic expressions at all (r2il + `IntAdd` → `Unimplemented`). PG `int4 + int4` overflow **errors**; `Arith::Checked` exists as a law + (`set_rules.rs:43`) but no evaluator implements checked expressions. Literal out of `i32` → `BindError::OutOfRange`. +- `numeric`, `float`: ABSENT (`Arith::Ieee` exists only as a refusal guard; `avg_finish` is `f64`). +- Collation / text order: ABSENT (codebook `=` only; plan :49 requires a separate order-preservation proof for `Lt`). +- Casts, `u32`/`u64` ordered compares: ABSENT (`NoUnsignedLaneCompare`). + +## Out of scope (listed, not mapped) + +Transaction isolation / MVCC (snapshot witnesses ≠ MVCC parity), DDL (`create_table` / `Registrar` is a +test-only seam `bind.rs:~390`), time zones, client protocol, error message text, `ORDER BY`/`LIMIT` +(Quack doc: absent `lib.rs:165`), strings beyond codebook equality, window functions. + +--- + +## (1) How a ClassView method declares this — minimal law per stratum + +Today `trait ClassView` (`class_view.rs:1049`) has **no per-method semantic accessor**: its method-shaped +metadata is `compute_dag` (ordering only, explicitly "NOT an ActionDef-body interpreter" `:950-954`) and +`default_targets`. The D-QSP plan wants laws "per method/operation, not one Semantics(ClassId)" +(plan :22). Minimal declaration, reusing existing types wherever one fits: + +| Stratum | What the method must declare | Existing type that fits | Missing | +|---|---|---|---| +| K3 predicates | per field: nullable? and its validity plane; logic of the predicate | `BoundField.validity: Option` (`bind.rs:87`); `set_algebra::Logic::{TwoValued,Kleene}` (`:185`); `set_rules::Truth` (`:49`) | a ClassView-side link field-position → validity (FieldRef has none; Binder owns it) — G9 | +| WHERE vs CHECK | designated values: `{T}` or `{T,U}` | none | a "designation" flag; nothing models `¬F` — G3 | +| aggregates | empty-result convention per measure; arithmetic mode | `SumFamily::{Plain,Sym}`, `Arith::{Exact,Wrapping,Checked,Ieee}`, `GroupFold` seeds | scalar NULL-preserving SUM terminal — G7 | +| grouping/dedup | NULL-key equality (NULLs-not-distinct) | none | G2 | +| set ops / joins | set vs bag; key uniqueness witness | `Population::{Distinct,Bag}`; `Semantics.universe` | bag carrier (G8); PK/uniqueness witness for `EqU32Via` | +| recursion | monotone? set/bag? bound | none (only DR `TooLarge`) | stratification + termination law | +| all | which refusals are semantic vs route | `set_rules::Refusal` (semantic); scattered route errors | a common two-sided refusal shape — G6 | + +So the minimal per-method declaration is a `Semantics` vector (existing) **plus** three missing +dimensions: designation (`{T}` vs `{T,U}`), NULL-key equality, and per-field validity binding. Do not +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). +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). +3. **G2 — NULL group key / NULLs-not-distinct** (binder-reserved NULL code + validity). Unblocks GROUP BY + NULL, DISTINCT, UNION/INTERSECT/EXCEPT over nullable columns, COUNT(DISTINCT) NULL handling (≈5). +4. **G8 — bag / multiplicity carrier** (ℕ per row or per key). Unblocks INNER fan-out, LEFT counts, + UNION ALL rows, INTERSECT ALL, EXCEPT ALL (≈5). +5. **G4 — column-vs-column compare.** Unblocks `x op y`, `IS DISTINCT FROM y`, BETWEEN with column + bounds, join residuals (≈4). +6. **G5 — read-time NULL-aware value expressions** (COALESCE, NULLIF, nullable CASE output validity). (≈3) +7. **G7 — scalar NULL-preserving SUM** (a scalar `SumSymI32`, or a declared "SUM = Σ0 + count" finish + like `avg_finish`). Unblocks empty/all-NULL `SUM`, AVG over numeric, HAVING on scalar-like groups (≈3). +8. **G6 — typed two-sided refusal** (`RouteRefusal` vs `SemanticRefusal` as one shape over the six + scattered error enums), plus **G9** per-field validity in ClassView. Cross-cutting: every row's + "Refusal" column becomes checkable rather than prose. + +## (3) Known traps + +- **T1. `normalize_kleene` preserves only the TRUE set.** It is not closed under an outer `NOT`: negating + a Kleene-normalized expression is not the Kleene negation of the original's meaning on UNKNOWN rows. + Normalize at the WHERE boundary only; never feed a normalized subterm to CHECK (`{T,U}`) or under a NOT. +- **T2. Two-valued `normalize` still lives on shared paths.** `set_program::share` calls `normalize` + (`set_program.rs:246`); relalg's `normalize` is two-valued (sound only because relalg lanes carry no + NULL). Any nullable lane routed through `share` reintroduces the `x<5 OR x>=5 → All` bug (PG: 1 row vs 2). +- **T3. `Sym` is assumed two-valued** under `Truth::ThreeValued` (Kleene entry "Open"): binding a `Sym` + to a nullable predicate silently re-enables `p ∨ ¬p → All`. Contract statement, not a check. +- **T4. HAVING shares one filter across aggregates.** `finish` infers "NULL ⇔ unreached group" from sink 0 + (`lib.rs:1772-1776`). With `COUNT(*)` and `MIN(x)` over a nullable `x`, a reached group whose x are all + NULL has PG `min = NULL` (HAVING UNKNOWN → dropped) but here MIN either sees NULL payloads (no + `valid(x)` gate) or COUNT(*) loses rows (gate added). No correct encoding exists today. +- **T5. NOT IN ≠ NOT EXISTS.** `negate(Semijoin)` is NOT EXISTS (NULL fk → TRUE). SQL `NOT IN (subquery)` + returns no rows if the subquery yields any NULL, and UNKNOWN for a NULL outer value. Lowering NOT IN to + the anti-semijoin is a silent wrong answer. +- **T6. GROUP BY NULLs are equal while `=` is not reflexive on NULL**, and Quack's group key zero-fallback + silently DROPS out-of-range keys and mis-buckets NULL payloads `< K` unless the caller gates validity — + which then loses PG's NULL group. +- **T7. Empty-marker leakage.** `MaskedSumI32` empty → `0` (PG NULL); r2il `MIN/MAX` empty push + `i64::MAX/MIN` onto the scalar stack; `SumSymI32` reserves `i64::MIN`. Any later scalar arithmetic + (`IntSub` in r2il) on an unchecked marker yields a plausible wrong number. Grouped sinks must pass + `normalize_group_sink` before use. +- **T8. Bag laws.** Idempotence (`A ∪ A = A`), absorption and `Count(¬A) = N − Count(A)` hold for distinct + rows only; `set_rules` refuses the range/complement rules under `Population::Bag`, but `SetExpr` + normalization itself (idempotence, absorption) has no bag guard — never normalize a UNION ALL / + fan-out description with it. +- **T9. Unknown-literal refusal on `<>`.** `Draft::bind` refuses a text literal the codebook has never + seen (`BindError::UnknownValue`, `bind.rs:345`) for BOTH `=` and `<>`. PG answers `x <> 'never-seen'` + as TRUE for every non-NULL row. This is a refusal, not a wrong answer, but it is a PG divergence on + a valid query. +- **T10. Semijoin precondition.** `Filter::Semijoin`'s foreign plane must be RESIDENT, never another + program's `Keep` output (`lib.rs:388-398`); a subquery-as-plane pipeline is the forbidden + population-intermediate shape and an ADMISSION B violation. ADMISSION B classification of + Semijoin/EqU32Via/Gather call sites is still open. +- **T11. `EqU32Via` assumes PK uniqueness of the foreign row and models no foreign-side NULL** + (`lib.rs:530`); a non-unique parent turns INNER JOIN multiplicity into a set. +- **T12. P0 performance law.** Every surface above folds masks (ns per op, µs per batch). A + tuple/row-decoding PG oracle harness is fine **as the oracle** (it lives in the example/test), never + as an execution path; a ms number means the path left the fold (lance-graph CLAUDE.md P0). + +## Proposed differential (not built) + +Extend `examples/k3_pg_parity.rs`' shape (random tables with NULLs → SQL text → `psql` → compare to an +independent row oracle and to Quack/contract): one file per stratum (`k3_*`, `agg_*`, `group_*`, +`join_*`), each case asserting either PG-equal answer or a named refusal. Without a server it prints +`SKIP` (lab instrument; no CI gate yet — Kleene entry "Not done"). diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index b36214e04..333bf508d 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -414 entries, 2026-08-06 .. 2026-10-21. +419 entries, 2026-08-06 .. 2026-10-21. | date | entry id | finding | file | |---|---|---|---| @@ -34,15 +34,20 @@ exactly one of them, never both. | 2026-10-21 | `D-RU-3` | | [2026-10-21-u3-cross-rule-cse.md](2026-10-21-u3-cross-rule-cse.md) | | 2026-10-21 | `D-RU-2` | | [2026-10-21-u2-let-planes.md](2026-10-21-u2-let-planes.md) | | 2026-10-21 | `tuple-zero-copy-council` | | [2026-10-21-tuple-zero-copy-council.md](2026-10-21-tuple-zero-copy-council.md) | +| 2026-10-21 | `pg-classview-polyfill-map` | | [2026-10-21-pg-classview-polyfill-map.md](2026-10-21-pg-classview-polyfill-map.md) | +| 2026-10-21 | `eval-egglog-datafrog-ascent` | | [2026-10-21-eval-egglog-datafrog-ascent.md](2026-10-21-eval-egglog-datafrog-ascent.md) | | 2026-10-21 | `dr256-iam-nested-groups` | | [2026-10-21-dr256-iam-nested-groups.md](2026-10-21-dr256-iam-nested-groups.md) | | 2026-10-21 | `D-RU-6-LAB-1` | | [2026-10-21-d-ru-6-tile-walk-probe.md](2026-10-21-d-ru-6-tile-walk-probe.md) | | 2026-10-21 | `D-RU-6-LAB-2` | | [2026-10-21-d-ru-6-sparse-compute.md](2026-10-21-d-ru-6-sparse-compute.md) | | 2026-10-21 | `D-RU-6-LAB-3` | | [2026-10-21-d-ru-6-dirty-frontier.md](2026-10-21-d-ru-6-dirty-frontier.md) | +| 2026-10-21 | `D-RFT-1` | | [2026-10-21-d-rft-d-lfa-0-assessment.md](2026-10-21-d-rft-d-lfa-0-assessment.md) | +| 2026-10-21 | `D-RFT-0` | | [2026-10-21-d-rft-0-kleene-normalization.md](2026-10-21-d-rft-0-kleene-normalization.md) | | 2026-10-21 | `D-RA-2` | | [2026-10-21-d-ra-2-relalg-symbolic-repoint.md](2026-10-21-d-ra-2-relalg-symbolic-repoint.md) | | 2026-10-21 | `D-CMR-6` | | [2026-10-21-d-cmr-6-rule-catalogue.md](2026-10-21-d-cmr-6-rule-catalogue.md) | | 2026-10-21 | `D-CMR-5` | | [2026-10-21-d-cmr-5-rescope.md](2026-10-21-d-cmr-5-rescope.md) | | 2026-10-21 | `D-CMR-2b` | | [2026-10-21-d-cmr-2b-scratch-probe.md](2026-10-21-d-cmr-2b-scratch-probe.md) | | 2026-10-21 | `D-CMR-2` | | [2026-10-21-d-cmr-2-lowering.md](2026-10-21-d-cmr-2-lowering.md) | +| 2026-10-21 | `D-QSP` | | [2026-10-21-coresearch-plans-mapping-foresight.md](2026-10-21-coresearch-plans-mapping-foresight.md) | | 2026-10-21 | `D-RU-6` | | [2026-10-21-coresearch-ms-vs-ns-folding.md](2026-10-21-coresearch-ms-vs-ns-folding.md) | | 2026-10-21 | `coresearch-classview-algebra-polyfill` | | [2026-10-21-coresearch-classview-algebra-polyfill.md](2026-10-21-coresearch-classview-algebra-polyfill.md) | | 2026-10-21 | `classview-dr-iam` | | [2026-10-21-classview-dr-iam.md](2026-10-21-classview-dr-iam.md) | diff --git a/crates/lance-graph-contract/examples/k3_pg_parity.rs b/crates/lance-graph-contract/examples/k3_pg_parity.rs new file mode 100644 index 000000000..5ae63d409 --- /dev/null +++ b/crates/lance-graph-contract/examples/k3_pg_parity.rs @@ -0,0 +1,277 @@ +//! D-RFT-0 / D-QSP-0: set normalization against PostgreSQL's three-valued +//! `WHERE`. +//! +//! Random [`SetExpr`]s over a table with nullable lanes are rendered to SQL. +//! PostgreSQL counts the rows each `WHERE` keeps for the expression as +//! written, after [`normalize_kleene`], and after the two-valued +//! [`normalize`]. A Kleene evaluator in this file counts the same rows +//! without PostgreSQL. Expected: as written = Kleene = PostgreSQL for every +//! expression; the two-valued form differs on some. +//! +//! Needs `psql` and a server; connection from the usual `PG*` variables. +//! Without one it prints `SKIP` and exits 0, so nothing here gates CI. +//! +//! ```text +//! PGHOST=/var/tmp/k3pg PGPORT=54329 PGUSER=k3 PGDATABASE=postgres \ +//! cargo run --release -p lance-graph-contract --example k3_pg_parity +//! ``` + +use lance_graph_contract::set_algebra::{normalize, normalize_kleene, Cmp, Res, SetExpr}; +use std::io::Write; +use std::process::{Command, Stdio}; + +const ROWS: usize = 200; +const EXPRS: usize = 2000; + +struct Rng(u64); +impl Rng { + fn next(&mut self) -> u64 { + self.0 ^= self.0 << 13; + self.0 ^= self.0 >> 7; + self.0 ^= self.0 << 17; + self.0 + } + fn below(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +/// Columns: `a0`, `a1` nullable int; `u0` nullable int code; `s0`, `s1` +/// boolean, never NULL (a `Sym` is two-valued). +struct Row { + a: [Option; 2], + u: Option, + s: [bool; 2], +} + +fn rows(rng: &mut Rng) -> Vec { + let mut v = || (rng.below(4) != 0).then(|| rng.below(9) as i32 - 4); + let a: Vec<_> = (0..ROWS).map(|_| [v(), v()]).collect(); + a.into_iter() + .map(|a| Row { + a, + u: (rng.below(4) != 0).then(|| rng.below(3) as u32), + s: [rng.below(2) == 0, rng.below(2) == 0], + }) + .collect() +} + +fn leaf(rng: &mut Rng) -> SetExpr { + const OPS: [Cmp; 6] = [Cmp::Lt, Cmp::Le, Cmp::Gt, Cmp::Ge, Cmp::Eq, Cmp::Ne]; + match rng.below(5) { + 0 => SetExpr::Sym(rng.below(2) as u32), + 1 | 2 => SetExpr::i32( + rng.below(2) as u16, + OPS[rng.below(6) as usize], + rng.below(11) as i32 - 5, + ), + 3 => SetExpr::Res(Res::U32 { + lane: 0, + eq: rng.below(2) == 0, + v: rng.below(3) as u32, + }), + _ => SetExpr::i32(rng.below(2) as u16, Cmp::Ge, i32::MIN), + } +} + +fn expr(rng: &mut Rng, depth: u32) -> SetExpr { + if depth == 0 || rng.below(4) == 0 { + return leaf(rng); + } + match rng.below(3) { + 0 => SetExpr::negated(expr(rng, depth - 1)), + k => { + let cs = (0..1 + rng.below(4)) + .map(|_| expr(rng, depth - 1)) + .collect(); + if k == 1 { + SetExpr::And(cs) + } else { + SetExpr::Or(cs) + } + } + } +} + +fn op_sql(op: Cmp) -> &'static str { + match op { + Cmp::Lt => "<", + Cmp::Le => "<=", + Cmp::Gt => ">", + Cmp::Ge => ">=", + Cmp::Eq => "=", + Cmp::Ne => "<>", + } +} + +fn sql(e: &SetExpr) -> String { + let junction = |cs: &[SetExpr], sep: &str, unit: &str| { + if cs.is_empty() { + return unit.to_string(); + } + let parts: Vec = cs.iter().map(sql).collect(); + format!("({})", parts.join(sep)) + }; + match e { + SetExpr::All => "TRUE".into(), + SetExpr::Empty => "FALSE".into(), + SetExpr::Sym(i) => format!("s{i}"), + // `t` as a bigint literal: `-2147483648` would otherwise parse as + // the negation of an out-of-range int. + SetExpr::Res(Res::I32 { lane, op, t }) => { + format!("(a{lane} {} {}::bigint)", op_sql(*op), i64::from(*t)) + } + SetExpr::Res(Res::U32 { lane, eq, v }) => { + format!("(u{lane} {} {v})", if *eq { "=" } else { "<>" }) + } + SetExpr::Not(c) => format!("(NOT {})", sql(c)), + SetExpr::And(cs) => junction(cs, " AND ", "TRUE"), + SetExpr::Or(cs) => junction(cs, " OR ", "FALSE"), + } +} + +/// Kleene evaluation, by definition (`None` = UNKNOWN). +fn kleene(r: &Row, e: &SetExpr) -> Option { + match e { + SetExpr::All => Some(true), + SetExpr::Empty => Some(false), + SetExpr::Sym(i) => Some(r.s[*i as usize]), + SetExpr::Res(Res::I32 { lane, op, t }) => r.a[*lane as usize].map(|x| match op { + Cmp::Lt => x < *t, + Cmp::Le => x <= *t, + Cmp::Gt => x > *t, + Cmp::Ge => x >= *t, + Cmp::Eq => x == *t, + Cmp::Ne => x != *t, + }), + SetExpr::Res(Res::U32 { eq, v, .. }) => r.u.map(|x| (x == *v) == *eq), + SetExpr::Not(c) => kleene(r, c).map(|b| !b), + SetExpr::And(cs) => { + let mut unknown = false; + for c in cs { + match kleene(r, c) { + Some(false) => return Some(false), + None => unknown = true, + Some(_) => {} + } + } + (!unknown).then_some(true) + } + SetExpr::Or(cs) => { + let mut unknown = false; + for c in cs { + match kleene(r, c) { + Some(true) => return Some(true), + None => unknown = true, + Some(_) => {} + } + } + (!unknown).then_some(false) + } + } +} + +fn lit(v: Option) -> String { + v.map_or("NULL".into(), |x| x.to_string()) +} + +fn main() { + let mut rng = Rng(0x00D1_5EED_0003_0001); + let table = rows(&mut rng); + let exprs: Vec = (0..EXPRS).map(|_| expr(&mut rng, 4)).collect(); + + let mut script = String::from( + "CREATE TEMP TABLE t (a0 int, a1 int, u0 int, s0 bool, s1 bool);\nINSERT INTO t VALUES\n", + ); + let values: Vec = table + .iter() + .map(|r| { + format!( + "({}, {}, {}, {}, {})", + lit(r.a[0]), + lit(r.a[1]), + lit(r.u), + r.s[0], + r.s[1] + ) + }) + .collect(); + script.push_str(&values.join(",\n")); + script.push_str(";\n"); + for e in &exprs { + script.push_str(&format!( + "SELECT count(*) FILTER (WHERE {}), count(*) FILTER (WHERE {}), \ + count(*) FILTER (WHERE {}) FROM t;\n", + sql(e), + sql(&normalize_kleene(e)), + sql(&normalize(e)) + )); + } + + let out = Command::new("psql") + .args(["-X", "-q", "-tA", "-F,", "-v", "ON_ERROR_STOP=1", "-f", "-"]) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .and_then(|mut child| { + // Write on a separate thread: psql answers while it reads, so a + // parent that wrote everything before reading would block once + // the stdout pipe filled. A server that refuses the connection + // closes the pipe early; the exit status and stderr below say + // why, so a write error is moot. + let mut stdin = child.stdin.take().expect("piped stdin"); + let writer = std::thread::spawn(move || { + let _ = stdin.write_all(script.as_bytes()); + }); + let out = child.wait_with_output(); + let _ = writer.join(); + out + }); + let out = match out { + Ok(o) if o.status.success() => o, + Ok(o) => { + println!( + "SKIP: psql failed: {}", + String::from_utf8_lossy(&o.stderr).trim() + ); + return; + } + Err(e) => { + println!("SKIP: could not run psql ({e})"); + return; + } + }; + let lines: Vec<&str> = std::str::from_utf8(&out.stdout) + .expect("utf-8") + .lines() + .filter(|l| !l.is_empty()) + .collect(); + assert_eq!(lines.len(), EXPRS, "one result row per expression"); + + let (mut kleene_ok, mut two_valued_wrong, mut rewritten) = (0, 0, 0); + for (e, line) in exprs.iter().zip(&lines) { + let n: Vec = line.split(',').map(|x| x.parse().expect("count")).collect(); + let oracle = table.iter().filter(|r| kleene(r, e) == Some(true)).count(); + assert_eq!(n[0], oracle, "PostgreSQL vs the Kleene oracle: {e:?}"); + assert_eq!(n[1], n[0], "normalize_kleene changed the count: {e:?}"); + kleene_ok += 1; + two_valued_wrong += usize::from(n[2] != n[0]); + rewritten += usize::from(normalize_kleene(e) != *e); + } + println!( + "PostgreSQL {}: {EXPRS} expressions over {ROWS} rows; as written = Kleene oracle = \ + normalize_kleene on {kleene_ok}/{EXPRS} ({rewritten} rewritten); two-valued \ + normalize wrong on {two_valued_wrong}", + std::str::from_utf8( + &Command::new("psql") + .args(["-X", "-tA", "-c", "SHOW server_version"]) + .output() + .map(|o| o.stdout) + .unwrap_or_default() + ) + .unwrap_or("?") + .trim() + ); + assert!(two_valued_wrong > 0, "the run never reached a lane cover"); +} diff --git a/crates/lance-graph-contract/src/set_algebra.rs b/crates/lance-graph-contract/src/set_algebra.rs index 1eeddfc0e..513b49222 100644 --- a/crates/lance-graph-contract/src/set_algebra.rs +++ b/crates/lance-graph-contract/src/set_algebra.rs @@ -49,6 +49,27 @@ //! No rewrite distributes, so normalization never grows an expression //! exponentially to remove nesting. //! +//! # Three-valued (SQL) logic: [`normalize_kleene`] +//! +//! A residual on a lane that may hold NULL is UNKNOWN on that row. A measure +//! and a SQL `WHERE` count the rows where the expression is TRUE. +//! [`normalize`] is two-valued: rewrites 3 and 4 assume a row is in a set or +//! in its complement, so a union that covers a lane becomes `All` and a +//! conjunct that covers a lane disappears. On a NULL row that turns UNKNOWN +//! into TRUE (`x < 5 OR x >= 5` keeps no NULL row in PostgreSQL, `All` keeps +//! every row). +//! +//! [`normalize_kleene`] runs the same rewrites with those two cases replaced: +//! a covered `I32` lane becomes `x >= i32::MIN`, which is TRUE exactly on the +//! rows where `x` is not NULL, and a covered `U32` lane keeps its atoms. Every +//! other rewrite preserves the rows where the expression is TRUE under +//! Kleene logic: De Morgan and the negated comparison are Kleene +//! equivalences; after negation normal form no negation sits above a +//! junction, so a rewrite that keeps a subterm's TRUE rows keeps the whole +//! expression's TRUE rows (`p ∧ ¬p` is `Empty` because no row makes both +//! TRUE). A [`SetExpr::Sym`] is two-valued by definition, so its complement +//! rule stays. +//! //! An interval is always emitted as `<` / `>` bounds or one `==`. //! //! Zero dependencies. @@ -159,12 +180,33 @@ impl SetExpr { const LO: i64 = i32::MIN as i64; const HI: i64 = i32::MAX as i64; +/// Which logic the residual lanes follow. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Logic { + /// Every row satisfies a residual or its negation. + TwoValued, + /// A residual lane may be NULL; the residual is UNKNOWN there (SQL). + Kleene, +} + /// Rewrite `e` to an equivalent description, to a fixpoint (at most 64 -/// rounds; every rewrite shrinks or keeps the expression). +/// rounds; every rewrite shrinks or keeps the expression). Two-valued: see +/// [`normalize_kleene`] for lanes that may hold NULL. pub fn normalize(e: &SetExpr) -> SetExpr { + normalize_with(e, Logic::TwoValued) +} + +/// [`normalize`] for lanes that may hold NULL: the result is TRUE on exactly +/// the rows where `e` is TRUE under Kleene logic (module docs). +pub fn normalize_kleene(e: &SetExpr) -> SetExpr { + normalize_with(e, Logic::Kleene) +} + +/// [`normalize`] under `logic`. +pub fn normalize_with(e: &SetExpr, logic: Logic) -> SetExpr { let mut cur = nnf(e, false); for _ in 0..64 { - let next = simplify(&cur); + let next = simplify(&cur, logic); if next == cur { return next; } @@ -192,18 +234,18 @@ fn nnf(e: &SetExpr, neg: bool) -> SetExpr { } } -fn simplify(e: &SetExpr) -> SetExpr { +fn simplify(e: &SetExpr, logic: Logic) -> SetExpr { match e { SetExpr::All | SetExpr::Empty | SetExpr::Sym(_) => e.clone(), - SetExpr::Res(_) => conj(vec![e.clone()]), - SetExpr::Not(c) => match simplify(c) { + SetExpr::Res(_) => conj(vec![e.clone()], logic), + SetExpr::Not(c) => match simplify(c, logic) { SetExpr::All => SetExpr::Empty, SetExpr::Empty => SetExpr::All, SetExpr::Not(x) => *x, s => SetExpr::negated(s), }, - SetExpr::And(cs) => conj(cs.iter().map(simplify).collect()), - SetExpr::Or(cs) => disj(cs.iter().map(simplify).collect()), + SetExpr::And(cs) => conj(cs.iter().map(|c| simplify(c, logic)).collect(), logic), + SetExpr::Or(cs) => disj(cs.iter().map(|c| simplify(c, logic)).collect(), logic), } } @@ -215,8 +257,18 @@ fn complement(e: &SetExpr) -> Option { } } -/// `[lo, hi]` as `<` / `>` bounds or one `==`; empty for the whole lane. -fn emit_interval(lane: u16, lo: i64, hi: i64) -> Vec { +/// `x >= i32::MIN`: TRUE on every row where lane `x` is not NULL. The one +/// atom [`normalize_kleene`] emits for a whole lane. +fn present(lane: u16) -> SetExpr { + SetExpr::i32(lane, Cmp::Ge, i32::MIN) +} + +/// `[lo, hi]` as `<` / `>` bounds or one `==`; for the whole lane, nothing +/// (two-valued) or [`present`] (Kleene). +fn emit_interval(lane: u16, lo: i64, hi: i64, logic: Logic) -> Vec { + if (lo, hi) == (LO, HI) && logic == Logic::Kleene { + return vec![present(lane)]; + } if lo == hi { return vec![SetExpr::i32(lane, Cmp::Eq, lo as i32)]; } @@ -244,7 +296,7 @@ fn interval(op: Cmp, t: i32) -> Option<(i64, i64)> { } /// A conjunction of simplified children. -fn conj(children: Vec) -> SetExpr { +fn conj(children: Vec, logic: Logic) -> SetExpr { let mut flat = Vec::new(); for c in children { match c { @@ -289,12 +341,22 @@ fn conj(children: Vec) -> SetExpr { if lo > hi { return SetExpr::Empty; } - out.extend(emit_interval(lane, lo, hi)); - if lo + 1 < hi { - for &v in excl.range(lo + 1..hi) { - out.push(SetExpr::i32(lane, Cmp::Ne, v as i32)); - } - } + let ne: Vec = if lo + 1 < hi { + excl.range(lo + 1..hi) + .map(|&v| SetExpr::i32(lane, Cmp::Ne, v as i32)) + .collect() + } else { + Vec::new() + }; + // A `!=` already holds only where the lane is not NULL, so the + // whole-lane atom is needed only when nothing else names the lane. + let logic = if ne.is_empty() { + logic + } else { + Logic::TwoValued + }; + out.extend(emit_interval(lane, lo, hi, logic)); + out.extend(ne); } for (lane, (is, nots)) in eqs { let mut is = is.into_iter(); @@ -310,7 +372,7 @@ fn conj(children: Vec) -> SetExpr { } /// A disjunction of simplified children. -fn disj(children: Vec) -> SetExpr { +fn disj(children: Vec, logic: Logic) -> SetExpr { let mut flat = Vec::new(); for c in children { match c { @@ -348,16 +410,23 @@ fn disj(children: Vec) -> SetExpr { // `x ≠ a` on a lane: a second `x ≠ b`, or any interval holding `a`, // covers the whole lane; otherwise every interval on the lane lies // inside `x ≠ a` and is absorbed by it. + // Under Kleene logic a covered lane is `present(lane)`, not `All`. for (lane, ne) in excluded { + let iv = ranges.remove(&lane).unwrap_or_default(); let mut ne = ne.into_iter(); - let (Some(a), None) = (ne.next(), ne.next()) else { - return SetExpr::All; + let covered = match (ne.next(), ne.next()) { + (Some(a), None) if !iv.iter().any(|&(lo, hi)| lo <= a && a <= hi) => { + out.push(SetExpr::i32(lane, Cmp::Ne, a as i32)); + false + } + _ => true, }; - let iv = ranges.remove(&lane).unwrap_or_default(); - if iv.iter().any(|&(lo, hi)| lo <= a && a <= hi) { - return SetExpr::All; + if covered { + if logic == Logic::TwoValued { + return SetExpr::All; + } + out.push(present(lane)); } - out.push(SetExpr::i32(lane, Cmp::Ne, a as i32)); } for (lane, mut iv) in ranges { iv.sort_unstable(); @@ -369,7 +438,7 @@ fn disj(children: Vec) -> SetExpr { } } for (lo, hi) in merged { - let atoms = emit_interval(lane, lo, hi); + let atoms = emit_interval(lane, lo, hi, logic); match atoms.len() { 0 => return SetExpr::All, 1 => out.extend(atoms), @@ -378,12 +447,18 @@ fn disj(children: Vec) -> SetExpr { } } for (lane, (is, nots)) in eqs { - let mut ns = nots.iter(); - match (ns.next(), ns.next()) { - (Some(_), Some(_)) => return SetExpr::All, - (Some(a), None) if is.contains(a) => return SetExpr::All, - (Some(&a), None) => out.push(SetExpr::ne_u32(lane, a)), - _ => out.extend(is.into_iter().map(|v| SetExpr::eq_u32(lane, v))), + let covered = nots.len() > 1 || nots.iter().any(|a| is.contains(a)); + if covered { + if logic == Logic::TwoValued { + return SetExpr::All; + } + // A covered `U32` lane has no single Kleene atom: keep its atoms. + out.extend(nots.iter().map(|&v| SetExpr::ne_u32(lane, v))); + out.extend(is.iter().map(|&v| SetExpr::eq_u32(lane, v))); + } else if let Some(&a) = nots.first() { + out.push(SetExpr::ne_u32(lane, a)); + } else { + out.extend(is.into_iter().map(|v| SetExpr::eq_u32(lane, v))); } } out.extend(rest); @@ -758,6 +833,150 @@ mod tests { } } + /// Which lane values are NULL in world `seed`: about one row in four, + /// per lane, for all four lanes (`I32` lanes 0..2, then `U32` lanes). + fn nulls(seed: u64) -> [Vec; 4] { + let mut s = seed.wrapping_mul(0x9E37_79B9_7F4A_7C15) | 1; + let mut lane = || { + (0..N) + .map(|_| { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + s.is_multiple_of(4) + }) + .collect::>() + }; + [lane(), lane(), lane(), lane()] + } + + /// Kleene evaluation, by definition: `None` is UNKNOWN. A residual is + /// UNKNOWN where its lane is NULL; a `Sym` is two-valued. + fn kleene(w: &World, null: &[Vec; 4], e: &SetExpr, row: usize) -> Option { + match e { + SetExpr::All => Some(true), + SetExpr::Empty => Some(false), + SetExpr::Sym(i) => Some(w.syms[*i as usize][row]), + SetExpr::Res(r) => { + let slot = match *r { + Res::I32 { lane, .. } => lane as usize, + Res::U32 { lane, .. } => 2 + lane as usize, + }; + (!null[slot][row]).then(|| res_holds(w, *r, row)) + } + SetExpr::Not(c) => kleene(w, null, c, row).map(|b| !b), + SetExpr::And(cs) => { + let mut unknown = false; + for c in cs { + match kleene(w, null, c, row) { + Some(false) => return Some(false), + None => unknown = true, + Some(_) => {} + } + } + (!unknown).then_some(true) + } + SetExpr::Or(cs) => { + let mut unknown = false; + for c in cs { + match kleene(w, null, c, row) { + Some(true) => return Some(true), + None => unknown = true, + Some(_) => {} + } + } + (!unknown).then_some(false) + } + } + } + + /// The rows where `e` is TRUE: what a measure counts and `WHERE` keeps. + fn true_rows(w: &World, null: &[Vec; 4], e: &SetExpr) -> Vec { + (0..N) + .map(|row| kleene(w, null, e, row) == Some(true)) + .collect() + } + + /// FAILS IF: `normalize_kleene` changes the rows where an expression is + /// TRUE when lanes hold NULL. Same generator as the two-valued test, + /// against an independent Kleene evaluator. Twin: the two-valued + /// `normalize` DOES change them on some inputs here, so the generator + /// reaches the lane-covering rewrites this mode exists to replace. + #[test] + fn normalize_kleene_keeps_the_true_rows_under_null() { + let mut g = Gen(0x5EED); + let (mut changed, mut two_valued_wrong) = (0, 0); + for k in 0..3000 { + let w = world(1 + k % 7); + let null = nulls(1 + k % 5); + let e = g.expr(5); + let want = true_rows(&w, &null, &e); + let n = normalize_kleene(&e); + assert_eq!(true_rows(&w, &null, &n), want, "{e:?}\n => {n:?}"); + assert_eq!(normalize_kleene(&n), n, "not idempotent: {e:?}"); + changed += usize::from(n != e); + two_valued_wrong += usize::from(true_rows(&w, &null, &normalize(&e)) != want); + } + assert!(changed * 2 > 3000, "only {changed} rewritten"); + assert!( + two_valued_wrong > 30, + "two-valued wrong on {two_valued_wrong}" + ); + } + + /// The four lane covers, one at a time, on rows `[3, NULL]`: two-valued + /// they become `All` (both rows), Kleene keeps one row. + #[test] + fn a_lane_cover_keeps_null_rows_out() { + let w = World { + syms: vec![vec![false; N]; SYMS as usize], + i32_lanes: [vec![3; N], vec![0; N]], + u32_lanes: [vec![1; N], vec![0; N]], + }; + let mut null = [ + vec![false; N], + vec![false; N], + vec![false; N], + vec![false; N], + ]; + for lane in &mut null { + for (row, v) in lane.iter_mut().enumerate() { + *v = row % 2 == 1; + } + } + let covers = [ + // interval union over the whole lane + SetExpr::Or(vec![ + SetExpr::i32(0, Cmp::Lt, 5), + SetExpr::i32(0, Cmp::Ge, 5), + ]), + // two `!=` + SetExpr::Or(vec![ + SetExpr::i32(0, Cmp::Ne, 1), + SetExpr::i32(0, Cmp::Ne, 2), + ]), + // `!=` and an interval holding its value + SetExpr::Or(vec![ + SetExpr::i32(0, Cmp::Ne, 1), + SetExpr::i32(0, Cmp::Lt, 4), + ]), + // a conjunct covering the whole lane (`sym0` is false everywhere) + SetExpr::And(vec![ + SetExpr::i32(0, Cmp::Ge, i32::MIN), + SetExpr::negated(SetExpr::Sym(0)), + ]), + // `U32`: two `!=`, then `!=` with its `==` + SetExpr::Or(vec![SetExpr::ne_u32(0, 1), SetExpr::ne_u32(0, 2)]), + SetExpr::Or(vec![SetExpr::ne_u32(0, 1), SetExpr::eq_u32(0, 1)]), + ]; + for e in &covers { + let want = true_rows(&w, &null, e); + assert_eq!(want.iter().filter(|&&b| b).count(), N.div_ceil(2), "{e:?}"); + assert_eq!(true_rows(&w, &null, &normalize_kleene(e)), want, "{e:?}"); + assert_ne!(true_rows(&w, &null, &normalize(e)), want, "{e:?}"); + } + } + /// FAILS IF: any rewrite changes the selected set. Differential against /// materialized bitsets over random nested expressions, incl. `All`, /// `Empty` and negations, in several worlds. @@ -789,6 +1008,21 @@ mod tests { } } + /// The Kleene form never grows the leaf count either: the whole-lane + /// atom `x >= i32::MIN` is emitted only where no `!=` already names the + /// lane, and a covered lane replaces at least two atoms with one. + #[test] + fn normalize_kleene_never_grows_leaf_count() { + let mut g = Gen(0xB0B); + for _ in 0..3000 { + let e = g.expr(5); + assert!(normalize_kleene(&e).leaves() <= e.leaves(), "{e:?}"); + } + // The `!=` case on its own: `x != 1` stays one atom. + let ne = SetExpr::i32(0, Cmp::Ne, 1); + assert_eq!(normalize_kleene(&ne), ne); + } + fn x() -> SetExpr { SetExpr::And(vec![SetExpr::Sym(1), SetExpr::Sym(4)]) } diff --git a/crates/lance-graph-contract/src/set_rules.rs b/crates/lance-graph-contract/src/set_rules.rs index 9dba6aad1..e5627a94a 100644 --- a/crates/lance-graph-contract/src/set_rules.rs +++ b/crates/lance-graph-contract/src/set_rules.rs @@ -27,7 +27,7 @@ //! //! Zero dependencies. -use crate::set_algebra::{normalize, SetExpr}; +use crate::set_algebra::{normalize, normalize_kleene, SetExpr}; /// How the arithmetic of a measure is evaluated. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -237,8 +237,8 @@ pub const CATALOGUE: &[RuleSpec] = &[ RuleSpec { rule: Rule::SetNormalize, pattern: "Count(S) / Sum(S) with S not normalized", - requires: "two-valued sets; the result is strictly smaller", - refuses: &[Refusal::NotTwoValued], + requires: "the result is strictly smaller; three-valued sets use the Kleene form", + refuses: &[], }, RuleSpec { rule: Rule::EmptyMeasure, @@ -439,13 +439,15 @@ fn apply(rule: Rule, m: &Measure, sem: &Semantics) -> Option return None, }; - let n = normalize(set); + // A measure counts the rows where its set is TRUE, and the Kleene + // form keeps exactly those (`set_algebra` module docs). + let n = match sem.truth { + Truth::TwoValued => normalize(set), + Truth::ThreeValued => normalize_kleene(set), + }; if n == *set { return None; } - if sem.truth != Truth::TwoValued { - return Some(Err(Refusal::NotTwoValued)); - } Some(Ok(rebuild(n))) } Rule::Complement => { @@ -921,6 +923,54 @@ mod tests { assert!(fired > 1200, "only {fired} steps fired"); } + /// 600 random measures over tables WITH NULL lanes, under three-valued + /// semantics, every rule: the answer equals the Kleene oracle's and set + /// normalization fires. Twin: on the same inputs the two-valued + /// normalization alone changes some answers, so the inputs reach the + /// cases the Kleene form exists for. + #[test] + fn rewrites_keep_the_answer_under_three_valued_tables() { + let mut rng = Rng(0x0BAD_5EED_1234_5678); + let sem3 = |n: usize| Semantics { + truth: Truth::ThreeValued, + ..Semantics::exact(n as u64) + }; + let (mut normalized, mut two_valued_wrong) = (0usize, 0usize); + for _ in 0..600 { + let n = 1 + rng.below(40) as usize; + let t = table(&mut rng, n, true, false); + let m = measure(&mut rng, 2); + let (r, tr) = rewrite(&m, &sem3(n), BUDGET); + assert!(!tr.budget_exhausted, "no fixpoint for {m:?}"); + assert!(r.size() <= m.size(), "size grew: {m:?} -> {r:?}"); + assert_eq!( + ev(&t, &m, Acc::Exact), + ev(&t, &r, Acc::Exact), + "{m:?}\n-> {r:?}" + ); + normalized += tr + .steps + .iter() + .filter(|s| **s == Rule::SetNormalize) + .count(); + let (r2, _) = rewrite_with( + &m, + &Semantics::exact(n as u64), + BUDGET, + &[Rule::SetNormalize], + ); + two_valued_wrong += usize::from(ev(&t, &r2, Acc::Exact) != ev(&t, &m, Acc::Exact)); + } + assert!( + normalized > 300, + "set normalization fired {normalized} times" + ); + assert!( + two_valued_wrong > 5, + "two-valued wrong on {two_valued_wrong}" + ); + } + /// Each rule fires on its own at least once in the random run above's /// distribution (so a dead rule is visible). #[test] @@ -1089,20 +1139,23 @@ mod tests { truth: Truth::ThreeValued, ..Semantics::exact(4) }; - let (r, tr) = rewrite(&m, &sem, BUDGET); + let (r, tr) = rewrite_with(&m, &sem, BUDGET, &[Rule::Complement]); assert_eq!(r, m); assert!(tr .refusals .contains(&(Rule::Complement, Refusal::NotTwoValued))); - assert!(tr - .refusals - .contains(&(Rule::SetNormalize, Refusal::NotTwoValued))); + // The whole catalogue: set normalization (Kleene form) turns `¬(x > 0)` + // into `x < 1`, UNKNOWN on the same NULL rows, so the count is kept. + let (r, tr) = rewrite(&m, &sem, BUDGET); + assert_eq!(r, Measure::Count(SetExpr::i32(0, Cmp::Lt, 1))); + assert_eq!(tr.steps, vec![Rule::SetNormalize]); + assert_eq!(ev(&t, &r, Acc::Exact), ev(&t, &m, Acc::Exact)); } /// NULL: two-valued normalization turns `A ∨ ¬A` into `All`, which /// counts the UNKNOWN rows too. #[test] - fn experiment_e_null_refuses_set_normalization() { + fn experiment_e_null_normalizes_in_the_kleene_form() { let a = SetExpr::i32(0, Cmp::Gt, 0); let m = Measure::Count(SetExpr::Or(vec![a.clone(), SetExpr::negated(a)])); let t = Table { @@ -1120,11 +1173,12 @@ mod tests { truth: Truth::ThreeValued, ..Semantics::exact(3) }; + // Three-valued, the Kleene form covers the lane with `x >= i32::MIN`: + // TRUE on the non-NULL rows only, so the count stays 2. let (r, tr) = rewrite(&m, &sem, BUDGET); assert_eq!(ev(&t, &r, Acc::Exact), Val::I(2), "rewritten to {r:?}"); - assert!(tr - .refusals - .contains(&(Rule::SetNormalize, Refusal::NotTwoValued))); + assert_eq!(r, Measure::Count(SetExpr::i32(0, Cmp::Ge, i32::MIN))); + assert_eq!(tr.steps, vec![Rule::SetNormalize]); // Two-valued, the same expression is the whole universe, counted. let (r2, tr2) = rewrite(&m, &Semantics::exact(3), BUDGET); assert_eq!(tr2.steps, vec![Rule::SetNormalize, Rule::CountAll]); @@ -1598,6 +1652,11 @@ mod tests { sorted.dedup(); assert_eq!(sorted.len(), rules.len()); assert_eq!(rules.len(), 8); - assert!(CATALOGUE.iter().all(|s| !s.refuses.is_empty())); + // Every rule but `SetNormalize` has a guard: set normalization keeps + // the rows where the set is TRUE under either logic, so it never + // refuses (three-valued sets take the Kleene form). + for s in CATALOGUE { + assert_eq!(s.refuses.is_empty(), s.rule == Rule::SetNormalize, "{s:?}"); + } } }