aboutsummaryrefslogtreecommitdiff
path: root/src/Curves/PointFormats.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Curves/PointFormats.v')
-rw-r--r--src/Curves/PointFormats.v156
1 files changed, 126 insertions, 30 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 32e6acdd0..cd27a2033 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,15 +1,16 @@
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField.
-Require Import Tactics.VerdiTactics.
-Require Import Logic.Eqdep_dec.
-Require Import BinNums NArith.
+Require Import Crypto.Galois.GaloisTheory Crypto.Galois.GaloisField.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Logic Logic.Eqdep_dec.
+Require Import BinNums NArith Nnat ZArith.
Module Type TwistedEdwardsParams (M : Modulus).
- Module Export GFDefs := ZGaloisField M.
+ Module Export GFDefs := GaloisField M.
Local Open Scope GF_scope.
- Axiom char_gt_2 : inject 2 <> 0.
+ Axiom char_gt_2 : (1+1) <> 0.
Parameter a : GF.
Axiom a_nonzero : a <> 0.
- Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
+ Parameter sqrt_a : GF.
+ Axiom a_square : sqrt_a^2 = a.
Parameter d : GF.
Axiom d_nonsquare : forall x, x * x <> d.
End TwistedEdwardsParams.
@@ -104,7 +105,7 @@ Qed.
Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M).
Local Open Scope GF_scope.
- (** Twisted Ewdwards curves with complete addition laws. References:
+ (** Twisted Edwards curves with complete addition laws. References:
* <https://eprint.iacr.org/2008/013.pdf>
* <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
* <https://eprint.iacr.org/2015/677.pdf>
@@ -133,22 +134,104 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
(* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *)
(* c=1 and an extra a in front of x^2 *)
- Lemma root_zero : forall x p, x^p = 0 -> x = 0.
- Admitted.
- Lemma root_nonzero : forall x p, x^p <> 0 -> x <> 0.
- Admitted.
+ (* NOTE: these should serve as an example for using field *)
+
Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
- Admitted.
+ intros; intuition; subst.
+ assert (0 * b = 0) by field; intuition.
+ Qed.
+
Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
- Admitted.
- Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
- Admitted.
- Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
- Admitted.
+ intros; intuition; subst.
+ assert (a0 * 0 = 0) by field; intuition.
+ Qed.
+
Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
- Admitted.
+ intros.
+ assert (H := Z.eq_dec (inject x) (inject y)).
+
+ destruct H.
+
+ - left; galois; intuition.
+
+ - right; intuition.
+ rewrite H in n.
+ assert (y = y); intuition.
+ Qed.
+
+ Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+ intros.
+ assert (Z := GF_eq_dec a0 0); destruct Z.
+
+ - left; intuition.
+
+ - assert (a0 * b / a0 = 0) by
+ ( rewrite H; field; intuition ).
+
+ field_simplify in H0.
+ replace (b/1) with b in H0 by (field; intuition).
+ right; intuition.
+ apply n in H0; intuition.
+ Qed.
+
+ Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+ intros; intuition; subst.
+ apply mul_zero_why in H1.
+ destruct H1; subst; intuition.
+ Qed.
Hint Resolve mul_nonzero_nonzero.
+ Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0.
+ intros.
+
+ induction p; inversion H.
+
+ revert H H1; generalize x; induction p; intros.
+
+ - simpl in H; apply mul_zero_why in H; destruct H; intuition.
+
+ + subst; intuition.
+
+ + apply IHp in H.
+ rewrite H1.
+ simpl in H1.
+ apply mul_zero_why in H1; destruct H1; intuition.
+ rewrite H0 in H.
+ apply mul_zero_why in H; destruct H; intuition.
+
+ simpl; intuition.
+
+ - simpl in H1; apply IHp in H1; simpl; intuition.
+ simpl in H; rewrite H in H1; rewrite H.
+ apply mul_zero_why in H1; destruct H1; intuition.
+
+ - simpl in H; subst; intuition.
+
+ Qed.
+
+ Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
+ intros; intuition.
+
+ induction p.
+
+ - apply H; intuition.
+
+ - apply H.
+ rewrite H1 in *.
+ induction p.
+
+ + simpl.
+ field.
+
+ + simpl in *.
+ replace (0 * 0) with 0 in * by field.
+ apply IHp; intuition.
+ induction p; inversion H2.
+
+ + simpl; intuition.
+
+ Qed.
+
Ltac whatsNotZero :=
repeat match goal with
| [H: ?lhs = ?rhs |- _ ] =>
@@ -159,7 +242,10 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
assert (rhs <> 0) by (rewrite H; auto)
| [H: (?a^?p)%GF <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
- assert (a <> 0) by (eapply root_nonzero; eauto)
+ let Y:=fresh in let Z:=fresh in try (
+ assert (p <> 0%N) as Z by (intro Y; inversion Y);
+ assert (a <> 0) by (eapply root_nonzero; eauto);
+ clear Z)
| [H: (?a*?b)%GF <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (a <> 0) by (eapply mul_nonzero_l; eauto)
@@ -173,11 +259,14 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
onCurve (x2, y2) ->
(d*x1*x2*y1*y2)^2 <> 1.
Proof.
+ (* TODO: this proof was made inconsistent by an actually
+ correct version of root_nonzero. This adds the necessary
+ hypothesis*)
unfold onCurve; intuition; whatsNotZero.
pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
destruct a_square as [sqrt_a a_square].
- rewrite <- a_square in *.
+ rewrite a_square in Ha_nonzero.
(* Furthermore... *)
pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
@@ -206,13 +295,18 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
end.
assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
+
+ rewrite a_square in *.
replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field.
(* contradiction: product of nonzero things is zero *)
- destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition];
- destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero; field.
+ destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition].
+ destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero.
+
+ + replace (inject 2%Z) with (1+1) in Hccc by field; intuition.
+
+ + rewrite <- a_square; simpl; rewrite Hccc; field.
Qed.
-
Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
onCurve (x1,y1) ->
onCurve (x2, y2) ->
@@ -239,8 +333,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
Definition projX (P:point) := fst (proj1_sig P).
Definition projY (P:point) := snd (proj1_sig P).
- Definition checkOnCurve x y : if Zbool.Zeq_bool (a*x^2 + y^2) (1 + d*x^2*y^2) then point else True.
- break_if. exists (x, y). exact (GFdecidable _ _ Heqb). trivial.
+ Definition checkOnCurve (x y: GF) : if Zbool.Zeq_bool (a*x^2 + y^2)%GF (1 + d*x^2*y^2)%GF then point else True.
+ break_if; trivial. exists (x, y). apply GFdecidable. exact Heqb.
Defined.
Hint Unfold onCurve mkPoint.
@@ -259,6 +353,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
Proof.
(* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
* c=1 and an extra a in front of x^2 *)
+
unfold unifiedAdd', onCurve in *; injection H; clear H; intros.
Ltac t x1 y1 x2 y2 :=
@@ -281,7 +376,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto.
- - rewrite <-HT1, <-HT2; field; rewrite HT1;
+ - rewrite <-HT1, <-HT2; field; rewrite HT1.
replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
by field; simpl; auto.
@@ -507,12 +602,13 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam
End CompleteTwistedEdwardsFacts.
Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
- Module Export GFDefs := ZGaloisField M.
+ Module Export GFDefs := GaloisField M.
Local Open Scope GF_scope.
- Axiom char_gt_2 : inject 2 <> 0.
+ Axiom char_gt_2 : (1+1) <> 0.
Definition a := inject (- 1).
Axiom a_nonzero : a <> 0.
- Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
+ Parameter sqrt_a : GF.
+ Axiom a_square : sqrt_a^2 = a.
Parameter d : GF.
Axiom d_nonsquare : forall x, x * x <> d.
End Minus1Params.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 11:37:50 +0000