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, 39 insertions, 0 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
new file mode 100644
index 000000000..9314f369e
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
@@ -0,0 +1,39 @@
+(* This file is autogenerated from Freeze.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Freeze.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := freeze_sig.
+End TAG.
+
+Ltac add_freeze_sig pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.freeze_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 c := Tag.get pkg TAG.c in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let bitwidth := Tag.get pkg TAG.bitwidth in
+                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
+                   let wt_pos := Tag.get pkg TAG.wt_pos in
+                   let wt_divides := Tag.get pkg TAG.wt_divides in
+                   let wt_multiples := Tag.get pkg TAG.wt_multiples in
+                   let freeze_sig := fresh "freeze_sig" in
+                   let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in
+                   constr:(freeze_sig)).
+Ltac add_Freeze_package pkg :=
+  let pkg := add_freeze_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeFreezePackage (PKG : PrePackage).
+  Module Import MakeFreezePackageInternal := MakePackageBase PKG.
+
+  Ltac get_freeze_sig _ := get TAG.freeze_sig.
+  Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
+End MakeFreezePackage.