This module contains the verification of the BitVec.umod bitblaster from Impl.Operations.Umod.
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.denote_go_eq_divRec_r
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(assign : α → Bool)
(curr : Nat)
(lhs : BitVec w)
(rhs : BitVec w)
(rbv : BitVec w)
(qbv : BitVec w)
(falseRef : aig.Ref)
(trueRef : aig.Ref)
(n : aig.RefVec w)
(d : aig.RefVec w)
(q : aig.RefVec w)
(r : aig.RefVec w)
(wn : Nat)
(wr : Nat)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx)
(hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false)
(htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true)
(idx : Nat)
(hidx : idx < w)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr falseRef trueRef n d wn wr q r).aig,
ref :=
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr falseRef trueRef n d wn wr q r).r.get idx hidx }⟧ = (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.denote_go
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(assign : α → Bool)
(lhs : BitVec w)
(rhs : BitVec w)
(falseRef : aig.Ref)
(trueRef : aig.Ref)
(n : aig.RefVec w)
(d : aig.RefVec w)
(q : aig.RefVec w)
(r : aig.RefVec w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx)
(hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = false)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = false)
(hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false)
(htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true)
(hzero : 0#w < rhs)
(idx : Nat)
(hidx : idx < w)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w falseRef trueRef n d w 0 q r).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig w falseRef trueRef n d w 0 q r).r.get idx hidx }⟧ = (lhs % rhs).getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastUmod
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(lhs : BitVec w)
(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 := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig input).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig input).vec.get idx hidx }⟧ = (lhs % rhs).getLsbD idx