15 files changed, 111 insertions, 19 deletions
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v
index 816b333fd..6a209e169 100644
--- a/src/Specific/X25519/C64/CurveParameters.v
+++ b/src/Specific/X25519/C64/CurveParameters.v
@@ -18,7 +18,7 @@ Definition curve : CurveParameters :=
     a24 := Some 121665;
     coef_div_modulus := Some 2%nat;
 
-    goldilocks := Some false;
+    goldilocks := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := true;
@@ -62,7 +62,8 @@ Definition curve : CurveParameters :=
       (t4, t3, t2, t1, t0)
             );
 
-    upper_bound_of_exponent := None;
+    upper_bound_of_exponent_loose := None;
+    upper_bound_of_exponent_tight := None;
     allowable_bit_widths := None;
     freeze_extra_allowable_bit_widths := None;
     modinv_fuel := None
diff --git a/src/Specific/X25519/C64/feadd.v b/src/Specific/X25519/C64/feadd.v
new file mode 100644
index 000000000..43d887638
--- /dev/null
+++ b/src/Specific/X25519/C64/feadd.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C64.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition add :
+  { add : feBW_tight -> feBW_tight -> feBW_loose
+  | forall a b, phiBW_loose (add a b) = F.add (phiBW_tight a) (phiBW_tight b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_add ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions add.
diff --git a/src/Specific/X25519/C64/feaddDisplay.log b/src/Specific/X25519/C64/feaddDisplay.log
new file mode 100644
index 000000000..bce3421b2
--- /dev/null
+++ b/src/Specific/X25519/C64/feaddDisplay.log
@@ -0,0 +1,7 @@
+λ x x0 : word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
+ ((x10 + x18), (x11 + x19), (x9 + x17), (x7 + x15), (x5 + x13)))
+(x, x0)%core
+     : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/X25519/C64/feaddDisplay.v b/src/Specific/X25519/C64/feaddDisplay.v
new file mode 100644
index 000000000..e1a666c66
--- /dev/null
+++ b/src/Specific/X25519/C64/feaddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C64.feadd.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display add.
diff --git a/src/Specific/X25519/C64/fecarry.v b/src/Specific/X25519/C64/fecarry.v
new file mode 100644
index 000000000..324aa5ffe
--- /dev/null
+++ b/src/Specific/X25519/C64/fecarry.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C64.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition carry :
+  { carry : feBW_loose -> feBW_tight
+  | forall a, phiBW_tight (carry a) = (phiBW_loose a) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_carry ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions carry.
diff --git a/src/Specific/X25519/C64/fecarryDisplay.log b/src/Specific/X25519/C64/fecarryDisplay.log
new file mode 100644
index 000000000..648dc77cf
--- /dev/null
+++ b/src/Specific/X25519/C64/fecarryDisplay.log
@@ -0,0 +1,27 @@
+λ x : word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x7, x8, x6, x4, x2)%core,
+ uint64_t x9 = (x2 >> 0x33);
+ uint64_t x10 = (x2 & 0x7ffffffffffff);
+ uint64_t x11 = (x9 + x4);
+ uint64_t x12 = (x11 >> 0x33);
+ uint64_t x13 = (x11 & 0x7ffffffffffff);
+ uint64_t x14 = (x12 + x6);
+ uint64_t x15 = (x14 >> 0x33);
+ uint64_t x16 = (x14 & 0x7ffffffffffff);
+ uint64_t x17 = (x15 + x8);
+ uint64_t x18 = (x17 >> 0x33);
+ uint64_t x19 = (x17 & 0x7ffffffffffff);
+ uint64_t x20 = (x18 + x7);
+ uint64_t x21 = (x20 >> 0x33);
+ uint64_t x22 = (x20 & 0x7ffffffffffff);
+ uint64_t x23 = (x10 + (0x13 * x21));
+ uint64_t x24 = (x23 >> 0x33);
+ uint64_t x25 = (x23 & 0x7ffffffffffff);
+ uint64_t x26 = (x24 + x13);
+ uint64_t x27 = (x26 >> 0x33);
+ uint64_t x28 = (x26 & 0x7ffffffffffff);
+ return (Return x22, Return x19, (x27 + x16), Return x28, Return x25))
+x
+     : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/X25519/C64/fecarryDisplay.v b/src/Specific/X25519/C64/fecarryDisplay.v
new file mode 100644
index 000000000..48d97919e
--- /dev/null
+++ b/src/Specific/X25519/C64/fecarryDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C64.fecarry.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display carry.
diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index 7292df912..eeaa4fad0 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
 Definition mul :
-  { mul : feBW -> feBW -> feBW
-  | forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }.
+  { mul : feBW_loose -> feBW_loose -> feBW_tight
+  | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }.
 Proof.
   Set Ltac Profiling.
   Time synthesize_mul ().
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index fa692f559..6939bca51 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
 Definition square :
-  { square : feBW -> feBW
-  | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }.
+  { square : feBW_loose -> feBW_tight
+  | forall a, phiBW_tight (square a) = F.mul (phiBW_loose a) (phiBW_loose a) }.
 Proof.
   Set Ltac Profiling.
   Time synthesize_square ().
