twist add is also proven

High/Zmodp2_rules.v

@@ -8,17 +8,13 @@ Require Import Ring.
 Open Scope ring_scope.
 Import GRing.Theory.
 Import Zmodp2.
+Import BinInt.
 
 Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type.
-Proof.
-move => x; rewrite ?exprSr expr0 GRing.mul1r //.
-Qed.
+Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed.
 
 Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R.
-Proof.
-move => x; rewrite ?exprSr expr0 GRing.mul1r //.
-Qed.
-
+Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed.
 
 Ltac ring_simplify_this :=
   repeat match goal with
@@ -34,7 +30,13 @@ Ltac ring_simplify_this :=
   | _ => done
 end.
 
+Lemma pi_2 : Zmodp.pi 2 = 2%:R.
+Proof. by apply/eqP ; zmodp_compute. Qed.
+Lemma pi_3 : Zmodp.pi 3 = 3%:R.
+Proof. by apply/eqP ; zmodp_compute. Qed.
+
 Ltac ringify := repeat match goal with
+  | [ |- context[Zmodp.pi 2]] => rewrite pi_2
   | [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
   | [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
   | [ |- context[Zmodp.opp ?a]] => have ->: Zmodp.opp a = -a => //
@@ -45,59 +47,140 @@ Ltac ringify := repeat match goal with
   | [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
   end.
 
-Lemma Zmodp2_add_Zmodp a b: Zmodp2 a 0 + Zmodp2 b 0 = Zmodp2 (a + b) 0.
+(*
+ * Operations of the form (a , 0) op (b , 0)
+ *)
+
+Lemma Zmodp2_add_Zmodp_a0 a b: Zmodp2 a 0 + Zmodp2 b 0 = Zmodp2 (a + b) 0.
 Proof.
   rewrite /GRing.add /= /add /=.
   ringify ; ring_simplify_this.
 Qed.
 
-Lemma Zmodp2_opp_Zmodp a :- Zmodp2 a 0 = Zmodp2 (-a) 0.
+Lemma Zmodp2_opp_Zmodp_a0 a: - Zmodp2 a 0 = Zmodp2 (-a) 0.
 Proof.
   rewrite /GRing.opp /= /opp /=.
   ringify ; ring_simplify_this.
 Qed.
 
-Lemma Zmodp2_sub_Zmodp a b:Zmodp2 a 0 - Zmodp2 b 0 = Zmodp2 (a - b) 0.
+Lemma Zmodp2_sub_Zmodp_a0 a b: Zmodp2 a 0 - Zmodp2 b 0 = Zmodp2 (a - b) 0.
 Proof.
   rewrite /GRing.add /= /add /=.
   ringify ; ring_simplify_this.
 Qed.
 
-Lemma Zmodp2_mul_Zmodp a b :Zmodp2 a 0 * Zmodp2 b 0 = Zmodp2 (a * b) 0.
+Lemma Zmodp2_mul_Zmodp_a0 a b :Zmodp2 a 0 * Zmodp2 b 0 = Zmodp2 (a * b) 0.
 Proof.
   rewrite /GRing.mul /= /mul /=.
   ringify ; ring_simplify_this.
 Qed.
 
-Lemma Zmodp2_pow_Zmodp : forall n a, (Zmodp2 a 0) ^+ n = Zmodp2 (a^+n) 0.
+Lemma Zmodp2_pow_Zmodp_a0 : forall n a, (Zmodp2 a 0) ^+ n = Zmodp2 (a^+n) 0.
 Proof.
   elim => [| n IHn] a.
   - by rewrite ?expr0.
-  - by rewrite ?exprS IHn Zmodp2_mul_Zmodp.
+  - by rewrite ?exprS IHn Zmodp2_mul_Zmodp_a0.
 Qed.
 
-Lemma Zmodp2_inv_Zmodp a :(Zmodp2 a 0)^-1 = Zmodp2 (a^-1) 0.
+Lemma Zmodp2_inv_Zmodp_a0 a :(Zmodp2 a 0)^-1 = Zmodp2 (a^-1) 0.
 Proof.
 have/orP := orbN (Zmodp.eqb a 0).
 move => []; move/Refl.eqb_spec.
 - by move => ->; rewrite ?invr0.
 - move => Ha.
 apply GRing.mulr1_eq.
-rewrite Zmodp2_mul_Zmodp GRing.mulfV //.
+rewrite Zmodp2_mul_Zmodp_a0 GRing.mulfV //.
 by apply/eqP.
 Qed.
 
-Lemma Zmodp2_div_Zmodp a b : (Zmodp2 a 0) / (Zmodp2 b 0) = Zmodp2 (a/b) 0.
+Lemma Zmodp2_div_Zmodp_a0 a b : (Zmodp2 a 0) / (Zmodp2 b 0) = Zmodp2 (a/b) 0.
 Proof.
-by rewrite Zmodp2_inv_Zmodp Zmodp2_mul_Zmodp.
+by rewrite Zmodp2_inv_Zmodp_a0 Zmodp2_mul_Zmodp_a0.
+Qed.
+
+
+(*
+ * Operations of the form (a , 0) op (b , 0)
+ *)
+Lemma Zmodp2_add_Zmodp_0a a b: Zmodp2 0 a + Zmodp2 0 b = Zmodp2 0 (a + b).
+Proof.
+  rewrite /GRing.add /= /add /=.
+  ringify ; ring_simplify_this.
 Qed.
 
+Lemma Zmodp2_opp_Zmodp_0a a: - Zmodp2 0 a = Zmodp2 0 (-a).
+Proof.
+  rewrite /GRing.opp /= /opp /=.
+  ringify ; ring_simplify_this.
+Qed.
+
+Lemma Zmodp2_sub_Zmodp_0a a b: Zmodp2 0 a - Zmodp2 0 b = Zmodp2 0 (a - b).
+Proof.
+  rewrite /GRing.add /= /add /=.
+  ringify ; ring_simplify_this.
+Qed.
+
+Lemma Zmodp2_mul_Zmodp_0a a b: Zmodp2 0 a * Zmodp2 0 b = Zmodp2  (2%:R * a * b) 0.
+Proof.
+  rewrite /GRing.mul /= /mul /=.
+  ringify ; ring_simplify_this.
+  by rewrite GRing.mulrA.
+Qed.
+
+
+Lemma Zmodp2_inv_Zmodp_0a a :(Zmodp2 0 a)^-1 = Zmodp2 0 ((2%:R * a)^-1).
+Proof.
+have/orP := orbN (Zmodp.eqb a 0).
+move => []; move/Refl.eqb_spec.
+- by move => -> ; rewrite GRing.mulr0 ?invr0.
+- move => Ha.
+  apply GRing.mulr1_eq.
+  rewrite Zmodp2_mul_Zmodp_0a GRing.mulfV //.
+  apply/eqP => H2a.
+  apply: Ha.
+  move: H2a.
+  move/(f_equal (fun x => (2%:R^-1) * x)).
+  rewrite GRing.mulrA GRing.mulr0 (mulrC 2%:R^-1) GRing.mulfV ; ring_simplify_this.
+  by zmodp_compute.
+Qed.
+
+(*
+ * Operations of the form (a , 0) op (0 , b)
+ *)
+
+
+Lemma Zmodp2_mul_Zmodp_ab1 a b: Zmodp2 a 0 * Zmodp2 0 b = Zmodp2 0 (a * b).
+Proof.
+  rewrite /GRing.mul /= /mul /=.
+  ringify ; ring_simplify_this.
+Qed.
+
+Lemma Zmodp2_mul_Zmodp_ab2 a b: Zmodp2 0 a * Zmodp2 b 0 = Zmodp2 0 (a * b).
+Proof.
+  rewrite /GRing.mul /= /mul /=.
+  ringify ; ring_simplify_this.
+Qed.
+
+Lemma Zmodp_mul_comm_2 (a:Zmodp.type) : 2%:R * a = a * 2%:R.
+Proof. by rewrite /GRing.mul /= Zmodp_ring.mul_comm. Qed.
+
+
+(*
+ * Big rewrite tactic
+ *)
 Ltac Zmodpify := repeat match goal with 
-  | _ => rewrite Zmodp2_add_Zmodp
-  | _ => rewrite Zmodp2_sub_Zmodp
-  | _ => rewrite Zmodp2_opp_Zmodp
-  | _ => rewrite Zmodp2_mul_Zmodp
-  | _ => rewrite Zmodp2_pow_Zmodp
-  | _ => rewrite Zmodp2_inv_Zmodp
-  | _ => rewrite Zmodp2_div_Zmodp
+  | _ => rewrite Zmodp2_add_Zmodp_a0
+  | _ => rewrite Zmodp2_sub_Zmodp_a0
+  | _ => rewrite Zmodp2_opp_Zmodp_a0
+  | _ => rewrite Zmodp2_add_Zmodp_0a
+  | _ => rewrite Zmodp2_sub_Zmodp_0a
+  | _ => rewrite Zmodp2_opp_Zmodp_0a
+  | _ => rewrite Zmodp2_mul_Zmodp_a0
+  | _ => rewrite Zmodp2_pow_Zmodp_a0
+  | _ => rewrite Zmodp2_inv_Zmodp_a0
+  | _ => rewrite Zmodp2_div_Zmodp_a0
+  | _ => rewrite Zmodp2_mul_Zmodp_0a
+  | _ => rewrite Zmodp2_mul_Zmodp_ab1
+  | _ => rewrite Zmodp2_mul_Zmodp_ab2
+  | _ => rewrite Zmodp2_inv_Zmodp_0a
 end.

High/curve_twist_incl_Fp2.v

@@ -103,6 +103,69 @@ Proof.
   - apply ontwist25519.
 Qed.
 
+Definition curve_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
+match p with
+  | EC_Inf => EC_Inf Zmodp2.type
+  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
+end.
+
+Definition twist_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
+match p with
+  | EC_Inf => EC_Inf Zmodp2.type
+  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 0 y)
+end.
+
+Lemma curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
+  p' = curve_Fp_to_Fp2 p ->
+  q' = curve_Fp_to_Fp2 q ->
+  MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add_no_check curve25519_mcuType p q).
+Proof.
+  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
+  rewrite /curve25519.a /curve25519.b.
+  match goal with
+    | [ |- _ = ?A ] => remember A as Freezer
+  end.
+  rewrite /eq_op /Equality.op /=.
+  rewrite /eq_op /Equality.op /=.
+  rewrite !eq_refl ?Bool.andb_true_r.
+  rewrite ?expr2.
+  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
+  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
+  Zmodpify => /=.
+  ringify.
+  subst Freezer.
+  ring_simplify_this.
+  case_eq (xp == xq) => -> //=.
+  case_eq ((yp == yq) && (yp != 0)) => -> //=.
+Qed.
+
+Lemma twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
+  p' = twist_Fp_to_Fp2 p ->
+  q' = twist_Fp_to_Fp2 q ->
+  MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = twist_Fp_to_Fp2 (MCGroup.add_no_check twist25519_mcuType p q).
+Proof.
+  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
+  rewrite /twist25519.a /twist25519.b.
+  match goal with
+    | [ |- _ = ?A ] => remember A as Freezer
+  end.
+  rewrite /eq_op /Equality.op /=.
+  rewrite /eq_op /Equality.op /=.
+  rewrite !eq_refl ?Bool.andb_true_r.
+  rewrite ?expr2.
+  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
+  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
+  Zmodpify => /=.
+  subst Freezer.
+  ringify.
+  ring_simplify_this.
+  case_eq (xp == xq) => -> ; rewrite -Zmodp_mul_comm_2 ?GRing.mulrA //=.
+  case_eq ((yp == yq) && (yp != 0)) => -> //=.
+Qed.
+
+
+
+
 (* a great definition ... *)
 (* Definition curve_to_Fp2 (p: mc curve25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
 match p with
@@ -114,15 +177,11 @@ match p with
 end.
  *)
 (* a not so great definition ... *)
-Definition curve_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
-match p with
-  | EC_Inf => EC_Inf Zmodp2.type
-  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
-end.
 
-(* Lemma curve_to_Fp2_inf : curve_to_Fp2 (MC (MCGroup.zeroO curve25519_mcuType)) = MC (MCGroup.zeroO curve25519_Fp2_mcuType).
+(* 
+Lemma curve_to_Fp2_inf : curve_to_Fp2 (MC (MCGroup.zeroO curve25519_mcuType)) = MC (MCGroup.zeroO curve25519_Fp2_mcuType).
 Proof. done. Qed.
- *)
+*)
 (* Lemma curve_to_Fp2_xy x y (P: oncurve curve25519_mcuType (|x , y|)): curve_to_Fp2 (MC P) = MC (oncurve25519_impl x y P).
 Proof. done. Qed.
  *)
@@ -141,41 +200,14 @@ match p with
 end.
  *)
 (* a not so great definition ... *)
-Definition twist_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
+(* Definition twist_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
 match p with
   | EC_Inf => EC_Inf Zmodp2.type
   | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 0 y)
 end.
+ *)
 
 
-Lemma add_stable : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
-  p' = curve_to_Fp2 p ->
-  q' = curve_to_Fp2 q ->
-  MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = curve_to_Fp2 (MCGroup.add_no_check curve25519_mcuType p q).
-Proof.
-  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //=.
-  move => [] -> -> [] -> ->.
-  rewrite /curve25519.a /curve25519.b.
-  match goal with
-    | [ |- _ = ?A ] => remember A as Freezer
-  end.
-  rewrite /eq_op.
-  rewrite /Equality.op /=.
-  rewrite /eq_op.
-  rewrite /Equality.op /=.
-  rewrite !eq_refl.
-  rewrite ?Bool.andb_true_r.
-  rewrite ?expr2.
-  ring_simplify_this.
-  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
-  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
-  Zmodpify => /=.
-  ringify.
-  subst Freezer.
-  ring_simplify_this.
-  case_eq (xp == xq) => -> //=.
-  case_eq ((yp == yq) && (yp != 0)) => -> //=.
-Qed.
 
 
 (* Lemma nP_is_nP2 : forall (x1 x2 xs: Zmodp.type),