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, 52 insertions, 19 deletions

diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index 56c91e577..aeaef91db 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 from __future__ import with_statement
-import json, sys, os, math, re, shutil
+import json, sys, os, math, re, shutil, io
 
 def compute_bitwidth(base):
     return 2**int(math.ceil(math.log(base, 2)))
@@ -175,12 +175,13 @@ def nested_list_to_string(v):
         assert(False)
 
 def make_curve_parameters(parameters):
-    def fix_option(term):
+    def fix_option(term, scope_string=''):
         if not isinstance(term, str) and not isinstance(term, unicode):
             return term
         if term[:len('Some ')] != 'Some ' and term != 'None':
-            if ' ' in term: return 'Some (%s)' % term
-            return 'Some %s' % term
+            if ' ' in term and (term[0] + term[-1]) not in ('()', '[]'):
+                return 'Some (%s)%s' % (term, scope_string)
+            return 'Some %s%s' % (term, scope_string)
         return term
     replacements = dict(parameters)
     assert(all(ch in '0123456789^+- ' for ch in parameters['modulus']))
@@ -208,9 +209,13 @@ def make_curve_parameters(parameters):
                                          parameters.get(op + '_code', None),
                                          nargs,
                                          sz)
-    for k in ('upper_bound_of_exponent', 'allowable_bit_widths', 'freeze_extra_allowable_bit_widths'):
-        if k not in replacements.keys():
-            replacements[k] = 'None'
+    replacements['coef_div_modulus_raw'] = replacements.get('coef_div_modulus', '0')
+    for k, scope_string in (('upper_bound_of_exponent', ''),
+                            ('allowable_bit_widths', '%nat'),
+                            ('freeze_extra_allowable_bit_widths', '%nat'),
+                            ('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'):
         replacements[k] = nested_list_to_string(replacements[k])
     for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'):
@@ -232,7 +237,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in %(carry_chains)s.
 
   Definition a24 : option Z := %(a24)s.
-  Definition coef_div_modulus : nat := %(coef_div_modulus)s%%nat. (* add %(coef_div_modulus)s*modulus before subtracting *)
+  Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *)
 
   Definition goldilocks : bool := %(goldilocks)s.
 
@@ -245,6 +250,7 @@ Module Curve <: CurveParameters.
   Definition upper_bound_of_exponent : option (Z -> Z) := %(upper_bound_of_exponent)s.
   Definition allowable_bit_widths : option (list nat) := %(allowable_bit_widths)s.
   Definition freeze_extra_allowable_bit_widths : option (list nat) := %(freeze_extra_allowable_bit_widths)s.
+  Definition modinv_fuel : option nat := %(modinv_fuel)s.
   Ltac extra_prove_mul_eq := %(extra_prove_mul_eq)s.
   Ltac extra_prove_square_eq := %(extra_prove_square_eq)s.
 End Curve.
@@ -257,12 +263,9 @@ Require Import %s.CurveParameters.
 
 Module Import T := MakeSynthesisTactics Curve.
 
-Module P <: SynthesisPrePackage.
-  Definition Synthesis_package' : Synthesis_package'_Type.
-  Proof. make_synthesis_package (). Defined.
-
-  Definition Synthesis_package
-    := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'.
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
 End P.
 
 Module Export S := PackageSynthesis Curve P.
@@ -282,6 +285,8 @@ Proof.
   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.
@@ -296,6 +301,8 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
 """ % {'prefix':prefix}
     elif fearg in ('freeze',):
         return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems.
@@ -310,11 +317,29 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
 """ % {'prefix':prefix}
+    elif fearg in ('feopp',):
+        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 -> feBW
+  | forall a, phiBW (%(arg)s a) = F.%(arg)s (phiBW 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 ('ladderstep', 'xzladderstep'):
         return r"""Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
 Require Import %(prefix)s.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -334,6 +359,8 @@ Proof.
   synthesize_xzladderstep ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions xzladderstep.
 """ % {'prefix':prefix}
     else:
         print('ERROR: Unsupported operation: %s' % fearg)
@@ -343,10 +370,12 @@ Time Defined.
 def make_display_arg(fearg, prefix):
     file_name = fearg
     function_name = fearg
-    if fearg in ('femul', 'fesub', 'feadd', 'fesquare'):
+    if fearg in ('femul', 'fesub', 'feadd', 'fesquare', 'feopp'):
         function_name = fearg[2:]
     elif fearg in ('freeze', 'xzladderstep'):
         pass
+    elif fearg in ('fenz',):
+        function_name = 'nonzero'
     elif fearg in ('ladderstep', ):
         function_name = 'xzladderstep'
     else:
@@ -404,12 +433,16 @@ def main(*args):
             if open(fname, 'r').read() == outputs[k]:
                 continue
         new_files.append(fname)
-        with open(fname, 'w') as f:
-            f.write(outputs[k])
+        with io.open(fname, 'w', newline='\n') as f:
+            f.write(unicode(outputs[k]))
             if fname[-len('compiler.sh'):] == 'compiler.sh':
                 mode = os.fstat(f.fileno()).st_mode
                 mode |= 0o111
-                os.fchmod(f.fileno(), mode & 0o7777)
+                mode &= 0o7777
+                if 'fchmod' in os.__dict__.keys():
+                    os.fchmod(f.fileno(), mode)
+                else:
+                    os.chmod(f.name, mode)
     if len(new_files) > 0:
         print('git add ' + ' '.join('"%s"' % i for i in new_files))