proposition: Theorem G1_PRF_A_equiv : Pr[G1] == Pr[k <-$ {0, 1}^ eta; [b, _] <-$2 PRF_A _ _ (f_oracle k) tt; ret b].
proof: Proof. Opaque PRFE_Encrypt_OC. unfold G1, PRF_A, PRFE_KeyGen. comp_skip. simpl. inline_first. eapply comp_spec_impl_eq. eapply (@comp_spec_seq _ _ (fun a1 a2 => fst a1 = fst a2 /\ snd a1 = fst (snd a2))); eauto with inhabited. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = fst b)). trivial. intuition. subst. eapply PRFE_EncryptOracle_spec. intuition. destruct b2. simpl in *. subst. prog_simp. simpl. do 2 prog_inline_l. do 2 prog_inline_r. comp_skip. prog_simp. unfold PRFE_Encrypt. do 3 prog_inline_l. do 2 (prog_inline_r; prog_simp). comp_skip. prog_simp. unfold f_oracle. prog_inline_l. do 3 (prog_inline_r; prog_simp). eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = fst b)). trivial. intuition. subst. eapply PRFE_EncryptOracle_spec. intuition. destruct b4; simpl in *; subst. prog_simp. simpl. prog_inline_l; prog_simp. prog_inline_r; prog_simp. eapply comp_spec_ret. intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime