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, 25 insertions, 5 deletions

diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 7078d4bec..4aa255d11 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -28,6 +28,7 @@ Module Type CurveParameters.
   Parameter coef_div_modulus : option nat.
 
   Parameter goldilocks : bool.
+  Parameter montgomery : bool.
 
   Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz).
   Parameter square_code : option (Z^sz -> Z^sz).
@@ -43,7 +44,7 @@ Module Type CurveParameters.
 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.
+  Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel.
 End TAG.
 
 Module FillCurveParameters (P : CurveParameters).
@@ -66,6 +67,7 @@ Module FillCurveParameters (P : CurveParameters).
   Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat.
 
   Definition goldilocks := P.goldilocks.
+  Definition montgomery := P.montgomery.
 
   Ltac default_mul :=
     lazymatch (eval hnf in P.mul_code) with
@@ -82,7 +84,9 @@ Module FillCurveParameters (P : CurveParameters).
 
   Definition upper_bound_of_exponent
     := defaulted P.upper_bound_of_exponent
-                 (fun exp => (2^exp + 2^(exp-3))%Z).
+                 (if P.montgomery
+                  then (fun exp => (2^exp - 1)%Z)
+                  else (fun exp => (2^exp + 2^(exp-3))%Z)).
   Local Notation list_8_if_not_exists ls :=
     (if existsb (Nat.eqb 8) ls
      then nil
@@ -91,7 +95,10 @@ Module FillCurveParameters (P : CurveParameters).
   Definition allowable_bit_widths
     := defaulted
          P.allowable_bit_widths
-         (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat.
+         ((if P.montgomery
+           then [8]
+           else nil)
+            ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat.
   Definition freeze_allowable_bit_widths
     := defaulted
          P.freeze_extra_allowable_bit_widths
@@ -109,6 +116,7 @@ Module FillCurveParameters (P : CurveParameters).
     let P_a24 := P.a24 in
     let P_coef_div_modulus := P.coef_div_modulus in
     let P_goldilocks := P.goldilocks in
+    let P_montgomery := P.montgomery in
     let P_mul_code := P.mul_code in
     let P_square_code := P.square_code in
     let P_upper_bound_of_exponent := P.upper_bound_of_exponent in
@@ -117,8 +125,8 @@ Module FillCurveParameters (P : CurveParameters).
     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 modinv_fuel
-                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_modinv_fuel
+                           sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks montgomery modinv_fuel
+                           P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_montgomery 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
@@ -141,6 +149,7 @@ Module FillCurveParameters (P : CurveParameters).
   Local Notation P_a24 := a24.
   Local Notation P_coef_div_modulus := coef_div_modulus.
   Local Notation P_goldilocks := goldilocks.
+  Local Notation P_montgomery := montgomery.
   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.
@@ -183,6 +192,11 @@ Module FillCurveParameters (P : CurveParameters).
       bool
       ltac:(let v := do_compute P_goldilocks in exact v)
              goldilocks.
+  Ltac pose_montgomery montgomery :=
+    cache_term_with_type_by
+      bool
+      ltac:(let v := do_compute P_montgomery in exact v)
+             montgomery.
 
   Ltac pose_modinv_fuel modinv_fuel :=
     cache_term_with_type_by
@@ -237,6 +251,11 @@ Module FillCurveParameters (P : CurveParameters).
     let goldilocks := pose_goldilocks goldilocks in
     Tag.update pkg TAG.goldilocks goldilocks.
 
+  Ltac add_montgomery pkg :=
+    let montgomery := fresh "montgomery" in
+    let montgomery := pose_montgomery montgomery in
+    Tag.update pkg TAG.montgomery montgomery.
+
   Ltac add_modinv_fuel pkg :=
     let modinv_fuel := fresh "modinv_fuel" in
     let modinv_fuel := pose_modinv_fuel modinv_fuel in
@@ -256,6 +275,7 @@ Module FillCurveParameters (P : CurveParameters).
     let pkg := add_a24 pkg in
     let pkg := add_coef_div_modulus pkg in
     let pkg := add_goldilocks pkg in
+    let pkg := add_montgomery pkg in
     let pkg := add_modinv_fuel pkg in
     let pkg := add_upper_bound_of_exponent pkg in
     Tag.strip_local pkg.