Fix calculation of T in mixed addition

We were previously overwriting the values used to calculate T. This
corrects the logic, while still minimizing memory consumption. The
result is a little messier in the order of statements, but not by much.

src/Bedrock/End2End/X25519/EdwardsXYZT.v

@@ -57,19 +57,20 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, half_ypx, h
   stackalloc 40 as YmX1;
   fe25519_sub(YmX1, Y1, X1);
   stackalloc 40 as A;
-  fe25519_mul(A, YpX1, half_ypx);
+  fe25519_mul(A, YmX1, half_ymx);
   stackalloc 40 as B;
-  fe25519_mul(B, YmX1, half_ymx);
+  fe25519_mul(B, YpX1, half_ypx);
   stackalloc 40 as C;
   fe25519_mul(C, xyd, T1);
-  fe25519_sub(ox, A, B);
-  fe25519_add(oy, A, B);
+  fe25519_sub(ox, B, A);
+  stackalloc 40 as F;
+  fe25519_sub(F, Z1, C);
   fe25519_add(oz, Z1, C);
-  fe25519_sub(ot, Z1, C);
-  fe25519_mul(ox, ox, ot);
-  fe25519_mul(oy, oy, oz);
-  fe25519_mul(oz, ot, oz);
-  fe25519_mul(ot, ox, oy)
+  fe25519_add(oy, B, A);
+  fe25519_mul(ot, ox, oy);
+  fe25519_mul(ox, ox, F);
+  fe25519_mul(oy, oz, oy);
+  fe25519_mul(oz, F, oz)
 }.
 
 (* Equivalent of m1double in src/Curves/Edwards/XYZT/Basic.v *)
@@ -262,36 +263,36 @@ Proof.
   (* Each binop produces 2 memory goals on the inputs, 2 bounds goals on the inputs, and 1 memory goal on the output. *)
   single_step. (* fe25519_add(YpX1, Y1, X1) *)
   single_step. (* fe25519_sub(YmX1, Y1, X1) *)
-  single_step. (* fe25519_mul(A, YpX1, half_ypx) *)
-  single_step. (* fe25519_mul(B, YmX1, half_ymx) *)
+  single_step. (* fe25519_mul(A, YmX1, half_ymx) *)
+  single_step. (* fe25519_mul(B, YpX1, half_ypx) *)
   single_step. (* fe25519_mul(C, xyd, T1) *)
-  single_step. (* fe25519_sub(ox, A, B) *)
-  single_step. (* fe25519_add(oy, A, B) *)
+  single_step. (* fe25519_sub(ox, B, A) *)
+  single_step. (* fe25519_sub(F, Z1, C) *)
   single_step. (* fe25519_add(oz, Z1, C) *)
-  single_step. (* fe25519_sub(ot, Z1, C) *)
-  single_step. (* fe25519_mul(ox, ox, ot) *)
-  single_step. (* fe25519_mul(oy, oy, oz) *)
-  single_step. (* fe25519_mul(oz, ot, oz) *)
+  single_step. (* fe25519_add(oy, B, A) *)
   single_step. (* fe25519_mul(ot, ox, oy) *)
+  single_step. (* fe25519_mul(ox, ox, F) *)
+  single_step. (* fe25519_mul(oy, oy, oz) *)
+  single_step. (* fe25519_mul(oz, F, oz) *)
 
   (* Solve the postconditions *)
   repeat straightline.
-  (* Rewrites the FElems for the stack (in H80) to be about bytes instead *)
+  (* Rewrites the FElems for the stack (in H84) to be about bytes instead *)
     cbv [FElem] in *.
     (* Prevent output from being rewritten by seprewrite_in *) 
-    remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H80.
-    remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H80.
-    remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H80.
-    remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H80.
-    do 5 (seprewrite_in @Bignum.Bignum_to_bytes H80).
+    remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H84.
+    remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H84.
+    remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H84.
+    remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H84.
+    do 6 (seprewrite_in @Bignum.Bignum_to_bytes H84).
     subst Pt Pz Py Px.
