aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Fold Karatsuba into json format and synthesisGravatar Jason Gross2017-10-18
| | | | | The json format now takes an additional, optional "goldilocks" boolean / boolean-string key determining if we're doing karatsuba.
* Build curve-specific files from jsonGravatar Jason Gross2017-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`.
* Generate C64 from python script and jsonGravatar Jason Gross2017-10-18
|
* Reorgainze synthesis framework files into a Framework folderGravatar Jason Gross2017-10-18
|
* Replace curve-specific definitions with tacticsGravatar Jason Gross2017-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This requires Coq >= 8.7 After | File Name | Before || Change --------------------------------------------------------------------------------------- 11m15.52s | Total | 11m14.53s || +0m00.99s --------------------------------------------------------------------------------------- 0m31.11s | Specific/X25519/C32/Synthesis | N/A || +0m31.10s N/A | Specific/X25519/C32/ArithmeticSynthesisTest | 0m30.80s || -0m30.80s 0m09.61s | Specific/X25519/C64/Synthesis | N/A || +0m09.60s N/A | Specific/X25519/C64/ArithmeticSynthesisTest | 0m08.56s || -0m08.56s 1m54.56s | Specific/X25519/C64/ladderstep | 1m56.56s || -0m02.00s 1m21.50s | Specific/IntegrationTestKaratsubaMul | 1m22.98s || -0m01.48s 1m15.96s | Specific/IntegrationTestLadderstep130 | 1m14.08s || +0m01.88s 0m51.80s | Specific/X25519/C32/femul | 0m53.79s || -0m01.99s 1m51.81s | Specific/NISTP256/AMD64/femul | 1m51.27s || +0m00.53s 0m28.68s | Specific/X25519/C32/fesquare | 0m28.30s || +0m00.37s 0m25.45s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.60s || -0m00.15s 0m18.81s | Specific/NISTP256/AMD64/fesub | 0m18.32s || +0m00.48s 0m16.01s | Specific/NISTP256/AMD64/feadd | 0m15.86s || +0m00.15s 0m15.15s | Specific/NISTP256/AMD64/feopp | 0m14.95s || +0m00.20s 0m12.42s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.15s || +0m00.26s 0m12.41s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.31s || +0m00.09s 0m11.10s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.31s || -0m00.21s 0m10.70s | Specific/X25519/C64/femul | 0m10.17s || +0m00.52s 0m09.94s | Specific/NISTP256/AMD64/fenz | 0m09.94s || +0m00.00s 0m09.37s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.36s || +0m00.00s 0m08.78s | Specific/IntegrationTestSub | 0m08.84s || -0m00.06s 0m07.98s | Specific/IntegrationTestFreeze | 0m08.12s || -0m00.13s 0m07.42s | Specific/X25519/C64/fesquare | 0m07.22s || +0m00.20s 0m00.99s | Specific/SynthesisFramework | N/A || +0m00.99s 0m00.88s | Specific/ReificationTypes | 0m00.91s || -0m00.03s 0m00.85s | Specific/ArithmeticSynthesisFramework | N/A || +0m00.85s N/A | Specific/X25519/C32/ReificationTypes | 0m00.82s || -0m00.82s N/A | Specific/X25519/C64/ReificationTypes | 0m00.77s || -0m00.77s 0m00.77s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.79s || -0m00.02s 0m00.72s | Specific/LadderstepSynthesisFramework | N/A || +0m00.72s 0m00.38s | Specific/IntegrationTestDisplayCommon | 0m00.40s || -0m00.02s 0m00.36s | Specific/IntegrationTestDisplayCommonTactics | 0m00.35s || +0m00.01s
* Factor out specific code underlying ReificationTypesGravatar Jason Gross2017-10-18
| | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------ 4m29.48s | Total | 4m30.12s || -0m00.63s ------------------------------------------------------------------------------ 0m27.97s | Specific/X25519/C32/fesquare | 0m26.68s || +0m01.28s 0m00.73s | Specific/X25519/C32/ReificationTypes | 0m02.43s || -0m01.70s 1m54.60s | Specific/X25519/C64/ladderstep | 1m55.11s || -0m00.51s 0m52.88s | Specific/X25519/C32/femul | 0m53.07s || -0m00.18s 0m29.56s | Specific/X25519/C32/ArithmeticSynthesisTest | 0m29.57s || -0m00.01s 0m10.01s | Specific/X25519/C64/femul | 0m10.08s || -0m00.07s 0m08.84s | Specific/IntegrationTestSub | 0m08.39s || +0m00.44s 0m08.42s | Specific/X25519/C64/ArithmeticSynthesisTest | 0m08.17s || +0m00.25s 0m07.64s | Specific/IntegrationTestFreeze | 0m08.01s || -0m00.37s 0m07.23s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.07s 0m00.86s | Specific/ReificationTypes | N/A || +0m00.86s 0m00.74s | Specific/X25519/C64/ReificationTypes | 0m01.30s || -0m00.56s
* Add 8.7-only CacheTermGravatar Jason Gross2017-10-18
|
* Add more notation constantsGravatar Jason Gross2017-10-18
|
* projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptionalGravatar Andres Erbsen2017-10-18
| | | | (Squashed and rebased by Jason Gross)
* Add a Require Import FunInd (Function isn't loaded by default anymore)Gravatar Pierre Letouzey2017-10-18
| | | | See PR #220 https://github.com/coq/coq/pull/220
* Add some more things to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
|
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
|
* Unfold more things in core unfolderGravatar Jason Gross2017-10-18
|
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
|
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
|
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
|
* Pattern more things in arithmetic/coreGravatar Jason Gross2017-10-17
|
* Allow instantiation of cps type arguments by unfoldingGravatar Jason Gross2017-10-17
|
* Make use of faster interp rewritingGravatar Jason Gross2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------- 10m34.32s | Total | 11m10.14s || -0m35.81s --------------------------------------------------------------------------------------- 0m04.75s | Compilers/Z/Bounds/Pipeline/Definition | 0m41.89s || -0m37.14s 1m24.64s | Specific/IntegrationTestKaratsubaMul | 1m20.20s || +0m04.43s 1m59.10s | Specific/X25519/C64/ladderstep | 2m00.27s || -0m01.17s 1m14.55s | Specific/IntegrationTestLadderstep130 | 1m13.12s || +0m01.42s 0m49.89s | Specific/X25519/C32/femul | 0m51.34s || -0m01.45s 0m26.72s | Specific/X25519/C32/fesquare | 0m27.79s || -0m01.07s 1m51.04s | Specific/NISTP256/AMD64/femul | 1m50.92s || +0m00.11s 0m25.48s | Specific/IntegrationTestMontgomeryP256_128 | 0m24.72s || +0m00.76s 0m18.54s | Specific/NISTP256/AMD64/fesub | 0m18.60s || -0m00.06s 0m15.57s | Specific/NISTP256/AMD64/feadd | 0m15.78s || -0m00.20s 0m14.93s | Specific/NISTP256/AMD64/feopp | 0m15.09s || -0m00.16s 0m12.13s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.34s || -0m00.20s 0m11.78s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.35s || -0m00.57s 0m11.06s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.24s || -0m00.17s 0m10.16s | Specific/X25519/C64/femul | 0m10.18s || -0m00.01s 0m09.78s | Specific/NISTP256/AMD64/fenz | 0m10.10s || -0m00.32s 0m09.06s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.26s || -0m00.19s 0m08.63s | Specific/IntegrationTestSub | 0m08.32s || +0m00.31s 0m07.84s | Specific/IntegrationTestFreeze | 0m07.87s || -0m00.03s 0m07.27s | Specific/X25519/C64/fesquare | 0m07.25s || +0m00.01s 0m00.80s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.81s || -0m00.01s 0m00.61s | Compilers/Z/Bounds/Pipeline | 0m00.70s || -0m00.08s
* Add InterpRewritingGravatar Jason Gross2017-10-17
| | | | | This is a faster version of [autorewrite with reflective_interp] on large chains of expressions.
* Add CacheTermGravatar Jason Gross2017-10-17
| | | | | The real use of this is with the 8.7-only transparent_abstract, but we can do some things even when we can only cache proofs.
* Turn on parenthetization in C outputGravatar Jason Gross2017-10-17
|
* Unify notation printing to allow changing it all at onceGravatar Jason Gross2017-10-17
|
* Allow unfolding of mapi_with_cps to specialize the function to the type ↵Gravatar Jason Gross2017-10-17
| | | | argument it gets passed
* Work around bug #5341Gravatar Jason Gross2017-10-17
|
* Fix some type annotations for better non-unfoldingGravatar Jason Gross2017-10-17
|
* Add MulSplitUnfolderGravatar Jason Gross2017-10-17
|
* Remove outdated json file, reorder remake_curves.shGravatar Jason Gross2017-10-17
|
* Add more json filesGravatar Jason Gross2017-10-16
|
* Add support for parenthesizing all CNotations expressionsGravatar Jason Gross2017-10-16
|
* Don't print ".0" for integer bases in the json filesGravatar Jason Gross2017-10-16
|
* bugfixes from messy rebase; remade json filesGravatar jadep2017-10-16
|
* Add more constantsGravatar Jason Gross2017-10-16
|
* Add some more power-of-two notationsGravatar Jason Gross2017-10-16
|
* Add more notationsGravatar Jason Gross2017-10-16
|
* Fix base generationGravatar Jason Gross2017-10-16
|
* Add more json filesGravatar Jason Gross2017-10-16
|
* Don't error if we can't open a fileGravatar Jason Gross2017-10-16
|
* Regenerate json filesGravatar Jason Gross2017-10-16
|
* Add faster arithmetic unfoldingGravatar Jason Gross2017-10-15
|
* Extend basesystem_partial_evaluation_RHSGravatar Jason Gross2017-10-15
| | | | | Now there's a version that handles things in Saturated.Core, and in Wrappers.
* Add strip_subst_localGravatar Jason Gross2017-10-15
|
* Add some constants from montgomeryGravatar Jason Gross2017-10-15
|
* Fix some issues with reification debug printingGravatar Jason Gross2017-10-15
|
* Add more constant notations from solinas primesGravatar Jason Gross2017-10-15
|
* Fix a typo in the previous commitGravatar Jason Gross2017-10-14
|
* Split up solve_op_mod_eqGravatar Jason Gross2017-10-14
| | | | This way, we can reuse it even when we can't fully compute the values
* Prettier json file generationGravatar Jason Gross2017-10-14
|
* Add generated json files from generate_parameters.pyGravatar Jason Gross2017-10-14
|
* Add curve-specific json filesGravatar Jason Gross2017-10-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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_chains" : "default", "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_chains" : "default", "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 )); " } ```
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 02:15:17 +0000