This module contains the verification of the overflow detection bitblaster from Impl.Carry.

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_eq_carry {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin origCin : aig.Ref) (lhs rhs : aig.RefVec w) (lhsExpr rhsExpr : BitVec w) (assign : α → Bool) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lhsExpr.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rhsExpr.getLsbD idx) (hcin : ⟦assign, { aig := aig, ref := cin }⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦assign, { aig := aig, ref := origCin }⟧) : ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin⟧ = BitVec.carry w lhsExpr rhsExpr ⟦assign, { aig := aig, ref := origCin }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit_eq_carry {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig) (lhs rhs : BitVec input.w) (assign : α → Bool) (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx) : ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit aig input⟧ = BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