proposition: Lemma vote_hiding (i j : pid) m: i != j → ∀ LA A ϵ_DDH, ValidPackage LA [interface #val #[ Exec i ] : 'bool → 'public] A_export A → fdisjoint Sigma1.MyAlg.Sigma_locs DDH.DDH_locs → fdisjoint LA DDH.DDH_locs → fdisjoint LA (P_i_locs i) → fdisjoint LA combined_locations → (∀ D, DDH.ϵ_DDH D <= ϵ_DDH) → AdvantageE (Exec_i_realised true m i j) (Exec_i_realised false m i j) A <= ϵ_DDH + ϵ_DDH.
proof: Proof. intros ij_neq LA A ϵ_DDH Va Hdisj Hdisj2 Hdisj3 Hdisj4 Dadv. have [f' [bij_f Hf]] := P_i_aux_equiv i j m Hdisj ij_neq. ssprove triangle (Exec_i_realised true m i j) [:: (Aux_realised true i j m f').(pack) ; (Aux true i j m f') ∘ (par DDH.DDH_ideal (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO)) ; (Aux false i j m f') ∘ (par DDH.DDH_ideal (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO)) ; (Aux_realised false i j m f').(pack) ] (Exec_i_realised false m i j) A as ineq. eapply le_trans. 2: { instantiate (1 := 0 + ϵ_DDH + 0 + ϵ_DDH + 0). by rewrite ?GRing.addr0 ?GRing.add0r. } eapply le_trans. 1: exact ineq. clear ineq. repeat eapply ler_add. { apply eq_ler. specialize (Hf true LA A Va). apply Hf. - rewrite fdisjointUr. apply /andP ; split ; assumption. - rewrite fdisjointUr. apply /andP ; split. 2: assumption. rewrite fdisjointUr. apply /andP ; split ; assumption. } { unfold Aux_realised. rewrite -Advantage_link. rewrite par_commut. have -> : (par DDH.DDH_ideal (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO)) = (par (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO) DDH.DDH_ideal). { apply par_commut. ssprove_valid. } erewrite Advantage_par. 3: apply DDH.DDH_real. 3: apply DDH.DDH_ideal. 2: { ssprove_valid. - eapply fsubsetUr. - apply fsubsetUl. } 1: rewrite Advantage_sym ; apply Dadv. - ssprove_valid. - unfold trimmed. rewrite -link_trim_commut. f_equal. unfold trim. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fsetU !in_fset1 !eq_refl. rewrite filterm0. done. - unfold trimmed. unfold trim. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fset1 !eq_refl. rewrite filterm0. done. - unfold trimmed. unfold trim. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fset1 !eq_refl. rewrite filterm0. done. } 2:{ unfold Aux_realised. rewrite -Advantage_link. rewrite par_commut. have -> : (par DDH.DDH_real (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO)) = (par (Sigma1.Sigma.Fiat_Shamir ∘ RO1.RO) DDH.DDH_real). { apply par_commut. ssprove_valid. } erewrite Advantage_par. 3: apply DDH.DDH_ideal. 3: apply DDH.DDH_real. 2: { ssprove_valid. - eapply fsubsetUr. - apply fsubsetUl. } 1: apply Dadv. - ssprove_valid. - unfold trimmed. rewrite -link_trim_commut. f_equal. unfold trim. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fsetU !in_fset1 !eq_refl. rewrite filterm0. done. - unfold trimmed. unfold trim. unfold DDH.DDH_E. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fset1 !eq_refl. rewrite filterm0. done. - unfold trimmed. unfold trim. unfold DDH.DDH_E. rewrite !fset_cons -fset0E fsetU0. rewrite !filterm_set. simpl. rewrite !in_fset1 !eq_refl. rewrite filterm0. done. } 2: { apply eq_ler. specialize (Hf false LA A Va). rewrite Advantage_sym. apply Hf. - rewrite fdisjointUr. apply /andP ; split ; assumption. - rewrite fdisjointUr. apply /andP ; split. 2: assumption. rewrite fdisjointUr. apply /andP ; split ; assumption. } apply eq_ler. eapply eq_rel_perf_ind with (inv := inv i). 5: apply Va. 1,2: apply Aux_ideal_realised. 3: { rewrite fdisjointUr. apply /andP ; split. 2: assumption. rewrite fdisjointUr. apply /andP ; split ; assumption. } 3: { rewrite fdisjointUr. apply /andP ; split. 2: assumption. rewrite fdisjointUr. apply /andP ; split ; assumption. } { ssprove_invariant. rewrite fsetUC. rewrite -!fsetUA. apply fsetUS. apply fsubsetUl. } simplify_eq_rel v. rewrite !setmE. rewrite !eq_refl. simpl. repeat simplify_linking. rewrite !cast_fun_K. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=>x_i. ssprove_sync=>x_j. pose f_v := (fun (x : secret) => if v then fto (Zp_add (otf x) Zp1) else fto (Zp_add (otf x) (Zp_opp Zp1)) ). assert (bijective f_v) as bij_fv. { exists (fun x => if v then fto (Zp_add (otf x) (Zp_opp Zp1)) else fto (Zp_add (otf x) Zp1) ). - intro x. unfold f_v. case v. + rewrite otf_fto. rewrite -Zp_addA. rewrite Zp_addC. have -> : (Zp_add Zp1 (Zp_opp Zp1)) = (Zp_add (Zp_opp Zp1) Zp1). { intro n. by rewrite Zp_addC. } rewrite Zp_addNz. rewrite Zp_add0z. by rewrite fto_otf. + rewrite otf_fto. rewrite -Zp_addA. rewrite Zp_addC. rewrite Zp_addNz. rewrite Zp_add0z. by rewrite fto_otf. - intro x. unfold f_v. case v. + rewrite otf_fto. rewrite -Zp_addA. rewrite Zp_addNz. rewrite Zp_addC. rewrite Zp_add0z. by rewrite fto_otf. + rewrite otf_fto. rewrite -Zp_addA. rewrite Zp_addC. have -> : (Zp_add Zp1 (Zp_opp Zp1)) = (Zp_add (Zp_opp Zp1) Zp1). { intro n. by rewrite Zp_addC. } rewrite Zp_addNz. rewrite Zp_add0z. by rewrite fto_otf. } eapply r_uniform_bij. 1: apply bij_fv. intro c. ssprove_swap_seq_rhs [:: 1 ; 2]%N. ssprove_swap_seq_rhs [:: 0 ]%N. ssprove_swap_seq_lhs [:: 1 ; 2]%N. ssprove_swap_seq_lhs [:: 0 ]%N. apply r_put_vs_put. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. apply r_put_vs_put. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. apply r_put_vs_put. unfold Sigma1.MyParam.R. rewrite -Hord otf_fto eq_refl. simpl. ssprove_sync=>r_i. apply r_put_vs_put. ssprove_restore_pre. { ssprove_invariant. apply preserve_update_r_ignored_heap_ignore. { rewrite in_fsetU. apply /orP ; right. unfold DDH.DDH_locs. rewrite !fset_cons -fset0E fsetU0. rewrite in_fsetU. apply /orP ; right. rewrite in_fsetU. apply /orP ; right. by apply /fset1P. } apply preserve_update_l_ignored_heap_ignore. 2: apply preserve_update_mem_nil. rewrite in_fsetU. apply /orP ; right. unfold DDH.DDH_locs. rewrite !fset_cons -fset0E fsetU0. rewrite in_fsetU. apply /orP ; right. rewrite in_fsetU. apply /orP ; right. by apply /fset1P. } ssprove_sync. ssprove_sync=>queries. case (queries (Sigma1.Sigma.prod_assoc (fto (g ^+ x_i), fto (g ^+ otf r_i)))) eqn:e. all: rewrite e. all: ssprove_code_simpl ; simpl. all: ssprove_code_simpl_more ; simpl. - apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. rewrite -Hord otf_fto eq_refl. simpl. ssprove_sync=>e_j. apply r_put_lhs. apply r_put_rhs. clear e queries. ssprove_restore_pre. 1: ssprove_invariant. ssprove_sync. ssprove_sync=>queries. case (queries (Sigma1.Sigma.prod_assoc (fto (g ^+ finv f' x_j), fto (g ^+ otf e_j)))) eqn:e. all: rewrite e. all: simpl; ssprove_code_simpl. all: ssprove_code_simpl_more. + apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. apply r_assertD. { intros ??. rewrite !domm_set. done. } intros _ _. apply r_ret. intros ???. split. 2: assumption. unfold f_v. apply vote_hiding_bij. + ssprove_sync=>e_i. apply r_put_vs_put. apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. apply r_assertD. { intros ??. rewrite !domm_set. done. } intros _ _. ssprove_restore_pre. 1: ssprove_invariant. apply r_ret. intros ???. split. 2: assumption. unfold f_v. apply vote_hiding_bij. - ssprove_sync=>e_i. apply r_put_vs_put. apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. rewrite -Hord otf_fto. rewrite -Hord eq_refl. simpl. ssprove_sync=>r_j. apply r_put_lhs. apply r_put_rhs. ssprove_restore_pre. 1: ssprove_invariant. ssprove_sync. ssprove_sync=>queries'. case (queries' (Sigma1.Sigma.prod_assoc (fto (g ^+ finv f' x_j), fto (g ^+ otf r_j)))) eqn:e'. all: rewrite e'. all: simpl; ssprove_code_simpl. all: ssprove_code_simpl_more. + apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. apply r_assertD. { intros ??. rewrite !domm_set. done. } intros _ _. apply r_ret. intros ???. split. 2: assumption. unfold f_v. apply vote_hiding_bij. + ssprove_sync=>e_j. apply r_put_vs_put. apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. apply r_assertD. { intros ??. rewrite !domm_set. done. } intros _ _. ssprove_restore_pre. 1: ssprove_invariant. apply r_ret. intros ???. split. 2: assumption. unfold f_v. apply vote_hiding_bij. 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_composition Package Prelude SigmaProtocol Schnorr DDH) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)