Documentation

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

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