This module contains the verification of the bitblaster for BitVec.mul from Impl.Operations.Mul.

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go_denote_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (hcurr : curr + 1 ≤ w) (acc lhs rhs : aig.RefVec w) (lexpr rexpr : BitVec w) (assign : α → Bool) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lexpr.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rexpr.getLsbD idx) (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lexpr.mulRec rexpr curr).getLsbD idx) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (go aig lhs rhs (curr + 1) acc).aig, ref := (go aig lhs rhs (curr + 1) acc).vec.get idx hidx }⟧ = (lexpr.mulRec rexpr w).getLsbD idx

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.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_blastMul {α : 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 := (blastMul aig input).aig, ref := (blastMul aig input).vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx