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.

12 files changed, 556 insertions, 232 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v
index a671c1dfd..789c73bd3 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v
@@ -183,6 +183,25 @@ Section with_args.
       ).
   Defined.
 
+  (* This is kind-of stupid, but we add it for consistency *)
+  Local Definition carry_ext_gen
+    : { f:Z^sz -> Z^sz
+      | let eval := MontgomeryAPI.eval (Z.pos r) in
+        ((forall (A : Z^sz) (_ : small (Z.pos r) A),
+             (eval A < eval m_enc
+              -> montgomery_to_F_gen (eval (f A))
+                 = montgomery_to_F_gen (eval A))))
+         /\ (forall (A : Z^sz) (_ : small (Z.pos r) A),
+                (eval A < eval m_enc
+                 -> 0 <= eval (f A) < eval m_enc))%Z }.
+  Proof.
+    exists (fun A => A).
+    abstract (
+        split; eauto; split; auto;
+        apply MontgomeryAPI.eval_small; auto; lia
+      ).
+  Defined.
+
   Local Definition nonzero_ext_gen
     : { f:Z^sz -> Z
       | let eval := MontgomeryAPI.eval (Z.pos r) in
@@ -347,6 +366,21 @@ Ltac pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map
     ltac:(fun _ => reduce_eq (); reflexivity)
            opp_ext.
 
+Ltac pose_carry_ext r sz m m_enc r' r_big montgomery_to_F carry_ext :=
+  internal_pose_sig_by_eq
+    { f:Z^sz -> Z^sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Z^sz) (_ : small (Z.pos r) A),
+           (eval A < eval m_enc
+            -> montgomery_to_F (eval (f A))
+               = (montgomery_to_F (eval A))))
+       /\ (forall (A : Z^sz) (_ : small (Z.pos r) A),
+              (eval A < eval m_enc
+               -> 0 <= eval (f A) < eval m_enc)))%Z }
+    (@carry_ext_gen r sz m m_enc r' r_big)
+    ltac:(fun _ => reduce_eq (); reflexivity)
+           carry_ext.
+
 Ltac pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext :=
   internal_pose_sig_by_eq
     { f:Z^sz -> Z
@@ -462,6 +496,29 @@ Ltac pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded :=
     ltac:(apply (proj2_sig opp_ext))
            opp_bounded.
 
+Ltac pose_carry_sig r sz m_enc montgomery_to_F carry_ext carry_sig :=
+  cache_term_with_type_by
+    { f:Z^sz -> Z^sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Z^sz) (_ : small (Z.pos r) A),
+        (eval A < eval m_enc
+         -> montgomery_to_F (eval (f A))
+            = (montgomery_to_F (eval A)))%Z }
+    ltac:(idtac;
+          let v := (eval cbv [proj1_sig carry_ext_gen carry_ext sig_by_eq] in (proj1_sig carry_ext)) in
+          (exists v);
+          abstract apply (proj2_sig carry_ext))
+           carry_sig.
+
+Ltac pose_carry_bounded r sz m_enc montgomery_to_F carry_ext carry_sig carry_bounded :=
+  cache_proof_with_type_by
+    (let eval := MontgomeryAPI.eval (Z.pos r) in
+     (forall (A : Z^sz) (_ : small (Z.pos r) A),
+         (eval A < eval m_enc
+          -> 0 <= eval (proj1_sig carry_sig A) < eval m_enc))%Z)
+    ltac:(apply (proj2_sig carry_ext))
+           carry_bounded.
+
 
 Ltac pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig :=
   cache_term_with_type_by
@@ -483,8 +540,8 @@ Ltac pose_ring ring :=
     ring.
 
 (* disable default unused things *)
-Ltac pose_carry_sig carry_sig :=
-  cache_term tt carry_sig.
+(*Ltac pose_carry_sig carry_sig :=
+  cache_term tt carry_sig.*)
 Ltac pose_freeze_sig freeze_sig :=
   cache_term tt freeze_sig.
 Ltac pose_Mxzladderstep_sig Mxzladderstep_sig :=
diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
index 5ade26d76..cefc0733f 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
@@ -9,7 +9,7 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | nonzero_sig.
+  Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | carry_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | carry_bounded | nonzero_sig.
 End TAG.
 
 Ltac add_m' pkg :=
@@ -206,6 +206,21 @@ Ltac add_opp_ext pkg :=
                    Tag.update pkg TAG.opp_ext opp_ext)
     ltac:(fun _ => pkg)
     ().
+Ltac add_carry_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let carry_ext := fresh "carry_ext" in
+                   let carry_ext := pose_carry_ext r sz m m_enc r' r_big montgomery_to_F carry_ext in
+                   Tag.update pkg TAG.carry_ext carry_ext)
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_nonzero_ext pkg :=
   if_montgomery
     pkg
@@ -331,6 +346,33 @@ Ltac add_opp_bounded pkg :=
                    Tag.update pkg TAG.opp_bounded opp_bounded)
     ltac:(fun _ => pkg)
     ().
+Ltac add_carry_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let carry_ext := Tag.get pkg TAG.carry_ext in
+                   let carry_sig := fresh "carry_sig" in
+                   let carry_sig := pose_carry_sig r sz m_enc montgomery_to_F carry_ext carry_sig in
+                   Tag.update pkg TAG.carry_sig carry_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_carry_bounded pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let carry_ext := Tag.get pkg TAG.carry_ext in
+                   let carry_sig := Tag.get pkg TAG.carry_sig in
+                   let carry_bounded := fresh "carry_bounded" in
+                   let carry_bounded := pose_carry_bounded r sz m_enc montgomery_to_F carry_ext carry_sig carry_bounded in
+                   Tag.update pkg TAG.carry_bounded carry_bounded)
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_nonzero_sig pkg :=
   if_montgomery
     pkg
@@ -353,14 +395,6 @@ Ltac add_ring pkg :=
                    Tag.update pkg TAG.ring ring)
     ltac:(fun _ => pkg)
     ().
-Ltac add_carry_sig pkg :=
-  if_montgomery
-    pkg
-    ltac:(fun _ => let carry_sig := fresh "carry_sig" in
-                   let carry_sig := pose_carry_sig carry_sig in
-                   Tag.update pkg TAG.carry_sig carry_sig)
-    ltac:(fun _ => pkg)
-    ().
 Ltac add_freeze_sig pkg :=
   if_montgomery
     pkg
@@ -393,6 +427,7 @@ Ltac add_Montgomery_package pkg :=
   let pkg := add_add_ext pkg in
   let pkg := add_sub_ext pkg in
   let pkg := add_opp_ext pkg in
+  let pkg := add_carry_ext pkg in
   let pkg := add_nonzero_ext pkg in
   let pkg := add_mul_sig pkg in
   let pkg := add_mul_bounded pkg in
@@ -402,9 +437,10 @@ Ltac add_Montgomery_package pkg :=
   let pkg := add_sub_bounded pkg in
   let pkg := add_opp_sig pkg in
   let pkg := add_opp_bounded pkg in
+  let pkg := add_carry_sig pkg in
+  let pkg := add_carry_bounded pkg in
   let pkg := add_nonzero_sig pkg in
   let pkg := add_ring pkg in
-  let pkg := add_carry_sig pkg in
   let pkg := add_freeze_sig pkg in
   let pkg := add_Mxzladderstep_sig pkg in
   Tag.strip_subst_local pkg.
@@ -443,6 +479,8 @@ Module MakeMontgomeryPackage (PKG : PrePackage).
   Notation sub_ext := (ltac:(let v := get_sub_ext () in exact v)) (only parsing).
   Ltac get_opp_ext _ := get TAG.opp_ext.
   Notation opp_ext := (ltac:(let v := get_opp_ext () in exact v)) (only parsing).
+  Ltac get_carry_ext _ := get TAG.carry_ext.
+  Notation carry_ext := (ltac:(let v := get_carry_ext () in exact v)) (only parsing).
   Ltac get_nonzero_ext _ := get TAG.nonzero_ext.
   Notation nonzero_ext := (ltac:(let v := get_nonzero_ext () in exact v)) (only parsing).
   Ltac get_mul_bounded _ := get TAG.mul_bounded.
@@ -453,6 +491,8 @@ Module MakeMontgomeryPackage (PKG : PrePackage).
   Notation sub_bounded := (ltac:(let v := get_sub_bounded () in exact v)) (only parsing).
   Ltac get_opp_bounded _ := get TAG.opp_bounded.
   Notation opp_bounded := (ltac:(let v := get_opp_bounded () in exact v)) (only parsing).
+  Ltac get_carry_bounded _ := get TAG.carry_bounded.
+  Notation carry_bounded := (ltac:(let v := get_carry_bounded () in exact v)) (only parsing).
   Ltac get_nonzero_sig _ := get TAG.nonzero_sig.
   Notation nonzero_sig := (ltac:(let v := get_nonzero_sig () in exact v)) (only parsing).
 End MakeMontgomeryPackage.
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 50ff2278b..ec080491d 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -12,7 +12,7 @@ Local Set Primitive Projections.
 Module Export Notations := RawCurveParameters.Notations.
 
 Module TAG. (* namespacing *)
-  Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | freeze | ladderstep | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
+  Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | freeze | ladderstep | upper_bound_of_exponent_tight | upper_bound_of_exponent_loose | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
 End TAG.
 
 Module Export CurveParameters.
@@ -48,7 +48,8 @@ Module Export CurveParameters.
 
       mul_code : option (Z^sz -> Z^sz -> Z^sz);
       square_code : option (Z^sz -> Z^sz);
-      upper_bound_of_exponent : Z -> Z;
+      upper_bound_of_exponent_tight : Z -> Z;
+      upper_bound_of_exponent_loose : Z -> Z;
       allowable_bit_widths : list nat;
       freeze_allowable_bit_widths : list nat;
       modinv_fuel : nat
@@ -69,7 +70,8 @@ Module Export CurveParameters.
               ladderstep
               mul_code
               square_code
-              upper_bound_of_exponent
+              upper_bound_of_exponent_tight
+              upper_bound_of_exponent_loose
               allowable_bit_widths
               freeze_allowable_bit_widths
               modinv_fuel].
@@ -118,7 +120,17 @@ Module Export CurveParameters.
                    then [8]
                    else nil)
                     ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat in
-
+        let upper_bound_of_exponent_tight
+            := defaulted (RawCurveParameters.upper_bound_of_exponent_tight CP)
+                         (if montgomery
+                          then (fun exp => (2^exp - 1)%Z)
+                          else (fun exp => (2^exp + 2^(exp-3))%Z))
+        (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) in
+        let upper_bound_of_exponent_loose
+            := defaulted (RawCurveParameters.upper_bound_of_exponent_loose CP)
+                         (if montgomery
+                          then (fun exp => (2^exp - 1)%Z)
+                          else (fun exp => (3 * upper_bound_of_exponent_tight exp)%Z)) in
         {|
           sz := sz;
           base := base;
@@ -136,12 +148,8 @@ Module Export CurveParameters.
 
           mul_code := RawCurveParameters.mul_code CP;
           square_code := RawCurveParameters.square_code CP;
-          upper_bound_of_exponent
-          := defaulted (RawCurveParameters.upper_bound_of_exponent CP)
-                       (if montgomery
-                        then (fun exp => (2^exp - 1)%Z)
-                        else (fun exp => (2^exp + 2^(exp-3))%Z));
-          (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
+          upper_bound_of_exponent_tight := upper_bound_of_exponent_tight;
+          upper_bound_of_exponent_loose := upper_bound_of_exponent_loose;
 
           allowable_bit_widths := allowable_bit_widths;
           freeze_allowable_bit_widths
@@ -174,7 +182,8 @@ Module Export CurveParameters.
           ladderstep := ?ladderstep';
           mul_code := ?mul_code';
           square_code := ?square_code';
-          upper_bound_of_exponent := ?upper_bound_of_exponent';
+          upper_bound_of_exponent_tight := ?upper_bound_of_exponent_tight';
+          upper_bound_of_exponent_loose := ?upper_bound_of_exponent_loose';
           allowable_bit_widths := ?allowable_bit_widths';
           freeze_allowable_bit_widths := ?freeze_allowable_bit_widths';
           modinv_fuel := ?modinv_fuel'
@@ -205,7 +214,8 @@ Module Export CurveParameters.
                     ladderstep := ladderstep';
                     mul_code := mul_code';
                     square_code := square_code';
-                    upper_bound_of_exponent := upper_bound_of_exponent';
+                    upper_bound_of_exponent_tight := upper_bound_of_exponent_tight';
+                    upper_bound_of_exponent_loose := upper_bound_of_exponent_loose';
                     allowable_bit_widths := allowable_bit_widths';
                     freeze_allowable_bit_widths := freeze_allowable_bit_widths';
                     modinv_fuel := modinv_fuel'
@@ -246,8 +256,10 @@ Module Export CurveParameters.
     internal_pose_of_CP CP CurveParameters.allowable_bit_widths allowable_bit_widths.
   Ltac pose_freeze_allowable_bit_widths CP freeze_allowable_bit_widths :=
     internal_pose_of_CP CP CurveParameters.freeze_allowable_bit_widths freeze_allowable_bit_widths.
-  Ltac pose_upper_bound_of_exponent CP upper_bound_of_exponent :=
-    internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent upper_bound_of_exponent.
+  Ltac pose_upper_bound_of_exponent_tight CP upper_bound_of_exponent_tight :=
+    internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent_tight upper_bound_of_exponent_tight.
+  Ltac pose_upper_bound_of_exponent_loose CP upper_bound_of_exponent_loose :=
+    internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent_loose upper_bound_of_exponent_loose.
   Ltac pose_modinv_fuel CP modinv_fuel :=
     internal_pose_of_CP CP CurveParameters.modinv_fuel modinv_fuel.
   Ltac pose_mul_code CP mul_code :=
@@ -340,11 +352,17 @@ Module Export CurveParameters.
     let freeze_allowable_bit_widths := pose_freeze_allowable_bit_widths CP freeze_allowable_bit_widths in
     Tag.update pkg TAG.freeze_allowable_bit_widths freeze_allowable_bit_widths.
 
-  Ltac add_upper_bound_of_exponent pkg :=
+  Ltac add_upper_bound_of_exponent_tight pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let upper_bound_of_exponent_tight := fresh "upper_bound_of_exponent_tight" in
+    let upper_bound_of_exponent_tight := pose_upper_bound_of_exponent_tight CP upper_bound_of_exponent_tight in
+    Tag.update pkg TAG.upper_bound_of_exponent_tight upper_bound_of_exponent_tight.
+
+  Ltac add_upper_bound_of_exponent_loose pkg :=
     let CP := Tag.get pkg TAG.CP in
-    let upper_bound_of_exponent := fresh "upper_bound_of_exponent" in
-    let upper_bound_of_exponent := pose_upper_bound_of_exponent CP upper_bound_of_exponent in
-    Tag.update pkg TAG.upper_bound_of_exponent upper_bound_of_exponent.
+    let upper_bound_of_exponent_loose := fresh "upper_bound_of_exponent_loose" in
+    let upper_bound_of_exponent_loose := pose_upper_bound_of_exponent_loose CP upper_bound_of_exponent_loose in
+    Tag.update pkg TAG.upper_bound_of_exponent_loose upper_bound_of_exponent_loose.
 
   Ltac add_modinv_fuel pkg :=
     let CP := Tag.get pkg TAG.CP in
@@ -379,7 +397,8 @@ Module Export CurveParameters.
     let pkg := add_ladderstep pkg in
     let pkg := add_allowable_bit_widths pkg in
     let pkg := add_freeze_allowable_bit_widths pkg in
-    let pkg := add_upper_bound_of_exponent pkg in
+    let pkg := add_upper_bound_of_exponent_tight pkg in
+    let pkg := add_upper_bound_of_exponent_loose pkg in
     let pkg := add_modinv_fuel pkg in
     let pkg := add_mul_code pkg in
     let pkg := add_square_code pkg in
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
index 7b960a09d..836e75489 100644
--- a/src/Specific/Framework/CurveParametersPackage.v
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -67,8 +67,10 @@ Module MakeCurveParametersPackage (PKG : PrePackage).
   Notation allowable_bit_widths := (ltac:(let v := get_allowable_bit_widths () in exact v)) (only parsing).
   Ltac get_freeze_allowable_bit_widths _ := get TAG.freeze_allowable_bit_widths.
   Notation freeze_allowable_bit_widths := (ltac:(let v := get_freeze_allowable_bit_widths () in exact v)) (only parsing).
-  Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent.
-  Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
+  Ltac get_upper_bound_of_exponent_tight _ := get TAG.upper_bound_of_exponent_tight.
+  Notation upper_bound_of_exponent_tight := (ltac:(let v := get_upper_bound_of_exponent_tight () in exact v)) (only parsing).
+  Ltac get_upper_bound_of_exponent_loose _ := get TAG.upper_bound_of_exponent_loose.
+  Notation upper_bound_of_exponent_loose := (ltac:(let v := get_upper_bound_of_exponent_loose () in exact v)) (only parsing).
   Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
   Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
   Ltac get_mul_code _ := get TAG.mul_code.
diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
index dbfc38a7d..1ccbb72a7 100644
--- a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
+++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
@@ -137,7 +137,7 @@ Ltac get_proj2_sig_map_arg _ :=
     => let P := get_proj2_sig_map_arg_helper E in
        uconstr:(fun e : T => P)
   end.
-Ltac get_phi_for_preglue _ :=
+Ltac get_phi1_for_preglue _ :=
   lazymatch goal with
   | [ |- { e | @?E e } ]
     => lazymatch E with
@@ -147,9 +147,22 @@ Ltac get_phi_for_preglue _ :=
          => phi
        end
   end.
+Ltac get_phi2_for_preglue _ :=
+  lazymatch goal with
+  | [ |- { e | @?E e } ]
+    => lazymatch E with
+       | context[_ = ?f (Tuple.map ?phi _)]
+         => phi
+       | context[_ = ?f (?phi _)]
+         => phi
+       | context[_ = ?phi _]
+         => phi
+       end
+  end.
 Ltac start_preglue :=
   apply_lift_sig; intros; cbv beta iota zeta;
-  let phi := get_phi_for_preglue () in
+  let phi := get_phi1_for_preglue () in
+  let phi2 := get_phi2_for_preglue () in
   let P' := get_proj2_sig_map_arg () in
   refine (proj2_sig_map (P:=P') _ _);
   [ let FINAL := fresh "FINAL" in
@@ -158,11 +171,11 @@ Ltac start_preglue :=
     repeat (let H := fresh in intro H; specialize (FINAL H));
     lazymatch goal with
     | [ |- ?phi _ = ?RHS ]
-      => refine (@eq_trans _ _ _ RHS FINAL _); cbv [phi]; clear a FINAL
+      => refine (@eq_trans _ _ _ RHS FINAL _); cbv [phi phi2]; clear a FINAL
     | [ |- _ /\ Tuple.map (Tuple.map ?phi) _ = _ ]
-      => split; cbv [phi]; [ refine (proj1 FINAL); shelve | ]
+      => split; cbv [phi phi2]; [ refine (proj1 FINAL); shelve | ]
     end
-  | cbv [phi] ].
+  | cbv [phi phi2] ].
 Ltac do_set_sig f_sig :=
   let fZ := fresh f_sig in
   set (fZ := proj1_sig f_sig);
diff --git a/src/Specific/Framework/MontgomeryReificationTypes.v b/src/Specific/Framework/MontgomeryReificationTypes.v
index 1b476dbe4..e25211e71 100644
--- a/src/Specific/Framework/MontgomeryReificationTypes.v
+++ b/src/Specific/Framework/MontgomeryReificationTypes.v
@@ -17,31 +17,31 @@ Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
 Require Import Crypto.Util.Tactics.PoseTermWithName.
 Require Import Crypto.Util.Tactics.CacheTerm.
 
-Ltac pose_meval feBW r meval :=
+Ltac pose_meval feBW_tight r meval :=
   cache_term_with_type_by
-    (feBW -> Z)
-    ltac:(exact (fun x : feBW => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x)))
+    (feBW_tight -> Z)
+    ltac:(exact (fun x : feBW_tight => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x)))
            meval.
 
-Ltac pose_feBW_small sz feBW meval r m_enc feBW_small :=
+Ltac pose_feBW_small sz feBW_tight meval r m_enc feBW_small :=
   cache_term
-    { v : feBW | meval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc }
+    { v : feBW_tight | meval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc }
     feBW_small.
 
-Ltac pose_feBW_of_feBW_small feBW feBW_small feBW_of_feBW_small :=
+Ltac pose_feBW_tight_of_feBW_small feBW_tight feBW_small feBW_tight_of_feBW_small :=
   cache_term_with_type_by
-    (feBW_small -> feBW)
+    (feBW_small -> feBW_tight)
     ltac:(refine (@proj1_sig _ _))
-           feBW_of_feBW_small.
+           feBW_tight_of_feBW_small.
 
-Ltac pose_phiM feBW m meval montgomery_to_F phiM :=
+Ltac pose_phiM feBW_tight m meval montgomery_to_F phiM :=
   cache_term_with_type_by
-    (feBW -> F m)
-    ltac:(exact (fun x : feBW => montgomery_to_F (meval x)))
+    (feBW_tight -> F m)
+    ltac:(exact (fun x : feBW_tight => montgomery_to_F (meval x)))
            phiM.
 
-Ltac pose_phiM_small feBW_small feBW_of_feBW_small m meval montgomery_to_F phiM_small :=
+Ltac pose_phiM_small feBW_small feBW_tight_of_feBW_small m meval montgomery_to_F phiM_small :=
   cache_term_with_type_by
     (feBW_small -> F m)
-    ltac:(exact (fun x : feBW_small => montgomery_to_F (meval (feBW_of_feBW_small x))))
+    ltac:(exact (fun x : feBW_small => montgomery_to_F (meval (feBW_tight_of_feBW_small x))))
            phiM_small.
diff --git a/src/Specific/Framework/MontgomeryReificationTypesPackage.v b/src/Specific/Framework/MontgomeryReificationTypesPackage.v
index 6f9364d6e..1be4afda5 100644
--- a/src/Specific/Framework/MontgomeryReificationTypesPackage.v
+++ b/src/Specific/Framework/MontgomeryReificationTypesPackage.v
@@ -8,16 +8,16 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := meval | feBW_small | feBW_of_feBW_small | phiM | phiM_small.
+  Inductive tags := meval | feBW_small | feBW_tight_of_feBW_small | phiM | phiM_small.
 End TAG.
 
 Ltac add_meval pkg :=
   if_montgomery
     pkg
-    ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in
+    ltac:(fun _ => let feBW_tight := Tag.get pkg TAG.feBW_tight in
                    let r := Tag.get pkg TAG.r in
                    let meval := fresh "meval" in
-                   let meval := pose_meval feBW r meval in
+                   let meval := pose_meval feBW_tight r meval in
                    Tag.update pkg TAG.meval meval)
     ltac:(fun _ => pkg)
     ().
@@ -25,34 +25,34 @@ Ltac add_feBW_small pkg :=
   if_montgomery
     pkg
     ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                   let feBW := Tag.get pkg TAG.feBW in
+                   let feBW_tight := Tag.get pkg TAG.feBW_tight in
                    let meval := Tag.get pkg TAG.meval in
                    let r := Tag.get pkg TAG.r in
                    let m_enc := Tag.get pkg TAG.m_enc in
                    let feBW_small := fresh "feBW_small" in
-                   let feBW_small := pose_feBW_small sz feBW meval r m_enc feBW_small in
+                   let feBW_small := pose_feBW_small sz feBW_tight meval r m_enc feBW_small in
                    Tag.update pkg TAG.feBW_small feBW_small)
     ltac:(fun _ => pkg)
     ().
