This module contains the verification of the bitblaster for BitVec.clz from
Impl.Operations.Clz. We prove that the accumulator of the go function
at stepn represents the portion of the ite nodes in the AIG constructed for
bits 0 until n.
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_denote_eq
{α : Type}
[Hashable α]
[DecidableEq α]
{curr w : Nat}
(aig : Sat.AIG α)
(acc xc : aig.RefVec w)
(x : BitVec w)
(assign : α → Bool)
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx)
(hacc :
∀ (idx : Nat) (hidx : idx < w),
if curr = 0 then ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (BitVec.ofNat w w).getLsbD idx
else ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (x.clzAuxRec (curr - 1)).getLsbD idx)
(idx : Nat)
(hidx : idx < w)
:
@[simp]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastClz
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(xc : aig.RefVec w)
(x : BitVec w)
(assign : α → Bool)
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx)
(idx : Nat)
(hidx : idx < w)
: