use ladderstep from donna (2% faster?)

2 files changed, 53 insertions, 18 deletions

diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
index c31fb26c6..735e6ac76 100644
--- a/src/Curves/Montgomery/XZ.v
+++ b/src/Curves/Montgomery/XZ.v
@@ -57,26 +57,54 @@ Module M.
         ((x2, z2), (x3, z3))%core
       end.
 
-      Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}.
+    (* optimized version from curve25519-donna by Adam Langley *)
+    Definition donnaladderstep (x1:F) (Q Q':F*F) : (F*F)*(F*F) :=
+      match Q, Q' with
+        pair x z, pair x' z'=>
+        dlet origx := x in
+        dlet x := x + z in
+        dlet z := origx - z in
+        dlet origx' := x' in
+        dlet x' := x' + z' in
+        dlet z' := origx' - z' in
+        dlet xx' := x' * z in
+        dlet zz' := x * z' in
+        dlet origx' := xx' in
+        dlet xx' := xx' + zz' in
+        dlet zz' := origx' - zz' in
+        dlet x3 := xx'^2 in
+        dlet zzz' := zz'^2 in
+        dlet z3 := zzz' * x1 in
+        dlet xx := x^2 in
+        dlet zz := z^2 in
+        dlet x2 := xx * zz in
+        dlet zz := xx - zz in
+        dlet zzz := zz * a24 in
+        dlet zzz := zzz + xx in
+        dlet z2 := zz * zzz in
+        ((x2, z2), (x3, z3))%core
+      end.
+
+    Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}.
 
-      Local Notation xor := Coq.Init.Datatypes.xorb.
+    Local Notation xor := Coq.Init.Datatypes.xorb.
 
-      (* Ideally, we would verify that this corresponds to x coordinate
-         multiplication *)
-      Local Open Scope core_scope.
-      Definition montladder (bound : positive) (testbit:Z->bool) (u:F) :=
-        let '(P1, P2, swap) :=
-            for (int i = BinInt.Z.pos bound; i >= 0; i--)
-                updating ('(P1, P2, swap) = ((1%F, 0%F), (u, 1%F), false)) {{
-              dlet s_i := testbit i in
-              dlet swap := xor swap s_i in
-              let '(P1, P2) := cswap swap P1 P2 in
-              dlet swap := s_i in
-              let '(P1, P2) := xzladderstep u P1 P2 in
-              (P1, P2, swap)
-        }} in
-        let '((x, z), _) := cswap swap P1 P2 in
-        x * Finv z.
+    (* Ideally, we would verify that this corresponds to x coordinate
+       multiplication *)
+    Local Open Scope core_scope.
+    Definition montladder (bound : positive) (testbit:Z->bool) (u:F) :=
+      let '(P1, P2, swap) :=
+          for (int i = BinInt.Z.pos bound; i >= 0; i--)
+              updating ('(P1, P2, swap) = ((1%F, 0%F), (u, 1%F), false)) {{
+            dlet s_i := testbit i in
+            dlet swap := xor swap s_i in
+            let '(P1, P2) := cswap swap P1 P2 in
+            dlet swap := s_i in
+            let '(P1, P2) := xzladderstep u P1 P2 in
+            (P1, P2, swap)
+      }} in
+      let '((x, z), _) := cswap swap P1 P2 in
+      x * Finv z.
 
   End MontgomeryCurve.
 End M.
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
index be0153251..d3fd486d8 100644
--- a/src/Curves/Montgomery/XZProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.SetoidSubst.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -32,8 +33,14 @@ Module M.
     Local Notation Mopp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
     Local Notation Mpoint := (@M.point F Feq Fadd Fmul a b).
     Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
+    Local Notation donnaladderstep := (M.donnaladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
     Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
 
+    Lemma donnaladderstep_ok x1 Q Q' :
+      let eq := fieldwise (n:=2) (fieldwise (n:=2) Feq) in
+      eq (xzladderstep x1 Q Q') (donnaladderstep x1 Q Q').
+    Proof. cbv; break_match; repeat split; fsatz. Qed.
+
     Definition projective (P:F*F) :=
       if dec (snd P = 0) then fst P <> 0 else True.
     Definition eq (P Q:F*F) := fst P * snd Q = fst Q * snd P.