proposition: Lemma randomPerm_unroll_wf : forall ls b0, (forall x, ls#x = None -> exists r, inRange _ ls r = false) -> well_formed_comp (randomPerm_unroll (ls, b0)).
proof: Proof. intuition. unfold randomPerm_unroll. case_eq (ls#b0); intuition; wftac. edestruct H; eauto. eapply getUnusedBvector_wf_h. eauto. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF