proposition: Lemma randomPerm_bad_preserves_wf : forall ls d ls' r, well_formed_Bvector_perm ls -> In (ls', r) (getSupport (randomPerm_bad (ls, d))) -> well_formed_Bvector_perm ls'.
proof: Proof. intuition. unfold randomPerm_bad in *. case_eq (ls#d); intuition; rewrite H1 in H0. simp_in_support. trivial. simp_in_support. case_eq (inRange _ ls x); intuition; rewrite H0 in H3. simp_in_support. simpl in *. intuition. inversion H3; clear H3; subst. apply filter_In in H4. intuition. unfold well_formed_Bvector_perm, well_formed_perm in *. intuition. destruct (in_dec (EqDec_dec _) d lsd). specialize (H6 d). intuition. simpl in *. rewrite eqbBvector_complete in H7. discriminate. edestruct (H (d :: lsd)). econstructor; trivial. intuition. simpl in H7. intuition. subst. trivial. specialize (H6 d0). intuition. simpl in H7. destruct (eqbBvector d0 d). discriminate. trivial. intuition. destruct (in_dec (EqDec_dec _) r x0). exists (removeFirst (EqDec_dec _) x0 r). intuition. simpl. case_eq (eqbBvector r0 r); intuition. apply eqbBvector_sound in H11. subst. exfalso. eapply removeFirst_NoDup_not_in; eauto. case_eq (eqbBvector r0 x); intuition. apply eqbBvector_sound in H12. subst. assert (inRange _ ls x = false). eapply H8. eapply removeFirst_in_iff. eauto. congruence. eapply H8. eapply removeFirst_in_iff. eauto. simpl. eapply in_getAllBvectors. eapply removeFirst_NoDup. trivial. eapply eq_add_S. simpl in H10. rewrite H10. symmetry. eapply removeFirst_length. trivial. destruct x0. simpl in *. lia. exists x0. intuition. simpl. simpl in n1. intuition. case_eq (eqbBvector r0 r); intuition. apply eqbBvector_sound in H13. subst. intuition. case_eq (eqbBvector r0 x); intuition. apply eqbBvector_sound in H14. subst. assert (inRange _ ls x = false). eapply H8. simpl. right. trivial. congruence. eapply H8. simpl. intuition. simpl. eapply in_getAllBvectors. inversion H7; clear H7; subst. trivial. repeat simp_in_support. eapply well_formed_perm_cons; trivial. simpl in *. discriminate. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF