AdaWorldAPI · Oct 21, 2026 · Oct 21, 2026 · Oct 21, 2026 · Oct 21, 2026 · Oct 21, 2026
diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md
@@ -1,4 +1,16 @@
-## 2026-10-21 — D-CMR-2 lowering in core (in PR)
+## 2026-10-21 — D-CMR-6 rule catalogue in the contract (in PR)
+
+- **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`.
+
+### Current Contract Inventory — net delta (`set_rules.rs`)
+
+- `lance_graph_contract::set_rules` (new). No existing type changed.
+
+## 2026-10-21 — main after #1650 (merged `f031089`)
+
+- **On main:** #1648 (D-RU-6 arm C, `walk_sparse`), #1649, #1650 (D-CMR-2 `fold::set_lower`; D-CMR-5 re-scoped to BLOCKED: lawful design proposed). Contract inventory delta: none (core module, see the D-CMR-2 section below).
+
+## 2026-10-21 — D-CMR-2 lowering in core (#1650, merged `f031089`)
 
 - **Core (new module, no contract change):** `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured, LowerError}`. A `SetExpr` is normalized (contract) and split into `Runs ∩ residual`: comparisons on an attested sorted `i32` lane (`SortedBasis`, one attestation scan) become runs by counted binary-search seeks; the rest compiles once to a mask-risc `Program` run over each run with `execute_extent`. Levels: geometry (no residual, `Count = Σ(hi−lo)`, nothing read), optics (`Count` terminal), etch (`Keep` into `Out::Mask`, outside bits cleared). `SetPlan::unsplit` is the geometry-off arm. Entry `entries/2026-10-21-d-cmr-2-lowering.md`.
 - Open: D-CMR-2b, a scratch-free `Pred` fold in mask-risc (`fused_ternlog` declines `Pred`); residual comparisons run tiled with per-tile scratch.

diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md
@@ -1,3 +1,10 @@
+## 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`.
+- **Locked:** a normalized `SetExpr` splits into `Runs` (counted seeks on an attested sorted `i32` lane) ∩ residual (one mask-risc program per run via `execute_extent`); geometry reads nothing, optics counts, etch keeps; attest / seek / query costs reported apart. D-CMR-5 reads "BLOCKED: lawful design proposed" per the operator's 2026-10-21 ruling (Q1 = C, Q2 = B conditionally).
+- **Deferred / open:** D-CMR-2b (scratch-free `Pred` fold in mask-risc, a measured performance experiment, not authorized); a facet / `u32` sorted basis; D-CMR-5's contract-level codebook witness.
+- **Confidence:** measured. 6 tests (row oracle over 400 random expressions at every level; geometry against empty planes, 0 extents); 4 disable runs red; clippy and fmt clean; CI green; Codex no findings.
+
 ## 2026-10-21 — lance-graph PR #1644 (merged `c05a313`, branch `claude/eager-albattani-iufugq`, head `6fc04a4`) — D-CMR-1 / D-RA-2: the contract owns single-table set algebra
 
 - **Added:** `lance_graph_contract::set_algebra::{SetExpr, Res, Cmp, normalize, Runs, OutOfUniverse}` (zero deps); relalg `tests/absorption_n17.rs`; entry `2026-10-20-d-cmr-1-set-algebra.md`.

diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md
@@ -255,11 +255,11 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES
 |---|---|---|---|
 | **D-CMR-0** | Plan, identity matrix, inventory, board rows | Shipped #1532 (docs) | docs only; every inventory row cites code |
 | **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | Shipped (#1644, `c05a313`): `contract::set_algebra::{SetExpr, Res, Runs, normalize}`; measures not yet (`entries/2026-10-20-d-cmr-1-set-algebra.md`) | algebra laws vs materialized bitsets as oracle |
-| **D-CMR-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | In PR (branch `claude/eager-albattani-iufugq`): `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured}`; geometry reads nothing, optics/etch run the residual per run via `execute_extent`. The scratch-free `Pred` fold in mask-risc is D-CMR-2b, not built (`entries/2026-10-21-d-cmr-2-lowering.md`) | == row oracle; `Count` without residual reads zero rows |
+| **D-CMR-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | Shipped (#1650, `f031089`): `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured}`; geometry reads nothing, optics/etch run the residual per run via `execute_extent`. The scratch-free `Pred` fold in mask-risc is D-CMR-2b, not built (`entries/2026-10-21-d-cmr-2-lowering.md`) | == row oracle; `Count` without residual reads zero rows |
 | **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 | Queued | Experiments A, D, E; each guard removal fails |
+| **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-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-2-lowering.md b/.claude/board/entries/2026-10-21-d-cmr-2-lowering.md
@@ -1,6 +1,6 @@
 # 2026-10-21 — D-CMR-2: the contract set algebra lowered onto mask-risc
 
-**Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** plan `d-cmr-concept-chain-normalization-v1.md` §3.4 and the D-CMR-2 row; ADMISSION B (`2026-10-20-six-decisions.md` §1) for the seeks.
+**Status:** TEST-PINNED, merged in #1650 (`f031089`); Codex review completed with no findings. **Basis:** plan `d-cmr-concept-chain-normalization-v1.md` §3.4 and the D-CMR-2 row; ADMISSION B (`2026-10-20-six-decisions.md` §1) for the seeks.
 
 - **Where:** `crates/lance-graph/src/fold/set_lower.rs` (`lance_graph::fold::set_lower`). Core already depends on the contract and mask-risc unconditionally; no new dependency.
 - **Split:** `SetPlan::new(&SetExpr, n_rows, Option<&SortedBasis>)` normalizes, then takes `Runs` from comparisons on the attested sorted lane (an exact basis-only expression, or the basis conjuncts of a top-level `And`) and leaves the rest as the residual. Mixed `Or`s stay residual and spend no seeks.

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
@@ -0,0 +1,24 @@
+# 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`.
+
+- **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 }`.
+- **Catalogue (`CATALOGUE`, data: rule, pattern, requires, refusals):**
+
+  | rule | rewrite | refuses on |
+  |---|---|---|
+  | `SetNormalize` | the set inside `Count`/`Sum` → `normalize` | three-valued |
+  | `Complement` | `Count(¬A) → N − Count(A)` | three-valued; no universe; bag; checked; IEEE |
+  | `RelationalDifference` | `Sum(A) − Sum(A∧B) → Sum(A∧¬B)`; `Count` likewise | three-valued; checked; IEEE; `_sym` sums |
+  | `AdditiveCancellation` | `(a+b) − a → b` | checked; IEEE; impure `a`; a `_sym` sum in `a` |
+  | `RangeIntersect` | `⋂[loᵢ,hiᵢ) → [max lo, min hi)` | basis mismatch; no universe; bound past it |
+  | `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.
+- **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.
+- **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/README.md b/.claude/board/entries/README.md
@@ -25,13 +25,14 @@ 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.
 
-402 entries, 2026-08-06 .. 2026-10-21.
+403 entries, 2026-08-06 .. 2026-10-21.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-21 | `D-RU-2` |  | [2026-10-21-u2-let-planes.md](2026-10-21-u2-let-planes.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-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) |
 | 2026-10-20 | `D-RU-1` |  | [2026-10-20-u1-jc-batch.md](2026-10-20-u1-jc-batch.md) |

diff --git 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 | OPEN (D-CMR-6) |
+| repeated rule application, complement, relational difference | IN PR (D-CMR-6, `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/lib.rs b/crates/lance-graph-contract/src/lib.rs
@@ -194,6 +194,9 @@ pub mod set_algebra;
 /// D-RU-2 / U2: a batch of selections whose shared parts are named once
 /// (`lets` over `set_algebra::SetExpr::Sym`). See module docs.
 pub mod set_program;
+/// D-CMR-6: guarded rewrite rules over measures (Count / Sum / ranges) and the
+/// fixpoint driver. See module docs.
+pub mod set_rules;
 pub mod settlement;
 /// D-BLW-5 payload-law DTO (`ShapeRankPayload`, `RemeasureKey`, `RemeasureLedger`) —
 /// distribution shape × Prozentrang, never the raw statistic. See module docs.