diff options
Diffstat (limited to 'src/Spec/CompleteEdwardsCurve.v')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 3348be1d9..2ad3877ac 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -5,6 +5,8 @@ Require Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.Spec.ModularArithmetic. Local Open Scope F_scope. +Global Set Asymmetric Patterns. + Class TwistedEdwardsParams := { q : BinInt.Z; a : F q; @@ -19,7 +21,7 @@ Class TwistedEdwardsParams := { Module E. Section TwistedEdwardsCurves. Context {prm:TwistedEdwardsParams}. - + (* Twisted Edwards curves with complete addition laws. References: * <https://eprint.iacr.org/2008/013.pdf> * <http://ed25519.cr.yp.to/ed25519-20110926.pdf> @@ -27,20 +29,20 @@ Module E. *) Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. Definition point := { P | onCurve P}. - + Definition zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q). - + Definition add' P1' P2' := let '(x1, y1) := P1' in let '(x2, y2) := P2' in (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - + Definition add (P1 P2 : point) : point := let 'exist P1' pf1 := P1 in let 'exist P2' pf2 := P2 in exist _ (add' P1' P2') (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2). - + Fixpoint mul (n:nat) (P : point) : point := match n with | O => zero @@ -48,7 +50,7 @@ Module E. end. End TwistedEdwardsCurves. End E. - + Delimit Scope E_scope with E. Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope.
\ No newline at end of file +Infix "*" := E.mul : E_scope. |