proposition: Theorem G2_4_bad_small : Pr[x <-$ G2_4; ret snd x] <= q2 / (2 ^ eta).
proof: Proof. pose proof @RF_Encrypt_wf as RF_Encrypt_wf. pose proof @RF_Encrypt_bad_prob as RF_Encrypt_bad_prob. pose proof @RF_Encrypt_bad_preserved as RF_Encrypt_bad_preserved. unfold G2_4. inline_first; comp_irr_l; wftac. inline_first; comp_irr_l; wftac. eapply oc_comp_wf; intuition. comp_simp. dist_inline_l. comp_irr_l; wftac. comp_inline_l; comp_irr_l; wftac. comp_inline_l. assert ( Pr [a <-$ (A2 s (x, (if x0 then p0 else p) xor x1)) (list (Bvector eta * Bvector eta) * bool)%type (pair_EqDec (list_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta))) bool_EqDec) (RF_Encrypt_bad x) ((x, x1) :: l, false); x2 <-$ ([b', o]<-2 a; ret (eqb x0 b', snd o)); ret snd x2 ] == Pr [a <-$ (A2 s (x, (if x0 then p0 else p) xor x1)) (list (Bvector eta * Bvector eta) * bool)%type (pair_EqDec (list_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta))) bool_EqDec) (RF_Encrypt_bad x) ((x, x1) :: l, false); ret (snd (snd a))] ). comp_skip. comp_simp. simpl. intuition. match goal with [H4:_ |- _ ] => rewrite H4; clear H4 end. eapply leRat_trans. eapply RndInAdaptive_prob; eauto. intros. destruct a. simpl in *; subst. eapply RF_Encrypt_bad_prob. intuition. eapply RF_Encrypt_bad_preserved. eauto. trivial. eapply eqRat_impl_leRat. rewrite <- ratMult_num_den. eapply eqRat_terms. lia. unfold posnatMult, natToPosnat, posnatToNat. lia. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime