proposition: Theorem schnorr_SHVZK : ∀ LA A, ValidPackage LA [interface #val #[ TRANSCRIPT ] : chInput → chTranscript ] A_export A → fdisjoint LA Sigma_locs → ɛ_SHVZK A = 0.
proof: Proof. intros LA A Va Hdisj. apply: eq_rel_perf_ind. all: ssprove_valid. 3: apply fdisjoints0. 1:{ instantiate (1 := heap_ignore Sigma_locs). ssprove_invariant. apply fsubsetUl. } simplify_eq_rel hwe. destruct hwe as [[h w] e]. ssprove_sync_eq. intros rel. unfold R in rel. apply reflection_nonsense in rel. eapply r_uniform_bij with (1 := bij_f (otf w) (otf e)). intros z_val. ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_restore_pre. 1: ssprove_invariant. apply r_ret. intros s₀ s₁ Hs. unfold f. rewrite rel. split. 2: apply Hs. simpl. rewrite otf_fto expg_mod. 2: rewrite order_ge1 ; apply expg_order. rewrite expgD - !expgVn. rewrite group_prodC group_prodA group_prodC group_prodA /=. rewrite expg_mod. 2: rewrite order_ge1 ; apply expg_order. rewrite -expgM -expgMn. 2: apply group_prodC. rewrite mulgV expg1n mul1g. cbn. rewrite Zp_mulC. reflexivity. 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) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude SigmaProtocol) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)