-Ltac add_feBW_of_feBW_small pkg :=
+Ltac add_feBW_tight_of_feBW_small pkg :=
   if_montgomery
     pkg
-    ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in
+    ltac:(fun _ => let feBW_tight := Tag.get pkg TAG.feBW_tight in
                    let feBW_small := Tag.get pkg TAG.feBW_small in
-                   let feBW_of_feBW_small := fresh "feBW_of_feBW_small" in
-                   let feBW_of_feBW_small := pose_feBW_of_feBW_small feBW feBW_small feBW_of_feBW_small in
-                   Tag.update pkg TAG.feBW_of_feBW_small feBW_of_feBW_small)
+                   let feBW_tight_of_feBW_small := fresh "feBW_tight_of_feBW_small" in
+                   let feBW_tight_of_feBW_small := pose_feBW_tight_of_feBW_small feBW_tight feBW_small feBW_tight_of_feBW_small in
+                   Tag.update pkg TAG.feBW_tight_of_feBW_small feBW_tight_of_feBW_small)
     ltac:(fun _ => pkg)
     ().
 Ltac add_phiM pkg :=
   if_montgomery
     pkg
-    ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in
+    ltac:(fun _ => let feBW_tight := Tag.get pkg TAG.feBW_tight in
                    let m := Tag.get pkg TAG.m in
                    let meval := Tag.get pkg TAG.meval in
                    let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
                    let phiM := fresh "phiM" in
-                   let phiM := pose_phiM feBW m meval montgomery_to_F phiM in
+                   let phiM := pose_phiM feBW_tight m meval montgomery_to_F phiM in
                    Tag.update pkg TAG.phiM phiM)
     ltac:(fun _ => pkg)
     ().
@@ -60,19 +60,19 @@ Ltac add_phiM_small pkg :=
   if_montgomery
     pkg
     ltac:(fun _ => let feBW_small := Tag.get pkg TAG.feBW_small in
-                   let feBW_of_feBW_small := Tag.get pkg TAG.feBW_of_feBW_small in
+                   let feBW_tight_of_feBW_small := Tag.get pkg TAG.feBW_tight_of_feBW_small in
                    let m := Tag.get pkg TAG.m in
                    let meval := Tag.get pkg TAG.meval in
                    let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
                    let phiM_small := fresh "phiM_small" in
-                   let phiM_small := pose_phiM_small feBW_small feBW_of_feBW_small m meval montgomery_to_F phiM_small in
+                   let phiM_small := pose_phiM_small feBW_small feBW_tight_of_feBW_small m meval montgomery_to_F phiM_small in
                    Tag.update pkg TAG.phiM_small phiM_small)
     ltac:(fun _ => pkg)
     ().
 Ltac add_MontgomeryReificationTypes_package pkg :=
   let pkg := add_meval pkg in
   let pkg := add_feBW_small pkg in
