Support p256 / montgomery in json format

Extra time comes from adding AMD128 to NISTP256, mostly.

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
13m25.13s | Total                                                    | 13m30.82s || -0m05.69s
---------------------------------------------------------------------------------------------
   N/A    | Specific/IntegrationTestMontgomeryP256_128               | 0m25.42s  || -0m25.42s
0m22.75s  | Specific/NISTP256/AMD128/femul                           |    N/A    || +0m22.75s
1m31.64s  | Specific/NISTP256/AMD64/femul                            | 1m52.42s  || -0m20.78s
0m14.46s  | Specific/NISTP256/AMD128/fesub                           |    N/A    || +0m14.46s
0m14.25s  | Specific/NISTP256/AMD128/feadd                           |    N/A    || +0m14.25s
0m14.12s  | Specific/NISTP256/AMD128/fenz                            |    N/A    || +0m14.11s
   N/A    | Specific/NISTP256/AMD64/MontgomeryP256                   | 0m13.00s  || -0m13.00s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Sub           | 0m12.40s  || -0m12.40s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Add           | 0m11.99s  || -0m11.99s
0m11.74s  | Specific/NISTP256/AMD128/feopp                           |    N/A    || +0m11.74s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Opp           | 0m11.22s  || -0m11.22s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Nonzero       | 0m09.27s  || -0m09.26s
   N/A    | Specific/MontgomeryP256_128                              | 0m09.26s  || -0m09.25s
0m08.42s  | Specific/NISTP256/AMD64/Synthesis                        |    N/A    || +0m08.41s
0m14.67s  | Specific/NISTP256/AMD64/fenz                             | 0m09.98s  || +0m04.68s
0m04.12s  | Specific/Framework/ArithmeticSynthesis/Montgomery        |    N/A    || +0m04.12s
0m03.58s  | Specific/NISTP256/AMD128/Synthesis                       |    N/A    || +0m03.58s
1m10.78s  | Specific/X2555/C128/ladderstep                           | 1m08.36s  || +0m02.42s
1m02.10s  | Specific/X25519/C32/femul                                | 1m00.59s  || +0m01.50s
0m43.59s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m44.86s  || -0m01.26s
0m34.97s  | Specific/X25519/C32/fesquare                             | 0m35.98s  || -0m01.00s
0m20.10s  | Specific/NISTP256/AMD64/fesub                            | 0m18.37s  || +0m01.73s
0m17.61s  | Specific/NISTP256/AMD64/feadd                            | 0m15.94s  || +0m01.67s
2m09.77s  | Specific/X25519/C64/ladderstep                           | 2m09.79s  || -0m00.01s
1m11.70s  | Specific/X2448/Karatsuba/C64/femul                       | 1m11.60s  || +0m00.10s
0m32.14s  | Specific/X25519/C32/Synthesis                            | 0m31.70s  || +0m00.44s
0m27.94s  | Specific/X25519/C32/freeze                               | 0m28.06s  || -0m00.11s
0m17.62s  | Specific/X25519/C64/femul                                | 0m17.41s  || +0m00.21s
0m15.21s  | Specific/X25519/C64/freeze                               | 0m14.74s  || +0m00.47s
0m14.86s  | Specific/NISTP256/AMD64/feopp                            | 0m14.96s  || -0m00.10s
0m14.58s  | Specific/X25519/C64/fesquare                             | 0m14.06s  || +0m00.51s
0m10.10s  | Specific/X25519/C64/Synthesis                            | 0m09.78s  || +0m00.32s
0m06.22s  | Specific/X2555/C128/Synthesis                            | 0m06.17s  || +0m00.04s
0m01.01s  | Specific/X25519/C32/CurveParameters                      | 0m01.05s  || -0m00.04s
0m00.99s  | Specific/Framework/SynthesisFramework                    | 0m01.08s  || -0m00.09s
0m00.79s  | Specific/Framework/MontgomeryReificationTypes            |    N/A    || +0m00.79s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.70s  || +0m00.08s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.75s  || +0m00.03s
0m00.76s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage |    N/A    || +0m00.76s
0m00.75s  | Specific/Framework/IntegrationTestTemporaryMiscCommon    | 0m00.80s  || -0m00.05s
0m00.75s  | Specific/Framework/MontgomeryReificationTypesPackage     |    N/A    || +0m00.75s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m00.75s  || -0m00.02s
0m00.72s  | Specific/Framework/ReificationTypesPackage               | 0m00.70s  || +0m00.02s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/Base              | 0m00.73s  || -0m00.01s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.69s  || +0m00.03s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s  || -0m00.04s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.75s  || -0m00.05s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.77s  || -0m00.07s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.71s  || -0m00.02s
0m00.67s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.74s  || -0m00.06s
0m00.43s  | Specific/X25519/C64/CurveParameters                      | 0m00.43s  || +0m00.00s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommon          | 0m00.40s  || -0m00.02s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommonTactics   | 0m00.37s  || +0m00.01s
0m00.34s  | Specific/Framework/CurveParameters                       | 0m00.32s  || +0m00.02s
0m00.33s  | Specific/X2555/C128/CurveParameters                      | 0m00.33s  || +0m00.00s
0m00.32s  | Specific/NISTP256/AMD128/CurveParameters                 |    N/A    || +0m00.32s
0m00.32s  | Specific/X2448/Karatsuba/C64/CurveParameters             | 0m00.33s  || -0m00.01s
0m00.31s  | Specific/Framework/CurveParametersPackage                | 0m00.33s  || -0m00.02s
0m00.30s  | Specific/NISTP256/AMD64/CurveParameters                  |    N/A    || +0m00.30s

