proposition: Lemma randomPerm_eq_unroll : forall s d x, well_formed_Bvector_perm s -> evalDist (randomPerm_Bvector (s, d)) x == evalDist (randomPerm_unroll (s, d)) x.
proof: Proof. intuition. unfold randomPerm_Bvector, randomPerm, randomPerm_unroll. case_eq (s#d); intuition. unfold getUnusedR. comp_skip. eapply repeat_unroll_eq; wftac. eapply well_formed_perm_1 in H; eauto. destruct H. exists x0. eapply filter_In; intuition. destruct (inRange _ s x0); intuition. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF