proposition: Lemma RndNat_uniform : forall v1 v2 n, v1 < n -> v2 < n -> evalDist (RndNat n) v1 == evalDist (RndNat n) v2.
proof: Proof. intuition. eapply evalDist_Repeat_eq; intuition. unfold RndNat_unchecked. remember (lognat n) as length. eapply (evalDist_iso (BVxor length (BVxor length (natToBv length v1) (natToBv length v2))) (BVxor length (BVxor length (natToBv length v1) (natToBv length v2)))); intuition. remember (BVxor length (natToBv length v1) (natToBv length v2)) as z. rewrite <- BVxor_assoc. rewrite BVxor_same_id. rewrite BVxor_id_l. trivial. rewrite <- BVxor_assoc. rewrite BVxor_same_id. rewrite BVxor_id_l. trivial. simpl. eapply in_getAllBvectors. eapply uniformity. simpl. destruct (EqDec_dec nat_EqDec (bvToNat x) v2); subst. destruct (EqDec_dec nat_EqDec (bvToNat (BVxor (lognat n) (BVxor (lognat n) (natToBv (lognat n) v1) (natToBv (lognat n) (bvToNat x))) x)) v1). intuition. exfalso. eapply n0. rewrite natToBv_bvToNat_inverse. rewrite BVxor_assoc. rewrite BVxor_same_id. rewrite BVxor_id_r. eapply bvToNat_natToBv_inverse. eapply lognat_monotonic. lia. destruct (EqDec_dec nat_EqDec (bvToNat (BVxor (lognat n) (BVxor (lognat n) (natToBv (lognat n) v1) (natToBv (lognat n) v2)) x)) v1). exfalso. eapply n0. rewrite BVxor_assoc in e. assert ((BVxor (lognat n) (natToBv (lognat n) v2) x) = (Bvect_false (lognat n))). eapply BVxor_id_r_inv. eapply bvToNat_natToBv_eq. eauto. apply BVxor_id_inv in H2. rewrite <- H2. eapply bvToNat_natToBv_inverse. eapply lognat_monotonic. lia. intuition. unfold ltNatBool. destruct (lt_dec v1 n); destruct (lt_dec v2 n); congruence. eapply filter_In; intuition. eapply RndNat_unchecked_lt_support. trivial. unfold ltNatBool. destruct (lt_dec v1 n); congruence. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1