-    extract_ex1_and_emp_in H80.
+    extract_ex1_and_emp_in H84.
 
   (* Solve stack/memory stuff *)
   repeat straightline.
 
   (* Post-conditions *)
-  exists x8,x9,x10,x11; ssplit. 2,3,4,5:solve_bounds.
+  exists x9,x10,x11,x8; ssplit. 2,3,4,5:solve_bounds.
   { (* Correctness: result matches Gallina *)
     cbv [bin_model bin_mul bin_add bin_carry_add bin_sub] in *.
     cbv match beta delta [m1add_precomputed_coordinates].

src/Curves/Edwards/XYZT/Precomputed.v

@@ -15,7 +15,7 @@ Section ExtendedCoordinates.
           {Feq_dec:DecidableRel Feq}.
 
   Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-  Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+  Local Notation "0" := Fzero.  Local Notation "1" := Fone. Local Notation "2" := (Fadd 1 1).
   Local Infix "+" := Fadd. Local Infix "*" := Fmul.
   Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
   Local Notation "x ^ 2" := (x*x).
@@ -31,27 +31,29 @@ Section ExtendedCoordinates.
 
   Definition of_twisted (P:Epoint) :=
     let '(x, y) := E.coordinates P in
-    ((y+x)/(1+1), (y-x)/(1+1), x*y*d). (* 1+1 ew *)
+    ((y+x)/2, (y-x)/2, x*y*d).
 
   Section TwistMinusOne.
     Context {a_eq_minus1:a = Fopp 1}.
+    (* https://hyperelliptic.org/EFD/g1p/data/twisted/extended-1/addition/madd-2008-hwcd-3,
+       but with halved precomputed coordinates (making D unnecessary) *)
     Definition m1add_precomputed_coordinates (P:F*F*F*F) (Q:precomputed_point) : F*F*F*F :=
     let '(X1, Y1, Z1, T1) := P in
     let '(half_ypx, half_ymx, xyd) := Q in
     let YpX1 := Y1+X1 in
     let YmX1 := Y1-X1 in
-    let A := YpX1*half_ypx in
-    let B := YmX1*half_ymx in
-    let C := xyd*T1 in
-    let X3 := A-B in
-    let Y3 := A+B in
+    let A := YmX1*half_ymx in
+    let B := YpX1*half_ypx in
+    let C := xyd*T1 in (* = T1*2d*T2, since Z2=1 so T2=X2*Y2 *)
+    let X3 := B-A in
+    let F := Z1-C in
     let Z3 := Z1+C in
-    let T3 := Z1-C in
-    (* X/Z, Y/T = x, y *)
-    let X3 := X3*T3 in
-    let Y3 := Y3*Z3 in
-    let Z3 := T3*Z3 in
+    let Y3 := B+A in
+    (* X/Z, Y/Z = x, y *)
     let T3 := X3*Y3 in
+    let X3 := X3*F in
+    let Y3 := Z3*Y3 in
+    let Z3 := F*Z3 in
     (X3, Y3, Z3, T3).
 
     Create HintDb points_as_coordinates discriminated.
@@ -62,7 +64,7 @@ Section ExtendedCoordinates.
     Lemma m1add_precomputed_coordinates_correct P Q :
       let '(X1, Y1, Z1, T1) := m1add_precomputed_coordinates (XYZT.Basic.coordinates P) (of_twisted Q) in
       let '(X2, Y2, Z2, T2) := coordinates (m1add P (XYZT_of_twisted Q)) in
-            Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
+            Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2 /\ X1*Y1 = Z1*T1.
     Proof.
       repeat match goal with
              | _ => progress autounfold with points_as_coordinates in *
@@ -73,5 +75,6 @@ Section ExtendedCoordinates.
              | |- _ /\ _ => split
              end; fsatz.
     Qed.
+
   End TwistMinusOne.
 End ExtendedCoordinates.