D-RA-2: relalg symbolic answers from contract::set_rules + #1651 closeout

.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`.
 

.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`.

.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 |

.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<RowRange>) | 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.

.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`.

.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) |

.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) |