proposition: Theorem G2_PRF_A_equiv : Pr[G2] == Pr[[b, _] <-$2 PRF_A _ _ PRFE_RandomFunc nil; ret b].
proof: Proof. pose proof RF_EncryptOracle_spec as RFE_spec. unfold G2, PRF_A. simpl. inline_first. eapply comp_spec_impl_eq. eapply (@comp_spec_seq _ _ (fun a1 a2 => fst a1 = fst a2 /\ snd a1 = snd (snd a2))); eauto with inhabited. eapply comp_spec_consequence. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = snd b)). trivial. intuition. subst. eapply RFE_spec. intuition. intuition. prog_simp. simpl. do 2 prog_inline_r. comp_skip. unfold RF_Encrypt at 1. prog_simp. prog_inline_l. do 2 prog_inline_r. comp_skip. prog_simp. simpl in *. subst. prog_inline_l. prog_inline_r. comp_skip. inversion H3; clear H3; subst. do 2 prog_inline_r. eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun x y => x = snd y)). trivial. intuition. subst. eapply RFE_spec. intuition. prog_simp. simpl. prog_inline_r. simpl. prog_simp. eapply comp_spec_ret. simpl in *. intuition. subst. intuition. subst; intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime