|
| 1 | +# 2026-10-23 — L1 result: a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) |
| 2 | + |
| 3 | +**Status:** MEASURED, lab only (`crates/dr-math-binding-probe`). Pre-registration: |
| 4 | +`2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`. Code: `src/recipe.rs`, `src/relcomp.rs` |
| 5 | +(`execute_certified`, `egglog_calls`), `tests/x8_fresh_frame.rs`. |
| 6 | + |
| 7 | +## Result: the hypothesis held |
| 8 | + |
| 9 | +**Positive case.** |
| 10 | +- Five proposed association orders of one 5-chain were each certified on frame 1. The target was the |
| 11 | + cheapest order by `Work` on frame 1's data. |
| 12 | +- All five certificates executed on independently issued frames 2, at densities 0/64, 4/64, 32/64 and 63/64. |
| 13 | +- egglog delta: 0 on every call. |
| 14 | +- Each result equals both the independent pair-enumeration oracle and `Chain::eval` of the requested order. |
| 15 | + |
| 16 | +**Refusals.** |
| 17 | +- Commutation `r0∘r1 → r1∘r0` was refused at certification (`DifferentLeaves`), so no certificate exists. |
| 18 | +- `execute_certified` refused each of the following, and computed nothing in each case: |
| 19 | + - `WrongTarget` (runtime ABI ≠ certificate ABI); |
| 20 | + - `NotCertifiedQuery` (another order of the same leaves); |
| 21 | + - `NotThisChain` (a 4-chain). |
| 22 | + |
| 23 | +**Silent twin.** Same shape, other data: executed every time and never refused. |
| 24 | + |
| 25 | +## Disable runs (all committed first, every anchor asserted) |
| 26 | + |
| 27 | +| run | patch | turned red | |
| 28 | +|---|---|---| |
| 29 | +| D1 | drop the ABI check | `a_different_runtime_abi_is_refused` (only) | |
| 30 | +| D2 | drop the source-digest check | `an_order_the_certificate_does_not_answer_is_refused` (only) | |
| 31 | +| 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) | |
| 32 | + |
| 33 | +The `NotThisChain` guard has no disable run. One was not pre-registered, so none is claimed. |
| 34 | + |
| 35 | +## Measured (reported, not gates; release, 4 cores, load about 1) |
| 36 | + |
| 37 | +- Cold `certify_reassociation`: **15 696 µs**. |
| 38 | +- Hot `execute_certified`: **2 142 ns/call**. It runs the certified cheaper order. |
| 39 | +- `Chain::eval` of the requested (left-deep) order: 7 216 ns/call. |
| 40 | +- Certificate: 1 284 B (1 012 B proof text, 9 compiled steps). |
| 41 | +- Under D3, 20 000 calls took 297 s. That is the cost of putting the prover on the reuse path. |
| 42 | + |
| 43 | +## What this does not show |
| 44 | + |
| 45 | +**Proof checking.** There is no independent proof checker. The proof text is egglog's own and is stored, |
| 46 | +not re-checked at reuse (S2 is still open). |
| 47 | + |
| 48 | +**Choice of target.** The cheapest target was picked on frame 1. On frame 2 the stored order may not be |
| 49 | +cheapest. Specialization selection is out of scope. |
| 50 | + |
| 51 | +**Identity.** `source_digest` and `compiled_digest` are SHA-256 over the lowered program. They identify |
| 52 | +the query and the artifact, not the proof. The law reference stays a separate field. The passive proof |
| 53 | +reference (option B, joint with CC1) is not designed here. |
| 54 | + |
| 55 | +**Coverage.** Thought-Git linkage, R2IL/Quack lowering and a second law are not covered. |
| 56 | + |
| 57 | +`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)` |
0 commit comments