This module contains the verification of the overflow detection bitblaster from Impl.Carry.
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_eq_carry
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : 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 }⟧)
:
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit_eq_carry
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Sat.AIG α)
(input : 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)
: