Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add

This module contains the verification of the BitVec.add bitblaster from Impl.Operations.Add.

@[simp]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.denote_mkFullAdderOut {α : Type} [Hashable α] [DecidableEq α] (assign : αBool) (aig : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig) :
assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input = (assign, { aig := aig, ref := input.lhs } ^^ assign, { aig := aig, ref := input.rhs } ^^ assign, { aig := aig, ref := input.cin })
@[simp]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry {α : Type} [Hashable α] [DecidableEq α] (assign : αBool) (aig : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig) :
assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry aig input = ((assign, { aig := aig, ref := input.lhs } ^^ assign, { aig := aig, ref := input.rhs }) && assign, { aig := aig, ref := input.cin } || assign, { aig := aig, ref := input.lhs } && assign, { aig := aig, ref := input.rhs })
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} (aig : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig) (start : Nat) (hstart : start < aig.decls.size) :
assign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig input).aig, ref := { gate := start, hgate := } } = assign, { aig := aig, ref := { gate := start, hgate := hstart } }
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {assign : αBool} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (start : Nat) (hstart : start < aig.decls.size) :
assign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig, ref := { gate := start, hgate := } } = assign, { aig := aig, ref := { gate := start, hgate := hstart } }
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig.decls.size) :
(Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx = (s.get idx hidx).cast hfoo
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_get {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (idx : Nat) (hidx : idx < curr) :
(Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx = (s.get idx hidx).cast
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.atLeastTwo_eq_halfAdder (lhsBit : Bool) (rhsBit : Bool) (carry : Bool) :
lhsBit.atLeastTwo rhsBit carry = ((lhsBit ^^ rhsBit) && carry || lhsBit && rhsBit)
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_denote_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (hcurr : curr w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (assign : αBool) (lhsExpr : BitVec w) (rhsExpr : BitVec w) (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 false) (idx : Nat) (hidx1 : idx < w) :
curr idxassign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx hidx1 } = (assign, { aig := aig, ref := lhs.get idx hidx1 } ^^ (assign, { aig := aig, ref := rhs.get idx hidx1 } ^^ BitVec.carry idx lhsExpr rhsExpr false))
theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastAdd {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (lhs : BitVec w) (rhs : BitVec w) (assign : αBool) (input : aig.BinaryRefVec w) (hleft : ∀ (idx : Nat) (hidx : idx < w), assign, { aig := aig, ref := input.lhs.get idx hidx } = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), assign, { aig := aig, ref := input.rhs.get idx hidx } = rhs.getLsbD idx) (idx : Nat) (hidx : idx < w) :
assign, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig input).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig input).vec.get idx hidx } = (lhs + rhs).getLsbD idx