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

@[irreducible]

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastMul {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (lhs : BitVec w) (rhs : BitVec w) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (input : aig.BinaryRefVec w) (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) (idx : Nat) (hidx : idx < w) : ⟦assign.toAIGAssignment, { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig input).aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig input).vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx