Saner checking for freeze and ladderstep

14 files changed, 189 insertions, 84 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
index 36e02bb0e..4ee04f6a1 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v
@@ -24,15 +24,6 @@ Module Export Exports.
   Export Coq.setoid_ring.ZArithRing.
 End Exports.
 
-Ltac solve_constant_sig :=
-  idtac;
-  lazymatch goal with
-  | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
-    => let t := (eval vm_compute in
-                    (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in
-       (exists t; vm_decide)
-  end.
-
 Local Ltac solve_constant_local_sig :=
   idtac;
   lazymatch goal with
@@ -348,12 +339,6 @@ Ltac pose_one_sig wt m base sz sz_nonzero base_pos one_sig :=
     (one_sig' m base sz sz_nonzero base_pos)
     one_sig.
 
-Ltac pose_a24_sig sz m wt a24 a24_sig :=
-  cache_term_with_type_by
-    { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }
-    solve_constant_sig
-    a24_sig.
-
 Ltac pose_add_sig wt m base sz add_sig :=
   cache_sig_with_type_by_existing_sig
     { add : (Z^sz -> Z^sz -> Z^sz)%type |
diff --git a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
index 10d6e42ed..52ed4ad33 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v
@@ -6,7 +6,7 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := mul_code_correct | square_code_correct | carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
+  Inductive tags := mul_code_correct | square_code_correct | carry_sig | zero_sig | one_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
 End TAG.
 
 Ltac add_mul_code_correct pkg P_extra_prove_mul_eq :=
@@ -75,17 +75,6 @@ Ltac add_one_sig pkg :=
                    let one_sig := fresh "one_sig" in
                    let one_sig := pose_one_sig wt m base sz sz_nonzero base_pos one_sig in
                    constr:(one_sig)).
-Ltac add_a24_sig pkg :=
-  Tag.update_by_tac_if_not_exists
-    pkg
-    TAG.a24_sig
-    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                   let m := Tag.get pkg TAG.m in
-                   let wt := Tag.get pkg TAG.wt in
-                   let a24 := Tag.get pkg TAG.a24 in
-                   let a24_sig := fresh "a24_sig" in
-                   let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
-                   constr:(a24_sig)).
 Ltac add_add_sig pkg :=
   Tag.update_by_tac_if_not_exists
     pkg
@@ -182,7 +171,6 @@ Ltac add_Defaults_package pkg P_extra_prove_mul_eq P_extra_prove_square_eq :=
   let pkg := add_carry_sig pkg in
   let pkg := add_zero_sig pkg in
   let pkg := add_one_sig pkg in
-  let pkg := add_a24_sig pkg in
   let pkg := add_add_sig pkg in
   let pkg := add_sub_sig pkg in
   let pkg := add_opp_sig pkg in
@@ -205,8 +193,6 @@ Module MakeDefaultsPackage (PKG : PrePackage).
   Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
   Ltac get_one_sig _ := get TAG.one_sig.
   Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing).
-  Ltac get_a24_sig _ := get TAG.a24_sig.
-  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
   Ltac get_add_sig _ := get TAG.add_sig.
   Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
   Ltac get_sub_sig _ := get TAG.sub_sig.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
index 5cda57da2..18fef6cc9 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
@@ -10,32 +10,40 @@ Module TAG.
 End TAG.
 
 Ltac add_m_correct_wt pkg :=
-  Tag.update_by_tac_if_not_exists
+  if_freeze
     pkg
-    TAG.m_correct_wt
-    ltac:(fun _ => let m := Tag.get pkg TAG.m in
-                   let c := Tag.get pkg TAG.c in
-                   let sz := Tag.get pkg TAG.sz in
-                   let wt := Tag.get pkg TAG.wt in
-                   let m_correct_wt := fresh "m_correct_wt" in
-                   let m_correct_wt := pose_m_correct_wt m c sz wt m_correct_wt in
-                   constr:(m_correct_wt)).
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.m_correct_wt
+                       ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                                      let c := Tag.get pkg TAG.c in
+                                      let sz := Tag.get pkg TAG.sz in
+                                      let wt := Tag.get pkg TAG.wt in
+                                      let m_correct_wt := fresh "m_correct_wt" in
+                                      let m_correct_wt := pose_m_correct_wt m c sz wt m_correct_wt in
+                                      constr:(m_correct_wt)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_freeze_sig pkg :=
-  Tag.update_by_tac_if_not_exists
+  if_freeze
     pkg
-    TAG.freeze_sig
-    ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
-                   let m := Tag.get pkg TAG.m in
-                   let base := Tag.get pkg TAG.base in
-                   let sz := Tag.get pkg TAG.sz in
-                   let c := Tag.get pkg TAG.c in
-                   let bitwidth := Tag.get pkg TAG.bitwidth in
-                   let m_enc := Tag.get pkg TAG.m_enc in
-                   let base_pos := Tag.get pkg TAG.base_pos in
-                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
-                   let freeze_sig := fresh "freeze_sig" in
-                   let freeze_sig := pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig in
-                   constr:(freeze_sig)).
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.freeze_sig
+                       ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
+                                      let m := Tag.get pkg TAG.m in
+                                      let base := Tag.get pkg TAG.base in
+                                      let sz := Tag.get pkg TAG.sz in
+                                      let c := Tag.get pkg TAG.c in
+                                      let bitwidth := Tag.get pkg TAG.bitwidth in
+                                      let m_enc := Tag.get pkg TAG.m_enc in
+                                      let base_pos := Tag.get pkg TAG.base_pos in
+                                      let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
+                                      let freeze_sig := fresh "freeze_sig" in
+                                      let freeze_sig := pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig in
+                                      constr:(freeze_sig)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_Freeze_package pkg :=
   let pkg := add_m_correct_wt pkg in
   let pkg := add_freeze_sig pkg in