1 files changed, 46 insertions, 5 deletions

diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v
index 617a36212..01f91731e 100644
--- a/src/Specific/Framework/SynthesisFramework.v
+++ b/src/Specific/Framework/SynthesisFramework.v
@@ -3,8 +3,10 @@ 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.ArithmeticSynthesis.MontgomeryPackage.
 Require Import Crypto.Specific.Framework.CurveParametersPackage.
 Require Import Crypto.Specific.Framework.ReificationTypesPackage.
+Require Import Crypto.Specific.Framework.MontgomeryReificationTypesPackage.
 Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -37,7 +39,9 @@ Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters).
     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_Montgomery_package pkg in
+    let pkg := add_MontgomeryReificationTypes_package pkg in
+    (* N.B. freeze is a "default" and must come after montgomery, which disables 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
@@ -64,6 +68,8 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack
   Module FP := MakeFreezePackage PKG.
   Module LP := MakeLadderstepPackage PKG.
   Module KP := MakeKaratsubaPackage PKG.
+  Module MP := MakeMontgomeryPackage PKG.
+  Module MRP := MakeMontgomeryReificationTypesPackage PKG.
   Include CP.
   Include BP.
   Include DP.
@@ -71,6 +77,8 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack
   Include FP.
   Include LP.
   Include KP.
+  Include MP.
+  Include MRP.
 
   Ltac synthesize_with_carry do_rewrite get_op_sig :=
     let carry_sig := get_carry_sig () in
@@ -85,10 +93,39 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack
   Ltac synthesize_1arg_with_carry get_op_sig :=
     synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig.
 
-  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_montgomery get_op_sig get_op_bounded :=
+    let phi := get_phi_for_preglue () in
+    let op_sig := get_op_sig () in
+    let op_bounded := get_op_bounded () in
+    let do_red _ :=
+        lazymatch (eval cbv [phi] in phi) with
+        | (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _)))
+          => cbv [feBW_of_feBW_small meval]
+        end in
+    start_preglue;
+    do_red ();
+    [ do_rewrite_with_sig_by op_sig op_sig_side_conditions_t;
+      cbv_runtime
+    | .. ];
+    fin_preglue;
+    factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t;
+    refine_reflectively_gen P.allowable_bit_widths anf.
+
+  Ltac synthesize_2arg_choice get_op_sig get_op_bounded :=
+    lazymatch (eval vm_compute in P.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 :=
+    lazymatch (eval vm_compute in P.montgomery) with
+    | true => synthesize_montgomery get_op_sig get_op_bounded
+    | false => synthesize_1arg_with_carry get_op_sig
+    end.
+
+  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_freeze _ :=
     let freeze_sig := get_freeze_sig () in
@@ -110,5 +147,9 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack
     | .. ];
     finish_conjoined_preglue ();
     refine_reflectively_gen P.allowable_bit_widths default.
+  Ltac synthesize_nonzero _ :=
+    let op_sig := get_nonzero_sig () in
+    nonzero_preglue op_sig ltac:(fun _ => cbv_runtime);
+    refine_reflectively_gen P.allowable_bit_widths anf.
 
 End PackageSynthesis.