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`. --- .gitignore | 6 + _CoqProject | 14 +- src/Specific/CurveParameters/x25519_c64.json | 3 +- src/Specific/Framework/make_curve.py | 52 ++- src/Specific/IntegrationTestFreeze.v | 12 - src/Specific/IntegrationTestFreezeDisplay.log | 23 -- src/Specific/IntegrationTestFreezeDisplay.v | 4 - src/Specific/IntegrationTestLadderstep130.v | 131 ------- src/Specific/IntegrationTestLadderstep130Display.v | 4 - src/Specific/IntegrationTestSub.v | 12 - src/Specific/IntegrationTestSubDisplay.log | 32 -- src/Specific/IntegrationTestSubDisplay.v | 4 - src/Specific/X25519/C32/CurveParameters.v | 436 ++++++++++----------- src/Specific/X25519/C32/compiler.sh | 2 +- src/Specific/X25519/C32/freeze.v | 12 + src/Specific/X25519/C32/freezeDisplay.log | 38 ++ src/Specific/X25519/C32/freezeDisplay.v | 4 + 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 ---- src/Specific/X2555/C128/CurveParameters.v | 31 ++ src/Specific/X2555/C128/Synthesis.v | 14 + src/Specific/X2555/C128/ladderstep.v | 22 ++ src/Specific/X2555/C128/ladderstepDisplay.v | 4 + 26 files changed, 443 insertions(+), 533 deletions(-) delete mode 100644 src/Specific/IntegrationTestFreeze.v delete mode 100644 src/Specific/IntegrationTestFreezeDisplay.log delete mode 100644 src/Specific/IntegrationTestFreezeDisplay.v delete mode 100644 src/Specific/IntegrationTestLadderstep130.v delete mode 100644 src/Specific/IntegrationTestLadderstep130Display.v delete mode 100644 src/Specific/IntegrationTestSub.v delete mode 100644 src/Specific/IntegrationTestSubDisplay.log delete mode 100644 src/Specific/IntegrationTestSubDisplay.v create mode 100644 src/Specific/X25519/C32/freeze.v create mode 100644 src/Specific/X25519/C32/freezeDisplay.log create mode 100644 src/Specific/X25519/C32/freezeDisplay.v 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 create mode 100644 src/Specific/X2555/C128/CurveParameters.v create mode 100644 src/Specific/X2555/C128/Synthesis.v create mode 100644 src/Specific/X2555/C128/ladderstep.v create mode 100644 src/Specific/X2555/C128/ladderstepDisplay.v 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/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v deleted file mode 100644 index ef826dba5..000000000 --- a/src/Specific/IntegrationTestFreeze.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 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/IntegrationTestFreezeDisplay.log b/src/Specific/IntegrationTestFreezeDisplay.log deleted file mode 100644 index e25c7e397..000000000 --- a/src/Specific/IntegrationTestFreezeDisplay.log +++ /dev/null @@ -1,23 +0,0 @@ -λ 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/IntegrationTestFreezeDisplay.v b/src/Specific/IntegrationTestFreezeDisplay.v deleted file mode 100644 index ab17a7e93..000000000 --- a/src/Specific/IntegrationTestFreezeDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.IntegrationTestFreeze. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display freeze. 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/IntegrationTestLadderstep130Display.v b/src/Specific/IntegrationTestLadderstep130Display.v deleted file mode 100644 index fa498e475..000000000 --- a/src/Specific/IntegrationTestLadderstep130Display.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.IntegrationTestLadderstep130. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display xzladderstep. 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/IntegrationTestSubDisplay.v b/src/Specific/IntegrationTestSubDisplay.v deleted file mode 100644 index 37a060f26..000000000 --- a/src/Specific/IntegrationTestSubDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.IntegrationTestSub. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display sub. 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 . *) - 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 . *) - 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/X25519/C32/freezeDisplay.v b/src/Specific/X25519/C32/freezeDisplay.v new file mode 100644 index 000000000..dc0defdc8 --- /dev/null +++ b/src/Specific/X25519/C32/freezeDisplay.v @@ -0,0 +1,4 @@ +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/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 )); -" -} 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/X2555/C128/ladderstepDisplay.v b/src/Specific/X2555/C128/ladderstepDisplay.v new file mode 100644 index 000000000..a8ea06084 --- /dev/null +++ b/src/Specific/X2555/C128/ladderstepDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.X2555.C128.ladderstep. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. + +Check display xzladderstep. -- cgit v1.2.3