proposition: Theorem security_based_on_prg LA A: ValidPackage LA [interface #val #[query]: 'unit → 'word × 'word × 'word ] A_export A -> Advantage GEN_STRETCH A <= prg_epsilon (A ∘ GEN_STRETCH_HYB_pkg_1) + prg_epsilon (A ∘ GEN_STRETCH_HYB_pkg_2).
proof: Proof. move=> vA. rewrite Advantage_E Advantage_sym. ssprove triangle (GEN_STRETCH true) [:: GEN_STRETCH_HYB_pkg_1 ∘ GEN true ; GEN_STRETCH_HYB_pkg_1 ∘ GEN false ; GEN_STRETCH_HYB_pkg_2 ∘ GEN true ; GEN_STRETCH_HYB_pkg_2 ∘ GEN false ] (GEN_STRETCH false) A as ineq. apply: le_trans. 1: by apply: ineq. rewrite GEN_equiv_true ?fdisjointUr ?fdisjoints0 // GRing.add0r. rewrite GEN_HYB_equiv ?fdisjointUr ?fdisjoints0 // GRing.addr0. rewrite GEN_equiv_false ?fdisjointUr ?fdisjoints0 // GRing.addr0. by rewrite /prg_epsilon !Advantage_E -!Advantage_link !(Advantage_sym (GEN true)). 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)