probe(dr-math): associativity of Boolean relation composition [5/5]

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

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

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" }

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.

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<Rows> = [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)),
+    }
+}

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;

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,