fact: Definition randomPerm(p : (list (D * R) * D)) : Comp (list (D * R) * R) := let (f, d) := p in match (f#d) with | None => (r <-$ getUnusedR f ; ret ((d, r) :: f, r)) | Some r => ret (f, r) end.
imports: Crypto Permutation CompFold Array FCF State