Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul

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