lab(drmc): certificate keeps egglog's ProofStore + ProofId, not its rendering; L1 board records

.claude/board/LATEST_STATE.md

@@ -1,3 +1,8 @@
+## 2026-10-23 — main after #1741 (merged `59538865`)
+
+- **On main since #1725:** L1 for D-DRMC-5 (#1740): a reassociation certificate executes on a fresh frame without egglog. The Julia e-graphs coresearch map (#1741). #1726–#1739 have no per-PR records yet.
+- **Contract inventory delta:** none; lab crates and board only.
+
 ## 2026-10-23 — main after #1725 (merged `b342d47c`)
 
 - **On main since #1682:** the D-QR plan family (#1660–#1663), D-QSP/D-RFT/D-LFA plans and probes (#1667–#1688), the math-foundry / egglog-r2il arc (#1690–#1699, #1705, #1717), the D-DRMC charter and probes (#1700, #1707, #1708), the Ascent BYODS plan (#1706), the Palette256 evidence and plasticity probes (#1709–#1722), and the decision-side probes P-D4, P-E2, P-D3 with the P-D4 correction (#1723–#1725). Per-PR records: `PR_ARC_INVENTORY.md` catch-up entries.

.claude/board/PR_ARC_INVENTORY.md

@@ -1,5 +1,20 @@
 <!-- 2026-10-23 catch-up: #1660–#1725 had no entries. One compact entry per PR, recorded from the merge commit. Board-hygiene-only PRs (#1664, #1665, #1672, #1678, #1683) get none, per the CLAUDE.md termination clause. -->
 
+## 2026-10-23 — lance-graph PR #1741 (merged `59538865`, branch `board/coresearch-julia-egraphs-20261023`, head `dcef8cc1`) — board: coresearch map, Julia e-graphs vs egglog/datafrog/Ascent; Lisp vs Prolog for MeTTa
+
+- **Added:** board only.
+- **Docs:** entry `2026-10-23-coresearch-julia-egraphs.md`. Probes P-J1..P-J4 named, none authorized.
+- **Confidence:** recorded from the merge commit.
+
+## 2026-10-23 — lance-graph PR #1740 (merged `c42140b7`, branch `lab/drmc-l1-x8-fresh-frame-20261023`, head `95b2cb18`) — lab: L1, a D-DRMC-5 certificate executes on a fresh frame without egglog
+
+- **Added:** `crates/dr-math-binding-probe` (`RecipeCertificate::{source_digest, program}`, `relcomp::{execute_certified, egglog_calls, ReuseRefusal}`, `tests/x8_fresh_frame.rs`).
+- **Locked:** a certificate answers its own query only; another order, another ABI or another chain length is refused. D1-D3 disable runs each turned their named test red.
+- **Deferred:** the certificate held egglog's proof as a rendered string; replaced by egglog's `ProofStore` + `ProofId` in the follow-up PR.
+- **Docs:** entries `2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`, `…-result.md`.
+- **Confidence:** MEASURED (lab).
+
+
 ## 2026-10-23 — lance-graph PR #1725 (merged `b342d47c`, branch `lab/pd4-refit-base-rate-20261022`, head `57fbec40`) — probe(P-D4): refit the base rate inside each bootstrap draw; the post-hoc gate does not pass
 
 - **Added:** `crates/causal-edge`.

.claude/board/STATUS_BOARD.md

