From 7eaaac1b8cf024aa0c2f967bfb04709ab6a75e2f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:16:48 +0000 Subject: [PATCH 1/3] dr-math-binding-probe: certificate keeps egglog's ProofStore + ProofId, not its rendering RecipeCertificate held the proof as egglog's pretty-printed string. It now holds EggProof { store: ProofStore, root: ProofId }, egglog's own hash-consed proof arena, with render() for display only and node_count() over the justification DAG. RecipeCertificate drops PartialEq/Eq (ProofStore has no equality). Comments: egglog's proof check is its own crate-private check_proof, not an independent one; prove_equation's _law gates the call but the rewrites are fixed in HEADER. New test the_proof_object_grows_with_the_reassociation. report_costs now prints the certificate without proof (272 B) and the proof as 8 nodes; the earlier 1 284 B counted the 1 012 B rendering. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/dr-math-binding-probe/Cargo.toml | 4 +- crates/dr-math-binding-probe/src/recipe.rs | 17 ++-- crates/dr-math-binding-probe/src/relcomp.rs | 92 +++++++++++++++++-- crates/dr-math-binding-probe/tests/relcomp.rs | 22 ++++- .../tests/x8_fresh_frame.rs | 12 ++- crates/egglog-r2il-probe/src/lib.rs | 2 +- 6 files changed, 125 insertions(+), 24 deletions(-) diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index 61a36f8bc..daaa6aed8 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/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" diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index 392e29ec1..9721aadb1 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -6,7 +6,8 @@ //! 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, @@ -80,7 +81,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 +95,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, - proof: String, + /// egglog's proof object, not a rendering or a digest of it. + proof: crate::relcomp::EggProof, } impl RecipeCertificate { @@ -102,7 +107,7 @@ impl RecipeCertificate { compiled: CompiledReference, source_digest: [u8; 32], program: Vec, - proof: String, + proof: crate::relcomp::EggProof, ) -> Self { Self { law, @@ -123,8 +128,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 } diff --git a/crates/dr-math-binding-probe/src/relcomp.rs b/crates/dr-math-binding-probe/src/relcomp.rs index 5752099b0..591f229d9 100644 --- a/crates/dr-math-binding-probe/src/relcomp.rs +++ b/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 { +) -> Result { 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 { +) -> Result { 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())) diff --git a/crates/dr-math-binding-probe/tests/relcomp.rs b/crates/dr-math-binding-probe/tests/relcomp.rs index 49dfdfc4c..eeb9e68fc 100644 --- a/crates/dr-math-binding-probe/tests/relcomp.rs +++ b/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 diff --git a/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs b/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs index 1107ec061..30040668b 100644 --- a/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs +++ b/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::() + // 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::() + std::mem::size_of::() + 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() ); } diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs index 5c1e6e699..82e319eb5 100644 --- a/crates/egglog-r2il-probe/src/lib.rs +++ b/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, From 6e140da8ea22195ceed95863b53a1e28e815d334 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:18:04 +0000 Subject: [PATCH 2/3] board: L1 records (#1740, #1741), EXP-DRMC-L1 row, certificate size correction Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .claude/board/LATEST_STATE.md | 5 +++++ .claude/board/PR_ARC_INVENTORY.md | 15 +++++++++++++++ .claude/board/STATUS_BOARD.md | 9 +++++++++ .../2026-10-23-drmc-l1-x8-fresh-frame-result.md | 4 ++++ 4 files changed, 33 insertions(+) diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 802d59aa4..f3f668af4 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.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. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index a6b3d49ef..2d40aff70 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,5 +1,20 @@ +## 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`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 39b1ce932..d75554930 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.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. diff --git a/.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md b/.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md index 0d0e16c4f..13b972684 100644 --- a/.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md +++ b/.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. From c0802ce569b4a489c1654407ae6e83103e29f761 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:34:33 +0000 Subject: [PATCH 3/3] dr-math-binding-probe: correct the stale "no certified DR64 law" comments recipe.rs and tests/contract_handoff.rs said no certified-compiler boundary exists for DR64 laws. The single-operand admit_recipe path still has no certifier, but relcomp::certify_reassociation (#1707) certifies one law: associativity of Boolean-Distinct composition over a DR64 chain. #1738 corrected two other sites; these two remained. Comments only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/dr-math-binding-probe/src/recipe.rs | 6 ++++-- crates/dr-math-binding-probe/tests/contract_handoff.rs | 7 ++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index 9721aadb1..42838dbe4 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -15,8 +15,10 @@ //! - 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)] diff --git a/crates/dr-math-binding-probe/tests/contract_handoff.rs b/crates/dr-math-binding-probe/tests/contract_handoff.rs index ff46aec0e..46d087a18 100644 --- a/crates/dr-math-binding-probe/tests/contract_handoff.rs +++ b/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(),