diff --git a/.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md b/.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md new file mode 100644 index 000000000..990ef7b47 --- /dev/null +++ b/.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. 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 new file mode 100644 index 000000000..0d0e16c4f --- /dev/null +++ b/.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)` diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 9cdb7763f..ba24af1b3 100644 --- a/.claude/board/entries/README.md +++ b/.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) | diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index 612a51eb1..392e29ec1 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/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, 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, + 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 diff --git a/crates/dr-math-binding-probe/src/relcomp.rs b/crates/dr-math-binding-probe/src/relcomp.rs index cead68a12..5752099b0 100644 --- a/crates/dr-math-binding-probe/src/relcomp.rs +++ b/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 = 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 { + 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::>() { + 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 = 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 + } } diff --git a/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs b/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs new file mode 100644 index 000000000..1107ec061 --- /dev/null +++ b/crates/dr-math-binding-probe/tests/x8_fresh_frame.rs @@ -0,0 +1,302 @@ +//! L1 (CC2 Law Frontier): a D-DRMC-5 reassociation certificate, issued on one +//! frame, executed on a second, independently issued frame without egglog. +//! Pre-registered in `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`. +use std::hint::black_box; +use std::time::Instant; + +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Scope, bind_dr64, + recipe::{Backend, CompiledReference, LawReference, LawShape, Primitive, RecipeCertificate}, + relcomp::{ + CertifyRefusal, Chain, ProofRefusal, RelExpr, ReuseRefusal, Rows, admit_composition_assoc, + all_orders, certify_reassociation, egglog_calls, execute_certified, lower, lowering_digest, + }, +}; + +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; +const ABI: u32 = 1; + +fn axis(i: u16) -> Axis { + let kind = [ + AxisKind::Identity, + AxisKind::Property, + AxisKind::Community, + AxisKind::Capability, + AxisKind::Identity, + AxisKind::Property, + ][i as usize]; + Axis { + class: 10 + i, + kind, + } +} +fn method(i: u16) -> MethodSignature { + MethodSignature::presence(10 + i, i, axis(i), axis(i + 1)) +} +/// A store at the given revisions. Two stores never share an issue, even at +/// equal revisions, so each call is an independently issued frame. +fn store(source: u64) -> FrameStore { + FrameStore::new(FrameRevisions { + source, + relation_map: 1, + coordinates: 1, + }) +} +fn bind<'a>(st: &FrameStore, m: MethodSignature, rows: &'a Rows) -> BoundDr64<'a> { + let at = Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + }; + bind_dr64( + st, + m, + m, + &at, + (FOCUS, SCOPE), + Operand { + rows, + validity: None, + }, + ) + .unwrap() +} +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() { + let mut word = 0u64; + for b in 0..64 { + x ^= x << 13; + x ^= x >> 7; + x ^= x << 17; + if (x % 64) < u64::from(keep_of_64) { + word |= 1 << b; + } + } + *r = word; + } + rows +} +/// Independent oracle, sharing no code with the compose kernel. +fn oracle(a: &Rows, b: &Rows) -> Rows { + let mut out = [0u64; 64]; + for i in 0..64 { + for k in 0..64 { + if (0..64).any(|j| (a[i] >> j) & 1 == 1 && (b[j] >> k) & 1 == 1) { + out[i] |= 1 << k; + } + } + } + out +} +fn oracle_eval(ops: &[Rows], order: &RelExpr) -> Rows { + match order { + RelExpr::Leaf(i) => ops[*i], + RelExpr::Comp(a, b) => oracle(&oracle_eval(ops, a), &oracle_eval(ops, b)), + } +} +fn data(seed: u64, density: u32, n: usize) -> Vec { + (0..n as u64) + .map(|i| fill(seed * 1009 + i * 31 + 7, density)) + .collect() +} +fn chain<'a>(st: &'a FrameStore, ops: &'a [Rows]) -> Chain<'a> { + let bound = ops + .iter() + .enumerate() + .map(|(i, r)| bind(st, method(i as u16), r)) + .collect(); + Chain::new(st, bound).unwrap() +} +fn law() -> LawReference { + LawReference { + id: 7, + revision: 1, + shape: LawShape::for_method(method(0), Primitive::BooleanCompose), + } +} +fn compiled(to: &RelExpr) -> CompiledReference { + CompiledReference { + law: law(), + compiled_digest: lowering_digest(&lower(to)), + compiler_revision: 1, + target_abi: ABI, + backend: Backend::ResidentDr64Simd, + } +} +fn l(i: usize) -> RelExpr { + RelExpr::Leaf(i) +} +fn c(a: RelExpr, b: RelExpr) -> RelExpr { + RelExpr::comp(a, b) +} +/// Five lanes, five proposed association orders of one 5-chain. +fn proposals() -> Vec { + vec![ + c(c(c(c(l(0), l(1)), l(2)), l(3)), l(4)), // left-deep + c(l(0), c(l(1), c(l(2), c(l(3), l(4))))), // right-deep + c(c(l(0), l(1)), c(l(2), c(l(3), l(4)))), + c(c(c(l(0), l(1)), l(2)), c(l(3), l(4))), + c(l(0), c(c(l(1), l(2)), c(l(3), l(4)))), + ] +} + +/// Frame 1: certify every proposal against the cheapest order by measured +/// work on frame 1's data. Returns (from, certificate) pairs. +fn certify_on_frame_one() -> Vec<(RelExpr, RecipeCertificate)> { + let st1 = store(1); + let ops1 = data(1, 8, 5); + let ch1 = chain(&st1, &ops1); + let to = all_orders(5) + .into_iter() + .min_by_key(|o| ch1.eval(o).unwrap().1) + .unwrap(); + let admitted = admit_composition_assoc(law().shape).unwrap(); + proposals() + .into_iter() + .map(|from| { + let cert = certify_reassociation(&admitted, law(), &from, &to, compiled(&to)).unwrap(); + (from, cert) + }) + .collect() +} + +/// Positive + silent twin: frame 2 is another store with other data. Every +/// certificate executes there, calls egglog zero times, and equals the +/// independent oracle and the chain's own evaluation of the requested order. +#[test] +fn a_certificate_from_frame_one_executes_on_a_fresh_frame_without_egglog() { + let certs = certify_on_frame_one(); + for (seed, density) in [(2, 0), (3, 4), (4, 32), (5, 63)] { + let st2 = store(2); + let ops2 = data(seed, density, 5); + let ch2 = chain(&st2, &ops2); + for (from, cert) in &certs { + let before = egglog_calls(); + let (rows, _) = execute_certified(cert, &ch2, from, ABI) + .unwrap_or_else(|e| panic!("silent twin refused: {e:?} (seed {seed})")); + assert_eq!(egglog_calls(), before, "the hit path ran egglog"); + assert_eq!(rows, oracle_eval(&ops2, from), "oracle, seed {seed}"); + assert_eq!(rows, ch2.eval(from).unwrap().0, "chain eval, seed {seed}"); + } + } +} + +/// Anti-vacuity: certification did call egglog, so a zero delta on the hit +/// path is a measurement, not a counter that never moves. +#[test] +fn certification_itself_calls_egglog() { + let before = egglog_calls(); + let _ = certify_on_frame_one(); + assert!(egglog_calls() >= before + 5); +} + +/// The adversarial lane: commutation is not a reassociation. No certificate is +/// issued, so there is nothing to reuse. +#[test] +fn a_commutation_proposal_gets_no_certificate() { + let admitted = admit_composition_assoc(law().shape).unwrap(); + let ab = c(l(0), l(1)); + let ba = c(l(1), l(0)); + assert_eq!( + certify_reassociation(&admitted, law(), &ab, &ba, compiled(&ba)).unwrap_err(), + CertifyRefusal::Proof(ProofRefusal::DifferentLeaves) + ); +} + +#[test] +fn a_different_runtime_abi_is_refused() { + let certs = certify_on_frame_one(); + let st2 = store(2); + let ops2 = data(9, 8, 5); + let ch2 = chain(&st2, &ops2); + let (from, cert) = &certs[0]; + assert_eq!( + execute_certified(cert, &ch2, from, ABI + 1).unwrap_err(), + ReuseRefusal::WrongTarget + ); +} + +/// A certificate answers its own query only: another order of the same chain +/// is refused, though associativity would make the answer equal. +#[test] +fn an_order_the_certificate_does_not_answer_is_refused() { + let certs = certify_on_frame_one(); + let st2 = store(2); + let ops2 = data(9, 8, 5); + let ch2 = chain(&st2, &ops2); + let (from0, cert0) = &certs[0]; + let (from1, _) = &certs[1]; + // Anti-vacuity: the two queries differ. + assert_ne!(from0, from1); + assert_eq!( + execute_certified(cert0, &ch2, from1, ABI).unwrap_err(), + ReuseRefusal::NotCertifiedQuery + ); + assert!(execute_certified(cert0, &ch2, from0, ABI).is_ok()); +} + +/// The certified query names five positions; a four-operand chain on frame 2 +/// is not that chain. +#[test] +fn a_chain_of_another_length_is_refused() { + let certs = certify_on_frame_one(); + let st2 = store(2); + let ops2 = data(9, 8, 4); + let ch4 = chain(&st2, &ops2); + let (from, cert) = &certs[0]; + assert_eq!( + execute_certified(cert, &ch4, from, ABI).unwrap_err(), + ReuseRefusal::NotThisChain + ); +} + +/// Measured, reported, not gated: cold certification in µs, hot execution in +/// ns per call, certificate size. Run with `--release -- --nocapture`. +#[test] +fn report_costs() { + let st1 = store(1); + let ops1 = data(1, 8, 5); + let ch1 = chain(&st1, &ops1); + let to = all_orders(5) + .into_iter() + .min_by_key(|o| ch1.eval(o).unwrap().1) + .unwrap(); + let from = proposals().remove(0); + let admitted = admit_composition_assoc(law().shape).unwrap(); + let t = Instant::now(); + let cert = certify_reassociation(&admitted, law(), &from, &to, compiled(&to)).unwrap(); + let cold_us = t.elapsed().as_secs_f64() * 1e6; + + let st2 = store(2); + let ops2 = data(3, 8, 5); + let ch2 = chain(&st2, &ops2); + let iters = 20_000u32; + let before = egglog_calls(); + let t = Instant::now(); + for _ in 0..iters { + black_box(execute_certified(black_box(&cert), &ch2, &from, ABI).unwrap()); + } + let hot_ns = t.elapsed().as_secs_f64() * 1e9 / f64::from(iters); + assert_eq!(egglog_calls(), before); + let t = Instant::now(); + for _ in 0..iters { + 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::() + + 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() + ); +}