-  let pkg := add_feBW_of_feBW_small pkg in
+  let pkg := add_feBW_tight_of_feBW_small pkg in
   let pkg := add_phiM pkg in
   let pkg := add_phiM_small pkg in
   Tag.strip_subst_local pkg.
@@ -85,8 +85,8 @@ Module MakeMontgomeryReificationTypesPackage (PKG : PrePackage).
   Notation meval := (ltac:(let v := get_meval () in exact v)) (only parsing).
   Ltac get_feBW_small _ := get TAG.feBW_small.
   Notation feBW_small := (ltac:(let v := get_feBW_small () in exact v)) (only parsing).
-  Ltac get_feBW_of_feBW_small _ := get TAG.feBW_of_feBW_small.
-  Notation feBW_of_feBW_small := (ltac:(let v := get_feBW_of_feBW_small () in exact v)) (only parsing).
+  Ltac get_feBW_tight_of_feBW_small _ := get TAG.feBW_tight_of_feBW_small.
+  Notation feBW_tight_of_feBW_small := (ltac:(let v := get_feBW_tight_of_feBW_small () in exact v)) (only parsing).
   Ltac get_phiM _ := get TAG.phiM.
   Notation phiM := (ltac:(let v := get_phiM () in exact v)) (only parsing).
   Ltac get_phiM_small _ := get TAG.phiM_small.
diff --git a/src/Specific/Framework/RawCurveParameters.v b/src/Specific/Framework/RawCurveParameters.v
index a3f3dd5b8..ae3040b10 100644
--- a/src/Specific/Framework/RawCurveParameters.v
+++ b/src/Specific/Framework/RawCurveParameters.v
@@ -37,8 +37,10 @@ Record CurveParameters :=
 
     mul_code : option (Z^sz -> Z^sz -> Z^sz);
     square_code : option (Z^sz -> Z^sz);
-    upper_bound_of_exponent
+    upper_bound_of_exponent_tight
     : option (Z -> Z) (* defaults to [fun exp => 2^exp + 2^(exp-3)] for non-montgomery, [fun exp => 2^exp - 1] for montgomery *);
+    upper_bound_of_exponent_loose
+    : option (Z -> Z) (* defaults to [3 * upper_bound_of_exponent_tight] for non-montgomery, [fun exp => 2^exp - 1] for montgomery *);
     allowable_bit_widths
     : option (list nat) (* defaults to [bitwidth :: 2*bitwidth :: nil] *);
     freeze_extra_allowable_bit_widths
@@ -61,7 +63,8 @@ Declare Reduction cbv_RawCurveParameters
             ladderstep
             mul_code
             square_code
-            upper_bound_of_exponent
+            upper_bound_of_exponent_tight
+            upper_bound_of_exponent_loose
             allowable_bit_widths
             freeze_extra_allowable_bit_widths
             modinv_fuel].
diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v
index 879c20aa9..3b2d68b0b 100644
--- a/src/Specific/Framework/ReificationTypes.v
+++ b/src/Specific/Framework/ReificationTypes.v
@@ -10,6 +10,8 @@ Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Decidable.
 
 Require Import Crypto.Util.Tactics.PoseTermWithName.
@@ -33,13 +35,19 @@ Ltac pose_local_bounds_exp sz limb_widths bounds_exp :=
                (Tuple.from_list sz limb_widths eq_refl))
            bounds_exp.
 
-Ltac pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds :=
+Ltac internal_pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds :=
   let b_of := get_b_of upper_bound_of_exponent in
   pose_term_with_type
     (Tuple.tuple zrange sz)
     ltac:(fun _ => eval compute in
                (Tuple.map (fun e => b_of e) bounds_exp))
            bounds.
+Ltac pose_local_bounds_tight sz upper_bound_of_exponent_tight bounds_exp bounds_tight :=
+  internal_pose_local_bounds sz upper_bound_of_exponent_tight bounds_exp bounds_tight.
+Ltac pose_local_bounds_loose sz upper_bound_of_exponent_loose bounds_exp bounds_loose :=
+  internal_pose_local_bounds sz upper_bound_of_exponent_loose bounds_exp bounds_loose.
+Ltac pose_local_bounds_limbwidths sz bounds_exp bounds_limbwidths :=
+  internal_pose_local_bounds sz (fun exp => (2^exp - 1)%Z) bounds_exp bounds_limbwidths.
 
 Ltac pose_bound1 r bound1 :=
   cache_term_with_type_by
@@ -69,16 +77,73 @@ Ltac pose_feW sz lgbitwidth feW :=
     Type
     ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v)
            feW.
-Ltac pose_feW_bounded feW bounds feW_bounded :=
+Ltac internal_pose_feW_bounded feW bounds feW_bounded :=
   cache_term_with_type_by
     (feW -> Prop)
     ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v)
            feW_bounded.
-Ltac pose_feBW sz adjusted_bitwidth' bounds feBW :=
+Ltac pose_feW_tight_bounded feW bounds_tight feW_tight_bounded :=
+  internal_pose_feW_bounded feW bounds_tight feW_tight_bounded.
+Ltac pose_feW_loose_bounded feW bounds_loose feW_loose_bounded :=
+  internal_pose_feW_bounded feW bounds_loose feW_loose_bounded.
+Ltac pose_feW_limbwidths_bounded feW bounds_limbwidths feW_limbwidths_bounded :=
+  internal_pose_feW_bounded feW bounds_limbwidths feW_limbwidths_bounded.
+
+Ltac internal_pose_feBW sz adjusted_bitwidth' bounds feBW :=
   cache_term_with_type_by
     Type
     ltac:(let v := eval cbv [adjusted_bitwidth' bounds] in (BoundedWord sz adjusted_bitwidth' bounds) in exact v)
            feBW.
+Ltac pose_feBW_tight sz adjusted_bitwidth' bounds_tight feBW_tight :=
+  internal_pose_feBW sz adjusted_bitwidth' bounds_tight feBW_tight.
+Ltac pose_feBW_loose sz adjusted_bitwidth' bounds_loose feBW_loose :=
+  internal_pose_feBW sz adjusted_bitwidth' bounds_loose feBW_loose.
+Ltac pose_feBW_limbwidths sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths :=
+  internal_pose_feBW sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths.
+
+Lemma relax'_pf {sz in_bounds out_bounds} {v : tuple Z sz}
+      (Htight : fieldwiseb is_tighter_than_bool in_bounds out_bounds = true)
+  : is_bounded_by None in_bounds v -> is_bounded_by None out_bounds v.
+Proof.
+  destruct sz as [|sz]; simpl in *; trivial.
+  induction sz as [|sz IHsz]; simpl in *;
+    repeat first [ exact I
+                 | progress destruct_head'_prod
+                 | progress destruct_head' zrange
+                 | progress cbv [is_tighter_than_bool] in *
+                 | progress split_andb
+                 | progress Z.ltb_to_lt
+                 | progress cbn [fst snd ZRange.lower ZRange.upper] in *
+                 | progress destruct_head_hnf' and
+                 | progress intros
+                 | apply conj
+                 | omega
+                 | solve [ eauto ] ].
+Qed.
+
+Definition relax' {sz adjusted_bitwidth'} {in_bounds out_bounds}
+           (Htight : Tuple.fieldwiseb ZRange.is_tighter_than_bool in_bounds out_bounds = true)
+  : BoundedWord sz adjusted_bitwidth' in_bounds
+    -> BoundedWord sz adjusted_bitwidth' out_bounds
+  := fun w => exist _ (proj1_sig w) (relax'_pf Htight (proj2_sig w)).
+
+Ltac internal_pose_feBW_relax sz feBW_in feBW_out feBW_relax :=
+  cache_term_with_type_by
+    (feBW_in -> feBW_out)
+    ltac:(refine (@relax' sz _ _ _ _);
+          lazymatch goal with
+          | [ |- fieldwiseb is_tighter_than_bool ?in_bounds ?out_bounds = true ]
+            => try cbv [in_bounds];
+               try cbv [out_bounds]
+          end;
+          abstract vm_cast_no_check (eq_refl true))
+           feBW_relax.
+Ltac pose_feBW_relax sz feBW_tight feBW_loose feBW_relax :=
+  internal_pose_feBW_relax sz feBW_tight feBW_loose feBW_relax.
+Ltac pose_feBW_relax_limbwidths_to_tight sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight :=
+  internal_pose_feBW_relax sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight.
+Ltac pose_feBW_relax_limbwidths_to_loose sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose :=
+  internal_pose_feBW_relax sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose.
 
 Lemma feBW_bounded_helper'
       sz adjusted_bitwidth' bounds
@@ -130,25 +195,36 @@ Proof.
     assumption.
 Qed.
 
-Ltac pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
-  match (eval vm_compute in freeze) with
+Ltac internal_pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
+  lazymatch (eval vm_compute in freeze) with
   | true
     => cache_proof_with_type_by
          (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < 2 * Z.pos m)
          ltac:(apply (@feBW_bounded_helper sz adjusted_bitwidth' bounds wt wt_nonneg);
-               vm_compute; clear; split; congruence)
+               cbv -[Z.lt Z.le];
+               clear; vm_decide)
                 feBW_bounded
   | false
     => cache_term tt feBW_bounded
   end.
+Ltac pose_feBW_tight_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded :=
+  internal_pose_feBW_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded.
+Ltac pose_feBW_limbwidths_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded :=
+  internal_pose_feBW_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded.
 
 Ltac pose_phiW feW m wt phiW :=
   cache_term_with_type_by
     (feW -> F m)
     ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x)))
            phiW.
-Ltac pose_phiBW feBW m wt phiBW :=
+Ltac internal_pose_phiBW feBW m wt phiBW :=
   cache_term_with_type_by
     (feBW -> F m)
     ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
            phiBW.
+Ltac pose_phiBW_tight feBW_tight m wt phiBW_tight :=
+  internal_pose_phiBW feBW_tight m wt phiBW_tight.
+Ltac pose_phiBW_loose feBW_loose m wt phiBW_loose :=
+  internal_pose_phiBW feBW_loose m wt phiBW_loose.
+Ltac pose_phiBW_limbwidths feBW_limbwidths m wt phiBW_limbwidths :=
+  internal_pose_phiBW feBW_limbwidths m wt phiBW_limbwidths.
diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v
index 55e3a2cb3..d10d72202 100644
--- a/src/Specific/Framework/ReificationTypesPackage.v
+++ b/src/Specific/Framework/ReificationTypesPackage.v
@@ -6,7 +6,7 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := limb_widths | bounds_exp | bounds | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_bounded | feBW | feBW_bounded | phiW | phiBW.
+  Inductive tags := limb_widths | bounds_exp | bounds_tight | bounds_loose | bounds_limbwidths | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_tight_bounded | feW_loose_bounded | feW_limbwidths_bounded | feBW_tight | feBW_loose | feBW_limbwidths | feBW_relax | feBW_relax_limbwidths_to_tight | feBW_relax_limbwidths_to_loose | feBW_tight_bounded | feBW_limbwidths_bounded | phiW | phiBW_tight | phiBW_loose | phiBW_limbwidths.
 End TAG.
 
 Ltac add_limb_widths pkg :=
@@ -23,13 +23,28 @@ Ltac add_bounds_exp pkg :=
   let bounds_exp := pose_local_bounds_exp sz limb_widths bounds_exp in
   Tag.local_update pkg TAG.bounds_exp bounds_exp.
 
-Ltac add_bounds pkg :=
+Ltac add_bounds_tight pkg :=
   let sz := Tag.get pkg TAG.sz in
-  let upper_bound_of_exponent := Tag.get pkg TAG.upper_bound_of_exponent in
+  let upper_bound_of_exponent_tight := Tag.get pkg TAG.upper_bound_of_exponent_tight in
   let bounds_exp := Tag.get pkg TAG.bounds_exp in
-  let bounds := fresh "bounds" in
-  let bounds := pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds in
-  Tag.local_update pkg TAG.bounds bounds.
+  let bounds_tight := fresh "bounds_tight" in
+  let bounds_tight := pose_local_bounds_tight sz upper_bound_of_exponent_tight bounds_exp bounds_tight in
+  Tag.local_update pkg TAG.bounds_tight bounds_tight.
+
+Ltac add_bounds_loose pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let upper_bound_of_exponent_loose := Tag.get pkg TAG.upper_bound_of_exponent_loose in
+  let bounds_exp := Tag.get pkg TAG.bounds_exp in
+  let bounds_loose := fresh "bounds_loose" in
+  let bounds_loose := pose_local_bounds_loose sz upper_bound_of_exponent_loose bounds_exp bounds_loose in
+  Tag.local_update pkg TAG.bounds_loose bounds_loose.
+
+Ltac add_bounds_limbwidths pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let bounds_exp := Tag.get pkg TAG.bounds_exp in
+  let bounds_limbwidths := fresh "bounds_limbwidths" in
+  let bounds_limbwidths := pose_local_bounds_limbwidths sz bounds_exp bounds_limbwidths in
+  Tag.local_update pkg TAG.bounds_limbwidths bounds_limbwidths.
 
 Ltac add_bound1 pkg :=
   let r := Tag.get pkg TAG.r in
@@ -68,33 +83,100 @@ Ltac add_feW pkg :=
   let feW := pose_feW sz lgbitwidth feW in
   Tag.update pkg TAG.feW feW.
 
-Ltac add_feW_bounded pkg :=
+Ltac add_feW_tight_bounded pkg :=
+  let feW := Tag.get pkg TAG.feW in
+  let bounds_tight := Tag.get pkg TAG.bounds_tight in
+  let feW_tight_bounded := fresh "feW_tight_bounded" in
+  let feW_tight_bounded := pose_feW_tight_bounded feW bounds_tight feW_tight_bounded in
+  Tag.update pkg TAG.feW_tight_bounded feW_tight_bounded.
+
+Ltac add_feW_loose_bounded pkg :=
+  let feW := Tag.get pkg TAG.feW in
+  let bounds_loose := Tag.get pkg TAG.bounds_loose in
+  let feW_loose_bounded := fresh "feW_loose_bounded" in
+  let feW_loose_bounded := pose_feW_loose_bounded feW bounds_loose feW_loose_bounded in
+  Tag.update pkg TAG.feW_loose_bounded feW_loose_bounded.
+
+Ltac add_feW_limbwidths_bounded pkg :=
   let feW := Tag.get pkg TAG.feW in
-  let bounds := Tag.get pkg TAG.bounds in
-  let feW_bounded := fresh "feW_bounded" in
-  let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
-  Tag.update pkg TAG.feW_bounded feW_bounded.
+  let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
+  let feW_limbwidths_bounded := fresh "feW_limbwidths_bounded" in
+  let feW_limbwidths_bounded := pose_feW_limbwidths_bounded feW bounds_limbwidths feW_limbwidths_bounded in
+  Tag.update pkg TAG.feW_limbwidths_bounded feW_limbwidths_bounded.
 
-Ltac add_feBW pkg :=
+Ltac add_feBW_tight pkg :=
   let sz := Tag.get pkg TAG.sz in
   let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
-  let bounds := Tag.get pkg TAG.bounds in
-  let feBW := fresh "feBW" in
-  let feBW := pose_feBW sz adjusted_bitwidth' bounds feBW in
-  Tag.update pkg TAG.feBW feBW.
+  let bounds_tight := Tag.get pkg TAG.bounds_tight in
+  let feBW_tight := fresh "feBW_tight" in
+  let feBW_tight := pose_feBW_tight sz adjusted_bitwidth' bounds_tight feBW_tight in
+  Tag.update pkg TAG.feBW_tight feBW_tight.
+
+Ltac add_feBW_loose pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let bounds_loose := Tag.get pkg TAG.bounds_loose in
+  let feBW_loose := fresh "feBW_loose" in
+  let feBW_loose := pose_feBW_loose sz adjusted_bitwidth' bounds_loose feBW_loose in
+  Tag.update pkg TAG.feBW_loose feBW_loose.
+
+Ltac add_feBW_limbwidths pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
+  let feBW_limbwidths := fresh "feBW_limbwidths" in
+  let feBW_limbwidths := pose_feBW_limbwidths sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths in
+  Tag.update pkg TAG.feBW_limbwidths feBW_limbwidths.
+
+Ltac add_feBW_relax pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let feBW_tight := Tag.get pkg TAG.feBW_tight in
+  let feBW_loose := Tag.get pkg TAG.feBW_loose in
+  let feBW_relax := fresh "feBW_relax" in
+  let feBW_relax := pose_feBW_relax sz feBW_tight feBW_loose feBW_relax in
+  Tag.update pkg TAG.feBW_relax feBW_relax.
 
