Reorganize the curve-specific synthesis framework

This brings in most of the changes that I made when figuring out how to
integrate montgomery into the framework.

The code is a bit slower because the we drop `Print Assumptions` at the
bottom of each synthesis problem, to record that things are closed under
the global context.  If we remove this, we get back the time that we
lost with this commit.

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
13m10.63s | Total                                                    | 11m51.91s || +1m18.71s
---------------------------------------------------------------------------------------------
1m15.83s  | Specific/X2555/C128/ladderstep                           | 1m02.57s  || +0m13.25s
1m03.07s  | Specific/X25519/C32/femul                                | 0m54.99s  || +0m08.07s
0m36.49s  | Specific/X25519/C32/fesquare                             | 0m27.77s  || +0m08.72s
1m08.99s  | Specific/X2448/Karatsuba/C64/femul                       | 1m01.88s  || +0m07.10s
0m26.82s  | Specific/X25519/C32/freeze                               | 0m19.81s  || +0m07.01s
2m06.29s  | Specific/X25519/C64/ladderstep                           | 2m00.03s  || +0m06.26s
0m17.48s  | Specific/X25519/C64/femul                                | 0m10.81s  || +0m06.67s
0m14.78s  | Specific/X25519/C64/freeze                               | 0m08.19s  || +0m06.58s
0m14.12s  | Specific/X25519/C64/fesquare                             | 0m07.45s  || +0m06.66s
1m48.54s  | Specific/NISTP256/AMD64/femul                            | 1m51.58s  || -0m03.04s
0m44.50s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m43.81s  || +0m00.68s
0m31.40s  | Specific/X25519/C32/Synthesis                            | 0m31.02s  || +0m00.37s
0m25.72s  | Specific/IntegrationTestMontgomeryP256_128               | 0m25.34s  || +0m00.37s
0m18.36s  | Specific/NISTP256/AMD64/fesub                            | 0m18.79s  || -0m00.42s
0m16.45s  | Specific/NISTP256/AMD64/feadd                            | 0m16.40s  || +0m00.05s
0m15.15s  | Specific/NISTP256/AMD64/feopp                            | 0m14.79s  || +0m00.36s
0m12.27s  | Specific/IntegrationTestMontgomeryP256_128_Sub           | 0m11.90s  || +0m00.36s
0m12.06s  | Specific/IntegrationTestMontgomeryP256_128_Add           | 0m11.89s  || +0m00.16s
0m10.93s  | Specific/IntegrationTestMontgomeryP256_128_Opp           | 0m11.39s  || -0m00.46s
0m10.12s  | Specific/X25519/C64/Synthesis                            | 0m09.86s  || +0m00.25s
0m09.86s  | Specific/NISTP256/AMD64/fenz                             | 0m09.54s  || +0m00.32s
0m09.40s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero       | 0m09.16s  || +0m00.24s
0m06.08s  | Specific/X2555/C128/Synthesis                            | 0m05.72s  || +0m00.36s
0m01.06s  | Specific/Framework/SynthesisFramework                    | 0m00.98s  || +0m00.08s
0m01.05s  | Specific/X25519/C32/CurveParameters                      | 0m01.01s  || +0m00.04s
0m00.88s  | Specific/Framework/ReificationTypes                      | 0m00.84s  || +0m00.04s
   N/A    | Specific/Framework/ArithmeticSynthesisFramework          | 0m00.82s  || -0m00.82s
0m00.81s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         |    N/A    || +0m00.81s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     |    N/A    || +0m00.79s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/Base              |    N/A    || +0m00.79s
0m00.79s  | Specific/Framework/ArithmeticSynthesis/Freeze            |    N/A    || +0m00.79s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/BasePackage       |    N/A    || +0m00.78s
0m00.76s  | Specific/Framework/IntegrationTestTemporaryMiscCommon    | 0m00.78s  || -0m00.02s
0m00.74s  | Specific/Framework/ArithmeticSynthesis/HelperTactics     |    N/A    || +0m00.74s
0m00.74s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  |    N/A    || +0m00.74s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     |    N/A    || +0m00.73s
0m00.72s  | Specific/Framework/ReificationTypesPackage               |    N/A    || +0m00.72s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Defaults          |    N/A    || +0m00.70s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage |    N/A    || +0m00.69s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   |    N/A    || +0m00.69s
0m00.68s  | Specific/Framework/ArithmeticSynthesis/Ladderstep        |    N/A    || +0m00.68s
   N/A    | Specific/Framework/LadderstepSynthesisFramework          | 0m00.68s  || -0m00.68s
