This module contains the verification of the BitVec.getLsb bitblaster from Impl.Operations.Extract.

theorem Std.Tactic.BVDecide.BVPred.denote_getD_eq_getLsbD {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (assign : α → Bool) (x : BitVec w) (xv : aig.RefVec w) (falseRef : aig.Ref) (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx) (hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false) (idx : Nat) : ⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx

@[simp]

theorem Std.Tactic.BVDecide.BVPred.denote_blastGetLsbD {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig) (assign : α → Bool) : ⟦assign, Std.Tactic.BVDecide.BVPred.blastGetLsbD aig target⟧ = if h : target.idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get target.idx h }⟧ else false