-Ltac add_feBW_bounded pkg :=
+Ltac add_feBW_relax_limbwidths_to_tight pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
+  let feBW_tight := Tag.get pkg TAG.feBW_tight in
+  let feBW_relax_limbwidths_to_tight := fresh "feBW_relax_limbwidths_to_tight" in
+  let feBW_relax_limbwidths_to_tight := pose_feBW_relax_limbwidths_to_tight sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight in
+  Tag.update pkg TAG.feBW_relax_limbwidths_to_tight feBW_relax_limbwidths_to_tight.
+
+Ltac add_feBW_relax_limbwidths_to_loose pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
+  let feBW_loose := Tag.get pkg TAG.feBW_loose in
+  let feBW_relax_limbwidths_to_loose := fresh "feBW_relax_limbwidths_to_loose" in
+  let feBW_relax_limbwidths_to_loose := pose_feBW_relax_limbwidths_to_loose sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose in
+  Tag.update pkg TAG.feBW_relax_limbwidths_to_loose feBW_relax_limbwidths_to_loose.
+
+Ltac add_feBW_tight_bounded pkg :=
   let freeze := Tag.get pkg TAG.freeze in
   let wt := Tag.get pkg TAG.wt in
   let sz := Tag.get pkg TAG.sz in
-  let feBW := Tag.get pkg TAG.feBW in
+  let feBW_tight := Tag.get pkg TAG.feBW_tight in
   let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
-  let bounds := Tag.get pkg TAG.bounds in
+  let bounds_tight := Tag.get pkg TAG.bounds_tight in
   let m := Tag.get pkg TAG.m in
   let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
-  let feBW_bounded := fresh "feBW_bounded" in
-  let feBW_bounded := pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded in
-  Tag.update pkg TAG.feBW_bounded feBW_bounded.
+  let feBW_tight_bounded := fresh "feBW_tight_bounded" in
+  let feBW_tight_bounded := pose_feBW_tight_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded in
+  Tag.update pkg TAG.feBW_tight_bounded feBW_tight_bounded.
+
+Ltac add_feBW_limbwidths_bounded pkg :=
+  let freeze := Tag.get pkg TAG.freeze in
+  let wt := Tag.get pkg TAG.wt in
+  let sz := Tag.get pkg TAG.sz in
+  let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
+  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
+  let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
+  let m := Tag.get pkg TAG.m in
+  let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
+  let feBW_limbwidths_bounded := fresh "feBW_limbwidths_bounded" in
+  let feBW_limbwidths_bounded := pose_feBW_limbwidths_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded in
+  Tag.update pkg TAG.feBW_limbwidths_bounded feBW_limbwidths_bounded.
 
 Ltac add_phiW pkg :=
   let feW := Tag.get pkg TAG.feW in
@@ -104,29 +186,57 @@ Ltac add_phiW pkg :=
   let phiW := pose_phiW feW m wt phiW in
   Tag.update pkg TAG.phiW phiW.
 
-Ltac add_phiBW pkg :=
-  let feBW := Tag.get pkg TAG.feBW in
+Ltac add_phiBW_tight pkg :=
+  let feBW_tight := Tag.get pkg TAG.feBW_tight in
+  let m := Tag.get pkg TAG.m in
+  let wt := Tag.get pkg TAG.wt in
+  let phiBW_tight := fresh "phiBW_tight" in
+  let phiBW_tight := pose_phiBW_tight feBW_tight m wt phiBW_tight in
+  Tag.update pkg TAG.phiBW_tight phiBW_tight.
+
+Ltac add_phiBW_loose pkg :=
+  let feBW_loose := Tag.get pkg TAG.feBW_loose in
+  let m := Tag.get pkg TAG.m in
+  let wt := Tag.get pkg TAG.wt in
+  let phiBW_loose := fresh "phiBW_loose" in
+  let phiBW_loose := pose_phiBW_loose feBW_loose m wt phiBW_loose in
+  Tag.update pkg TAG.phiBW_loose phiBW_loose.
+
+Ltac add_phiBW_limbwidths pkg :=
+  let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
   let m := Tag.get pkg TAG.m in
   let wt := Tag.get pkg TAG.wt in
-  let phiBW := fresh "phiBW" in
-  let phiBW := pose_phiBW feBW m wt phiBW in
-  Tag.update pkg TAG.phiBW phiBW.
+  let phiBW_limbwidths := fresh "phiBW_limbwidths" in
+  let phiBW_limbwidths := pose_phiBW_limbwidths feBW_limbwidths m wt phiBW_limbwidths in
+  Tag.update pkg TAG.phiBW_limbwidths phiBW_limbwidths.
 
 Ltac add_ReificationTypes_package pkg :=
   let pkg := add_limb_widths pkg in
   let pkg := add_bounds_exp pkg in
-  let pkg := add_bounds pkg in
+  let pkg := add_bounds_tight pkg in
+  let pkg := add_bounds_loose pkg in
+  let pkg := add_bounds_limbwidths pkg in
   let pkg := add_bound1 pkg in
   let pkg := add_lgbitwidth pkg in
   let pkg := add_adjusted_bitwidth' pkg in
   let pkg := add_adjusted_bitwidth pkg in
   let pkg := add_feZ pkg in
   let pkg := add_feW pkg in
-  let pkg := add_feW_bounded pkg in
-  let pkg := add_feBW pkg in
-  let pkg := add_feBW_bounded pkg in
+  let pkg := add_feW_tight_bounded pkg in
+  let pkg := add_feW_loose_bounded pkg in
+  let pkg := add_feW_limbwidths_bounded pkg in
+  let pkg := add_feBW_tight pkg in
+  let pkg := add_feBW_loose pkg in
+  let pkg := add_feBW_limbwidths pkg in
+  let pkg := add_feBW_relax pkg in
+  let pkg := add_feBW_relax_limbwidths_to_tight pkg in
+  let pkg := add_feBW_relax_limbwidths_to_loose pkg in
+  let pkg := add_feBW_tight_bounded pkg in
+  let pkg := add_feBW_limbwidths_bounded pkg in
   let pkg := add_phiW pkg in
-  let pkg := add_phiBW pkg in
+  let pkg := add_phiBW_tight pkg in
+  let pkg := add_phiBW_loose pkg in
+  let pkg := add_phiBW_limbwidths pkg in
   Tag.strip_subst_local pkg.
 
 
@@ -139,14 +249,34 @@ Module MakeReificationTypesPackage (PKG : PrePackage).
   Notation adjusted_bitwidth := (ltac:(let v := get_adjusted_bitwidth () in exact v)) (only parsing).
   Ltac get_feW _ := get TAG.feW.
   Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing).
-  Ltac get_feW_bounded _ := get TAG.feW_bounded.
-  Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
-  Ltac get_feBW _ := get TAG.feBW.
-  Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
-  Ltac get_feBW_bounded _ := get TAG.feBW_bounded.
-  Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing).
+  Ltac get_feW_tight_bounded _ := get TAG.feW_tight_bounded.
+  Notation feW_tight_bounded := (ltac:(let v := get_feW_tight_bounded () in exact v)) (only parsing).
+  Ltac get_feW_loose_bounded _ := get TAG.feW_loose_bounded.
+  Notation feW_loose_bounded := (ltac:(let v := get_feW_loose_bounded () in exact v)) (only parsing).
+  Ltac get_feW_limbwidths_bounded _ := get TAG.feW_limbwidths_bounded.
+  Notation feW_limbwidths_bounded := (ltac:(let v := get_feW_limbwidths_bounded () in exact v)) (only parsing).
+  Ltac get_feBW_tight _ := get TAG.feBW_tight.
+  Notation feBW_tight := (ltac:(let v := get_feBW_tight () in exact v)) (only parsing).
+  Ltac get_feBW_loose _ := get TAG.feBW_loose.
+  Notation feBW_loose := (ltac:(let v := get_feBW_loose () in exact v)) (only parsing).
+  Ltac get_feBW_limbwidths _ := get TAG.feBW_limbwidths.
+  Notation feBW_limbwidths := (ltac:(let v := get_feBW_limbwidths () in exact v)) (only parsing).
+  Ltac get_feBW_relax _ := get TAG.feBW_relax.
+  Notation feBW_relax := (ltac:(let v := get_feBW_relax () in exact v)) (only parsing).
+  Ltac get_feBW_relax_limbwidths_to_tight _ := get TAG.feBW_relax_limbwidths_to_tight.
+  Notation feBW_relax_limbwidths_to_tight := (ltac:(let v := get_feBW_relax_limbwidths_to_tight () in exact v)) (only parsing).
+  Ltac get_feBW_relax_limbwidths_to_loose _ := get TAG.feBW_relax_limbwidths_to_loose.
+  Notation feBW_relax_limbwidths_to_loose := (ltac:(let v := get_feBW_relax_limbwidths_to_loose () in exact v)) (only parsing).
+  Ltac get_feBW_tight_bounded _ := get TAG.feBW_tight_bounded.
+  Notation feBW_tight_bounded := (ltac:(let v := get_feBW_tight_bounded () in exact v)) (only parsing).
+  Ltac get_feBW_limbwidths_bounded _ := get TAG.feBW_limbwidths_bounded.
+  Notation feBW_limbwidths_bounded := (ltac:(let v := get_feBW_limbwidths_bounded () in exact v)) (only parsing).
   Ltac get_phiW _ := get TAG.phiW.
   Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing).
