proposition: Lemma commitment_binding : ∀ LA A, ValidPackage LA [interface #val #[ SOUNDNESS ] : chSoundness → 'bool ] A_export A → fdisjoint LA (Sigma_to_Com_locs :|: KEY_locs) → AdvantageE (Com_Binding ∘ Sigma_to_Com ∘ KEY) (Special_Soundness_t) A = 0.
proof: Proof. intros LA A VA Hdisj. eapply eq_rel_perf_ind_eq. 4: apply VA. 1:{ ssprove_valid. 3: apply fsub0set. 1: instantiate (1 := (Sigma_to_Com_locs :|: KEY_locs)). 2: apply fsubsetUr. 1: apply fsubsetUl. apply fsubsetxx. } 1: ssprove_valid. 2: assumption. 2: apply fdisjoints0. rewrite Sigma_to_Com_equation_1. simplify_eq_rel h. ssprove_code_simpl. simpl. destruct h, s0, s1, s1, s2. apply r_ret. auto. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)