From 102904674d12d1791f55a55cb66a334e5c21715a Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 21 Oct 2017 23:43:59 -0400
Subject: Add tight and loose bounds, no carry in add, sub

Following Andres' suggestions to allow making ladderstep from other
synthesis things.

It went though mostly without a hitch, though there were a number of
boilerplate changes needed.
---
 src/Specific/solinas64_2e150m3/CurveParameters.v | 5 +++--
 src/Specific/solinas64_2e150m3/femul.v           | 4 ++--
 src/Specific/solinas64_2e150m3/fesquare.v        | 4 ++--
 src/Specific/solinas64_2e150m3/freeze.v          | 4 ++--
 4 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'src/Specific/solinas64_2e150m3')

diff --git a/src/Specific/solinas64_2e150m3/CurveParameters.v b/src/Specific/solinas64_2e150m3/CurveParameters.v
index 3b5dbdd48..bf35f1164 100644
--- a/src/Specific/solinas64_2e150m3/CurveParameters.v
+++ b/src/Specific/solinas64_2e150m3/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_2e150m3/femul.v b/src/Specific/solinas64_2e150m3/femul.v
index 93dc6f33b..78ea2def5 100644
--- a/src/Specific/solinas64_2e150m3/femul.v
+++ b/src/Specific/solinas64_2e150m3/femul.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e150m3.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_2e150m3/fesquare.v b/src/Specific/solinas64_2e150m3/fesquare.v
index ae9a5f780..1dff45ec2 100644
--- a/src/Specific/solinas64_2e150m3/fesquare.v
+++ b/src/Specific/solinas64_2e150m3/fesquare.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e150m3.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_2e150m3/freeze.v b/src/Specific/solinas64_2e150m3/freeze.v
index a48b95941..cf4aab1df 100644
--- a/src/Specific/solinas64_2e150m3/freeze.v
+++ b/src/Specific/solinas64_2e150m3/freeze.v
@@ -3,8 +3,8 @@ Require Import Crypto.Specific.solinas64_2e150m3.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 ().
-- 
cgit v1.2.3