0m00.42s  | Specific/Framework/IntegrationTestDisplayCommon          | 0m00.39s  || +0m00.02s
0m00.40s  | Specific/X25519/C64/CurveParameters                      | 0m00.44s  || -0m00.03s
0m00.34s  | Specific/Framework/IntegrationTestDisplayCommonTactics   | 0m00.35s  || -0m00.00s
0m00.33s  | Specific/X2555/C128/CurveParameters                      | 0m00.31s  || +0m00.02s
0m00.33s  | Specific/Framework/CurveParameters                       | 0m00.31s  || +0m00.02s
0m00.33s  | Specific/Framework/CurveParametersPackage                |    N/A    || +0m00.33s
0m00.31s  | Specific/X2448/Karatsuba/C64/CurveParameters             | 0m00.32s  || -0m00.01s
0m00.07s  | Specific/Framework/Packages                              |    N/A    || +0m00.07s

1 files changed, 155 insertions, 8 deletions

diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 2d0bf5152..7078d4bec 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -1,6 +1,8 @@
 Require Export Coq.ZArith.BinInt.
 Require Export Coq.Lists.List.
 Require Export Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Import Crypto.Util.TagList.
 Require Crypto.Util.Tuple.
 
 Module Export Notations.
@@ -23,7 +25,7 @@ Module Type CurveParameters.
   Parameter carry_chains
     : option (list (list nat)). (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *)
   Parameter a24 : option Z.
-  Parameter coef_div_modulus : nat.
+  Parameter coef_div_modulus : option nat.
 
   Parameter goldilocks : bool.
 
@@ -35,10 +37,15 @@ Module Type CurveParameters.
     : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *)
   Parameter freeze_extra_allowable_bit_widths
     : option (list nat). (* defaults to [8 :: nil] *)
+  Parameter modinv_fuel : option nat.
   Ltac extra_prove_mul_eq := idtac.
   Ltac extra_prove_square_eq := idtac.
 End CurveParameters.
 
