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 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) : (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val = Std.Tactic.BVDecide.BVExpr.bitblast aig expr

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_mem_prefix {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign.toAIGAssignment, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.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 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.vec.get idx hidx }⟧ = (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx

@[simp]

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