proposition: Lemma randomPerm_unroll_preserves_wf : forall ls d ls' r, well_formed_Bvector_perm ls -> In (ls', r) (getSupport (randomPerm_unroll (ls, d))) -> well_formed_Bvector_perm ls'.
proof: Proof. intuition. unfold randomPerm_unroll in *. case_eq (ls#d); intuition. rewrite H1 in H0. simpl in *. intuition. inversion H2; clear H2; subst. trivial. rewrite H1 in H0. apply getSupport_Bind_In in H0. destruct H0. intuition. apply getSupport_Bind_In in H2. destruct H2. intuition. simpl in H3. intuition. inversion H0; clear H0; subst. case_eq (inRange _ ls x0); intuition; rewrite H0 in H4. simpl in *. apply filter_In in H4. intuition. eapply well_formed_perm_cons; eauto. destruct (inRange _ ls r); intuition. simpl in *. intuition. subst. eapply well_formed_perm_cons; eauto. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF