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 ≤ idx → ⟦assign, { 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