aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* 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
* Update constants filesGravatar Jason Gross2017-09-21
|
* Add extract_ExprGravatar Jason Gross2017-09-21
|
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
|
* make benchGravatar Jason Gross2017-09-12
|
* fsatz tests: 1/(1/x) = xGravatar Andres Erbsen2017-09-11
|
* Fix more commented out alternativesGravatar Jason Gross2017-09-05
|
* Fix commented out alternate version in ladderstepGravatar Jason Gross2017-09-05
|
* Add decidable equality with nilGravatar Jason Gross2017-08-13
|
* 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
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes #239 After | File Name | Before || Change --------------------------------------------------------------------------------------- 10m04.12s | Total | 10m05.68s || -0m01.55s --------------------------------------------------------------------------------------- 2m45.12s | Specific/X25519/C64/ladderstep | 2m48.45s || -0m03.32s 1m06.06s | Specific/IntegrationTestLadderstep130 | 1m04.76s || +0m01.29s 2m03.02s | Specific/NISTP256/AMD64/femul | 2m02.29s || +0m00.72s 1m20.35s | Specific/IntegrationTestKaratsubaMul | 1m20.10s || +0m00.25s 0m25.29s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.17s || +0m00.11s 0m16.66s | Specific/IntegrationTestFreeze | 0m16.18s || +0m00.48s 0m14.81s | Specific/NISTP256/AMD64/feadd | 0m15.09s || -0m00.27s 0m14.58s | Specific/NISTP256/AMD64/fesub | 0m14.48s || +0m00.09s 0m13.23s | Specific/X25519/C64/femul | 0m13.54s || -0m00.30s 0m12.00s | Specific/NISTP256/AMD64/feopp | 0m12.07s || -0m00.07s 0m11.25s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.44s || -0m00.18s 0m11.23s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.19s || +0m00.04s 0m11.06s | Specific/IntegrationTestSub | 0m11.24s || -0m00.17s 0m10.39s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.41s || -0m00.01s 0m09.85s | Specific/X25519/C64/fesquare | 0m09.75s || +0m00.09s 0m09.19s | Specific/NISTP256/AMD64/fenz | 0m09.04s || +0m00.15s 0m08.76s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.11s || -0m00.34s 0m00.69s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.11s 0m00.59s | Compilers/Z/Bounds/Pipeline | 0m00.57s || +0m00.02s
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
| | | | This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
|
* Fix Demo.vGravatar Jason Gross2017-07-08
|
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
|
* More fine-grained importsGravatar Jason Gross2017-07-08
|
* Add UnfoldArgGravatar Jason Gross2017-07-08
|
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
|
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
|
* Stronger contextsGravatar Jason Gross2017-07-07
|
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
|
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
|
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
|
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
|
* 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 ```
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
|
* 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 a mis-aligned comment marker in CNotations scriptGravatar Jason Gross2017-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
|\
* | Closed under the global contextGravatar Andres Erbsen2017-07-02
| |
* | prove [MontgomeryAPI.small_add]Gravatar Andres Erbsen2017-07-02
| |
* | fix [small_div] argumentsGravatar Andres Erbsen2017-07-02
| |
* | [small] admits progress...Gravatar Andres Erbsen2017-07-01
| |
* | make displayGravatar Andres Erbsen2017-07-01
| |
* | proved small_sat_addGravatar jadep2017-07-01
| |
* | changes to log files after running make cGravatar jadep2017-07-01
| |
* | change opp to runtime_oppGravatar jadep2017-07-01
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 10:53:33 +0000