diff --git a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
index e8fa1b407..e04e3b2ec 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v
@@ -1,5 +1,6 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Crypto.Arithmetic.Saturated.Wrappers.
 Require Import Crypto.Util.ZUtil.ModInv.
 Require Import Crypto.Util.Tactics.CacheTerm.
@@ -171,3 +172,12 @@ Ltac cache_sig_with_type_by_existing_sig_helper cbv_tac ty existing_sig id :=
           do_replace_match_with_destructuring_match_in_goal;
           reflexivity)
            id.
+
+Ltac solve_constant_sig :=
+  idtac;
+  lazymatch goal with
+  | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ]
+    => let t := (eval vm_compute in
+                    (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in
+       (exists t; vm_decide)
+  end.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
index ba3fd9078..f5540a93f 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v
@@ -1,12 +1,19 @@
 Require Import Coq.ZArith.BinIntDef.
-Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.Core. Import B.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Curves.Montgomery.XZ.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.PoseTermWithName.
 Require Import Crypto.Util.Tactics.CacheTerm.
+Require Import Crypto.Util.Option.
+
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Infix "^" := tuple : type_scope.
 
 (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
 Definition FMxzladderstep {m} := @M.donnaladderstep (F m) F.add F.sub F.mul.
@@ -46,6 +53,13 @@ Section with_notations.
        end.
 End with_notations.
 
+Ltac pose_a24_sig sz m wt a24 a24_sig :=
+  let a24 := (eval vm_compute in (invert_Some a24)) in
+  cache_term_with_type_by
+    { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }
+    solve_constant_sig
+    a24_sig.
+
 Ltac pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig :=
   cache_term_with_type_by
     { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
index 200ad593a..5b43277cc 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
@@ -7,25 +7,45 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := Mxzladderstep_sig.
+  Inductive tags := a24_sig | Mxzladderstep_sig.
 End TAG.
 
+Ltac add_a24_sig pkg :=
+  if_ladderstep
+    pkg
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.a24_sig
+                       ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                                      let m := Tag.get pkg TAG.m in
+                                      let wt := Tag.get pkg TAG.wt in
+                                      let a24 := Tag.get pkg TAG.a24 in
+                                      let a24_sig := fresh "a24_sig" in
+                                      let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
+                                      constr:(a24_sig)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_Mxzladderstep_sig pkg :=
-  Tag.update_by_tac_if_not_exists
+  if_ladderstep
     pkg
-    TAG.Mxzladderstep_sig
-    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                   let wt := Tag.get pkg TAG.wt in
-                   let m := Tag.get pkg TAG.m in
-                   let add_sig := Tag.get pkg TAG.add_sig in
-                   let sub_sig := Tag.get pkg TAG.sub_sig in
-                   let mul_sig := Tag.get pkg TAG.mul_sig in
-                   let square_sig := Tag.get pkg TAG.square_sig in
-                   let carry_sig := Tag.get pkg TAG.carry_sig in
-                   let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
-                   let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
-                   constr:(Mxzladderstep_sig)).
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.Mxzladderstep_sig
+                       ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                                      let wt := Tag.get pkg TAG.wt in
+                                      let m := Tag.get pkg TAG.m in
+                                      let add_sig := Tag.get pkg TAG.add_sig in
+                                      let sub_sig := Tag.get pkg TAG.sub_sig in
+                                      let mul_sig := Tag.get pkg TAG.mul_sig in
+                                      let square_sig := Tag.get pkg TAG.square_sig in
+                                      let carry_sig := Tag.get pkg TAG.carry_sig in
+                                      let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
+                                      let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
+                                      constr:(Mxzladderstep_sig)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_Ladderstep_package pkg :=
+  let pkg := add_a24_sig pkg in
   let pkg := add_Mxzladderstep_sig pkg in
   Tag.strip_subst_local pkg.
 
@@ -33,6 +53,8 @@ Ltac add_Ladderstep_package pkg :=
 Module MakeLadderstepPackage (PKG : PrePackage).
   Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
 
+  Ltac get_a24_sig _ := get TAG.a24_sig.
+  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
   Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
   Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
 End MakeLadderstepPackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
index 568877838..d21ad2d9e 100755
--- a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
+++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py
@@ -11,13 +11,13 @@ CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST = ['../CurveParametersPackage.v', 'BaseP
 NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)),
                         ('Defaults.v', (CP_BASE_LIST, 'not_exists')),
                         ('../ReificationTypes.v', (CP_BASE_LIST, None)),
-                        ('Freeze.v', (CP_BASE_LIST, 'not_exists')),
-                        ('Ladderstep.v', (CP_BASE_DEFAULTS_LIST, 'not_exists')),
+                        ('Freeze.v', (CP_BASE_LIST, ('freeze', 'not_exists'))),
+                        ('Ladderstep.v', (CP_BASE_DEFAULTS_LIST, ('ladderstep', 'not_exists'))),
                         ('Karatsuba.v', (CP_BASE_DEFAULTS_LIST, 'goldilocks')),
                         ('Montgomery.v', (CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST, 'montgomery')),
                         ('../MontgomeryReificationTypes.v', (CP_BASE_LIST + ['MontgomeryPackage.v', '../ReificationTypesPackage.v'], 'montgomery'))]
 ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v']
-CONFIGS = ('goldilocks', 'montgomery')
+CONFIGS = ('goldilocks', 'montgomery', 'freeze', 'ladderstep')
 
 EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', )
 
@@ -95,11 +95,22 @@ def make_add_from_pose(name, args_str, indent='', only_if=None, local=False):
 %(indent)s    TAG.%(name)s
 %(indent)s    ltac:(fun _ => %(body)s).''' % locals()
     else:
-        body += r'''Tag.%(local_str)supdate pkg TAG.%(name)s %(name)s''' % locals()
+        if isinstance(only_if, tuple) and 'not_exists' in only_if:
+            only_if = [i for i in only_if if i != 'not_exists']
+            assert(len(only_if) == 1)
+            only_if = only_if[0]
+            body += 'constr:(%(name)s)' % locals()
+            body = body.strip('\n ').replace('\n', '\n                   ')
+            body = r'''Tag.update_by_tac_if_not_exists
+%(indent)s      pkg
+%(indent)s      TAG.%(name)s
+%(indent)s      ltac:(fun _ => %(body)s).''' % locals()
+        else:
+            body += r'''Tag.%(local_str)supdate pkg TAG.%(name)s %(name)s''' % locals()
         if only_if is None:
             ret += body + '.\n'
         else:
-            body = body.strip('\n ').replace('\n', '\n                 ')
+            body = body.strip('\n .').replace('\n', '\n                 ')
             ret += r'''
 %(indent)s  if_%(only_if)s
 %(indent)s    pkg
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index c77b159e4..50ff2278b 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -1,3 +1,4 @@
+Require Import Coq.QArith.Qround.
 Require Export Coq.ZArith.BinInt.
 Require Export Coq.Lists.List.
 Require Export Crypto.Util.ZUtil.Notations.
@@ -11,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 | 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 | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
 End TAG.
 
 Module Export CurveParameters.
@@ -37,11 +38,13 @@ Module Export CurveParameters.
       s : Z;
       c : list limb;
       carry_chains : list (list nat);
-      a24 : Z;
+      a24 : option Z;
       coef_div_modulus : nat;
 
       goldilocks : bool;
       montgomery : bool;
+      freeze : bool;
+      ladderstep : bool;
 
       mul_code : option (Z^sz -> Z^sz -> Z^sz);
       square_code : option (Z^sz -> Z^sz);
@@ -62,6 +65,8 @@ Module Export CurveParameters.
               coef_div_modulus
               goldilocks
               montgomery
+              freeze
+              ladderstep
               mul_code
               square_code
               upper_bound_of_exponent
@@ -97,6 +102,10 @@ Module Export CurveParameters.
         let montgomery := RawCurveParameters.montgomery CP in
         let s := RawCurveParameters.s CP in
         let c := RawCurveParameters.c CP in
+        let freeze
+            := defaulted
+                 (RawCurveParameters.freeze CP)
+                 (s =? 2^(Qceiling (base * sz))) in
         let goldilocks :=
             defaulted
               (RawCurveParameters.goldilocks CP)
@@ -117,11 +126,13 @@ Module Export CurveParameters.
           s := s;
           c := c;
           carry_chains := defaulted (RawCurveParameters.carry_chains CP) [seq 0 (pred sz); [0; 1]]%nat;
-          a24 := defaulted (RawCurveParameters.a24 CP) 0;
+          a24 := RawCurveParameters.a24 CP;
           coef_div_modulus := defaulted (RawCurveParameters.coef_div_modulus CP) 0%nat;
 
           goldilocks := goldilocks;
           montgomery := montgomery;
+          freeze := freeze;
+          ladderstep := RawCurveParameters.ladderstep CP;
 
           mul_code := RawCurveParameters.mul_code CP;
           square_code := RawCurveParameters.square_code CP;
@@ -159,6 +170,8 @@ Module Export CurveParameters.
           coef_div_modulus := ?coef_div_modulus';
           goldilocks := ?goldilocks';
           montgomery := ?montgomery';
+          freeze := ?freeze';
+          ladderstep := ?ladderstep';
           mul_code := ?mul_code';
           square_code := ?square_code';
           upper_bound_of_exponent := ?upper_bound_of_exponent';
@@ -172,6 +185,8 @@ Module Export CurveParameters.
          let carry_chains' := do_compute carry_chains' in
          let goldilocks' := do_compute goldilocks' in
          let montgomery' := do_compute montgomery' in
+         let freeze' := do_compute freeze' in
+         let ladderstep' := do_compute ladderstep' in
          let allowable_bit_widths' := do_compute allowable_bit_widths' in
          let freeze_allowable_bit_widths' := do_compute freeze_allowable_bit_widths' in
          let modinv_fuel' := do_compute modinv_fuel' in
@@ -186,6 +201,8 @@ Module Export CurveParameters.
                     coef_div_modulus := coef_div_modulus';
                     goldilocks := goldilocks';
                     montgomery := montgomery';
+                    freeze := freeze';
+                    ladderstep := ladderstep';
                     mul_code := mul_code';
                     square_code := square_code';
                     upper_bound_of_exponent := upper_bound_of_exponent';
@@ -221,6 +238,10 @@ Module Export CurveParameters.
     internal_pose_of_CP CP CurveParameters.goldilocks goldilocks.
   Ltac pose_montgomery CP montgomery :=
     internal_pose_of_CP CP CurveParameters.montgomery montgomery.
+  Ltac pose_freeze CP freeze :=
+    internal_pose_of_CP CP CurveParameters.freeze freeze.
+  Ltac pose_ladderstep CP ladderstep :=
+    internal_pose_of_CP CP CurveParameters.ladderstep ladderstep.
   Ltac pose_allowable_bit_widths CP allowable_bit_widths :=
     internal_pose_of_CP CP CurveParameters.allowable_bit_widths allowable_bit_widths.
   Ltac pose_freeze_allowable_bit_widths CP freeze_allowable_bit_widths :=
@@ -295,6 +316,18 @@ Module Export CurveParameters.
     let montgomery := pose_montgomery CP montgomery in
     Tag.update pkg TAG.montgomery montgomery.
 
+  Ltac add_freeze pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let freeze := fresh "freeze" in
+    let freeze := pose_freeze CP freeze in
+    Tag.update pkg TAG.freeze freeze.
+
+  Ltac add_ladderstep pkg :=
+    let CP := Tag.get pkg TAG.CP in
+    let ladderstep := fresh "ladderstep" in
+    let ladderstep := pose_ladderstep CP ladderstep in
+    Tag.update pkg TAG.ladderstep ladderstep.
+
   Ltac add_allowable_bit_widths pkg :=
     let CP := Tag.get pkg TAG.CP in
     let allowable_bit_widths := fresh "allowable_bit_widths" in
@@ -342,6 +375,8 @@ Module Export CurveParameters.
     let pkg := add_coef_div_modulus pkg in
     let pkg := add_goldilocks pkg in
     let pkg := add_montgomery pkg in
+    let pkg := add_freeze pkg in
+    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
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
index 458c1d4ea..7b960a09d 100644
--- a/src/Specific/Framework/CurveParametersPackage.v
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -19,6 +19,22 @@ Ltac if_montgomery pkg tac_true tac_false arg :=
   | false => tac_false arg
   end.
 
+Ltac if_freeze pkg tac_true tac_false arg :=
+  let freeze := Tag.get pkg TAG.freeze in
+  let freeze := (eval vm_compute in (freeze : bool)) in
+  lazymatch freeze with
+  | true => tac_true arg
+  | false => tac_false arg
+  end.
+
+Ltac if_ladderstep pkg tac_true tac_false arg :=
+  let ladderstep := Tag.get pkg TAG.ladderstep in
+  let ladderstep := (eval vm_compute in (ladderstep : bool)) in
+  lazymatch ladderstep with
+  | true => tac_true arg
+  | false => tac_false arg
+  end.
+
 
 Module MakeCurveParametersPackage (PKG : PrePackage).
   Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG.
@@ -43,6 +59,10 @@ Module MakeCurveParametersPackage (PKG : PrePackage).
   Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing).
   Ltac get_montgomery _ := get TAG.montgomery.
   Notation montgomery := (ltac:(let v := get_montgomery () in exact v)) (only parsing).
