dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8)

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

@@ -0,0 +1,92 @@
+# 2026-10-23 — EXP-DRMC-L1-PREREG — L1 (CC2 Law Frontier): a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) — pre-registration
+
+**Status:** PRE-REGISTERED. This entry is committed before any code. Lab only:
+`crates/dr-math-binding-probe`, no production crate touched.
+**Authorization:** operator, 2026-10-23 ("CC2: L1 starten … nur im Lab, keine Produktionsänderungen"), coordinated
+in EXO-50 (`20261023-cc2-dual-frontier-05`, `GPT:gpt-ada-01/20261023-cc1-cc2-ownership-sync-13`).
+
+## Hypothesis
+
+A `RecipeCertificate` that `certify_reassociation` issues on frame F1 can be executed against a chain bound on a
+second, independently issued frame F2 (other `FrameStore`, other data, same law shape). The run calls egglog zero
+times, and its result equals an independent pair-enumeration oracle. Every incompatible request is refused rather
+than silently recomputed.
+
+## What already exists (not rebuilt)
+
+D-DRMC-5 (#1707) supplies:
+- the typed `Chain` (frame, focus, scope and domain guards);
+- `admit_composition_assoc`;
+- the egglog proof;
+- the `lower`/`raise` round trip;
+- `certify_reassociation`, which binds the certificate to `lowering_digest(lower(to))`.
+
+## Additions (minimal, in `dr-math-binding-probe`)
+
+1. **The certificate records which query it answers.** The certificate gains `source_digest` =
+   `lowering_digest(lower(from))`. Today it proves `from = to` but does not record `from`. A reuse could then run
+   `to` for a request that the certificate never covered.
+2. **`execute_certified(cert, chain, requested, runtime_abi)`.** It refuses in three cases:
+   - `WrongTarget` when `cert.compiled().target_abi != runtime_abi`. Today `target_abi` is stored but never
+     checked.
+   - `NotCertifiedQuery` when `lowering_digest(lower(requested)) != source_digest`.
+   - `NotThisChain` when `requested` does not cover the chain's positions.
+
+   Otherwise it executes the certificate's step list (the compiled artifact) on a stack with `compose`. It never
+   calls the prover.
+3. **A thread-local egglog invocation counter.** It is incremented inside `prove_equation`, the only egglog call
+   site, and exposed read-only. The hit path asserts the delta is 0.
+
+## Tests (new file `tests/x8_fresh_frame.rs`)
+
+**Positive.**
+- Five lanes propose five association orders of one 5-chain (left-deep, right-deep, three balanced).
+- Each proposed order is certified on F1 against the cheapest-by-`Work` target.
+- On F2 (new store, new random data at three densities), each certificate executes:
+  - egglog delta = 0;
+  - result == `oracle_eval` of the requested order;
+  - result == `Chain::eval` of the requested order.
+
+**Adversarial.** A lane proposes commutation `r0∘r1 → r1∘r0`. Certification is refused, and no certificate
+exists to reuse.
+
+**Negative (must refuse, never fall back).**
+- `WrongTarget`: runtime ABI ≠ certificate ABI.
+- `NotCertifiedQuery`: a different order with the same leaves.
+- `NotThisChain`: a 4-chain on F2 against a 5-chain certificate.
+- Chain construction refuses on F2 for Bag, three-valued and domain-mismatch operands. That guard lives in
+  `Chain::new` (D-DRMC-5) and is cited, not re-claimed.
+
+**Silent twin.** Same shape, different data, same requested order: it MUST execute and MUST NOT refuse. A refusal
+or a baseline recompute counts as failure, never as reuse.
+
+**Disable runs** (commit first; each patch's anchor asserted before applying):
+- D1: drop the ABI check. The `WrongTarget` test goes red.
+- D2: drop the source-digest check. The `NotCertifiedQuery` test goes red.
+- D3: route execution through `prove_reassociation`. The zero-egglog assertion goes red.
+
+**Measured, reported, not gates.**
+- Cold `certify_reassociation`, in µs.
+- Hot `execute_certified` on a 5-chain, in ns per call.
+- Certificate bytes: proof text length plus fixed references.
+- Units: ns hot, µs cold, never ms.
+
+## Kill conditions
+
+L1 fails if any of the following happens:
+- a requested order the certificate does not cover executes;
+- an ABI mismatch executes;
+- the hit path calls egglog;
+- any F2 result differs from the oracle;
+- the silent twin refuses.
+
+## Out of scope
+
+- Choosing the cheapest order (specialization selection).
+- R2IL/Quack lowering.
+- An independent proof checker (S2).
+- The Thought-Git side. CC1 owns the passive reference; the shared type is to be agreed as option B before any
+  contract PR.
+
+Note from the operator: a compiled-program digest is not the proof's identity. The certificate keeps the law,
+`source_digest`, `compiled_digest` and the proof as distinct fields.

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

@@ -0,0 +1,57 @@
+# 2026-10-23 — EXP-DRMC-L1 — L1 result: a certified reassociation reused on a fresh frame (D-DRMC-5 + X8)
+
+**Status:** MEASURED, lab only (`crates/dr-math-binding-probe`). Pre-registration:
+`2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`. Code: `src/recipe.rs`, `src/relcomp.rs`
+(`execute_certified`, `egglog_calls`), `tests/x8_fresh_frame.rs`.
+
+## Result: the hypothesis held
+
+**Positive case.**
+- Five proposed association orders of one 5-chain were each certified on frame 1. The target was the
+  cheapest order by `Work` on frame 1's data.
+- All five certificates executed on independently issued frames 2, at densities 0/64, 4/64, 32/64 and 63/64.
+- egglog delta: 0 on every call.
+- Each result equals both the independent pair-enumeration oracle and `Chain::eval` of the requested order.
+
+**Refusals.**
+- Commutation `r0∘r1 → r1∘r0` was refused at certification (`DifferentLeaves`), so no certificate exists.
+- `execute_certified` refused each of the following, and computed nothing in each case:
+  - `WrongTarget` (runtime ABI ≠ certificate ABI);
+  - `NotCertifiedQuery` (another order of the same leaves);
+  - `NotThisChain` (a 4-chain).
+
+**Silent twin.** Same shape, other data: executed every time and never refused.
+
+## Disable runs (all committed first, every anchor asserted)
+
+| run | patch | turned red |
+|---|---|---|
+| D1 | drop the ABI check | `a_different_runtime_abi_is_refused` (only) |
+| D2 | drop the source-digest check | `an_order_the_certificate_does_not_answer_is_refused` (only) |
+| D3 | call `prove_reassociation` inside `execute_certified` | `a_certificate_from_frame_one_executes_on_a_fresh_frame_without_egglog` + `report_costs` (both assert the egglog delta) |
+
+The `NotThisChain` guard has no disable run. One was not pre-registered, so none is claimed.
+
+## Measured (reported, not gates; release, 4 cores, load about 1)
+
+- Cold `certify_reassociation`: **15 696 µs**.
+- Hot `execute_certified`: **2 142 ns/call**. It runs the certified cheaper order.
+- `Chain::eval` of the requested (left-deep) order: 7 216 ns/call.
+- Certificate: 1 284 B (1 012 B proof text, 9 compiled steps).
+- Under D3, 20 000 calls took 297 s. That is the cost of putting the prover on the reuse path.
+
+## What this does not show
+
+**Proof checking.** There is no independent proof checker. The proof text is egglog's own and is stored,
+not re-checked at reuse (S2 is still open).
+
+**Choice of target.** The cheapest target was picked on frame 1. On frame 2 the stored order may not be
+cheapest. Specialization selection is out of scope.
+
+**Identity.** `source_digest` and `compiled_digest` are SHA-256 over the lowered program. They identify
+the query and the artifact, not the proof. The law reference stays a separate field. The passive proof
+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)`

.claude/board/entries/README.md

@@ -25,13 +25,15 @@ 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.
 
-449 entries, 2026-08-06 .. 2026-10-23.
+451 entries, 2026-08-06 .. 2026-10-23.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-23 | `ps2-compose-chain-preregistration` |  | [2026-10-23-ps2-compose-chain-preregistration.md](2026-10-23-ps2-compose-chain-preregistration.md) |
 | 2026-10-23 | `ledger-revision-1635-1726` |  | [2026-10-23-ledger-revision-1635-1726.md](2026-10-23-ledger-revision-1635-1726.md) |
 | 2026-10-23 | `exo129-learned-lut-preregistration` |  | [2026-10-23-exo129-learned-lut-preregistration.md](2026-10-23-exo129-learned-lut-preregistration.md) |
+| 2026-10-23 | `EXP-DRMC-L1` | L1 result: a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) | [2026-10-23-drmc-l1-x8-fresh-frame-result.md](2026-10-23-drmc-l1-x8-fresh-frame-result.md) |
+| 2026-10-23 | `EXP-DRMC-L1-PREREG` | L1 (CC2 Law Frontier): a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) — pre-registration | [2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md](2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md) |
 | 2026-10-23 | `D-TGA-5D` |  | [2026-10-23-d-tga-5d-protected-readers-preregistration.md](2026-10-23-d-tga-5d-protected-readers-preregistration.md) |
 | 2026-10-23 | `D-TGA-5` |  | [2026-10-23-d-tga-5-squash-gate-preregistration.md](2026-10-23-d-tga-5-squash-gate-preregistration.md) |
 | 2026-10-23 | `coresearch-thought-git-markov` |  | [2026-10-23-coresearch-thought-git-markov.md](2026-10-23-coresearch-thought-git-markov.md) |

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

@@ -78,26 +78,51 @@ pub struct CompiledReference {
 ///
 /// ```compile_fail
 /// use dr_math_binding_probe::recipe::RecipeCertificate;
-/// let forged = RecipeCertificate { law: todo!(), compiled: todo!(), proof: todo!() };
+/// let forged = RecipeCertificate { law: todo!(), compiled: todo!(), source_digest: [0; 32], program: vec![], proof: todo!() };
 /// ```
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct RecipeCertificate {
     law: LawReference,
     compiled: CompiledReference,
+    /// Digest of the query the proof starts from (`lowering_digest` of the
+    /// `from` order). The certificate answers this query and no other; the
+    /// compiled digest names the program that answers it.
+    source_digest: [u8; 32],
+    /// 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,
 }
 
 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 {
+    pub(crate) fn issue(
+        law: LawReference,
+        compiled: CompiledReference,
+        source_digest: [u8; 32],
+        program: Vec<crate::relcomp::Step>,
+        proof: String,
+    ) -> Self {
         Self {
             law,
             compiled,
+            source_digest,
+            program,
             proof,
         }
     }
 
+    /// The checked step list this certificate's compiled digest names.
+    pub fn program(&self) -> &[crate::relcomp::Step] {
+        &self.program
+    }
+
+    /// Digest of the query this certificate answers.
+    pub fn source_digest(&self) -> &[u8; 32] {
+        &self.source_digest
+    }
+
     /// The checked proof the certifier was given (egglog's rendering).
     pub fn proof(&self) -> &str {
         &self.proof

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

@@ -30,6 +30,8 @@
 //! one is the specialization-selection question, still open (see README).
 //!
 //! The compose kernel is plain `u64` word arithmetic, no intrinsics.
+use std::cell::Cell;
+
 use egglog::{CommandOutput, EGraph};
 use sha2::{Digest, Sha256};
 
@@ -261,6 +263,18 @@ pub fn admit_composition_assoc(shape: LawShape) -> Result<AdmittedLaw, LawRefusa
 
 // ── proof (egglog) ─────────────────────────────────────────────────────────
 
+thread_local! {
+    static EGGLOG_CALLS: Cell<u64> = const { Cell::new(0) };
+}
+
+/// How many times this thread has run egglog through [`prove_equation`], the
+/// only egglog call site in this crate. Lets a test assert that a cached
+/// recipe executes without the prover. Thread-local, so parallel tests do not
+/// see each other's calls.
+pub fn egglog_calls() -> u64 {
+    EGGLOG_CALLS.with(Cell::get)
+}
+
 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";
@@ -297,6 +311,7 @@ pub fn prove_equation(
     rhs: &str,
     fuel: usize,
 ) -> Result<String, 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"
     );
@@ -422,5 +437,73 @@ pub fn certify_reassociation(
     if compiled.compiled_digest != lowering_digest(&steps) {
         return Err(CertifyRefusal::CompiledMismatch);
     }
-    Ok(RecipeCertificate::issue(law, compiled, proof))
+    let source_digest = lowering_digest(&lower(from));
+    Ok(RecipeCertificate::issue(
+        law,
+        compiled,
+        source_digest,
+        steps,
+        proof,
+    ))
+}
+
+// ── reuse on a bound chain (X8) ────────────────────────────────────────────
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum ReuseRefusal {
+    /// The runtime ABI is not the one the certificate was compiled for.
+    WrongTarget,
+    /// The requested order is not the query the certificate answers.
+    NotCertifiedQuery,
+    /// The requested order does not cover this chain's positions in order.
+    NotThisChain,
+    /// The certified program does not run on this chain (malformed steps or a
+    /// leaf outside the chain).
+    ProgramDoesNotFit,
+}
+
+/// Answer `requested` on `chain` with a certified recipe, without proving
+/// anything: check the target, check that `requested` is the query the
+/// certificate answers, then run the certified step list with the compose
+/// kernel. The chain carries its own frame, focus, scope and semiring guards
+/// (checked by [`Chain::new`]); the certificate carries none of them, so the
+/// same certificate serves any chain that passes them.
+///
+/// On any refusal nothing is computed: the caller decides on a baseline.
+pub fn execute_certified(
+    cert: &RecipeCertificate,
+    chain: &Chain<'_>,
+    requested: &RelExpr,
+    runtime_abi: u32,
+) -> Result<(Rows, Work), ReuseRefusal> {
+    if cert.compiled().target_abi != runtime_abi {
+        return Err(ReuseRefusal::WrongTarget);
+    }
+    if lowering_digest(&lower(requested)) != *cert.source_digest() {
+        return Err(ReuseRefusal::NotCertifiedQuery);
+    }
+    if requested.leaves() != (0..chain.len()).collect::<Vec<_>>() {
+        return Err(ReuseRefusal::NotThisChain);
+    }
+    run_steps(chain, cert.program()).ok_or(ReuseRefusal::ProgramDoesNotFit)
+}
+
+fn run_steps(chain: &Chain<'_>, steps: &[Step]) -> Option<(Rows, Work)> {
+    let mut work = Work::default();
+    let mut stack: Vec<Rows> = Vec::new();
+    for s in steps {
+        match *s {
+            Step::Push(i) => stack.push(*chain.operands.get(i)?.rows),
+            Step::Compose => {
+                let b = stack.pop()?;
+                let a = stack.pop()?;
+                stack.push(compose(&a, &b, &mut work));
+            }
+        }
+    }
+    if stack.len() == 1 {
+        stack.pop().map(|r| (r, work))
+    } else {
+        None
+    }
 }