proposition: Theorem fiat_shamir_correct : ∀ LA A , ValidPackage LA [interface #val #[ RUN ] : chRelation → chTranscript ] A_export A → fdisjoint LA (Sigma_locs :|: RO_locs) → fdisjoint Sigma_locs RO_locs → AdvantageE (Fiat_Shamir ∘ RO) RUN_interactive A = 0.
proof: Proof. intros LA A Va Hdisj Hdisj_oracle. eapply eq_rel_perf_ind_ignore. 6: apply Hdisj. 6:{ rewrite fdisjointUr in Hdisj. move: Hdisj => /andP [h _]. apply h. } 5: apply Va. 1:{ ssprove_valid. 2: apply fsubsetUl. 2: apply fsubsetUr. eapply valid_package_inject_export. 2: apply Fiat_Shamir. apply fsubset_ext. intros. rewrite fset_cons. apply /fsetUP. right. assumption. } 1:{ eapply valid_package_inject_export. 2: apply RUN_interactive. apply fsubset_ext. intros. rewrite fset_cons. apply /fsetUP. right. assumption. } 1:{ apply fsubsetU. erewrite fsubsetUr. auto. } simplify_eq_rel hw. ssprove_code_simpl. destruct hw as [h w]. ssprove_sync. intros rel. eapply rsame_head_alt. 1: exact _. 1:{ intros l Il. apply get_pre_cond_heap_ignore. revert l Il. apply /fdisjointP. assumption. } 1:{ intros. apply put_pre_cond_heap_ignore. } intros [a st]. ssprove_contract_put_get_lhs. rewrite emptymE. apply r_put_lhs. ssprove_sync. intro e. apply r_put_lhs. ssprove_restore_pre. 1: ssprove_invariant. eapply r_reflexivity_alt. - exact _. - intros l Il. ssprove_invariant. revert l Il. apply /fdisjointP. assumption. - intros. ssprove_invariant. 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)