pub fn certify_mapping(
grid: BoundedExpr,
datapath: BoundedExpr,
) -> Option<PlacementCertificate>Expand description
Emit a proof-carrying certificate that the placed grid equals the datapath spec for every bounded
input, by refuting ¬(grid ≡ datapath) and KEEPING the checkable refutation. Fail-closed: returns None
when the equivalence does not actually hold (a wrong mapping earns no certificate) or the obligation
leaves the propositional fragment (bit-blast the datapath first). A returned certificate is guaranteed
recheck-valid by construction — the underlying prover only hands back a
refutation it has already PR/RUP-verified.