proposition: Lemma run_interactive_shvzk : ∀ LA A, ValidPackage LA [interface #val #[ RUN ] : chRelation → chTranscript ] A_export A → fdisjoint LA Sigma_locs → AdvantageE RUN_interactive (SHVZK_real_aux ∘ SHVZK_real) A = 0.
proof: Proof. intros LA A Va Hdisj. eapply eq_rel_perf_ind_eq. 5,6: apply Hdisj. 4: apply Va. 2:{ rewrite <- fsetUid. eapply valid_link. - apply SHVZK_real_aux. - apply SHVZK_real. } 1:{ eapply valid_package_inject_export. 2: apply RUN_interactive. apply fsubset_ext. intros ? ?. rewrite fset_cons. apply /fsetUP. right. assumption. } simplify_eq_rel hw. ssprove_code_simpl. rewrite cast_fun_K. ssprove_code_simpl. destruct hw as [h w]. ssprove_code_simpl_more. ssprove_code_simpl. ssprove_swap_rhs 0%N. ssprove_sync_eq. intro rel. ssprove_swap_rhs 0%N. apply rsame_head. intros [a st]. ssprove_sync_eq. intro e. apply rsame_head. intro z. apply r_ret. intuition 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)