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 : Sat.AIG α) (target : ShiftConcatInput aig w) (assign : α → Bool) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (blastShiftConcat aig target).aig, ref := (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 : Sat.AIG α) (target : 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 := (blastShiftConcat aig target).aig, ref := (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} {inv : Bool} (aig : Sat.AIG α) (n d q r : aig.RefVec w) (wn wr start : Nat) (hstart : start < aig.decls.size) : ⟦assign, { aig := (blastDivSubtractShift aig n d wn wr q r).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_q {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (assign : α → Bool) (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (qbv 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) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (blastDivSubtractShift aig n d wn wr q r).aig, ref := (blastDivSubtractShift aig 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 : Sat.AIG α) (assign : α → Bool) (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (qbv 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) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (blastDivSubtractShift aig n d wn wr q r).aig, ref := (blastDivSubtractShift aig 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 : Sat.AIG α) (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (qbv rbv : BitVec w) : (blastDivSubtractShift aig 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 : Sat.AIG α) (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (qbv rbv : BitVec w) : (blastDivSubtractShift aig 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 : Sat.AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w) (n d q r : aig.RefVec w) (wn 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) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (go aig curr n d wn wr q r).aig, ref := (go aig curr 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 : Sat.AIG α) (assign : α → Bool) (lhs rhs : BitVec w) (n d q 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) (hzero : 0#w < rhs) (idx : Nat) (hidx : idx < w) : ⟦assign, { aig := (go aig w n d w 0 q r).aig, ref := (go aig w 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} {inv : Bool} (aig : Sat.AIG α) (curr : Nat) (n d q r : aig.RefVec w) (wn wr start : Nat) (hstart : start < aig.decls.size) : ⟦assign, { aig := (go aig curr n d wn wr q r).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastUdiv {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (lhs 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 := (blastUdiv aig input).aig, ref := (blastUdiv aig input).vec.get idx hidx }⟧ = (lhs / rhs).getLsbD idx