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