diff --git a/.claude/board/entries/2026-10-22-drmc-5-assoc-probe.md b/.claude/board/entries/2026-10-22-drmc-5-assoc-probe.md new file mode 100644 index 000000000..a66c0314f --- /dev/null +++ b/.claude/board/entries/2026-10-22-drmc-5-assoc-probe.md @@ -0,0 +1,20 @@ +# 2026-10-22 — D-DRMC-5: associativity probe started + +**Status:** probe slice 1 landed on `lab/dr-math-5-assoc-probe-20261022` +(stacked on #1704). Operator request: "start the associativity probe". + +`crates/dr-math-binding-probe/src/relcomp.rs`: typed composition chain over +bound DR64 operands (domains, frame issue, focus, scope, Boolean semiring +only); law admission for `BooleanCompose` over two-valued Distinct; egglog +proof of reassociation from the admitted rule, with commutation refused; +push/compose lowering with a round-trip check; `certify_reassociation`, the +first issuer of a `RecipeCertificate`. + +Measured (example `assoc_orders`, release, 4-vCPU shared Xeon @ 2.10 GHz): +14 orders of one dense-to-sparse 5-chain, same relation, 6 414 to 15 310 +row-ORs, about 4.4 to 10.8 µs per evaluation. Cold egglog proof about +12.5 ms, reported, not a gate. + +OPEN: specialization selection (choose an order without evaluating all of +them), certificate rebinding to a second frame (X8), any GF(2)/M4RI +reduction, R2IL/Quack wiring. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index dd6231c6a..c1b9e6090 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,12 +25,13 @@ 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. -429 entries, 2026-08-06 .. 2026-10-22. +430 entries, 2026-08-06 .. 2026-10-22. | date | entry id | finding | file | |---|---|---|---| | 2026-10-22 | `math-compiler-stage-b-e1` | | [2026-10-22-math-compiler-stage-b-e1.md](2026-10-22-math-compiler-stage-b-e1.md) | | 2026-10-22 | `math-compiler-gap-matrix` | | [2026-10-22-math-compiler-gap-matrix.md](2026-10-22-math-compiler-gap-matrix.md) | +| 2026-10-22 | `D-DRMC-5` | | [2026-10-22-drmc-5-assoc-probe.md](2026-10-22-drmc-5-assoc-probe.md) | | 2026-10-22 | `D-MPS-9` | | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) | | 2026-10-22 | `D-DRMC` | | [2026-10-22-coresearch-drmc-stack.md](2026-10-22-coresearch-drmc-stack.md) | | 2026-10-21 | `zero-copy-join-index-map` | | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) | diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index 1ee8ff503..61a36f8bc 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/crates/dr-math-binding-probe/Cargo.toml @@ -10,6 +10,11 @@ description = "Borrowed DR64 / ClassView-style typed structure and source witnes [dependencies] lance-graph-contract = { path = "../lance-graph-contract" } +# The proof route for D-DRMC-5: public API only (EGraph::new_with_proofs, +# parse_and_run_program, `prove`). egglog checks every proof it returns. +egglog = { git = "https://github.com/AdaWorldAPI/egglog", branch = "main" } +# Compiled identity of a certified lowering (relcomp::lowering_digest). +sha2 = "0.10" [dev-dependencies] lance-graph-act-r = { path = "../lance-graph-act-r" } diff --git a/crates/dr-math-binding-probe/README.md b/crates/dr-math-binding-probe/README.md index 67a671d24..83f1308f7 100644 --- a/crates/dr-math-binding-probe/README.md +++ b/crates/dr-math-binding-probe/README.md @@ -16,3 +16,17 @@ Run from the crate's directory (own `[workspace]`): `cargo test`. **Explicit non-proofs:** `FrameStore` is a lab stand-in for the source owner (the seal proves issue identity, not that the revisions describe real data); focus and scope are caller-supplied values, `MethodSignature` is a fixture rather than registry-resolved ClassView method metadata, no optimized fold or real foreign relation binder executes, no ACL policy is evaluated. Production admission requires the existing source owner, D-RMAP-1A table bindings, D-RFT/D-QSP method law, index seal and permission checks. A bitmap is not a universal row binding and cannot express all graph path multiplicities. Next stack: finite population claim/violation ledger, then compiler recipe eligibility. + +## D-DRMC-5: associativity of Boolean relation composition (`relcomp`) + +The first law the certified-compiler boundary can certify (charter, "Experimental success criterion"). `(R ∘ S) ∘ T = R ∘ (S ∘ T)` over OR/AND is established algebra; the probe tests whether the pieces around it preserve it. + +- **Typing.** A `Chain` composes only where each operand's column domain is the next one's row domain, under one frame issue (still current), one focus and one scope, and only for two-valued Distinct relations. +- **Law admission.** `admit_composition_assoc` admits associativity only for the `BooleanCompose` shape over two-valued Distinct relations; Bag (counting) and three-valued composition are other semirings and are refused. An `AdmittedLaw` has no other constructor. +- **Proof.** egglog, given only the admitted rule (both directions), proves every reassociation of a 5-chain and checks its own proofs. Commutation, which associativity does not imply, gets no proof even with both terms in the e-graph. +- **Lowering.** An order lowers to push/compose steps that raise back to the same order. This is a structural check; the compose kernel is checked against an independent pair enumeration. +- **Certificate.** `certify_reassociation` issues a `RecipeCertificate` (carrying egglog's proof text) only with all of the above, and refuses a law reference for another shape, a non-reassociation, a missing code identity, and a compiled digest that is not `lowering_digest` of the checked lowering. A `Chain` borrows its frame store, so the frame cannot advance while the chain is alive. + +`cargo run --release --example assoc_orders` reports one dense-to-sparse 5-chain on a 4-vCPU shared Xeon @ 2.10 GHz: all 14 orders give the same relation; work runs from 6 414 to 15 310 row-ORs and the time per evaluation from about 4.4 to 10.8 µs. The cold egglog proof between the two extreme orders is about 12.5 ms (a cold, out-of-fold cost: reported, not a gate). + +**Not done:** choosing an order (the specialization-selection gate; the cost above is measured by evaluating every order, which a selector must not do), rebinding a certificate to a second frame (X8), any GF(2)/M4RI reduction, and wiring into R2IL/Quack. diff --git a/crates/dr-math-binding-probe/examples/assoc_orders.rs b/crates/dr-math-binding-probe/examples/assoc_orders.rs new file mode 100644 index 000000000..b15429594 --- /dev/null +++ b/crates/dr-math-binding-probe/examples/assoc_orders.rs @@ -0,0 +1,113 @@ +//! Per-order work and time for one 5-chain, plus the cold egglog proof. +//! Fold times are per evaluation (ns); the proof is a cold, out-of-fold cost, +//! reported in µs and not a gate. +use std::hint::black_box; +use std::time::Instant; + +use dr_math_binding_probe::{ + Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, Scope, + bind_dr64, + recipe::{LawShape, Primitive}, + relcomp::{Chain, RelExpr, Rows, admit_composition_assoc, all_orders, prove_reassociation}, +}; + +fn fill(seed: u64, keep_of_64: u32) -> Rows { + let mut x = seed | 1; + let mut rows = [0u64; 64]; + for r in rows.iter_mut() { + for b in 0..64 { + x ^= x << 13; + x ^= x >> 7; + x ^= x << 17; + if (x % 64) < u64::from(keep_of_64) { + *r |= 1 << b; + } + } + } + rows +} + +fn main() { + let axis = |i: u16| Axis { + class: 10 + i, + kind: AxisKind::Identity, + }; + let method = |i: u16| MethodSignature::presence(10 + i, i, axis(i), axis(i + 1)); + let st = FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: 1, + }); + let (focus, scope) = (Focus { revision: 1 }, Scope { id: 1 }); + // Dense on the left, sparse on the right: the order matters. + let ops: Vec = [48, 32, 16, 4, 1] + .iter() + .enumerate() + .map(|(i, d)| fill(i as u64 + 3, *d)) + .collect(); + let bound = ops + .iter() + .enumerate() + .map(|(i, r)| { + let m = method(i as u16); + let at = Guards { + frame: st.seal(), + focus, + scope, + }; + bind_dr64( + &st, + m, + m, + &at, + (focus, scope), + Operand { + rows: r, + validity: None, + }, + ) + .unwrap() + }) + .collect(); + let chain = Chain::new(&st, bound).unwrap(); + let reference = chain.eval(&all_orders(5)[0]).unwrap().0; + println!("{:<40} {:>8} {:>10}", "order", "row_ors", "ns/eval"); + for o in all_orders(5) { + let (rows, work) = chain.eval(&o).unwrap(); + assert_eq!(rows, reference); + let mut samples = Vec::new(); + for _ in 0..7 { + let t = Instant::now(); + for _ in 0..1000 { + black_box(chain.eval(black_box(&o)).unwrap()); + } + samples.push(t.elapsed().as_nanos() / 1000); + } + samples.sort(); + println!("{:<40} {:>8} {:>10}", show(&o), work.row_ors, samples[3]); + } + let law = admit_composition_assoc(LawShape::for_method(method(0), Primitive::BooleanCompose)) + .unwrap(); + let orders = all_orders(5); + let (from, to) = (&orders[0], orders.last().unwrap()); + let mut us = Vec::new(); + for _ in 0..5 { + let t = Instant::now(); + prove_reassociation(&law, from, to).unwrap(); + us.push(t.elapsed().as_micros()); + } + us.sort(); + println!( + "\ncold egglog proof {} = {} (reported, not a gate): median {} µs", + show(from), + show(to), + us[2] + ); +} + +fn show(o: &RelExpr) -> String { + match o { + RelExpr::Leaf(i) => format!("r{i}"), + RelExpr::Comp(a, b) => format!("({} {})", show(a), show(b)), + } +} diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs index 7d6cd9909..9a22bb00c 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/crates/dr-math-binding-probe/src/lib.rs @@ -277,3 +277,7 @@ pub mod population; /// Reusable mathematical law / proof / compiled artifact identity separation (lab only). pub mod recipe; + +/// Associativity of Boolean relation composition: typing, law admission, +/// egglog proof, lowering check and the first certificate. +pub mod relcomp; diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index d727d7766..612a51eb1 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -78,15 +78,31 @@ pub struct CompiledReference { /// /// ```compile_fail /// use dr_math_binding_probe::recipe::RecipeCertificate; -/// let forged = RecipeCertificate { law: todo!(), compiled: todo!() }; +/// let forged = RecipeCertificate { law: todo!(), compiled: todo!(), proof: todo!() }; /// ``` -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct RecipeCertificate { law: LawReference, compiled: CompiledReference, + proof: String, } impl RecipeCertificate { + /// Only the in-crate certifiers call this, after their own checks + /// (today: [`crate::relcomp::certify_reassociation`]). + pub(crate) fn issue(law: LawReference, compiled: CompiledReference, proof: String) -> Self { + Self { + law, + compiled, + proof, + } + } + + /// The checked proof the certifier was given (egglog's rendering). + pub fn proof(&self) -> &str { + &self.proof + } + pub fn law(&self) -> &LawReference { &self.law } @@ -125,8 +141,10 @@ pub struct RecipeOffer<'a> { /// Cold-stage metadata admission for a mathematically typed, already-bound /// register: effect capability, law shape, law identity, code identity and -/// target first, then certification. Certification refuses for every shape -/// today; see the module docs. +/// target first, then certification. This single-operand path has no +/// certifier for any shape and refuses with `NoCertifiedCompiler`; the one +/// certifier that exists, for reassociating a composition chain, is +/// [`crate::relcomp::certify_reassociation`]. pub fn admit_recipe<'a>( operand: BoundDr64<'a>, primitive: Primitive, @@ -157,9 +175,7 @@ pub fn admit_recipe<'a>( }) } -/// The certified-compiler boundary. It has no implementation for any -/// Boolean-DR64 law shape: that needs a typed relational statement language, -/// egglog laws over it with checked proofs, and a lowering check. +/// The single-operand certifier: none exists for any law shape. fn certify( _law: LawReference, _compiled: CompiledReference, diff --git a/crates/dr-math-binding-probe/src/relcomp.rs b/crates/dr-math-binding-probe/src/relcomp.rs new file mode 100644 index 000000000..cead68a12 --- /dev/null +++ b/crates/dr-math-binding-probe/src/relcomp.rs @@ -0,0 +1,426 @@ +//! D-DRMC-5: associativity of Boolean relation composition, the first law the +//! certified-compiler boundary can certify (charter, "Experimental success +//! criterion"). +//! +//! `(R ∘ S) ∘ T = R ∘ (S ∘ T)` over OR/AND is established algebra. What this +//! probe tests is whether the pieces around it preserve it: +//! +//! 1. **Typing**: a [`Chain`] of bound DR64 operands composes only where each +//! operand's column domain is the next one's row domain, under one frame +//! issue, one focus and one scope, and only for two-valued Distinct +//! relations (the Boolean semiring). +//! 2. **Law admission**: [`admit_composition_assoc`] admits associativity only +//! for the `BooleanCompose` shape over two-valued Distinct relations. An +//! [`AdmittedLaw`] cannot be built any other way. +//! 3. **Proof**: egglog, given only the admitted rule, proves that two +//! association orders of the same chain are equal, and checks its own +//! proof. An equation the admitted rule does not imply (commutation) is +//! refused. +//! 4. **Lowering**: an order lowers to a list of compose steps; +//! [`lower`]/[`raise`] round-trip, and the steps keep the leaves in chain +//! order. This is a structural check of the lowering, not a proof of the +//! compose kernel; the kernel is tested against an independent pair +//! enumeration in `tests/relcomp.rs`. +//! 5. **Certificate**: [`certify_reassociation`] issues a +//! [`RecipeCertificate`] only with all of the above. +//! +//! Cost: composing `A` with `B` ORs one row of `B` per set bit of `A`, so the +//! [`Work`] of an order is the popcount of every left operand it composes. +//! Orders of one chain compute the same relation at different cost; picking +//! one is the specialization-selection question, still open (see README). +//! +//! The compose kernel is plain `u64` word arithmetic, no intrinsics. +use egglog::{CommandOutput, EGraph}; +use sha2::{Digest, Sha256}; + +use crate::recipe::{CompiledReference, LawReference, LawShape, Primitive, RecipeCertificate}; +use crate::{BoundDr64, FrameStore, Population, Truth}; + +/// One 64 × 64 Boolean relation register (512 B). +pub type Rows = [u64; 64]; + +/// An association order over chain positions `0..n`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum RelExpr { + Leaf(usize), + Comp(Box, Box), +} + +impl RelExpr { + pub fn comp(a: RelExpr, b: RelExpr) -> Self { + RelExpr::Comp(Box::new(a), Box::new(b)) + } + + /// Leaves left to right. + pub fn leaves(&self) -> Vec { + match self { + RelExpr::Leaf(i) => vec![*i], + RelExpr::Comp(a, b) => { + let mut v = a.leaves(); + v.extend(b.leaves()); + v + } + } + } + + /// The `Rel` term egglog sees: leaf `i` is `(Base \"r{i}\")`. + pub fn egglog_term(&self) -> String { + match self { + RelExpr::Leaf(i) => format!("(Base \"r{i}\")"), + RelExpr::Comp(a, b) => format!("(Comp {} {})", a.egglog_term(), b.egglog_term()), + } + } +} + +/// Every association order of a chain of `n` operands (Catalan(n-1) of them). +pub fn all_orders(n: usize) -> Vec { + fn range(lo: usize, hi: usize) -> Vec { + if hi - lo == 1 { + return vec![RelExpr::Leaf(lo)]; + } + let mut out = Vec::new(); + for split in lo + 1..hi { + for a in range(lo, split) { + for b in range(split, hi) { + out.push(RelExpr::comp(a.clone(), b)); + } + } + } + out + } + if n == 0 { Vec::new() } else { range(0, n) } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ComposeRefusal { + EmptyChain, + /// Only two-valued Distinct relations compose over OR/AND here. + NotBooleanDistinct { + at: usize, + }, + /// Operand `at`'s column domain is not operand `at + 1`'s row domain. + DomainMismatch { + at: usize, + }, + DifferentFrame { + at: usize, + }, + StaleFrame, + DifferentFocus { + at: usize, + }, + DifferentScope { + at: usize, + }, + /// The order does not cover this chain's positions `0..n` in order. + NotThisChain, +} + +/// Operands that compose in sequence: domains line up, one frame issue that +/// is still current, one focus, one scope. +/// +/// The chain borrows the store it was checked against, so the frame stays +/// current until the chain is dropped: advancing or dropping the store while +/// a chain is alive does not compile. +/// +/// ```compile_fail +/// use dr_math_binding_probe::{FrameRevisions, FrameStore, relcomp::Chain}; +/// let mut st = FrameStore::new(FrameRevisions { source: 1, relation_map: 1, coordinates: 1 }); +/// let chain = Chain::new(&st, Vec::new()); +/// st.advance(FrameRevisions { source: 2, relation_map: 1, coordinates: 1 }); +/// drop(chain); +/// ``` +#[derive(Debug)] +pub struct Chain<'a> { + _store: &'a FrameStore, + operands: Vec>, +} + +impl<'a> Chain<'a> { + pub fn new( + store: &'a FrameStore, + operands: Vec>, + ) -> Result { + let first = operands.first().ok_or(ComposeRefusal::EmptyChain)?; + for (at, op) in operands.iter().enumerate() { + if op.method.truth != Truth::TwoValued || op.method.population != Population::Distinct { + return Err(ComposeRefusal::NotBooleanDistinct { at }); + } + if !op.frame.same_issue(&first.frame) { + return Err(ComposeRefusal::DifferentFrame { at }); + } + if op.focus != first.focus { + return Err(ComposeRefusal::DifferentFocus { at }); + } + if op.scope != first.scope { + return Err(ComposeRefusal::DifferentScope { at }); + } + } + for (at, pair) in operands.windows(2).enumerate() { + if pair[0].method.column != pair[1].method.row { + return Err(ComposeRefusal::DomainMismatch { at }); + } + } + store + .check(&first.frame) + .map_err(|_| ComposeRefusal::StaleFrame)?; + Ok(Self { + _store: store, + operands, + }) + } + + pub fn len(&self) -> usize { + self.operands.len() + } + + pub fn is_empty(&self) -> bool { + self.operands.is_empty() + } + + /// Evaluate one association order with the compose kernel. + pub fn eval(&self, order: &RelExpr) -> Result<(Rows, Work), ComposeRefusal> { + if order.leaves() != (0..self.len()).collect::>() { + return Err(ComposeRefusal::NotThisChain); + } + let mut work = Work::default(); + let rows = self.eval_rec(order, &mut work); + Ok((rows, work)) + } + + fn eval_rec(&self, order: &RelExpr, work: &mut Work) -> Rows { + match order { + RelExpr::Leaf(i) => *self.operands[*i].rows, + RelExpr::Comp(a, b) => { + let (a, b) = (self.eval_rec(a, work), self.eval_rec(b, work)); + compose(&a, &b, work) + } + } + } +} + +/// Row ORs performed: one per set bit of each left operand composed. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)] +pub struct Work { + pub row_ors: u64, +} + +/// `out[i] = OR over j in a[i] of b[j]`: Boolean composition over OR/AND. +pub fn compose(a: &Rows, b: &Rows, work: &mut Work) -> Rows { + let mut out = [0u64; 64]; + for (o, &row) in out.iter_mut().zip(a.iter()) { + let mut bits = row; + while bits != 0 { + *o |= b[bits.trailing_zeros() as usize]; + bits &= bits - 1; + work.row_ors += 1; + } + } + out +} + +// ── law admission ────────────────────────────────────────────────────────── + +/// Associativity, admitted for one law shape. No public constructor: only +/// [`admit_composition_assoc`] makes one. +/// +/// ```compile_fail +/// use dr_math_binding_probe::relcomp::AdmittedLaw; +/// let forged = AdmittedLaw { shape: todo!() }; +/// ``` +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct AdmittedLaw { + shape: LawShape, +} + +impl AdmittedLaw { + pub fn shape(&self) -> LawShape { + self.shape + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum LawRefusal { + /// Associativity is admitted for relation composition only. + NotComposition, + /// Only the Boolean semiring (two-valued, Distinct) is admitted here. + /// Bag (counting) and three-valued composition are other semirings and + /// are not admitted by this probe. + NotBooleanSemiring, +} + +pub fn admit_composition_assoc(shape: LawShape) -> Result { + if shape.primitive != Primitive::BooleanCompose { + return Err(LawRefusal::NotComposition); + } + if shape.truth != Truth::TwoValued || shape.population != Population::Distinct { + return Err(LawRefusal::NotBooleanSemiring); + } + Ok(AdmittedLaw { shape }) +} + +// ── proof (egglog) ───────────────────────────────────────────────────────── + +const HEADER: &str = "(datatype Rel (Base String) (Comp Rel Rel))\n(ruleset assoc)\n\ +(rewrite (Comp (Comp a b) c) (Comp a (Comp b c)) :ruleset assoc)\n\ +(rewrite (Comp a (Comp b c)) (Comp (Comp a b) c) :ruleset assoc)\n"; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum ProofRefusal { + /// The two orders do not share leaves; no rewrite law could relate them. + DifferentLeaves, + /// egglog found no proof from the admitted rule (or failed); its message. + NotProved(String), +} + +/// Ask egglog to prove `from = to` using only the admitted associativity rule +/// (both directions). Returns egglog's proof text; egglog checks every proof +/// it returns. +pub fn prove_reassociation( + law: &AdmittedLaw, + from: &RelExpr, + to: &RelExpr, +) -> Result { + if from.leaves() != to.leaves() { + return Err(ProofRefusal::DifferentLeaves); + } + // Every order of an n-chain is reachable in at most n - 2 rotations. + let fuel = from.leaves().len().max(2); + prove_equation(law, &from.egglog_term(), &to.egglog_term(), fuel) +} + +/// Ask egglog to prove an arbitrary equation between two `Rel` terms from the +/// admitted rule, running it `fuel` times. Proves only; issues nothing. +pub fn prove_equation( + _law: &AdmittedLaw, + lhs: &str, + rhs: &str, + fuel: usize, +) -> Result { + let program = format!( + "{HEADER}(let lhs {lhs})\n(let rhs {rhs})\n(run assoc {fuel})\n(prove (= lhs rhs))\n" + ); + EGraph::new_with_proofs() + .parse_and_run_program(None, &program) + .map_err(|e| ProofRefusal::NotProved(e.to_string()))? + .into_iter() + .find_map(|out| match out { + CommandOutput::ProveExists { + proof_store, + proof_id, + } => Some(proof_store.proof_to_string(proof_id)), + _ => None, + }) + .ok_or_else(|| ProofRefusal::NotProved("no proof returned".to_owned())) +} + +// ── lowering ─────────────────────────────────────────────────────────────── + +/// One compose step over a value stack: leaves are pushed in chain order, +/// `Compose` pops right then left and pushes their composition. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Step { + Push(usize), + Compose, +} + +pub fn lower(order: &RelExpr) -> Vec { + match order { + RelExpr::Leaf(i) => vec![Step::Push(*i)], + RelExpr::Comp(a, b) => { + let mut v = lower(a); + v.extend(lower(b)); + v.push(Step::Compose); + v + } + } +} + +/// The order a step list computes, or `None` if it is malformed. +pub fn raise(steps: &[Step]) -> Option { + let mut stack = Vec::new(); + for s in steps { + match *s { + Step::Push(i) => stack.push(RelExpr::Leaf(i)), + Step::Compose => { + let b = stack.pop()?; + let a = stack.pop()?; + stack.push(RelExpr::comp(a, b)); + } + } + } + if stack.len() == 1 { stack.pop() } else { None } +} + +/// SHA-256 over a canonical encoding of a step list: a domain tag, then per +/// step `0x00` + the leaf index as `u64` little-endian, or `0x01` for +/// `Compose`. This is the compiled identity a reassociation certificate is +/// bound to; the artifact is the step list, evaluated by the compose kernel. +pub fn lowering_digest(steps: &[Step]) -> [u8; 32] { + let mut h = Sha256::new(); + h.update(b"dr-math-binding-probe/lowering/v1"); + for s in steps { + match *s { + Step::Push(i) => { + h.update([0u8]); + h.update((i as u64).to_le_bytes()); + } + Step::Compose => h.update([1u8]), + } + } + h.finalize().into() +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum LoweringRefusal { + /// The steps do not raise back to the order they were lowered from. + NotRoundTrip, +} + +/// Structural lowering check for one order. +pub fn validate_lowering(order: &RelExpr, steps: &[Step]) -> Result<(), LoweringRefusal> { + if raise(steps).as_ref() != Some(order) { + return Err(LoweringRefusal::NotRoundTrip); + } + Ok(()) +} + +// ── certificate ──────────────────────────────────────────────────────────── + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum CertifyRefusal { + /// The law reference names a different shape than the admitted law. + LawNotAdmitted, + Proof(ProofRefusal), + Lowering(LoweringRefusal), + MissingCodeIdentity, + /// The compiled digest is not the digest of `to`'s checked lowering. + CompiledMismatch, +} + +/// Certify the recipe "evaluate `from` as `to`": the law is admitted for the +/// reference's shape, egglog proves `from = to` from the admitted rule, `to` +/// lowers and raises back to itself, and `compiled.compiled_digest` is the +/// [`lowering_digest`] of that checked lowering. A caller cannot attach a +/// digest of anything else. +pub fn certify_reassociation( + admitted: &AdmittedLaw, + law: LawReference, + from: &RelExpr, + to: &RelExpr, + compiled: CompiledReference, +) -> Result { + if law.shape != admitted.shape || compiled.law != law { + return Err(CertifyRefusal::LawNotAdmitted); + } + let proof = prove_reassociation(admitted, from, to).map_err(CertifyRefusal::Proof)?; + let steps = lower(to); + validate_lowering(to, &steps).map_err(CertifyRefusal::Lowering)?; + if compiled.compiler_revision == 0 || compiled.compiled_digest == [0u8; 32] { + return Err(CertifyRefusal::MissingCodeIdentity); + } + if compiled.compiled_digest != lowering_digest(&steps) { + return Err(CertifyRefusal::CompiledMismatch); + } + Ok(RecipeCertificate::issue(law, compiled, proof)) +} diff --git a/crates/dr-math-binding-probe/tests/relcomp.rs b/crates/dr-math-binding-probe/tests/relcomp.rs new file mode 100644 index 000000000..49dfdfc4c --- /dev/null +++ b/crates/dr-math-binding-probe/tests/relcomp.rs @@ -0,0 +1,382 @@ +//! D-DRMC-5: associativity of Boolean relation composition. +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Scope, Truth, bind_dr64, + recipe::{Backend, CompiledReference, LawReference, LawShape, Primitive}, + relcomp::{ + CertifyRefusal, Chain, ComposeRefusal, LawRefusal, ProofRefusal, RelExpr, Rows, Step, Work, + admit_composition_assoc, all_orders, certify_reassociation, compose, lower, + lowering_digest, prove_equation, prove_reassociation, raise, validate_lowering, + }, +}; + +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; + +/// Five distinct domains, so every adjacent pair in a chain is typed. +fn axis(i: u16) -> Axis { + let kind = [ + AxisKind::Identity, + AxisKind::Property, + AxisKind::Community, + AxisKind::Capability, + AxisKind::Identity, + AxisKind::Property, + ][i as usize]; + Axis { + class: 10 + i, + kind, + } +} +fn method(i: u16) -> MethodSignature { + MethodSignature::presence(10 + i, i, axis(i), axis(i + 1)) +} +fn store() -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: 1, + }) +} +fn bind<'a>(st: &FrameStore, m: MethodSignature, rows: &'a Rows, focus: Focus) -> BoundDr64<'a> { + let at = Guards { + frame: st.seal(), + focus, + scope: SCOPE, + }; + bind_dr64( + st, + m, + m, + &at, + (focus, SCOPE), + Operand { + rows, + validity: None, + }, + ) + .unwrap() +} +/// Deterministic xorshift fill with a density knob (bits kept per 64). +fn fill(seed: u64, keep_of_64: u32) -> Rows { + let mut x = seed | 1; + let mut rows = [0u64; 64]; + for r in rows.iter_mut() { + let mut word = 0u64; + for b in 0..64 { + x ^= x << 13; + x ^= x >> 7; + x ^= x << 17; + if (x % 64) < u64::from(keep_of_64) { + word |= 1 << b; + } + } + *r = word; + } + rows +} +/// Independent oracle: (a∘b)[i][k] iff some j has a[i][j] and b[j][k], +/// enumerated pair by pair, sharing no code with `compose`. +fn oracle(a: &Rows, b: &Rows) -> Rows { + let mut out = [0u64; 64]; + for i in 0..64 { + for k in 0..64 { + let hit = (0..64).any(|j| (a[i] >> j) & 1 == 1 && (b[j] >> k) & 1 == 1); + if hit { + out[i] |= 1 << k; + } + } + } + out +} +fn oracle_eval(ops: &[Rows], order: &RelExpr) -> Rows { + match order { + RelExpr::Leaf(i) => ops[*i], + RelExpr::Comp(a, b) => oracle(&oracle_eval(ops, a), &oracle_eval(ops, b)), + } +} +fn left_deep(n: usize) -> RelExpr { + (1..n).fold(RelExpr::Leaf(0), |acc, i| { + RelExpr::comp(acc, RelExpr::Leaf(i)) + }) +} +fn right_deep(n: usize) -> RelExpr { + (0..n - 1).rev().fold(RelExpr::Leaf(n - 1), |acc, i| { + RelExpr::comp(RelExpr::Leaf(i), acc) + }) +} +fn shape() -> LawShape { + LawShape::for_method(method(0), Primitive::BooleanCompose) +} +fn law() -> LawReference { + LawReference { + id: 7, + revision: 1, + shape: shape(), + } +} +/// The compiled reference for evaluating `to`: its digest is the digest of +/// `to`'s lowering, the only digest a certificate accepts. +fn compiled(to: &RelExpr) -> CompiledReference { + CompiledReference { + law: law(), + compiled_digest: lowering_digest(&lower(to)), + compiler_revision: 1, + target_abi: 1, + backend: Backend::ResidentDr64Simd, + } +} + +#[test] +fn the_kernel_matches_pair_enumeration() { + for (seed, density) in [(1, 3), (2, 8), (3, 32), (4, 63), (5, 0)] { + let (a, b) = (fill(seed, density), fill(seed * 31 + 7, density)); + let mut w = Work::default(); + assert_eq!(compose(&a, &b, &mut w), oracle(&a, &b), "seed {seed}"); + assert_eq!( + w.row_ors, + a.iter().map(|r| u64::from(r.count_ones())).sum::() + ); + } + // Anti-vacuity: the fixtures are neither empty nor full after composing. + let c = oracle(&fill(1, 3), &fill(38, 3)); + assert!(c.iter().any(|r| *r != 0) && c.iter().any(|r| *r != u64::MAX)); +} + +/// Every association order of a 4- and a 5-chain computes the oracle's +/// relation, and the fixtures make the orders differ in work. +#[test] +fn every_order_computes_the_same_relation() { + let st = store(); + for n in [4usize, 5] { + let ops: Vec = (0..n as u64) + .map(|i| fill(i + 11, 2 + 6 * i as u32)) + .collect(); + let bound = ops + .iter() + .enumerate() + .map(|(i, r)| bind(&st, method(i as u16), r, FOCUS)) + .collect(); + let chain = Chain::new(&st, bound).unwrap(); + let orders = all_orders(n); + assert_eq!(orders.len(), if n == 4 { 5 } else { 14 }); + let expected = oracle_eval(&ops, &left_deep(n)); + assert!(expected.iter().any(|r| *r != 0) && expected.iter().any(|r| *r != u64::MAX)); + let mut works = Vec::new(); + for o in &orders { + let (rows, work) = chain.eval(o).unwrap(); + assert_eq!(rows, expected, "order {o:?}"); + works.push(work.row_ors); + } + let (lo, hi) = (works.iter().min().unwrap(), works.iter().max().unwrap()); + assert!( + lo < hi, + "orders must differ in cost on these fixtures: {works:?}" + ); + } +} + +#[test] +fn a_chain_refuses_mistyped_or_misguarded_operands() { + let mut st = store(); + let r = fill(1, 8); + let ok = |i| bind(&st, method(i), &r, FOCUS); + // Domains: operand 1's row must be operand 0's column. + let skip = bind(&st, method(2), &r, FOCUS); + assert_eq!( + Chain::new(&st, vec![ok(0), skip]).unwrap_err(), + ComposeRefusal::DomainMismatch { at: 0 } + ); + assert_eq!( + Chain::new(&st, vec![]).unwrap_err(), + ComposeRefusal::EmptyChain + ); + let other_focus = bind(&st, method(1), &r, Focus { revision: 9 }); + assert_eq!( + Chain::new(&st, vec![ok(0), other_focus]).unwrap_err(), + ComposeRefusal::DifferentFocus { at: 1 } + ); + let other = store(); + let foreign = bind(&other, method(1), &r, FOCUS); + assert_eq!( + Chain::new(&st, vec![ok(0), foreign]).unwrap_err(), + ComposeRefusal::DifferentFrame { at: 1 } + ); + let (a, b) = (ok(0), ok(1)); + st.advance(FrameRevisions { + source: 2, + relation_map: 1, + coordinates: 1, + }); + assert_eq!( + Chain::new(&st, vec![a, b]).unwrap_err(), + ComposeRefusal::StaleFrame + ); +} + +#[test] +fn a_three_valued_operand_does_not_compose() { + let st = store(); + let (r, v) = (fill(1, 8), [u64::MAX; 64]); + let mut m = method(1); + m.truth = Truth::ThreeValued; + let at = Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + }; + let k3 = bind_dr64( + &st, + m, + m, + &at, + (FOCUS, SCOPE), + Operand { + rows: &r, + validity: Some(&v), + }, + ) + .unwrap(); + assert_eq!( + Chain::new(&st, vec![bind(&st, method(0), &r, FOCUS), k3]).unwrap_err(), + ComposeRefusal::NotBooleanDistinct { at: 1 } + ); +} + +#[test] +fn an_order_over_other_positions_is_refused() { + let st = store(); + let r = fill(1, 8); + let chain = Chain::new( + &st, + vec![ + bind(&st, method(0), &r, FOCUS), + bind(&st, method(1), &r, FOCUS), + ], + ) + .unwrap(); + let swapped = RelExpr::comp(RelExpr::Leaf(1), RelExpr::Leaf(0)); + assert_eq!( + chain.eval(&swapped).unwrap_err(), + ComposeRefusal::NotThisChain + ); +} + +#[test] +fn associativity_is_admitted_only_for_boolean_composition() { + assert!(admit_composition_assoc(shape()).is_ok()); + let mut other = shape(); + other.primitive = Primitive::Selection; + assert_eq!( + admit_composition_assoc(other).unwrap_err(), + LawRefusal::NotComposition + ); + for (truth, population) in [ + ( + Truth::ThreeValued, + dr_math_binding_probe::Population::Distinct, + ), + (Truth::TwoValued, dr_math_binding_probe::Population::Bag), + ] { + let mut s = shape(); + s.truth = truth; + s.population = population; + assert_eq!( + admit_composition_assoc(s).unwrap_err(), + LawRefusal::NotBooleanSemiring + ); + } +} + +#[test] +fn egglog_proves_every_reassociation_of_a_five_chain() { + let law = admit_composition_assoc(shape()).unwrap(); + for to in all_orders(5) { + let proof = prove_reassociation(&law, &left_deep(5), &to).unwrap(); + assert!(!proof.is_empty()); + } +} + +/// Can-it-refuse: commutation is not implied by associativity, so egglog +/// finds no proof even with both terms in the e-graph. +#[test] +fn egglog_refuses_an_equation_the_admitted_rule_does_not_imply() { + let law = admit_composition_assoc(shape()).unwrap(); + let ab = RelExpr::comp(RelExpr::Leaf(0), RelExpr::Leaf(1)); + let ba = RelExpr::comp(RelExpr::Leaf(1), RelExpr::Leaf(0)); + assert!(matches!( + prove_equation(&law, &ab.egglog_term(), &ba.egglog_term(), 4), + Err(ProofRefusal::NotProved(_)) + )); + assert_eq!( + prove_reassociation(&law, &ab, &ba).unwrap_err(), + ProofRefusal::DifferentLeaves + ); +} + +#[test] +fn lowering_round_trips_and_keeps_leaf_order() { + for o in all_orders(5) { + let steps = lower(&o); + assert_eq!(steps.iter().filter(|s| **s == Step::Compose).count(), 4); + assert_eq!(raise(&steps).as_ref(), Some(&o)); + assert!(validate_lowering(&o, &steps).is_ok()); + } + let wrong = lower(&left_deep(4)); + assert!(validate_lowering(&right_deep(4), &wrong).is_err()); + assert_eq!(raise(&[Step::Compose]), None); +} + +#[test] +fn a_reassociation_recipe_gets_a_certificate() { + let law_ok = admit_composition_assoc(shape()).unwrap(); + let to = right_deep(4); + let cert = certify_reassociation(&law_ok, law(), &left_deep(4), &to, compiled(&to)).unwrap(); + assert_eq!(cert.law(), &law()); + assert_eq!( + cert.compiled().compiled_digest, + lowering_digest(&lower(&to)) + ); + assert!(cert.proof().contains("Comp")); +} + +/// The digest binds the certificate to the checked lowering: a nonzero digest +/// of another order, or an arbitrary one, is refused, though the proof and the +/// lowering check both pass. +#[test] +fn a_certificate_is_bound_to_the_checked_lowering() { + let admitted = admit_composition_assoc(shape()).unwrap(); + let (from, to) = (left_deep(4), right_deep(4)); + // Anti-vacuity: the two orders lower to different digests. + assert_ne!(lowering_digest(&lower(&from)), lowering_digest(&lower(&to))); + for digest in [lowering_digest(&lower(&from)), [9; 32]] { + let mut c = compiled(&to); + c.compiled_digest = digest; + assert_eq!( + certify_reassociation(&admitted, law(), &from, &to, c).unwrap_err(), + CertifyRefusal::CompiledMismatch + ); + } + assert!(certify_reassociation(&admitted, law(), &from, &to, compiled(&to)).is_ok()); +} + +#[test] +fn certification_refuses_without_each_ingredient() { + let admitted = admit_composition_assoc(shape()).unwrap(); + // Law reference for another shape than the admitted one. + let mut foreign = law(); + foreign.shape.row_kind = AxisKind::Capability; + let mut c = compiled(&right_deep(3)); + c.law = foreign; + assert!(certify_reassociation(&admitted, foreign, &left_deep(3), &right_deep(3), c).is_err()); + // Not a reassociation: different leaves, no proof. + let swapped = RelExpr::comp(RelExpr::Leaf(1), RelExpr::Leaf(0)); + let two = RelExpr::comp(RelExpr::Leaf(0), RelExpr::Leaf(1)); + assert!(certify_reassociation(&admitted, law(), &two, &swapped, compiled(&swapped)).is_err()); + // No code identity. + let mut no_code = compiled(&right_deep(3)); + no_code.compiled_digest = [0; 32]; + assert!( + certify_reassociation(&admitted, law(), &left_deep(3), &right_deep(3), no_code).is_err() + ); +}