proposition: Lemma test_bij (i j : pid) (m : chMap pid (chProd public choiceTranscript1)) : (i != j)%N → ∃ (f : Secret → Secret), ∀ (x : Secret), bijective f /\ (∀ zk, compute_key (setm m j (fto (g ^+ x), zk)) i = g ^+ (f x)).
proof: Proof. simpl. intros ne. have H := compute_key_bij m i j ne. simpl in H. destruct H as [a [b [a_pos [a_leq_q H]]]]. set a_ord := @inZp ((Zp_trunc #[g]).+1) a. set b_ord := @inZp ((Zp_trunc #[g]).+1) b. pose f' := (fun (x : Secret) => Zp_add (Zp_mul x a_ord) b_ord). exists f'. unfold f'. clear f'. intros x. have := q_order_g. unfold q. intros Hq. split. 2: { intro zk. rewrite (H x zk). apply /eqP. rewrite eq_expg_mod_order. apply /eqP. simpl. rewrite modn_small. 2: { rewrite q_order_g. apply ltn_pmod. apply (prime_gt0 prime_order). } repeat rewrite -> Zp_cast at 3. 2-5: apply (prime_gt1 prime_order). symmetry. rewrite modn_small. 2: { apply ltn_pmod. apply (prime_gt0 prime_order). } simpl. unfold q, q'. rewrite Fp_cast. 2: apply prime_order. rewrite modnMmr. rewrite modnDm. rewrite mulnC. reflexivity. } assert (coprime q'.+2 a_ord) as a_ord_coprime. { rewrite -unitFpE. 2: rewrite Hq ; apply prime_order. rewrite unitfE. simpl. rewrite Zp_cast. 2: apply (prime_gt1 prime_order). unfold q, q' in a_leq_q. rewrite Fp_cast in a_leq_q. 2: apply prime_order. rewrite modn_small. 2: apply a_leq_q. erewrite <- inj_eq. 2: apply ord_inj. rewrite val_Zp_nat. 2: { rewrite pdiv_id. 1: apply prime_gt1. 1,2: rewrite Hq ; apply prime_order. } rewrite -> pdiv_id at 1. 1,2: rewrite Hq. 2: apply prime_order. unfold q in a_leq_q. rewrite modn_small. 2: apply a_leq_q. assumption. } pose f' := (fun (x : Secret) => Zp_mul (Zp_add (Zp_opp b_ord) x) (Zp_inv a_ord)). exists f'. - intro z. unfold f'. clear f'. simpl. rewrite Zp_addC. rewrite -Zp_addA. have -> : (Zp_add b_ord (Zp_opp b_ord)) = Zp0. 1: by rewrite Zp_addC Zp_addNz. rewrite Zp_addC. rewrite Zp_add0z. rewrite -Zp_mulA. rewrite Zp_mulzV. 2: { rewrite -> q_field at 1. assumption. } rewrite Zp_mulz1. reflexivity. - intro z. unfold f'. clear f'. simpl. rewrite Zp_addC. rewrite -Zp_mulA. rewrite Zp_mul_addl. have -> : (Zp_mul (Zp_inv a_ord) a_ord) = Zp1. { rewrite Zp_mulC. rewrite Zp_mulzV. + reflexivity. + rewrite -> q_field at 1. assumption. } rewrite -Zp_mul_addl. rewrite Zp_mulz1. rewrite Zp_addA. have -> : (Zp_add b_ord (Zp_opp b_ord)) = Zp0. 1: by rewrite Zp_addC Zp_addNz. rewrite Zp_add0z. 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) 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)