aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
* 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
|
* 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 )); " } ```
* 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
* Fix display logGravatar Jason Gross2017-10-06
|
* Factor out some bits of ladderstep preglueGravatar Jason Gross2017-10-05
| | | | | This requires some changes to nonzero, which now needs to unfold proj1_sig itself.
* Add missing tactic in comment in ladderstepGravatar Jason Gross2017-09-27
|
* Add src/Specific/X25519/C32/compiler.sh, update ↵Gravatar Jason Gross2017-09-27
| | | | src/Specific/X25519/C64/scalarmult.c
* Add curve25519-donna-c64 to etc/third_partyGravatar Jason Gross2017-09-27
|
* Add missing fileGravatar Jason Gross2017-09-21
|
* Add femul,fesqure for C32Gravatar Jason Gross2017-09-21
| | | | | 32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't add it yet
* Add extract_ExprGravatar Jason Gross2017-09-21
|
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
|
* make benchGravatar Jason Gross2017-09-12
|
* Fix more commented out alternativesGravatar Jason Gross2017-09-05
|
* Fix commented out alternate version in ladderstepGravatar Jason Gross2017-09-05
|
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it a bit more uniform, and hopefully more automatable and packageable. Unfortunately, there's still no spec for this part of the pipeline, so the tactics simply aggregate common patterns. Alas, this also makes things a bit slower; I suspect that [Defined] is the place where things are slower. After | File Name | Before || Change --------------------------------------------------------------------------------------- 13m51.14s | Total | 12m59.29s || +0m51.84s --------------------------------------------------------------------------------------- 1m54.18s | Specific/IntegrationTestKaratsubaMul | 1m43.12s || +0m11.06s 1m38.97s | Specific/IntegrationTestLadderstep130 | 1m30.26s || +0m08.70s 2m19.75s | Specific/NISTP256/AMD64/femul | 2m14.08s || +0m05.66s 0m39.90s | Specific/IntegrationTestMontgomeryP256_128 | 0m34.21s || +0m05.68s 0m21.95s | Specific/NISTP256/AMD64/fesub | 0m19.23s || +0m02.71s 0m21.37s | Specific/NISTP256/AMD64/feadd | 0m18.82s || +0m02.55s 0m21.02s | Specific/X25519/C64/femul | 0m18.32s || +0m02.69s 0m20.53s | Specific/IntegrationTestFreeze | 0m23.26s || -0m02.73s 0m18.28s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m15.32s || +0m02.96s 0m18.20s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m15.52s || +0m02.67s 0m16.35s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m13.52s || +0m02.83s 0m13.92s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s || +0m02.08s 0m18.23s | Specific/NISTP256/AMD64/MontgomeryP256 | 0m16.62s || +0m01.60s 0m15.54s | Specific/IntegrationTestSub | 0m14.53s || +0m01.00s 0m14.78s | Specific/X25519/C64/fesquare | 0m13.13s || +0m01.64s 0m13.71s | Specific/NISTP256/AMD64/fenz | 0m12.69s || +0m01.02s 3m14.34s | Specific/X25519/C64/ladderstep | 3m14.32s || +0m00.02s 0m16.54s | Specific/NISTP256/AMD64/feopp | 0m16.48s || +0m00.05s 0m12.21s | Specific/MontgomeryP256_128 | 0m12.70s || -0m00.48s 0m00.73s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.72s || +0m00.01s 0m00.64s | Specific/IntegrationTestDisplayCommon | 0m00.60s || +0m00.04s
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
|
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
|
* make benchGravatar Andres Erbsen2017-07-06
|
* make benchGravatar Jason Gross2017-07-06
| | | | | | | | | | | | | | | ``` make -j test make -j -k bench touch capture.sh make -k bench sudo etc/turboboost.sh off sudo etc/hyperthreading.sh off touch capture.sh make -k bench sudo etc/turboboost.sh on sudo etc/hyperthreading.sh on ```
* benchmark NISTZ256 with and without adxGravatar Andres Erbsen2017-07-05
|
* make benchGravatar Andres Erbsen2017-07-05
|
* make benchGravatar Andres Erbsen2017-07-04
|
* use att style assembly with icc, test itGravatar Andres Erbsen2017-07-04
|
* test p256 mixed additionGravatar Andres Erbsen2017-07-04
| | | | | passed after fixing some stupid typos in glue code -- no conceptual issues.
* work around GCC issues 81294 and 81300Gravatar Andres Erbsen2017-07-03
|
* fix mulx argument order using sed, test feadd, femul (fails due to #234)Gravatar Andres Erbsen2017-07-03
|
* Fix display targetGravatar Jason Gross2017-07-03
|
* X25519 test (passed on first try)Gravatar Andres Erbsen2017-07-02
|
* automate P256 integrationGravatar Andres Erbsen2017-07-02
|
* Merge branch 'use-cmovznz' of https://github.com/JasonGross/fiat-cryptoGravatar Andres Erbsen2017-07-02
|\
* | make displayGravatar Andres Erbsen2017-07-01
| |
* | changes to log files after running make cGravatar jadep2017-07-01
| |
* | add missing importGravatar jadep2017-06-30
| |
* | Fix misnamed references in Specific/ (broke after saturated arithetic reorg)Gravatar jadep2017-06-30
| |
* | Reorganization of saturated arithmeticGravatar jadep2017-06-29
| |
| * make displayGravatar Jason Gross2017-06-29
| |
* | make displayGravatar Jason Gross2017-06-29
| |
* | Fix unfolding to not unfold sub_with_get_borrow in P256Gravatar Jason Gross2017-06-29
|/
* Use -std=gnu11 for older versions of gccGravatar Jason Gross2017-06-28
|
* match C code in Jacobian additionGravatar Andres Erbsen2017-06-27
|
* p256 compilation and benchmarks with manual kludgesGravatar Andres Erbsen2017-06-27
|
* More proof fixingGravatar Jason Gross2017-06-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 19:24:50 +0000