This module contains the verification of the bitblaster for predicates over BitVec expressions (BVPred) from Impl.Pred.

theorem Std.Tactic.BVDecide.BVPred.bitblast_aig_IsPrefix (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Sat.AIG.IsPrefix aig.decls (bitblast aig input).result.val.aig.decls

theorem Std.Tactic.BVDecide.BVPred.bitblast_denote_mem_prefix {inv : Bool} (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) (assign : BVExpr.Assignment) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVPred.bitblast_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : BVExpr.Assignment} (input : BVExpr.WithCache BVPred aig) (hinv : BVExpr.Cache.Inv assign aig input.cache) : BVExpr.Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache

theorem Std.Tactic.BVDecide.BVPred.denote_bitblast (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) (assign : BVExpr.Assignment) (hinv : BVExpr.Cache.Inv assign aig input.cache) : ⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := (bitblast aig input).result.val.ref }⟧ = eval assign input.val