This module contains the verification of the BitVec expressions (BVExpr) bitblaster from Impl.Expr.

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_val_eq_bitblast {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) : (go aig expr).val = bitblast aig expr

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_mem_prefix {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (go aig expr).val.aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (go aig expr).val.aig, ref := (go aig expr).val.vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.denote_bitblast {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (bitblast aig expr).aig, ref := (bitblast aig expr).vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx