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 : Sat.AIG α) (input : FullAdderInput aig) : ⟦assign, 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 : Sat.AIG α) (input : FullAdderInput aig) : ⟦assign, 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} {inv : Bool} (aig : Sat.AIG α) (input : FullAdderInput aig) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign, { aig := (mkFullAdder aig input).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {assign : α → Bool} {inv : Bool} (aig : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (start : Nat) (hstart : start < aig.decls.size) : ⟦assign, { aig := (go aig lhs rhs curr hcurr cin s).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig lhs rhs curr hcurr cin s).aig.decls.size) : (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 : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : Nat) (hidx : idx < curr) : (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 rhsBit 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 : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (assign : α → Bool) (lhsExpr 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 := (go aig lhs rhs curr hcurr cin s).aig, ref := (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.blastAdd.denote_blast {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (lhs 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 := (blast aig input).aig, ref := (blast aig input).vec.get idx hidx }⟧ = (lhs + rhs).getLsbD idx

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastAdd {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (lhs 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 := (blastAdd aig input).aig, ref := (blastAdd aig input).vec.get idx hidx }⟧ = (lhs + rhs).getLsbD idx