diff --git a/src/Specific/X25519/C64/fesub.v b/src/Specific/X25519/C64/fesub.v
new file mode 100644
index 000000000..b17e79366
--- /dev/null
+++ b/src/Specific/X25519/C64/fesub.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C64.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition sub :
+  { sub : feBW_tight -> feBW_tight -> feBW_loose
+  | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_sub ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions sub.
diff --git a/src/Specific/X25519/C64/fesubDisplay.log b/src/Specific/X25519/C64/fesubDisplay.log
new file mode 100644
index 000000000..e85a042f8
--- /dev/null
+++ b/src/Specific/X25519/C64/fesubDisplay.log
@@ -0,0 +1,7 @@
+λ x x0 : word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
+ (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0xfffffffffffda + x5) - x13)))
+(x, x0)%core
+     : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/X25519/C64/fesubDisplay.v b/src/Specific/X25519/C64/fesubDisplay.v
new file mode 100644
index 000000000..2bbf2f589
--- /dev/null
+++ b/src/Specific/X25519/C64/fesubDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C64.fesub.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display sub.
diff --git a/src/Specific/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v
index 2c7fe8b85..0e66bdb73 100644
--- a/src/Specific/X25519/C64/freeze.v
+++ b/src/Specific/X25519/C64/freeze.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
 Definition freeze :
-  { freeze : feBW -> feBW
-  | forall a, phiBW (freeze a) = phiBW a }.
+  { freeze : feBW_tight -> feBW_limbwidths
+  | forall a, phiBW_limbwidths (freeze a) = phiBW_tight a }.
 Proof.
   Set Ltac Profiling.
   Time synthesize_freeze ().
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index fc62c9317..868f10a48 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -9,11 +9,11 @@ Definition xzladderstep :
   | forall x1 Q Q',
       let xz := xzladderstep x1 Q Q' in
       let eval := B.Positional.Fdecode wt in
-      feW_bounded x1
-      -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
-      -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
-      -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
-          /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
+      feW_tight_bounded x1
+      -> feW_tight_bounded (fst Q) /\ feW_tight_bounded (snd Q)
+      -> feW_tight_bounded (fst Q') /\ feW_tight_bounded (snd Q')
+      -> ((feW_tight_bounded (fst (fst xz)) /\ feW_tight_bounded (snd (fst xz)))
+          /\ (feW_tight_bounded (fst (snd xz)) /\ feW_tight_bounded (snd (snd xz))))
          /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (m:=m) (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }.
 Proof.
   Set Ltac Profiling.
diff --git a/src/Specific/X25519/C64/scalarmult.c b/src/Specific/X25519/C64/scalarmult.c
index bde9a9b22..01f81d393 100644
--- a/src/Specific/X25519/C64/scalarmult.c
+++ b/src/Specific/X25519/C64/scalarmult.c
@@ -1,3 +1,5 @@
+/* WARNING: This file was copied from Specific/CurveParameters/X25519_C64/scalarmult.c.
+ If you edit it here, changes will be erased the next time remake_curves.sh is run. */
 // The synthesized parts are from fiat-crypto, copyright MIT 2017.
 // The synthesis framework is released under the MIT license.
 // The non-synthesized parts are from curve25519-donna by Adam Langley (Google):
@@ -41,7 +43,6 @@ typedef unsigned int uint128_t __attribute__((mode(TI)));
 typedef uint8_t u8;
 typedef uint64_t limb;
 typedef limb felem[5];
-//static void crecip(felem out, const felem z);
 
 static void force_inline
 fmul(felem output, const felem in2, const felem in) {
@@ -201,7 +202,6 @@ swap_conditional(limb a[5], limb b[5], limb iswap) {
   }
 }
 
-
 /* Calculates nQ where Q is the x-coordinate of a point on the curve
  *
  *   resultx/resultz: the x coordinate of the resulting curve point (short form)
@@ -223,7 +223,6 @@ cmult(limb *resultx, limb *resultz, const u8 *n, const limb *q) {
     u8 byte = n[31 - i];
     for (j = 0; j < 8; ++j) {
       const limb bit = byte >> 7;
-      // printf("%01d ", bit);
 
       swap_conditional(nqx, nqpqx, bit);
       swap_conditional(nqz, nqpqz, bit);
@@ -249,9 +248,6 @@ cmult(limb *resultx, limb *resultz, const u8 *n, const limb *q) {
       nqpqz2 = t;
 
       byte <<= 1;
-
-      // { felem pr; crecip(pr, nqz); fmul(pr, pr, nqx); uint8_t s[32]; fcontract(s, pr); printf("0x"); for (int i = 31; i>=0; --i) { printf("%02x", s[i]); }; printf(" "); }
-      // { felem pr; crecip(pr, nqpqz); fmul(pr, pr, nqpqx); uint8_t s[32]; fcontract(s, pr); printf("0x"); for (int i = 31; i>=0; --i) { printf("%02x", s[i]); }; printf("\n"); }
     }
   }