+  Ltac get_freeze _ := get TAG.freeze.
+  Notation freeze := (ltac:(let v := get_freeze () in exact v)) (only parsing).
+  Ltac get_ladderstep _ := get TAG.ladderstep.
+  Notation ladderstep := (ltac:(let v := get_ladderstep () in exact v)) (only parsing).
   Ltac get_allowable_bit_widths _ := get TAG.allowable_bit_widths.
   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.
diff --git a/src/Specific/Framework/OutputType.v b/src/Specific/Framework/OutputType.v
index 50739c824..463a66a87 100644
--- a/src/Specific/Framework/OutputType.v
+++ b/src/Specific/Framework/OutputType.v
@@ -26,7 +26,7 @@ Section gen.
     Definition rT := ((Tbase b)^curve.(sz))%ctype.
     Definition T' := (interp_flat_type rT).
     Definition RT := (Unit -> rT)%ctype.
-    Definition wt := (wt_gen m curve.(sz)).
+    Definition wt := (wt_gen curve.(base)).
     Definition encode : F m -> Expr RT
       := fun v var
          => Abs
diff --git a/src/Specific/Framework/RawCurveParameters.v b/src/Specific/Framework/RawCurveParameters.v
index b84089eaf..a3f3dd5b8 100644
--- a/src/Specific/Framework/RawCurveParameters.v
+++ b/src/Specific/Framework/RawCurveParameters.v
@@ -32,6 +32,8 @@ Record CurveParameters :=
 
     goldilocks : option bool; (* defaults to true iff the prime ([s-c]) is of the form [2²ᵏ - 2ᵏ - 1] *)
     montgomery : bool;
