From 0ae5f6871b29d20f48b5df6dab663b5a44162d01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 15:07:03 -0400 Subject: remove trailing whitespace from src/ --- src/Spec/CompleteEdwardsCurve.v | 6 +++--- src/Spec/EdDSA.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 5df36e295..88388ee0a 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -24,12 +24,12 @@ Module E. nonsquare_d : forall x, x^2 <> d }. Context `{twisted_edwards_params}. - + Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }. Definition coordinates (P:point) : (F*F) := proj1_sig P. Program Definition zero : point := (0, 1). - + Program Definition add (P1 P2:point) : point := exist _ ( let (x1, y1) := coordinates P1 in let (x2, y2) := coordinates P2 in @@ -47,7 +47,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 diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index bd8a095dd..2c7097207 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -26,7 +26,7 @@ Section EdDSA. {PointEncoding : canonical encoding of E as Word.word b} (* wire format *) {FlEncoding : canonical encoding of { n | n < l } as Word.word b} := - { + { EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; EdDSA_c_valid : c = 2 \/ c = 3; -- cgit v1.2.3