proposition: Theorem G2_4_5_badness_same : Pr[x <-$ G2_4; ret (snd x)] == Pr[x <-$ G2_5; ret (snd x)].
proof: Proof. pose proof @RF_Encrypt_bad_wf as RF_Encrypt_bad_wf. pose proof @RF_Encrypt_bad_preserved as RF_Encrypt_bad_preserved. unfold G2_4, G2_5. do 4 (inline_first; comp_skip; comp_simp). inline_first. inline_first. eapply comp_spec_impl_eq. eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq_until_bad _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a => snd a) (fun a => snd a) (fun a b => forall z, z <> x -> arrayLookup _ (fst a) z = arrayLookup _ (fst b) z)). intuition. intuition. intuition. simpl in *; subst. clear H2. comp_skip. unfold PRFE_RandomFunc, randomFunc. case_eq (eqbBvector x b); intuition. prog_irr_l. destruct (arrayLookup (Bvector_EqDec eta) a b); wftac. prog_irr_r. destruct ( arrayLookup (Bvector_EqDec eta) a0 b); wftac. prog_simp. eapply comp_spec_ret; simpl in *; intuition. rewrite orb_true_r in H9. discriminate. rewrite orb_true_r in H9. discriminate. case_eq (arrayLookup (Bvector_EqDec eta) a b); intuition. rewrite <- H4. rewrite H7. prog_simp. eapply comp_spec_ret; simpl in *; intuition. intuition; subst. rewrite eqbBvector_complete in H6. discriminate. rewrite <- H4. rewrite H7. prog_inline_l. prog_inline_r. comp_skip. prog_simp. eapply comp_spec_ret; simpl in *; intuition. case_eq (eqbBvector z b); intuition. intuition; subst. rewrite eqbBvector_complete in H6. discriminate. intros. destruct c. destruct b. eauto. trivial. intros. destruct c. destruct b. eapply RF_Encrypt_bad_preserved . eauto. trivial. intuition. simpl. case_eq ( eqbBvector z x); intuition. apply eqbBvector_sound in H5; intuition. trivial. intuition. prog_simp. clear H2. eapply comp_spec_ret; simpl in *; intuition. subst. trivial. destruct p1; simpl in *. subst; intuition. Unshelve. eauto. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime