Build curve-specific files from json

The X25519 curves are now generated from `.json` files.  This code
only works in >= 8.7, because it makes use of the
recently-merged-from-fiat `transparent_abstract` tactic to allow
defining things in tactics without massive slowdown.  The structure is
as follows:

0. The module types and tactic definitions that set up the
infrastructure live in `src/Specific/Framework/`

1. There are `.json` files in `src/Specific/CurveParameters/` that
specify curve characteristics.   A simple example is `x2555_130.json`,
which is:
```json
{
    "modulus"          : "2^255-5",
    "base"             : "130",
    "a24"              : "121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *)",
    "sz"               : "3",
    "bitwidth"         : "128",
    "carry_chain1"     : "default",
    "carry_chain2"     : ["0", "1"],
    "coef_div_modulus" : "2",
    "operations"       : ["ladderstep"]
}
```
A more complicated example is `x25519_c64.json`:
```json
{
    "modulus"          : "2^255-19",
    "base"             : "51",
    "a24"              : "121665",
    "sz"               : "5",
    "bitwidth"         : "64",
    "carry_chain1"     : "default",
    "carry_chain2"     : ["0", "1"],
    "coef_div_modulus" : "2",
    "operations"       : ["femul", "fesquare", "freeze", "ladderstep"],
    "extra_files"      : ["X25519_C64/scalarmult.c"],
    "compiler"         : "gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes",
    "mul_header"       : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>;. *)",
    "mul_code"
    :
    "
  uint128_t t[5];
  limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;

  r0 = in[0];
  r1 = in[1];
  r2 = in[2];
  r3 = in[3];
  r4 = in[4];

  s0 = in2[0];
  s1 = in2[1];
  s2 = in2[2];
  s3 = in2[3];
  s4 = in2[4];

  t[0]  =  ((uint128_t) r0) * s0;
  t[1]  =  ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;
  t[2]  =  ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;
  t[3]  =  ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;
  t[4]  =  ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;

  r4 *= 19;
  r1 *= 19;
  r2 *= 19;
  r3 *= 19;

  t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;
  t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;
  t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;
  t[3] += ((uint128_t) r4) * s4;
",
    "square_header"    : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>;. *)",
    "square_code"
    :
    "
  uint128_t t[5];
  limb r0,r1,r2,r3,r4,c;
  limb d0,d1,d2,d4,d419;

  r0 = in[0];
  r1 = in[1];
  r2 = in[2];
  r3 = in[3];
  r4 = in[4];

  do {
    d0 = r0 * 2;
    d1 = r1 * 2;
    d2 = r2 * 2 * 19;
    d419 = r4 * 19;
    d4 = d419 * 2;

    t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3     ));
    t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));
    t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3     ));
    t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419   ));
    t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2     ));
"
}
```
3. The `src/Specific/CurveParameters/remake_curves.sh` script holds a
list of curves to be made, what directories they should end up living
in, and it invokes `src/Specific/Framework/make_curve.py` to transform
these files into outputs.  The Python script fills in a few defaults
(such as computing `s` and `c` from the modulus, if you don't pass
them explicitly), and does a lot of processing on the C code that is
pasted verbatim from donna to get it to be in the right format for
Coq.

This Python script creates the files:
- `CurveParameters.v` (the Coq-ified version of the json file, which
  instantiates an appropriate module type);
- `Synthesis.v`, which instantiates a `MakeSynthesisTactics` with the
  curve parameter modules, invokes a tactic from the applied module
functor to synthesize all of the relevant non-reflective bits
(basically, what used to live in @jadephilipoom 's
`ArithmeticSynthesisTest.v`), and then instantiates another module
functor `PackageSynthesis` which defines notations via tactics in
terms to access the names of the various fields defined by the
synthesis tactic;
- any other files you ask it for, such as `compiler.sh`, `femul.v`,
 `femulDisplay.v`.  All of the `*Display.v` files are simple, and all
the the operation synthesis files have a single `Definition` (with the
appropriate type), and solve the definition by invoking a single
tactic defined in `PackageSynthesis`, e.g., `synthesize_mul` or
`synthesize_ladderstep`.

21 files changed, 400 insertions, 490 deletions

diff --git a/.gitignore b/.gitignore
index e4788b21f..191e360a7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,6 +45,8 @@ src/Specific/X25519/C64/fesquare.c
 src/Specific/X25519/C64/fesquare.h
 src/Specific/X25519/C64/ladderstep.c
 src/Specific/X25519/C64/ladderstep.h
+src/Specific/X25519/C64/freeze.c
+src/Specific/X25519/C64/freeze.h
 src/Specific/X25519/C64/measure
 src/Specific/X25519/C64/test
 src/Specific/X25519/C32/femul.c
@@ -53,8 +55,12 @@ src/Specific/X25519/C32/fesquare.c
 src/Specific/X25519/C32/fesquare.h
 src/Specific/X25519/C32/ladderstep.c
 src/Specific/X25519/C32/ladderstep.h
+src/Specific/X25519/C32/freeze.c
+src/Specific/X25519/C32/freeze.h
 src/Specific/X25519/C32/measure
 src/Specific/X25519/C32/test
+src/Specific/X2555/C128/ladderstep.c
+src/Specific/X2555/C128/ladderstep.h
 third_party/openssl-curve25519/measure
 third_party/openssl-nistp256c64/measure
 third_party/openssl-nistz256-adx/measure
diff --git a/_CoqProject b/_CoqProject
index 9dc26ab87..e141313b6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -229,12 +229,8 @@ src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
 src/Specific/ArithmeticSynthesisTest130.v
-src/Specific/IntegrationTestFreeze.v
-src/Specific/IntegrationTestFreezeDisplay.v
 src/Specific/IntegrationTestKaratsubaMul.v
 src/Specific/IntegrationTestKaratsubaMulDisplay.v
-src/Specific/IntegrationTestLadderstep130.v
-src/Specific/IntegrationTestLadderstep130Display.v
 src/Specific/IntegrationTestMontgomeryP256_128.v
 src/Specific/IntegrationTestMontgomeryP256_128Display.v
 src/Specific/IntegrationTestMontgomeryP256_128_Add.v
@@ -245,8 +241,6 @@ src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
 src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v
 src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
 src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v
-src/Specific/IntegrationTestSub.v
-src/Specific/IntegrationTestSubDisplay.v
 src/Specific/Karatsuba.v
 src/Specific/MontgomeryP256_128.v
 src/Specific/Framework/ArithmeticSynthesisFramework.v
@@ -277,14 +271,22 @@ src/Specific/X25519/C32/femul.v
 src/Specific/X25519/C32/femulDisplay.v
 src/Specific/X25519/C32/fesquare.v
 src/Specific/X25519/C32/fesquareDisplay.v
+src/Specific/X25519/C32/freeze.v
+src/Specific/X25519/C32/freezeDisplay.v
 src/Specific/X25519/C64/CurveParameters.v
 src/Specific/X25519/C64/Synthesis.v
 src/Specific/X25519/C64/femul.v
 src/Specific/X25519/C64/femulDisplay.v
 src/Specific/X25519/C64/fesquare.v
 src/Specific/X25519/C64/fesquareDisplay.v
+src/Specific/X25519/C64/freeze.v
+src/Specific/X25519/C64/freezeDisplay.v
 src/Specific/X25519/C64/ladderstep.v
 src/Specific/X25519/C64/ladderstepDisplay.v
+src/Specific/X2555/C128/CurveParameters.v
+src/Specific/X2555/C128/Synthesis.v
+src/Specific/X2555/C128/ladderstep.v
+src/Specific/X2555/C128/ladderstepDisplay.v
 src/Util/AdditionChainExponentiation.v
 src/Util/AutoRewrite.v
 src/Util/Bool.v
diff --git a/src/Specific/CurveParameters/x25519_c64.json b/src/Specific/CurveParameters/x25519_c64.json
index 64bbb872e..45f27b535 100644
--- a/src/Specific/CurveParameters/x25519_c64.json
+++ b/src/Specific/CurveParameters/x25519_c64.json
@@ -4,7 +4,8 @@
     "a24"              : "121665",
     "sz"               : "5",
     "bitwidth"         : "64",
-    "carry_chains"     : "default",
+    "carry_chain1"     : "default",
+    "carry_chain2"     : ["0", "1"],
     "coef_div_modulus" : "2",
     "operations"       : ["femul", "fesquare", "freeze", "ladderstep"],
     "extra_files"      : ["X25519_C64/scalarmult.c"],
diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py
index 58ffdc31a..b530a72ee 100755
--- a/src/Specific/Framework/make_curve.py
+++ b/src/Specific/Framework/make_curve.py
@@ -1,11 +1,11 @@
 #!/usr/bin/env python
 from __future__ import with_statement
-import json, sys, os, math, re
+import json, sys, os, math, re, shutil
 
 def compute_bitwidth(base):
     return 2**int(math.ceil(math.log(base, 2)))
-def compute_sz(modulus, bitwidth):
-    return 1 + int(math.ceil(math.log(modulus, 2) / bitwidth))
+def compute_sz(modulus, base):
+    return 1 + int(math.ceil(math.log(modulus, 2) / base))
 def default_carry_chain(cc):
     assert(cc == 'carry_chain1')
     return 'Some (seq 0 (pred sz))'
@@ -67,6 +67,9 @@ def format_c_code(header, code, numargs, sz, indent='      ', closing_indent='
     lines = [repeat_until_unchanged((lambda line: re.sub(r'\(([A-Za-z0-9_]+)\)', r'\1', line)),
                                     line)
              for line in lines]
+    lines = [repeat_until_unchanged((lambda line: re.sub(r'\(([A-Za-z0-9_]+\[[0-9]+\])\)', r'\1', line)),
+                                    line)
+             for line in lines]
     out_match = re.match(r'^\s*u?int[0-9]+_t ([A-Za-z_][A-Za-z_0-9]*)\[([0-9]+)\]$', lines[0])
     if out_match is not None:
         out_var, out_count = out_match.groups()
@@ -81,8 +84,8 @@ def format_c_code(header, code, numargs, sz, indent='      ', closing_indent='
         limb_match = re.match(r'^\s*limb [a-zA-Z0-9, ]+$', line)
         in_match = re.match(r'^\s*([A-Za-z_][A-Za-z0-9_]*)\s*=\s*in([0-9]*)\[([0-9]+)\]$', line)
         fixed_line = do_fix(line)
-        normal_match = re.match(r'^(\s*)([A-Za-z_][A-Za-z0-9_]*)(\s*)=(\s*)([A-Za-z_0-9\(\) *+-]+)$', fixed_line)
-        upd_match = re.match(r'^(\s*)([A-Za-z_][A-Za-z0-9_]*)(\s*)([*+])=(\s*)([A-Za-z_0-9\(\) *+-]+)$', fixed_line)
+        normal_match = re.match(r'^(\s*)([A-Za-z_][A-Za-z0-9_]*)(\s*)=(\s*)([A-Za-z_0-9\(\)\s<>*+-]+)$', fixed_line)
+        upd_match = re.match(r'^(\s*)([A-Za-z_][A-Za-z0-9_]*)(\s*)([*+])=(\s*)([A-Za-z_0-9\(\)\s<>*+-]+)$', fixed_line)
         if line == '':
             ret_code.append(line)
         elif out_match or limb_match: pass
@@ -104,13 +107,25 @@ def format_c_code(header, code, numargs, sz, indent='      ', closing_indent='
         else:
             print('Unhandled line:')
             raw_input(line)
-    main_code = '\n'.join((indent + i.strip(' \n')).rstrip() for i in ' '.join(ret_code).strip().split('\n'))
+    ret_code = ' '.join(ret_code).strip().split('\n')
+    ret_code = [((indent + i.strip(' \n')) if i.strip()[:len('dlet ')] == 'dlet '
+                 else (indent + '  ' + i.rstrip(' \n'))).rstrip()
+                for i in ret_code]
+    main_code = '\n'.join(ret_code)
     arg_code = []
     for in_count in sorted(input_map.keys()):
         arg_code.append("%slet '(%s) := %s in"
                         % (indent,
                            ', '.join(v for k, v in sorted(input_map[in_count].items(), reverse=True)),
                            ARGS[in_count]))
+    if len(input_map.keys()) == 0:
+        for in_count in range(numargs):
+            in_str = str(in_count + 1)
+            if in_count == 0: in_str = ''
+            arg_code.append("%slet '(%s) := %s in"
+                            % (indent,
+                               ', '.join(do_fix('in%s[%d]' % (in_str, v)) for v in reversed(range(sz))),
+                               ARGS[in_count]))
     ret += '\n%s\n' % '\n'.join(arg_code)
     ret += main_code
     ret += '\n%s(%s)' % (indent, ', '.join(do_fix('%s[%d]' % (out_var, i)) for i in reversed(range(sz))))
@@ -121,10 +136,10 @@ def make_curve_parameters(parameters):
     replacements = dict(parameters)
     assert(all(ch in '0123456789^+- ' for ch in parameters['modulus']))
     modulus = eval(parameters['modulus'].replace('^', '**'))
-    base = int(parameters['base'])
+    base = float(parameters['base'])
     replacements['bitwidth'] = parameters.get('bitwidth', str(compute_bitwidth(base)))
     bitwidth = int(replacements['bitwidth'])
-    replacements['sz'] = parameters.get('sz', str(compute_sz(modulus, bitwidth)))
+    replacements['sz'] = parameters.get('sz', str(compute_sz(modulus, base)))
     sz = int(replacements['sz'])
     for cc in ('carry_chain1', 'carry_chain2'):
         if cc in replacements.keys() and isinstance(replacements[cc], list):
@@ -293,6 +308,13 @@ Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
 Check display %(function_name)s.
 """ % locals()
 
+def make_compiler(compiler):
+    return r"""#!/bin/sh
+set -eu
+
+%s "$@"
+""" % compiler
+
 
 def main(*args):
     if '--help' in args[1:] or '-h' in args[1:]: usage(0)
@@ -302,7 +324,7 @@ def main(*args):
     with open(args[1], 'r') as f:
         parameters = f.read()
     output_folder = os.path.realpath(args[2])
-    assert('|' not in parameters)
+    parameters_folder = os.path.dirname(os.path.realpath(args[1]))
     parameters = json.loads(parameters, strict=False)
     root = get_file_root(folder=output_folder)
     output_prefix = 'Crypto.' + os.path.normpath(os.path.relpath(output_folder, os.path.join(root, 'src'))).replace(os.sep, '.')
@@ -312,6 +334,10 @@ def main(*args):
     for arg in parameters['operations']:
         outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix)
         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()
+    if 'compiler' in parameters.keys():
+        outputs['compiler.sh'] = make_compiler(parameters['compiler'])
     file_list = tuple((k, os.path.join(output_folder, k)) for k in sorted(outputs.keys()))
     if not force:
         extant_files = [os.path.relpath(fname, os.getcwd())
@@ -322,12 +348,20 @@ def main(*args):
             sys.exit(1)
     if not os.path.isdir(output_folder):
         os.makedirs(output_folder)
+    new_files = []
     for k, fname in file_list:
         if os.path.isfile(fname):
             if open(fname, 'r').read() == outputs[k]:
                 continue
+        new_files.append(fname)
         with open(fname, 'w') as f:
             f.write(outputs[k])
+            if fname[-len('compiler.sh'):] == 'compiler.sh':
+                mode = os.fstat(f.fileno()).st_mode
+                mode |= 0o111
+                os.fchmod(f.fileno(), mode & 0o7777)
+    if len(new_files) > 0:
+        print('git add ' + ' '.join('"%s"' % i for i in new_files))
 
 if __name__ == '__main__':
     main(*sys.argv)
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
deleted file mode 100644
index aba794f4b..000000000
--- a/src/Specific/IntegrationTestLadderstep130.v
+++ /dev/null
@@ -1,131 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Classes.Morphisms.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest130.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Require Import Crypto.Util.Tactics.SetEvars.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Curves.Montgomery.XZ.
-Import ListNotations.
-
-Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
-
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
-
-  Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feW_bounded : feW -> Prop
-    := fun w => is_bounded_by None bounds (map wordToZ w).
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feW -> F m :=
-    fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
-
-  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
-  Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul.
-
-  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
-  Definition Mxzladderstep_sig
-    : { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz)
-      | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
-  Proof.
-    exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))).
-    intros a24 x1 Q Q' eval.
-    cbv [FMxzladderstep M.xzladderstep].
-    destruct Q, Q'; cbv [map map' fst snd Let_In eval].
-    repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
-    reflexivity.
-  Defined.
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition xzladderstep :
-    { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
-    | forall x1 Q Q',
-        let xz := xzladderstep x1 Q Q' in
-        let eval := B.Positional.Fdecode wt in
-        feW_bounded x1
-        -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
-        -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
-        -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
-            /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
-           /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
-  Proof.
-    apply_lift_sig.
-    intros a b c; cbv beta iota zeta.
-    lazymatch goal with
-    | [ |- { e | ?A -> ?B -> ?C -> @?E e } ]
-      => refine (proj2_sig_map (P:=fun e => A -> B -> C -> (_:Prop)) _ _)
-    end.
-    { intros ? FINAL.
-      repeat let H := fresh in intro H; specialize (FINAL H).
-      cbv [phi].
-      split; [ refine (proj1 FINAL); shelve | ].
-      do 4 match goal with
-           | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ]
-             => rewrite <- (Tuple.map_map (n:=N) f g
-                            : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x))))
-           end.
-      rewrite <- (proj2_sig Mxzladderstep_sig).
-      apply f_equal.
-      cbv [proj1_sig]; cbv [Mxzladderstep_sig].
-      context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _).
-      cbv [M.xzladderstep a24_sig].
-      repeat lazymatch goal with
-             | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
-               => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
-             end.
-      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig].
-      cbv_runtime.
-      refine (proj2 FINAL). }
-    subst feW feW_bounded; cbv beta.
-    (* jgross start here! *)
-    Set Ltac Profiling.
-    (*
-    Time Glue.refine_to_reflective_glue (128::256::nil)%nat%list.
-    Time ReflectiveTactics.refine_with_pipeline_correct default.
-    { Time ReflectiveTactics.do_reify. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
-    { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
-    { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). }
-    { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
-    { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
-    { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
-     *)
-    Time refine_reflectively128.
-    Show Ltac Profile.
-  Time Defined.
-
-Time End BoundedField25p5.
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
deleted file mode 100644
index 99999c9ae..000000000
--- a/src/Specific/IntegrationTestSub.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.X25519.C64.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition sub :
-  { sub : feBW -> feBW -> feBW
-  | forall a b, phiBW (sub a b) = F.sub (phiBW a) (phiBW b) }.
-Proof.
-  Set Ltac Profiling.
-  Time synthesize_sub ().
-  Show Ltac Profile.
-Time Defined.
diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log
deleted file mode 100644
index cbb1c6ff5..000000000
--- a/src/Specific/IntegrationTestSubDisplay.log
+++ /dev/null
@@ -1,32 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
- uint64_t x20 = ((0xffffffffffffe + x10) - x18);
- uint64_t x21 = ((0xffffffffffffe + x11) - x19);
- uint64_t x22 = ((0xffffffffffffe + x9) - x17);
- uint64_t x23 = ((0xffffffffffffe + x7) - x15);
- uint64_t x24 = ((0xfffffffffffda + x5) - x13);
- uint64_t x25 = (x24 >> 0x33);
- uint64_t x26 = (x24 & 0x7ffffffffffff);
- uint64_t x27 = (x25 + x23);
- uint64_t x28 = (x27 >> 0x33);
- uint64_t x29 = (x27 & 0x7ffffffffffff);
- uint64_t x30 = (x28 + x22);
- uint64_t x31 = (x30 >> 0x33);
- uint64_t x32 = (x30 & 0x7ffffffffffff);
- uint64_t x33 = (x31 + x21);
- uint64_t x34 = (x33 >> 0x33);
- uint64_t x35 = (x33 & 0x7ffffffffffff);
- uint64_t x36 = (x34 + x20);
- uint64_t x37 = (x36 >> 0x33);
- uint64_t x38 = (x36 & 0x7ffffffffffff);
- uint64_t x39 = (x26 + (0x13 * x37));
- uint64_t x40 = (x39 >> 0x33);
- uint64_t x41 = (x39 & 0x7ffffffffffff);
- uint64_t x42 = (x40 + x29);
- uint64_t x43 = (x42 >> 0x33);
- uint64_t x44 = (x42 & 0x7ffffffffffff);
- return (Return x38, Return x35, (x43 + x32), Return x44, Return x41))
-(x, x0)%core
-     : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
index 5040bf182..c8c7cb04f 100644
--- a/src/Specific/X25519/C32/CurveParameters.v
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -11,234 +11,234 @@ Module Curve <: CurveParameters.
   Definition bitwidth : Z := 32.
   Definition s : Z := 2^255.
   Definition c : list limb := [(1, 19)].
-  Definition carry_chain1 := Eval vm_compute in Some (seq 0 (pred sz)).
-  Definition carry_chain2 := Some [0;1]%nat.
+  Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)).
+  Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat.
 
-  Definition a24 := 121665%Z.
-  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+  Definition a24 : Z := 121665.
+  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
 
   Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
     := Some (fun a b =>
       (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
-      let '(in2_9, in2_8, in2_7, in2_6, in2_5, in2_4, in2_3, in2_2, in2_1, in2_0) := b in
-      dlet output_0 := in2_0 * in_0 in
-dlet output_1 :=       in2_0 * in_1 +
-                    in2_1 * in_0 in
-dlet output_2 :=  2 *  in2_1 * in_1 +
-                    in2_0 * in_2 +
-                    in2_2 * in_0 in
-dlet output_3 :=       in2_1 * in_2 +
-                    in2_2 * in_1 +
-                    in2_0 * in_3 +
-                    in2_3 * in_0 in
-dlet output_4 :=       in2_2 * in_2 +
-               2 * (in2_1 * in_3 +
-                    in2_3 * in_1) +
-                    in2_0 * in_4 +
-                    in2_4 * in_0 in
-dlet output_5 :=       in2_2 * in_3 +
-                    in2_3 * in_2 +
-                    in2_1 * in_4 +
-                    in2_4 * in_1 +
-                    in2_0 * in_5 +
-                    in2_5 * in_0 in
-dlet output_6 :=  2 * (in2_3 * in_3 +
-                    in2_1 * in_5 +
-                    in2_5 * in_1) +
-                    in2_2 * in_4 +
-                    in2_4 * in_2 +
-                    in2_0 * in_6 +
-                    in2_6 * in_0 in
-dlet output_7 :=       in2_3 * in_4 +
-                    in2_4 * in_3 +
-                    in2_2 * in_5 +
-                    in2_5 * in_2 +
-                    in2_1 * in_6 +
-                    in2_6 * in_1 +
-                    in2_0 * in_7 +
-                    in2_7 * in_0 in
-dlet output_8 :=       in2_4 * in_4 +
-               2 * (in2_3 * in_5 +
-                    in2_5 * in_3 +
-                    in2_1 * in_7 +
-                    in2_7 * in_1) +
-                    in2_2 * in_6 +
-                    in2_6 * in_2 +
-                    in2_0 * in_8 +
-                    in2_8 * in_0 in
-dlet output_9 :=       in2_4 * in_5 +
-                    in2_5 * in_4 +
-                    in2_3 * in_6 +
-                    in2_6 * in_3 +
-                    in2_2 * in_7 +
-                    in2_7 * in_2 +
-                    in2_1 * in_8 +
-                    in2_8 * in_1 +
-                    in2_0 * in_9 +
-                    in2_9 * in_0 in
-dlet output_10 := 2 * (in2_5 * in_5 +
-                    in2_3 * in_7 +
-                    in2_7 * in_3 +
-                    in2_1 * in_9 +
-                    in2_9 * in_1) +
-                    in2_4 * in_6 +
-                    in2_6 * in_4 +
-                    in2_2 * in_8 +
-                    in2_8 * in_2 in
-dlet output_11 :=      in2_5 * in_6 +
-                    in2_6 * in_5 +
-                    in2_4 * in_7 +
-                    in2_7 * in_4 +
-                    in2_3 * in_8 +
-                    in2_8 * in_3 +
-                    in2_2 * in_9 +
-                    in2_9 * in_2 in
-dlet output_12 :=      in2_6 * in_6 +
-               2 * (in2_5 * in_7 +
-                    in2_7 * in_5 +
-                    in2_3 * in_9 +
-                    in2_9 * in_3) +
-                    in2_4 * in_8 +
-                    in2_8 * in_4 in
-dlet output_13 :=      in2_6 * in_7 +
-                    in2_7 * in_6 +
-                    in2_5 * in_8 +
-                    in2_8 * in_5 +
-                    in2_4 * in_9 +
-                    in2_9 * in_4 in
-dlet output_14 := 2 * (in2_7 * in_7 +
-                    in2_5 * in_9 +
-                    in2_9 * in_5) +
-                    in2_6 * in_8 +
-                    in2_8 * in_6 in
-dlet output_15 :=      in2_7 * in_8 +
-                    in2_8 * in_7 +
-                    in2_6 * in_9 +
-                    in2_9 * in_6 in
-dlet output_16 :=      in2_8 * in_8 +
-               2 * (in2_7 * in_9 +
-                    in2_9 * in_7) in
-dlet output_17 :=      in2_8 * in_9 +
-                    in2_9 * in_8 in
-dlet output_18 := 2 *  in2_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+      let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in
+      let '(in29, in28, in27, in26, in25, in24, in23, in22, in21, in20) := b in
+      dlet output0 :=       in20 * in0 in
+      dlet output1 :=       in20 * in1 +
+                            in21 * in0 in
+      dlet output2 :=  2 *  in21 * in1 +
+                            in20 * in2 +
+                            in22 * in0 in
+      dlet output3 :=       in21 * in2 +
+                            in22 * in1 +
+                            in20 * in3 +
+                            in23 * in0 in
+      dlet output4 :=       in22 * in2 +
+                       2 * (in21 * in3 +
+                            in23 * in1) +
+                            in20 * in4 +
+                            in24 * in0 in
+      dlet output5 :=       in22 * in3 +
+                            in23 * in2 +
+                            in21 * in4 +
+                            in24 * in1 +
+                            in20 * in5 +
+                            in25 * in0 in
+      dlet output6 :=  2 * (in23 * in3 +
+                            in21 * in5 +
+                            in25 * in1) +
+                            in22 * in4 +
+                            in24 * in2 +
+                            in20 * in6 +
+                            in26 * in0 in
+      dlet output7 :=       in23 * in4 +
+                            in24 * in3 +
+                            in22 * in5 +
+                            in25 * in2 +
+                            in21 * in6 +
+                            in26 * in1 +
+                            in20 * in7 +
+                            in27 * in0 in
+      dlet output8 :=       in24 * in4 +
+                       2 * (in23 * in5 +
+                            in25 * in3 +
+                            in21 * in7 +
+                            in27 * in1) +
+                            in22 * in6 +
+                            in26 * in2 +
+                            in20 * in8 +
+                            in28 * in0 in
+      dlet output9 :=       in24 * in5 +
+                            in25 * in4 +
+                            in23 * in6 +
+                            in26 * in3 +
+                            in22 * in7 +
+                            in27 * in2 +
+                            in21 * in8 +
+                            in28 * in1 +
+                            in20 * in9 +
+                            in29 * in0 in
+      dlet output10 := 2 * (in25 * in5 +
+                            in23 * in7 +
+                            in27 * in3 +
+                            in21 * in9 +
+                            in29 * in1) +
+                            in24 * in6 +
+                            in26 * in4 +
+                            in22 * in8 +
+                            in28 * in2 in
+      dlet output11 :=      in25 * in6 +
+                            in26 * in5 +
+                            in24 * in7 +
+                            in27 * in4 +
+                            in23 * in8 +
+                            in28 * in3 +
+                            in22 * in9 +
+                            in29 * in2 in
+      dlet output12 :=      in26 * in6 +
+                       2 * (in25 * in7 +
+                            in27 * in5 +
+                            in23 * in9 +
+                            in29 * in3) +
+                            in24 * in8 +
+                            in28 * in4 in
+      dlet output13 :=      in26 * in7 +
+                            in27 * in6 +
+                            in25 * in8 +
+                            in28 * in5 +
+                            in24 * in9 +
+                            in29 * in4 in
+      dlet output14 := 2 * (in27 * in7 +
+                            in25 * in9 +
+                            in29 * in5) +
+                            in26 * in8 +
+                            in28 * in6 in
+      dlet output15 :=      in27 * in8 +
+                            in28 * in7 +
+                            in26 * in9 +
+                            in29 * in6 in
+      dlet output16 :=      in28 * in8 +
+                       2 * (in27 * in9 +
+                            in29 * in7) in
+      dlet output17 :=      in28 * in9 +
+                            in29 * in8 in
+      dlet output18 := 2 *  in29 * in9 in
+      dlet output8 := output8 + output18 << 4 in
+      dlet output8 := output8 + output18 << 1 in
+      dlet output8 := output8 + output18 in
+      dlet output7 := output7 + output17 << 4 in
+      dlet output7 := output7 + output17 << 1 in
+      dlet output7 := output7 + output17 in
+      dlet output6 := output6 + output16 << 4 in
+      dlet output6 := output6 + output16 << 1 in
+      dlet output6 := output6 + output16 in
+      dlet output5 := output5 + output15 << 4 in
+      dlet output5 := output5 + output15 << 1 in
+      dlet output5 := output5 + output15 in
+      dlet output4 := output4 + output14 << 4 in
+      dlet output4 := output4 + output14 << 1 in
+      dlet output4 := output4 + output14 in
+      dlet output3 := output3 + output13 << 4 in
+      dlet output3 := output3 + output13 << 1 in
+      dlet output3 := output3 + output13 in
+      dlet output2 := output2 + output12 << 4 in
+      dlet output2 := output2 + output12 << 1 in
+      dlet output2 := output2 + output12 in
+      dlet output1 := output1 + output11 << 4 in
+      dlet output1 := output1 + output11 << 1 in
+      dlet output1 := output1 + output11 in
+      dlet output0 := output0 + output10 << 4 in
+      dlet output0 := output0 + output10 << 1 in
+      dlet output0 := output0 + output10 in
+      (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0)
             ).
 
   Definition square_code : option (Z^sz -> Z^sz)
     := Some (fun a =>
       (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
-      let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
-dlet output_0 :=       in_0 * in_0 in
-dlet output_1 :=  2 *  in_0 * in_1 in
-dlet output_2 :=  2 * (in_1 * in_1 +
-                    in_0 * in_2) in
-dlet output_3 :=  2 * (in_1 * in_2 +
-                    in_0 * in_3) in
-dlet output_4 :=       in_2 * in_2 +
-               4 *  in_1 * in_3 +
-               2 *  in_0 * in_4 in
-dlet output_5 :=  2 * (in_2 * in_3 +
-                    in_1 * in_4 +
-                    in_0 * in_5) in
-dlet output_6 :=  2 * (in_3 * in_3 +
-                    in_2 * in_4 +
-                    in_0 * in_6 +
-               2 *  in_1 * in_5) in
-dlet output_7 :=  2 * (in_3 * in_4 +
-                    in_2 * in_5 +
-                    in_1 * in_6 +
-                    in_0 * in_7) in
-dlet output_8 :=       in_4 * in_4 +
-               2 * (in_2 * in_6 +
-                    in_0 * in_8 +
-               2 * (in_1 * in_7 +
-                    in_3 * in_5)) in
-dlet output_9 :=  2 * (in_4 * in_5 +
-                    in_3 * in_6 +
-                    in_2 * in_7 +
-                    in_1 * in_8 +
-                    in_0 * in_9) in
-dlet output_10 := 2 * (in_5 * in_5 +
-                    in_4 * in_6 +
-                    in_2 * in_8 +
-               2 * (in_3 * in_7 +
-                    in_1 * in_9)) in
-dlet output_11 := 2 * (in_5 * in_6 +
-                    in_4 * in_7 +
-                    in_3 * in_8 +
-                    in_2 * in_9) in
-dlet output_12 :=      in_6 * in_6 +
-               2 * (in_4 * in_8 +
-               2 * (in_5 * in_7 +
-                    in_3 * in_9)) in
-dlet output_13 := 2 * (in_6 * in_7 +
-                    in_5 * in_8 +
-                    in_4 * in_9) in
-dlet output_14 := 2 * (in_7 * in_7 +
-                    in_6 * in_8 +
-               2 *  in_5 * in_9) in
-dlet output_15 := 2 * (in_7 * in_8 +
-                    in_6 * in_9) in
-dlet output_16 :=      in_8 * in_8 +
-               4 *  in_7 * in_9 in
-dlet output_17 := 2 *  in_8 * in_9 in
-dlet output_18 := 2 *  in_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+      let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in
+      dlet output0 :=       in0 * in0 in
+      dlet output1 :=  2 *  in0 * in1 in
+      dlet output2 :=  2 * (in1 * in1 +
+                            in0 * in2) in
+      dlet output3 :=  2 * (in1 * in2 +
+                            in0 * in3) in
+      dlet output4 :=       in2 * in2 +
+                       4 *  in1 * in3 +
+                       2 *  in0 * in4 in
+      dlet output5 :=  2 * (in2 * in3 +
+                            in1 * in4 +
+                            in0 * in5) in
+      dlet output6 :=  2 * (in3 * in3 +
+                            in2 * in4 +
+                            in0 * in6 +
+                       2 *  in1 * in5) in
+      dlet output7 :=  2 * (in3 * in4 +
+                            in2 * in5 +
+                            in1 * in6 +
+                            in0 * in7) in
+      dlet output8 :=       in4 * in4 +
+                       2 * (in2 * in6 +
+                            in0 * in8 +
+                       2 * (in1 * in7 +
+                            in3 * in5)) in
+      dlet output9 :=  2 * (in4 * in5 +
+                            in3 * in6 +
+                            in2 * in7 +
+                            in1 * in8 +
+                            in0 * in9) in
+      dlet output10 := 2 * (in5 * in5 +
+                            in4 * in6 +
+                            in2 * in8 +
+                       2 * (in3 * in7 +
+                            in1 * in9)) in
+      dlet output11 := 2 * (in5 * in6 +
+                            in4 * in7 +
+                            in3 * in8 +
+                            in2 * in9) in
+      dlet output12 :=      in6 * in6 +
+                       2 * (in4 * in8 +
+                       2 * (in5 * in7 +
+                            in3 * in9)) in
+      dlet output13 := 2 * (in6 * in7 +
+                            in5 * in8 +
+                            in4 * in9) in
+      dlet output14 := 2 * (in7 * in7 +
+                            in6 * in8 +
+                       2 *  in5 * in9) in
+      dlet output15 := 2 * (in7 * in8 +
+                            in6 * in9) in
+      dlet output16 :=      in8 * in8 +
+                       4 *  in7 * in9 in
+      dlet output17 := 2 *  in8 * in9 in
+      dlet output18 := 2 *  in9 * in9 in
+      dlet output8 := output8 + output18 << 4 in
+      dlet output8 := output8 + output18 << 1 in
+      dlet output8 := output8 + output18 in
+      dlet output7 := output7 + output17 << 4 in
+      dlet output7 := output7 + output17 << 1 in
+      dlet output7 := output7 + output17 in
+      dlet output6 := output6 + output16 << 4 in
+      dlet output6 := output6 + output16 << 1 in
+      dlet output6 := output6 + output16 in
+      dlet output5 := output5 + output15 << 4 in
+      dlet output5 := output5 + output15 << 1 in
+      dlet output5 := output5 + output15 in
+      dlet output4 := output4 + output14 << 4 in
+      dlet output4 := output4 + output14 << 1 in
+      dlet output4 := output4 + output14 in
+      dlet output3 := output3 + output13 << 4 in
+      dlet output3 := output3 + output13 << 1 in
+      dlet output3 := output3 + output13 in
+      dlet output2 := output2 + output12 << 4 in
+      dlet output2 := output2 + output12 << 1 in
+      dlet output2 := output2 + output12 in
+      dlet output1 := output1 + output11 << 4 in
+      dlet output1 := output1 + output11 << 1 in
+      dlet output1 := output1 + output11 in
+      dlet output0 := output0 + output10 << 4 in
+      dlet output0 := output0 + output10 << 1 in
+      dlet output0 := output0 + output10 in
+      (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0)
             ).
 
   Definition upper_bound_of_exponent : option (Z -> Z) := None.
diff --git a/src/Specific/X25519/C32/compiler.sh b/src/Specific/X25519/C32/compiler.sh
index e64df574a..401968c8b 100755
--- a/src/Specific/X25519/C32/compiler.sh
+++ b/src/Specific/X25519/C32/compiler.sh
@@ -1,4 +1,4 @@
 #!/bin/sh
 set -eu
 
-gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes $@
+gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes "$@"
diff --git a/src/Specific/X25519/C32/freeze.v b/src/Specific/X25519/C32/freeze.v
new file mode 100644
index 000000000..9af1e8e0f
--- /dev/null
+++ b/src/Specific/X25519/C32/freeze.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C32.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition freeze :
+  { freeze : feBW -> feBW
+  | forall a, phiBW (freeze a) = phiBW a }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_freeze ().
+  Show Ltac Profile.
+Time Defined.
diff --git a/src/Specific/X25519/C32/freezeDisplay.log b/src/Specific/X25519/C32/freezeDisplay.log
new file mode 100644
index 000000000..b2582c34a
--- /dev/null
+++ b/src/Specific/X25519/C32/freezeDisplay.log
@@ -0,0 +1,38 @@
+λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint32_t x20, uint8_t x21 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, Const 67108845);
+ uint32_t x23, uint8_t x24 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x21, Return x4, 0x1ffffff);
+ uint32_t x26, uint8_t x27 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x24, Return x6, 0x3ffffff);
+ uint32_t x29, uint8_t x30 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x27, Return x8, 0x1ffffff);
+ uint32_t x32, uint8_t x33 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x30, Return x10, 0x3ffffff);
+ uint32_t x35, uint8_t x36 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x33, Return x12, 0x1ffffff);
+ uint32_t x38, uint8_t x39 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x36, Return x14, 0x3ffffff);
+ uint32_t x41, uint8_t x42 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x39, Return x16, 0x1ffffff);
+ uint32_t x44, uint8_t x45 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x42, Return x18, 0x3ffffff);
+ uint32_t x47, uint8_t x48 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x45, Return x17, 0x1ffffff);
+ uint32_t x49 = (uint32_t)cmovznz(x48, 0x0, 0xffffffff);
+ uint32_t x50 = x49 & Const 67108845;
+ uint32_t x52, uint8_t x53 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x20, Return x50);
+ uint32_t x54 = x49 & 0x1ffffff;
+ uint32_t x56, uint8_t x57 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x53, Return x23, Return x54);
+ uint32_t x58 = x49 & 0x3ffffff;
+ uint32_t x60, uint8_t x61 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x26, Return x58);
+ uint32_t x62 = x49 & 0x1ffffff;
+ uint32_t x64, uint8_t x65 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x61, Return x29, Return x62);
+ uint32_t x66 = x49 & 0x3ffffff;
+ uint32_t x68, uint8_t x69 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x65, Return x32, Return x66);
+ uint32_t x70 = x49 & 0x1ffffff;
+ uint32_t x72, uint8_t x73 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x35, Return x70);
+ uint32_t x74 = x49 & 0x3ffffff;
+ uint32_t x76, uint8_t x77 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x73, Return x38, Return x74);
+ uint32_t x78 = x49 & 0x1ffffff;
+ uint32_t x80, uint8_t x81 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x77, Return x41, Return x78);
+ uint32_t x82 = x49 & 0x3ffffff;
+ uint32_t x84, uint8_t x85 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x44, Return x82);
+ uint32_t x86 = x49 & 0x1ffffff;
+ uint32_t x88, uint8_t _ = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x85, Return x47, Return x86);
+ (Return x88, Return x84, Return x80, Return x76, Return x72, Return x68, Return x64, Return x60, Return x56, Return x52))
+x
+     : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/IntegrationTestFreezeDisplay.v b/src/Specific/X25519/C32/freezeDisplay.v
index ab17a7e93..dc0defdc8 100644
--- a/src/Specific/IntegrationTestFreezeDisplay.v
+++ b/src/Specific/X25519/C32/freezeDisplay.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.IntegrationTestFreeze.
+Require Import Crypto.Specific.X25519.C32.freeze.
 Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
 
 Check display freeze.
diff --git a/src/Specific/X25519/C64/compiler.sh b/src/Specific/X25519/C64/compiler.sh
index e64df574a..401968c8b 100755
--- a/src/Specific/X25519/C64/compiler.sh
+++ b/src/Specific/X25519/C64/compiler.sh
@@ -1,4 +1,4 @@
 #!/bin/sh
 set -eu
 
-gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes $@
+gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes "$@"
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/X25519/C64/freeze.v
index ef826dba5..ef826dba5 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/X25519/C64/freeze.v
diff --git a/src/Specific/IntegrationTestFreezeDisplay.log b/src/Specific/X25519/C64/freezeDisplay.log
index e25c7e397..e25c7e397 100644
--- a/src/Specific/IntegrationTestFreezeDisplay.log
+++ b/src/Specific/X25519/C64/freezeDisplay.log
diff --git a/src/Specific/IntegrationTestSubDisplay.v b/src/Specific/X25519/C64/freezeDisplay.v
index 37a060f26..d3f1a5499 100644
--- a/src/Specific/IntegrationTestSubDisplay.v
+++ b/src/Specific/X25519/C64/freezeDisplay.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.IntegrationTestSub.
+Require Import Crypto.Specific.X25519.C64.freeze.
 Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
 
-Check display sub.
+Check display freeze.
diff --git a/src/Specific/X25519/C64/parameters.json b/src/Specific/X25519/C64/parameters.json
deleted file mode 100644
index b03a8cee5..000000000
--- a/src/Specific/X25519/C64/parameters.json
+++ /dev/null
@@ -1,75 +0,0 @@
-{
-    "modulus"          : "2^255-19",
-    "base"             : "51",
-    "operations"       : ["femul", "fesquare", "ladderstep", "freeze"],
-    "sz"               : "5",
-    "bitwidth"         : "64",
-    "s"                : "2^255",
-    "c"                : [["1", "19"]],
-    "carry_chain1"     : "default",
-    "carry_chain2"     : ["0", "1"],
-    "a24"              : "121665",
-    "coef_div_modulus" : "2",
-    "mul_header"       : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
-    "mul_code"
-    :
-    "
-  uint128_t t[5];
-  limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;
-
-  r0 = in[0];
-  r1 = in[1];
-  r2 = in[2];
-  r3 = in[3];
-  r4 = in[4];
-
-  s0 = in2[0];
-  s1 = in2[1];
-  s2 = in2[2];
-  s3 = in2[3];
-  s4 = in2[4];
-
-  t[0]  =  ((uint128_t) r0) * s0;
-  t[1]  =  ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;
-  t[2]  =  ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;
-  t[3]  =  ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;
-  t[4]  =  ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;
-
-  r4 *= 19;
-  r1 *= 19;
-  r2 *= 19;
-  r3 *= 19;
-
-  t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;
-  t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;
-  t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;
-  t[3] += ((uint128_t) r4) * s4;
-",
-    "square_header"    : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
-    "square_code"
-    :
-    "
-  uint128_t t[5];
-  limb r0,r1,r2,r3,r4,c;
-  limb d0,d1,d2,d4,d419;
-
-  r0 = in[0];
-  r1 = in[1];
-  r2 = in[2];
-  r3 = in[3];
-  r4 = in[4];
-
-  do {
-    d0 = r0 * 2;
-    d1 = r1 * 2;
-    d2 = r2 * 2 * 19;
-    d419 = r4 * 19;
-    d4 = d419 * 2;
-
-    t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3     ));
-    t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));
-    t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3     ));
-    t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419   ));
-    t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2     ));
-"
-}
diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v
new file mode 100644
index 000000000..a0a0dc027
--- /dev/null
+++ b/src/Specific/X2555/C128/CurveParameters.v
@@ -0,0 +1,31 @@
+Require Import Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Util.LetIn.
+
+(***
+Modulus : 2^255-5
+Base: 130
+***)
+
+Module Curve <: CurveParameters.
+  Definition sz : nat := 3%nat.
+  Definition bitwidth : Z := 128.
+  Definition s : Z := 2^255.
+  Definition c : list limb := [(1, 5)].
+  Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)).
+  Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat.
+
+  Definition a24 : Z := 121665 (* XXX TODO(andreser) FIXME?  Is this right for this curve? *).
+  Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
+
+  Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
+    := None.
+
+  Definition square_code : option (Z^sz -> Z^sz)
+    := None.
+
+  Definition upper_bound_of_exponent : option (Z -> Z) := None.
+  Definition allowable_bit_widths : option (list nat) := None.
+  Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
+  Ltac extra_prove_mul_eq := idtac.
+  Ltac extra_prove_square_eq := idtac.
+End Curve.
diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v
new file mode 100644
index 000000000..f88491af2
--- /dev/null
+++ b/src/Specific/X2555/C128/Synthesis.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Specific.Framework.SynthesisFramework.
+Require Import Crypto.Specific.X2555.C128.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'.
+End P.
+
+Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/X2555/C128/ladderstep.v b/src/Specific/X2555/C128/ladderstep.v
new file mode 100644
index 000000000..b1d83df4a
--- /dev/null
+++ b/src/Specific/X2555/C128/ladderstep.v
@@ -0,0 +1,22 @@
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.X2555.C128.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition xzladderstep :
+  { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
+  | forall x1 Q Q',
+      let xz := xzladderstep x1 Q Q' in
+      let eval := B.Positional.Fdecode wt in
+      feW_bounded x1
+      -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
+      -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
+      -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
+          /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
+         /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (m:=m) (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }.
+Proof.
+  Set Ltac Profiling.
+  synthesize_xzladderstep ().
+  Show Ltac Profile.
+Time Defined.
diff --git a/src/Specific/IntegrationTestLadderstep130Display.v b/src/Specific/X2555/C128/ladderstepDisplay.v
index fa498e475..a8ea06084 100644
--- a/src/Specific/IntegrationTestLadderstep130Display.v
+++ b/src/Specific/X2555/C128/ladderstepDisplay.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Specific.IntegrationTestLadderstep130.
+Require Import Crypto.Specific.X2555.C128.ladderstep.
 Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
 
 Check display xzladderstep.