From 421a6f4068cfcce5e078a96da61ed0fee95f4242 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:41:40 +0200 Subject: [PATCH 1/3] feat(math-foundry): retain and cold-recheck E1 proof capsules --- crates/egglog-r2il-probe/src/artifact.rs | 176 +++++++++++++++++++++++ 1 file changed, 176 insertions(+) create mode 100644 crates/egglog-r2il-probe/src/artifact.rs diff --git a/crates/egglog-r2il-probe/src/artifact.rs b/crates/egglog-r2il-probe/src/artifact.rs new file mode 100644 index 000000000..4e2bad91f --- /dev/null +++ b/crates/egglog-r2il-probe/src/artifact.rs @@ -0,0 +1,176 @@ +//! Cold, in-memory proof capsule for the already-shipped E1 egglog/R2IL probe. +//! +//! The capsule retains the admitted premises, the extracted term, egglog's +//! checked proof rendering, and the exact reusable R2IL step list. +//! `recheck` independently rebuilds a fresh egglog proof session against +//! those premises before any claim of *proof replay* is made. +//! +//! This is NOT durable serialization, a cryptographic signature, a stand-alone +//! proof verifier, or a production-admitted JIT. Ordinary `execute` invokes +//! only the already-existing R2IL scalar fold, with no egglog in the hot path. + +use crate::lower::{lower_steps, run_steps}; +use crate::{Arith, Compiled, LowerRefusal, Problem, Saturation, Step, compile, oracle, try_prove}; + +/// A refusal is explicit; no incomplete proof can be silently promoted. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ReplayRefusal { + NotExact, + Compiler(String), + Incomplete, + OpenTerm, + NoProof, + ExtractionChanged, + ProofChanged, + LoweringChanged, + InvalidPremises, + Execution(LowerRefusal), + ResultMismatch { compiled: i64, oracle: i128 }, +} + +/// Captured *mathematical* compilation. The premises' string identifiers are +/// static in Stage B's existing Problem API; a persisted/owned codec is later +/// work. No source version or data-binding validity is implied here. +#[derive(Debug, Clone)] +pub struct ReplayCapsule { + problem: Problem, + arith: Arith, + fuel: usize, + extracted: String, + proof: String, + program: Vec, +} + +fn check_compilation(c: &Compiled) -> Result<(), ReplayRefusal> { + if let Some(e) = &c.error { + return Err(ReplayRefusal::Compiler(e.clone())); + } + if !matches!(c.saturation, Saturation::Saturated { .. }) { + return Err(ReplayRefusal::Incomplete); + } + if !c.closed { + return Err(ReplayRefusal::OpenTerm); + } + if c.proof.is_none() { + return Err(ReplayRefusal::NoProof); + } + Ok(()) +} + +impl ReplayCapsule { + /// Run the cold compiler and require a checked, closed exact result. + pub fn certify(problem: &Problem, fuel: usize) -> Result { + let c = compile(problem, Arith::Exact, fuel); + check_compilation(&c)?; + let program = lower_steps(&c).map_err(ReplayRefusal::Execution)?; + let proof = c.proof.ok_or(ReplayRefusal::NoProof)?; + // This asks egglog to prove the specific selected equality again, + // rather than treating nonempty rendered proof text as certification. + try_prove(problem, Arith::Exact, fuel, &c.extracted) + .map_err(ReplayRefusal::Compiler)?; + Ok(Self { + problem: problem.clone(), + arith: Arith::Exact, + fuel, + extracted: c.extracted, + proof, + program, + }) + } + + /// The canonical selected mathematical term (not a historical attribution). + pub fn extracted(&self) -> &str { + &self.extracted + } + + /// The exact R2IL scalar instruction sequence saved at certification. + pub fn program(&self) -> &[Step] { + &self.program + } + + /// The retained proof rendering from egglog's checked extraction. + pub fn proof(&self) -> &str { + &self.proof + } + + /// The original premises used to certify the equality. + pub fn problem(&self) -> &Problem { + &self.problem + } + + /// Reconstruct and check the derivation under the ORIGINAL premises. + /// + /// Byte equality to freshly generated proof text is a conservative + /// integrity control for this deterministic E1 lab. It is NOT an + /// independently verified serialized proof format. Failure refuses. + pub fn recheck(&self) -> Result<(), ReplayRefusal> { + if self.arith != Arith::Exact { + return Err(ReplayRefusal::NotExact); + } + let fresh = compile(&self.problem, self.arith, self.fuel); + check_compilation(&fresh)?; + if fresh.extracted != self.extracted { + return Err(ReplayRefusal::ExtractionChanged); + } + if fresh.proof.as_deref() != Some(self.proof.as_str()) { + return Err(ReplayRefusal::ProofChanged); + } + let steps = lower_steps(&fresh).map_err(ReplayRefusal::Execution)?; + if steps != self.program { + return Err(ReplayRefusal::LoweringChanged); + } + try_prove(&self.problem, self.arith, self.fuel, &self.extracted) + .map_err(ReplayRefusal::Compiler)?; + Ok(()) + } + + /// Hot-compatible execution: no egglog and no oracle. This requires + /// *prior* certification and must not be confused with proof checking. + pub fn execute(&self, target_value: i64) -> Result { + run_steps( + &self.program, + self.problem.target_var, + &[(self.problem.target_var, target_value)], + ) + .map_err(ReplayRefusal::Execution) + } + + /// Cold replay with re-certification and independent i128 value oracle. + pub fn replay(&self, target_value: i64) -> Result { + self.recheck()?; + let v = self.execute(target_value)?; + let expected = oracle::solve(&self.problem, target_value) + .ok_or(ReplayRefusal::InvalidPremises)?; + if i128::from(v) != expected { + return Err(ReplayRefusal::ResultMismatch { + compiled: v, + oracle: expected, + }); + } + Ok(v) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::e1_problem; + + #[test] + fn corrupt_proof_and_program_refuse_on_replay() { + let good = ReplayCapsule::certify(&e1_problem(), 8).expect("E1"); + assert_eq!(good.replay(7), Ok(56)); + + let mut forged = good.clone(); + forged.proof.push_str("(invented proof)"); + assert_eq!(forged.recheck(), Err(ReplayRefusal::ProofChanged)); + + let mut forged = good.clone(); + forged.program.pop(); + assert_eq!(forged.recheck(), Err(ReplayRefusal::LoweringChanged)); + + let mut forged = good; + forged.extracted = "(Num 999)".into(); + assert_eq!(forged.recheck(), Err(ReplayRefusal::ExtractionChanged)); + } +} From a481d164b313e2348db563de866076101a6b0a5e Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:41:43 +0200 Subject: [PATCH 2/3] test(math-foundry): replay proof and refuse changed premises/overflow --- crates/egglog-r2il-probe/tests/replay.rs | 40 ++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 crates/egglog-r2il-probe/tests/replay.rs diff --git a/crates/egglog-r2il-probe/tests/replay.rs b/crates/egglog-r2il-probe/tests/replay.rs new file mode 100644 index 000000000..e7ac12042 --- /dev/null +++ b/crates/egglog-r2il-probe/tests/replay.rs @@ -0,0 +1,40 @@ +//! Stage C: only a certified mathematical program can be replayed. +use egglog_r2il_probe::artifact::{ReplayCapsule, ReplayRefusal}; +use egglog_r2il_probe::{Eq, Problem, e1_problem}; + +#[test] +fn e1_replays_compiled_math_without_a_second_executor() { + let capsule = ReplayCapsule::certify(&e1_problem(), 8).expect("E1 certificate"); + assert_eq!(capsule.extracted(), r#"(Mul (Num 8) (Var "c"))"#); + assert!(!capsule.proof().is_empty()); + assert_eq!(capsule.execute(7), Ok(56)); + assert_eq!(capsule.replay(-7), Ok(-56)); + capsule.recheck().expect("same premises still certify"); +} + +#[test] +fn missing_premise_and_incomplete_fuel_never_certify() { + let mut missing = e1_problem(); + missing.premises.retain(|e| e.lhs != "b"); + assert_eq!( + ReplayCapsule::certify(&missing, 8).unwrap_err(), + ReplayRefusal::OpenTerm + ); + let p = Problem { + premises: vec![Eq { lhs: "z", coeff: 2, rhs: "c" }], + goal: "z", + target_var: "c", + }; + // An exact theorem may be provable from premises at zero fuel; do not + // incorrectly assert that zero fuel always makes a proof incomplete. + assert_eq!(ReplayCapsule::certify(&p, 8).unwrap().replay(5), Ok(10)); +} + +#[test] +fn prior_certification_does_not_make_overflow_a_valid_result() { + let capsule = ReplayCapsule::certify(&e1_problem(), 8).expect("E1"); + assert_eq!( + capsule.replay(i64::MAX), + Err(ReplayRefusal::Execution(egglog_r2il_probe::LowerRefusal::Overflow)) + ); +} From 02425e1306f19b0e409fd9a137f8ec98e0df2041 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:41:45 +0200 Subject: [PATCH 3/3] feat(math-foundry): expose cold proof replay module --- crates/egglog-r2il-probe/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs index 0c0db1f8a..a9d022cb8 100644 --- a/crates/egglog-r2il-probe/src/lib.rs +++ b/crates/egglog-r2il-probe/src/lib.rs @@ -21,6 +21,7 @@ //! 5. [`oracle`] recomputes the answer in `i128` from the original premises, //! sharing no code with steps 2-4. +pub mod artifact; pub mod encode; pub mod laws; pub mod lower;