diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index e2b59a4d3..e8609125e 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,4 +1,16 @@ -## 2026-10-21 — D-CMR-6 rule catalogue in the contract (in PR) +## 2026-10-21 — D-RA-2: relalg `symbolic` repointed onto `contract::set_rules` (in PR) + +- **Contract:** `set_rules::Rule::{EmptyMeasure, CountAll}` added (catalogue 8 rules). **relalg:** `normalize::symbolic` delegates to `set_rules::rewrite`; crepe's symbolic answers follow through `lance_graph_relalg::run`. Entry `entries/2026-10-21-d-ra-2-relalg-symbolic-repoint.md`. + +### Current Contract Inventory — net delta (`set_rules.rs`) + +- Two `Rule` variants added; no type removed or changed. + +## 2026-10-21 — main after #1651 (merged `6bf4f86`) + +- **On main:** #1651 (D-CMR-6 `contract::set_rules`, plus the #1650 closeout). Contract inventory delta: `set_rules.rs` (see the D-CMR-6 section below). + +## 2026-10-21 — D-CMR-6 rule catalogue in the contract (#1651, merged `6bf4f86`) - **Contract (new module):** `set_rules::{Measure, RowRange, Semantics, Arith, Truth, SumFamily, Population, Rule, Refusal, RuleSpec, CATALOGUE, Trace, rewrite, rewrite_with, all_rules}`. Six guarded rules (set normalization, complement, relational difference, additive cancellation, range intersection, range count) as data, applied to a fixpoint with a step budget; every applied step strictly shrinks the measure; refused matches keep the original and are traced. Zero dependencies; `set_algebra.rs` / `set_program.rs` unchanged. Entry `entries/2026-10-21-d-cmr-6-rule-catalogue.md`. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index 29c590507..abe09425d 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,3 +1,10 @@ +## 2026-10-21 — lance-graph PR #1651 (merged `6bf4f86`, branch `claude/eager-albattani-iufugq`, head `43218eb`) — D-CMR-6: guarded rule catalogue and fixpoint driver in the contract; #1650 closeout + +- **Added:** `lance_graph_contract::set_rules::{Measure, RowRange, Semantics, Arith, Truth, SumFamily, Population, Rule, Refusal, RuleSpec, CATALOGUE, Trace, rewrite, rewrite_with, all_rules}` (zero deps); entry `2026-10-21-d-cmr-6-rule-catalogue.md`. Also the #1650 board closeout (D-CMR-2 Shipped, PR_ARC #1650). +- **Locked:** six rules as data (set normalization, complement, relational difference, additive cancellation, range intersection, range count), each with explicit refusals (three-valued, no universe, bag, checked, IEEE, `_sym` sums, impure, basis mismatch, past universe); the driver applies only strictly shrinking rewrites to a fixpoint or a step budget; refused matches keep the original and are traced. `set_algebra.rs`, `set_program.rs`, crepe, relalg and mask-risc unchanged. +- **Deferred / open:** repointing crepe and relalg onto `set_rules`; a prefix-lane `Sum([lo,hi))` rule; D-CMR-8 only if rules compete. +- **Confidence:** measured. 22 tests (the 22nd, the range rules' no-universe refusal, added in the closeout after Codex's review of #1654) (differential vs `i128` / wrapping oracles over random tables and rule subsets; experiments A, D, E); every guard disable-verified red; Codex found four missing guards (complement for bags and checked/IEEE, `_sym` cancellation, IEEE range count), all fixed with tests before merge; CI green. + ## 2026-10-21 — lance-graph PR #1650 (merged `f031089`, branch `claude/eager-albattani-iufugq`, head `98d97ef`) — D-CMR-2: the contract set algebra lowered onto mask-risc; D-CMR-5 re-scoped - **Added:** `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured, LowerError}` (core, no new dependency); entries `2026-10-21-d-cmr-2-lowering.md`, `2026-10-21-d-cmr-5-rescope.md`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index d0e4bc20c..b974a3c6d 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -243,7 +243,7 @@ Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own work | **D-HOLO-H14c** | Thought-first positional reads `Thought(t)[Table(a)[i] : Table(b)[i]]`: point projection, presence/Hamming populations through mask-risc, explicit terminal rows; memory and fragmentation of positional tables; Lance 13 masked I/O; coordinate identity across rewrites (sub-ids -1 … -6) | Measured 2026-10-15 (v4, entry 2026-10-15-d-holo-h14c-thought-first): acceptance A–E met (tables consulted == k for every U; k = 2 read at U = 31 0.90–1.16x U = 2); C vs B on query-shaped reads mixed; uniform 1 % positional tables ≈ 93x payload resident (flagged); Lance prediction holds (uniform 1 % mask 1.00x bytes, clustered 0.24x); stale maps omit silently, refused by the version check; returned to the operator | tables consulted == requested lanes for every touched count; at k = 2, U = 31 read <= 1.25x U = 2; populations load no value; no row materialized outside the terminal; no wrong coordinate across rewrites; Lance prediction (1 % uniform mask does not halve bytes_read, 1 % clustered does) | | **D-HOLO-H14d** | C's own operation in four stages, C only: (1) relalg symbolic reduction of the thought's set expression, (2) materialize `R = P_a ∧ P_b ∧ A` (or `∨`) over presence planes, (3) Lance 13 read pruned by `R`, (4) COUNT/EXISTS from `R` or the operation on `T_a[i], T_b[i]` for survivors; sub-ids -1 … -5 | Measured 2026-10-16 (v4, entry 2026-10-16-d-holo-h14d-logic-mask-read): stage 1 decides 675/2,000 programs with 0 runs, 396 answered only after the rewrite, 2 widened (ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN), passes 1,065 vs 5,898; R costs 2–10 ns per 64-address word; Lance scans exactly |R| everywhere, bytes 1.00x at uniform 1 % full tile, 0.19x clustered 1 %, 0.01–0.12x inside a 1,024/8,192 aperture; payload ~6 ns per lane load, reads == |R| × k, not flat at small |R| (fixed word scan; prediction 4 falsified); fused Σ ~1.3 ns per value; point query 8–45 ns hot; returned to the operator | `R` == per-address reference; rewritten == as written on 2,000 programs; payload reads == |R| × k; Lance rows == |R| with reference values; five disable runs red | | **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | Shipped #1546 `c21bd165` (11 tests, 11 disable runs red; four comparisons on one lane 8 → 2 ops; 70/2,000 small descriptions refused as written, all run rewritten) | == row oracle over 400 generated descriptions × 5 measures | -| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). D-CMR-1 shipped (#1644): relalg `normalize` delegates to `contract::set_algebra::normalize`; repointing crepe follows D-CMR-6 | relalg tests pass unchanged against the contract IR | +| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). D-CMR-1 shipped (#1644): relalg `normalize` delegates to `contract::set_algebra::normalize`. After D-CMR-6: relalg `symbolic` (and crepe through it) delegates to `contract::set_rules` (in PR; `entries/2026-10-21-d-ra-2-relalg-symbolic-repoint.md`); crepe's join-body rewrites stay | relalg tests pass unchanged against the contract IR | | **D-RA-3** | Datalog rules as algebra values; names are labels resolved through the label codebook, never strings in a rule — council v3 (2026-10-16) places the Datalog VALUES in `metta::datalog`; D-RA-2 still gates relalg | Queued (after D-RA-2) | codebook-built rules == hand-written `Rel`; unknown label refused at resolution | | **D-RA-4** | **⛔ VIOLATION — GATHER. DO NOT BUILD. CORRECT: D-HOLO-H14c / H14d.** Bound recursion via external frontier driver over D-CMR-5 preimage | Queued (after D-CMR-5) | == row-oracle closure; frontier past bound refused | @@ -259,7 +259,7 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES | **D-CMR-3** | Quack frontend: `Filter` → set IR (extent hoisting falls out) | Queued | identical answers on the quack suite; other-basis range stays residual | | **D-CMR-4** | Two dimensions: `Rect` over composite coordinates, row-major or Morton runs | Queued | rectangle ∩ == bitset oracle | | **D-CMR-5** | **BLOCKED: lawful design proposed (operator 2026-10-21).** Preimage `f⁻¹(S)` as a co-addressed transposed tile fold over a version-witnessed projection of `f`, built in preparation by a sequential same-table scan with frozen-codebook endpoint translation (ADMISSION B; reusable across queries). `S` enters only as a membership plane translated into the same frozen coordinates. No seek or load of `f` keyed by `S`'s values or a previous fold (Q1 = C), no `Gather`, no scatter terminal. R1 (`rmap` `rebind` / `discover` escape-driven seeks) stays option C. ⊘ Was: "VIOLATION — GATHER. DO NOT BUILD" (entry `2026-10-21-d-cmr-5-rescope.md`) | BLOCKED — needs a contract-level attested witness for the frozen codebook (`rmap::Witness` is a probe-local stand-in); no preimage operator exists; not admitted, not ready to build | == row oracle; program checked Gather-free with a silence twin; attest / projection / query costs reported apart; a many-to-one `f` gives a valid distinct-source preimage (tested) and a bag-sensitive Count/Sum over it is refused (tested); refusal on a stale or missing witness | -| **D-CMR-6** | Rule catalogue + fixpoint driver: complement, relational difference | In PR (`contract::set_rules`; `entries/2026-10-21-d-cmr-6-rule-catalogue.md`) | Experiments A, D, E; each guard removal fails | +| **D-CMR-6** | Rule catalogue + fixpoint driver: complement, relational difference | Shipped (#1651, `6bf4f86`; `contract::set_rules`; `entries/2026-10-21-d-cmr-6-rule-catalogue.md`) | Experiments A, D, E; each guard removal fails | | **D-CMR-7** | NAL frontend: aperture → `Runs` | Queued (after NAL lands in core) | NAL W2 tests unchanged | | **D-CMR-8** | Equality-saturation probe (`egg`/`egglog` as references) | Queued (only if rules compete) | compared against D-CMR-6; no dependency without evidence | | **D-CMR-9** | Benchmark: eager materialization vs set IR vs row loop | Queued | answers asserted before timing; tier from the build's report | diff --git a/.claude/board/entries/2026-10-21-d-cmr-6-rule-catalogue.md b/.claude/board/entries/2026-10-21-d-cmr-6-rule-catalogue.md index bd08c9e8b..aaf394ace 100644 --- a/.claude/board/entries/2026-10-21-d-cmr-6-rule-catalogue.md +++ b/.claude/board/entries/2026-10-21-d-cmr-6-rule-catalogue.md @@ -1,6 +1,6 @@ # 2026-10-21 — D-CMR-6: the guarded rule catalogue and fixpoint driver in the contract -**Status:** TEST-PINNED, in PR (branch `claude/eager-albattani-iufugq`). **Basis:** plan `d-cmr-concept-chain-normalization-v1.md` §3.5, §4, §7 and the D-CMR-6 row; ownership `gpt-ada-01/004`, `/007`; claim EXO-50 `session_013z2e1YXkm6o6HNrDn5BPWA/016`. +**Status:** TEST-PINNED, merged in #1651 (`6bf4f86`). **Basis:** plan `d-cmr-concept-chain-normalization-v1.md` §3.5, §4, §7 and the D-CMR-6 row; ownership `gpt-ada-01/004`, `/007`; claim EXO-50 `session_013z2e1YXkm6o6HNrDn5BPWA/016`. - **Where:** `crates/lance-graph-contract/src/set_rules.rs` (`lance_graph_contract::set_rules`), zero dependencies. It consumes `set_algebra::{SetExpr, normalize}` and edits neither `set_algebra.rs` nor `set_program.rs` (U2). crepe, relalg and mask-risc are untouched; no consumer carries a second copy of these rules. - **Types:** `Measure` = `Const | Count(SetExpr) | Sum{lane,set} | CountRows(Vec) | Opaque{id,pure} | Add | Sub`. `Semantics { universe, arith: Exact|Wrapping|Checked|Ieee, truth: TwoValued|ThreeValued, sums: Plain|Sym, population: Distinct|Bag }`. @@ -16,9 +16,10 @@ | `RangeCount` | `Count([lo,hi)) → max(0, hi−lo)` | bag; IEEE; no universe; bound past it | - **Driver:** `rewrite` / `rewrite_with(enabled)` try rules at a node before its children, apply only a rewrite that strictly decreases `(set nodes, all nodes)`, stop at the fixpoint or the step budget (`Trace::budget_exhausted` set only if another step would fire). Refused matches are recorded once each in `Trace::refusals`; the original is kept. -- **Tests (21):** 600 random measures over random two-valued tables, under exact (`i128`) and wrapping (`i64`) oracles, with random rule subsets (disabling any optimization keeps the answer): equal answers, size never grows, no refusal on valid input, most inputs rewritten (anti-vacuity). Every non-range rule fires on random input. Experiment A (relational difference vs the `i128` oracle; checked refuses, and the eager `i32` accumulator is the counterexample: the original overflows, the rewritten sum is 5). Experiment D (three ranges → intersect → `Const(20)`; with intersection disabled the count cannot fire; disjoint ranges → 0). Experiment E: NULL (complement, relational difference, and set normalization `A ∨ ¬A → All` each shown wrong on a NULL table and refused), no universe, IEEE (`f32` rounding), checked, impure (`Opaque` evaluated twice), `_sym` sums (the `Count` twin still fires), basis mismatch, bound past the universe, bag. Budget and catalogue-shape tests. +- **Tests (22):** 600 random measures over random two-valued tables, under exact (`i128`) and wrapping (`i64`) oracles, with random rule subsets (disabling any optimization keeps the answer): equal answers, size never grows, no refusal on valid input, most inputs rewritten (anti-vacuity). Every non-range rule fires on random input. Experiment A (relational difference vs the `i128` oracle; checked refuses, and the eager `i32` accumulator is the counterexample: the original overflows, the rewritten sum is 5). Experiment D (three ranges → intersect → `Const(20)`; with intersection disabled the count cannot fire; disjoint ranges → 0). Experiment E: NULL (complement, relational difference, and set normalization `A ∨ ¬A → All` each shown wrong on a NULL table and refused), no universe, IEEE (`f32` rounding), checked, impure (`Opaque` evaluated twice), `_sym` sums (the `Count` twin still fires), basis mismatch, bound past the universe, bag. Budget and catalogue-shape tests. - **Disable runs** (`cargo test -p lance-graph-contract --lib set_rules`): each guard removed in turn turns exactly the named test red — set-normalize three-valued (`experiment_e_null_refuses_set_normalization`), complement three-valued and universe, relational-difference three-valued / checked / IEEE / `_sym`, cancellation checked / IEEE / impure, range basis / past-universe, range-count bag; removing the size check fails the differential test. - **Codex review of #1651 (four findings, fixed):** complement for bags (multiplicities `[2, 1]`: `Count(¬A) = 1`, `N − Count(A) = 0`) and under checked / IEEE arithmetic; cancellation of a `_sym` sum; range count under IEEE. Each new guard has a test and its own disable run. +- **Codex review of #1654:** the range rules' no-universe refusal had no negative control; `experiment_e_no_universe_refuses_the_range_rules` added, disable run red. - **Gates:** contract lib 1,539 pass; relalg suite (own workspace) 26 pass, unchanged; clippy `-D warnings` and fmt clean. OPEN: repointing crepe and relalg onto `set_rules` (separate, after this); a prefix-lane `Sum([lo,hi)) → P[hi] − P[lo]` rule (needs a prefix lane, separate candidate); D-CMR-8 only if rules compete. diff --git a/.claude/board/entries/2026-10-21-d-ra-2-relalg-symbolic-repoint.md b/.claude/board/entries/2026-10-21-d-ra-2-relalg-symbolic-repoint.md new file mode 100644 index 000000000..187eb70b7 --- /dev/null +++ b/.claude/board/entries/2026-10-21-d-ra-2-relalg-symbolic-repoint.md @@ -0,0 +1,13 @@ +# 2026-10-21 — D-RA-2: relalg's symbolic answers repointed onto `contract::set_rules` (crepe through relalg) + +**Status:** TEST-PINNED, in PR (branch `claude/eager-albattani-iufugq`). **Basis:** six-decisions §2 ("D-CMR-6 publishes the catalogue → repoint crepe"); D-RA-2 option A; claim EXO-50 `session_013z2e1YXkm6o6HNrDn5BPWA/019`. + +- **What was duplicated:** `lance_graph_relalg::normalize::symbolic` decided `Count(∅) = 0`, `Sum(∅) = 0`, `Min/Max(∅) = None` and `Count(All) = n` by matching `Rel::Empty` / `Rel::All` locally — single-table measure identities outside the contract. +- **Contract (`set_rules`, two rules added):** `EmptyMeasure` (`Count(∅) → 0`, `Sum(∅) → 0`; refuses `_sym` sums, whose empty sum is a sentinel) and `CountAll` (`Count(All) → N`; refuses no universe, bag, IEEE). The catalogue has 8 rules. +- **relalg:** `symbolic` builds `set_rules::Measure::{Count, Sum}` from the query, rewrites it under relalg's semantics (`Semantics::exact(n_rows)`: two-valued planes and lanes, exact `i64` sums of `i32`, distinct rows) and answers only a `Const`. `Min`/`Max` answer `None` only when their `Count` folds to 0. Public signature unchanged. +- **crepe:** no code change. Its symbolic answers come from `lance_graph_relalg::run` → `symbolic`, so they now come from the contract. Its own `optimize.rs` rewrites (binding propagation, duplicate atom, duplicate rule) work on Datalog join bodies over several relations; they are not single-table identities and stay. +- **Tests:** contract `set_rules` 25 (3 new: empty/All folding against the oracle incl. after normalization; `_sym` refuses the empty sum; `Count(All)` refuses no universe / bag / IEEE). Two existing tests re-pinned because the new rules fire on their fixtures: the two-valued half of `experiment_e_null_refuses_set_normalization` now folds to `Const(3)`; `experiment_e_sym_family_refuses_cancelling_a_sum` also records `EmptyMeasure`'s `_sym` refusal. +- **Disable runs:** relalg `symbolic` → `None`: 3 relalg tests red (`a_contradiction_…`, `a_tautology_…`, `an_inequality_in_a_union_…`). Contract `Count(∅)` rule off: `a_contradiction_…` red. Contract `Count(All)` rule off: `a_tautology_…` and `an_inequality_…` red. So relalg's answers depend on the contract. Each new contract guard (empty-sum `_sym`, `Count(All)` universe / bag / IEEE) red when removed. +- **Gates:** relalg 26 unchanged; contract lib 1,547; crepe-plan-probe 46 pass unchanged (built against the repointed relalg and contract); clippy `-D warnings`, fmt clean. + +OPEN: `Min`/`Max` stay outside `set_rules::Measure` (their empty answer is `None`, not an integer); emptiness is decided by the contract's `Count`. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index d726cdc6e..4f8798545 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. -404 entries, 2026-08-06 .. 2026-10-21. +406 entries, 2026-08-06 .. 2026-10-21. | date | entry id | finding | file | |---|---|---|---| @@ -34,6 +34,7 @@ exactly one of them, never both. | 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-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-2` | | [2026-10-21-d-cmr-2-lowering.md](2026-10-21-d-cmr-2-lowering.md) | diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index 97b6f4d59..d7dd8525d 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -268,7 +268,7 @@ median of 101, tier named from the build's own report, answers asserted first. | sets with a universe, interval sets as values | OPEN (D-CMR-1) | | multi-run extents, two-dimensional sets, preimage | OPEN (D-CMR-2, -4, -5) | | chains composed before lowering | OPEN (D-CMR-3, -7) | -| repeated rule application, complement, relational difference | IN PR (D-CMR-6, `contract::set_rules`) | +| repeated rule application, complement, relational difference | SHIPPED (D-CMR-6, #1651, `contract::set_rules`) | | prefix aggregates | candidate | | value-arithmetic IR (`a+b` as an expression) | OPEN, shared with NAL §4 C and D-SQLP | | equality saturation | research (D-CMR-8) | diff --git a/crates/lance-graph-contract/src/set_rules.rs b/crates/lance-graph-contract/src/set_rules.rs index f7f097919..9dba6aad1 100644 --- a/crates/lance-graph-contract/src/set_rules.rs +++ b/crates/lance-graph-contract/src/set_rules.rs @@ -194,6 +194,10 @@ pub enum Rule { RangeIntersect, /// `Count([lo, hi)) → max(0, hi − lo)`. RangeCount, + /// `Count(∅) → 0` and `Sum(∅) → 0`. + EmptyMeasure, + /// `Count(All) → N`. + CountAll, } /// Why a rule whose pattern matched did not fire. @@ -236,6 +240,18 @@ pub const CATALOGUE: &[RuleSpec] = &[ requires: "two-valued sets; the result is strictly smaller", refuses: &[Refusal::NotTwoValued], }, + RuleSpec { + rule: Rule::EmptyMeasure, + pattern: "Count(∅) → 0; Sum(∅) → 0", + requires: "for a sum, plain sums (a `_sym` sum over no row is a sentinel)", + refuses: &[Refusal::SymFamily], + }, + RuleSpec { + rule: Rule::CountAll, + pattern: "Count(All) → N", + requires: "a fixed universe N of distinct rows; not IEEE", + refuses: &[Refusal::NoUniverse, Refusal::Bag, Refusal::Ieee], + }, RuleSpec { rule: Rule::Complement, pattern: "Count(¬A) → N − Count(A)", @@ -539,6 +555,35 @@ fn apply(rule: Rule, m: &Measure, sem: &Semantics) -> Option match m { + Measure::Count(SetExpr::Empty) => Some(Ok(Measure::Const(0))), + Measure::Sum { + set: SetExpr::Empty, + .. + } => { + if sem.sums == SumFamily::Sym { + return Some(Err(Refusal::SymFamily)); + } + Some(Ok(Measure::Const(0))) + } + _ => None, + }, + Rule::CountAll => { + let Measure::Count(SetExpr::All) = m else { + return None; + }; + let Some(n) = sem.universe else { + return Some(Err(Refusal::NoUniverse)); + }; + if sem.population == Population::Bag { + return Some(Err(Refusal::Bag)); + } + // Stepwise rounding of the count differs from one conversion. + if sem.arith == Arith::Ieee { + return Some(Err(Refusal::Ieee)); + } + Some(Ok(Measure::Const(i128::from(n)))) + } Rule::RangeCount => { let Measure::CountRows(rs) = m else { return None; @@ -1080,9 +1125,10 @@ mod tests { assert!(tr .refusals .contains(&(Rule::SetNormalize, Refusal::NotTwoValued))); - // Two-valued, the same expression is the whole universe. - let (r2, _) = rewrite(&m, &Semantics::exact(3), BUDGET); - assert_eq!(r2, Measure::Count(SetExpr::All)); + // 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]); + assert_eq!(r2, Measure::Const(3)); } #[test] @@ -1265,6 +1311,42 @@ mod tests { assert_eq!(tr.refusals, vec![(Rule::RangeCount, Refusal::PastUniverse)]); } + /// No universe: a range bound cannot be checked against the population, + /// so neither range rule fires (Codex review of #1654). + #[test] + fn experiment_e_no_universe_refuses_the_range_rules() { + let sem = Semantics { + universe: None, + ..Semantics::exact(0) + }; + let two = Measure::CountRows(vec![ + RowRange { + basis: 0, + lo: 0, + hi: 10, + }, + RowRange { + basis: 0, + lo: 5, + hi: 20, + }, + ]); + let (r, tr) = rewrite(&two, &sem, BUDGET); + assert_eq!(r, two); + assert_eq!( + tr.refusals, + vec![(Rule::RangeIntersect, Refusal::NoUniverse)] + ); + let one = Measure::CountRows(vec![RowRange { + basis: 0, + lo: 0, + hi: 10, + }]); + let (r, tr) = rewrite(&one, &sem, BUDGET); + assert_eq!(r, one); + assert_eq!(tr.refusals, vec![(Rule::RangeCount, Refusal::NoUniverse)]); + } + /// Bag: after fan-out a range holds rows with multiplicity, so /// `hi − lo` undercounts. #[test] @@ -1357,9 +1439,13 @@ mod tests { }; let (r, tr) = rewrite(&c, &sem, BUDGET); assert_eq!(r, c); + // `EmptyMeasure` refuses the `Sum(∅)` operands under `_sym` as well. assert_eq!( tr.refusals, - vec![(Rule::AdditiveCancellation, Refusal::SymFamily)] + vec![ + (Rule::AdditiveCancellation, Refusal::SymFamily), + (Rule::EmptyMeasure, Refusal::SymFamily), + ] ); // A dropped operand with no sum still cancels under `_sym`. let k = Measure::Count(SetExpr::Sym(0)); @@ -1391,6 +1477,102 @@ mod tests { assert_ne!(acc, (1u32 << 25) as f32); } + /// `Count(∅)` and `Sum(∅)` are 0; `Count(All)` is the universe. The + /// constant agrees with the oracle, including after normalization. + #[test] + fn empty_and_all_measures_fold_to_constants() { + let t = table(&mut Rng(19), 12, false, true); + let sem = Semantics::exact(12); + let cases = [ + (Measure::Count(SetExpr::Empty), 0), + ( + Measure::Sum { + lane: 0, + set: SetExpr::Empty, + }, + 0, + ), + (Measure::Count(SetExpr::All), 12), + // Normalization first: `S0 ∧ ¬S0` is empty, `S0 ∨ ¬S0` is All. + ( + Measure::Sum { + lane: 1, + set: SetExpr::And(vec![SetExpr::Sym(0), SetExpr::negated(SetExpr::Sym(0))]), + }, + 0, + ), + ( + Measure::Count(SetExpr::Or(vec![ + SetExpr::Sym(0), + SetExpr::negated(SetExpr::Sym(0)), + ])), + 12, + ), + ]; + for (m, want) in cases { + let (r, tr) = rewrite(&m, &sem, BUDGET); + assert_eq!(r, Measure::Const(want), "{m:?}: {tr:?}"); + assert_eq!(ev(&t, &m, Acc::Exact), Val::I(want)); + } + } + + /// `_sym`: a sum over no row is the sentinel, never 0. The count still + /// folds. + #[test] + fn sym_family_refuses_the_empty_sum() { + let sem = Semantics { + sums: SumFamily::Sym, + ..Semantics::exact(4) + }; + let m = Measure::Sum { + lane: 0, + set: SetExpr::Empty, + }; + let (r, tr) = rewrite(&m, &sem, BUDGET); + assert_eq!(r, m); + assert_eq!(tr.refusals, vec![(Rule::EmptyMeasure, Refusal::SymFamily)]); + assert_eq!( + rewrite(&Measure::Count(SetExpr::Empty), &sem, BUDGET).0, + Measure::Const(0) + ); + } + + /// `Count(All)` needs a universe of distinct rows, and not IEEE. + #[test] + fn count_all_refuses_without_universe_for_bags_and_under_ieee() { + let m = Measure::Count(SetExpr::All); + let mut t = table(&mut Rng(23), 3, false, false); + t.mult = vec![2, 1, 1]; + assert_ne!(ev(&t, &m, Acc::Exact), Val::I(3)); + for (sem, why) in [ + ( + Semantics { + universe: None, + ..Semantics::exact(0) + }, + Refusal::NoUniverse, + ), + ( + Semantics { + population: Population::Bag, + ..Semantics::exact(3) + }, + Refusal::Bag, + ), + ( + Semantics { + arith: Arith::Ieee, + ..Semantics::exact(3) + }, + Refusal::Ieee, + ), + ] { + let (r, tr) = rewrite(&m, &sem, BUDGET); + assert_eq!(r, m); + assert_eq!(tr.refusals, vec![(Rule::CountAll, why)]); + } + } + // ── driver ─────────────────────────────────────────────────────────── #[test] @@ -1415,7 +1597,7 @@ mod tests { sorted.sort(); sorted.dedup(); assert_eq!(sorted.len(), rules.len()); - assert_eq!(rules.len(), 6); + assert_eq!(rules.len(), 8); assert!(CATALOGUE.iter().all(|s| !s.refuses.is_empty())); } } diff --git a/crates/lance-graph-relalg/src/normalize.rs b/crates/lance-graph-relalg/src/normalize.rs index cde5000f3..f7f7efcc9 100644 --- a/crates/lance-graph-relalg/src/normalize.rs +++ b/crates/lance-graph-relalg/src/normalize.rs @@ -8,8 +8,13 @@ //! [`SetExpr`] (`Plane(i)` is the opaque set `Sym(i)`; an [`Atom`] is the //! residual [`Res`] with the same fields), normalized there, and converted //! back. The rule list is documented at the contract module. +//! +//! [`symbolic`] likewise asks the contract's rule catalogue +//! ([`lance_graph_contract::set_rules`], D-CMR-6) whether the measure folds +//! to a constant, instead of matching `Empty` / `All` here. use lance_graph_contract::set_algebra::{self as sa, Res, SetExpr}; +use lance_graph_contract::set_rules::{self as sr, Semantics}; use crate::ir::{Atom, Cmp, Measure, Rel}; use crate::lower::Answer; @@ -19,16 +24,36 @@ pub fn normalize(rel: &Rel) -> Rel { from_set(&sa::normalize(&to_set(rel))) } +/// Step budget for [`symbolic`]'s rewrite; every step shrinks the measure, so +/// a description this crate lowers reaches its fixpoint well inside it. +const SYMBOLIC_BUDGET: usize = 256; + /// The answer, if the description alone determines it: no row is read and /// no program runs. +/// +/// The decision is the contract's: the measure is rewritten by +/// [`set_rules::rewrite`](sr::rewrite) under this crate's semantics (planes +/// and lanes are two-valued, sums are exact `i64` over `i32`, rows are +/// distinct, the universe is `n_rows`), and answered only when it folds to a +/// constant. `Min` / `Max` are answered (`None`) only when the rows are +/// provably empty, i.e. when their `Count` folds to `0`. pub fn symbolic(rel: &Rel, m: Measure, n_rows: usize) -> Option { - match (rel, m) { - (Rel::Empty, Measure::Count) => Some(Answer::Count(0)), - (Rel::Empty, Measure::Sum(_)) => Some(Answer::Sum(0)), - (Rel::Empty, Measure::Min(_)) => Some(Answer::Min(None)), - (Rel::Empty, Measure::Max(_)) => Some(Answer::Max(None)), - (Rel::All, Measure::Count) => Some(Answer::Count(n_rows as u64)), - _ => None, + let set = to_set(rel); + let probe = match m { + Measure::Count | Measure::Min(_) | Measure::Max(_) => sr::Measure::Count(set), + Measure::Sum(lane) => sr::Measure::Sum { lane, set }, + Measure::Keep => return None, + }; + let sem = Semantics::exact(n_rows as u64); + let sr::Measure::Const(c) = sr::rewrite(&probe, &sem, SYMBOLIC_BUDGET).0 else { + return None; + }; + match m { + Measure::Count => u64::try_from(c).ok().map(Answer::Count), + Measure::Sum(_) => i64::try_from(c).ok().map(Answer::Sum), + Measure::Min(_) => (c == 0).then_some(Answer::Min(None)), + Measure::Max(_) => (c == 0).then_some(Answer::Max(None)), + Measure::Keep => None, } }