feat(math-foundry): E1 cold proof capsule and replayable R2IL recipe

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<Step>,
+}
+
+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<Self, ReplayRefusal> {
+        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<i64, ReplayRefusal> {
+        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<i64, ReplayRefusal> {
+        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));
+    }
+}

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;

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))
+    );
+}