From 1859ad21d7a20bc9702b2a72ba3e22a6f6b9a5fb Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Mon, 20 May 2024 22:33:04 +0200 Subject: [PATCH] Extractor? But incorrect simulator? --- theories/hacspec/Hacspec_ovn_to_sigma.v | 1691 ++++++++++++----------- 1 file changed, 917 insertions(+), 774 deletions(-) diff --git a/theories/hacspec/Hacspec_ovn_to_sigma.v b/theories/hacspec/Hacspec_ovn_to_sigma.v index 6bf63e2..cd4d61f 100644 --- a/theories/hacspec/Hacspec_ovn_to_sigma.v +++ b/theories/hacspec/Hacspec_ovn_to_sigma.v @@ -69,6 +69,21 @@ Import GroupScope GRing.Theory. Import PackageNotation. +From Hammer Require Import Reflect. +From Hammer Require Import Hammer. +Hammer_version. +Hammer_objects. + +(* Set Hammer Z3. *) +(* Unset Hammer Parallel. *) +(* (* (* disable the preliminary sauto tactic *) *) *) +(* (* Set Hammer SAutoLimit 0. *) *) +(* Set Hammer GSMode 1. *) +(* Set Hammer ATPLimit 30. *) +(* Hammer_cleanup. *) + +Require Import SMTCoq.SMTCoq. +(* Set SMT Solver "z3". (** Use Z3, also "CVC4" **) *) Module Misc. @@ -90,7 +105,8 @@ Module Misc. + discriminate H. - intros. destruct (choice_complete_subdef (fun x => P (f x)) (match H with ex_intro _ x H_P => ex_intro _ (f_inv x) (eq_ind_r P H_P (η x)) end )). - exists x. now destruct (find_subdef _ _). + exists x. + now destruct (find_subdef _ _). - intros P Q H_eq n. now rewrite (choice_extensional_subdef (fun x => P (f x)) (fun x => Q (f x)) (fun x => H_eq (f x)) n). Qed. @@ -867,6 +883,131 @@ Module HacspecGroup (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat Add Ring v_Z_ring : hacspec_ring_theory ( setoid (setoid_structure f_Z) ring_eq_ext ). (* Add Field v_Z_field : hacspec_field_theory ( setoid (setoid_structure _) ring_eq_ext ). *) + Definition zq_ring_theory q : + ring_theory (R := 'Z_q) (0)%R (1)%R + (GRing.add) (GRing.mul) + (fun x y => GRing.add x (GRing.opp y)) + (GRing.opp) eq_op. + Proof. + apply (mk_rt (R := 'Z_q) (0)%R (1)%R + (GRing.add) (GRing.mul) + (fun x y => GRing.add x (GRing.opp y)) + (GRing.opp) eq_op). + all: intros. + all: apply (ssrbool.introT eqP). + { + apply add0r. + } + { + apply addrC. + } + { + apply addrA. + } + { + apply mul1r. + } + { + apply mulrC. + } + { + apply mulrA. + } + { + apply mulrDl. + } + { + reflexivity. + } + { + apply (ssrbool.elimT eqP). + rewrite subr_eq0. + apply eqxx. + } + Defined. + + Lemma all_unit_in_prime_field q `{prime q} : forall (p : 'Z_q), (p != 0%R)%N -> p \is a GRing.unit. + Proof. + intros. + assert (1 < q)%N. + { + destruct q. + - destruct p. + now destruct m. + - destruct q. + + destruct p. + now destruct m. + + easy. + } + epose (unitZpE (p := q) p H0). + setoid_rewrite Zp_nat in e. + rewrite valZpK in e. + + rewrite e. + - rewrite (prime_coprime _ prime0). + cbn. + rewrite modn_small. + + now destruct p, m. + + destruct p. + simpl. + pose Zp_cast. + clear -i H0. + now rewrite Zp_cast in i. + Qed. + + Definition zq_field_theory q `{prime q} : + field_theory (R := 'Z_q) 0%R 1%R (GRing.add) + (GRing.mul) (fun x y => GRing.add x (GRing.opp y)) + (GRing.opp) (fun x y => GRing.mul x (GRing.inv y)) + (GRing.inv) eq_op. + Proof. + apply (mk_field + (fun x y => GRing.mul x (GRing.inv y)) + (GRing.inv) + (zq_ring_theory q) + ). + { + easy. + } + { + easy. + } + { + intros. + apply (ssrbool.introT eqP). + apply mulVr. + now apply all_unit_in_prime_field. + } + Defined. + + Lemma zq_ring_eq_ext q : Ring_theory.ring_eq_ext + (R := 'Z_q) (GRing.add) + (GRing.mul) + (GRing.opp) eq_op. + Proof. + constructor. + - intros x y H. + intros z w H0. + apply (ssrbool.introT eqP). + apply (ssrbool.elimT eqP) in H , H0. + subst. + reflexivity. + - intros x y H. + intros z w H0. + apply (ssrbool.introT eqP). + apply (ssrbool.elimT eqP) in H , H0. + subst. + reflexivity. + - intros x y H. + apply (ssrbool.introT eqP). + apply (ssrbool.elimT eqP) in H. + subst. + reflexivity. + Qed. + + Add Ring v_Z_ring : hacspec_ring_theory ( setoid (setoid_structure f_Z) ring_eq_ext ). + (* Add Field v_Z_field : hacspec_field_theory ( setoid (setoid_structure _) ring_eq_ext ). *) + End HacspecGroup. Module Type SecureGroup (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperationProperties OVN_impl). @@ -889,6 +1030,17 @@ Module HacspecGroupParam (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupO Definition g_gen : ζ = <[g]> := v_G_g_gen. Definition prime_order : prime #[g] := v_G_prime_order. + (* order of g *) + Definition q : nat := #[g]. + + Definition hacspec_zq_ring_theory := @zq_ring_theory q. + Definition hacspec_zq_field_theory := @zq_field_theory q prime_order. + + Definition hacspec_zq_setoid_structure := (setoid_structure ('Z_q)). + Definition hacspec_zq_ring_eq_ext := zq_ring_eq_ext q. + Add Ring zq_ring : hacspec_zq_ring_theory ( setoid hacspec_zq_setoid_structure hacspec_zq_ring_eq_ext ). + (* Add Field zq_field : hacspec_zq_field_theory ( setoid hacspec_zq_setoid_structure hacspec_zq_ring_eq_ext ). *) + End HacspecGroupParam. Module Type OVN_schnorr_proof_preconditions (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperationProperties OVN_impl) (SG : SecureGroup OVN_impl GOP). @@ -1063,9 +1215,6 @@ Module Type OVN_or_proof_preconditions (OVN_impl : Hacspec_ovn.HacspecOVNParams) Include HacspecGroup. Export HacspecGroup. - (* order of g *) - Definition q : nat := #[HacspecGroup.g]. - Module MyParam <: SigmaProtocolParams. Definition Witness : finType := prod (Finite.clone _ 'Z_q) 'bool. @@ -1242,7 +1391,7 @@ Module Type OVN_or_proof_preconditions (OVN_impl : Hacspec_ovn.HacspecOVNParams) (a1 == (g ^+ r1) * (x ^+ d1)) && (b1 == (h ^+ r1) * (y ^+ d1)) && (a2 == (g ^+ r2) * (x ^+ d2)) && - (b2 == (h ^+ r2) * ((y * (g ^-1)) ^+ d2))). + (b2 == (h ^+ r2) * (y(* (y * (g ^-1)) *) ^+ d2))). Definition Extractor (xhy : choiceStatement) (a : choiceMessage) (c : choiceChallenge) (c' : choiceChallenge) @@ -1283,8 +1432,9 @@ Module Type OVN_or_proof_preconditions (OVN_impl : Hacspec_ovn.HacspecOVNParams) (* assert (b1 = (h ^+ r1') * (y ^+ d1')) by admit. *) (* assert (b2 = (h ^+ r2') * ((y * (g ^-1)) ^+ d2')) by admit. *) - refine (let xi := ((r1 - r1') + (r2 - r2')) / ((d1' - d1) + (d2' - d2)) in _). - refine (xi, y == h ^+ nat_of_ord xi * g). + (* refine (let vi := _ in _). *) + refine (let xi := ((r1' - r1) + (r2' - r2)) / ((d1 - d1') + (d2 - d2')) in _). + refine (xi, false). Defined. Definition KeyGen (xv : choiceWitness) := @@ -1893,27 +2043,85 @@ Module OVN_or_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat apply e ; clear e. Qed. - Definition f_d2r2_to_wd : 'Z_q -> 'I_MyAlg.i_witness -> Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) → Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)). - Proof. - intros m c dr. - destruct (ch2prod dr) as [d2 r2]. - refine (prod2ch _). (* w, d1 *) - simpl. - refine (fto ((otf r2) + (m * (otf d2))), fto (otf c - otf d2)). - Defined. + Definition f_d2r2_to_wd : 'Z_q -> 'I_MyAlg.i_witness -> Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) → Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) := + fun m c dr => + let '(d2, r2) := (ch2prod dr) in + prod2ch (fto ((otf r2) + (m * (otf d2))), fto (otf c - otf d2)). - Lemma f_d2r2_to_wd_bij : forall m c, bijective (f_d2r2_to_wd m c). Admitted. - - Definition f_d1r1_to_wd : 'Z_q -> 'I_MyAlg.i_witness -> Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) → Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)). - Proof. - intros m c dr. - destruct (ch2prod dr) as [d2 r1]. - refine (prod2ch _). (* w, d1 *) - simpl. - refine (fto ((otf r1) + (m * (otf c - otf d2))), fto (otf d2)). - Defined. + Lemma f_d2r2_to_wd_bij : forall m c, bijective (f_d2r2_to_wd m c). + intros. + eapply (Bijective (g := fun dr => + let '(d2, r2) := (ch2prod dr) in + prod2ch (fto (otf c - otf r2), fto (otf d2 - (otf c - otf r2) * m)))). + - intros z. + unfold f_d2r2_to_wd. + rewrite <- prod2ch_ch2prod. + set (ch2prod _) at 2 3. + destruct s eqn:ch2z. + rewrite ch2prod_prod2ch. + rewrite !otf_fto. + f_equal. + rewrite subKr. + rewrite !fto_otf. + f_equal. + rewrite mulrC. + rewrite addrK. + rewrite !fto_otf. + reflexivity. + - intros z. + unfold f_d2r2_to_wd. + rewrite <- prod2ch_ch2prod. + set (ch2prod _) at 2 3. + destruct s eqn:ch2z. + rewrite ch2prod_prod2ch. + rewrite !otf_fto. + f_equal. + rewrite subKr. + rewrite !fto_otf. + f_equal. + rewrite mulrC. + rewrite subrK. + rewrite !fto_otf. + reflexivity. + Qed. - Lemma f_d1r1_to_wd_bij : forall m c, bijective (f_d1r1_to_wd m c). Admitted. + Definition f_d1r1_to_wd : 'Z_q -> 'I_MyAlg.i_witness -> Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) → Arit (uniform (MyAlg.i_witness * MyAlg.i_witness)) := + fun m c dr => + let '(d2, r1) := ch2prod dr in + prod2ch (fto ((otf r1) + (m * (otf c - otf d2))), fto (otf d2)). + + Lemma f_d1r1_to_wd_bij : forall m c, bijective (f_d1r1_to_wd m c). + intros. + eapply (Bijective (g := fun dr => + let '(d2, r2) := (ch2prod dr) in + prod2ch (r2, fto (otf d2 - m * (otf c - otf r2))))). + - intros z. + unfold f_d1r1_to_wd. + rewrite <- prod2ch_ch2prod. + set (ch2prod _) at -1. + destruct s eqn:ch2z. + rewrite ch2prod_prod2ch. + rewrite !fto_otf. + rewrite !otf_fto. + f_equal. + f_equal. + rewrite addrK. + rewrite !fto_otf. + reflexivity. + - intros z. + unfold f_d1r1_to_wd. + rewrite <- prod2ch_ch2prod. + set (ch2prod _) at -1. + destruct s eqn:ch2z. + rewrite ch2prod_prod2ch. + rewrite !fto_otf. + rewrite !otf_fto. + f_equal. + f_equal. + rewrite subrK. + rewrite !fto_otf. + reflexivity. + Qed. Lemma swap_samples : forall {n m : nat} {C} `{Positive n} `{Positive m} (c : 'I_n -> 'I_m -> raw_code C), @@ -2232,111 +2440,8 @@ Module OVN_or_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat } Qed. - Lemma prod_swap : (forall a b (x : gT) y, a * x ^+ y = b -> a = b * x ^- y). - Proof. - intros. - generalize dependent b. - generalize dependent a. - generalize dependent x. - induction y ; intros. - + rewrite expg0 in H |- *. - rewrite invg1. - now rewrite !mulg1 in H |- *. - + (* specialize (IHy x (a * x) b). *) - (* rewrite expgS in H. *) - (* rewrite mulgA in H. *) - (* specialize (IHy H) ; clear H. *) - rewrite expgSr. - rewrite invMg. - rewrite mulgA. - apply IHy. - rewrite <- H. - rewrite expgSr. - rewrite mulgA. - rewrite <- mulgA. - rewrite <- mulgA. - rewrite (mulgA (x ^+ y)). - rewrite mulgK. - reflexivity. - Qed. - - Lemma mulg_invg_cancel_r : (forall (x : gT) y, x ^+ y * x ^- y = 1). - Proof. - intros. - generalize dependent x. - induction y ; intros. - + rewrite expg0. - rewrite invg1. - now rewrite mulg1. - + rewrite expgSr. - rewrite invMg. - rewrite mulgA. - rewrite mulgK. - rewrite IHy. - reflexivity. - Qed. - - Lemma mulg_invg_cancel_l : (forall (x : gT) y, x ^- y * x ^+ y = 1). - Proof. - intros. - generalize dependent x. - induction y ; intros. - + rewrite expg0. - rewrite invg1. - now rewrite mulg1. - + rewrite expgS. - rewrite invMg. - rewrite <- mulgA. - rewrite mulKg. - rewrite IHy. - reflexivity. - Qed. - - Lemma prod_swap_iff : (forall a b (x : gT) y, a * x ^+ y = b <-> a = b * x ^- y). - Proof. - split ; intros. - - erewrite <- prod_swap. - + reflexivity. - + apply H. - - rewrite H. - rewrite <- mulgA. - rewrite mulg_invg_cancel_l. - now rewrite mulg1. - Qed. - - Lemma prod_swap_left : (forall a b (x : gT) y, x ^+ y * a = b -> a = x ^- y * b). - Proof. - intros. - generalize dependent b. - generalize dependent a. - generalize dependent x. - induction y ; intros. - + rewrite expg0 in H |- *. - rewrite invg1. - now rewrite !mul1g in H |- *. - + rewrite expgSr. - rewrite invMg. - rewrite <- mulgA. - rewrite <- IHy with (a := x * a). - 1: now rewrite mulKg. - rewrite mulgA. - rewrite <- expgSr. - apply H. - Qed. - - Lemma prod_swap_left_iff : (forall a b (x : gT) y, x ^+ y * a = b <-> a = x ^- y * b). - Proof. - split ; intros. - - erewrite <- prod_swap_left. - + reflexivity. - + apply H. - - rewrite H. - rewrite mulgA. - rewrite mulg_invg_cancel_r. - now rewrite mul1g. - Qed. - Lemma invg_id : (forall (x : gT), x ^-1 = x ^- 1). + Lemma invg_id : (forall (x : gT), x ^-1 = x ^- 1%R). Proof. reflexivity. Qed. Lemma trunc_extra : forall (h : gT), h ^+ (Zp_trunc q).+2 = 1. @@ -2345,100 +2450,75 @@ Module OVN_or_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat now rewrite modnn. Qed. - (* Lemma expg_neg : (forall (x : gT) (n : 'Z_q), x ^- n = x ^+ ((Zp_trunc q).+2 - n)). *) - (* Proof. *) - (* intros. *) - (* destruct n0 ; simpl. *) - (* induction m. *) - (* + rewrite subn0. *) - (* rewrite trunc_extra. *) - (* rewrite expg0. *) - (* rewrite invg1. *) - (* reflexivity. *) - (* + *) - (* Qed. *) + Lemma reverse_opp : (forall (x : gT) (n : 'Z_q), x ^+ ((Zp_trunc q).+2 - n) = x ^+ GRing.opp n). + Proof. now intros ; rewrite trunc_pow. Qed. - Lemma mulg_invg : (forall (x : gT) (y : 'Z_q), x ^+ y * x ^- 1 = x ^+ nat_of_ord (y - 1)). + Lemma neg_is_opp : (forall (x : gT) (n : 'Z_q), x ^- n = x ^+ GRing.opp n). Proof. - intros. - symmetry. - apply prod_swap. - - simpl. - + intros x n. rewrite trunc_pow. - rewrite expgD. - rewrite trunc_pow. - rewrite modn_small. - 2: easy. - rewrite <- expgD. - rewrite <- expgD. - rewrite <- addnA. - rewrite expgD. + destruct n as [n ?] ; simpl. + induction n. + - rewrite invg1. + rewrite subn0. + now rewrite trunc_extra. + - rewrite expgSr. + rewrite invMg. + rewrite IHn ; [ | easy ]. + rewrite subnS. + eapply canLR with (f := fun y => mulg (x^+1) y). + { + clear ; intros ?. + rewrite mulgA. + rewrite mulVg. + rewrite mul1g. + reflexivity. + } - rewrite addn1. - rewrite (trunc_extra). - rewrite mulg1. - reflexivity. + rewrite <- expgD. + rewrite addSn. + rewrite add0n. + set (subn _ _). + now rewrite (Nat.lt_succ_pred 0 n1). Qed. - Lemma mulg_invg_sub : (forall (x : gT) (y z : 'Z_q), (* (0 < y - z)%N -> *) x ^+ y * x ^- z = x ^+ nat_of_ord (y - z)). + Lemma mulg_cancel : forall (x : gT) (y : 'Z_q), + (cancel (mulg^~ (x ^+ y)) (mulg^~ (x ^- y)) + /\ cancel (mulg^~ (x ^- y)) (mulg^~ (x ^+ y))) + /\ (cancel (mulg (x ^+ y)) (mulg (x ^- y)) + /\ cancel (mulg (x ^- y)) (mulg (x ^+ y))). Proof. - intros. - destruct z as [z ?]. simpl in *. + now intros x y + ; repeat split + ; intros z + ; (rewrite <- mulgA || rewrite mulgA) + ; (rewrite mulgV || rewrite mulVg) + ; (rewrite mulg1 || rewrite mul1g). + Qed. - symmetry. - apply prod_swap_iff. - rewrite !trunc_pow. - rewrite !expgD. - rewrite !trunc_pow. - rewrite <- !expgD. - rewrite <- addnA. - rewrite subnK. - 2: easy. - rewrite !expgD. - rewrite trunc_extra. - rewrite mulg1. - reflexivity. + Lemma prod_swap_iff : (forall a b (x : gT) (y : 'Z_q), (a * x ^- y = b <-> a = b * x ^+ y) /\ (x ^- y * a = b <-> a = x ^+ y * b)). + Proof. + repeat split ; + [ eapply (canRL (f := mulg^~ _) (g := mulg^~ _)) + | eapply (canLR (f := mulg^~ _) (g := mulg^~ _)) + | eapply (canRL) + | eapply (canLR) ] ; apply (mulg_cancel x y). Qed. - Lemma mulg_invg_left_sub : (forall (x : gT) (y z : 'Z_q), (* (0 < y - z)%N -> *) x ^- y * x ^+ z = x ^+ nat_of_ord (z - y)). + Lemma mulg_invg_sub : (forall (x : gT) (y z : 'Z_q), x ^+ y * x ^- z = x ^+ nat_of_ord (y - z)). Proof. intros. - destruct z as [z ?]. simpl in *. - - symmetry. - apply prod_swap_left_iff. - rewrite !trunc_pow. - rewrite !expgD. - rewrite !trunc_pow. - rewrite <- !expgD. - rewrite addnC. - rewrite <- addnA. - rewrite subnK. - 2: easy. - rewrite !expgD. - rewrite trunc_extra. - rewrite mulg1. - reflexivity. + rewrite neg_is_opp. + rewrite <- expgD. + now rewrite trunc_pow. Qed. - - Lemma expg_sub : (forall (x : gT) (y : 'Z_q), (* (0 < y - z)%N -> *) x ^- y = x ^+ nat_of_ord (0 - y)). + Lemma mulg_invg_left_sub : (forall (x : gT) (y z : 'Z_q), x ^- y * x ^+ z = x ^+ nat_of_ord (z - y)). Proof. intros. - simpl. - rewrite !trunc_pow. - - rewrite <- mul1g. - symmetry. - apply prod_swap_iff. - symmetry. + rewrite neg_is_opp. rewrite <- expgD. - rewrite subnK. - 2: easy. - rewrite trunc_extra. - reflexivity. + now rewrite trunc_pow. Qed. Lemma cyclic_always_commute : forall (x y : gT), commute x y. @@ -2465,64 +2545,79 @@ Module OVN_or_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat apply commute_refl. Qed. - Lemma div_cancel : forall (x : gT) (s : 'Z_q), x ^+ nat_of_ord (s / s)%R = x. + Lemma div_cancel : forall (x : gT) (s : 'Z_q), s != 0 -> x ^+ nat_of_ord (s / s)%R = x. Proof. clear ; intros. - (* Set Printing Coercions. *) - (* epose proof (@mulrV _ s) ; simpl in H. *) - rewrite <- (FieldToWitnessCancel s). - setoid_rewrite (FieldToWitnessInv (ret_both (WitnessToField s))). - setoid_rewrite (FieldToWitnessMul). - rewrite WitnessToField_f_inv. - simpl. - rewrite <- WitnessToField_f_inv. - rewrite !(proj1 both_equivalence_is_pure_eq (mul_inv_cancel _)). - rewrite FieldToWitnessOne. + rewrite mulrV. + 2: apply all_unit_in_prime_field ; [apply prime_order | assumption ]. now rewrite expg1. Qed. - Lemma expg_div : (forall (x : gT) (y z : 'Z_q), x ^+ y ^- z = x ^+ (y / z)%R). - Proof. - intros. - destruct y. - induction m ; simpl (nat_of_ord (Ordinal _)). - - set (_ ^+ _). - rewrite expg_sub. - rewrite expgAC. - rewrite expg0. - unfold "/" ; simpl GRing.Nmodule_isSemiRing.mul. - simpl. - rewrite mul0n. - rewrite modn_small. - 2: easy. - now rewrite expg0. - - rewrite expg_sub. - rewrite expgAC. - rewrite expgS. - rewrite <- expgAC. - rewrite <- !expg_sub. - rewrite IHm. - 1: easy. - intros. - (* symmetry. *) - (* apply prod_swap_left_iff. *) - (* symmetry. *) - (* rewrite <- expgD. *) - - rewrite !trunc_pow. - rewrite !expgD. - rewrite !expgM. - simpl. - f_equal. + (* Lemma expg_div : (forall (x : gT) (y z : 'Z_q), x ^+ y ^- z = x ^+ (y / z)%R). *) + (* Proof. *) + (* intros. *) + (* destruct y. *) + (* induction m ; simpl (nat_of_ord (Ordinal _)). *) + (* - set (_ ^+ _). *) + (* rewrite expg_sub. *) + (* rewrite expgAC. *) + (* rewrite expg0. *) + (* unfold "/" ; simpl GRing.Nmodule_isSemiRing.mul. *) + (* simpl. *) + (* rewrite mul0n. *) + (* rewrite modn_small. *) + (* 2: easy. *) + (* now rewrite expg0. *) + (* - rewrite expg_sub. *) + (* rewrite expgAC. *) + (* rewrite expgS. *) + (* rewrite <- expgAC. *) + (* rewrite <- !expg_sub. *) + (* rewrite IHm. *) + (* 1: easy. *) + (* intros. *) + (* (* symmetry. *) *) + (* (* apply prod_swap_left_iff. *) *) + (* (* symmetry. *) *) + (* (* rewrite <- expgD. *) *) + + (* rewrite !trunc_pow. *) + (* rewrite !expgD. *) + (* rewrite !expgM. *) + (* simpl. *) - rewrite expg_sub. - simpl. - rewrite !trunc_pow. - Admitted. + (* epose (prod_swap_left_iff). *) + (* symmetry in i0. *) + (* symmetry. *) + (* apply i0. *) + (* rewrite mulgA. *) + (* replace (x ^+ (z^-1)%R) with (x ^- z). *) + (* 2:{ *) + (* epose canRL. *) + + (* unfold "^-1"%R. *) + (* simpl. *) + (* unfold "^-1". *) + (* simpl. *) + (* (* rewrite !trunc_pow. *) *) + (* (* rewrite !expgD. *) *) + (* rewrite !expgM. *) + + (* apply *) + (* } *) + (* rewrite <- expgD. *) + (* rewrite mulVr. *) + + (* f_equal. *) + + (* rewrite expg_sub. *) + (* simpl. *) + (* rewrite !trunc_pow. *) + (* Admitted. *) - (* Lemma proving that the output of the extractor defined for Schnorr's - protocol is perfectly indistinguishable from real protocol execution. - *) + (* Lemma proving that the output of the extractor defined for Schnorr's *) + (* protocol is perfectly indistinguishable from real protocol execution. *) + (* *) Lemma extractor_success: ∀ LA A, ValidPackage LA [interface @@ -2553,602 +2648,650 @@ Module OVN_or_proof (OVN_impl : Hacspec_ovn.HacspecOVNParams) (GOP : GroupOperat repeat (apply (ssrbool.elimT andP) in H0 ; destruct H0). repeat (apply (ssrbool.elimT andP) in H1 ; destruct H1). apply reflection_nonsense in H0, H6, H5, H4, H3, H1, H9, H8, H7, H2. - subst. - apply r_ret ; intros; split ; [ | assumption ]. - rewrite andb_true_intro ; [ easy | ]. - split. - - rewrite !(trunc_pow). + eassert (Hd2d1 : ld2 = otf e - ld1). + { + rewrite H0. + rewrite addrC. + rewrite addKr. + reflexivity. + } - clear -H7 H9. + eassert (H'd2d1 : rd2 = otf e' - rd1). + { + rewrite H1. + rewrite addrC. + rewrite addKr. + reflexivity. + } - apply prod_swap in H9, H7. - rewrite <- mulgA in H9, H7. + apply f_equal with (f := fto) in H0, H1. + rewrite !fto_otf in H0, H1. - rewrite !mulg_invg_sub in H9, H7. - symmetry in H9, H7. - apply prod_swap_left_iff in H9, H7. - rewrite !mulg_invg_left_sub in H9, H7. - assert (x ^+ ((rd1 - ld1) + (rd2 - ld2))%R = g ^+ ((lr1 - rr1) + (lr2 - rr2))%R). - { - simpl. - rewrite !trunc_pow. - rewrite !expgD. - rewrite !trunc_pow. - rewrite !expgD. - rewrite !trunc_pow. - - simpl in H7, H9. - rewrite !trunc_pow in H7, H9. - rewrite !expgD in H7, H9. - rewrite !trunc_pow in H7, H9. - rewrite H7 H9. - reflexivity. - } + subst la1 lb1 la2 lb2. - rewrite !expgM. - rewrite <- H. - rewrite <- !expgM. + apply r_ret ; intros; split ; [ | assumption ]. + symmetry. - set ( _ + _). + apply (proj1 (prod_swap_iff _ _ _ _)) in H9, H7, H8, H2. + rewrite <- mulgA in H9, H7, H8, H2. + + rewrite !mulg_invg_sub in H9, H7, H8, H2. + symmetry in H9, H7, H8, H2. + apply (proj2 (prod_swap_iff _ _ _ _)) in H9, H7, H8, H2. + rewrite !mulg_invg_left_sub in H9, H7, H8, H2. + + + (* assert (y ^+ (otf e - otf e')%R = h ^+ ((rr1 - lr1) + (rr2 - lr2))%R * g ^+ (ld2 - rd2)%R). *) + (* { *) + (* rewrite (trunc_pow h). *) + (* rewrite expgD. *) + (* rewrite H8. *) + (* rewrite H2. *) + (* rewrite (expgMn _ (cyclic_always_commute _ _)). *) + + (* rewrite mulgA. *) + (* rewrite <- mulgA. *) + (* rewrite expgVn. *) + (* rewrite neg_is_opp. *) + (* rewrite <- !expgD. *) + (* replace (g ^+ ((GRing.opp (_ - rd2))%R + (ld2 - rd2)%R)) with *) + (* (g ^+ (0 - (ld2 - rd2) + (ld2 - rd2))%R) by now rewrite trunc_pow ; rewrite sub0r. *) + (* rewrite subrK. *) + (* rewrite expg0. *) + (* rewrite mulg1. *) - replace (x ^+ _) - with (x ^+ ((s / s)%R)) by now rewrite !trunc_pow. - - (* Set Printing Coercions. *) - rewrite div_cancel. - apply eqxx. - - clear -H8 H2. - rename H8 into H9. - rename H2 into H7. - - apply prod_swap in H9, H7. - rewrite <- mulgA in H9, H7. - - rewrite !mulg_invg_sub in H9, H7. - symmetry in H9, H7. - apply prod_swap_left_iff in H9, H7. - rewrite !mulg_invg_left_sub in H9, H7. - assert (y ^+ nat_of_ord (rd1 - ld1) * (y * g^-1) ^+ nat_of_ord (rd2 - ld2) = h ^+ nat_of_ord (lr1 - rr1) * h ^+ nat_of_ord (lr2 - rr2)). - { - rewrite !trunc_pow. - rewrite !expgD. - rewrite !trunc_pow. - - simpl in H7, H9. - rewrite !trunc_pow in H7, H9. - rewrite !expgD in H7, H9. - rewrite !trunc_pow in H7, H9. - rewrite H7 H9. - reflexivity. - } - clear H7 H9. - - change (y == _ * g) with (y == h ^+ nat_of_ord ((lr1 - rr1 + (lr2 - rr2)) / (rd1 - ld1 + (rd2 - ld2))) * g). - - destruct (y == h ^+ nat_of_ord ((lr1 - rr1 + (lr2 - rr2)) / (rd1 - ld1 + (rd2 - ld2))) * g) eqn:yhg. - + apply reflection_nonsense in yhg. - rewrite yhg. - apply eqxx. - + exfalso. - refine (Bool.eq_true_false_abs _ _ yhg) ; clear yhg. - rewrite !(trunc_pow). - rewrite !expgM. - - rewrite !(trunc_pow). - rewrite !expgD. - rewrite <- H. - do 3 rewrite (expgMn _ (cyclic_always_commute _ _)). - rewrite mulgA. - rewrite expgVn. - rewrite <- !expgM. - rewrite <- expgD. - - replace (y ^+ ((_ * _)%R + (_ * _)%R)) with (y - ^+ nat_of_ord ((rd1 - ld1) * ((rd1 - ld1 + (rd2 - ld2))^-1)%R + - (rd2 - ld2) * ((rd1 - ld1 + (rd2 - ld2))^-1)%R)). - 2:{ - rewrite !(trunc_pow). - rewrite !expgD. - rewrite !(trunc_pow). - reflexivity. - } - replace (y ^+ _) with y. - 2:{ - setoid_rewrite <- (GRing.mulrDl (rd1 - ld1) (rd2 - ld2) (GRing.inv (rd1 - ld1 + (rd2 - ld2)))). - now rewrite div_cancel. - } - - rewrite <- (expg1 y) at 2. - apply (ssrbool.introT eqP). - symmetry. - rewrite <- mulgA. - apply prod_swap_left_iff. - rewrite mulVg. - - Admitted. - -End OVN_or_proof. - -(*** Example (Z89) *) - -From OVN Require Import Hacspec_ovn_Ovn_z_89_. - -Module Z89_impl <: HacspecOVNParams. - #[local] Open Scope hacspec_scope. - - Definition v_G : choice_type := t_g_z_89_. - Transparent v_G. - Hint Unfold v_G. - - Definition n : both uint_size := ret_both 55. - - Instance Serializable_chFin (n : positive) : Serializable.Serializable (chFin n). - Proof. - destruct n as [[] ?] ; [ discriminate | ]. - refine (serialize_by_other (fun x => nat_of_ord x) (fun x => inord x) (inord_val)). - apply Serializable.nat_serializable. - Defined. - - Instance v_Z_t_Field : t_Field _ := t_z_89__t_Field. - (* Instance t_Eq_from_eqType (A : eqType) : t_Eq A := *) - (* {| Hacspec_Lib_Comparable.eqb := fun x y => x == y; eqb_leibniz := fun x y => RelationClasses.symmetry (rwP eqP) |}. *) - (* Instance v_G_t_Eq : t_Eq v_G := _. *) + (* rewrite H'd2d1 Hd2d1. *) + (* replace ((otf _ - ld1 - (otf e' - rd1))%R) with *) + (* ((rd1 - ld1) + (otf e - otf e'))%R. *) + (* 2:{ *) + (* rewrite (addrC (otf e) (GRing.opp ld1)). *) + (* rewrite <- (addrC (GRing.opp ld1)). *) + (* rewrite <- !addrA. *) + (* f_equal. *) + (* symmetry. *) + (* apply /eqP. *) + (* rewrite subr_eq. *) + (* apply /eqP. *) + (* rewrite <- addrA. *) + (* rewrite (addrC rd1). *) + (* rewrite <- addrA. *) + (* rewrite subrK. *) + (* now rewrite subrK. *) + (* } *) + (* (* rewrite !trunc_pow. *) *) + (* rewrite !expgD. *) + (* apply prod_swap_iff. *) + + (* rewrite neg_is_opp. *) + (* rewrite opprB. *) + (* rewrite <- !expgD. *) + (* rewrite !trunc_pow. *) + (* reflexivity. *) + (* } *) + + assert (x ^+ ((ld1 - rd1) + (ld2 - rd2))%R = g ^+ ((rr1 - lr1) + (rr2 - lr2))%R). + { + rewrite !(trunc_pow). + rewrite !(expgD). - Instance v_G_t_Copy : t_Copy v_G := _. - Instance v_G_t_PartialEq : t_PartialEq v_G v_G := _. - Instance v_G_t_Clone : t_Clone v_G := _. - Instance v_G_t_Serialize : t_Serialize v_G := _. - Instance v_G_t_Eq : t_Eq v_G := _. + setoid_rewrite <- H7. + setoid_rewrite <- H9. + reflexivity. + } + clear H7 H9. - Instance v_G_t_Group : t_Group v_G := t_g_z_89__t_Group. + assert (y ^+ ((ld1 - rd1) + (ld2 - rd2))%R (* * g ^- nat_of_ord (ld2 - rd2) *) = h ^+ ((rr1 - lr1)%R + (rr2 - lr2)%R)%R). + { + rewrite !(trunc_pow y). + rewrite !(trunc_pow h). + rewrite !(expgD h). + setoid_rewrite H8. + setoid_rewrite H2. + + (* rewrite (expgMn _ (cyclic_always_commute _ _)). *) + (* rewrite mulgA. *) + rewrite expgD. + (* rewrite expgVn. *) + reflexivity. + } + clear H8 H2. - Definition v_A : choice_type := 'nat. - Instance v_A_t_Sized : t_Sized v_A. Admitted. - Definition v_A_t_HasActions : t_HasActions v_A. - Proof. - constructor. - refine (ret_both (0%nat : 'nat)). - Defined. + replace + (y == + h ^+ _ * g) with + (y == + h ^+ ((rr1 - lr1 + (rr2 - lr2)) / + (ld1 - rd1 + (ld2 - rd2)))%R * g) by + now rewrite !(trunc_pow). - Instance f_field_type_Serializable : Serializable.Serializable v_G_t_Group.(f_Z). Admitted. - Instance f_group_type_Serializable : Serializable.Serializable v_G. Admitted. + rewrite !(trunc_pow). + rewrite !expgM. -End Z89_impl. + rewrite <- H4. + rewrite <- H5. -Module Z89_group_operations <: GroupOperationProperties Z89_impl. - Include Z89_impl. + (* rewrite (expgMn _ (cyclic_always_commute _ _)). *) + rewrite <- !expgM. - Ltac unfold_both_eq := - intros ; - apply both_equivalence_is_pure_eq ; - cbn ; - repeat (try unfold lift2_both at 1 ; try unfold lift1_both at 1 ; simpl). + set ( _ + _). -(* (a + b) + c = a + (b + c) *) + replace (x ^+ _) + with (x ^+ ((s / s)%R)) by now rewrite !trunc_pow. + replace (y ^+ _) + with (y ^+ ((s / s)%R)) by now rewrite !trunc_pow. - Corollary both_equivalence_bind_comm : forall {A} {a : both A} {b : both A} {f : A -> A -> both A}, - bind_both a (fun x => - bind_both b (fun y => f x y)) - ≈both - bind_both b (fun y => bind_both a (fun x => f x y)) - . - Proof. - intros. - cbn. - unfold both_equivalence. - now rewrite <- both_pure. + assert (s != 0). + { + subst s e e'. + clear -H. + apply /eqP. + intros ?. + assert (fto (ld1 + ld2) = fto (rd1 + rd2)). + 2:{ + rewrite H1 in H. + rewrite eqxx in H. + discriminate. + } + f_equal. + apply /eqP. + setoid_rewrite <- (subr_eq (ld1 + ld2) rd1 rd2). + rewrite <- addrA. + rewrite addrC. + rewrite <- (add0r rd1). + setoid_rewrite <- subr_eq. + rewrite <- addrA. + rewrite addrC. + apply /eqP. + apply H0. + } + rewrite !div_cancel ; [ | assumption ..]. + rewrite mulg1. + now rewrite !eqxx. Qed. - Lemma f_sub_by_opp : forall x y, f_sub x y ≈both f_add x (f_opp y). - Proof. Admitted. - (* intros. *) - (* simpl. *) - - (* repeat unfold Build_t_z_89_ at 1. *) - - (* repeat unfold f_z_val at 1. *) - (* repeat unfold ".-" at 1. *) - (* repeat unfold ".+" at 1. *) - (* repeat unfold ".%" at 1. *) - (* unfold_both_eq. *) - - (* Set Printing Coercions. *) - - (* set (x' := is_pure _). *) - (* set (y' := is_pure _). *) - - (* set (int_xO _); change (Hacspec_Lib_Pre.int_sub (int_xI s) _) with (@int_xO U8 s); subst s. *) - (* set (n88 := int_xO _). *) - - (* replace (wrepr U8 0) with (Hacspec_Lib_Pre.zero (WS := U8)). *) - (* 2: admit. *) - (* rewrite add_zero_l. *) - - - - (* rewrite !add_repr. *) + (* Require Import mathcomp.algebra.all_algebra. *) +End OVN_or_proof. +(*** Example (Z89) *) - (* replace (Hacspec_Lib_Pre.int_sub 89 1) with *) - (* (88). *) +(* From OVN Require Import Hacspec_ovn_Ovn_z_89_. *) - (* unfold Hacspec_Lib_Pre.int_sub. *) - (* unfold Hacspec_Lib_Pre.int_add. *) - (* unfold Hacspec_Lib_Pre.int_mod. *) +(* Module Z89_impl <: HacspecOVNParams. *) +(* #[local] Open Scope hacspec_scope. *) - (* (* unfold wrepr. *) *) - (* (* set (unsigned _ mod _) ; fold (wrepr U8 z) ; subst z. *) *) - (* (* set (unsigned _ mod _) at 2 ; fold (wrepr U8 z) ; subst z. *) *) +(* Definition v_G : choice_type := t_g_z_89_. *) +(* Transparent v_G. *) +(* Hint Unfold v_G. *) - (* assert (forall x, wrepr U8 (urepr x) = x) by apply ureprK. *) +(* Definition n : both uint_size := ret_both 55. *) - (* unfold unsigned. *) - (* unfold sub_word. *) +(* Instance Serializable_chFin (n : positive) : Serializable.Serializable (chFin n). *) +(* Proof. *) +(* destruct n as [[] ?] ; [ discriminate | ]. *) +(* refine (serialize_by_other (fun x => nat_of_ord x) (fun x => inord x) (inord_val)). *) +(* apply Serializable.nat_serializable. *) +(* Defined. *) + +(* Instance v_Z_t_Field : t_Field _ := t_z_89__t_Field. *) +(* (* Instance t_Eq_from_eqType (A : eqType) : t_Eq A := *) *) +(* (* {| Hacspec_Lib_Comparable.eqb := fun x y => x == y; eqb_leibniz := fun x y => RelationClasses.symmetry (rwP eqP) |}. *) *) +(* (* Instance v_G_t_Eq : t_Eq v_G := _. *) *) + +(* Instance v_G_t_Copy : t_Copy v_G := _. *) +(* Instance v_G_t_PartialEq : t_PartialEq v_G v_G := _. *) +(* Instance v_G_t_Clone : t_Clone v_G := _. *) +(* Instance v_G_t_Serialize : t_Serialize v_G := _. *) +(* Instance v_G_t_Eq : t_Eq v_G := _. *) + +(* Instance v_G_t_Group : t_Group v_G := t_g_z_89__t_Group. *) + +(* Definition v_A : choice_type := 'nat. *) +(* Instance v_A_t_Sized : t_Sized v_A. Admitted. *) +(* Definition v_A_t_HasActions : t_HasActions v_A. *) +(* Proof. *) +(* constructor. *) +(* refine (ret_both (0%nat : 'nat)). *) +(* Defined. *) - (* (* unfold wrepr. *) *) - (* change (nat_of_wsize U8) with (wsize_size_minus_1 U8).+1. *) - (* set (z := urepr _ - _) ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 2 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 3 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 4 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 5 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 6 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ - _) at 7 ; fold (wrepr U8 z) ; subst z. *) +(* Instance f_field_type_Serializable : Serializable.Serializable v_G_t_Group.(f_Z). Admitted. *) +(* Instance f_group_type_Serializable : Serializable.Serializable v_G. Admitted. *) - (* set (int_xO _); change (urepr (int_xI s) - _) with (urepr (@int_xO U8 s)); subst s. *) - (* set (n88 := int_xO _). *) +(* End Z89_impl. *) - (* unfold add_word. *) - (* set (z := urepr _ + _) ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ + _) at 2 ; fold (wrepr U8 z) ; subst z. *) - (* set (z := urepr _ + _) at 3 ; fold (wrepr U8 z) ; subst z. *) - (* rewrite !H. *) +(* Module Z89_group_operations <: GroupOperationProperties Z89_impl. *) +(* Include Z89_impl. *) - (* rewrite wrepr_add. *) - (* rewrite !H. *) +(* Ltac unfold_both_eq := *) +(* intros ; *) +(* apply both_equivalence_is_pure_eq ; *) +(* cbn ; *) +(* repeat (try unfold lift2_both at 1 ; try unfold lift1_both at 1 ; simpl). *) - (* rewrite wrepr_sub. *) - (* rewrite !H. *) +(* (* (a + b) + c = a + (b + c) *) *) - (* set (urepr _). *) - (* set (urepr _). *) +(* Corollary both_equivalence_bind_comm : forall {A} {a : both A} {b : both A} {f : A -> A -> both A}, *) +(* bind_both a (fun x => *) +(* bind_both b (fun y => f x y)) *) +(* ≈both *) +(* bind_both b (fun y => bind_both a (fun x => f x y)) *) +(* . *) +(* Proof. *) +(* intros. *) +(* cbn. *) +(* unfold both_equivalence. *) +(* now rewrite <- both_pure. *) +(* Qed. *) - (* Admitted. *) +(* Lemma f_sub_by_opp : forall x y, f_sub x y ≈both f_add x (f_opp y). *) +(* Proof. Admitted. *) +(* (* intros. *) *) +(* (* simpl. *) *) - Lemma f_addA : forall x y z, f_add x (f_add y z) ≈both f_add (f_add x y) z. - Admitted. - (* Proof. unfold_both_eq. now rewrite Zp_addA. Qed. *) +(* (* repeat unfold Build_t_z_89_ at 1. *) *) - Lemma f_addC: forall x y, f_add x y ≈both f_add y x. - Proof. Admitted. - (* Proof. unfold_both_eq. now rewrite Zp_addC. Qed. *) - (* Axiom f_mul_addr: right_distributive (f_mul) (f_add). *) - (* Axiom f_mul_addl: left_distributive (f_mul) (f_add). *) - Lemma f_add0z: forall x, f_add f_field_zero x ≈both x. - Proof. Admitted. - (* Proof. *) - (* unfold_both_eq. *) - (* replace (inord _) with (Zp0 (p' := 88 (* 89 *))) by now apply ord_inj ; rewrite inordK. *) - (* now rewrite Zp_add0z. *) - (* Qed. *) +(* (* repeat unfold f_z_val at 1. *) *) +(* (* repeat unfold ".-" at 1. *) *) +(* (* repeat unfold ".+" at 1. *) *) +(* (* repeat unfold ".%" at 1. *) *) +(* (* unfold_both_eq. *) *) - Lemma f_addNz: forall x, f_add (f_opp x) x ≈both f_field_zero. - Proof. Admitted. - (* Proof. *) - (* unfold_both_eq. *) - (* replace (inord _) with (Zp0 (p' := (* 89 *) 88)) by now apply ord_inj ; rewrite inordK. *) - (* rewrite Zp_add0z. *) - (* now rewrite Zp_addNz. *) - (* Qed. *) - - (* Lemma nat_of_ord_helper : *) - (* (forall (a b : v_G), (nat_of_ord a * nat_of_ord b)%nat = nat_of_ord (a * b)). *) - (* Admitted. *) +(* (* Set Printing Coercions. *) *) - Definition prod_pow_add_mul : ∀ x y z : both f_Z, f_prod (f_g_pow x) (f_pow (f_g_pow z) y) ≈both f_g_pow (f_add x (f_mul z y)). - Proof. Admitted. - (* Proof. *) - (* unfold_both_eq ; repeat setoid_rewrite <- expgnE. *) +(* (* set (x' := is_pure _). *) *) +(* (* set (y' := is_pure _). *) *) - (* (* unfold Zp_mul. *) *) - (* (* rewrite nat_of_ord_helper. *) *) +(* (* set (int_xO _); change (Hacspec_Lib_Pre.int_sub (int_xI s) _) with (@int_xO U8 s); subst s. *) *) +(* (* set (n88 := int_xO _). *) *) - (* (* rewrite modZp. *) *) +(* (* replace (wrepr U8 0) with (Hacspec_Lib_Pre.zero (WS := U8)). *) *) +(* (* 2: admit. *) *) +(* (* rewrite add_zero_l. *) *) - (* unfold expgn at 1, expgn_rec. *) - (* unfold Zp_mul. *) - (* unfold expgn at 1, expgn_rec. *) - (* Admitted. *) - Definition prod_pow_pow : forall h x a b, f_prod (f_pow h x) (f_pow (f_pow h a) b) ≈both f_pow h (f_add x (f_mul a b)). - Proof. Admitted. - (* intros. *) - (* unfold_both_eq ; repeat setoid_rewrite <- expgnE. *) - (* Set Printing Coercions. *) - (* (* unfold Zp_mul. *) *) - (* set (h' := is_pure (both_prog _)). *) - (* set (x' := nat_of_ord _). *) - (* set (a' := nat_of_ord _). *) - (* set (b' := nat_of_ord _). *) +(* (* rewrite !add_repr. *) *) - (* unfold Zp_mul. *) - (* rewrite nat_of_ord_helper. *) - (* rewrite valZpK. *) - (* rewrite <- expgM. *) - (* rewrite <- expgD. *) +(* (* replace (Hacspec_Lib_Pre.int_sub 89 1) with *) *) +(* (* (88). *) *) - (* (* f_equal. *) *) +(* (* unfold Hacspec_Lib_Pre.int_sub. *) *) +(* (* unfold Hacspec_Lib_Pre.int_add. *) *) +(* (* unfold Hacspec_Lib_Pre.int_mod. *) *) - (* rewrite <- modnDm. *) - (* rewrite modn_mod. *) - (* rewrite modnDm. *) +(* (* (* unfold wrepr. *) *) *) +(* (* (* set (unsigned _ mod _) ; fold (wrepr U8 z) ; subst z. *) *) *) +(* (* (* set (unsigned _ mod _) at 2 ; fold (wrepr U8 z) ; subst z. *) *) *) - (* rewrite expg_mod ; [reflexivity | ]. *) +(* (* assert (forall x, wrepr U8 (urepr x) = x) by apply ureprK. *) *) - (* apply ord_inj. *) - (* simpl. *) +(* (* unfold unsigned. *) *) +(* (* unfold sub_word. *) *) - (* destruct h' ; simpl. *) - (* repeat (discriminate || (destruct m as [ | m ] ; [ reflexivity | ])). (* SLOW *) *) - (* Qed. *) +(* (* (* unfold wrepr. *) *) *) +(* (* change (nat_of_wsize U8) with (wsize_size_minus_1 U8).+1. *) *) +(* (* set (z := urepr _ - _) ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 2 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 3 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 4 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 5 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 6 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ - _) at 7 ; fold (wrepr U8 z) ; subst z. *) *) - Definition div_prod_cancel : forall x y, f_div (f_prod x y) y ≈both x. Admitted. +(* (* set (int_xO _); change (urepr (int_xI s) - _) with (urepr (@int_xO U8 s)); subst s. *) *) +(* (* set (n88 := int_xO _). *) *) - Definition mul_comm : forall x y, f_mul x y ≈both f_mul y x. Admitted. +(* (* unfold add_word. *) *) +(* (* set (z := urepr _ + _) ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ + _) at 2 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* set (z := urepr _ + _) at 3 ; fold (wrepr U8 z) ; subst z. *) *) +(* (* rewrite !H. *) *) - (* HB.instance Definition sort_group : hasChoice (Choice.sort (chElement v_G)) := _. (* Choice.clone (Choice.sort (chElement v_G)) _. *) *) +(* (* rewrite wrepr_add. *) *) +(* (* rewrite !H. *) *) - (* HB.instance Definition Choice_choice : Choice v_G := _. *) - Definition v_G_countable : Choice_isCountable (Choice.sort (chElement v_G)) := [ Countable of v_G by <: ]. - Definition v_G_isFinite : isFinite (Choice.sort (chElement v_G)). - Proof. Admitted. - (* [ Finite of v_G by <: ]. *) +(* (* rewrite wrepr_sub. *) *) +(* (* rewrite !H. *) *) - Definition v_Z_countable : Choice_isCountable (Choice.sort (chElement v_G_t_Group.(f_Z))) := [ Countable of v_G_t_Group.(f_Z) by <: ]. - Definition v_Z_isFinite : isFinite (Choice.sort (chElement v_G_t_Group.(f_Z))). - Proof. Admitted. - (* [ Finite of v_G_t_Group.(f_Z) by <: ]. *) +(* (* set (urepr _). *) *) +(* (* set (urepr _). *) *) - Definition f_prodA : associative (lower2 f_prod). Admitted. - Definition f_prod1 : associative (lower2 f_prod). Admitted. - Definition f_prod_left_id : left_id (is_pure f_group_one) (lower2 f_prod). Admitted. - Definition f_invK : involutive (lower1 f_inv). Admitted. - Definition f_invM : {morph (lower1 f_inv) : x y / (lower2 f_prod) x y >-> (lower2 f_prod) y x}. Admitted. +(* (* Admitted. *) *) - Definition v_Z_Field : GRing.Field (v_G_t_Group.(f_Z)). Admitted. +(* Lemma f_addA : forall x y z, f_add x (f_add y z) ≈both f_add (f_add x y) z. *) +(* Admitted. *) +(* (* Proof. unfold_both_eq. now rewrite Zp_addA. Qed. *) *) + +(* Lemma f_addC: forall x y, f_add x y ≈both f_add y x. *) +(* Proof. Admitted. *) +(* (* Proof. unfold_both_eq. now rewrite Zp_addC. Qed. *) *) +(* (* Axiom f_mul_addr: right_distributive (f_mul) (f_add). *) *) +(* (* Axiom f_mul_addl: left_distributive (f_mul) (f_add). *) *) +(* Lemma f_add0z: forall x, f_add f_field_zero x ≈both x. *) +(* Proof. Admitted. *) +(* (* Proof. *) *) +(* (* unfold_both_eq. *) *) +(* (* replace (inord _) with (Zp0 (p' := 88 (* 89 *))) by now apply ord_inj ; rewrite inordK. *) *) +(* (* now rewrite Zp_add0z. *) *) +(* (* Qed. *) *) - Definition prod_inv_cancel : forall x, f_prod (f_inv x) x ≈both f_group_one. Admitted. +(* Lemma f_addNz: forall x, f_add (f_opp x) x ≈both f_field_zero. *) +(* Proof. Admitted. *) +(* (* Proof. *) *) +(* (* unfold_both_eq. *) *) +(* (* replace (inord _) with (Zp0 (p' := (* 89 *) 88)) by now apply ord_inj ; rewrite inordK. *) *) +(* (* rewrite Zp_add0z. *) *) +(* (* now rewrite Zp_addNz. *) *) +(* (* Qed. *) *) + +(* (* Lemma nat_of_ord_helper : *) *) +(* (* (forall (a b : v_G), (nat_of_ord a * nat_of_ord b)%nat = nat_of_ord (a * b)). *) *) +(* (* Admitted. *) *) + +(* Definition prod_pow_add_mul : ∀ x y z : both f_Z, f_prod (f_g_pow x) (f_pow (f_g_pow z) y) ≈both f_g_pow (f_add x (f_mul z y)). *) +(* Proof. Admitted. *) +(* (* Proof. *) *) +(* (* unfold_both_eq ; repeat setoid_rewrite <- expgnE. *) *) -End Z89_group_operations. +(* (* (* unfold Zp_mul. *) *) *) +(* (* (* rewrite nat_of_ord_helper. *) *) *) -Module Z89_secure_group <: SecureGroup Z89_impl Z89_group_operations. - Module Group := HacspecGroup Z89_impl Z89_group_operations. - Include Group. +(* (* (* rewrite modZp. *) *) *) - (* Lemma prime_q : prime (nat_of_ord (is_pure f_q)). *) - (* Proof. *) - (* rewrite inordK. *) - (* simpl. *) - (* Qed. *) +(* (* unfold expgn at 1, expgn_rec. *) *) +(* (* unfold Zp_mul. *) *) +(* (* unfold expgn at 1, expgn_rec. *) *) +(* (* Admitted. *) *) - (* Lemma prime_g : prime (nat_of_ord (is_pure f_g)). *) - (* Proof. now rewrite inordK. Qed. *) +(* Definition prod_pow_pow : forall h x a b, f_prod (f_pow h x) (f_pow (f_pow h a) b) ≈both f_pow h (f_add x (f_mul a b)). *) +(* Proof. Admitted. *) +(* (* intros. *) *) +(* (* unfold_both_eq ; repeat setoid_rewrite <- expgnE. *) *) +(* (* Set Printing Coercions. *) *) +(* (* (* unfold Zp_mul. *) *) *) - Lemma lower2_cancel_lift2_both : forall {A B C : choice_type} (f : A -> B -> C) x y, lower2 (lift2_both f) x y = f x y. - Proof. reflexivity. Qed. +(* (* set (h' := is_pure (both_prog _)). *) *) +(* (* set (x' := nat_of_ord _). *) *) +(* (* set (a' := nat_of_ord _). *) *) +(* (* set (b' := nat_of_ord _). *) *) - Lemma v_G_prime_order : prime #[(is_pure f_g : v_G_is_group)]. - simpl. - Admitted. - (* Proof. *) - (* intros. *) - (* simpl. *) - (* (* replace (inord 1) with (inord 89). *) *) - (* (* pose (order_Zp1 88). *) *) - (* (* unfold Zp1 in e. *) *) - (* epose order1. *) - (* Set Printing All. *) - (* replace (inZp _) with (inord (n' := 88) 1) in e. *) - (* - rewrite order1. *) - (* rewrite order1 in e. *) - (* Set Printing All. *) - - (* unfold v_G_is_group. *) - (* simpl. *) - (* unfold order. *) - (* simpl. *) - (* rewrite e. *) - (* easy. *) - (* - apply ord_inj; now rewrite inordK. *) - (* Qed. *) +(* (* unfold Zp_mul. *) *) +(* (* rewrite nat_of_ord_helper. *) *) +(* (* rewrite valZpK. *) *) - Lemma v_G_g_gen : [set : v_G_is_group] = <[ is_pure f_g : v_G_is_group]>. Admitted. -End Z89_secure_group. +(* (* rewrite <- expgM. *) *) +(* (* rewrite <- expgD. *) *) -(* Module OVN_schnorr_proof_params_Z89 <: OVN_schnorr_proof_preconditions Z89_impl Z89_group_operations Z89_secure_group. *) -(* Include Z89_secure_group. *) +(* (* (* f_equal. *) *) *) -(* Module HacspecGroup := HacspecGroupParam Z89_impl Z89_group_operations Z89_secure_group. *) -(* Module Schnorr := Schnorr HacspecGroup. *) +(* (* rewrite <- modnDm. *) *) +(* (* rewrite modn_mod. *) *) +(* (* rewrite modnDm. *) *) -(* Import Schnorr.MyParam. *) -(* Import Schnorr.MyAlg. *) +(* (* rewrite expg_mod ; [reflexivity | ]. *) *) -(* Import Schnorr.Sigma.Oracle. *) -(* Import Schnorr.Sigma. *) +(* (* apply ord_inj. *) *) +(* (* simpl. *) *) -(* Definition StatementToGroup : Statement -> v_G := id. *) +(* (* destruct h' ; simpl. *) *) +(* (* repeat (discriminate || (destruct m as [ | m ] ; [ reflexivity | ])). (* SLOW *) *) *) +(* (* Qed. *) *) -(* (* Lemma group_size : #[HacspecGroup.g].-2.+2 = 89. *) *) -(* (* Proof. *) *) -(* (* rewrite totient_gen. *) *) -(* (* epose (@generator_order v_G_is_group (is_pure f_g) (1)). *) *) -(* (* rewrite e. *) *) -(* (* 2:{ *) *) -(* (* simpl. *) *) -(* (* pose (cycle_generator). *) *) -(* (* unfold generator. *) *) -(* (* reflexivity. *) *) -(* (* epose (@generator_cycle v_G_is_group (is_pure f_g)). *) *) -(* (* simpl in i. *) *) -(* (* unfold generator in i. *) *) - -(* (* assert (HacspecGroup.g = inZp 1). *) *) -(* (* { *) *) -(* (* unfold inZp. *) *) -(* (* unfold HacspecGroup.g. *) *) -(* (* simpl. *) *) -(* (* unfold inord. *) *) -(* (* unfold ord0. *) *) -(* (* unfold insubd. *) *) -(* (* unfold insub. *) *) -(* (* unfold odflt. *) *) -(* (* unfold oapp. *) *) -(* (* unfold sub. *) *) -(* (* destruct idP. *) *) -(* (* - simpl. *) *) +(* Definition div_prod_cancel : forall x y, f_div (f_prod x y) y ≈both x. Admitted. *) +(* Definition mul_comm : forall x y, f_mul x y ≈both f_mul y x. Admitted. *) -(* (* simpl. *) *) +(* (* HB.instance Definition sort_group : hasChoice (Choice.sort (chElement v_G)) := _. (* Choice.clone (Choice.sort (chElement v_G)) _. *) *) *) -(* (* simpl. *) *) +(* (* HB.instance Definition Choice_choice : Choice v_G := _. *) *) +(* Definition v_G_countable : Choice_isCountable (Choice.sort (chElement v_G)) := [ Countable of v_G by <: ]. *) +(* Definition v_G_isFinite : isFinite (Choice.sort (chElement v_G)). *) +(* Proof. Admitted. *) +(* (* [ Finite of v_G by <: ]. *) *) +(* Definition v_Z_countable : Choice_isCountable (Choice.sort (chElement v_G_t_Group.(f_Z))) := [ Countable of v_G_t_Group.(f_Z) by <: ]. *) +(* Definition v_Z_isFinite : isFinite (Choice.sort (chElement v_G_t_Group.(f_Z))). *) +(* Proof. Admitted. *) +(* (* [ Finite of v_G_t_Group.(f_Z) by <: ]. *) *) -(* (* cbn. *) *) -(* (* rewrite card_Aut_cycle. *) *) -(* (* reflexivity. *) *) +(* Definition f_prodA : associative (lower2 f_prod). Admitted. *) +(* Definition f_prod1 : associative (lower2 f_prod). Admitted. *) +(* Definition f_prod_left_id : left_id (is_pure f_group_one) (lower2 f_prod). Admitted. *) +(* Definition f_invK : involutive (lower1 f_inv). Admitted. *) +(* Definition f_invM : {morph (lower1 f_inv) : x y / (lower2 f_prod) x y >-> (lower2 f_prod) y x}. Admitted. *) -(* Lemma inord_is_inZp : forall {n} x, (x < n.+1)%nat -> inord (n' := n) x = inZp (p' := n) x. *) -(* Proof. *) -(* intros n x H. *) -(* rewrite <- (inordK (m := x) (n' := n)) ; [ | assumption ]. *) -(* rewrite (valZpK (inord (n' := n) x)). *) -(* rewrite inord_val. *) -(* reflexivity. *) -(* Qed. *) +(* Definition v_Z_Field : GRing.Field (v_G_t_Group.(f_Z)). Admitted. *) -(* Definition WitnessToField : Witness -> v_G_t_Group.(f_Z) := fun x => mkword _ (Z.of_nat ((nat_of_ord x) %% Schnorr.q)). *) -(* Definition FieldToWitness : v_G_t_Group.(f_Z) -> Witness := fun x => inord ((Z.to_nat (unsigned x)) %% Schnorr.q). *) +(* Definition prod_inv_cancel : forall x, f_prod (f_inv x) x ≈both f_group_one. Admitted. *) -(* Lemma group_size_is_q : (Schnorr.q = Z.to_nat (unsigned (is_pure (HacspecGroup.v_G_t_Group.(f_Z_t_Field).(f_q))))). *) -(* Admitted. *) +(* End Z89_group_operations. *) +(* Module Z89_secure_group <: SecureGroup Z89_impl Z89_group_operations. *) +(* Module Group := HacspecGroup Z89_impl Z89_group_operations. *) +(* Include Group. *) -(* Lemma in_equality : forall v u, is_true (0 <= v < u)%R <-> is_true (Z.to_nat v < Z.to_nat u)%N. *) -(* Admitted. *) +(* (* Lemma prime_q : prime (nat_of_ord (is_pure f_q)). *) *) +(* (* Proof. *) *) +(* (* rewrite inordK. *) *) +(* (* simpl. *) *) +(* (* Qed. *) *) -(* Lemma WitnessToFieldCancel : forall x, WitnessToField (FieldToWitness x) = x. *) -(* Proof. *) -(* intros. *) -(* simpl in *. *) +(* (* Lemma prime_g : prime (nat_of_ord (is_pure f_g)). *) *) +(* (* Proof. now rewrite inordK. Qed. *) *) -(* destruct x. *) -(* unfold WitnessToField, FieldToWitness. *) -(* simpl. *) -(* rewrite !inordK. *) -(* 2:{ *) -(* simpl. *) -(* rewrite Schnorr.order_ge1. *) -(* simpl. *) -(* Set Printing Coercions. *) -(* unfold unsigned. *) -(* unfold urepr. *) -(* simpl. *) - -(* apply ltn_pmod. *) -(* now rewrite group_size_is_q. *) -(* } *) -(* apply word_ext. *) -(* rewrite modn_mod. *) -(* rewrite modnZE ; [ | now rewrite group_size_is_q]. *) -(* rewrite Z2Nat.id ; [ | now destruct toword ]. *) -(* cbn. *) +(* Lemma lower2_cancel_lift2_both : forall {A B C : choice_type} (f : A -> B -> C) x y, lower2 (lift2_both f) x y = f x y. *) +(* Proof. reflexivity. Qed. *) -(* rewrite group_size_is_q. *) -(* cbn. *) -(* rewrite Z2Nat.id ; [ | easy ]. *) -(* unfold Build_t_z_89_ at 1. *) +(* Lemma v_G_prime_order : prime #[(is_pure f_g : v_G_is_group)]. *) (* simpl. *) -(* set (Z.pos _). *) -(* rewrite (Z.mod_small z). *) -(* - rewrite Z.mod_small. *) - - - -(* (* assert (forall p b x, Z.pos p <= b -> x mod (Z.pos p) mod b = x mod (Z.pos p)). *) *) -(* (* { *) *) -(* (* intros. *) *) -(* (* rewrite Z.mod_small_iff. *) *) - -(* (* epose (Znumtheory.Zmod_div_mod b (Z.pos p) xa). *) *) -(* (* rewrite <- e. *) *) - -(* (* induction p. *) *) -(* (* - *) *) -(* (* cbn. *) *) (* Admitted. *) - - - -(* Lemma FieldToWitnessCancel : *) -(* forall x, FieldToWitness (WitnessToField x) = x. *) -(* Proof. *) -(* intros. *) -(* unfold WitnessToField, FieldToWitness. *) -(* unfold unsigned. *) -(* rewrite mkwordK. *) -(* simpl. *) -(* rewrite Zmod_small. *) -(* 2: { *) -(* destruct x. *) -(* cbn. *) -(* rewrite Schnorr.order_ge1 in i. *) - -(* (* rewrite Nat2Z.id. *) *) -(* (* now rewrite inord_val. *) *) -(* (* Qed. *) *) -(* Admitted. *) - -(* Axiom WitnessToFieldAdd : forall x y, WitnessToField (Zp_add x y) = is_pure (f_add (ret_both (WitnessToField x)) (ret_both (WitnessToField y))). *) -(* Axiom WitnessToFieldMul : forall x y, WitnessToField (Zp_mul x y) = is_pure (f_mul (ret_both (WitnessToField x)) (ret_both (WitnessToField y))). *) - -(* Axiom randomness_sample_is_bijective : *) -(* bijective *) -(* (λ x : 'I_(2 ^ 32), *) -(* fto *) -(* (FieldToWitness *) -(* (is_pure *) -(* (f_random_field_elem (ret_both (Hacspec_Lib_Pre.repr _ (Z.of_nat (nat_of_ord x)))))))). *) - -(* Axiom hash_is_psudorandom : *) -(* forall {A B} i (H : Positive i) f pre post (c0 : _ -> raw_code A) (c1 : _ -> raw_code B) l, *) -(* bijective f *) -(* → (∀ x1 : Arit (uniform i), ⊢ ⦃ pre ⦄ c0 x1 ≈ c1 (f x1) ⦃ post ⦄) -> *) -(* ⊢ ⦃ pre ⦄ *) -(* e ← sample uniform i ;; *) -(* c0 e ≈ *) -(* x ← is_state *) -(* (f_hash (t_Group := v_G_t_Group) *) -(* (impl__into_vec *) -(* (unsize *) -(* (box_new *) -(* (array_from_list l))))) ;; c1 x ⦃ post ⦄. *) - -(* Axiom conversion_is_true : *) -(* forall (b : both (v_G_t_Group.(f_Z))), StatementToGroup *) -(* (HacspecGroup.g ^+ FieldToWitness (is_pure b)) = is_pure (f_g_pow b). *) - -(* End OVN_schnorr_proof_params_Z89. *) - -(* Module OVN_schnorr_proof_Z89 := OVN_schnorr_proof Z89_impl Z89_group_operations . *) - -(* Schnorr_Z89.Sigma.RUN_interactive *) - -(* Import Schnorr_Z89.Sigma. *) -(* Import Schnorr_Z89.MyAlg. *) -(* Import Schnorr_Z89.Sigma.Oracle. *) - -(* Import Z89_impl. *) +(* (* Proof. *) *) +(* (* intros. *) *) +(* (* simpl. *) *) +(* (* (* replace (inord 1) with (inord 89). *) *) *) +(* (* (* pose (order_Zp1 88). *) *) *) +(* (* (* unfold Zp1 in e. *) *) *) +(* (* epose order1. *) *) +(* (* Set Printing All. *) *) +(* (* replace (inZp _) with (inord (n' := 88) 1) in e. *) *) +(* (* - rewrite order1. *) *) +(* (* rewrite order1 in e. *) *) +(* (* Set Printing All. *) *) + +(* (* unfold v_G_is_group. *) *) +(* (* simpl. *) *) +(* (* unfold order. *) *) +(* (* simpl. *) *) +(* (* rewrite e. *) *) +(* (* easy. *) *) +(* (* - apply ord_inj; now rewrite inordK. *) *) +(* (* Qed. *) *) + +(* Lemma v_G_g_gen : [set : v_G_is_group] = <[ is_pure f_g : v_G_is_group]>. Admitted. *) +(* End Z89_secure_group. *) + +(* (* Module OVN_schnorr_proof_params_Z89 <: OVN_schnorr_proof_preconditions Z89_impl Z89_group_operations Z89_secure_group. *) *) +(* (* Include Z89_secure_group. *) *) + +(* (* Module HacspecGroup := HacspecGroupParam Z89_impl Z89_group_operations Z89_secure_group. *) *) +(* (* Module Schnorr := Schnorr HacspecGroup. *) *) + +(* (* Import Schnorr.MyParam. *) *) +(* (* Import Schnorr.MyAlg. *) *) + +(* (* Import Schnorr.Sigma.Oracle. *) *) +(* (* Import Schnorr.Sigma. *) *) + +(* (* Definition StatementToGroup : Statement -> v_G := id. *) *) + +(* (* (* Lemma group_size : #[HacspecGroup.g].-2.+2 = 89. *) *) *) +(* (* (* Proof. *) *) *) +(* (* (* rewrite totient_gen. *) *) *) +(* (* (* epose (@generator_order v_G_is_group (is_pure f_g) (1)). *) *) *) +(* (* (* rewrite e. *) *) *) +(* (* (* 2:{ *) *) *) +(* (* (* simpl. *) *) *) +(* (* (* pose (cycle_generator). *) *) *) +(* (* (* unfold generator. *) *) *) +(* (* (* reflexivity. *) *) *) +(* (* (* epose (@generator_cycle v_G_is_group (is_pure f_g)). *) *) *) +(* (* (* simpl in i. *) *) *) +(* (* (* unfold generator in i. *) *) *) + +(* (* (* assert (HacspecGroup.g = inZp 1). *) *) *) +(* (* (* { *) *) *) +(* (* (* unfold inZp. *) *) *) +(* (* (* unfold HacspecGroup.g. *) *) *) +(* (* (* simpl. *) *) *) +(* (* (* unfold inord. *) *) *) +(* (* (* unfold ord0. *) *) *) +(* (* (* unfold insubd. *) *) *) +(* (* (* unfold insub. *) *) *) +(* (* (* unfold odflt. *) *) *) +(* (* (* unfold oapp. *) *) *) +(* (* (* unfold sub. *) *) *) +(* (* (* destruct idP. *) *) *) +(* (* (* - simpl. *) *) *) + + +(* (* (* simpl. *) *) *) + +(* (* (* simpl. *) *) *) + + +(* (* (* cbn. *) *) *) +(* (* (* rewrite card_Aut_cycle. *) *) *) +(* (* (* reflexivity. *) *) *) + +(* (* Lemma inord_is_inZp : forall {n} x, (x < n.+1)%nat -> inord (n' := n) x = inZp (p' := n) x. *) *) +(* (* Proof. *) *) +(* (* intros n x H. *) *) +(* (* rewrite <- (inordK (m := x) (n' := n)) ; [ | assumption ]. *) *) +(* (* rewrite (valZpK (inord (n' := n) x)). *) *) +(* (* rewrite inord_val. *) *) +(* (* reflexivity. *) *) +(* (* Qed. *) *) + +(* (* Definition WitnessToField : Witness -> v_G_t_Group.(f_Z) := fun x => mkword _ (Z.of_nat ((nat_of_ord x) %% Schnorr.q)). *) *) +(* (* Definition FieldToWitness : v_G_t_Group.(f_Z) -> Witness := fun x => inord ((Z.to_nat (unsigned x)) %% Schnorr.q). *) *) + +(* (* Lemma group_size_is_q : (Schnorr.q = Z.to_nat (unsigned (is_pure (HacspecGroup.v_G_t_Group.(f_Z_t_Field).(f_q))))). *) *) +(* (* Admitted. *) *) + + +(* (* Lemma in_equality : forall v u, is_true (0 <= v < u)%R <-> is_true (Z.to_nat v < Z.to_nat u)%N. *) *) +(* (* Admitted. *) *) + +(* (* Lemma WitnessToFieldCancel : forall x, WitnessToField (FieldToWitness x) = x. *) *) +(* (* Proof. *) *) +(* (* intros. *) *) +(* (* simpl in *. *) *) + +(* (* destruct x. *) *) +(* (* unfold WitnessToField, FieldToWitness. *) *) +(* (* simpl. *) *) +(* (* rewrite !inordK. *) *) +(* (* 2:{ *) *) +(* (* simpl. *) *) +(* (* rewrite Schnorr.order_ge1. *) *) +(* (* simpl. *) *) +(* (* Set Printing Coercions. *) *) +(* (* unfold unsigned. *) *) +(* (* unfold urepr. *) *) +(* (* simpl. *) *) + +(* (* apply ltn_pmod. *) *) +(* (* now rewrite group_size_is_q. *) *) +(* (* } *) *) +(* (* apply word_ext. *) *) +(* (* rewrite modn_mod. *) *) +(* (* rewrite modnZE ; [ | now rewrite group_size_is_q]. *) *) +(* (* rewrite Z2Nat.id ; [ | now destruct toword ]. *) *) +(* (* cbn. *) *) + +(* (* rewrite group_size_is_q. *) *) +(* (* cbn. *) *) +(* (* rewrite Z2Nat.id ; [ | easy ]. *) *) +(* (* unfold Build_t_z_89_ at 1. *) *) +(* (* simpl. *) *) +(* (* set (Z.pos _). *) *) +(* (* rewrite (Z.mod_small z). *) *) +(* (* - rewrite Z.mod_small. *) *) + + + +(* (* (* assert (forall p b x, Z.pos p <= b -> x mod (Z.pos p) mod b = x mod (Z.pos p)). *) *) *) +(* (* (* { *) *) *) +(* (* (* intros. *) *) *) +(* (* (* rewrite Z.mod_small_iff. *) *) *) + +(* (* (* epose (Znumtheory.Zmod_div_mod b (Z.pos p) xa). *) *) *) +(* (* (* rewrite <- e. *) *) *) + +(* (* (* induction p. *) *) *) +(* (* (* - *) *) *) +(* (* (* cbn. *) *) *) +(* (* Admitted. *) *) + + + +(* (* Lemma FieldToWitnessCancel : *) *) +(* (* forall x, FieldToWitness (WitnessToField x) = x. *) *) +(* (* Proof. *) *) +(* (* intros. *) *) +(* (* unfold WitnessToField, FieldToWitness. *) *) +(* (* unfold unsigned. *) *) +(* (* rewrite mkwordK. *) *) +(* (* simpl. *) *) +(* (* rewrite Zmod_small. *) *) +(* (* 2: { *) *) +(* (* destruct x. *) *) +(* (* cbn. *) *) +(* (* rewrite Schnorr.order_ge1 in i. *) *) + +(* (* (* rewrite Nat2Z.id. *) *) *) +(* (* (* now rewrite inord_val. *) *) *) +(* (* (* Qed. *) *) *) +(* (* Admitted. *) *) + +(* (* Axiom WitnessToFieldAdd : forall x y, WitnessToField (Zp_add x y) = is_pure (f_add (ret_both (WitnessToField x)) (ret_both (WitnessToField y))). *) *) +(* (* Axiom WitnessToFieldMul : forall x y, WitnessToField (Zp_mul x y) = is_pure (f_mul (ret_both (WitnessToField x)) (ret_both (WitnessToField y))). *) *) + +(* (* Axiom randomness_sample_is_bijective : *) *) +(* (* bijective *) *) +(* (* (λ x : 'I_(2 ^ 32), *) *) +(* (* fto *) *) +(* (* (FieldToWitness *) *) +(* (* (is_pure *) *) +(* (* (f_random_field_elem (ret_both (Hacspec_Lib_Pre.repr _ (Z.of_nat (nat_of_ord x)))))))). *) *) + +(* (* Axiom hash_is_psudorandom : *) *) +(* (* forall {A B} i (H : Positive i) f pre post (c0 : _ -> raw_code A) (c1 : _ -> raw_code B) l, *) *) +(* (* bijective f *) *) +(* (* → (∀ x1 : Arit (uniform i), ⊢ ⦃ pre ⦄ c0 x1 ≈ c1 (f x1) ⦃ post ⦄) -> *) *) +(* (* ⊢ ⦃ pre ⦄ *) *) +(* (* e ← sample uniform i ;; *) *) +(* (* c0 e ≈ *) *) +(* (* x ← is_state *) *) +(* (* (f_hash (t_Group := v_G_t_Group) *) *) +(* (* (impl__into_vec *) *) +(* (* (unsize *) *) +(* (* (box_new *) *) +(* (* (array_from_list l))))) ;; c1 x ⦃ post ⦄. *) *) + +(* (* Axiom conversion_is_true : *) *) +(* (* forall (b : both (v_G_t_Group.(f_Z))), StatementToGroup *) *) +(* (* (HacspecGroup.g ^+ FieldToWitness (is_pure b)) = is_pure (f_g_pow b). *) *) + +(* (* End OVN_schnorr_proof_params_Z89. *) *) + +(* (* Module OVN_schnorr_proof_Z89 := OVN_schnorr_proof Z89_impl Z89_group_operations . *) *) + +(* (* Schnorr_Z89.Sigma.RUN_interactive *) *) + +(* (* Import Schnorr_Z89.Sigma. *) *) +(* (* Import Schnorr_Z89.MyAlg. *) *) +(* (* Import Schnorr_Z89.Sigma.Oracle. *) *) + +(* (* Import Z89_impl. *) *)