proposition: Lemma CCA_EVAL_HYB_equiv_true: CCA_EVAL_TAG_pkg_tt ∘ TAG false ≈₀ CCA_EVAL_HYB_pkg ∘ CPA_EVAL true.
proof: Proof. apply eq_rel_perf_ind with ( (fun '(h0, h1) => h0 = h1) ⋊ couple_lhs S_loc T_loc (fun S T => S = T) ). 1: { ssprove_invariant=> //=. all: by rewrite /CCA_EVAL_TAG_locs /TAG_locs_ff !fset_cons !in_fsetU !in_fset1 eq_refl Bool.orb_true_r. } simplify_eq_rel m. all: simplify_linking. all: ssprove_code_simpl. all: ssprove_code_simpl. - case: m => [ml mr]. apply: r_get_vs_get_remember => S. ssprove_sync=> [|[ke|]]; first by move=> ? ? ->. 2: ssprove_sync=> ke; ssprove_sync; first by move=> ? ? ->. all: apply: r_get_vs_get_remember => T. all: ssprove_sync=> [|[km|]]; first by move=> ? ? ->. 2,4: ssprove_sync=> km; ssprove_sync; first by move=> ? ? ->. all: apply: (r_rem_couple_lhs S_loc T_loc) => Hinv. all: apply: r_put_vs_put. all: apply: r_put_vs_put. all: ssprove_restore_mem; last by apply: r_ret. all: ssprove_invariant. all: by rewrite Hinv. - case: m => [c t]. apply: r_get_remember_lhs => S. destruct ((c, t) \in domm S) eqn:Heq. all: rewrite Heq. 1: by apply: r_ret => ? ? []. apply: r_get_remember_lhs => T. apply: (r_rem_couple_lhs S_loc T_loc) => Hinv. rewrite -Hinv Heq /=. by apply: r_ret => ? ? [] []. 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)