4 files changed, 9 insertions, 8 deletions
diff --git a/src/Specific/solinas64_2e336m17/CurveParameters.v b/src/Specific/solinas64_2e336m17/CurveParameters.v
index f3415361d..bfc39f125 100644
--- a/src/Specific/solinas64_2e336m17/CurveParameters.v
+++ b/src/Specific/solinas64_2e336m17/CurveParameters.v
@@ -18,7 +18,7 @@ Definition curve : CurveParameters :=
     a24 := None;
     coef_div_modulus := Some 2%nat;
 
-    goldilocks := Some false;
+    goldilocks := None;
     montgomery := false;
     freeze := Some true;
     ladderstep := false;
@@ -27,7 +27,8 @@ Definition curve : CurveParameters :=
 
     square_code := None;
 
-    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/solinas64_2e336m17/femul.v b/src/Specific/solinas64_2e336m17/femul.v
index ffd402365..9d162fcd0 100644
--- a/src/Specific/solinas64_2e336m17/femul.v
+++ b/src/Specific/solinas64_2e336m17/femul.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e336m17.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/solinas64_2e336m17/fesquare.v b/src/Specific/solinas64_2e336m17/fesquare.v
index 015d213ad..622bb2e2a 100644
--- a/src/Specific/solinas64_2e336m17/fesquare.v
+++ b/src/Specific/solinas64_2e336m17/fesquare.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e336m17.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/solinas64_2e336m17/freeze.v b/src/Specific/solinas64_2e336m17/freeze.v
index a4b6fb12d..7f76aa11c 100644
--- a/src/Specific/solinas64_2e336m17/freeze.v
+++ b/src/Specific/solinas64_2e336m17/freeze.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e336m17.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 ().