Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Carry

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 : aig.Ref) (origCin : aig.Ref) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (lhsExpr : BitVec w) (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 : BitVec input.w) (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 }