This module contains the verification of the BitVec.udiv bitblaster from Impl.Operations.Udiv.
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastShiftConcat
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(target : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w)
(assign : α → Bool)
(idx : Nat)
(hidx : idx < w)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).vec.get idx hidx }⟧ = if idx = 0 then ⟦assign, { aig := aig, ref := target.bit }⟧
else ⟦assign, { aig := aig, ref := target.lhs.get (idx - 1) ⋯ }⟧
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastShiftConcat_eq_shiftConcat
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(target : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w)
(x : BitVec w)
(b : Bool)
(assign : α → Bool)
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = x.getLsbD idx)
(hb : ⟦assign, { aig := aig, ref := target.bit }⟧ = b)
(idx : Nat)
(hidx : idx < w)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).vec.get idx hidx }⟧ = (x.shiftConcat b).getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
{assign : α → Bool}
(aig : Std.Sat.AIG α)
(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)
(start : Nat)
(hstart : start < aig.decls.size)
:
⟦assign,
{
aig :=
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_q
{α : 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)
(wn : Nat)
(wr : Nat)
(q : aig.RefVec w)
(r : aig.RefVec w)
(qbv : BitVec w)
(rbv : BitVec 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 }⟧ = 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.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
ref :=
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get
idx hidx }⟧ = (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_r
{α : 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)
(wn : Nat)
(wr : Nat)
(q : aig.RefVec w)
(r : aig.RefVec w)
(qbv : BitVec w)
(rbv : BitVec 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)
(hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx)
(hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false)
(idx : Nat)
(hidx : idx < w)
:
⟦assign,
{
aig :=
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
ref :=
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r.get
idx hidx }⟧ = (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.getLsbD idx
@[simp]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_wn
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(lhs : BitVec w)
(rhs : BitVec w)
(falseRef : aig.Ref)
(trueRef : aig.Ref)
(n : aig.RefVec w)
(d : aig.RefVec w)
(wn : Nat)
(wr : Nat)
(q : aig.RefVec w)
(r : aig.RefVec w)
(qbv : BitVec w)
(rbv : BitVec w)
:
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn = (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn
@[simp]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_wr
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(lhs : BitVec w)
(rhs : BitVec w)
(falseRef : aig.Ref)
(trueRef : aig.Ref)
(n : aig.RefVec w)
(d : aig.RefVec w)
(wn : Nat)
(wr : Nat)
(q : aig.RefVec w)
(r : aig.RefVec w)
(qbv : BitVec w)
(rbv : BitVec w)
:
(Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr = (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wr
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_go_eq_divRec_q
{α : 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).q.get idx hidx }⟧ = (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.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).q.get idx hidx }⟧ = (lhs / rhs).getLsbD idx
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
{assign : α → Bool}
(aig : Std.Sat.AIG α)
(curr : Nat)
(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)
(start : Nat)
(hstart : start < aig.decls.size)
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr falseRef trueRef n d wn wr q r).aig,
ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastUdiv
{α : 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.blastUdiv aig input).aig,
ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv aig input).vec.get idx hidx }⟧ = (lhs / rhs).getLsbD idx