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, 63 insertions, 57 deletions

diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
index 9c80efaa0..617a36212 100644
--- a/src/Specific/Framework/SynthesisFramework.v
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -1,72 +1,76 @@
-Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework.
-Require Import Crypto.Specific.Framework.ReificationTypes.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.KaratsubaPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage.
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ReificationTypesPackage.
+Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.BoundedWord.
+Require Import Crypto.Util.TagList.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Require Crypto.Specific.Framework.CurveParameters.
 
 Module Export Exports.
-  Export ArithmeticSynthesisFramework.Exports.
+  Export ArithmeticSynthesis.Defaults.Exports.
+  Export ArithmeticSynthesis.Freeze.Exports.
 End Exports.
 
-Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
-  Module AS := MakeArithmeticSynthesisTestTactics Curve.
+(* Alisases for exporting *)
+Module Type PrePackage := PrePackage.
+Module Tag.
+  Notation Context := Tag.Context (only parsing).
+End Tag.
 
-  Ltac get_synthesis_package _ :=
-    let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in
-    lazymatch arithmetic_synthesis_pkg with
-    | (?sz, ?bitwidth, ?s, ?c, ?carry_chains, ?a24, ?coef_div_modulus, ?goldilocks, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chains, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?half_sz, ?half_sz_nonzero, ?sqrt_s, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring)
-      => let reification_types_pkg := get_ReificationTypes_package wt sz m wt_nonneg AS.P.upper_bound_of_exponent in
-         let ladderstep_pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in
-         constr:((arithmetic_synthesis_pkg, reification_types_pkg, ladderstep_pkg))
-    | _ => let dummy := match goal with
-                        | _ => fail "Did you update get_ArithmeticSynthesis_package but forget to update get_synthesis_package?"
-                        end in
-           constr:(I : I)
-    end.
-  Ltac make_synthesis_package _ :=
-    lazymatch goal with
-    | [ |- { T : _ & _ } ]
-      => first [ eexists (_, _, _)
-               | eexists (_, _)
-               | eexists ]
-    | [ |- _ ] => idtac
-    end;
-    let pkg := get_synthesis_package () in
-    exact pkg.
-End MakeSynthesisTactics.
+Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
+  Module P := FillCurveParameters Curve.
 
-Local Notation eta2 x := (fst x, snd x) (only parsing).
-Local Notation eta3 x := (eta2 (fst x), snd x) (only parsing).
+  Ltac add_Synthesis_package pkg :=
+    let P_default_mul _ := P.default_mul in
+    let P_extra_prove_mul_eq _ := P.extra_prove_mul_eq in
+    let P_default_square _ := P.default_square in
+    let P_extra_prove_square_eq _ := P.extra_prove_square_eq in
+    let pkg := P.add_CurveParameters_package pkg in
+    let pkg := add_Base_package pkg in
+    let pkg := add_ReificationTypes_package pkg in
+    let pkg := add_Karatsuba_package pkg in
+    (* N.B. freeze is a "default" and must come after anything that may disable it *)
+    let pkg := add_Freeze_package pkg in
+    (* N.B. the Defaults must come after other possible ways of adding the _sig lemmas *)
+    let pkg := add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq in
+    (* N.B. Ladderstep must come after Defaults *)
+    let pkg := add_Ladderstep_package pkg in
+    pkg.
 
-Notation Synthesis_package'_Type :=
-  { ABC : _ & let '(a, b, c) := eta3 ABC in (a * b * c)%type } (only parsing).
+  Ltac get_Synthesis_package _ :=
+    let pkg := constr:(Tag.empty) in
+    add_Synthesis_package pkg.
 
-Module Type SynthesisPrePackage.
-  Parameter Synthesis_package' : Synthesis_package'_Type.
-  Parameter Synthesis_package : let '(a, b, c) := eta3 (projT1 Synthesis_package') in (a * b * c)%type.
-End SynthesisPrePackage.
+  Ltac make_Synthesis_package _ :=
+    let pkg := get_Synthesis_package () in
+    exact pkg.
+End MakeSynthesisTactics.
 
-Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : SynthesisPrePackage).
-  Module CP := CurveParameters.FillCurveParameters Curve.
+Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePackage).
+  Module P := CurveParameters.FillCurveParameters Curve.
 
-  Module PP <: ReificationTypesPrePackage <: ArithmeticSynthesisPrePackage <: LadderstepPrePackage.
-    Definition ArithmeticSynthesis_package := Eval compute in let '(a, b, c) := P.Synthesis_package in a.
-    Definition ArithmeticSynthesis_package' : { T : _ & T } := existT _ _ ArithmeticSynthesis_package.
-    Definition ReificationTypes_package := Eval compute in let '(a, b, c) := P.Synthesis_package in b.
-    Definition ReificationTypes_package' : { T : _ & T } := existT _ _ ReificationTypes_package.
-    Definition Ladderstep_package := Eval compute in let '(a, b, c) := P.Synthesis_package in c.
-    Definition Ladderstep_package' : { T : _ & T } := existT _ _ Ladderstep_package.
-  End PP.
-  Module RT := MakeReificationTypes PP.
-  Module AS := MakeArithmeticSynthesisTest PP.
-  Module LS := MakeLadderstep PP.
-  Include RT.
-  Include AS.
-  Include LS.
+  Module CP := MakeCurveParametersPackage PKG.
+  Module BP := MakeBasePackage PKG.
+  Module DP := MakeDefaultsPackage PKG.
+  Module RP := MakeReificationTypesPackage PKG.
+  Module FP := MakeFreezePackage PKG.
+  Module LP := MakeLadderstepPackage PKG.
+  Module KP := MakeKaratsubaPackage PKG.
+  Include CP.
+  Include BP.
+  Include DP.
+  Include RP.
+  Include FP.
+  Include LP.
+  Include KP.
 
   Ltac synthesize_with_carry do_rewrite get_op_sig :=
     let carry_sig := get_carry_sig () in
@@ -75,7 +79,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
     [ do_rewrite op_sig carry_sig; cbv_runtime
     | .. ];
     fin_preglue;
-    refine_reflectively_gen CP.allowable_bit_widths default.
+    refine_reflectively_gen P.allowable_bit_widths default.
   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 :=
@@ -84,6 +88,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
   Ltac synthesize_mul _ := synthesize_2arg_with_carry get_mul_sig.
   Ltac synthesize_add _ := synthesize_2arg_with_carry get_add_sig.
   Ltac synthesize_sub _ := synthesize_2arg_with_carry get_sub_sig.
+  Ltac synthesize_opp _ := synthesize_1arg_with_carry get_opp_sig.
   Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig.
   Ltac synthesize_freeze _ :=
     let freeze_sig := get_freeze_sig () in
@@ -92,7 +97,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
     [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime
     | .. ];
     fin_preglue;
-    refine_reflectively_gen CP.freeze_allowable_bit_widths anf.
+    refine_reflectively_gen P.freeze_allowable_bit_widths anf.
   Ltac synthesize_xzladderstep _ :=
     let Mxzladderstep_sig := get_Mxzladderstep_sig () in
     let a24_sig := get_a24_sig () in
@@ -104,5 +109,6 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis
       cbv_runtime
     | .. ];
     finish_conjoined_preglue ();
-    refine_reflectively_gen CP.allowable_bit_widths default.
+    refine_reflectively_gen P.allowable_bit_widths default.
+
 End PackageSynthesis.