aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* 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
|
* Generate sz as an int in python2Gravatar 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 )); " } ```
* Support python2 and python3 in json generationGravatar Jason Gross2017-10-14
|
* Add SmartFlatTypeMap_PairGravatar Jason Gross2017-10-14
|
* Fix a bug in CommonSubexpressionEliminationProperties.vGravatar Jason Gross2017-10-13
| | | | I'm very confused about how and when it was introduced...
* Add pow_ceil_mul_nat_divide_upperboundGravatar Jason Gross2017-10-13
|
* Support machines without controllable cpu speedGravatar Jason Gross2017-10-13
|
* Update smithers scriptGravatar Jason Gross2017-10-13
|
* add primes list andres scraped from curves at moderncrypto dot orgGravatar jadep2017-10-13
|
* add file input/output to json-generating scriptGravatar jadep2017-10-13
|
* add support for unsaturated limbs in json-generationGravatar jadep2017-10-13
|
* add examples to json-generation file for referenceGravatar jadep2017-10-13
|
* add script to generate json files given a primeGravatar jadep2017-10-13
|
* Add some SmartMap tuple lemmasGravatar Jason Gross2017-10-13
|
* Fix a spelling errorGravatar Jason Gross2017-10-13
|
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
| | | | This makes it easier to extend the bounds analysis framework.
* Add comment to Compilers/Z/Bounds/Interpretation.vGravatar Jason Gross2017-10-13
| | | | | Hopefully this will help with extending the framework. Also remove [t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
* Add some helper compilation lemmasGravatar Jason Gross2017-10-13
|
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
|
* Allow test and bench to fail on travisGravatar Jason Gross2017-10-11
| | | | | | | | We now only build selected-test and selected-bench with one version of Coq (picked 8.7+beta2, because hopefully it'll be faster than 8.6.1). Previously, some travis builds failed because some travis machines don't support adc, adcx, mulx, etc.
* Add targets for no-curves-proofs-non-specific, and selected-specific,Gravatar Jason Gross2017-10-11
| | | | Also hopefully fix travis
* Smithers doesn't support -o pipefailGravatar Jason Gross2017-10-11
|
* Factor out -w "-notation-overridden" in MakefileGravatar Jason Gross2017-10-10
|
* Add etc/ci/smithers.sh for smithers testingGravatar Jason Gross2017-10-10
|
* More Makefile factoringGravatar Jason Gross2017-10-10
|
* Update Makefile by deduplicating some file listsGravatar Jason Gross2017-10-10
|
* Hopefully fix travisGravatar Jason Gross2017-10-10
| | | | | | Travis was too slow to run all of the coq target, so we split off the no-curves-proofs and the curves-proofs targets, and, while we're at it, also add 8.7+beta1 tests.
* Add update_by_tac_if_not_existsGravatar Jason Gross2017-10-10
|
* TagList: make get error, and fix bugsGravatar Jason Gross2017-10-10
|
* Add TagListGravatar Jason Gross2017-10-10
| | | | | List of dynamically-typed key-value pairs, and some helper definitions and tactics.
* Add notationsGravatar Jason Gross2017-10-10
|
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
|
* Fix .dir-locals.el to work on WindowsGravatar Jason Gross2017-10-07
| | | | Previously, it was splitting on : and adding extra paths with, e.g., c:/
* Generalize phisGravatar Jason Gross2017-10-07
| | | | | | | | | | | | | | | | After | File Name | Before || Change ----------------------------------------------------------------------- 3m56.20s | Total | 4m14.86s || -0m18.66s ----------------------------------------------------------------------- 0m02.44s | Specific/X25519/C32/ReificationTypes | 0m19.48s || -0m17.03s 2m00.12s | Specific/X25519/C64/ladderstep | 1m55.72s || +0m04.40s 0m01.16s | Specific/X25519/C64/ReificationTypes | 0m05.17s || -0m04.00s 0m26.27s | Specific/X25519/C32/fesquare | 0m27.76s || -0m01.49s 0m52.60s | Specific/X25519/C32/femul | 0m52.46s || +0m00.14s 0m10.35s | Specific/X25519/C64/femul | 0m10.28s || +0m00.07s 0m08.30s | Specific/IntegrationTestSub | 0m08.69s || -0m00.38s 0m07.97s | Specific/IntegrationTestFreeze | 0m08.00s || -0m00.03s 0m06.99s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.31s
* Factor out the compute bit of the compute notation in curve paramsGravatar Jason Gross2017-10-07
| | | | This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time
* Factor out parameter-specific codeGravatar Jason Gross2017-10-07
| | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------ 6m08.27s | Total | 6m25.95s || -0m17.68s ------------------------------------------------------------------------------ N/A | Specific/ArithmeticSynthesisTest32 | 0m39.62s || -0m39.61s 0m38.34s | Specific/X25519/C32/ArithmeticSynthesisTest | N/A || +0m38.34s 0m20.46s | Specific/X25519/C32/ReificationTypes | N/A || +0m20.46s 2m31.97s | Specific/X25519/C64/ladderstep | 2m51.10s || -0m19.12s N/A | Specific/ArithmeticSynthesisTest | 0m09.54s || -0m09.53s 0m09.50s | Specific/X25519/C64/ArithmeticSynthesisTest | N/A || +0m09.50s 1m03.72s | Specific/X25519/C32/femul | 1m11.22s || -0m07.50s 0m10.44s | Specific/IntegrationTestFreeze | 0m17.29s || -0m06.84s 0m34.55s | Specific/X25519/C32/fesquare | 0m40.47s || -0m05.92s 0m05.50s | Specific/X25519/C64/ReificationTypes | N/A || +0m05.50s 0m12.47s | Specific/X25519/C64/femul | 0m13.98s || -0m01.50s 0m08.93s | Specific/X25519/C64/fesquare | 0m10.67s || -0m01.74s 0m11.14s | Specific/IntegrationTestSub | 0m12.06s || -0m00.92s 0m00.50s | Specific/X25519/C32/CurveParameters | N/A || +0m00.50s 0m00.38s | Specific/CurveParameters | N/A || +0m00.38s 0m00.37s | Specific/X25519/C64/CurveParameters | N/A || +0m00.37s
* [travis] trunk is now called masterGravatar Jason Gross2017-10-06
|
* Switch Coq {8.6 => 8.6.1} on travisGravatar Jason Gross2017-10-06
|
* Drop 8.5 travis buildGravatar Jason Gross2017-10-06
| | | | It's not useful, since we pass -compat 8.6
* Fix printenv sed script in Makefile for Windows supportGravatar Jason Gross2017-10-06
|
* Coq 8.5 can't handle symbol-free notationsGravatar Jason Gross2017-10-06
|
* Fix display logGravatar Jason Gross2017-10-06
|
* Clean up TestCase a bitGravatar Jason Gross2017-10-06
|
* Add another constantGravatar Jason Gross2017-10-06
|
* Fix the printlite targetGravatar Jason Gross2017-10-06
|
* Add pow_ceil_mul_nat_nonnegGravatar Jason Gross2017-10-05
|
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
|