From 1ef8e318e0ebeedb5c5deb6064587177ae367ee0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 23:54:44 +0000 Subject: [PATCH 1/4] D-CMR-1 / D-RA-2: contract owns single-table set algebra; relalg delegates lance_graph_contract::set_algebra (zero dependencies): - SetExpr {All, Empty, Sym, Res, And, Or, Not}, Res (one-lane residual), Cmp; normalize = the one implementation of the single-table rewrites (De Morgan, associative flattening, idempotence, complement pairs, per-lane interval fusion/merge, absorption). - Absorption is matched against flattened sibling sets, one child at a time: closes ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN (N17). - Runs: sorted disjoint half-open intervals with intersect / union / difference / complement(universe); complement refuses a set past the declared universe. - Tests: differential vs materialized bitsets (3,000 random nested expressions), no leaf growth, N17 + dual, partial-cover silence twin, flatten-before-depth, Runs laws vs bitsets incl. empty/full/boundary. lance-graph-relalg: normalize converts Rel <-> SetExpr and delegates. Public API unchanged; the 16 existing tests pass unchanged; N17 regression in tests/absorption_n17.rs. Disable runs recorded in entries/2026-10-20-d-cmr-1-set-algebra.md. Board: LATEST_STATE contract inventory, STATUS_BOARD D-CMR-1 / D-RA-2, ISSUES N17, entry + index. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/ISSUES.md | 2 +- .claude/board/LATEST_STATE.md | 9 + .claude/board/STATUS_BOARD.md | 4 +- .../entries/2026-10-20-d-cmr-1-set-algebra.md | 19 + .claude/board/entries/README.md | 3 +- crates/lance-graph-contract/src/lib.rs | 1 + .../lance-graph-contract/src/set_algebra.rs | 922 ++++++++++++++++++ crates/lance-graph-relalg/Cargo.toml | 3 + crates/lance-graph-relalg/src/normalize.rs | 382 ++------ .../tests/absorption_n17.rs | 36 + 10 files changed, 1071 insertions(+), 310 deletions(-) create mode 100644 .claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md create mode 100644 crates/lance-graph-contract/src/set_algebra.rs create mode 100644 crates/lance-graph-relalg/tests/absorption_n17.rs diff --git a/.claude/board/ISSUES.md b/.claude/board/ISSUES.md index 6df1779c1..5862acf44 100644 --- a/.claude/board/ISSUES.md +++ b/.claude/board/ISSUES.md @@ -78,7 +78,7 @@ ## ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN — `normalize` can leave a program wider than as written (2026-10-16) -**Status:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs). +**Status:** RESOLVED in PR (D-CMR-1, branch `claude/eager-albattani-iufugq`): absorption is matched against flattened sibling sets in `contract::set_algebra::normalize`; TEST-PINNED by `absorption_after_de_morgan_matches_flattened_siblings` (contract) and `tests/absorption_n17.rs` (relalg), both disable-verified red. **Was:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs). - `¬(x ∧ (x ∨ y))` with `x = P1 ∧ P4` should reduce by absorption to `¬x = ¬P1 ∨ ¬P4`. `lance-graph-relalg::normalize` pushes the negation inward first (De Morgan), flattens, and returns `¬P1 ∨ ¬P4 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5 ∧ ¬P7)`: the dual absorption pattern `a ∨ (a ∧ b)` is present but `a` is spread across the flattened `Or`, so the rule no longer matches. - Consequence: the rewritten program needs more scratch slots than the original; the original answers, the rewrite is refused (`MAX_SLOTS` = 8). Answers are never wrong; only width. diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index aafe46203..e6a815869 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,12 @@ +## 2026-10-20 — D-CMR-1 / D-RA-2: single-table set algebra in the contract (in PR) + +- **Contract (new module):** `set_algebra::{SetExpr, Res, Cmp, normalize, Runs, OutOfUniverse}`. `SetExpr` = `All | Empty | Sym(u32) | Res(Res) | And | Or | Not`; `Sym` is an opaque two-valued set (no storage layout named), `Res` a residual predicate on one lane. `normalize` is the one implementation of the single-table rewrites (De Morgan, associative flattening, idempotence, complement pairs, per-lane interval fusion and merge, absorption matched against flattened siblings). `Runs` = sorted disjoint half-open row intervals with `∩ ∪ ∖` and `complement(universe)`, refused (`OutOfUniverse`) past the declared universe. No dependency added; no lowering, join or gather. +- **relalg:** `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`) and delegates; public API unchanged; the 16 pre-existing tests pass unchanged. Closes `ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN` (N17). Entry `entries/2026-10-20-d-cmr-1-set-algebra.md`. + +### Current Contract Inventory — net delta (`set_algebra.rs`) + +- `lance_graph_contract::set_algebra::{Cmp, Res, SetExpr, normalize, Runs, OutOfUniverse}` — see above. 10 tests: differential `normalize` vs materialized bitsets (3,000 random nested expressions, anti-vacuity on rewrite rate), no leaf growth, N17 and its dual, partial-cover silence twin, flatten-before-depth, De Morgan / complement pairs, `Runs` laws vs bitsets (universes 0..100), explicit-universe refusal. + ## 2026-10-20 — main after #1626 (merged `bc8012da`) - **On main:** #1621 (`fcd1f60e`, D-RMAP focus probe and native join), #1622 (`4dbd0853`, plans D-RST and D-RPR), #1623 (`8b570ed3`, D-RMAP-2 tile-GEMM cell, polyfill tier), #1624 (`7d2722bd`, consolidation, plan links, D-RPR-1 handoff probe), #1625 (`37b866ee`, BF16 byte count), #1626 (`bc8012da`, D-RMAP-2 on the AMX tier). All six have arc entries. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index aa19ce69b..c34a7ebba 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -227,7 +227,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). Next: D-CMR-1 | 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). In PR with D-CMR-1: relalg `normalize` delegates to `contract::set_algebra::normalize`; remaining rules (none in relalg today) and repointing crepe follow D-CMR-6 | 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 | @@ -238,7 +238,7 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES | D-id | scope | status | gate / falsifier | |---|---|---|---| | **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 | Queued — first architecture PR after the D-RA-2 decision (`entries/2026-10-20-six-decisions.md` §2) | algebra laws vs materialized bitsets as oracle | +| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | In PR (branch `claude/eager-albattani-iufugq`): `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 | Queued (after D-CMR-1; lowering reaches mask-risc through core via `lance_graph::fold`, #1537 — there is no contract → mask-risc edge) | == 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 | diff --git a/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md new file mode 100644 index 000000000..0a30c4065 --- /dev/null +++ b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md @@ -0,0 +1,19 @@ +# 2026-10-20 — D-CMR-1 / D-RA-2: the contract owns single-table set algebra + +**Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`). + +- **Moved:** relalg's rewrite rules to `lance_graph_contract::set_algebra::normalize`, unchanged except absorption. relalg's `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`, `Atom` ↔ `Res`) and delegates. `symbolic`, `run`, lowering and the public API are unchanged. The contract stays dependency-free. +- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept. That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`). +- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`. `complement(universe)` refuses a set that reaches past the universe. +- **Regression:** the 16 pre-existing relalg tests pass unchanged. 3 tests are new: `conversion_round_trips` plus 2 in `tests/absorption_n17.rs`. +- **Disable runs** (commands: `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml --no-fail-fast` and `cargo test -p lance-graph-contract --lib set_algebra`): + + | probe | what breaks | + |---|---| + | contract `normalize` returns its input | 10 of 14 `rewrites.rs` tests, and both N17 tests in relalg | + | generalized absorption off | only the N17 tests: one in relalg, two in the contract | + | absorption on a partial cover (`all` → `any`) | the silence twin, and the bitset differential (an unsound rule) | + +- **Scope held:** no joins, gathers, positional addressing, recursion, D-MPS-8 or `graph_hop`. Measures (`Count`/`Sum` on `Runs`) are not in this PR. + +OPEN: D-CMR-6 catalogue; repointing crepe and Quack at the contract. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 091796db8..abd5bb16a 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. -394 entries, 2026-08-06 .. 2026-10-20. +395 entries, 2026-08-06 .. 2026-10-20. | date | entry id | finding | file | |---|---|---|---| @@ -46,6 +46,7 @@ exactly one of them, never both. | 2026-10-20 | `D-RMAP-2` | | [2026-10-20-d-rmap-2-tile-gemm-cell.md](2026-10-20-d-rmap-2-tile-gemm-cell.md) | | 2026-10-20 | `D-RMAP-2-AMX` | | [2026-10-20-d-rmap-2-amx-tier.md](2026-10-20-d-rmap-2-amx-tier.md) | | 2026-10-20 | `D-RMAP-2-AMX-RERUN` | §5a-AMX re-measured on a second AMX host | [2026-10-20-d-rmap-2-amx-remeasured.md](2026-10-20-d-rmap-2-amx-remeasured.md) | +| 2026-10-20 | `D-CMR-1` | | [2026-10-20-d-cmr-1-set-algebra.md](2026-10-20-d-cmr-1-set-algebra.md) | | 2026-10-20 | `D-SRAM-2` | | [2026-10-20-crepe-rule-optimizer-spike.md](2026-10-20-crepe-rule-optimizer-spike.md) | | 2026-10-20 | `ce64-isa-not-storage` | | [2026-10-20-ce64-isa-not-storage.md](2026-10-20-ce64-isa-not-storage.md) | | 2026-10-20 | `arm-b-prepare` | | [2026-10-20-arm-b-prepare.md](2026-10-20-arm-b-prepare.md) | diff --git a/crates/lance-graph-contract/src/lib.rs b/crates/lance-graph-contract/src/lib.rs index f05c2192b..2ec79c93a 100644 --- a/crates/lance-graph-contract/src/lib.rs +++ b/crates/lance-graph-contract/src/lib.rs @@ -190,6 +190,7 @@ pub mod scenario; pub mod scheduler; pub mod selection; pub mod sensorium; +pub mod set_algebra; pub mod settlement; /// D-BLW-5 payload-law DTO (`ShapeRankPayload`, `RemeasureKey`, `RemeasureLedger`) — /// distribution shape × Prozentrang, never the raw statistic. See module docs. diff --git a/crates/lance-graph-contract/src/set_algebra.rs b/crates/lance-graph-contract/src/set_algebra.rs new file mode 100644 index 000000000..2dd801609 --- /dev/null +++ b/crates/lance-graph-contract/src/set_algebra.rs @@ -0,0 +1,922 @@ +//! Single-table set algebra: what a selection MEANS, independent of how any +//! executor stores or evaluates it (D-CMR-1 / D-RA-2, `ADR-2026-10-20-SIX` §2). +//! +//! ```text +//! lance-graph-contract::set_algebra +//! (SetExpr, Res, Runs, normalize: the one implementation) +//! ▲ ▲ ▲ +//! relalg (lowers Quack (later) crepe / R2IL (later) +//! to mask-risc) +//! ``` +//! +//! # What lives here, and what does not +//! +//! - [`SetExpr`]: a description of one population's subset. A [`SetExpr::Sym`] +//! is an opaque two-valued set (an executor may bind it to a plane, a +//! bitmap, anything); a [`Res`] is a residual predicate on one lane. Neither +//! names a storage layout. Bitsets are consumers of this meaning, not part +//! of it. +//! - [`normalize`]: the rewrite to an equivalent, cheaper description. It +//! reads no row and builds nothing. +//! - [`Runs`]: sorted, disjoint, half-open row intervals, closed under `∩`, +//! `∪`, `∖`, and complement against an EXPLICIT universe. +//! +//! Not here: joins, gathers, positional addressing across tables, recursion, +//! lowering, execution. A consumer owns those. +//! +//! # Rewrites (all run to a fixpoint) +//! +//! 1. Negation is pushed to the leaves (De Morgan); a negated comparison +//! becomes the opposite comparison. +//! 2. `And` / `Or` are flattened (associativity), so the depth a consumer +//! admits is measured on normalized structure, never parser nesting; +//! `All` / `Empty` are absorbed or dominate; duplicates are removed +//! (idempotence); `p ∧ ¬p` is `Empty`, `p ∨ ¬p` is `All`. +//! 3. In an `And`, every comparison on one `I32` lane becomes one interval +//! (plus the excluded values inside it); an empty interval makes the whole +//! conjunction `Empty`. Equalities on one `U32` lane agree or contradict. +//! 4. In an `Or`, intervals on one `I32` lane that overlap or touch merge; a +//! union covering the whole lane is `All`. +//! 5. Absorption, matched against FLATTENED sibling sets: in an `Or`, a dual +//! child `And(ms)` is dropped when some member `m` is already covered by +//! the siblings (`m` is a sibling, or `m` is an `Or` whose members are all +//! siblings); dually in an `And`. This closes +//! ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN: `¬(x ∧ (x ∨ y))` with +//! `x = P1 ∧ P4` is `¬P1 ∨ ¬P4`, not the wider form De Morgan emits. +//! +//! No rewrite distributes, so normalization never grows an expression +//! exponentially to remove nesting. +//! +//! An interval is always emitted as `<` / `>` bounds or one `==`. +//! +//! Zero dependencies. + +use std::collections::{BTreeMap, BTreeSet}; + +/// An ordered comparison against a constant. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Cmp { + Lt, + Le, + Gt, + Ge, + Eq, + Ne, +} + +/// A residual predicate on one lane of the table: opaque to interval +/// reasoning except for what its own lane type licenses. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Res { + /// `lane op t` over signed 32-bit values. + I32 { lane: u16, op: Cmp, t: i32 }, + /// `lane == v` (`eq`) or `lane != v` (`!eq`) over unsigned 32-bit codes. + U32 { lane: u16, eq: bool, v: u32 }, +} + +impl Res { + /// The complement predicate (two-valued: a row either satisfies it or + /// not). + pub fn negate(self) -> Res { + match self { + Res::I32 { lane, op, t } => Res::I32 { + lane, + t, + op: match op { + Cmp::Lt => Cmp::Ge, + Cmp::Ge => Cmp::Lt, + Cmp::Le => Cmp::Gt, + Cmp::Gt => Cmp::Le, + Cmp::Eq => Cmp::Ne, + Cmp::Ne => Cmp::Eq, + }, + }, + Res::U32 { lane, eq, v } => Res::U32 { lane, eq: !eq, v }, + } + } +} + +/// A description of a subset of one population. The variant order is part +/// of the contract: [`normalize`] sorts siblings by it. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum SetExpr { + /// The whole universe. + All, + /// The empty set. + Empty, + /// An opaque two-valued set, identified by number. What carries it is the + /// consumer's business. + Sym(u32), + /// A residual predicate on one lane. + Res(Res), + And(Vec), + Or(Vec), + Not(Box), +} + +impl SetExpr { + pub fn i32(lane: u16, op: Cmp, t: i32) -> SetExpr { + SetExpr::Res(Res::I32 { lane, op, t }) + } + + pub fn eq_u32(lane: u16, v: u32) -> SetExpr { + SetExpr::Res(Res::U32 { lane, eq: true, v }) + } + + pub fn ne_u32(lane: u16, v: u32) -> SetExpr { + SetExpr::Res(Res::U32 { lane, eq: false, v }) + } + + pub fn negated(e: SetExpr) -> SetExpr { + SetExpr::Not(Box::new(e)) + } + + /// Nesting depth of junctions (`And` / `Or` / `Not`); a leaf is 0. After + /// [`normalize`] this is the depth of the flattened structure. + pub fn depth(&self) -> usize { + match self { + SetExpr::And(cs) | SetExpr::Or(cs) => { + 1 + cs.iter().map(SetExpr::depth).max().unwrap_or(0) + } + SetExpr::Not(c) => 1 + c.depth(), + _ => 0, + } + } + + /// Number of leaves (`Sym` and `Res`). + pub fn leaves(&self) -> usize { + match self { + SetExpr::Sym(_) | SetExpr::Res(_) => 1, + SetExpr::And(cs) | SetExpr::Or(cs) => cs.iter().map(SetExpr::leaves).sum(), + SetExpr::Not(c) => c.leaves(), + _ => 0, + } + } +} + +const LO: i64 = i32::MIN as i64; +const HI: i64 = i32::MAX as i64; + +/// Rewrite `e` to an equivalent description, to a fixpoint (at most 64 +/// rounds; every rewrite shrinks or keeps the expression). +pub fn normalize(e: &SetExpr) -> SetExpr { + let mut cur = nnf(e, false); + for _ in 0..64 { + let next = simplify(&cur); + if next == cur { + return next; + } + cur = next; + } + cur +} + +/// Negation normal form: `Not` survives only around a `Sym`. +fn nnf(e: &SetExpr, neg: bool) -> SetExpr { + match e { + SetExpr::All if neg => SetExpr::Empty, + SetExpr::Empty if neg => SetExpr::All, + SetExpr::Sym(_) if neg => SetExpr::negated(e.clone()), + SetExpr::Res(r) if neg => SetExpr::Res(r.negate()), + SetExpr::All | SetExpr::Empty | SetExpr::Sym(_) | SetExpr::Res(_) => e.clone(), + SetExpr::Not(c) => nnf(c, !neg), + SetExpr::And(cs) | SetExpr::Or(cs) => { + let cs = cs.iter().map(|c| nnf(c, neg)).collect(); + match (e, neg) { + (SetExpr::And(_), false) | (SetExpr::Or(_), true) => SetExpr::And(cs), + _ => SetExpr::Or(cs), + } + } + } +} + +fn simplify(e: &SetExpr) -> SetExpr { + match e { + SetExpr::All | SetExpr::Empty | SetExpr::Sym(_) => e.clone(), + SetExpr::Res(_) => conj(vec![e.clone()]), + SetExpr::Not(c) => match simplify(c) { + 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()), + } +} + +fn complement(e: &SetExpr) -> Option { + match e { + SetExpr::Sym(_) => Some(SetExpr::negated(e.clone())), + SetExpr::Not(x) => Some((**x).clone()), + _ => None, + } +} + +/// `[lo, hi]` as `<` / `>` bounds or one `==`; empty for the whole lane. +fn emit_interval(lane: u16, lo: i64, hi: i64) -> Vec { + if lo == hi { + return vec![SetExpr::i32(lane, Cmp::Eq, lo as i32)]; + } + let mut v = Vec::new(); + if hi < HI { + v.push(SetExpr::i32(lane, Cmp::Lt, (hi + 1) as i32)); + } + if lo > LO { + v.push(SetExpr::i32(lane, Cmp::Gt, (lo - 1) as i32)); + } + v +} + +/// The interval an ordered comparison or equality selects; `None` for `!=`. +fn interval(op: Cmp, t: i32) -> Option<(i64, i64)> { + let t = i64::from(t); + Some(match op { + Cmp::Lt => (LO, t - 1), + Cmp::Le => (LO, t), + Cmp::Gt => (t + 1, HI), + Cmp::Ge => (t, HI), + Cmp::Eq => (t, t), + Cmp::Ne => return None, + }) +} + +/// A conjunction of simplified children. +fn conj(children: Vec) -> SetExpr { + let mut flat = Vec::new(); + for c in children { + match c { + SetExpr::And(cs) => flat.extend(cs), + SetExpr::Empty => return SetExpr::Empty, + SetExpr::All => {} + c => flat.push(c), + } + } + let mut ranges: BTreeMap)> = BTreeMap::new(); + let mut eqs: BTreeMap, BTreeSet)> = BTreeMap::new(); + let mut rest = Vec::new(); + for c in flat { + match c { + SetExpr::Res(Res::I32 { lane, op, t }) => { + let e = ranges.entry(lane).or_insert((LO, HI, BTreeSet::new())); + match interval(op, t) { + Some((lo, hi)) => { + e.0 = e.0.max(lo); + e.1 = e.1.min(hi); + } + None => { + e.2.insert(i64::from(t)); + } + } + } + SetExpr::Res(Res::U32 { lane, eq, v }) => { + let e = eqs.entry(lane).or_default(); + if eq { &mut e.0 } else { &mut e.1 }.insert(v); + } + c => rest.push(c), + } + } + let mut out = Vec::new(); + for (lane, (mut lo, mut hi, excl)) in ranges { + while lo <= hi && excl.contains(&lo) { + lo += 1; + } + while lo <= hi && excl.contains(&hi) { + hi -= 1; + } + 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)); + } + } + } + for (lane, (is, nots)) in eqs { + let mut is = is.into_iter(); + match (is.next(), is.next()) { + (Some(_), Some(_)) => return SetExpr::Empty, + (Some(v), None) if nots.contains(&v) => return SetExpr::Empty, + (Some(v), None) => out.push(SetExpr::eq_u32(lane, v)), + _ => out.extend(nots.into_iter().map(|v| SetExpr::ne_u32(lane, v))), + } + } + out.extend(rest); + finish(out, true) +} + +/// A disjunction of simplified children. +fn disj(children: Vec) -> SetExpr { + let mut flat = Vec::new(); + for c in children { + match c { + SetExpr::Or(cs) => flat.extend(cs), + SetExpr::All => return SetExpr::All, + SetExpr::Empty => {} + c => flat.push(c), + } + } + let mut ranges: BTreeMap> = BTreeMap::new(); + let mut excluded: BTreeMap> = BTreeMap::new(); + let mut eqs: BTreeMap, BTreeSet)> = BTreeMap::new(); + let mut rest = Vec::new(); + for c in flat { + if let Some((lane, lo, hi)) = as_interval(&c) { + ranges.entry(lane).or_default().push((lo, hi)); + continue; + } + match c { + SetExpr::Res(Res::I32 { + lane, + op: Cmp::Ne, + t, + }) => { + excluded.entry(lane).or_default().insert(i64::from(t)); + } + SetExpr::Res(Res::U32 { lane, eq, v }) => { + let e = eqs.entry(lane).or_default(); + if eq { &mut e.0 } else { &mut e.1 }.insert(v); + } + c => rest.push(c), + } + } + let mut out = Vec::new(); + // `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. + for (lane, ne) in excluded { + let mut ne = ne.into_iter(); + let (Some(a), None) = (ne.next(), ne.next()) else { + return SetExpr::All; + }; + let iv = ranges.remove(&lane).unwrap_or_default(); + if iv.iter().any(|&(lo, hi)| lo <= a && a <= hi) { + return SetExpr::All; + } + out.push(SetExpr::i32(lane, Cmp::Ne, a as i32)); + } + for (lane, mut iv) in ranges { + iv.sort_unstable(); + let mut merged: Vec<(i64, i64)> = Vec::new(); + for (lo, hi) in iv { + match merged.last_mut() { + Some(last) if lo <= last.1 + 1 => last.1 = last.1.max(hi), + _ => merged.push((lo, hi)), + } + } + for (lo, hi) in merged { + let atoms = emit_interval(lane, lo, hi); + match atoms.len() { + 0 => return SetExpr::All, + 1 => out.extend(atoms), + _ => out.push(finish(atoms, true)), + } + } + } + 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))), + } + } + out.extend(rest); + finish(out, false) +} + +/// The interval a simplified child selects on one lane, if it is exactly one. +fn as_interval(c: &SetExpr) -> Option<(u16, i64, i64)> { + let one = |r: &SetExpr| match r { + SetExpr::Res(Res::I32 { lane, op, t }) => interval(*op, *t).map(|(lo, hi)| (*lane, lo, hi)), + _ => None, + }; + match c { + SetExpr::Res(_) => one(c), + SetExpr::And(cs) if !cs.is_empty() => { + let mut acc: Option<(u16, i64, i64)> = None; + for x in cs { + let (lane, lo, hi) = one(x)?; + acc = Some(match acc { + None => (lane, lo, hi), + Some((l, a, b)) if l == lane => (l, a.max(lo), b.min(hi)), + Some(_) => return None, + }); + } + acc.filter(|&(_, lo, hi)| lo <= hi) + } + _ => None, + } +} + +/// Whether `m` is covered by `sibs` in a junction of kind `and`: inside an +/// `Or` (`and == false`), `m ⊆ ⋃ sibs`; inside an `And`, `m ⊇ ⋂ sibs`. True +/// when `m` is a sibling, or `m` is the parent's own kind (an `Or` inside an +/// `Or`'s dual child, an `And` inside an `And`'s) with every member a sibling. +fn covered(m: &SetExpr, sibs: &[&SetExpr], and: bool) -> bool { + if sibs.contains(&m) { + return true; + } + match (m, and) { + (SetExpr::Or(ks), false) | (SetExpr::And(ks), true) => { + !ks.is_empty() && ks.iter().all(|k| sibs.contains(&k)) + } + _ => false, + } +} + +/// Sort, deduplicate, apply complement and absorption, and collapse. +fn finish(mut out: Vec, and: bool) -> SetExpr { + out.sort(); + out.dedup(); + let (unit, zero) = if and { + (SetExpr::All, SetExpr::Empty) + } else { + (SetExpr::Empty, SetExpr::All) + }; + if out + .iter() + .any(|c| complement(c).is_some_and(|n| out.binary_search(&n).is_ok())) + { + return zero; + } + // Absorption against the flattened siblings. Children are dropped one at + // a time and each test uses only the children still kept, so two dual + // children can never justify dropping each other. + let mut i = 0; + while i < out.len() { + let drop = match (&out[i], and) { + (SetExpr::Or(ms), true) | (SetExpr::And(ms), false) => { + let sibs: Vec<&SetExpr> = out + .iter() + .enumerate() + .filter(|&(j, _)| j != i) + .map(|(_, s)| s) + .collect(); + ms.iter().any(|m| covered(m, &sibs, and)) + } + _ => false, + }; + if drop { + out.remove(i); + } else { + i += 1; + } + } + match out.len() { + 0 => unit, + 1 => out.pop().unwrap_or(unit), + _ if and => SetExpr::And(out), + _ => SetExpr::Or(out), + } +} + +/// A universe was violated: an interval reached past the population size the +/// caller declared. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct OutOfUniverse { + pub universe: u64, + pub end: u64, +} + +/// Sorted, disjoint, non-adjacent, non-empty half-open row intervals +/// `[lo, hi)`. Closed under `∩`, `∪`, `∖` at a cost linear in the number of +/// intervals, with no row read. +#[derive(Debug, Clone, Default, PartialEq, Eq, Hash)] +pub struct Runs { + runs: Vec<(u64, u64)>, +} + +impl Runs { + /// The empty set. + pub fn empty() -> Runs { + Runs::default() + } + + /// `[0, universe)`. + pub fn full(universe: u64) -> Runs { + Runs::from_intervals([(0, universe)]) + } + + /// Canonicalize arbitrary intervals: empty ones dropped, overlapping or + /// touching ones merged. + pub fn from_intervals(iv: impl IntoIterator) -> Runs { + let mut v: Vec<(u64, u64)> = iv.into_iter().filter(|&(lo, hi)| lo < hi).collect(); + v.sort_unstable(); + let mut runs: Vec<(u64, u64)> = Vec::with_capacity(v.len()); + for (lo, hi) in v { + match runs.last_mut() { + Some(last) if lo <= last.1 => last.1 = last.1.max(hi), + _ => runs.push((lo, hi)), + } + } + Runs { runs } + } + + /// The canonical intervals. + pub fn intervals(&self) -> &[(u64, u64)] { + &self.runs + } + + pub fn is_empty(&self) -> bool { + self.runs.is_empty() + } + + /// Number of rows. + pub fn count(&self) -> u64 { + self.runs.iter().map(|&(lo, hi)| hi - lo).sum() + } + + pub fn contains(&self, row: u64) -> bool { + let i = self.runs.partition_point(|&(_, hi)| hi <= row); + self.runs.get(i).is_some_and(|&(lo, _)| lo <= row) + } + + /// The exclusive upper end of the last interval, or 0. + pub fn end(&self) -> u64 { + self.runs.last().map_or(0, |&(_, hi)| hi) + } + + pub fn union(&self, o: &Runs) -> Runs { + Runs::from_intervals(self.runs.iter().chain(o.runs.iter()).copied()) + } + + pub fn intersect(&self, o: &Runs) -> Runs { + let (mut i, mut j) = (0, 0); + let mut out = Vec::new(); + while i < self.runs.len() && j < o.runs.len() { + let (a, b) = (self.runs[i], o.runs[j]); + let (lo, hi) = (a.0.max(b.0), a.1.min(b.1)); + if lo < hi { + out.push((lo, hi)); + } + if a.1 < b.1 { + i += 1; + } else { + j += 1; + } + } + Runs { runs: out } + } + + /// `self ∖ o`. Needs no universe: it is `self ∩ ¬o` restricted to `self`. + pub fn difference(&self, o: &Runs) -> Runs { + let mut out = Vec::new(); + let mut j = 0; + for &(lo, hi) in &self.runs { + let mut cur = lo; + while j < o.runs.len() && o.runs[j].1 <= cur { + j += 1; + } + let mut k = j; + while k < o.runs.len() && o.runs[k].0 < hi { + let (blo, bhi) = o.runs[k]; + if blo > cur { + out.push((cur, blo)); + } + cur = cur.max(bhi); + if bhi >= hi { + break; + } + k += 1; + } + if cur < hi { + out.push((cur, hi)); + } + } + Runs { runs: out } + } + + /// `[0, universe) ∖ self`. Refused when `self` reaches past `universe`: + /// complement only exists against an explicitly declared population. + pub fn complement(&self, universe: u64) -> Result { + let end = self.end(); + if end > universe { + return Err(OutOfUniverse { universe, end }); + } + Ok(Runs::full(universe).difference(self)) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + // ── Independent oracle: materialized bitsets over an explicit universe. + // It knows nothing of `normalize`; it evaluates by definition. + + const N: usize = 97; // not a word multiple: exercises the tail + const SYMS: u32 = 4; + + struct World { + syms: Vec>, + i32_lanes: [Vec; 2], + u32_lanes: [Vec; 2], + } + + fn world(seed: u64) -> World { + let mut s = seed; + let mut next = move || { + s ^= s << 13; + s ^= s >> 7; + s ^= s << 17; + s + }; + let syms = (0..SYMS) + .map(|_| (0..N).map(|_| next() % 3 == 0).collect()) + .collect(); + let i32_lanes = [ + (0..N).map(|_| (next() % 11) as i32 - 5).collect(), + (0..N).map(|_| (next() % 7) as i32).collect(), + ]; + let u32_lanes = [ + (0..N).map(|_| (next() % 4) as u32).collect(), + (0..N).map(|_| (next() % 3) as u32).collect(), + ]; + World { + syms, + i32_lanes, + u32_lanes, + } + } + + fn res_holds(w: &World, r: Res, row: usize) -> bool { + match r { + Res::I32 { lane, op, t } => { + let x = w.i32_lanes[lane as usize][row]; + 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, + } + } + Res::U32 { lane, eq, v } => (w.u32_lanes[lane as usize][row] == v) == eq, + } + } + + fn eval(w: &World, e: &SetExpr) -> Vec { + match e { + SetExpr::All => vec![true; N], + SetExpr::Empty => vec![false; N], + SetExpr::Sym(i) => w.syms[*i as usize].clone(), + SetExpr::Res(r) => (0..N).map(|row| res_holds(w, *r, row)).collect(), + SetExpr::Not(c) => eval(w, c).into_iter().map(|b| !b).collect(), + SetExpr::And(cs) => cs.iter().fold(vec![true; N], |acc, c| { + acc.iter().zip(eval(w, c)).map(|(a, b)| *a && b).collect() + }), + SetExpr::Or(cs) => cs.iter().fold(vec![false; N], |acc, c| { + acc.iter().zip(eval(w, c)).map(|(a, b)| *a || b).collect() + }), + } + } + + struct Gen(u64); + impl Gen { + fn next(&mut self) -> u64 { + self.0 = self + .0 + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + self.0 >> 33 + } + fn leaf(&mut self) -> SetExpr { + const OPS: [Cmp; 6] = [Cmp::Lt, Cmp::Le, Cmp::Gt, Cmp::Ge, Cmp::Eq, Cmp::Ne]; + match self.next() % 5 { + 0 | 1 => SetExpr::Sym((self.next() % SYMS as u64) as u32), + 2 | 3 => SetExpr::i32( + (self.next() % 2) as u16, + OPS[(self.next() % 6) as usize], + (self.next() % 13) as i32 - 6, + ), + _ => SetExpr::Res(Res::U32 { + lane: (self.next() % 2) as u16, + eq: self.next().is_multiple_of(2), + v: (self.next() % 4) as u32, + }), + } + } + fn expr(&mut self, depth: u32) -> SetExpr { + if depth == 0 || self.next().is_multiple_of(4) { + return match self.next() % 12 { + 0 => SetExpr::All, + 1 => SetExpr::Empty, + _ => self.leaf(), + }; + } + match self.next() % 3 { + 0 => SetExpr::negated(self.expr(depth - 1)), + k => { + let n = 1 + self.next() % 4; + let cs = (0..n).map(|_| self.expr(depth - 1)).collect(); + if k == 1 { + SetExpr::And(cs) + } else { + SetExpr::Or(cs) + } + } + } + } + } + + /// FAILS IF: any rewrite changes the selected set. Differential against + /// materialized bitsets over random nested expressions, incl. `All`, + /// `Empty` and negations, in several worlds. + #[test] + fn normalize_preserves_meaning_against_materialized_bitsets() { + let mut g = Gen(0x5EED); + let mut changed = 0; + for k in 0..3000 { + let w = world(1 + k % 7); + let e = g.expr(5); + let n = normalize(&e); + assert_eq!(eval(&w, &n), eval(&w, &e), "{e:?}\n => {n:?}"); + assert_eq!(normalize(&n), n, "not idempotent: {e:?}"); + if n != e { + changed += 1; + } + } + // Anti-vacuity: the rewrites actually fired on most inputs. + assert!(changed * 2 > 3000, "only {changed} rewritten"); + } + + /// FAILS IF: normalization ever grows an expression (no distribution). + #[test] + fn normalize_never_grows_leaf_count() { + let mut g = Gen(0xB0B); + for _ in 0..3000 { + let e = g.expr(5); + assert!(normalize(&e).leaves() <= e.leaves(), "{e:?}"); + } + } + + fn x() -> SetExpr { + SetExpr::And(vec![SetExpr::Sym(1), SetExpr::Sym(4)]) + } + + /// N17, ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN. FAILS IF: absorption is + /// matched only against unflattened members, leaving + /// `¬P1 ∨ ¬P4 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5 ∧ ¬P7)`. + #[test] + fn absorption_after_de_morgan_matches_flattened_siblings() { + let y = SetExpr::And(vec![SetExpr::Sym(5), SetExpr::Sym(7)]); + let e = SetExpr::negated(SetExpr::And(vec![x(), SetExpr::Or(vec![x(), y])])); + let want = SetExpr::Or(vec![ + SetExpr::negated(SetExpr::Sym(1)), + SetExpr::negated(SetExpr::Sym(4)), + ]); + assert_eq!(normalize(&e), want); + } + + /// Dual of N17. FAILS IF: an `Or` whose members are all conjunction + /// siblings is not absorbed: `P1 ∧ P4 ∧ ((P1 ∧ P4) ∨ P5)` is `P1 ∧ P4`. + #[test] + fn dual_absorption_inside_a_conjunction() { + let e = SetExpr::And(vec![x(), SetExpr::Or(vec![x(), SetExpr::Sym(5)])]); + assert_eq!(normalize(&e), x()); + } + + /// Silence twin. FAILS IF: absorption fires when only SOME members of the + /// nested junction are siblings: `¬P1 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5)` stays. + #[test] + fn absorption_stays_silent_on_a_partial_cover() { + let e = SetExpr::Or(vec![ + SetExpr::negated(SetExpr::Sym(1)), + SetExpr::And(vec![ + SetExpr::Or(vec![ + SetExpr::negated(SetExpr::Sym(1)), + SetExpr::negated(SetExpr::Sym(4)), + ]), + SetExpr::negated(SetExpr::Sym(5)), + ]), + ]); + // Same set of children, in sort order (`And` sorts before `Not`). + let SetExpr::Or(cs) = &e else { unreachable!() }; + assert_eq!( + normalize(&e), + SetExpr::Or(vec![cs[1].clone(), cs[0].clone()]) + ); + } + + /// FAILS IF: nesting from the parser survives normalization: the depth a + /// consumer admits is that of the flattened form. + #[test] + fn associative_nesting_flattens_before_depth_is_measured() { + let mut nested = SetExpr::Sym(0); + for i in 1..8u32 { + nested = SetExpr::Or(vec![nested, SetExpr::Sym(i % SYMS + 10 * i)]); + } + assert_eq!(nested.depth(), 7); + let n = normalize(&nested); + assert_eq!(n.depth(), 1, "{n:?}"); + assert_eq!(n.leaves(), 8); + } + + #[test] + fn de_morgan_and_complement_pairs() { + let a = SetExpr::Sym(0); + let b = SetExpr::Sym(1); + let e = SetExpr::negated(SetExpr::Or(vec![a.clone(), b.clone()])); + assert_eq!( + normalize(&e), + SetExpr::And(vec![SetExpr::negated(a.clone()), SetExpr::negated(b)]) + ); + assert_eq!( + normalize(&SetExpr::And(vec![a.clone(), SetExpr::negated(a.clone())])), + SetExpr::Empty + ); + assert_eq!( + normalize(&SetExpr::Or(vec![a.clone(), SetExpr::negated(a)])), + SetExpr::All + ); + } + + // ── Runs: laws against materialized bitsets, with an explicit universe. + + fn bits(r: &Runs, u: u64) -> Vec { + (0..u).map(|i| r.contains(i)).collect() + } + + fn rand_runs(g: &mut Gen, u: u64) -> Runs { + let n = g.next() % 5; + Runs::from_intervals((0..n).map(|_| { + let lo = g.next() % (u + 1); + let hi = lo + g.next() % (u + 1 - lo + 1); + (lo, hi.min(u)) + })) + } + + fn canonical(r: &Runs) -> bool { + r.intervals().iter().all(|&(lo, hi)| lo < hi) + && r.intervals().windows(2).all(|w| w[0].1 < w[1].0) + } + + /// FAILS IF: `∩ ∪ ∖ ¬` disagree with the bitset definition, lose + /// canonical form, or break De Morgan / distributivity, incl. empty and + /// full sets and the universe boundary. + #[test] + fn runs_obey_the_set_laws_against_bitsets() { + let mut g = Gen(77); + for u in [0u64, 1, 2, 63, 64, 65, 100] { + for _ in 0..300 { + let (a, b, c) = ( + rand_runs(&mut g, u), + rand_runs(&mut g, u), + rand_runs(&mut g, u), + ); + let (ba, bb) = (bits(&a, u), bits(&b, u)); + let and: Vec = ba.iter().zip(&bb).map(|(x, y)| *x && *y).collect(); + let or: Vec = ba.iter().zip(&bb).map(|(x, y)| *x || *y).collect(); + let diff: Vec = ba.iter().zip(&bb).map(|(x, y)| *x && !*y).collect(); + let not_a: Vec = ba.iter().map(|x| !x).collect(); + let i = a.intersect(&b); + let un = a.union(&b); + let d = a.difference(&b); + let na = a.complement(u).unwrap(); + for r in [&i, &un, &d, &na] { + assert!(canonical(r), "{r:?}"); + } + assert_eq!(bits(&i, u), and); + assert_eq!(bits(&un, u), or); + assert_eq!(bits(&d, u), diff); + assert_eq!(bits(&na, u), not_a); + assert_eq!(i.count(), and.iter().filter(|x| **x).count() as u64); + // De Morgan. + assert_eq!( + un.complement(u).unwrap(), + na.intersect(&b.complement(u).unwrap()) + ); + // Distributivity. + assert_eq!(a.intersect(&b.union(&c)), i.union(&a.intersect(&c))); + // Identities. + assert_eq!(a.intersect(&Runs::full(u)), a); + assert_eq!(a.union(&Runs::empty()), a); + assert!(a.intersect(&Runs::empty()).is_empty()); + assert_eq!(a.complement(u).unwrap().complement(u).unwrap(), a); + assert_eq!(a.difference(&b), a.intersect(&b.complement(u).unwrap())); + } + } + } + + /// FAILS IF: complement silently assumes a universe smaller than the set + /// it complements. + #[test] + fn complement_requires_an_explicit_universe_that_covers_the_set() { + let r = Runs::from_intervals([(3, 10)]); + assert_eq!( + r.complement(9), + Err(OutOfUniverse { + universe: 9, + end: 10 + }) + ); + assert_eq!(r.complement(10).unwrap(), Runs::from_intervals([(0, 3)])); + assert_eq!(Runs::empty().complement(0).unwrap(), Runs::empty()); + assert_eq!(Runs::empty().complement(5).unwrap(), Runs::full(5)); + } +} diff --git a/crates/lance-graph-relalg/Cargo.toml b/crates/lance-graph-relalg/Cargo.toml index adffbe3ed..9a3956bd7 100644 --- a/crates/lance-graph-relalg/Cargo.toml +++ b/crates/lance-graph-relalg/Cargo.toml @@ -18,6 +18,9 @@ lance-graph-r2il = { path = "../lance-graph-r2il" } # By git `main`, the coordinate `lance-graph-r2il` uses (one `ogar-loco`). ogar-loco = { git = "https://github.com/AdaWorldAPI/OGAR", branch = "main" } ogar-r2il = { git = "https://github.com/AdaWorldAPI/OGAR", branch = "main" } +# The set algebra (normalize) lives in the contract (D-CMR-1 / D-RA-2, +# ADR-2026-10-20-SIX §2); this crate converts and lowers. +lance-graph-contract = { path = "../lance-graph-contract" } [patch."https://github.com/AdaWorldAPI/lance-graph"] lance-graph-contract = { path = "../lance-graph-contract" } diff --git a/crates/lance-graph-relalg/src/normalize.rs b/crates/lance-graph-relalg/src/normalize.rs index c250e198f..f2a19c0c2 100644 --- a/crates/lance-graph-relalg/src/normalize.rs +++ b/crates/lance-graph-relalg/src/normalize.rs @@ -1,42 +1,22 @@ //! Rewrites: each takes a description to an equivalent, cheaper one, before //! anything runs. None of them reads a row. //! -//! 1. Negation is pushed to the leaves (De Morgan); a negated comparison -//! becomes the opposite comparison. -//! 2. `And` / `Or` are flattened; `All` and `Empty` are absorbed or -//! dominate; duplicates are removed; `p ∧ ¬p` is `Empty`, `p ∨ ¬p` is -//! `All`. -//! 3. In an `And`, every comparison on one `I32` lane becomes one interval -//! (plus the excluded values inside it); an empty interval makes the whole -//! conjunction `Empty`. Equalities on one `U32` lane either agree or -//! contradict. -//! 4. In an `Or`, intervals on one `I32` lane that overlap or touch are -//! merged; a union covering the whole lane is `All`. -//! 5. Absorption: `x ∧ (x ∨ y) = x`, `x ∨ (x ∧ y) = x`. -//! -//! The rewrites run to a fixpoint. An interval is always emitted as `<` / `>` -//! bounds or one `==`, the forms `IntSLess` / `IntEqual` lower without a -//! negation pass. +//! The rewrites themselves live in +//! [`lance_graph_contract::set_algebra::normalize`] (D-CMR-1 / D-RA-2, +//! `ADR-2026-10-20-SIX` §2): the contract owns what a selection means, this +//! crate owns how it executes. Here a [`Rel`] is converted to the contract's +//! [`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. -use std::collections::{BTreeMap, BTreeSet}; +use lance_graph_contract::set_algebra::{self as sa, Res, SetExpr}; use crate::ir::{Atom, Cmp, Measure, Rel}; use crate::lower::Answer; -const LO: i64 = i32::MIN as i64; -const HI: i64 = i32::MAX as i64; - /// Rewrite `rel` to an equivalent description, to a fixpoint. pub fn normalize(rel: &Rel) -> Rel { - let mut cur = nnf(rel, false); - for _ in 0..64 { - let next = simplify(&cur); - if next == cur { - return next; - } - cur = next; - } - cur + from_set(&sa::normalize(&to_set(rel))) } /// The answer, if the description alone determines it: no row is read and @@ -52,296 +32,86 @@ pub fn symbolic(rel: &Rel, m: Measure, n_rows: usize) -> Option { } } -fn negate(a: Atom) -> Atom { - match a { - Atom::I32 { lane, op, t } => Atom::I32 { - lane, - t, - op: match op { - Cmp::Lt => Cmp::Ge, - Cmp::Ge => Cmp::Lt, - Cmp::Le => Cmp::Gt, - Cmp::Gt => Cmp::Le, - Cmp::Eq => Cmp::Ne, - Cmp::Ne => Cmp::Eq, - }, - }, - Atom::U32 { lane, eq, v } => Atom::U32 { lane, eq: !eq, v }, +fn cmp_to(c: Cmp) -> sa::Cmp { + match c { + Cmp::Lt => sa::Cmp::Lt, + Cmp::Le => sa::Cmp::Le, + Cmp::Gt => sa::Cmp::Gt, + Cmp::Ge => sa::Cmp::Ge, + Cmp::Eq => sa::Cmp::Eq, + Cmp::Ne => sa::Cmp::Ne, } } -/// Negation normal form: `Not` survives only around a plane. -fn nnf(rel: &Rel, neg: bool) -> Rel { - match rel { - Rel::All if neg => Rel::Empty, - Rel::Empty if neg => Rel::All, - Rel::Plane(_) if neg => Rel::Not(Box::new(rel.clone())), - Rel::Atom(a) if neg => Rel::Atom(negate(*a)), - Rel::All | Rel::Empty | Rel::Plane(_) | Rel::Atom(_) => rel.clone(), - Rel::Not(c) => nnf(c, !neg), - Rel::And(cs) | Rel::Or(cs) => { - let cs = cs.iter().map(|c| nnf(c, neg)).collect(); - match (rel, neg) { - (Rel::And(_), false) | (Rel::Or(_), true) => Rel::And(cs), - _ => Rel::Or(cs), - } - } +fn cmp_from(c: sa::Cmp) -> Cmp { + match c { + sa::Cmp::Lt => Cmp::Lt, + sa::Cmp::Le => Cmp::Le, + sa::Cmp::Gt => Cmp::Gt, + sa::Cmp::Ge => Cmp::Ge, + sa::Cmp::Eq => Cmp::Eq, + sa::Cmp::Ne => Cmp::Ne, } } -fn simplify(rel: &Rel) -> Rel { +fn to_set(rel: &Rel) -> SetExpr { match rel { - Rel::All | Rel::Empty | Rel::Plane(_) => rel.clone(), - Rel::Atom(_) => conj(vec![rel.clone()]), - Rel::Not(c) => match simplify(c) { - Rel::All => Rel::Empty, - Rel::Empty => Rel::All, - Rel::Not(x) => *x, - s => Rel::Not(Box::new(s)), - }, - Rel::And(cs) => conj(cs.iter().map(simplify).collect()), - Rel::Or(cs) => disj(cs.iter().map(simplify).collect()), - } -} - -fn complement(r: &Rel) -> Option { - match r { - Rel::Plane(_) => Some(Rel::Not(Box::new(r.clone()))), - Rel::Not(x) => Some((**x).clone()), - _ => None, - } -} - -/// `[lo, hi]` as `<` / `>` bounds or one `==`; empty for the whole lane. -fn emit_interval(lane: u16, lo: i64, hi: i64) -> Vec { - if lo == hi { - return vec![Rel::i32(lane, Cmp::Eq, lo as i32)]; - } - let mut v = Vec::new(); - if hi < HI { - v.push(Rel::i32(lane, Cmp::Lt, (hi + 1) as i32)); - } - if lo > LO { - v.push(Rel::i32(lane, Cmp::Gt, (lo - 1) as i32)); - } - v -} - -/// The interval an ordered comparison or equality selects; `None` for `!=`. -fn interval(op: Cmp, t: i32) -> Option<(i64, i64)> { - let t = i64::from(t); - Some(match op { - Cmp::Lt => (LO, t - 1), - Cmp::Le => (LO, t), - Cmp::Gt => (t + 1, HI), - Cmp::Ge => (t, HI), - Cmp::Eq => (t, t), - Cmp::Ne => return None, - }) -} - -/// A conjunction of simplified children. -fn conj(children: Vec) -> Rel { - let mut flat = Vec::new(); - for c in children { - match c { - Rel::And(cs) => flat.extend(cs), - Rel::Empty => return Rel::Empty, - Rel::All => {} - c => flat.push(c), - } - } - // Fuse comparisons per lane. - let mut ranges: BTreeMap)> = BTreeMap::new(); - let mut eqs: BTreeMap, BTreeSet)> = BTreeMap::new(); - let mut rest = Vec::new(); - for c in flat { - match c { - Rel::Atom(Atom::I32 { lane, op, t }) => { - let e = ranges.entry(lane).or_insert((LO, HI, BTreeSet::new())); - match interval(op, t) { - Some((lo, hi)) => { - e.0 = e.0.max(lo); - e.1 = e.1.min(hi); - } - None => { - e.2.insert(i64::from(t)); - } - } - } - Rel::Atom(Atom::U32 { lane, eq, v }) => { - let e = eqs.entry(lane).or_default(); - if eq { &mut e.0 } else { &mut e.1 }.insert(v); - } - c => rest.push(c), - } + Rel::All => SetExpr::All, + Rel::Empty => SetExpr::Empty, + Rel::Plane(i) => SetExpr::Sym(u32::from(*i)), + Rel::Atom(Atom::I32 { lane, op, t }) => SetExpr::Res(Res::I32 { + lane: *lane, + op: cmp_to(*op), + t: *t, + }), + Rel::Atom(Atom::U32 { lane, eq, v }) => SetExpr::Res(Res::U32 { + lane: *lane, + eq: *eq, + v: *v, + }), + Rel::And(cs) => SetExpr::And(cs.iter().map(to_set).collect()), + Rel::Or(cs) => SetExpr::Or(cs.iter().map(to_set).collect()), + Rel::Not(c) => SetExpr::Not(Box::new(to_set(c))), } - let mut out = Vec::new(); - for (lane, (mut lo, mut hi, excl)) in ranges { - while lo <= hi && excl.contains(&lo) { - lo += 1; - } - while lo <= hi && excl.contains(&hi) { - hi -= 1; - } - if lo > hi { - return Rel::Empty; - } - out.extend(emit_interval(lane, lo, hi)); - if lo + 1 < hi { - for &v in excl.range(lo + 1..hi) { - out.push(Rel::i32(lane, Cmp::Ne, v as i32)); - } - } - } - for (lane, (is, nots)) in eqs { - let mut is = is.into_iter(); - match (is.next(), is.next()) { - (Some(_), Some(_)) => return Rel::Empty, - (Some(v), None) if nots.contains(&v) => return Rel::Empty, - (Some(v), None) => out.push(Rel::eq_u32(lane, v)), - _ => out.extend(nots.into_iter().map(|v| Rel::ne_u32(lane, v))), - } - } - out.extend(rest); - finish(out, true) } -/// A disjunction of simplified children. -fn disj(children: Vec) -> Rel { - let mut flat = Vec::new(); - for c in children { - match c { - Rel::Or(cs) => flat.extend(cs), - Rel::All => return Rel::All, - Rel::Empty => {} - c => flat.push(c), - } - } - // Intervals per lane: a comparison atom, or an `And` that is exactly the - // bounds of one interval on one lane. - let mut ranges: BTreeMap> = BTreeMap::new(); - let mut excluded: BTreeMap> = BTreeMap::new(); - let mut eqs: BTreeMap, BTreeSet)> = BTreeMap::new(); - let mut rest = Vec::new(); - for c in flat { - if let Some((lane, lo, hi)) = as_interval(&c) { - ranges.entry(lane).or_default().push((lo, hi)); - continue; - } - match c { - Rel::Atom(Atom::I32 { - lane, - op: Cmp::Ne, - t, - }) => { - excluded.entry(lane).or_default().insert(i64::from(t)); - } - Rel::Atom(Atom::U32 { lane, eq, v }) => { - let e = eqs.entry(lane).or_default(); - if eq { &mut e.0 } else { &mut e.1 }.insert(v); - } - c => rest.push(c), - } - } - let mut out = Vec::new(); - // `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. - for (lane, ne) in excluded { - let mut ne = ne.into_iter(); - let (Some(a), None) = (ne.next(), ne.next()) else { - return Rel::All; - }; - let iv = ranges.remove(&lane).unwrap_or_default(); - if iv.iter().any(|&(lo, hi)| lo <= a && a <= hi) { - return Rel::All; - } - out.push(Rel::i32(lane, Cmp::Ne, a as i32)); +/// Inverse of [`to_set`]. Every `Sym` the contract returns came from a +/// `Plane`, so the narrowing never fails on a converted input. +fn from_set(e: &SetExpr) -> Rel { + match e { + SetExpr::All => Rel::All, + SetExpr::Empty => Rel::Empty, + SetExpr::Sym(i) => { + Rel::Plane(u16::try_from(*i).expect("Sym ids originate from u16 planes")) + } + SetExpr::Res(Res::I32 { lane, op, t }) => Rel::i32(*lane, cmp_from(*op), *t), + SetExpr::Res(Res::U32 { lane, eq, v }) => Rel::Atom(Atom::U32 { + lane: *lane, + eq: *eq, + v: *v, + }), + SetExpr::And(cs) => Rel::And(cs.iter().map(from_set).collect()), + SetExpr::Or(cs) => Rel::Or(cs.iter().map(from_set).collect()), + SetExpr::Not(c) => Rel::Not(Box::new(from_set(c))), } - for (lane, mut iv) in ranges { - iv.sort_unstable(); - let mut merged: Vec<(i64, i64)> = Vec::new(); - for (lo, hi) in iv { - match merged.last_mut() { - Some(last) if lo <= last.1 + 1 => last.1 = last.1.max(hi), - _ => merged.push((lo, hi)), - } - } - for (lo, hi) in merged { - let atoms = emit_interval(lane, lo, hi); - match atoms.len() { - 0 => return Rel::All, - 1 => out.extend(atoms), - _ => out.push(finish(atoms, true)), - } - } - } - for (lane, (is, nots)) in eqs { - let mut ns = nots.iter(); - match (ns.next(), ns.next()) { - // `v ≠ a ∨ v ≠ b` with `a ≠ b` holds everywhere. - (Some(_), Some(_)) => return Rel::All, - (Some(a), None) if is.contains(a) => return Rel::All, - // `v ≠ a ∨ v = b` with `b ≠ a` is `v ≠ a`. - (Some(&a), None) => out.push(Rel::ne_u32(lane, a)), - _ => out.extend(is.into_iter().map(|v| Rel::eq_u32(lane, v))), - } - } - out.extend(rest); - finish(out, false) } -/// The interval a simplified child selects on one lane, if it is exactly -/// one. -fn as_interval(c: &Rel) -> Option<(u16, i64, i64)> { - let one = |r: &Rel| match r { - Rel::Atom(Atom::I32 { lane, op, t }) => interval(*op, *t).map(|(lo, hi)| (*lane, lo, hi)), - _ => None, - }; - match c { - Rel::Atom(_) => one(c), - Rel::And(cs) if !cs.is_empty() => { - let mut acc: Option<(u16, i64, i64)> = None; - for x in cs { - let (lane, lo, hi) = one(x)?; - acc = Some(match acc { - None => (lane, lo, hi), - Some((l, a, b)) if l == lane => (l, a.max(lo), b.min(hi)), - Some(_) => return None, - }); - } - acc.filter(|&(_, lo, hi)| lo <= hi) - } - _ => None, - } -} +#[cfg(test)] +mod tests { + use super::*; -/// Sort, deduplicate, apply complement and absorption, and collapse. -fn finish(mut out: Vec, and: bool) -> Rel { - out.sort(); - out.dedup(); - let (unit, zero) = if and { - (Rel::All, Rel::Empty) - } else { - (Rel::Empty, Rel::All) - }; - if out - .iter() - .any(|c| complement(c).is_some_and(|n| out.binary_search(&n).is_ok())) - { - return zero; - } - // Absorption: drop a dual child that shares a member with its siblings. - let set: BTreeSet = out.iter().cloned().collect(); - out.retain(|c| match (c, and) { - (Rel::Or(ms), true) | (Rel::And(ms), false) => !ms.iter().any(|m| set.contains(m)), - _ => true, - }); - match out.len() { - 0 => unit, - 1 => out.pop().unwrap_or(unit), - _ if and => Rel::And(out), - _ => Rel::Or(out), + /// FAILS IF: the conversion is lossy. Order of variants and fields is + /// shared with the contract, so sorting agrees on both sides. + #[test] + fn conversion_round_trips() { + let rel = Rel::Or(vec![ + Rel::All, + Rel::Empty, + Rel::Plane(u16::MAX), + Rel::i32(3, Cmp::Le, -7), + Rel::ne_u32(1, 9), + Rel::And(vec![Rel::eq_u32(0, 2), Rel::Not(Box::new(Rel::Plane(4)))]), + ]); + assert_eq!(from_set(&to_set(&rel)), rel); } } diff --git a/crates/lance-graph-relalg/tests/absorption_n17.rs b/crates/lance-graph-relalg/tests/absorption_n17.rs new file mode 100644 index 000000000..a01a3b506 --- /dev/null +++ b/crates/lance-graph-relalg/tests/absorption_n17.rs @@ -0,0 +1,36 @@ +//! N17 / ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN, through relalg's public +//! `normalize`, which delegates to `lance_graph_contract::set_algebra`. + +use lance_graph_relalg::{normalize, Rel}; + +fn not(r: Rel) -> Rel { + Rel::Not(Box::new(r)) +} + +/// FAILS IF: `¬(x ∧ (x ∨ y))` with `x = P1 ∧ P4` keeps the redundant +/// `(¬P1 ∨ ¬P4) ∧ ¬P5 ∧ ¬P7` arm De Morgan emits; it is `¬P1 ∨ ¬P4`. +#[test] +fn absorption_after_de_morgan_is_as_narrow_as_written() { + let x = Rel::And(vec![Rel::Plane(1), Rel::Plane(4)]); + let y = Rel::And(vec![Rel::Plane(5), Rel::Plane(7)]); + let rel = not(Rel::And(vec![x.clone(), Rel::Or(vec![x, y])])); + assert_eq!( + normalize(&rel), + Rel::Or(vec![not(Rel::Plane(1)), not(Rel::Plane(4))]) + ); +} + +/// FAILS IF: nesting from the parser reaches lowering: `Or(a, Or(b, c))` is +/// one flat `Or` after `normalize`, which `run` applies before the slot check. +#[test] +fn nested_disjunction_is_flat_before_admission() { + let mut nested = Rel::eq_u32(0, 0); + for v in 1..8 { + nested = Rel::Or(vec![nested, Rel::eq_u32(1, v)]); + } + let Rel::Or(cs) = normalize(&nested) else { + panic!("not an Or") + }; + assert_eq!(cs.len(), 8); + assert!(cs.iter().all(|c| matches!(c, Rel::Atom(_)))); +} From a621d2d964f82cae239c2ea0af3f4d230b477de2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 00:22:22 +0000 Subject: [PATCH 2/4] set_algebra: absorb a sub-junction sibling; flip crepe-plan-probe's N17 pin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI (probe) showed crepe-plan-probe's pin m_the_known_absorption_gap firing: the compound-x case is now fixed, as the pin asked to be told. Its Or-x variant exposed a second absorption shape: after De Morgan, (¬P0 ∧ ¬P2) ∨ (¬P0 ∧ ¬P2 ∧ ¬P1), i.e. one dual child a sub-conjunction of another. normalize now also drops And(ms) in an Or when a sibling And(ks) has every k in ms (dually in an And). Red first (absorption_of_a_superset_conjunction), green after, disable-verified; the bitset differential stays green. crepe-plan-probe: the pin is flipped to assert both compound cases now reduce, renamed ..._is_closed_and_not_produced. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- crates/crepe-plan-probe/tests/pipeline.rs | 23 ++++++------- .../lance-graph-contract/src/set_algebra.rs | 32 ++++++++++++++++++- 2 files changed, 43 insertions(+), 12 deletions(-) diff --git a/crates/crepe-plan-probe/tests/pipeline.rs b/crates/crepe-plan-probe/tests/pipeline.rs index 04ae9f5cf..e18f80fc0 100644 --- a/crates/crepe-plan-probe/tests/pipeline.rs +++ b/crates/crepe-plan-probe/tests/pipeline.rs @@ -674,14 +674,15 @@ fn l_renamed_and_noisy_rules_give_the_same_plan() { // M. The H14d absorption case // --------------------------------------------------------------------------- -/// `normalize` still misses `¬(x ∧ (x ∨ y)) = ¬x` (H14d, 2026-10-16) — but -/// only when `x` is itself an `And` or `Or`. Measured here: with `x` a plane or -/// a comparison it reduces correctly; with `x = p0 ∧ p2` De Morgan and -/// flattening run first and the absorption no longer matches. A relalg defect, -/// pinned here, not fixed in the optimizer. This spike never builds the shape: -/// it only emits an `And` of planes (no `Not`, no `Or`). +/// `¬(x ∧ (x ∨ y)) = ¬x` (H14d, 2026-10-16). Until D-CMR-1 `normalize` missed +/// it when `x` was itself an `And` or `Or`: De Morgan and flattening ran first +/// and absorption no longer matched. Fixed upstream in +/// `lance_graph_contract::set_algebra::normalize` (absorption against +/// flattened siblings and sub-junctions), which relalg now delegates to; this +/// pin flipped with it. Not fixed in the optimizer. This spike never builds the +/// shape: it only emits an `And` of planes (no `Not`, no `Or`). #[test] -fn m_the_known_absorption_gap_is_untouched_and_not_produced() { +fn m_the_known_absorption_gap_is_closed_and_not_produced() { let absorbed = |x: Rel| { let e = Rel::Not(Box::new(Rel::And(vec![ x.clone(), @@ -691,12 +692,12 @@ fn m_the_known_absorption_gap_is_untouched_and_not_produced() { }; assert!(absorbed(Rel::Plane(0)), "leaf x reduces"); assert!( - !absorbed(Rel::And(vec![Rel::Plane(0), Rel::Plane(2)])), - "compound x: fixed upstream? update this pin" + absorbed(Rel::And(vec![Rel::Plane(0), Rel::Plane(2)])), + "compound x (And) must reduce since D-CMR-1" ); assert!( - !absorbed(Rel::Or(vec![Rel::Plane(0), Rel::Plane(2)])), - "compound x: fixed upstream? update this pin" + absorbed(Rel::Or(vec![Rel::Plane(0), Rel::Plane(2)])), + "compound x (Or) must reduce since D-CMR-1" ); // What this spike produces: duplicates collapse, nothing widens. let ours = Rel::And(vec![Rel::Plane(0), Rel::Plane(1), Rel::Plane(0)]); diff --git a/crates/lance-graph-contract/src/set_algebra.rs b/crates/lance-graph-contract/src/set_algebra.rs index 2dd801609..e7244ff8a 100644 --- a/crates/lance-graph-contract/src/set_algebra.rs +++ b/crates/lance-graph-contract/src/set_algebra.rs @@ -40,7 +40,9 @@ //! 5. Absorption, matched against FLATTENED sibling sets: in an `Or`, a dual //! child `And(ms)` is dropped when some member `m` is already covered by //! the siblings (`m` is a sibling, or `m` is an `Or` whose members are all -//! siblings); dually in an `And`. This closes +//! siblings), or when a sibling `And(ks)` has every `k` among `ms` +//! (`x ∨ (x ∧ y)` with `x` itself a conjunction); dually in an `And`. +//! This closes //! ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN: `¬(x ∧ (x ∨ y))` with //! `x = P1 ∧ P4` is `¬P1 ∨ ¬P4`, not the wider form De Morgan emits. //! @@ -428,6 +430,20 @@ fn covered(m: &SetExpr, sibs: &[&SetExpr], and: bool) -> bool { } } +/// Whether sibling `s` absorbs a dual child with members `ms`: inside an `Or` +/// (`and == false`), `s = And(ks)` with every `k` in `ms`, so +/// `And(ms) ⊆ s`; inside an `And`, `s = Or(ks)` with every `k` in `ms`, so +/// `Or(ms) ⊇ s`. This is `x ∨ (x ∧ y) = x` when `x` is itself a junction and +/// flattening has spread it into `ms`. +fn sub_junction(s: &SetExpr, ms: &[SetExpr], and: bool) -> bool { + match (s, and) { + (SetExpr::And(ks), false) | (SetExpr::Or(ks), true) => { + !ks.is_empty() && ks.iter().all(|k| ms.contains(k)) + } + _ => false, + } +} + /// Sort, deduplicate, apply complement and absorption, and collapse. fn finish(mut out: Vec, and: bool) -> SetExpr { out.sort(); @@ -457,6 +473,7 @@ fn finish(mut out: Vec, and: bool) -> SetExpr { .map(|(_, s)| s) .collect(); ms.iter().any(|m| covered(m, &sibs, and)) + || sibs.iter().any(|s| sub_junction(s, ms, and)) } _ => false, }; @@ -781,6 +798,19 @@ mod tests { assert_eq!(normalize(&e), x()); } + /// FAILS IF: absorption misses `x ∨ (x ∧ y)` when `x` is itself a + /// conjunction, i.e. one dual child is a sub-conjunction of another: + /// `¬(x ∧ (x ∨ P1))` with `x = P0 ∨ P2` is `¬P0 ∧ ¬P2`. + #[test] + fn absorption_of_a_superset_conjunction() { + let x = SetExpr::Or(vec![SetExpr::Sym(0), SetExpr::Sym(2)]); + let e = SetExpr::negated(SetExpr::And(vec![ + x.clone(), + SetExpr::Or(vec![x.clone(), SetExpr::Sym(1)]), + ])); + assert_eq!(normalize(&e), normalize(&SetExpr::negated(x))); + } + /// Silence twin. FAILS IF: absorption fires when only SOME members of the /// nested junction are siblings: `¬P1 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5)` stays. #[test] From e336d0a5707fc4ce4a4e37afd82de4474164e0b8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 00:24:10 +0000 Subject: [PATCH 3/4] set_algebra: Runs::union is one O(n+m) merge pass (codex P2) union re-sorted n+m intervals through from_intervals while the type promises cost linear in intervals. Now a two-pointer merge of the two canonical lists. Covered by runs_obey_the_set_laws_against_bitsets; dropping the max in the merge turns it red. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .../lance-graph-contract/src/set_algebra.rs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/crates/lance-graph-contract/src/set_algebra.rs b/crates/lance-graph-contract/src/set_algebra.rs index e7244ff8a..1eeddfc0e 100644 --- a/crates/lance-graph-contract/src/set_algebra.rs +++ b/crates/lance-graph-contract/src/set_algebra.rs @@ -557,8 +557,25 @@ impl Runs { self.runs.last().map_or(0, |&(_, hi)| hi) } + /// `self ∪ o`: one merge pass over the two canonical lists, O(n + m). pub fn union(&self, o: &Runs) -> Runs { - Runs::from_intervals(self.runs.iter().chain(o.runs.iter()).copied()) + let (a, b) = (&self.runs, &o.runs); + let (mut i, mut j) = (0, 0); + let mut out: Vec<(u64, u64)> = Vec::with_capacity(a.len() + b.len()); + while i < a.len() || j < b.len() { + let next = if j >= b.len() || (i < a.len() && a[i].0 <= b[j].0) { + i += 1; + a[i - 1] + } else { + j += 1; + b[j - 1] + }; + match out.last_mut() { + Some(last) if next.0 <= last.1 => last.1 = last.1.max(next.1), + _ => out.push(next), + } + } + Runs { runs: out } } pub fn intersect(&self, o: &Runs) -> Runs { From 6fc04a4e36b8b00372fba6b3a90bd1908490e4c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 21 Oct 2026 00:27:30 +0000 Subject: [PATCH 4/4] board: D-CMR-1 entry records absorption form 2 and the O(n+m) union; entries index after #1643 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md | 8 +++++--- .claude/board/entries/README.md | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md index 0a30c4065..e86db05df 100644 --- a/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md +++ b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md @@ -3,15 +3,17 @@ **Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`). - **Moved:** relalg's rewrite rules to `lance_graph_contract::set_algebra::normalize`, unchanged except absorption. relalg's `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`, `Atom` ↔ `Res`) and delegates. `symbolic`, `run`, lowering and the public API are unchanged. The contract stays dependency-free. -- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept. That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`). -- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`. `complement(universe)` refuses a set that reaches past the universe. +- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept, in two forms: (1) a member of the dual child is a sibling, or a junction of siblings; (2) a sibling junction's members all occur in the dual child (`x ∨ (x ∧ y)` with `x` itself a conjunction). That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`) for `x` a leaf, an `And` or an `Or`. Form 2 was found by crepe-plan-probe's N17 pin (CI `probe`), which this PR flips to assert the reduction. +- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`, each one merge pass, O(n + m). `complement(universe)` refuses a set that reaches past the universe. - **Regression:** the 16 pre-existing relalg tests pass unchanged. 3 tests are new: `conversion_round_trips` plus 2 in `tests/absorption_n17.rs`. - **Disable runs** (commands: `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml --no-fail-fast` and `cargo test -p lance-graph-contract --lib set_algebra`): | probe | what breaks | |---|---| | contract `normalize` returns its input | 10 of 14 `rewrites.rs` tests, and both N17 tests in relalg | - | generalized absorption off | only the N17 tests: one in relalg, two in the contract | + | absorption form 1 off | only the N17 tests: one in relalg, two in the contract | + | absorption form 2 off | only `absorption_of_a_superset_conjunction` | + | `max` dropped in the `union` merge | `runs_obey_the_set_laws_against_bitsets` | | absorption on a partial cover (`all` → `any`) | the silence twin, and the bitset differential (an unsound rule) | - **Scope held:** no joins, gathers, positional addressing, recursion, D-MPS-8 or `graph_hop`. Measures (`Count`/`Sum` on `Runs`) are not in this PR. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 45cb6c593..9273c10f0 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. -396 entries, 2026-08-06 .. 2026-10-20. +397 entries, 2026-08-06 .. 2026-10-20. | date | entry id | finding | file | |---|---|---|---|