proposition: Theorem OWP_HCP : HCP_Advantage f' b A <= (OWP_Advantage f OWP_HCP_B).
proof: Proof. Abort. End OWP_impl_HCP. Section PseudorandomGenerator. Variable n1 : nat. Variable n2 : nat. Variable f : Bvector n1 -> Bvector n2. Hypothesis n2_greater : n2 > n1. Variable A : Bvector n2 -> Comp bool. Definition PRG_G1 := r <-$ {0, 1} ^ n1; g <-$ (A (f r)); ret g. Definition PRG_G2 := r <-$ {0, 1} ^ n2; g <-$ (A r); ret g. Definition PRG_Advantage := | (Pr[PRG_G1]) - (Pr[PRG_G2]) |. End PseudorandomGenerator. Require Import FCF.DetSem. Section OWP_HCP_Impl_PRG. Variable n : nat. Hypothesis n_pos : n > 0. Variable f : Bvector n -> Bvector n. Variable f_inv : Bvector n -> Bvector n. Hypothesis f_inv1 : forall v, f (f_inv v) = v. Hypothesis f_inv2 : forall v, f_inv (f v) = v. Variable b : Bvector n -> bool. Definition OWP_HCP_PRG_fun(v : Bvector n) := (b v) :: (f v). Variable A : Bvector (S n) -> Comp bool. Hypothesis wf_A : forall v, well_formed_comp (A v). Definition B (v : Bvector n)(b : bool) : Comp bool := (A (b :: v)). Lemma rnd_concat_eq : forall (v : Bvector (S n)), evalDist ({0, 1} ^ (S n)) v == evalDist (rb <-$ {0, 1}; r <-$ {0, 1} ^ n; ret (rb :: r)) v. intuition. dist_inline_first. eapply det_eq_impl_dist_sem_eq; wftac. unfold evalDet_equiv. intuition. inversion H; clear H; subst. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s (S n)); intuition. rewrite H in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H5; clear H5; subst. destruct s; simpl in *; try congruence. case_eq (shiftOut s n); intuition; rewrite H0 in H; try congruence. destruct p. inversion H; clear H; subst. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. econstructor. eauto. simpl. rewrite shiftOut_0. econstructor. eauto. simpl. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. econstructor. eauto. simpl. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. econstructor. eauto. simpl. rewrite H0. econstructor. eauto. simpl. econstructor. econstructor. eauto. simpl. econstructor. rewrite H in H4. inversion H4; clear H4; subst. inversion H0; clear H0; subst. simpl in *. destruct s; simpl in *. econstructor. econstructor. eauto. simpl. econstructor. case_eq (shiftOut s n); intuition. rewrite H in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H5; clear H5; subst. rewrite H in H4. econstructor. econstructor. eauto. simpl. rewrite shiftOut_0. econstructor. eauto. simpl. econstructor. eauto. simpl. econstructor. eauto. simpl. rewrite H. econstructor. inversion H; clear H; subst. inversion H0; clear H0; subst. simpl in *. case_eq (shiftOut s 1); intuition; rewrite H in H4. destruct p. inversion H4; clear H4; subst. simpl in *. inversion H5; clear H5; subst. simpl in *. inversion H4; clear H4; subst. simpl in *. case_eq (shiftOut b1 n); intuition; rewrite H0 in H5. destruct p. inversion H5; clear H5; subst. simpl in *. inversion H6; clear H6; subst. simpl in *. inversion H5; clear H5; subst. econstructor. econstructor. eauto. simpl. destruct s; simpl in *; try discriminate. rewrite shiftOut_0 in H. inversion H; clear H; subst. rewrite H0. econstructor. eauto. simpl. econstructor. inversion H5. inversion H4. inversion H0; clear H0; subst. simpl in *. destruct s. simpl in *. econstructor. econstructor. eauto. simpl. econstructor. simpl in *. rewrite shiftOut_0 in H4. inversion H4; clear H4; subst. simpl in *. inversion H3; clear H3; subst. simpl in *. inversion H4; clear H4; subst. simpl in *. case_eq (shiftOut s n); intuition; rewrite H in H3. destruct p. inversion H3; clear H3; subst. simpl in *. inversion H5; clear H5; subst. simpl in *. inversion H4. econstructor. econstructor. eauto. simpl. rewrite H. econstructor. Qed.
imports: FCF.FCF FCF.SemEquiv