From 28359fcb5be530da65d5049846927a84a880b919 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 6 Oct 2017 01:50:59 -0400 Subject: 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 . *)", "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 . *)", "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`. --- src/Specific/X25519/C64/compiler.sh | 2 +- src/Specific/X25519/C64/freeze.v | 12 +++++ src/Specific/X25519/C64/freezeDisplay.log | 23 ++++++++++ src/Specific/X25519/C64/freezeDisplay.v | 4 ++ src/Specific/X25519/C64/parameters.json | 75 ------------------------------- 5 files changed, 40 insertions(+), 76 deletions(-) create mode 100644 src/Specific/X25519/C64/freeze.v create mode 100644 src/Specific/X25519/C64/freezeDisplay.log create mode 100644 src/Specific/X25519/C64/freezeDisplay.v delete mode 100644 src/Specific/X25519/C64/parameters.json (limited to 'src/Specific/X25519/C64') 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 . *)", - "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 . *)", - "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 )); -" -} -- cgit v1.2.3