Module sva_to_proof 

Bounded SVA/FOL obligation → ProofExpr (the certified-prover seam).

BoundedExpr is an SVA assertion (or Kripke-lowered FOL spec) already unrolled to discrete timesteps, with each signal-at-time a signal@t variable. This module lowers that bounded obligation into the logicaffeine_proof::ProofExpr vocabulary, where the pure-Rust CDCL → RUP → kernel trust tiers discharge it with a certificate — the very seam the grid solver uses, and the reason hardware proving runs in the browser with no Z3.

Boolean (1-bit signal) obligations lower directly. Data-path operands — integers, bitvectors, arrays, comparisons, quantifiers, uninterpreted applications — return None, signalling that the caller must bit-blast them to the Boolean fragment first (the next layer). Returning None rather than guessing keeps the lowering fail-closed.

Functions

bounded_to_proof

Lower a Boolean-fragment BoundedExpr to ProofExpr, or None for any node outside the propositional fragment (integers, bitvectors, arrays, ordered comparisons, quantifiers, uninterpreted applications) — those require bit-blasting, not direct lowering.