proposition: Theorem schnorr_com_hiding : ∀ LA A, ValidPackage LA [interface #val #[HIDING] : (chChallenge) × (chChallenge) → chMessage ] A_export (A ∘ par KEY (ID Hiding_E)) -> fdisjoint LA KEY_locs -> fdisjoint LA Sigma_to_Com_locs -> fdisjoint LA (fset [:: setup_loc]) -> fdisjoint LA Sigma_locs -> fdisjoint LA Simulator_locs -> ɛ_hiding A <= 0.
proof: Proof. intros LA A VA Hd1 Hd2 Hd3 Hd4 Hd5. eapply le_trans. 1: eapply commitment_hiding with (LA := LA). all: try assumption. 1: apply fdisjoint0s. { unfold Sigma_locs. unfold commit_loc. unfold statement_loc. unfold witness_loc. rewrite !fset_cons. rewrite -fset0E. rewrite fdisjointUr ; apply /andP ; split. - rewrite fdisjoints1. rewrite fset1E. rewrite fsetU0. rewrite -fset1E. unfold "\notin". rewrite in_fset1. case (_ == _) eqn:e. 2: done. move: e => /eqP. done. - rewrite fdisjointUr ; apply /andP ; split. + rewrite fdisjoints1. rewrite fset1E. rewrite fsetU0. rewrite -fset1E. unfold "\notin". rewrite in_fset1. case (_ == _) eqn:e. 2: done. move: e => /eqP. done. + apply fdisjoints0. } rewrite addr0. rewrite add0r. erewrite schnorr_SHVZK. 2: { ssprove_valid. 1: instantiate (1 := (LA :|: (setup_loc |: Sigma_to_Com_locs))). 3: apply fsubsetxx. 2: apply fsub0set. - apply fsubsetUl. - apply fsubsetU ; apply /orP ; right. apply fsubsetxx. } 2: { unfold Sigma_to_Com_locs. unfold Simulator_locs. rewrite fsetU0. rewrite fdisjointUl ; apply /andP ; split. - assumption. - unfold Sigma_locs. rewrite fdisjointUl ; apply /andP ; split. + rewrite fdisjoint1s. unfold "\notin". rewrite -fset1E. rewrite in_fset1. done. + unfold Com_locs. rewrite fset_cons. rewrite fdisjointUl ; apply /andP ; split. ++ rewrite fdisjoint1s. rewrite -fset1E. unfold "\notin". rewrite in_fset1. done. ++ rewrite -!fset1E. rewrite fdisjoint1s. unfold "\notin". rewrite in_fset1. done. } rewrite Advantage_sym. erewrite schnorr_SHVZK. 2: { ssprove_valid. 1: instantiate (1 := (LA :|: (setup_loc |: Sigma_to_Com_locs))). 3: apply fsubsetxx. 2: apply fsub0set. - apply fsubsetUl. - apply fsubsetU ; apply /orP ; right. apply fsubsetxx. } 2: { unfold Sigma_to_Com_locs. unfold Simulator_locs. rewrite fsetU0. rewrite fdisjointUl ; apply /andP ; split. - assumption. - unfold Sigma_locs. rewrite fdisjointUl ; apply /andP ; split. + rewrite fdisjoint1s. unfold "\notin". rewrite -fset1E. rewrite in_fset1. done. + unfold Com_locs. rewrite fset_cons. rewrite fdisjointUl ; apply /andP ; split. ++ rewrite fdisjoint1s. rewrite -fset1E. unfold "\notin". rewrite in_fset1. done. ++ rewrite -!fset1E. rewrite fdisjoint1s. unfold "\notin". rewrite in_fset1. done. } rewrite addr0 add0r. apply eq_ler. eapply eq_rel_perf_ind. 1,2: exact _. 1:{ instantiate (1 := (heap_ignore Com_locs)). ssprove_invariant. unfold Sigma_to_Com_locs. rewrite !fset0U. apply fsubsetU; apply /orP; left. apply fsubsetU; apply /orP; left. apply fsubsetU; apply /orP; right. apply fsubsetU; apply /orP; left. apply fsubsetxx. } 2: apply VA. 3: { rewrite fset0U. rewrite fdisjointUr ; apply /andP ; split. 2: assumption. rewrite fdisjointUr ; apply /andP ; split. 2: assumption. rewrite fset1E. assumption. } 2: { rewrite fset0U. rewrite fdisjointUr ; apply /andP ; split. 2: assumption. rewrite fdisjointUr ; apply /andP ; split. 2: assumption. rewrite fset1E. assumption. } rewrite Sigma_to_Com_Aux_equation_1. simplify_eq_rel hwe. ssprove_code_simpl. simplify_linking. destruct hwe as [e e']. apply r_const_sample_R. 1: apply LosslessOp_uniform. intros e_rand. rewrite !cast_fun_K. ssprove_code_simpl. ssprove_code_simpl_more. apply r_const_sample_L. 1: apply LosslessOp_uniform. intros b. simpl. case (Nat.even b) eqn:hb. - rewrite hb ; clear hb. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=>setup. apply r_assertD. 1: done. intros _ _. ssprove_sync=> w. apply r_assertD. 1: done. intros _ _. ssprove_sync. apply r_assertD. 1: done. intros _ rel. ssprove_sync=>x. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. eapply r_put_vs_put. eapply r_put_vs_put. eapply r_put_vs_put. ssprove_restore_pre. 1: ssprove_invariant. apply r_ret. intuition auto. - rewrite hb ; clear hb. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=>setup. apply r_assertD. 1: done. intros _ _. ssprove_sync=> w. apply r_assertD. 1: done. intros _ _. ssprove_sync. apply r_assertD. 1: done. intros _ rel. ssprove_sync=>x. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. eapply r_put_vs_put. eapply r_put_vs_put. eapply r_put_vs_put. ssprove_restore_pre. 1: ssprove_invariant. 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) 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)