@@ -1,3 +1,12 @@
+## D-DRMC — DR × math binding probe, law frontier (2026-10-23)
+
+Lab only (`crates/dr-math-binding-probe`). Charter and probes: #1700, #1707, #1708; L1 in #1740.
+
+| D-id | scope | status | gate / falsifier |
+|---|---|---|---|
+| **EXP-DRMC-L1** | a D-DRMC-5 reassociation certificate issued on one frame executes on an independently issued frame without egglog | MEASURED (#1740 `c42140b7`; `entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md`); certificate holds egglog's `ProofStore` + `ProofId` (follow-up PR) | zero egglog calls on the hit path, equal to an independent oracle at densities 0/4/32/63; wrong ABI, other order, other length refused; D1-D3 red |
+| **EXP-DRMC-L2** | distributivity plus a false ∩ variant | Held (behind the ProofRef agreement with CC1, EXO-50 07-07e) | — |
+
 ## D-RFT / D-QSP — ClassView × Quack semantic substrate (2026-10-21)
 
 Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`, `d-lfa-lance-graph-flow-rubicon-assimilation-v1.md`; merged). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them.

.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md

@@ -55,3 +55,7 @@ reference (option B, joint with CC1) is not designed here.
 **Coverage.** Thought-Git linkage, R2IL/Quack lowering and a second law are not covered.
 
 `L1 | STATUS: measured | OUTCOME: certificate reused on a fresh frame with 0 egglog calls, 3 refusals pinned by disable runs | OPEN: independent checker, option B reference, L2 (distributivity + false ∩ variant)`
+
+## Correction (2026-10-23, follow-up PR)
+
+The 1 284 B certificate size counted egglog's rendered proof (1 012 B) as the proof. The certificate now holds egglog's `ProofStore` + `ProofId`; `report_costs` prints the certificate without the proof (272 B, 9 steps) and the proof as 8 nodes, with the 1 012 B rendering for display only. The arena's heap size is not measured.

crates/dr-math-binding-probe/Cargo.toml

@@ -11,7 +11,9 @@ 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.
+# parse_and_run_program, `prove`, the read-only `egglog::proof` module).
+# egglog checks every proof it returns with its own checker; that check is
+# egglog's, not an independent one.
 egglog = { git = "https://github.com/AdaWorldAPI/egglog", branch = "main" }
 # Compiled identity of a certified lowering (relcomp::lowering_digest).
 sha2 = "0.10"

crates/dr-math-binding-probe/src/recipe.rs

@@ -6,16 +6,19 @@
 //! mathematical shape can potentially be reused across ClassViews.
 //!
 //! Authority is split, and none of it sits here:
-//! - egglog derives equivalences from admitted laws and checks its own proofs;
+//! - egglog derives equivalences from admitted laws and checks its own proofs
+//!   (egglog's checker, not an independent one);
 //! - law admission owns the assumptions a law holds under (a finite-population
 //!   report never admits a law);
 //! - a certified-compiler boundary, after both of those and a lowering check,
 //!   issues a [`RecipeCertificate`];
 //! - Stage B's `ReplayCapsule` is replay and audit evidence for its own E1
 //!   substitution language, not a proof authority for anything else.
 //!
-//! No certified-compiler boundary exists for a Boolean-DR64 law yet, so this
-//! layer checks everything it can and then refuses with `NoCertifiedCompiler`.
+//! This single-operand layer has no certifier for any law shape, so it checks
+//! everything it can and then refuses with `NoCertifiedCompiler`. One law is
+//! certified elsewhere: associativity of Boolean-Distinct composition over a
+//! chain of DR64 operands, by [`crate::relcomp::certify_reassociation`].
 use crate::{AxisKind, BoundDr64, Population, Truth};
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
@@ -80,7 +83,10 @@ pub struct CompiledReference {
 /// use dr_math_binding_probe::recipe::RecipeCertificate;
 /// let forged = RecipeCertificate { law: todo!(), compiled: todo!(), source_digest: [0; 32], program: vec![], proof: todo!() };
 /// ```
-#[derive(Clone, Debug, PartialEq, Eq)]
+///
+/// Not `PartialEq`: egglog's proof arena has no equality, and two proofs of
+/// one equation need not be the same proof.
+#[derive(Clone, Debug)]
 pub struct RecipeCertificate {
     law: LawReference,
     compiled: CompiledReference,
@@ -91,7 +97,8 @@ pub struct RecipeCertificate {
     /// The checked step list `compiled.compiled_digest` names, kept so a
     /// reuse runs the program without searching for it or re-lowering.
     program: Vec<crate::relcomp::Step>,
-    proof: String,
+    /// egglog's proof object, not a rendering or a digest of it.
+    proof: crate::relcomp::EggProof,
 }
 
 impl RecipeCertificate {
@@ -102,7 +109,7 @@ impl RecipeCertificate {
         compiled: CompiledReference,
         source_digest: [u8; 32],
         program: Vec<crate::relcomp::Step>,
-        proof: String,
+        proof: crate::relcomp::EggProof,
     ) -> Self {
         Self {
             law,
@@ -123,8 +130,8 @@ impl RecipeCertificate {
         &self.source_digest
     }
 
-    /// The checked proof the certifier was given (egglog's rendering).
-    pub fn proof(&self) -> &str {
+    /// The proof the certifier was given, as egglog's own object.
+    pub fn proof(&self) -> &crate::relcomp::EggProof {
         &self.proof
     }
 

crates/dr-math-binding-probe/src/relcomp.rs

@@ -13,8 +13,8 @@
 //!    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
+//!    association orders of the same chain are equal, and checks the proof
+//!    with its own checker (not an independent check). 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
@@ -32,6 +32,7 @@
 //! The compose kernel is plain `u64` word arithmetic, no intrinsics.
 use std::cell::Cell;
 
+use egglog::proof::{Justification, ProofId, ProofStore};
 use egglog::{CommandOutput, EGraph};
 use sha2::{Digest, Sha256};
 
@@ -287,14 +288,80 @@ pub enum ProofRefusal {
     NotProved(String),
 }
 
+/// egglog's proof of one equation, kept as egglog's own object: the
+/// hash-consed proof arena and the id of the root proof in it. Never reduced
+/// to a string or a digest; [`EggProof::render`] is for display only.
+///
+/// egglog checks this proof before returning it (its crate-private
+/// `check_proof`, before and after simplification, panicking on failure).
+/// That is egglog's own check, not an independent one.
+#[derive(Clone)]
+pub struct EggProof {
+    store: ProofStore,
+    root: ProofId,
+}
+
+impl EggProof {
+    /// The proof arena. [`ProofStore::get`] reads any node in it.
+    pub fn store(&self) -> &ProofStore {
+        &self.store
+    }
+
+    /// The root proof, an id into [`EggProof::store`].
+    pub fn root(&self) -> ProofId {
+        self.root
+    }
+
+    /// egglog's pretty-printed rendering. For display; not the proof.
+    pub fn render(&self) -> String {
+        self.store.proof_to_string(self.root)
+    }
+
+    /// Distinct proof nodes reachable from the root; a shared sub-proof
+    /// counts once.
+    pub fn node_count(&self) -> usize {
+        let mut seen = std::collections::HashSet::new();
+        let mut todo = vec![self.root];
+        while let Some(id) = todo.pop() {
+            if !seen.insert(id) {
+                continue;
+            }
+            match self.store.get(id).justification() {
+                Justification::Fiat | Justification::Eval => {}
+                Justification::Rule { premise_proofs, .. } => todo.extend(premise_proofs),
+                Justification::MergeFn {
+                    old_proof,
+                    new_proof,
+                    ..
+                } => todo.extend([*old_proof, *new_proof]),
+                Justification::Trans(a, b) => todo.extend([*a, *b]),
+                Justification::Sym(a) => todo.push(*a),
+                Justification::Congr {
+                    proof, child_proof, ..
+                } => todo.extend([*proof, *child_proof]),
+                Justification::ContainerNormalize { proof } => todo.push(*proof),
+            }
+        }
+        seen.len()
+    }
+}
+
+impl std::fmt::Debug for EggProof {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        f.debug_struct("EggProof")
+            .field("root", &format_args!("{}", self.root))
+            .field("nodes", &self.node_count())
+            .finish()
+    }
+}
+
 /// 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.
+/// (both directions). Returns egglog's proof object (see [`EggProof`]).
 pub fn prove_reassociation(
     law: &AdmittedLaw,
     from: &RelExpr,
     to: &RelExpr,
-) -> Result<String, ProofRefusal> {
+) -> Result<EggProof, ProofRefusal> {
     if from.leaves() != to.leaves() {
         return Err(ProofRefusal::DifferentLeaves);
     }
@@ -303,14 +370,18 @@ pub fn prove_reassociation(
     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.
+/// Ask egglog to prove an arbitrary equation between two `Rel` terms, running
+/// it `fuel` times. Proves only; issues nothing.
+///
+/// The `_law` argument gates the call (only an [`AdmittedLaw`] can be passed)
+/// but does not choose the rules: the rewrites are fixed in `HEADER`, the two
+/// directions of associativity, the only law this probe admits.
 pub fn prove_equation(
     _law: &AdmittedLaw,
     lhs: &str,
     rhs: &str,
     fuel: usize,
-) -> Result<String, ProofRefusal> {
+) -> Result<EggProof, ProofRefusal> {
     EGGLOG_CALLS.with(|n| n.set(n.get() + 1));
     let program = format!(
         "{HEADER}(let lhs {lhs})\n(let rhs {rhs})\n(run assoc {fuel})\n(prove (= lhs rhs))\n"
@@ -323,7 +394,10 @@ pub fn prove_equation(
             CommandOutput::ProveExists {
                 proof_store,
                 proof_id,
-            } => Some(proof_store.proof_to_string(proof_id)),
+            } => Some(EggProof {
+                store: proof_store,
+                root: proof_id,
+            }),
             _ => None,
         })
         .ok_or_else(|| ProofRefusal::NotProved("no proof returned".to_owned()))

crates/dr-math-binding-probe/tests/contract_handoff.rs

@@ -1,6 +1,7 @@
 //! D-DRMC-4: cross-layer *contract* fixture, no proof engine or write path.
-//! No certified-compiler boundary exists for DR64 laws, so the recipe offer
-//! refuses with `NoCertifiedCompiler`; ACT-R arbitration runs on the census
+//! The single-operand recipe offer has no certifier for any law shape, so it
+//! refuses with `NoCertifiedCompiler` (the one certified law, reassociation of
+//! a DR64 chain, goes through `relcomp::certify_reassociation`); ACT-R arbitration runs on the census
 //! eligibility alone and never on a proof.
 use dr_math_binding_probe::{
     Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
@@ -134,7 +135,7 @@ fn class_dependency_to_mathematical_offer_to_act_r_proposal_has_no_effect_path()
         (1, 1, 0, 0)
     );
 
-    // Every metadata check passes; no DR64 certificate can be issued.
+    // Every metadata check passes; this single-operand path has no certifier.
     assert_eq!(
         admit_recipe(
             r.clone(),

crates/dr-math-binding-probe/tests/relcomp.rs

@@ -293,10 +293,28 @@ 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());
+        assert!(proof.node_count() > 0);
     }
 }
 
+/// The proof is egglog's object, not a rendering: its node count grows with
+/// the number of rotations, so a trivial equation has a smaller proof than a
+/// full left-deep to right-deep reassociation.
+#[test]
+fn the_proof_object_grows_with_the_reassociation() {
+    let law = admit_composition_assoc(shape()).unwrap();
+    let same = prove_reassociation(&law, &left_deep(5), &left_deep(5)).unwrap();
+    let far = prove_reassociation(&law, &left_deep(5), &right_deep(5)).unwrap();
+    assert!(
+        far.node_count() > same.node_count(),
+        "far {} vs same {}",
+        far.node_count(),
+        same.node_count()
+    );
+    let root = far.store().get(far.root());
+    assert_ne!(root.lhs(), root.rhs());
+}
+
 /// Can-it-refuse: commutation is not implied by associativity, so egglog
 /// finds no proof even with both terms in the e-graph.
 #[test]
@@ -337,7 +355,7 @@ fn a_reassociation_recipe_gets_a_certificate() {
         cert.compiled().compiled_digest,
         lowering_digest(&lower(&to))
     );
-    assert!(cert.proof().contains("Comp"));
+    assert!(cert.proof().render().contains("Comp"));
 }
 
 /// The digest binds the certificate to the checked lowering: a nonzero digest

crates/dr-math-binding-probe/tests/x8_fresh_frame.rs

@@ -287,16 +287,18 @@ fn report_costs() {
         black_box(ch2.eval(black_box(&from)).unwrap());
     }
     let eval_ns = t.elapsed().as_secs_f64() * 1e9 / f64::from(iters);
-    let bytes = cert.proof().len()
-        + std::mem::size_of::<LawReference>()
+    // The proof is egglog's arena, whose heap size is not measured here; the
+    // rest of the certificate is counted in bytes.
+    let bytes = std::mem::size_of::<LawReference>()
         + std::mem::size_of::<CompiledReference>()
         + 32
         + std::mem::size_of_val(cert.program());
     println!(
         "L1 costs (reported, not gates): cold certify {cold_us:.0} us; \
          hot execute_certified {hot_ns:.0} ns/call; plain eval of the requested order {eval_ns:.0} ns/call; \
-         certificate {bytes} B ({} B proof text, {} steps)",
-        cert.proof().len(),
-        cert.program().len()
+         certificate without proof {bytes} B, {} steps; proof {} nodes ({} B rendered, display only)",
+        cert.program().len(),
+        cert.proof().node_count(),
+        cert.proof().render().len()
     );
 }

crates/egglog-r2il-probe/src/lib.rs

@@ -15,7 +15,7 @@
 //!    first under its default AST-size cost, with every non-target variable a
 //!    `Def` priced at 1000 ([`encode::HEADER`]). The answer is the cheapest
 //!    variant that is not the goal's own name. egglog checks every proof it
-//!    returns.
+//!    returns, with its own checker (not an independent check).
 //! 4. [`lower`] turns the term into calls on the EXISTING R2IL scalar
 //!    arithmetic (`INT_MULT` through `FoldDialect`); no new opcode.
 //! 5. [`oracle`] recomputes the answer in `i128` from the original premises,