From 701c9cb6979bdf24c8c5bc6e6905187186541f41 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 22:37:59 +0000 Subject: [PATCH 1/4] lance-graph-relalg: relational IR, proven rewrites, lowering through R2IL (D-RA-1) A query is described as a selection over one table's row space (All, Empty, Plane, comparison atoms, And/Or/Not) plus a measure. normalize() rewrites the description before anything runs: negation to the leaves, flattening and unit/zero absorption, complement, interval fusion per I32 lane in conjunctions, interval union in disjunctions, U32 equality agreement, absorption. A description that normalizes to Empty (or All, for a count) is answered without a program. Everything else lowers into R2IL calls over FoldDialect, which builds and runs one mask-risc program per fold. tests/rewrites.rs checks rewritten == as written == a row oracle over 400 generated descriptions and five measures, plus the cost effects (fewer passes, no program for contradictions and tautologies, a ten-way conjunction that only fits the scratch arena after fusion). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- Cargo.toml | 4 + crates/lance-graph-relalg/Cargo.toml | 26 ++ crates/lance-graph-relalg/src/ir.rs | 108 +++++ crates/lance-graph-relalg/src/lib.rs | 10 + crates/lance-graph-relalg/src/lower.rs | 231 ++++++++++ crates/lance-graph-relalg/src/normalize.rs | 325 ++++++++++++++ crates/lance-graph-relalg/tests/rewrites.rs | 469 ++++++++++++++++++++ 7 files changed, 1173 insertions(+) create mode 100644 crates/lance-graph-relalg/Cargo.toml create mode 100644 crates/lance-graph-relalg/src/ir.rs create mode 100644 crates/lance-graph-relalg/src/lib.rs create mode 100644 crates/lance-graph-relalg/src/lower.rs create mode 100644 crates/lance-graph-relalg/src/normalize.rs create mode 100644 crates/lance-graph-relalg/tests/rewrites.rs diff --git a/Cargo.toml b/Cargo.toml index a2606c45b..f7b0de8d7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -111,6 +111,10 @@ exclude = [ # needs the OGAR checkout too. Own workspace root; verify via # `cargo test --manifest-path crates/lance-graph-nal/Cargo.toml`. "crates/lance-graph-nal", + # Relational algebra over coordinate populations (D-RA-1): path-deps + # lance-graph-r2il like lance-graph-nal. Own workspace root; verify via + # `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml`. + "crates/lance-graph-relalg", "crates/symbiont", # OGAR (Open Graph of Active Record) activation crate — re-exports OGAR's full # AR surface (ogar-vocab Class/codebook + ogar-class-view impl ClassView + diff --git a/crates/lance-graph-relalg/Cargo.toml b/crates/lance-graph-relalg/Cargo.toml new file mode 100644 index 000000000..adffbe3ed --- /dev/null +++ b/crates/lance-graph-relalg/Cargo.toml @@ -0,0 +1,26 @@ +[package] +name = "lance-graph-relalg" +version = "0.1.0" +edition = "2021" +publish = false +description = "Relational algebra over coordinate populations: an IR that describes a query, proven rewrites before anything runs, lowering through R2IL into one mask-risc program per fold (D-RA-1)." + +# Its OWN workspace root, like `lance-graph-nal`: it path-deps the r2il crate, +# which git-deps OGAR. Verify via +# `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml`. +[workspace] + +[dependencies] +# The only bulk engine. +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } +# The lowering target: queries become R2IL call sequences over FoldDialect. +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" } + +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "../lance-graph-contract" } + +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "../../../ndarray" } diff --git a/crates/lance-graph-relalg/src/ir.rs b/crates/lance-graph-relalg/src/ir.rs new file mode 100644 index 000000000..c246651d5 --- /dev/null +++ b/crates/lance-graph-relalg/src/ir.rs @@ -0,0 +1,108 @@ +//! The IR. It describes a selection over one table's row space; it never +//! holds rows. + +/// An ordered comparison of an `I32` lane against a constant. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Cmp { + /// `lane < t` + Lt, + /// `lane <= t` + Le, + /// `lane > t` + Gt, + /// `lane >= t` + Ge, + /// `lane == t` + Eq, + /// `lane != t` + Ne, +} + +/// One predicate on one lane of the table. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Atom { + /// `lanes[lane] op t` on an `I32` lane. + I32 { lane: u16, op: Cmp, t: i32 }, + /// `lanes[lane] == v` (`eq`) or `!= v` (`!eq`) on a `U32` lane. + U32 { lane: u16, eq: bool, v: u32 }, +} + +/// A set of rows of the table, described, not computed. +/// +/// `And` is intersection (σ of a conjunction, ∩), `Or` is union (∪), and +/// `And[a, Not b]` is difference (−). Projection and aggregation are the +/// [`Measure`] a [`Query`] ends with. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Rel { + /// Every row. + All, + /// No row. + Empty, + /// A resident mask plane, `Planes::masks[i]`. + Plane(u16), + /// The rows where one predicate holds. + Atom(Atom), + /// Intersection. + And(Vec), + /// Union. + Or(Vec), + /// Complement within the table. + Not(Box), +} + +impl Rel { + /// `a − b`. + pub fn diff(a: Rel, b: Rel) -> Rel { + Rel::And(vec![a, Rel::Not(Box::new(b))]) + } + + /// `lanes[lane] op t` on an `I32` lane. + pub fn i32(lane: u16, op: Cmp, t: i32) -> Rel { + Rel::Atom(Atom::I32 { lane, op, t }) + } + + /// `lanes[lane] == v` on a `U32` lane. + pub fn eq_u32(lane: u16, v: u32) -> Rel { + Rel::Atom(Atom::U32 { lane, eq: true, v }) + } + + /// `lanes[lane] != v` on a `U32` lane. + pub fn ne_u32(lane: u16, v: u32) -> Rel { + Rel::Atom(Atom::U32 { lane, eq: false, v }) + } + + /// How many predicates the description names (a lowering emits one + /// predicate pass per atom). + pub fn atoms(&self) -> usize { + match self { + Rel::Atom(_) => 1, + Rel::And(cs) | Rel::Or(cs) => cs.iter().map(Rel::atoms).sum(), + Rel::Not(c) => c.atoms(), + _ => 0, + } + } +} + +/// What a query produces from its rows. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Measure { + /// How many rows. + Count, + /// Σ of an `I32` lane. + Sum(u16), + /// Minimum of an `I32` lane. + Min(u16), + /// Maximum of an `I32` lane. + Max(u16), + /// The rows themselves, written into a caller-owned mask. + Keep, +} + +/// A selection and what to produce from it. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Query { + /// Which rows. + pub rel: Rel, + /// What to produce. + pub measure: Measure, +} diff --git a/crates/lance-graph-relalg/src/lib.rs b/crates/lance-graph-relalg/src/lib.rs new file mode 100644 index 000000000..992f8085f --- /dev/null +++ b/crates/lance-graph-relalg/src/lib.rs @@ -0,0 +1,10 @@ +//! `lance-graph-relalg` — relational algebra over coordinate populations +//! (D-RA-1, `.claude/plans/relalg-v1.md`). + +pub mod ir; +pub mod lower; +pub mod normalize; + +pub use ir::{Atom, Cmp, Measure, Query, Rel}; +pub use lower::{run, run_as_written, Answer, RelError, Run}; +pub use normalize::{normalize, symbolic}; diff --git a/crates/lance-graph-relalg/src/lower.rs b/crates/lance-graph-relalg/src/lower.rs new file mode 100644 index 000000000..bbd91483c --- /dev/null +++ b/crates/lance-graph-relalg/src/lower.rs @@ -0,0 +1,231 @@ +//! Lowering: a [`Query`] becomes R2IL calls over [`FoldDialect`], which +//! builds and runs one mask-risc program at the measure. Nothing here loops +//! over rows. + +use lance_graph_mask_risc::{Foreign, Planes}; +use lance_graph_r2il::{ + FoldDialect, FoldError, Val, INT_AND, INT_EQUAL, INT_NOT, INT_OR, INT_S_LESS, LOAD, POP_COUNT, +}; +use ogar_loco::{Dialect, FnIndex}; +use ogar_r2il::{KEEP, MAX, MIN, RANGE, SUM}; + +use crate::ir::{Atom, Cmp, Measure, Query, Rel}; +use crate::normalize::{normalize, symbolic}; + +/// `LOAD` spaces, as `FoldDialect` reads them. +const SPACE_U32: u8 = 0; +const SPACE_I32: u8 = 1; +const SPACE_PLANE: u8 = 3; + +/// What a query produced. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Answer { + /// Row count. + Count(u64), + /// Σ of the lane over the rows. + Sum(i64), + /// Minimum, `None` for no rows. + Min(Option), + /// Maximum, `None` for no rows. + Max(Option), + /// The rows were written into the caller's mask. + Kept, +} + +/// An answer and what it cost. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Run { + /// The answer. + pub answer: Answer, + /// mask-risc ops executed (the facade passes). + pub passes: usize, + /// mask-risc programs executed; `0` when the answer was known from the + /// description alone. + pub programs: usize, +} + +/// Why a query was refused. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum RelError { + /// The dialect or mask-risc refused the lowering. + Fold(FoldError), + /// `Measure::Keep` without a mask to write into. + NoKeepSink, +} + +impl From for RelError { + fn from(e: FoldError) -> Self { + RelError::Fold(e) + } +} + +/// Rewrite the query, then lower and run it. +pub fn run(q: &Query, planes: &Planes<'_>, keep: Option<&mut [u64]>) -> Result { + let rel = normalize(&q.rel); + if let Some(answer) = symbolic(&rel, q.measure, planes.n_rows) { + return Ok(Run { + answer, + passes: 0, + programs: 0, + }); + } + run_as_written( + &Query { + rel, + measure: q.measure, + }, + planes, + keep, + ) +} + +/// Lower and run the query exactly as written, without any rewrite. The +/// reference the rewrites are measured against. +pub fn run_as_written( + q: &Query, + planes: &Planes<'_>, + keep: Option<&mut [u64]>, +) -> Result { + let mut d = match (q.measure, keep) { + (Measure::Keep, Some(sink)) => FoldDialect::with_keep(planes, &Foreign::NONE, sink), + (Measure::Keep, None) => return Err(RelError::NoKeepSink), + _ => FoldDialect::new(planes, &Foreign::NONE), + }; + let mut stack = Vec::new(); + lower_rel(&mut d, &mut stack, &q.rel)?; + let answer = match q.measure { + Measure::Count => { + call(&mut d, POP_COUNT, [0; 3], &mut stack)?; + Answer::Count(scalar(&mut stack)? as u64) + } + Measure::Sum(lane) => { + load(&mut d, &mut stack, SPACE_I32, lane)?; + call(&mut d, SUM, [0; 3], &mut stack)?; + Answer::Sum(scalar(&mut stack)?) + } + Measure::Min(lane) => { + load(&mut d, &mut stack, SPACE_I32, lane)?; + call(&mut d, MIN, [0; 3], &mut stack)?; + let v = scalar(&mut stack)?; + Answer::Min((v != i64::MAX).then_some(v as i32)) + } + Measure::Max(lane) => { + load(&mut d, &mut stack, SPACE_I32, lane)?; + call(&mut d, MAX, [0; 3], &mut stack)?; + let v = scalar(&mut stack)?; + Answer::Max((v != i64::MIN).then_some(v as i32)) + } + Measure::Keep => { + call(&mut d, KEEP, [0; 3], &mut stack)?; + Answer::Kept + } + }; + Ok(Run { + answer, + passes: d.facade_passes(), + programs: d.programs_run(), + }) +} + +fn call( + d: &mut FoldDialect<'_>, + f: FnIndex, + v: [u8; 3], + s: &mut Vec, +) -> Result<(), FoldError> { + d.call(f, v, s) +} + +fn load(d: &mut FoldDialect<'_>, s: &mut Vec, space: u8, idx: u16) -> Result<(), FoldError> { + s.push(Val::Scalar(i64::from(idx))); + call(d, LOAD, [space, 0, 0], s) +} + +fn scalar(s: &mut Vec) -> Result { + match s.pop() { + Some(Val::Scalar(v)) => Ok(v), + _ => Err(FoldError::WrongOperandKind(POP_COUNT)), + } +} + +/// The empty population: `RANGE 0 0`, which reads no lane. +fn empty(d: &mut FoldDialect<'_>, s: &mut Vec) -> Result<(), FoldError> { + call(d, RANGE, [0, 0, 0], s) +} + +/// Push the mask of `rel`. +fn lower_rel(d: &mut FoldDialect<'_>, s: &mut Vec, rel: &Rel) -> Result<(), FoldError> { + match rel { + Rel::Empty => empty(d, s), + Rel::All => { + empty(d, s)?; + call(d, INT_NOT, [0; 3], s) + } + Rel::Plane(p) => load(d, s, SPACE_PLANE, *p), + Rel::Atom(a) => lower_atom(d, s, *a), + Rel::Not(c) => { + lower_rel(d, s, c)?; + call(d, INT_NOT, [0; 3], s) + } + Rel::And(cs) => fold(d, s, cs, INT_AND, &Rel::All), + Rel::Or(cs) => fold(d, s, cs, INT_OR, &Rel::Empty), + } +} + +fn fold( + d: &mut FoldDialect<'_>, + s: &mut Vec, + cs: &[Rel], + op: FnIndex, + unit: &Rel, +) -> Result<(), FoldError> { + let Some((first, rest)) = cs.split_first() else { + return lower_rel(d, s, unit); + }; + lower_rel(d, s, first)?; + for c in rest { + lower_rel(d, s, c)?; + call(d, op, [0; 3], s)?; + } + Ok(()) +} + +fn lower_atom(d: &mut FoldDialect<'_>, s: &mut Vec, a: Atom) -> Result<(), FoldError> { + match a { + Atom::U32 { lane, eq, v } => { + load(d, s, SPACE_U32, lane)?; + s.push(Val::Scalar(i64::from(v))); + call(d, INT_EQUAL, [0; 3], s)?; + if !eq { + call(d, INT_NOT, [0; 3], s)?; + } + Ok(()) + } + Atom::I32 { lane, op, t } => { + let t = Val::Scalar(i64::from(t)); + // `IntSLess` is the only ordered compare: `<` is `lane < t`, `>` + // is `t < lane`, and `<=` / `>=` are the negations of `>` / `<`. + match op { + Cmp::Lt | Cmp::Ge => { + load(d, s, SPACE_I32, lane)?; + s.push(t); + call(d, INT_S_LESS, [0; 3], s)?; + } + Cmp::Gt | Cmp::Le => { + s.push(t); + load(d, s, SPACE_I32, lane)?; + call(d, INT_S_LESS, [0; 3], s)?; + } + Cmp::Eq | Cmp::Ne => { + load(d, s, SPACE_I32, lane)?; + s.push(t); + call(d, INT_EQUAL, [0; 3], s)?; + } + } + if matches!(op, Cmp::Ge | Cmp::Le | Cmp::Ne) { + call(d, INT_NOT, [0; 3], s)?; + } + Ok(()) + } + } +} diff --git a/crates/lance-graph-relalg/src/normalize.rs b/crates/lance-graph-relalg/src/normalize.rs new file mode 100644 index 000000000..c67eb7582 --- /dev/null +++ b/crates/lance-graph-relalg/src/normalize.rs @@ -0,0 +1,325 @@ +//! 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. + +use std::collections::{BTreeMap, BTreeSet}; + +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 +} + +/// The answer, if the description alone determines it: no row is read and +/// no program runs. +pub fn symbolic(rel: &Rel, m: Measure, n_rows: usize) -> Option { + match (rel, m) { + (Rel::Empty, Measure::Count) => Some(Answer::Count(0)), + (Rel::Empty, Measure::Sum(_)) => Some(Answer::Sum(0)), + (Rel::Empty, Measure::Min(_)) => Some(Answer::Min(None)), + (Rel::Empty, Measure::Max(_)) => Some(Answer::Max(None)), + (Rel::All, Measure::Count) => Some(Answer::Count(n_rows as u64)), + _ => None, + } +} + +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 }, + } +} + +/// 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 simplify(rel: &Rel) -> Rel { + 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), + } + } + 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 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::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 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, + } +} + +/// 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), + } +} diff --git a/crates/lance-graph-relalg/tests/rewrites.rs b/crates/lance-graph-relalg/tests/rewrites.rs new file mode 100644 index 000000000..e1dbfb304 --- /dev/null +++ b/crates/lance-graph-relalg/tests/rewrites.rs @@ -0,0 +1,469 @@ +//! D-RA-1: every rewrite is checked three ways — the rewritten query, the +//! query as written, and a row-at-a-time oracle over the same lanes must give +//! the same answer — and the rewrites that change cost are pinned by the +//! passes they save. + +use lance_graph_mask_risc::{words_for, ExecError, LaneRef, Planes}; +use lance_graph_r2il::FoldError; +use lance_graph_relalg::{ + normalize, run, run_as_written, Answer, Atom, Cmp, Measure, Query, Rel, RelError, +}; + +const N: usize = 1_000; + +// Lane indexes. +const X: u16 = 0; // i32, (i % 50) - 20: negatives, zero, positives +const Y: u16 = 1; // i32, (i * 7) % 31 +const V: u16 = 2; // i32, the summed value +const K: u16 = 3; // u32, i % 5 + +struct Fixture { + x: Vec, + y: Vec, + v: Vec, + k: Vec, + p0: Vec, + p1: Vec, +} + +fn plane(f: impl Fn(usize) -> bool) -> Vec { + let mut w = vec![0u64; words_for(N)]; + for r in (0..N).filter(|&r| f(r)) { + w[r / 64] |= 1 << (r % 64); + } + w +} + +fn fixture() -> Fixture { + Fixture { + x: (0..N).map(|i| (i % 50) as i32 - 20).collect(), + y: (0..N).map(|i| ((i * 7) % 31) as i32).collect(), + v: (0..N).map(|i| (i % 13) as i32 - 6).collect(), + k: (0..N).map(|i| (i % 5) as u32).collect(), + p0: plane(|r| r % 3 == 0), + p1: plane(|r| r % 7 < 3), + } +} + +/// Run `f` with the fixture's planes. +fn with_planes(fx: &Fixture, f: impl FnOnce(&Planes<'_>) -> T) -> T { + let lanes = [ + LaneRef::I32(&fx.x), + LaneRef::I32(&fx.y), + LaneRef::I32(&fx.v), + LaneRef::U32(&fx.k), + ]; + let masks: [&[u64]; 2] = [&fx.p0, &fx.p1]; + let planes = Planes { + n_rows: N, + masks: &masks, + lanes: &lanes, + }; + f(&planes) +} + +// ── the row oracle ───────────────────────────────────────────────────────── + +fn atom_holds(fx: &Fixture, a: Atom, r: usize) -> bool { + match a { + Atom::I32 { lane, op, t } => { + let x = match lane { + X => fx.x[r], + Y => fx.y[r], + V => fx.v[r], + _ => unreachable!("fixture has no I32 lane {lane}"), + }; + 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, + } + } + Atom::U32 { lane, eq, v } => { + assert_eq!(lane, K); + (fx.k[r] == v) == eq + } + } +} + +fn holds(fx: &Fixture, rel: &Rel, r: usize) -> bool { + match rel { + Rel::All => true, + Rel::Empty => false, + Rel::Plane(p) => { + let w = if *p == 0 { &fx.p0 } else { &fx.p1 }; + w[r / 64] >> (r % 64) & 1 == 1 + } + Rel::Atom(a) => atom_holds(fx, *a, r), + Rel::And(cs) => cs.iter().all(|c| holds(fx, c, r)), + Rel::Or(cs) => cs.iter().any(|c| holds(fx, c, r)), + Rel::Not(c) => !holds(fx, c, r), + } +} + +fn oracle(fx: &Fixture, q: &Query) -> (Answer, Vec) { + let rows: Vec = (0..N).filter(|&r| holds(fx, &q.rel, r)).collect(); + let mask = plane(|r| holds(fx, &q.rel, r)); + let vals = |l: u16| -> Vec { + let lane = if l == X { + &fx.x + } else if l == Y { + &fx.y + } else { + &fx.v + }; + rows.iter().map(|&r| lane[r]).collect() + }; + let a = match q.measure { + Measure::Count => Answer::Count(rows.len() as u64), + Measure::Sum(l) => Answer::Sum(vals(l).iter().map(|&v| i64::from(v)).sum()), + Measure::Min(l) => Answer::Min(vals(l).into_iter().min()), + Measure::Max(l) => Answer::Max(vals(l).into_iter().max()), + Measure::Keep => Answer::Kept, + }; + (a, mask) +} + +/// One run's result and the mask it kept. +type Ran = (Result, Vec); + +/// Rewritten and as-written answers, each with its kept mask. +fn both(fx: &Fixture, q: &Query) -> (Ran, Ran) { + with_planes(fx, |planes| { + let mut k1 = vec![0u64; words_for(N)]; + let mut k2 = vec![0u64; words_for(N)]; + let r1 = run(q, planes, Some(&mut k1)); + let r2 = run_as_written(q, planes, Some(&mut k2)); + ((r1, k1), (r2, k2)) + }) +} + +/// The one refusal the as-written lowering may give: one fold needs more +/// scratch slots than the dialect has (every negation takes a fresh slot). +fn out_of_slots(e: &RelError) -> bool { + matches!( + e, + RelError::Fold(FoldError::Exec(ExecError::ScratchBufferTooSmall { .. })) + ) +} + +// ── a deterministic generator of small descriptions ──────────────────────── + +struct Gen(u64); + +impl Gen { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + + fn pick(&mut self, xs: &[T]) -> T { + xs[(self.next() % xs.len() as u64) as usize] + } + + fn atom(&mut self) -> Rel { + if self.next().is_multiple_of(4) { + let v = (self.next() % 6) as u32; + return if self.next().is_multiple_of(2) { + Rel::eq_u32(K, v) + } else { + Rel::ne_u32(K, v) + }; + } + let lane = self.pick(&[X, X, Y]); + let op = self.pick(&[Cmp::Lt, Cmp::Le, Cmp::Gt, Cmp::Ge, Cmp::Eq, Cmp::Ne]); + let t = self.pick(&[-21, -20, -5, 0, 1, 7, 15, 29, 30, i32::MIN, i32::MAX]); + Rel::i32(lane, op, t) + } + + /// A tree naming at most `budget` atoms (so the as-written lowering fits + /// the dialect's scratch slots). + fn rel(&mut self, depth: u32, budget: &mut u32) -> Rel { + if depth == 0 || *budget <= 1 || self.next().is_multiple_of(3) { + debug_assert!(*budget > 0); + // Every leaf costs a scratch slot, planes included. + *budget = budget.saturating_sub(1); + return match self.next() % 8 { + 0 => Rel::Plane((self.next() % 2) as u16), + 1 => Rel::Not(Box::new(Rel::Plane((self.next() % 2) as u16))), + _ => self.atom(), + }; + } + match self.next() % 3 { + 0 => Rel::Not(Box::new(self.rel(depth - 1, budget))), + k => { + // Stop adding children once the leaf budget is spent. + let n = 2 + (self.next() % 2) as usize; + let mut cs = Vec::new(); + while cs.len() < n && *budget > 0 { + cs.push(self.rel(depth - 1, budget)); + } + if k == 1 { + Rel::And(cs) + } else { + Rel::Or(cs) + } + } + } + } +} + +const MEASURES: [Measure; 5] = [ + Measure::Count, + Measure::Sum(V), + Measure::Min(X), + Measure::Max(Y), + Measure::Keep, +]; + +/// FAILS IF: any rewrite changes which rows a description selects — the +/// rewritten answer, the as-written answer and the row oracle must agree on +/// every measure, kept masks included — or a rewrite is not idempotent. +#[test] +fn rewritten_equals_as_written_equals_row_oracle() { + let fx = fixture(); + let mut g = Gen(0xD0_0D); + let mut changed = 0; + let mut refused = 0; + for i in 0..400 { + let mut budget = 3; + let rel = g.rel(3, &mut budget); + let norm = normalize(&rel); + assert_eq!(normalize(&norm), norm, "not idempotent: {rel:?}"); + if norm != rel { + changed += 1; + } + for m in MEASURES { + let q = Query { + rel: rel.clone(), + measure: m, + }; + let (want, want_mask) = oracle(&fx, &q); + let ((r1, k1), (r2, k2)) = both(&fx, &q); + let r1 = r1.unwrap_or_else(|e| panic!("#{i} rewritten {rel:?}: {e:?}")); + assert_eq!(r1.answer, want, "#{i} rewritten {rel:?} -> {norm:?} {m:?}"); + if m == Measure::Keep { + assert_eq!(k1, want_mask, "#{i} rewritten keep {rel:?}"); + } + match r2 { + Ok(r2) => { + assert_eq!(r2.answer, want, "#{i} as written {rel:?} {m:?}"); + if m == Measure::Keep { + assert_eq!(k2, want_mask, "#{i} as written keep {rel:?}"); + } + } + Err(e) if out_of_slots(&e) => refused += 1, + Err(e) => panic!("#{i} as written {rel:?}: {e:?}"), + } + } + } + // Anti-vacuity: the generator must reach the rewrites, or this test only + // proves the identity. + eprintln!("rewritten {changed}/400 descriptions; as written refused {refused} runs"); + assert!( + changed * 3 > 400, + "only {changed}/400 descriptions were rewritten" + ); + // The as-written arm must still be the comparison most of the time. + assert!( + refused * 10 < 400 * MEASURES.len(), + "as written refused {refused} runs" + ); +} + +/// Count both ways against the oracle. The as-written run is `None` when it +/// ran out of scratch slots. +fn count(fx: &Fixture, rel: Rel) -> (lance_graph_relalg::Run, Option) { + let q = Query { + rel, + measure: Measure::Count, + }; + let (want, _) = oracle(fx, &q); + let ((r1, _), (r2, _)) = both(fx, &q); + let r1 = r1.expect("rewritten"); + assert_eq!(r1.answer, want); + let r2 = match r2 { + Ok(r2) => { + assert_eq!(r2.answer, want); + Some(r2) + } + Err(e) if out_of_slots(&e) => None, + Err(e) => panic!("as written: {e:?}"), + }; + (r1, r2) +} + +/// Both runs, the as-written one required. +fn count_both(fx: &Fixture, rel: Rel) -> (lance_graph_relalg::Run, lance_graph_relalg::Run) { + let (r1, r2) = count(fx, rel); + (r1, r2.expect("as written ran out of slots")) +} + +/// FAILS IF: comparisons on one lane are not fused into one interval. +#[test] +fn comparisons_on_one_lane_fuse_into_one_interval() { + let rel = Rel::And(vec![ + Rel::i32(X, Cmp::Lt, 30), + Rel::i32(X, Cmp::Le, 19), + Rel::i32(X, Cmp::Ge, -5), + Rel::i32(X, Cmp::Gt, -10), + ]); + assert_eq!( + normalize(&rel), + Rel::And(vec![Rel::i32(X, Cmp::Lt, 20), Rel::i32(X, Cmp::Gt, -6)]) + ); + let (r1, r2) = count_both(&fixture(), rel); + assert!(r1.passes < r2.passes, "{} vs {}", r1.passes, r2.passes); +} + +/// FAILS IF: fusion merges comparisons on different lanes. +#[test] +fn comparisons_on_different_lanes_stay_apart() { + let rel = Rel::And(vec![Rel::i32(X, Cmp::Lt, 5), Rel::i32(Y, Cmp::Lt, 3)]); + assert_eq!(normalize(&rel).atoms(), 2); + count(&fixture(), rel); +} + +/// FAILS IF: an excluded value at an interval end is not folded into the +/// bound, or a single surviving value is not an equality. +#[test] +fn exclusions_at_the_ends_tighten_the_interval() { + let base = vec![ + Rel::i32(X, Cmp::Ge, 0), + Rel::i32(X, Cmp::Le, 3), + Rel::i32(X, Cmp::Ne, 0), + Rel::i32(X, Cmp::Ne, 3), + ]; + assert_eq!( + normalize(&Rel::And(base.clone())), + Rel::And(vec![Rel::i32(X, Cmp::Lt, 3), Rel::i32(X, Cmp::Gt, 0)]) + ); + let mut one = base; + one.push(Rel::i32(X, Cmp::Ne, 1)); + assert_eq!(normalize(&Rel::And(one.clone())), Rel::i32(X, Cmp::Eq, 2)); + count(&fixture(), Rel::And(one)); +} + +/// FAILS IF: a contradiction is executed instead of answered. +#[test] +fn a_contradiction_is_answered_without_a_program() { + let fx = fixture(); + for rel in [ + Rel::And(vec![Rel::i32(X, Cmp::Lt, 5), Rel::i32(X, Cmp::Gt, 10)]), + Rel::And(vec![Rel::eq_u32(K, 1), Rel::eq_u32(K, 2)]), + Rel::And(vec![Rel::eq_u32(K, 1), Rel::ne_u32(K, 1)]), + Rel::And(vec![Rel::Plane(0), Rel::Not(Box::new(Rel::Plane(0)))]), + Rel::i32(X, Cmp::Lt, i32::MIN), + Rel::i32(X, Cmp::Gt, i32::MAX), + ] { + assert_eq!(normalize(&rel), Rel::Empty, "{rel:?}"); + for m in [ + Measure::Count, + Measure::Sum(V), + Measure::Min(X), + Measure::Max(X), + ] { + let q = Query { + rel: rel.clone(), + measure: m, + }; + let r = with_planes(&fx, |p| run(&q, p, None)).expect("run"); + assert_eq!(r.answer, oracle(&fx, &q).0, "{rel:?} {m:?}"); + assert_eq!(r.programs, 0, "{rel:?} {m:?} ran a program"); + } + } +} + +/// FAILS IF: a tautology's count is executed instead of answered. +#[test] +fn a_tautology_is_counted_without_a_program() { + let fx = fixture(); + for rel in [ + Rel::Or(vec![Rel::i32(X, Cmp::Lt, 5), Rel::i32(X, Cmp::Ge, 5)]), + Rel::Or(vec![Rel::Plane(1), Rel::Not(Box::new(Rel::Plane(1)))]), + Rel::i32(X, Cmp::Le, i32::MAX), + Rel::i32(X, Cmp::Ge, i32::MIN), + ] { + assert_eq!(normalize(&rel), Rel::All, "{rel:?}"); + let (r, _) = count(&fx, rel); + assert_eq!(r.answer, Answer::Count(N as u64)); + assert_eq!(r.programs, 0); + } +} + +/// FAILS IF: overlapping or adjacent intervals in a union are not merged. +#[test] +fn a_union_of_intervals_merges() { + assert_eq!( + normalize(&Rel::Or(vec![ + Rel::i32(X, Cmp::Lt, 5), + Rel::i32(X, Cmp::Lt, 9) + ])), + Rel::i32(X, Cmp::Lt, 9) + ); + let eqs = Rel::Or(vec![ + Rel::i32(X, Cmp::Eq, 3), + Rel::i32(X, Cmp::Eq, 5), + Rel::i32(X, Cmp::Eq, 4), + ]); + assert_eq!( + normalize(&eqs), + Rel::And(vec![Rel::i32(X, Cmp::Lt, 6), Rel::i32(X, Cmp::Gt, 2)]) + ); + let (r1, r2) = count_both(&fixture(), eqs); + assert!(r1.passes < r2.passes, "{} vs {}", r1.passes, r2.passes); + // A gap stays a gap. + let gap = Rel::Or(vec![Rel::i32(X, Cmp::Eq, 3), Rel::i32(X, Cmp::Eq, 5)]); + assert_eq!(normalize(&gap).atoms(), 2); + count(&fixture(), gap); +} + +/// FAILS IF: `x ∧ (x ∨ y)` is not reduced to `x`. +#[test] +fn absorption() { + let rel = Rel::And(vec![ + Rel::Plane(0), + Rel::Or(vec![Rel::Plane(0), Rel::i32(Y, Cmp::Lt, 3)]), + ]); + assert_eq!(normalize(&rel), Rel::Plane(0)); + count(&fixture(), rel); +} + +/// FAILS IF: a negation is not pushed to the leaves. +#[test] +fn negation_reaches_the_leaves() { + let rel = Rel::Not(Box::new(Rel::And(vec![ + Rel::i32(X, Cmp::Lt, 5), + Rel::Plane(0), + ]))); + assert_eq!( + normalize(&rel), + Rel::Or(vec![ + Rel::i32(X, Cmp::Gt, 4), + Rel::Not(Box::new(Rel::Plane(0))) + ]) + ); + count(&fixture(), rel); +} + +/// FAILS IF: the rewrite stops shrinking a wide conjunction — as written it +/// needs more scratch slots than one fold has and is refused; rewritten it is +/// one interval and runs. +#[test] +fn a_wide_conjunction_runs_only_after_the_rewrite() { + let rel = Rel::And((0..10).map(|i| Rel::i32(X, Cmp::Lt, 20 - i)).collect()); + let fx = fixture(); + let q = Query { + rel, + measure: Measure::Count, + }; + let ((r1, _), (r2, _)) = both(&fx, &q); + assert!(r2.as_ref().is_err_and(out_of_slots), "as written: {r2:?}"); + assert_eq!(r1.expect("rewritten").answer, oracle(&fx, &q).0); +} From b18a0ebfa254415bb793ddf5c343cee2c42d9211 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 22:40:48 +0000 Subject: [PATCH 2/4] relalg: plan, board rows, crate doc as a D-CMR prototype relalg-v1 maps the crate onto D-CMR: the rules are D-CMR-6 constraint propagation over residual comparisons, the R2IL lowering is D-CMR-2's job by NAL's route, and D-RA-2 moves the rules into the contract set IR. Measured in the plan: 8 -> 2 mask-risc ops for four comparisons on one lane, contradictions and tautologies with no program, and 70 of 2,000 small descriptions that fit one fold only after the rewrite. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .claude/board/INTEGRATION_PLANS.md | 8 +++ .claude/board/STATUS_BOARD.md | 11 ++++ .claude/plans/relalg-v1.md | 71 +++++++++++++++++++++ crates/lance-graph-relalg/src/lib.rs | 27 ++++++++ crates/lance-graph-relalg/tests/rewrites.rs | 8 +++ 5 files changed, 125 insertions(+) create mode 100644 .claude/plans/relalg-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index eb4050f40..f092f5393 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,11 @@ +## 2026-10-13 (2) — relalg-v1 — relational algebra over coordinate populations, rewritten before it runs → `.claude/plans/relalg-v1.md` + +**Status:** D-RA-1 MEASURED (prototype crate); D-RA-2..4 PROPOSAL. A prototype for D-CMR, not a competing IR. + +- `Rel` describes a row set of one table; `normalize` applies De Morgan, unit/zero, complement, value-interval fusion per lane, interval union and absorption to a fixpoint; `∅` and (for a count) `U` are answered without a program; everything else lowers through R2IL over `FoldDialect`. +- Measured: == row oracle on 400 generated descriptions × 5 measures; four comparisons on one lane 8 → 2 mask-risc ops; 70/2,000 small descriptions do not fit one fold as written (each negation takes a scratch slot), all fit after the rewrite. +- D-RA-2 moves the rules into the contract set IR (D-CMR-1/-6); Datalog text (D-RA-3) and bound recursion (D-RA-4) wait for it. + ## 2026-10-13 (1) — d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result → `.claude/plans/d-cmr-concept-chain-normalization-v1.md` **Status:** PROPOSAL D-CMR-0..9, revised to a set-theory IR (see the last bullet). Only D-CMR-0 (plan, board rows) is in the PR; no code, no dependency. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 64841a178..1859a0728 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,14 @@ +## D-RA — Relational algebra over coordinate populations, a D-CMR prototype (2026-10-13) + +Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own workspace root, excluded). Prototype for D-CMR-6 rules over residual comparisons and a lowering through R2IL. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | In PR (10 tests, 8 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 | Queued (maintainer decision) | relalg tests pass unchanged against the contract IR | +| **D-RA-3** | Thin Datalog front end, non-recursive | Queued (after D-RA-2) | parsed == hand-written `Rel` | +| **D-RA-4** | Bound recursion via external frontier driver over D-CMR-5 preimage | Queued (after D-CMR-5) | == row-oracle closure; frontier past bound refused | + ## D-CMR — Concept-chain normalization: preserve the equation, not the intermediate result (2026-10-13) Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RESET. One new IR (set theory, plan §3.1 insufficiency proof); no method-body algebra, no dependency. diff --git a/.claude/plans/relalg-v1.md b/.claude/plans/relalg-v1.md new file mode 100644 index 000000000..948b5592e --- /dev/null +++ b/.claude/plans/relalg-v1.md @@ -0,0 +1,71 @@ +# relalg-v1 — relational algebra over coordinate populations, rewritten before it runs + +**Status:** D-RA-1 MEASURED (prototype crate `crates/lance-graph-relalg`, own +workspace root, excluded). D-RA-2..4 PROPOSAL. +**Date:** 2026-10-13. **Repo:** lance-graph. +**Relation to D-CMR:** a prototype for +`d-cmr-concept-chain-normalization-v1.md`. It tests the rule catalogue (D-CMR-6) +on residual comparisons and a lowering through R2IL (D-CMR-2's job, via the +route NAL uses). It is not a third frontend syntax and not the home of the set +algebra; D-CMR puts that in `lance-graph-contract` (D-CMR-1). + +## 1. What D-RA-1 built + +- `Rel`: a set of rows of one table, described (`All`, `Empty`, a resident + plane, one comparison on one `I32` or `U32` lane, `And` / `Or` / `Not`), and + a `Measure` (`Count`, `Sum`, `Min`, `Max`, `Keep`). +- `normalize`: to a fixpoint — negation to the leaves; flattening, unit and + zero; duplicates; `p ∧ ¬p = ∅`, `p ∨ ¬p = U`; per `I32` lane in a + conjunction, one value interval plus the excluded values inside it, `∅` when + empty; per lane in a disjunction, overlapping or adjacent intervals merged, + `U` when they cover the lane; `U32` equalities agree or contradict; + absorption. Intervals are emitted as `<` / `>` / `==`, the forms + `IntSLess` / `IntEqual` lower without a negation pass. +- `symbolic`: `∅` answers `Count 0`, `Sum 0`, `Min/Max None`; `U` answers + `Count n_rows`. No program runs. +- `run`: R2IL calls over `FoldDialect` (`LOAD`, `IntSLess`, `IntEqual`, + `IntAnd`, `IntOr`, `IntNot`, `RANGE`, then `PopCount` / `SUM` / `MIN` / + `MAX` / `KEEP`). mask-risc executes; the crate has no row loop. + +In D-CMR terms every comparison here is a residual: the lanes are not a proven +row ordering, so no row interval (`Runs`) is formed. The interval work is +constraint propagation over value intervals of one lane (§3.5's first +mechanism), not geometry. + +## 2. Measured (`cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml`) + +| test | result | +|---|---| +| 400 generated descriptions × 5 measures: rewritten == as written == row oracle, idempotent | 273/400 rewritten; 70 of 2,000 as-written runs refused (below) | +| four comparisons on one lane | rewritten 2 mask-risc ops, as written 8 | +| `x=3 ∨ x=4 ∨ x=5` | rewritten 2 ops, as written 5 | +| contradictions (`x<5 ∧ x>10`, `k=1 ∧ k=2`, `k=1 ∧ k≠1`, `p ∧ ¬p`, `xMAX`) | answered with 0 programs, all four scalar measures | +| tautologies (`x<5 ∨ x≥5`, `p ∨ ¬p`, `x≤MAX`, `x≥MIN`) | `Count = n_rows`, 0 programs | +| ten comparisons on one lane | as written refused (`ScratchBufferTooSmall`), rewritten runs | + +Eight disable runs, each red: fusing across lanes, no symbolic answer, no +absorption, union ignoring adjacency, no end tightening, `≤` negated to `≥`, +no complement check, `<` off by one. + +**Finding:** normalization decides whether a description fits one fold, not +only how fast it runs. `FoldDialect` gives one fold 8 scratch slots and every +negation as written takes a fresh one, so 70 of 2,000 small descriptions (at +most three leaves) do not lower as written at all. After the rewrite every one +of them runs. + +## 3. Path + +| D-id | step | gate / falsifier | +|---|---|---| +| D-RA-1 | Prototype: `Rel`, `normalize`, `symbolic`, R2IL lowering | == row oracle on generated descriptions; each guard removal fails | +| D-RA-2 | Move the rules into the contract set IR (D-CMR-1/-6) with a universe per set; relalg keeps only the R2IL lowering, or is deleted | relalg's tests pass unchanged against the contract IR | +| D-RA-3 | Thin Datalog front end: rule text → `Rel` (non-recursive rules, constants bound to lanes) | parsed rules == hand-written `Rel` on the D-RA-1 suite | +| D-RA-4 | Bound recursion: `ancestor(c, Y)` as a frontier fixpoint in an external driver (option d′ of `entries/2026-10-03-coresearch-chained-hop.md`), each step a D-CMR-5 preimage; unbound closure refused | == row oracle closure; a step that grows the frontier past its bound is refused, never truncated | + +D-RA-2 is a decision for the maintainer (see the PR). D-RA-3 and D-RA-4 wait +for it. + +## 4. Not built + +Joins (a hop is a preimage over coordinates, D-CMR-5, never a foreign key), +recursion, row intervals, `Sum(A) − Sum(A∧B)`, Datalog text. diff --git a/crates/lance-graph-relalg/src/lib.rs b/crates/lance-graph-relalg/src/lib.rs index 992f8085f..c36764941 100644 --- a/crates/lance-graph-relalg/src/lib.rs +++ b/crates/lance-graph-relalg/src/lib.rs @@ -1,5 +1,32 @@ //! `lance-graph-relalg` — relational algebra over coordinate populations //! (D-RA-1, `.claude/plans/relalg-v1.md`). +//! +//! A PROTOTYPE for D-CMR (`.claude/plans/d-cmr-concept-chain-normalization-v1.md`): +//! rearrange the description of a query with proven identities before anything +//! runs, and lower only the irreducible remainder. +//! +//! # What it holds +//! +//! - [`Rel`]: a set of rows of one table, described — `All`, `Empty`, a +//! resident plane, a comparison on one lane, `And` / `Or` / `Not`. In D-CMR +//! terms every comparison is a residual (`Res`): the lanes are not a proven +//! row ordering, so no row interval (`Runs`) is formed here. +//! - [`normalize()`]: the rewrites, to a fixpoint (see [`mod@normalize`]'s +//! module doc). The interval work is constraint propagation over VALUE intervals of +//! one lane — narrow bounds, detect `∅` — not row intervals. +//! - [`symbolic`]: a description that normalizes to `Empty` (or `All`, for a +//! count) is answered without running a program. +//! - [`run`]: lowering into R2IL calls over +//! [`FoldDialect`](lance_graph_r2il::FoldDialect), which builds and runs one +//! mask-risc program per fold. This crate never loops over rows. +//! +//! # What it is not +//! +//! Not a third frontend syntax beside Quack's `Filter` and NAL's R2IL +//! programs, and not the home of the rule catalogue: D-CMR puts the set +//! algebra in `lance-graph-contract`. The rules and tests here are the +//! evidence for that move; recursion (`μ`) and the hop (preimage) are not +//! built. pub mod ir; pub mod lower; diff --git a/crates/lance-graph-relalg/tests/rewrites.rs b/crates/lance-graph-relalg/tests/rewrites.rs index e1dbfb304..48cabd72b 100644 --- a/crates/lance-graph-relalg/tests/rewrites.rs +++ b/crates/lance-graph-relalg/tests/rewrites.rs @@ -319,6 +319,10 @@ fn comparisons_on_one_lane_fuse_into_one_interval() { Rel::And(vec![Rel::i32(X, Cmp::Lt, 20), Rel::i32(X, Cmp::Gt, -6)]) ); let (r1, r2) = count_both(&fixture(), rel); + eprintln!( + "passes: rewritten {} vs as written {}", + r1.passes, r2.passes + ); assert!(r1.passes < r2.passes, "{} vs {}", r1.passes, r2.passes); } @@ -417,6 +421,10 @@ fn a_union_of_intervals_merges() { Rel::And(vec![Rel::i32(X, Cmp::Lt, 6), Rel::i32(X, Cmp::Gt, 2)]) ); let (r1, r2) = count_both(&fixture(), eqs); + eprintln!( + "passes: rewritten {} vs as written {}", + r1.passes, r2.passes + ); assert!(r1.passes < r2.passes, "{} vs {}", r1.passes, r2.passes); // A gap stays a gap. let gap = Rel::Or(vec![Rel::i32(X, Cmp::Eq, 3), Rel::i32(X, Cmp::Eq, 5)]); From c7e4732adc1eb79aaf3baf17c06bc9b72e814eef Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 22:42:07 +0000 Subject: [PATCH 3/4] relalg: no strings in the IR; Datalog rules are algebra values Atom, Cmp and Measure must be Copy (compile-time guard), so no String can enter a description. D-RA-3 is re-scoped: a rule is a Rel built from coordinates; names are labels resolved once through the label codebook, never stored in a rule or used as an address, and text is a label view, never a query path. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .claude/board/INTEGRATION_PLANS.md | 2 +- .claude/board/STATUS_BOARD.md | 2 +- .claude/plans/relalg-v1.md | 5 +++-- crates/lance-graph-relalg/src/ir.rs | 13 ++++++++++++- 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index f092f5393..7f2b6ed79 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -4,7 +4,7 @@ - `Rel` describes a row set of one table; `normalize` applies De Morgan, unit/zero, complement, value-interval fusion per lane, interval union and absorption to a fixpoint; `∅` and (for a count) `U` are answered without a program; everything else lowers through R2IL over `FoldDialect`. - Measured: == row oracle on 400 generated descriptions × 5 measures; four comparisons on one lane 8 → 2 mask-risc ops; 70/2,000 small descriptions do not fit one fold as written (each negation takes a scratch slot), all fit after the rewrite. -- D-RA-2 moves the rules into the contract set IR (D-CMR-1/-6); Datalog text (D-RA-3) and bound recursion (D-RA-4) wait for it. +- D-RA-2 moves the rules into the contract set IR (D-CMR-1/-6); Datalog rules as algebra values with names only as codebook labels (D-RA-3) and bound recursion (D-RA-4) wait for it. ## 2026-10-13 (1) — d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result → `.claude/plans/d-cmr-concept-chain-normalization-v1.md` diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 1859a0728..3f3a132c7 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -6,7 +6,7 @@ Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own work |---|---|---|---| | **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | In PR (10 tests, 8 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 | Queued (maintainer decision) | relalg tests pass unchanged against the contract IR | -| **D-RA-3** | Thin Datalog front end, non-recursive | Queued (after D-RA-2) | parsed == hand-written `Rel` | +| **D-RA-3** | Datalog rules as algebra values; names are labels resolved through the label codebook, never strings in a rule | Queued (after D-RA-2) | codebook-built rules == hand-written `Rel`; unknown label refused at resolution | | **D-RA-4** | Bound recursion via external frontier driver over D-CMR-5 preimage | Queued (after D-CMR-5) | == row-oracle closure; frontier past bound refused | ## D-CMR — Concept-chain normalization: preserve the equation, not the intermediate result (2026-10-13) diff --git a/.claude/plans/relalg-v1.md b/.claude/plans/relalg-v1.md index 948b5592e..5adbc0a23 100644 --- a/.claude/plans/relalg-v1.md +++ b/.claude/plans/relalg-v1.md @@ -59,7 +59,7 @@ of them runs. |---|---|---| | D-RA-1 | Prototype: `Rel`, `normalize`, `symbolic`, R2IL lowering | == row oracle on generated descriptions; each guard removal fails | | D-RA-2 | Move the rules into the contract set IR (D-CMR-1/-6) with a universe per set; relalg keeps only the R2IL lowering, or is deleted | relalg's tests pass unchanged against the contract IR | -| D-RA-3 | Thin Datalog front end: rule text → `Rel` (non-recursive rules, constants bound to lanes) | parsed rules == hand-written `Rel` on the D-RA-1 suite | +| D-RA-3 | Datalog rules as algebra values, not text: a rule is a `Rel` built from coordinates (lane indexes, numeric constants, classids). Names are labels only, resolved through the label codebook to coordinates once; no string is stored in a rule or used as an address. A text rendering is a label view of the value, never a query path | rules built from codebook coordinates == hand-written `Rel`; a rule naming an unknown label is refused at resolution, never kept as a string | | D-RA-4 | Bound recursion: `ancestor(c, Y)` as a frontier fixpoint in an external driver (option d′ of `entries/2026-10-03-coresearch-chained-hop.md`), each step a D-CMR-5 preimage; unbound closure refused | == row oracle closure; a step that grows the frontier past its bound is refused, never truncated | D-RA-2 is a decision for the maintainer (see the PR). D-RA-3 and D-RA-4 wait @@ -68,4 +68,5 @@ for it. ## 4. Not built Joins (a hop is a preimage over coordinates, D-CMR-5, never a foreign key), -recursion, row intervals, `Sum(A) − Sum(A∧B)`, Datalog text. +recursion, row intervals, `Sum(A) − Sum(A∧B)`. Datalog text as a query path +is excluded by design: strings are labels, the query is algebra. diff --git a/crates/lance-graph-relalg/src/ir.rs b/crates/lance-graph-relalg/src/ir.rs index c246651d5..1e0b3f0b8 100644 --- a/crates/lance-graph-relalg/src/ir.rs +++ b/crates/lance-graph-relalg/src/ir.rs @@ -1,5 +1,16 @@ //! The IR. It describes a selection over one table's row space; it never -//! holds rows. +//! holds rows and never holds a string: lanes are indexes, constants are +//! numbers. A name a person reads is a label, resolved through the label +//! codebook before a description is built, never part of it. + +// No string in the IR: an atom and a measure are `Copy`, which a `String` +// field would break at compile time. +const _: fn() = || { + fn copy() {} + copy::(); + copy::(); + copy::(); +}; /// An ordered comparison of an `I32` lane against a constant. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] From 1b2e8f5b22d9616447e037d2c444bb5a725479e2 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 22:55:31 +0000 Subject: [PATCH 4/4] relalg: reconcile I32 inequalities with intervals in a union MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit x = t ∨ x ≠ t stayed unrewritten because equalities went to the interval map and inequalities to the rest (codex review on #1546). A union now treats x ≠ a like the U32 case: a second inequality or an interval holding a covers the lane; otherwise the intervals are inside x ≠ a and absorbed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- crates/lance-graph-relalg/src/normalize.rs | 22 +++++++++++++++ crates/lance-graph-relalg/tests/rewrites.rs | 31 +++++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/crates/lance-graph-relalg/src/normalize.rs b/crates/lance-graph-relalg/src/normalize.rs index c67eb7582..c250e198f 100644 --- a/crates/lance-graph-relalg/src/normalize.rs +++ b/crates/lance-graph-relalg/src/normalize.rs @@ -221,6 +221,7 @@ fn disj(children: Vec) -> Rel { // 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 { @@ -229,6 +230,13 @@ fn disj(children: Vec) -> Rel { 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); @@ -237,6 +245,20 @@ fn disj(children: Vec) -> Rel { } } 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)); + } for (lane, mut iv) in ranges { iv.sort_unstable(); let mut merged: Vec<(i64, i64)> = Vec::new(); diff --git a/crates/lance-graph-relalg/tests/rewrites.rs b/crates/lance-graph-relalg/tests/rewrites.rs index 48cabd72b..cdfa58f35 100644 --- a/crates/lance-graph-relalg/tests/rewrites.rs +++ b/crates/lance-graph-relalg/tests/rewrites.rs @@ -475,3 +475,34 @@ fn a_wide_conjunction_runs_only_after_the_rewrite() { assert!(r2.as_ref().is_err_and(out_of_slots), "as written: {r2:?}"); assert_eq!(r1.expect("rewritten").answer, oracle(&fx, &q).0); } + +/// FAILS IF: a `!=` on an `I32` lane is not reconciled with the intervals +/// beside it in a disjunction (codex review on #1546): `x = t ∨ x ≠ t` and +/// `x ≠ a ∨ x ≠ b` cover the lane; `x ≠ a ∨ (interval without a)` is `x ≠ a`. +#[test] +fn an_inequality_in_a_union_meets_the_intervals() { + let fx = fixture(); + for rel in [ + Rel::Or(vec![Rel::i32(X, Cmp::Eq, 3), Rel::i32(X, Cmp::Ne, 3)]), + Rel::Or(vec![Rel::i32(X, Cmp::Ne, 3), Rel::i32(X, Cmp::Ne, 4)]), + Rel::Or(vec![Rel::i32(X, Cmp::Ne, 3), Rel::i32(X, Cmp::Lt, 10)]), + ] { + assert_eq!(normalize(&rel), Rel::All, "{rel:?}"); + let (r, _) = count(&fx, rel); + assert_eq!(r.programs, 0); + } + let rel = Rel::Or(vec![Rel::i32(X, Cmp::Ne, 3), Rel::i32(X, Cmp::Gt, 10)]); + assert_eq!(normalize(&rel), Rel::i32(X, Cmp::Ne, 3)); + count(&fx, rel); + // The reported shape: the tautology plus three unrelated terms fits no + // fold as written, and must be answered without one. + let wide = Rel::Or(vec![ + Rel::i32(X, Cmp::Eq, 3), + Rel::i32(X, Cmp::Ne, 3), + Rel::i32(Y, Cmp::Le, 3), + Rel::Not(Box::new(Rel::Plane(0))), + Rel::ne_u32(K, 2), + ]); + let (r, _) = count(&fx, wide); + assert_eq!(r.programs, 0); +}