proposition: Theorem G2_3_bad_equiv : Pr[x <-$ G2_3; ret (snd x)] == Pr[G2_3_bad].
proof: Proof. unfold G2_3, G2_3_bad. inline_first. comp_skip. unfold au_F_A. simpl. inline_first. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = fst b)). trivial. intuition. subst. unfold F_randomFunc, WCR_Oracle. inline_first. comp_simp. case_eq (arrayLookup_f (Bvector_EqDec b) (fst x2) (F x a)); intuition. simpl. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. simpl. inline_first. comp_skip. apply (oneVector c). apply (oneVector c). comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. simpl in *. intuition; subst. comp_simp. simpl. inline_first. unfold funcCollision. case_eq (findCollision (list_EqDec (Bvector_EqDec b)) (Bvector_EqDec b) (fst (split (fst (snd b1))))); intuition. destruct p. destruct p. simpl. comp_simp. eapply comp_spec_ret; intuition. destruct b1. simpl in *. destruct p. simpl in *. apply findCollision_correct in H2. intuition. case_eq (eqb l l0); intuition. rewrite eqb_leibniz in H4. intuition. simpl. assert (forall a b, In (a, b) (fst (split l1)) -> b = F x a). intuition. eapply (@oc_comp_invariant _ _ _ _ _ (fun l1 => forall a b, In (a, b) (fst (split l1)) -> b = F x a)) in H0. eauto. intuition. unfold F_randomFunc in *. case_eq (arrayLookup_f (Bvector_EqDec b) c0 (F x d)); intuition. rewrite H11 in H7. repeat simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. intuition. pairInv. trivial. rewrite H11 in H7. repeat simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. intuition. pairInv. trivial. intuition. simpl in *. intuition. trivial. assert (b0 = F x l). eapply H6. trivial. eapply H6 in H5. subst. rewrite H7. rewrite eqbBvector_complete. trivial. comp_simp. rewrite eqb_refl. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv