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`.

5 files changed, 40 insertions, 76 deletions

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/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v
new file mode 100644
index 000000000..ef826dba5
--- /dev/null
+++ b/src/Specific/X25519/C64/freeze.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C64.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/C64/freezeDisplay.log b/src/Specific/X25519/C64/freezeDisplay.log
new file mode 100644
index 000000000..e25c7e397
--- /dev/null
+++ b/src/Specific/X25519/C64/freezeDisplay.log
@@ -0,0 +1,23 @@
+λ x : word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x7, x8, x6, x4, x2)%core,
+ uint64_t x10, uint8_t x11 = subborrow_u51(0x0, x2, 0x7ffffffffffed);
+ uint64_t x13, uint8_t x14 = subborrow_u51(x11, x4, 0x7ffffffffffff);
+ uint64_t x16, uint8_t x17 = subborrow_u51(x14, x6, 0x7ffffffffffff);
+ uint64_t x19, uint8_t x20 = subborrow_u51(x17, x8, 0x7ffffffffffff);
+ uint64_t x22, uint8_t x23 = subborrow_u51(x20, x7, 0x7ffffffffffff);
+ uint64_t x24 = (uint64_t)cmovznz(x23, 0x0, 0xffffffffffffffffL);
+ uint64_t x25 = (x24 & 0x7ffffffffffed);
+ uint64_t x27, uint8_t x28 = addcarryx_u51(0x0, x10, x25);
+ uint64_t x29 = (x24 & 0x7ffffffffffff);
+ uint64_t x31, uint8_t x32 = addcarryx_u51(x28, x13, x29);
+ uint64_t x33 = (x24 & 0x7ffffffffffff);
+ uint64_t x35, uint8_t x36 = addcarryx_u51(x32, x16, x33);
+ uint64_t x37 = (x24 & 0x7ffffffffffff);
+ uint64_t x39, uint8_t x40 = addcarryx_u51(x36, x19, x37);
+ uint64_t x41 = (x24 & 0x7ffffffffffff);
+ uint64_t x43, uint8_t _ = addcarryx_u51(x40, x22, x41);
+ (Return x43, Return x39, Return x35, Return x31, Return x27))
+x
+     : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/X25519/C64/freezeDisplay.v b/src/Specific/X25519/C64/freezeDisplay.v
new file mode 100644
index 000000000..d3f1a5499
--- /dev/null
+++ b/src/Specific/X25519/C64/freezeDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C64.freeze.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+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     ));
-"
-}