proposition: Lemma ATTACK_equiv_true: ATTACK true ≈₀ ATTACK_GEN_pkg ∘ GEN_STRETCH true.
proof: Proof. apply: eq_rel_perf_ind_eq. simplify_eq_rel m. apply rpost_weaken_rule with eq; last by move=> [? ?] [? ?] []. simplify_linking. ssprove_code_simpl. ssprove_sync_eq=> s0. erewrite bind_cong. 2: by []. 2: { apply: boolp.funext => x. erewrite (@code_link_map_loop _ 'word _ (zip _ _) tt) => /=. erewrite bind_cong. 1,2: by []. apply: boolp.funext => y. by rewrite {1}(lock (y.1)). } rewrite -(bind_ret _ (map_loop (unzip2 m) s0 _)). erewrite bind_cong. 2: by []. 2: { apply: boolp.funext => x. rewrite {1}(surjective_pairing x). by rewrite {1}(lock x.1). } move: (@locked _) => /= X. ssprove_code_simpl. rewrite -(size_map snd) -/unzip2. move: 0 (unzip2 m) => {m} a m. elim: m => [|mi m IHm] /= in X a s0*. 1: by apply: rreflexivity_rule. rewrite (lock seq_to_chseq). ssprove_code_simpl. case: (PRG s0) => [ti si] /=. rewrite -lock. erewrite (bind_cong _ _ (@map_loop _ 'word _ (iota a.+1 (size m)) si _)). 2: by []. 2: { apply: boolp.funext => x. by rewrite unzip2_seq_to_chseq. } ssprove_code_simpl. by specialize (IHm (fun x => X (seq_to_chseq (enc ti mi :: unzip2 x)))). 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)