fact: Definition randomPerm_unroll(p : (list (Bvector n * Bvector n)) * Bvector n) : Comp (list (Bvector n * Bvector n) * Bvector n) := let (f, d) := p in match f#d with | None => (r <-$ (r0 <-$ {0, 1}^n; if (negb (inRange _ f r0)) then ret r0 else getUnusedBvector f) ; ret ((d, r) :: f, r)) | Some r => ret (f, r) end.
imports: Crypto Permutation Broken.ConstructedFunc State FCF