Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)

2 files changed, 32 insertions, 0 deletions

diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v
index 735e6ac76..87a53b7fe 100644
--- a/src/Curves/Montgomery/XZ.v
+++ b/src/Curves/Montgomery/XZ.v
@@ -85,6 +85,31 @@ Module M.
         ((x2, z2), (x3, z3))%core
       end.
 
+    Context {ap2d4:F} {ap2d4_correct:(1+1+1+1)*a24 = a+1+1}.
+    Definition boringladderstep (x1:F) (Q Q':F*F) : (F*F)*(F*F) :=
+      match Q, Q' with
+        pair x2 z2, pair x3 z3 =>
+        dlet tmp0l := x3 - z3 in
+        dlet tmp1l := x2 - z2 in
+        dlet x2l := x2 + z2 in
+        dlet z2l := x3 + z3 in
+        dlet z3 := tmp0l * x2l in
+        dlet z2 := z2l * tmp1l in
+        dlet tmp0 := tmp1l^2 in
+        dlet tmp1 := x2l^2 in
+        dlet x3l := z3 + z2 in
+        dlet z2l := z3 - z2 in
+        dlet x2 := tmp1 * tmp0 in
+        dlet tmp1l := tmp1 - tmp0 in
+        dlet z2 := z2l^2 in
+        dlet z3 := ap2d4 * tmp1l in
+        dlet x3 := x3l^2 in
+        dlet tmp0l := tmp0 + z3 in
+        dlet z3 := x1 * z2 in
+        dlet z2 := tmp1l * tmp0l 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.
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
index d3fd486d8..71d30919c 100644
--- a/src/Curves/Montgomery/XZProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -29,11 +29,13 @@ Module M.
 
     Context {a b: F} {b_nonzero:b <> 0}.
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
+    Context {ap2d4:F} {ap2d4_correct:(1+1+1+1)*a24 = a+1+1}.
     Local Notation Madd := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
     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 boringladderstep := (M.boringladderstep(ap2d4:=ap2d4)(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' :
@@ -41,6 +43,11 @@ Module M.
       eq (xzladderstep x1 Q Q') (donnaladderstep x1 Q Q').
     Proof. cbv; break_match; repeat split; fsatz. Qed.
 
+    Lemma boringladderstep_ok x1 Q Q' :
+      let eq := fieldwise (n:=2) (fieldwise (n:=2) Feq) in
+      eq (xzladderstep x1 Q Q') (boringladderstep 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.