def BitVec.iunfoldr {w : Nat} {α : Type u_1} (f : Fin w → α → α × Bool) (s : α) : α × BitVec w

Constructs a bitvector by iteratively computing a state for each bit using the function f, starting with the initial state s. At each step, the prior state and the current bit index are passed to f, and it produces a bit along with the next state value. These bits are assembled into the final bitvector.

It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit in v (e.g., getLsb v i = b_i).

The theorem iunfoldr_replace allows uses of BitVec.iunfoldr to be replaced wiht declarative specifications that are easier to reason about.

Equations

• BitVec.iunfoldr f s = Fin.hIterate (fun (i : Nat) => α × BitVec i) (s, BitVec.nil) fun (i : Fin w) (q : α × BitVec ↑i) => (fun (p : α × Bool) => (p.fst, BitVec.cons p.snd q.snd)) (f i q.fst)

theorem BitVec.iunfoldr.fst_eq {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (s : α) (init : s = state 0) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (iunfoldr f s).fst = state w

theorem BitVec.iunfoldr_getLsbD' {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (∀ (i : Fin w), (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd) ∧ (iunfoldr f (state 0)).fst = state w

theorem BitVec.iunfoldr_getLsbD {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w) (ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)) : (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd

theorem BitVec.iunfoldr_replace {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α) (init : state 0 = a) (step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value[↑i])) : iunfoldr f a = (state w, value)

Given a function state that provides the correct state for every potential iteration count and a function that computes these states from the correct initial state, the result of applying BitVec.iunfoldr f to the initial state is the state corresponding to the bitvector's width paired with the bitvector that consists of each computed bit.

This theorem can be used to prove properties of functions that are defined using BitVec.iunfoldr.

theorem BitVec.iunfoldr_replace_snd {w : Nat} {α : Type u_1} {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α) (init : state 0 = a) (step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value[↑i])) : (iunfoldr f a).snd = value