-  Ltac get_phiBW _ := get TAG.phiBW.
-  Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
+  Ltac get_phiBW_tight _ := get TAG.phiBW_tight.
+  Notation phiBW_tight := (ltac:(let v := get_phiBW_tight () in exact v)) (only parsing).
+  Ltac get_phiBW_loose _ := get TAG.phiBW_loose.
+  Notation phiBW_loose := (ltac:(let v := get_phiBW_loose () in exact v)) (only parsing).
+  Ltac get_phiBW_limbwidths _ := get TAG.phiBW_limbwidths.
+  Notation phiBW_limbwidths := (ltac:(let v := get_phiBW_limbwidths () in exact v)) (only parsing).
 End MakeReificationTypesPackage.
diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
index b45931430..a7f8e5ee5 100644
--- a/src/Specific/Framework/SynthesisFramework.v
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -77,22 +77,26 @@ Module PackageSynthesis (PKG : PrePackage).
   Include MP.
   Include MRP.
 
-  Ltac synthesize_with_carry do_rewrite get_op_sig :=
-    let carry_sig := get_carry_sig () in
+  Ltac synthesize do_rewrite get_op_sig :=
     let op_sig := get_op_sig () in
     let allowable_bit_widths := get_allowable_bit_widths () in
     start_preglue;
