proposition: Lemma CTXT_HYB_equiv_1: CTXT_EVAL_SAMP_pkg ∘ EVAL_SAMP true ≈₀ CTXT_HYB_pkg_1 ∘ SAMP Key_N false.
proof: Proof. apply eq_rel_perf_ind with ( (fun '(h0, h1) => h0 = h1) ⋊ couple_rhs T_loc R_loc (fun T R => forall m r, r \notin domm R -> getm T (mkciph m r) = None) ). 1: { ssprove_invariant=> //. all: by rewrite /CTXT_HYB_locs_1 !fset_cons !in_fsetU !in_fset1 eq_refl !Bool.orb_true_r. } simplify_eq_rel m. all: ssprove_code_simpl. 1: rewrite cast_fun_K. all: ssprove_code_simpl. all: apply: r_get_vs_get_remember => R. all: ssprove_code_simpl_more. - ssprove_sync=> H1. ssprove_sync=> r. apply: r_get_vs_get_remember => T. apply: (r_rem_couple_rhs T_loc R_loc) => Hinv. rewrite Hinv -?in_compl ?sample_subset_in //. ssprove_sync=> c. ssprove_sync=> [|Tinv]; first by move=> ? ? ->. ssprove_swap_seq_lhs [:: 1; 0]. ssprove_sync=> [|S]; first by move=> ? ? ->. do 4 apply: r_put_vs_put. all: ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> m' r'. rewrite domm_set in_fsetU => /norP [H H']. rewrite setmE mkciph_eq. rewrite in_fset1 in H. move: H => /negPf ->. by rewrite Bool.andb_false_r Hinv. - ssprove_sync=> [|S]; first by move=> ? ? ->. ssprove_sync=> H1. ssprove_sync=> [|Tinv]; first by move=> ? ? ->. case: (getm Tinv m) => [c|]. + apply: r_put_vs_put. all: ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> s0 s1 [[/= Hinv <-] <-] m' r'. rewrite get_set_heap_eq domm_set in_fsetU => /norP [H H']. rewrite get_set_heap_neq. 2: by apply /eqP. by rewrite Hinv. + ssprove_sync=> c. apply: r_get_vs_get_remember => T. apply: (r_rem_couple_rhs T_loc R_loc) => Hinv. do 3 apply: r_put_vs_put. all: ssprove_restore_mem; last by apply: r_ret. ssprove_invariant=> m' r'. rewrite domm_set in_fsetU => /norP [H H']. rewrite setmE -(mkciph_ciph_to_pair c) mkciph_eq. rewrite in_fset1 in H. move /negPf in H. by rewrite H Bool.andb_false_r Hinv. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)