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

diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index aeaef91db..afed1243c 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -216,7 +216,10 @@ def make_curve_parameters(parameters):
                             ('coef_div_modulus', '%nat'),
                             ('modinv_fuel', '%nat')):
         replacements[k] = fix_option(nested_list_to_string(replacements.get(k, 'None')), scope_string=scope_string)
-    for k in ('s', 'c', 'goldilocks'):
+    for k in ('montgomery', ):
+        if k not in replacements.keys():
+            replacements[k] = False
+    for k in ('s', 'c', 'goldilocks', 'montgomery'):
         replacements[k] = nested_list_to_string(replacements[k])
     for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'):
         if k not in replacements.keys():
@@ -240,6 +243,7 @@ Module Curve <: CurveParameters.
   Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *)
 
   Definition goldilocks : bool := %(goldilocks)s.
+  Definition montgomery : bool := %(montgomery)s.
 
   Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
     := %(mul)s.
@@ -271,9 +275,10 @@ End P.
 Module Export S := PackageSynthesis Curve P.
 """ % prefix
 
-def make_synthesized_arg(fearg, prefix):
+def make_synthesized_arg(fearg, prefix, montgomery=False):
     if fearg in ('femul', 'fesub', 'feadd'):
-        return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+        if not montgomery:
+            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import %(prefix)s.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -288,6 +293,22 @@ Time Defined.
 
 Print Assumptions %(arg)s.
 """ % {'prefix':prefix, 'arg':fearg[2:]}
+        else:
+            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import %(prefix)s.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition %(arg)s :
+  { %(arg)s : feBW_small -> feBW_small -> feBW_small
+  | forall a b, phiM_small (%(arg)s a b) = F.%(arg)s (phiM_small a) (phiM_small b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_%(arg)s ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions %(arg)s.
+""" % {'prefix':prefix, 'arg':fearg[2:]}
     elif fearg in ('fesquare',):
         return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import %(prefix)s.Synthesis.
@@ -321,7 +342,8 @@ Time Defined.
 Print Assumptions freeze.
 """ % {'prefix':prefix}
     elif fearg in ('feopp',):
-        return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+        if not montgomery:
+            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import %(prefix)s.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -336,6 +358,43 @@ Time Defined.
 
 Print Assumptions %(arg)s.
 """ % {'prefix':prefix, 'arg':fearg[2:]}
+        else:
+            return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import %(prefix)s.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition %(arg)s :
+  { %(arg)s : feBW_small -> feBW_small
+  | forall a, phiM_small (%(arg)s a) = F.%(arg)s (phiM_small a) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_%(arg)s ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions %(arg)s.
+""" % {'prefix':prefix, 'arg':fearg[2:]}
+    elif fearg in ('fenz',):
+        assert(fearg == 'fenz')
+        assert(montgomery)
+        full_arg = 'nonzero'
+        return r"""Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import %(prefix)s.Synthesis.
+Local Open Scope Z_scope.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition %(full_arg)s :
+  { %(full_arg)s : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1
+  | forall a, (BoundedWord.BoundedWordToZ _ _ _ (%(full_arg)s a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_%(full_arg)s ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions %(full_arg)s.
+""" % {'prefix':prefix, 'full_arg':full_arg}
     elif fearg in ('ladderstep', 'xzladderstep'):
         return r"""Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -411,7 +470,7 @@ def main(*args):
     outputs['CurveParameters.v'] = make_curve_parameters(parameters)
     outputs['Synthesis.v'] = make_synthesis(output_prefix)
     for arg in parameters['operations']:
-        outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix)
+        outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix, montgomery=(parameters.get('montgomery', 'false') == 'true'))
         outputs[arg + 'Display.v'] = make_display_arg(arg, output_prefix)
     for fname in parameters.get('extra_files', []):
         outputs[os.path.basename(fname)] = open(os.path.join(parameters_folder, fname), 'r').read()