+Module TAG.
+  Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel.
+End TAG.
+
 Module FillCurveParameters (P : CurveParameters).
   Local Notation defaulted opt_v default
     := (match opt_v with
@@ -56,7 +63,7 @@ Module FillCurveParameters (P : CurveParameters).
   Definition c := P.c.
   Definition carry_chains := defaulted P.carry_chains [seq 0 (pred sz); [0; 1]]%nat.
   Definition a24 := defaulted P.a24 0.
-  Definition coef_div_modulus := P.coef_div_modulus.
+  Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat.
 
   Definition goldilocks := P.goldilocks.
 
@@ -74,11 +81,23 @@ Module FillCurveParameters (P : CurveParameters).
     end.
 
   Definition upper_bound_of_exponent
-    := defaulted P.upper_bound_of_exponent (fun exp => (2^exp + 2^(exp-3))%Z).
+    := defaulted P.upper_bound_of_exponent
+                 (fun exp => (2^exp + 2^(exp-3))%Z).
+  Local Notation list_8_if_not_exists ls :=
+    (if existsb (Nat.eqb 8) ls
+     then nil
+     else [8]%nat)
+      (only parsing).
   Definition allowable_bit_widths
-    := defaulted P.allowable_bit_widths (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat.
+    := defaulted
+         P.allowable_bit_widths
+         (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat.
   Definition freeze_allowable_bit_widths
-    := defaulted P.freeze_extra_allowable_bit_widths [8]%nat ++ allowable_bit_widths.
+    := defaulted
+         P.freeze_extra_allowable_bit_widths
+         (list_8_if_not_exists allowable_bit_widths)
+         ++ allowable_bit_widths.
+  Definition modinv_fuel := defaulted P.modinv_fuel 10%nat.
 
   (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *)
   Ltac do_unfold v' :=
@@ -95,10 +114,11 @@ Module FillCurveParameters (P : CurveParameters).
     let P_upper_bound_of_exponent := P.upper_bound_of_exponent in
     let P_allowable_bit_widths := P.allowable_bit_widths in
     let P_freeze_extra_allowable_bit_widths := P.freeze_extra_allowable_bit_widths in
+    let P_modinv_fuel := P.modinv_fuel in
     let v' := (eval cbv [id
                            List.app
-                           sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks
-                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks
+                           sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks modinv_fuel
+                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_modinv_fuel
                            P_mul_code P_square_code
                            upper_bound_of_exponent allowable_bit_widths freeze_allowable_bit_widths
                            P_upper_bound_of_exponent P_allowable_bit_widths P_freeze_extra_allowable_bit_widths
@@ -112,4 +132,131 @@ Module FillCurveParameters (P : CurveParameters).
          (only parsing).
   Ltac extra_prove_mul_eq := P.extra_prove_mul_eq.
   Ltac extra_prove_square_eq := P.extra_prove_square_eq.
-End FillCurveParameters.
+
+  Local Notation P_sz := sz.
+  Local Notation P_bitwidth := bitwidth.
+  Local Notation P_s := s.
+  Local Notation P_c := c.
+  Local Notation P_carry_chains := carry_chains.
+  Local Notation P_a24 := a24.
+  Local Notation P_coef_div_modulus := coef_div_modulus.
+  Local Notation P_goldilocks := goldilocks.
+  Local Notation P_upper_bound_of_exponent := upper_bound_of_exponent.
+  Local Notation P_allowable_bit_widths := allowable_bit_widths.
+  Local Notation P_freeze_allowable_bit_widths := freeze_allowable_bit_widths.
+  Local Notation P_modinv_fuel := modinv_fuel.
+
+  Ltac pose_sz sz :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := do_compute P_sz in exact v)
+             sz.
+  Ltac pose_bitwidth bitwidth :=
+    cache_term_with_type_by
+      Z
+      ltac:(let v := do_compute P_bitwidth in exact v)
+             bitwidth.
+  Ltac pose_s s := (* don't want to compute, e.g., [2^255] *)
+    cache_term_with_type_by
+      Z
+      ltac:(let v := do_unfold P_s in exact v)
+             s.
+  Ltac pose_c c :=
+    cache_term_with_type_by
+      (list limb)
+      ltac:(let v := do_compute P_c in exact v)
+             c.
+  Ltac pose_carry_chains carry_chains :=
+    let v := do_compute P_carry_chains in
+    cache_term v carry_chains.
+
+  Ltac pose_a24 a24 :=
+    let v := do_compute P_a24 in
+    cache_term v a24.
+  Ltac pose_coef_div_modulus coef_div_modulus :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := do_compute P_coef_div_modulus in exact v)
+             coef_div_modulus.
+  Ltac pose_goldilocks goldilocks :=
+    cache_term_with_type_by
+      bool
+      ltac:(let v := do_compute P_goldilocks in exact v)
+             goldilocks.
+
+  Ltac pose_modinv_fuel modinv_fuel :=
+    cache_term_with_type_by
+      nat
+      ltac:(let v := do_compute P_modinv_fuel in exact v)
+             modinv_fuel.
+
+  Ltac pose_upper_bound_of_exponent upper_bound_of_exponent :=
+    cache_term_with_type_by
+      (Z -> Z)
+      ltac:(let v := do_unfold P_upper_bound_of_exponent in exact v)
+             upper_bound_of_exponent.
+
+  (* Everything below this line autogenerated by remake_packages.py *)
+  Ltac add_sz pkg :=
+    let sz := fresh "sz" in
+    let sz := pose_sz sz in
+    Tag.update pkg TAG.sz sz.
+
+  Ltac add_bitwidth pkg :=
+    let bitwidth := fresh "bitwidth" in
+    let bitwidth := pose_bitwidth bitwidth in
+    Tag.update pkg TAG.bitwidth bitwidth.
+
+  Ltac add_s pkg :=
+    let s := fresh "s" in
+    let s := pose_s s in
+    Tag.update pkg TAG.s s.
+
+  Ltac add_c pkg :=
+    let c := fresh "c" in
+    let c := pose_c c in
+    Tag.update pkg TAG.c c.
+
+  Ltac add_carry_chains pkg :=
+    let carry_chains := fresh "carry_chains" in
+    let carry_chains := pose_carry_chains carry_chains in
+    Tag.update pkg TAG.carry_chains carry_chains.
+
+  Ltac add_a24 pkg :=
+    let a24 := fresh "a24" in
+    let a24 := pose_a24 a24 in
+    Tag.update pkg TAG.a24 a24.
+
+  Ltac add_coef_div_modulus pkg :=
+    let coef_div_modulus := fresh "coef_div_modulus" in
+    let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in
+    Tag.update pkg TAG.coef_div_modulus coef_div_modulus.
+
+  Ltac add_goldilocks pkg :=
+    let goldilocks := fresh "goldilocks" in
+    let goldilocks := pose_goldilocks goldilocks in
+    Tag.update pkg TAG.goldilocks goldilocks.
+
+  Ltac add_modinv_fuel pkg :=
+    let modinv_fuel := fresh "modinv_fuel" in
+    let modinv_fuel := pose_modinv_fuel modinv_fuel in
+    Tag.update pkg TAG.modinv_fuel modinv_fuel.
+
+  Ltac add_upper_bound_of_exponent pkg :=
+    let upper_bound_of_exponent := fresh "upper_bound_of_exponent" in
+    let upper_bound_of_exponent := pose_upper_bound_of_exponent upper_bound_of_exponent in
+    Tag.update pkg TAG.upper_bound_of_exponent upper_bound_of_exponent.
+
+  Ltac add_CurveParameters_package pkg :=
+    let pkg := add_sz pkg in
+    let pkg := add_bitwidth pkg in
+    let pkg := add_s pkg in
+    let pkg := add_c pkg in
+    let pkg := add_carry_chains pkg in
+    let pkg := add_a24 pkg in
+    let pkg := add_coef_div_modulus pkg in
+    let pkg := add_goldilocks pkg in
+    let pkg := add_modinv_fuel pkg in
+    let pkg := add_upper_bound_of_exponent pkg in
+    Tag.strip_local pkg.
+End FillCurveParameters.
\ No newline at end of file