proposition: Lemma PKE_CCA_perf : ∀ b, (PKE_CCA KEM_DEM b) ≈₀ Aux b.
proof: Proof. intro b. unfold Aux. eapply eq_rel_perf_ind with (inv := inv). 1: exact _. simplify_eq_rel m. all: ssprove_code_simpl. - ssprove_code_simpl_more. ssprove_code_simpl. ssprove_swap_seq_rhs [:: 1 ; 0 ; 2 ; 1 ]%N. eapply r_get_vs_get_remember. 1: ssprove_invariant. intro sk. ssprove_sync. intro skNone. eapply r_get_remember_rhs. intro pk. eapply (r_rem_couple_lhs pk_loc sk_loc). 1,3: exact _. 1:{ eapply Remembers_lhs_from_tracked_rhs. all: ssprove_invariant. } intro eps. destruct sk. 1: discriminate. destruct pk. 1: contradiction. simpl. eapply r_scheme_bind_spec. 1: eapply KEM_kgen_spec. intros [pk' sk'] pps. eapply r_put_vs_put. eapply r_put_vs_put. ssprove_restore_mem. 1:{ ssprove_invariant. - intros s₀ s₁ hh. unfold triple_rhs in *. simpl in *. destruct hh as [[[hi ?] ?] e]. simpl in *. rewrite e in hi. get_heap_simpl. destruct (get_heap s₁ k_loc), (get_heap s₁ ek_loc). all: try contradiction. auto. - auto. } apply r_ret. auto. - ssprove_code_simpl_more. ssprove_code_simpl. ssprove_swap_seq_rhs [:: 5 ; 4 ; 3 ; 2 ; 1 ]%N. ssprove_contract_get_rhs. eapply r_get_vs_get_remember. 1: ssprove_invariant. intro pk. ssprove_sync. intro pkSome. destruct pk as [pk|]. 2: discriminate. simpl. ssprove_swap_seq_rhs [:: 3 ; 2 ; 1 ]%N. ssprove_contract_get_rhs. eapply r_get_vs_get_remember. 1: ssprove_invariant. intro ek. ssprove_sync. intro ekNone. rewrite ekNone. simpl. eapply r_get_vs_get_remember_rhs. 1: ssprove_invariant. intro c. ssprove_sync. intro cNone. eapply r_scheme_bind_spec. 1: eapply KEM_encap_spec. intros [k' ek'] hkek. ssprove_code_simpl_more. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_swap_seq_rhs [:: 3 ; 2 ; 1 ]%N. ssprove_contract_put_rhs. ssprove_swap_seq_rhs [:: 3 ; 2 ; 1 ; 0 ]%N. eapply r_get_remind_rhs. 1: exact _. rewrite cNone. simpl. ssprove_forget. ssprove_swap_seq_rhs [:: 0 ]%N. eapply r_get_remember_rhs. intros k. eapply (r_rem_triple_rhs pk_loc k_loc ek_loc). 1-4: exact _. intro hpke. destruct ek. 1: discriminate. destruct k. 1: contradiction. simpl. ssprove_swap_seq_rhs [:: 0 ; 1 ]%N. ssprove_contract_put_get_rhs. simpl. ssprove_swap_seq_rhs [:: 1 ; 0 ; 2 ; 1 ]%N. ssprove_contract_put_rhs. ssprove_swap_seq_lhs [:: 0 ]%N. ssprove_sync. apply r_put_rhs. apply r_put_vs_put. ssprove_restore_mem. 1:{ ssprove_invariant. intros s₀ s₁ hh. unfold triple_rhs in *. simpl in *. destruct hh as [[[[[hi ?] epk] ?] ?] ?]. simpl in *. get_heap_simpl. rewrite epk. simpl. auto. } apply r_ret. auto. - destruct m as [ek' c']. simpl. ssprove_swap_seq_rhs [:: 1 ; 0 ]%N. ssprove_swap_seq_lhs [:: 1 ; 0 ]%N. eapply r_get_vs_get_remember_rhs. 1: ssprove_invariant. intros ek. destruct (ek == Some ek') eqn:eek. + rewrite eek. ssprove_code_simpl_more. ssprove_code_simpl. ssprove_code_simpl_more. eapply r_get_remember_rhs. intro pk. eapply r_get_remember_lhs. intro sk. eapply (r_rem_couple_lhs pk_loc sk_loc). 1,3: exact _. 1:{ eapply Remembers_lhs_from_tracked_rhs. - exact _. - ssprove_invariant. } intro eps. eapply sameSomeRel_sameSome in eps as eps'. rewrite eps'. ssprove_sync. intro skSome. ssprove_swap_seq_rhs [:: 1 ]%N. ssprove_contract_get_rhs. ssprove_sync. intro c. ssprove_sync. intro neq. move: neq => /eqP neq. move: eek => /eqP eek. subst ek. destruct (c != Some c') eqn:e. 2:{ move: e => /eqP e. subst. contradiction. } rewrite e. simpl. eapply r_get_remember_rhs. intro k. eapply (r_rem_triple_rhs pk_loc k_loc ek_loc). 1-4: exact _. intro hpke. destruct sk as [sk|]. 2: discriminate. destruct pk as [pk|]. 2: contradiction. destruct k as [k|]. 2: contradiction. simpl. simpl in hpke. simpl in eps. unfold PkeyPair in eps. eapply hpke in eps as h. simpl in h. subst. ssprove_forget_all. apply r_ret. auto. + rewrite eek. ssprove_code_simpl_more. ssprove_swap_seq_rhs [:: 5 ; 4 ; 3 ; 2 ; 1 ; 0 ]%N. eapply r_get_remind_rhs. 1: exact _. ssprove_forget. ssprove_swap_seq_rhs [:: 3 ; 2 ; 1 ; 0 ]%N. apply r_get_vs_get_remember. 1: ssprove_invariant. intros sk. apply r_get_remember_rhs. intro pk. eapply (r_rem_couple_lhs pk_loc sk_loc). 1,3: exact _. 1:{ apply Remembers_lhs_from_tracked_rhs. all: ssprove_invariant. } intro eps. eapply sameSomeRel_sameSome in eps as eps'. rewrite eps'. ssprove_forget_all. ssprove_sync. intro skSome. ssprove_sync. intro c. ssprove_sync. intro ee. destruct sk as [sk|]. 2: discriminate. simpl. rewrite eek. simpl. apply r_ret. auto. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)