+    freeze : option bool; (* defaults to true iff [s = 2^(base * sz)] *)
+    ladderstep : bool;
 
     mul_code : option (Z^sz -> Z^sz -> Z^sz);
     square_code : option (Z^sz -> Z^sz);
@@ -55,6 +57,8 @@ Declare Reduction cbv_RawCurveParameters
             coef_div_modulus
             goldilocks
             montgomery
+            freeze
+            ladderstep
             mul_code
             square_code
             upper_bound_of_exponent
diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v
index 5160f441f..879c20aa9 100644
--- a/src/Specific/Framework/ReificationTypes.v
+++ b/src/Specific/Framework/ReificationTypes.v
@@ -130,12 +130,17 @@ Proof.
     assumption.
 Qed.
 
-Ltac pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
-  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)
-           feBW_bounded.
+Ltac pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
+  match (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)
+                feBW_bounded
+  | false
+    => cache_term tt feBW_bounded
+  end.
 
 Ltac pose_phiW feW m wt phiW :=
   cache_term_with_type_by
diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v
index f0703b4ac..55e3a2cb3 100644
--- a/src/Specific/Framework/ReificationTypesPackage.v
+++ b/src/Specific/Framework/ReificationTypesPackage.v
@@ -84,6 +84,7 @@ Ltac add_feBW pkg :=
   Tag.update pkg TAG.feBW feBW.
 
 Ltac add_feBW_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
@@ -92,7 +93,7 @@ Ltac add_feBW_bounded pkg :=
   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 wt sz feBW adjusted_bitwidth' bounds m wt_nonneg 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.
 
 Ltac add_phiW pkg :=
diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index 65577fec6..1642ae7d9 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -242,6 +242,8 @@ def make_curve_parameters(parameters):
                                          nargs,
                                          sz)
     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', ''),
                             ('allowable_bit_widths', '%nat'),
                             ('freeze_extra_allowable_bit_widths', '%nat'),
@@ -279,6 +281,8 @@ Definition curve : CurveParameters :=
 
     goldilocks := %(goldilocks)s;
     montgomery := %(montgomery)s;
+    freeze := %(freeze)s;
+    ladderstep := %(ladderstep)s;
 
     mul_code := %(mul)s;