proposition: Lemma P_i_aux_equiv (i j : pid) m: fdisjoint Sigma1.MyAlg.Sigma_locs DDH.DDH_locs → i != j → (∃ f, bijective f ∧ (∀ b, (Exec_i_realised b m i j) ≈₀ Aux_realised b i j m f)).
proof: Proof. intros Hdisj ij_neq. have [f' Hf] := test_bij' i j m ij_neq. simpl in Hf. exists f'. split. { assert ('I_#|'Z_#[g]|) as x. { rewrite card_ord. eapply Ordinal. rewrite ltnS. apply ltnSn. } specialize (Hf x). destruct Hf. assumption. } intro b. eapply eq_rel_perf_ind with (inv := inv i). { ssprove_invariant. rewrite -!fsetUA. apply fsetUS. do 2 (apply fsubsetU ; apply /orP ; right). apply fsubsetUl. } simplify_eq_rel v. rewrite !setmE. rewrite !eq_refl. ssprove_code_simpl. repeat simplify_linking. ssprove_sync => x_i. rewrite !cast_fun_K. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_swap_seq_rhs [:: 4 ; 5 ; 6 ; 7]%N. ssprove_swap_seq_rhs [:: 2 ; 3 ; 4 ; 5 ; 6]%N. ssprove_swap_seq_rhs [:: 0 ; 1 ; 2 ; 3 ; 4 ; 5]%N. ssprove_contract_put_get_rhs. apply r_put_rhs. ssprove_swap_seq_lhs [:: 0 ; 1 ; 2 ; 3]%N. unfold Sigma1.MyParam.R. have Hord : ∀ x, (nat_of_ord x) = (nat_of_ord (otf x)). { unfold otf. intros n x. rewrite enum_val_ord. done. } 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. - unfold DDH.DDH_locs. rewrite in_fsetU. apply /orP ; right. rewrite fset_cons. rewrite in_fsetU. apply /orP ; left. by apply /fset1P. - apply preserve_update_mem_nil. } ssprove_sync. ssprove_swap_seq_lhs [:: 0 ]%N. ssprove_swap_seq_rhs [:: 2 ; 1 ; 0]%N. ssprove_sync => queries. destruct (queries (Sigma1.Sigma.prod_assoc (fto (g ^+ x_i), fto (g ^+ otf r_i)))) eqn:e. all: rewrite e; simpl. all: ssprove_code_simpl_more. - ssprove_swap_seq_lhs [:: 0 ; 1 ; 2 ; 3 ; 4 ; 5]%N. ssprove_swap_seq_lhs [:: 0 ; 1 ]%N. eapply r_uniform_bij. { apply Hf. + rewrite card_ord. rewrite Zp_cast. 2: apply (prime_gt1 prime_order). eapply Ordinal. apply (prime_gt1 prime_order). } intro x. specialize (Hf x). destruct Hf as [bij_f Hf]. apply bij_inj in bij_f. apply finv_f in bij_f. ssprove_contract_put_get_rhs. rewrite bij_f. rewrite -Hord !otf_fto !eq_refl. simpl. apply r_put_rhs. ssprove_restore_pre. { apply preserve_update_r_ignored_heap_ignore. - unfold DDH.DDH_locs. rewrite !fset_cons. rewrite !in_fsetU. apply /orP ; right. apply /orP ; right. apply /orP ; left. by apply /fset1P. - apply preserve_update_mem_nil. } apply r_get_remember_lhs. intros ?. apply r_get_remember_rhs. intros ?. ssprove_forget_all. ssprove_sync=>r_j. apply r_put_vs_put. ssprove_restore_pre. 1: ssprove_invariant. clear e queries. ssprove_sync. ssprove_swap_seq_lhs [:: 0]%N. ssprove_sync=>queries. destruct (queries (Sigma1.Sigma.prod_assoc (fto (g ^+ x), fto (g ^+ otf r_j)))) eqn:e. all: rewrite e. all: ssprove_code_simpl. all: ssprove_code_simpl_more. + ssprove_swap_seq_lhs [:: 0 ; 1]%N. simpl. 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_swap_lhs 1%N. { move: H0 => /eqP. erewrite eqn_add2r. intros contra. discriminate. } ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_restore_pre. { repeat apply preserve_update_l_ignored_heap_ignore. 1,2: unfold P_i_locs ; rewrite in_fsetU. 1,2: apply /orP ; left ; rewrite !fset_cons ; rewrite -fset0E fsetU0 ; rewrite in_fsetU. - apply /orP ; right. by apply /fset1P. - apply /orP ; left. by apply /fset1P. - apply preserve_update_mem_nil. } rewrite otf_fto. rewrite compute_key_set_i. set zk := (fto (g ^+ x), fto (g ^+ otf r_j), s1, fto (otf x2 + otf s1 * otf x)). clearbody zk. specialize (Hf zk). rewrite !Hord. rewrite Hf. rewrite -!Hord. rewrite -expgM. rewrite mulnC. case b; apply r_ret ; done. + ssprove_swap_seq_lhs [:: 0 ; 1 ; 2 ; 3]%N. simpl. 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_swap_lhs 1%N. { move: H0 => /eqP. erewrite eqn_add2r. intros contra. discriminate. } ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_restore_pre. { repeat apply preserve_update_l_ignored_heap_ignore. 1,2: unfold P_i_locs ; rewrite in_fsetU. 1,2: apply /orP ; left ; rewrite !fset_cons ; rewrite -fset0E fsetU0 ; rewrite in_fsetU. - apply /orP ; right. by apply /fset1P. - apply /orP ; left. by apply /fset1P. - ssprove_invariant. } rewrite otf_fto. rewrite compute_key_set_i. set zk := (fto (g ^+ x), fto (g ^+ otf r_j), e_j, fto (otf x2 + otf e_j * otf x)). clearbody zk. specialize (Hf zk). rewrite !Hord. rewrite Hf. rewrite -!Hord. rewrite -expgM. rewrite mulnC. case b; apply r_ret ; done. - ssprove_swap_seq_lhs [:: 0 ; 1 ; 2 ; 3 ; 4 ; 5 ; 6 ; 7]%N. ssprove_swap_seq_lhs [:: 2 ; 1 ; 0 ]%N. eapply r_uniform_bij. { apply Hf. + rewrite card_ord. rewrite Zp_cast. 2: apply (prime_gt1 prime_order). eapply Ordinal. apply (prime_gt1 prime_order). } intro x. specialize (Hf x). destruct Hf as [bij_f Hf]. apply bij_inj in bij_f. apply finv_f in bij_f. ssprove_contract_put_get_rhs. rewrite bij_f. rewrite -Hord !otf_fto !eq_refl. simpl. apply r_put_rhs. ssprove_restore_pre. { apply preserve_update_r_ignored_heap_ignore. - unfold DDH.DDH_locs. rewrite !fset_cons. rewrite !in_fsetU. apply /orP ; right. apply /orP ; right. apply /orP ; left. by apply /fset1P. - apply preserve_update_mem_nil. } 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 eq_refl. simpl. ssprove_sync=>r_j. apply r_put_vs_put. ssprove_restore_pre. 1: ssprove_invariant. clear e queries. ssprove_sync. ssprove_swap_seq_lhs [:: 0]%N. ssprove_sync=>queries. destruct (queries (Sigma1.Sigma.prod_assoc (fto (g ^+ x), fto (g ^+ otf r_j)))) eqn:e. all: rewrite e. all: ssprove_code_simpl. all: ssprove_code_simpl_more. + ssprove_swap_seq_lhs [:: 0 ; 1]%N. simpl. 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_swap_lhs 1%N. { move: H0 => /eqP. erewrite eqn_add2r. intros contra. discriminate. } ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_restore_pre. { repeat apply preserve_update_l_ignored_heap_ignore. 1,2: unfold P_i_locs ; rewrite in_fsetU. 1,2: apply /orP ; left ; rewrite !fset_cons ; rewrite -fset0E fsetU0 ; rewrite in_fsetU. - apply /orP ; right. by apply /fset1P. - apply /orP ; left. by apply /fset1P. - apply preserve_update_mem_nil. } rewrite otf_fto. rewrite compute_key_set_i. set zk := (fto (g ^+ x), fto (g ^+ otf r_j), s, fto (otf x2 + otf s * otf x)). clearbody zk. specialize (Hf zk). rewrite !Hord. rewrite Hf. rewrite -!Hord. rewrite -expgM. rewrite mulnC. case b; apply r_ret ; done. + ssprove_swap_seq_lhs [:: 0 ; 1 ; 2 ; 3]%N. simpl. 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_swap_lhs 1%N. { move: H0 => /eqP. erewrite eqn_add2r. intros contra. discriminate. } ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_contract_put_get_lhs. apply r_put_lhs. ssprove_restore_pre. { repeat apply preserve_update_l_ignored_heap_ignore. 1,2: unfold P_i_locs ; rewrite in_fsetU. 1,2: apply /orP ; left ; rewrite !fset_cons ; rewrite -fset0E fsetU0 ; rewrite in_fsetU. - apply /orP ; right. by apply /fset1P. - apply /orP ; left. by apply /fset1P. - ssprove_invariant. } rewrite otf_fto. rewrite compute_key_set_i. set zk := (fto (g ^+ x), fto (g ^+ otf r_j), e_j, fto (otf x2 + otf e_j * otf x)). clearbody zk. specialize (Hf zk). rewrite !Hord. rewrite Hf. rewrite -!Hord. rewrite -expgM. rewrite mulnC. case b; apply r_ret ; done. 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)