aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* Support p256 / montgomery in json formatGravatar Jason Gross2017-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extra time comes from adding AMD128 to NISTP256, mostly. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m25.13s | Total | 13m30.82s || -0m05.69s --------------------------------------------------------------------------------------------- N/A | Specific/IntegrationTestMontgomeryP256_128 | 0m25.42s || -0m25.42s 0m22.75s | Specific/NISTP256/AMD128/femul | N/A || +0m22.75s 1m31.64s | Specific/NISTP256/AMD64/femul | 1m52.42s || -0m20.78s 0m14.46s | Specific/NISTP256/AMD128/fesub | N/A || +0m14.46s 0m14.25s | Specific/NISTP256/AMD128/feadd | N/A || +0m14.25s 0m14.12s | Specific/NISTP256/AMD128/fenz | N/A || +0m14.11s N/A | Specific/NISTP256/AMD64/MontgomeryP256 | 0m13.00s || -0m13.00s N/A | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.40s || -0m12.40s N/A | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.99s || -0m11.99s 0m11.74s | Specific/NISTP256/AMD128/feopp | N/A || +0m11.74s N/A | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.22s || -0m11.22s N/A | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.27s || -0m09.26s N/A | Specific/MontgomeryP256_128 | 0m09.26s || -0m09.25s 0m08.42s | Specific/NISTP256/AMD64/Synthesis | N/A || +0m08.41s 0m14.67s | Specific/NISTP256/AMD64/fenz | 0m09.98s || +0m04.68s 0m04.12s | Specific/Framework/ArithmeticSynthesis/Montgomery | N/A || +0m04.12s 0m03.58s | Specific/NISTP256/AMD128/Synthesis | N/A || +0m03.58s 1m10.78s | Specific/X2555/C128/ladderstep | 1m08.36s || +0m02.42s 1m02.10s | Specific/X25519/C32/femul | 1m00.59s || +0m01.50s 0m43.59s | Specific/X2448/Karatsuba/C64/Synthesis | 0m44.86s || -0m01.26s 0m34.97s | Specific/X25519/C32/fesquare | 0m35.98s || -0m01.00s 0m20.10s | Specific/NISTP256/AMD64/fesub | 0m18.37s || +0m01.73s 0m17.61s | Specific/NISTP256/AMD64/feadd | 0m15.94s || +0m01.67s 2m09.77s | Specific/X25519/C64/ladderstep | 2m09.79s || -0m00.01s 1m11.70s | Specific/X2448/Karatsuba/C64/femul | 1m11.60s || +0m00.10s 0m32.14s | Specific/X25519/C32/Synthesis | 0m31.70s || +0m00.44s 0m27.94s | Specific/X25519/C32/freeze | 0m28.06s || -0m00.11s 0m17.62s | Specific/X25519/C64/femul | 0m17.41s || +0m00.21s 0m15.21s | Specific/X25519/C64/freeze | 0m14.74s || +0m00.47s 0m14.86s | Specific/NISTP256/AMD64/feopp | 0m14.96s || -0m00.10s 0m14.58s | Specific/X25519/C64/fesquare | 0m14.06s || +0m00.51s 0m10.10s | Specific/X25519/C64/Synthesis | 0m09.78s || +0m00.32s 0m06.22s | Specific/X2555/C128/Synthesis | 0m06.17s || +0m00.04s 0m01.01s | Specific/X25519/C32/CurveParameters | 0m01.05s || -0m00.04s 0m00.99s | Specific/Framework/SynthesisFramework | 0m01.08s || -0m00.09s 0m00.79s | Specific/Framework/MontgomeryReificationTypes | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || +0m00.08s 0m00.78s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.75s || +0m00.03s 0m00.76s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | N/A || +0m00.76s 0m00.75s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.80s || -0m00.05s 0m00.75s | Specific/Framework/MontgomeryReificationTypesPackage | N/A || +0m00.75s 0m00.73s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.75s || -0m00.02s 0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.70s || +0m00.02s 0m00.72s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.73s || -0m00.01s 0m00.72s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.69s || +0m00.03s 0m00.72s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s || -0m00.04s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.75s || -0m00.05s 0m00.70s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.77s || -0m00.07s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.71s || -0m00.02s 0m00.67s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.74s || -0m00.06s 0m00.43s | Specific/X25519/C64/CurveParameters | 0m00.43s || +0m00.00s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.40s || -0m00.02s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.37s || +0m00.01s 0m00.34s | Specific/Framework/CurveParameters | 0m00.32s || +0m00.02s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.33s || +0m00.00s 0m00.32s | Specific/NISTP256/AMD128/CurveParameters | N/A || +0m00.32s 0m00.32s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.33s || -0m00.01s 0m00.31s | Specific/Framework/CurveParametersPackage | 0m00.33s || -0m00.02s 0m00.30s | Specific/NISTP256/AMD64/CurveParameters | N/A || +0m00.30s
* Reorganize the curve-specific synthesis frameworkGravatar Jason Gross2017-10-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This brings in most of the changes that I made when figuring out how to integrate montgomery into the framework. The code is a bit slower because the we drop `Print Assumptions` at the bottom of each synthesis problem, to record that things are closed under the global context. If we remove this, we get back the time that we lost with this commit. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m10.63s | Total | 11m51.91s || +1m18.71s --------------------------------------------------------------------------------------------- 1m15.83s | Specific/X2555/C128/ladderstep | 1m02.57s || +0m13.25s 1m03.07s | Specific/X25519/C32/femul | 0m54.99s || +0m08.07s 0m36.49s | Specific/X25519/C32/fesquare | 0m27.77s || +0m08.72s 1m08.99s | Specific/X2448/Karatsuba/C64/femul | 1m01.88s || +0m07.10s 0m26.82s | Specific/X25519/C32/freeze | 0m19.81s || +0m07.01s 2m06.29s | Specific/X25519/C64/ladderstep | 2m00.03s || +0m06.26s 0m17.48s | Specific/X25519/C64/femul | 0m10.81s || +0m06.67s 0m14.78s | Specific/X25519/C64/freeze | 0m08.19s || +0m06.58s 0m14.12s | Specific/X25519/C64/fesquare | 0m07.45s || +0m06.66s 1m48.54s | Specific/NISTP256/AMD64/femul | 1m51.58s || -0m03.04s 0m44.50s | Specific/X2448/Karatsuba/C64/Synthesis | 0m43.81s || +0m00.68s 0m31.40s | Specific/X25519/C32/Synthesis | 0m31.02s || +0m00.37s 0m25.72s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.34s || +0m00.37s 0m18.36s | Specific/NISTP256/AMD64/fesub | 0m18.79s || -0m00.42s 0m16.45s | Specific/NISTP256/AMD64/feadd | 0m16.40s || +0m00.05s 0m15.15s | Specific/NISTP256/AMD64/feopp | 0m14.79s || +0m00.36s 0m12.27s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.90s || +0m00.36s 0m12.06s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.89s || +0m00.16s 0m10.93s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.39s || -0m00.46s 0m10.12s | Specific/X25519/C64/Synthesis | 0m09.86s || +0m00.25s 0m09.86s | Specific/NISTP256/AMD64/fenz | 0m09.54s || +0m00.32s 0m09.40s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.16s || +0m00.24s 0m06.08s | Specific/X2555/C128/Synthesis | 0m05.72s || +0m00.36s 0m01.06s | Specific/Framework/SynthesisFramework | 0m00.98s || +0m00.08s 0m01.05s | Specific/X25519/C32/CurveParameters | 0m01.01s || +0m00.04s 0m00.88s | Specific/Framework/ReificationTypes | 0m00.84s || +0m00.04s N/A | Specific/Framework/ArithmeticSynthesisFramework | 0m00.82s || -0m00.82s 0m00.81s | Specific/Framework/ArithmeticSynthesis/Karatsuba | N/A || +0m00.81s 0m00.79s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Base | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Freeze | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/BasePackage | N/A || +0m00.78s 0m00.76s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.78s || -0m00.02s 0m00.74s | Specific/Framework/ArithmeticSynthesis/HelperTactics | N/A || +0m00.74s 0m00.74s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | N/A || +0m00.74s 0m00.73s | Specific/Framework/ArithmeticSynthesis/FreezePackage | N/A || +0m00.73s 0m00.72s | Specific/Framework/ReificationTypesPackage | N/A || +0m00.72s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Defaults | N/A || +0m00.70s 0m00.69s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | N/A || +0m00.69s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | N/A || +0m00.69s 0m00.68s | Specific/Framework/ArithmeticSynthesis/Ladderstep | N/A || +0m00.68s N/A | Specific/Framework/LadderstepSynthesisFramework | 0m00.68s || -0m00.68s 0m00.42s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.39s || +0m00.02s 0m00.40s | Specific/X25519/C64/CurveParameters | 0m00.44s || -0m00.03s 0m00.34s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.35s || -0m00.00s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParametersPackage | N/A || +0m00.33s 0m00.31s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.32s || -0m00.01s 0m00.07s | Specific/Framework/Packages | N/A || +0m00.07s
* 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`.
* 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
* Revert "Add -compat 8.6 to _CoqProject"Gravatar Jason Gross2017-10-18
| | | | This reverts commit 131f341f368b606fd50b57f135e602e40e132b46.
* 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.
* Add MulSplitUnfolderGravatar Jason Gross2017-10-17
|
* Add faster arithmetic unfoldingGravatar Jason Gross2017-10-15
|
* Add TagListGravatar Jason Gross2017-10-10
| | | | | List of dynamically-typed key-value pairs, and some helper definitions and tactics.
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
|
* 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
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
|
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
|
* 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
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
|
* Add UnfoldArgGravatar Jason Gross2017-07-08
|
* automate P256 integrationGravatar Andres Erbsen2017-07-02
|
* Reorganization of saturated arithmeticGravatar jadep2017-06-29
|
* Add nonzero synthesisGravatar Jason Gross2017-06-26
|
* Weierstrass Jacobian mixed additionGravatar Andres Erbsen2017-06-23
|
* Add (partially admitted) integration tests for add, sub, oppGravatar Jason Gross2017-06-22
|
* move Specifi p256 files into their own directoryGravatar Andres Erbsen2017-06-22
|
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
|
* Add fold_left_orb_true, fold_left_orb_pullGravatar Jason Gross2017-06-20
|
* Add ModInvGravatar Jason Gross2017-06-18
| | | | This closes #209.
* compile X25519 C code from MakefileGravatar Andres Erbsen2017-06-18
|
* add 128-bit display fileGravatar Jason Gross2017-06-17
|
* Add 128-bit version of montgomery for testingGravatar Jason Gross2017-06-17
|
* Finish MontgomeryP256 (less conditional subtract)Gravatar Jason Gross2017-06-17
|
* Add initial IntegrationTestMontgomeryP256.vGravatar Jason Gross2017-06-17
|
* Fix spellingGravatar Jason Gross2017-06-17
|
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-06-16
| | | | | | | The new parameterized definitions and proofs are in WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused) in WordByWord/Abstract/*. I replaced definitions I didn't know how to write in the Saturated API with the use of an axiom.
* Fix buildGravatar Jason Gross2017-06-16
|
* Revert PR #203Gravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964 and https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747 Revert "update ocq2C sed script" This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e. Revert "make display" This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e. Revert "Make use of CArrayNotations" This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb. Revert "Fix CArrayNotations" This reverts commit d0d0fbd4499296a2164e209466227892671556f0. Revert "Revert "Revert "Add CArrayNotations""" This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
| | | | This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-06-15
| | | | | | | This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339. It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469), which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out).
* Finish karatsuba mul, add display file (#199)Gravatar Jason Gross2017-06-15
| | | This closes #182.
* Add CArrayNotationsGravatar Jason Gross2017-06-15
|
* Add -compat 8.6 to _CoqProjectGravatar Jason Gross2017-06-15
| | | | | | This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet).
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
|
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
|
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
|
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
|
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
| | | | Now it can handle ops that return (Tbase TZ)
* Add Z.peano_rectGravatar Jason Gross2017-06-13
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 22:49:12 +0000