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.

@[irreducible]

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) : ⟦assign, { aig := (go aig xc curr acc).aig, ref := (go aig xc curr acc).vec.get idx hidx }⟧ = (x.clzAuxRec (w - 1)).getLsbD idx

@[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) : ⟦assign, { aig := (blastClz aig xc).aig, ref := (blastClz aig xc).vec.get idx hidx }⟧ = (x.clzAuxRec (w - 1)).getLsbD idx