Skip to main content

prove_bounded_equivalence

logicaffeine_compile::codegen_sva::hw_pipeline

Function prove_bounded_equivalence 

Source 
pub fn prove_bounded_equivalence(
    fol_bounded: &BoundedExpr,
    sva_bounded: &BoundedExpr,
    bound: u32,
) -> Result<EquivalenceResult, HwError>
Expand description

Check FOL ↔ SVA semantic equivalence at a bound with our pure-Rust, certified prover (no Z3) — the in-browser counterpart of check_z3_equivalence. Lowers both bounded obligations to ProofExpr and discharges F ↔ S through the CDCL → RUP tiers: an equivalent verdict is RUP-certified, a non-equivalent one carries a counterexample trace (name@t → "1"/"0"). Errors (fail-closed, never a false “equivalent”) if either obligation leaves the Boolean fragment — data-path needs bit-blasting, not wired yet.