-    [ do_rewrite op_sig carry_sig; cbv_runtime
+    [ do_rewrite op_sig; cbv_runtime
     | .. ];
     fin_preglue;
     refine_reflectively_gen allowable_bit_widths default.
+  Ltac synthesize_with_carry do_rewrite get_op_sig :=
+    let carry_sig := get_carry_sig () in
+    synthesize ltac:(fun op_sig => do_rewrite op_sig carry_sig) get_op_sig.
+  Ltac synthesize_narg get_op_sig :=
+    synthesize do_rewrite_with_sig get_op_sig.
   Ltac synthesize_2arg_with_carry get_op_sig :=
     synthesize_with_carry do_rewrite_with_2sig_add_carry get_op_sig.
   Ltac synthesize_1arg_with_carry get_op_sig :=
     synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig.
 
   Ltac synthesize_montgomery get_op_sig get_op_bounded :=
-    let phi := get_phi_for_preglue () in
+    let phi := get_phi1_for_preglue () in
     let op_sig := get_op_sig () in
     let op_bounded := get_op_bounded () in
     let allowable_bit_widths := get_allowable_bit_widths () in
@@ -110,30 +114,38 @@ Module PackageSynthesis (PKG : PrePackage).
     factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t;
     refine_reflectively_gen allowable_bit_widths anf.
 
-  Ltac synthesize_2arg_choice get_op_sig get_op_bounded :=
-    let montgomery := get_montgomery () in
-    lazymatch (eval vm_compute in montgomery) with
-    | true => synthesize_montgomery get_op_sig get_op_bounded
-    | false => synthesize_2arg_with_carry get_op_sig
-    end.
-  Ltac synthesize_1arg_choice get_op_sig get_op_bounded :=
+  Ltac synthesize_narg_choice_gen synthesize get_op_sig get_op_bounded :=
     let montgomery := get_montgomery () in
     lazymatch (eval vm_compute in montgomery) with
     | true => synthesize_montgomery get_op_sig get_op_bounded
-    | false => synthesize_1arg_with_carry get_op_sig
+    | false => synthesize get_op_sig
     end.
+  Ltac synthesize_narg_choice get_op_sig get_op_bounded :=
+    synthesize_narg_choice_gen synthesize_narg get_op_sig get_op_bounded.
+  Ltac synthesize_2arg_choice_with_carry get_op_sig get_op_bounded :=
+    synthesize_narg_choice_gen synthesize_2arg_with_carry get_op_sig get_op_bounded.
+  Ltac synthesize_1arg_choice_with_carry get_op_sig get_op_bounded :=
+    synthesize_narg_choice_gen synthesize_1arg_with_carry get_op_sig get_op_bounded.
 
-  Ltac synthesize_mul _ := synthesize_2arg_choice get_mul_sig get_mul_bounded.
-  Ltac synthesize_add _ := synthesize_2arg_choice get_add_sig get_add_bounded.
-  Ltac synthesize_sub _ := synthesize_2arg_choice get_sub_sig get_sub_bounded.
-  Ltac synthesize_opp _ := synthesize_1arg_choice get_opp_sig get_opp_bounded.
-  Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig.
+  Ltac synthesize_carry_mul _ := synthesize_2arg_choice_with_carry get_mul_sig get_mul_bounded.
+  Ltac synthesize_carry_add _ := synthesize_2arg_choice_with_carry get_add_sig get_add_bounded.
+  Ltac synthesize_carry_sub _ := synthesize_2arg_choice_with_carry get_sub_sig get_sub_bounded.
+  Ltac synthesize_carry_opp _ := synthesize_1arg_choice_with_carry get_opp_sig get_opp_bounded.
+  Ltac synthesize_carry_square _ := synthesize_1arg_with_carry get_square_sig.
+  Ltac synthesize_nocarry_mul _ := synthesize_narg_choice get_mul_sig get_mul_bounded.
+  Ltac synthesize_add _ := synthesize_narg_choice get_add_sig get_add_bounded.
+  Ltac synthesize_sub _ := synthesize_narg_choice get_sub_sig get_sub_bounded.
+  Ltac synthesize_opp _ := synthesize_narg_choice get_opp_sig get_opp_bounded.
+  Ltac synthesize_carry _ := synthesize_narg_choice get_carry_sig get_carry_bounded.
+  Ltac synthesize_nocarry_square _ := synthesize_narg get_square_sig.
+  Ltac synthesize_mul _ := synthesize_carry_mul ().
+  Ltac synthesize_square _ := synthesize_carry_square ().
   Ltac synthesize_freeze _ :=
     let freeze_sig := get_freeze_sig () in
-    let feBW_bounded := get_feBW_bounded () in
+    let feBW_tight_bounded := get_feBW_tight_bounded () in
     let freeze_allowable_bit_widths := get_freeze_allowable_bit_widths () in
     start_preglue;
-    [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime
+    [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_tight_bounded); cbv_runtime
     | .. ];
     fin_preglue;
     refine_reflectively_gen freeze_allowable_bit_widths anf.
diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index 1642ae7d9..88860f343 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -44,21 +44,6 @@ def compute_c(modulus_str):
         return list(reversed(ret))
     # XXX FIXME: Is this the right way to extract c?
     return [('1', rest)]
-def compute_goldilocks(s, c):
-    # true if the prime is of the form 2^2k - 2^k - 1
-    ms = re.match(r'^2\^([0-9]+)$', s)
-    if ms is None: return False
-    two_k = int(ms.groups()[0])
-    assert(isinstance(c, list))
-    if len(c) != 2: return False
-    one_vs = [str(v) for k, v in c if str(k) == '1']
-    others = [(str(k), str(v)) for k, v in c if str(k) != '1']
-    if len(one_vs) != 1 or len(others) != 1 or one_vs[0] != '1' or others[0][1] != '1': return False
-    mk = re.match(r'^2\^([0-9]+)$', others[0][0])
-    if mk is None: return False
-    k = int(mk.groups()[0])
-    if two_k != 2 * k: return False
-    return True
 
 def parse_base(base):
     ret = 0
@@ -235,7 +220,6 @@ def make_curve_parameters(parameters):
         replacements['carry_chains'] = 'Some %s%%nat' % nested_list_to_string(default_carry_chains(replacements['sz']))
     replacements['s'] = parameters.get('s', compute_s(parameters['modulus']))
     replacements['c'] = parameters.get('c', compute_c(parameters['modulus']))
-    replacements['goldilocks'] = parameters.get('goldilocks', compute_goldilocks(replacements['s'], replacements['c']))
     for op, nargs in (('mul', 2), ('square', 1)):
         replacements[op] = format_c_code(parameters.get(op + '_header', None),
                                          parameters.get(op + '_code', None),
@@ -244,7 +228,8 @@ def make_curve_parameters(parameters):
     replacements['coef_div_modulus_raw'] = replacements.get('coef_div_modulus', '0')
     replacements['freeze'] = fix_option(nested_list_to_string(replacements.get('freeze', 'freeze' in parameters.get('operations', []))))
     replacements['ladderstep'] = nested_list_to_string(replacements.get('ladderstep', any(f in parameters.get('operations', []) for f in ('ladderstep', 'xzladderstep'))))
-    for k, scope_string in (('upper_bound_of_exponent', ''),
+    for k, scope_string in (('upper_bound_of_exponent_loose', ''),
+                            ('upper_bound_of_exponent_tight', ''),
                             ('allowable_bit_widths', '%nat'),
                             ('freeze_extra_allowable_bit_widths', '%nat'),
                             ('coef_div_modulus', '%nat'),
@@ -288,7 +273,8 @@ Definition curve : CurveParameters :=
 
     square_code := %(square)s;
 
-    upper_bound_of_exponent := %(upper_bound_of_exponent)s;
+    upper_bound_of_exponent_loose := %(upper_bound_of_exponent_loose)s;
+    upper_bound_of_exponent_tight := %(upper_bound_of_exponent_tight)s;
     allowable_bit_widths := %(allowable_bit_widths)s;
     freeze_extra_allowable_bit_widths := %(freeze_extra_allowable_bit_widths)s;
     modinv_fuel := %(modinv_fuel)s
@@ -312,31 +298,34 @@ Module Export S := PackageSynthesis P.
 """ % prefix
 
 def make_synthesized_arg(fearg, prefix, montgomery=False):
-    if fearg in ('femul', 'fesub', 'feadd'):
+    def make_from_arg(arg, nargs, phi_arg_postfix='', phi_output_postfix='', prefix=prefix):
+        LETTERS = 'abcdefghijklmnopqrstuvwxyz'
+        assert(nargs <= len(LETTERS))
+        arg_names = ' '.join(LETTERS[:nargs])
         if not montgomery:
-            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import %(prefix)s.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition %(arg)s :
-  { %(arg)s : feBW -> feBW -> feBW
-  | forall a b, phiBW (%(arg)s a b) = F.%(arg)s (phiBW a) (phiBW b) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_%(arg)s ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions %(arg)s.
-""" % {'prefix':prefix, 'arg':fearg[2:]}
+            arg_types = ' -> '.join(['feBW%s' % phi_arg_postfix] * nargs)
+            mapped_args = ' '.join('(phiBW%s %s)' % (phi_arg_postfix, l)
+                                   for l in LETTERS[:nargs])
+            feBW_output = 'feBW' + phi_output_postfix
+            phi_output = 'phiBW' + phi_output_postfix
         else:
-            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+            arg_types = ' -> '.join(['feBW_small'] * nargs)
+            mapped_args = ' '.join('(phiM_small %s)' % l
+                                   for l in LETTERS[:nargs])
+            feBW_output = 'feBW_small'
+            phi_output = 'phiM_small'
+        return locals()
+    GEN_PREARG = r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import %(prefix)s.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
 Definition %(arg)s :
-  { %(arg)s : feBW_small -> feBW_small -> feBW_small
-  | forall a b, phiM_small (%(arg)s a b) = F.%(arg)s (phiM_small a) (phiM_small b) }.
+  { %(arg)s : %(arg_types)s -> %(feBW_output)s
+  | forall %(arg_names)s, %(phi_output)s (%(arg)s %(arg_names)s) = """
+    GEN_MIDARG = "F.%(arg)s %(mapped_args)s"
+    SQUARE_MIDARG = "F.mul %(mapped_args)s %(mapped_args)s"
+    CARRY_MIDARG = "%(mapped_args)s"
+    GEN_POSTARG = r""" }.
 Proof.
   Set Ltac Profiling.
   Time synthesize_%(arg)s ().
@@ -344,31 +333,31 @@ Proof.
 Time Defined.
 
 Print Assumptions %(arg)s.
-""" % {'prefix':prefix, 'arg':fearg[2:]}
-    elif fearg in ('fesquare',):
-        return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import %(prefix)s.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) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_square ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions square.
-""" % {'prefix':prefix}
+"""
+    GEN_ARG = GEN_PREARG + GEN_MIDARG + GEN_POSTARG
+    SQUARE_ARG = GEN_PREARG + SQUARE_MIDARG + GEN_POSTARG
+    CARRY_ARG = GEN_PREARG + CARRY_MIDARG + GEN_POSTARG
+    nargs_map = {'mul':2, 'sub':2, 'add':2, 'square':1, 'opp':1, 'carry':1}
+    special_args = {'fecarry':CARRY_ARG, 'fecarry_square':SQUARE_ARG, 'fesquare':SQUARE_ARG}
+    if fearg in ('fecarry_mul', 'fecarry_sub', 'fecarry_add', 'fecarry_square', 'fecarry_opp'):
+        nargs = nargs_map[fearg.split('_')[-1]]
+        ARG = special_args.get(fearg, GEN_ARG)
+        return ARG % make_from_arg(fearg[2:], nargs=nargs, phi_arg_postfix='_tight', phi_output_postfix='_tight')
+    elif fearg in ('femul', 'fesquare', 'fecarry'):
+        ARG = special_args.get(fearg, GEN_ARG)
+        nargs = nargs_map[fearg[2:]]
+        return ARG % make_from_arg(fearg[2:], nargs=nargs, phi_arg_postfix='_loose', phi_output_postfix='_tight')
+    if fearg in ('fesub', 'feadd', 'feopp'):
+        nargs = nargs_map[fearg[2:]]
+        return GEN_ARG % make_from_arg(fearg[2:], nargs=nargs, phi_arg_postfix='_tight', phi_output_postfix='_loose')
     elif fearg in ('freeze',):
         return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import %(prefix)s.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 ().
@@ -377,39 +366,6 @@ Time Defined.
 
 Print Assumptions freeze.
 """ % {'prefix':prefix}
-    elif fearg in ('feopp',):
-        if not montgomery:
-            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import %(prefix)s.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition %(arg)s :
-  { %(arg)s : feBW -> feBW
-  | forall a, phiBW (%(arg)s a) = F.%(arg)s (phiBW a) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_%(arg)s ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions %(arg)s.
-""" % {'prefix':prefix, 'arg':fearg[2:]}
-        else:
-            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import %(prefix)s.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition %(arg)s :
-  { %(arg)s : feBW_small -> feBW_small
-  | forall a, phiM_small (%(arg)s a) = F.%(arg)s (phiM_small a) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_%(arg)s ().
-  Show Ltac Profile.
-Time Defined.
-
-Print Assumptions %(arg)s.
-""" % {'prefix':prefix, 'arg':fearg[2:]}
     elif fearg in ('fenz',):
         assert(fearg == 'fenz')
         assert(montgomery)
@@ -443,11 +399,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.
@@ -465,7 +421,8 @@ Print Assumptions xzladderstep.
 def make_display_arg(fearg, prefix):
     file_name = fearg
     function_name = fearg
-    if fearg in ('femul', 'fesub', 'feadd', 'fesquare', 'feopp'):
+    if fearg in ('femul', 'fesub', 'feadd', 'fesquare', 'feopp', 'fecarry',
+                 'fecarry_mul', 'fecarry_sub', 'fecarry_add', 'fecarry_square', 'fecarry_opp'):
         function_name = fearg[2:]
     elif fearg in ('freeze', 'xzladderstep'):
         pass
@@ -489,6 +446,17 @@ set -eu
 %s "$@"
 """ % compiler
 
+DONT_EDIT_STR = 'WARNING: This file was copied from %s.\n If you edit it here, changes will be erased the next time remake_curves.sh is run.'
+DONT_EDIT_HEADERS = {
+    '.c' : '/* ' + DONT_EDIT_STR + ' */',
+    '.h' : '/* ' + DONT_EDIT_STR + ' */',
+    '.v' : '(* ' + DONT_EDIT_STR + ' *)',
+    '.ml' : '(* ' + DONT_EDIT_STR + ' *)',
+    '.ml4' : '(* ' + DONT_EDIT_STR + ' *)',
+    '.py' : '# ' + DONT_EDIT_STR.replace('\n', '\n# '),
+}
+
+
 
 def main(*args):
     if '--help' in args[1:] or '-h' in args[1:]: usage(0)
@@ -509,7 +477,11 @@ def main(*args):
         outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix, montgomery=as_bool(parameters.get('montgomery', 'false')))
         outputs[arg + 'Display.v'] = make_display_arg(arg, output_prefix)
     for fname in parameters.get('extra_files', []):
-        outputs[os.path.basename(fname)] = open(os.path.join(parameters_folder, fname), 'r').read()
+        _, ext = os.path.splitext(fname)
+        header = ''
+        if ext in DONT_EDIT_HEADERS.keys():
+            header = DONT_EDIT_HEADERS[ext] % os.path.relpath(fname, os.path.join(root, 'src'))
+        outputs[os.path.basename(fname)] = header + '\n' + open(os.path.join(parameters_folder, fname), 'r').read()
     if 'compiler' in parameters.keys():
         outputs['compiler.sh'] = make_compiler(parameters['compiler'])
     file_list = tuple((k, os.path.join(output_folder, k)) for k in sorted(outputs.keys()))