aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Handle equality in parsingGravatar Jason Gross2017-08-14
|
* Fixup header and footerGravatar Jason Gross2017-08-14
|
* Update scheduler to know about implicit mulx argGravatar Jason Gross2017-08-14
| | | | | Now it prefers putting together mulx with the same implicit arg (approximated as the same variable with the lower number).
* Use a more realistic processor modelGravatar Jason Gross2017-08-13
|
* Revert "Revert "Subset compiler differently""Gravatar Jason Gross2017-08-13
| | | | This reverts commit c8c82f2edf416b667ba487dfa2cff0795d37cbe6.
* Revert "Subset compiler differently"Gravatar Jason Gross2017-08-13
| | | | This reverts commit 7038444e6515ec51a3b6d1cdfe972664d3f16c81.
* Subset compiler differentlyGravatar Jason Gross2017-08-13
|
* Add heuristic searchGravatar Jason Gross2017-08-13
|
* Add decidable equality with nilGravatar Jason Gross2017-08-13
|
* Update the graph makerGravatar Jason Gross2017-08-13
|
* Update exhaustive search compilerGravatar Jason Gross2017-08-13
|
* Add memoize.py to zinc compiler folderGravatar Jason Gross2017-08-11
|
* wip on register allocation in pythonGravatar Jason Gross2017-08-09
|
* Fix the sense of dependencies in zinc generationGravatar Jason Gross2017-08-09
| | | | | This brings the maximum window size back down to 53, so we use the old method of making dependencies, rather than the new one.
* Get all scheduling done in one frameGravatar Jason Gross2017-08-09
|
* Fix wipGravatar Jason Gross2017-08-09
|
* Larger instruction window for zincGravatar Jason Gross2017-08-09
|
* Add a faster version of the zinc compilerGravatar Jason Gross2017-08-06
|
* Add initial stab at C-compilation by optimizationGravatar Jason Gross2017-08-06
|
* Update crypto-defects.mdGravatar Andres Erbsen2017-07-29
|
* 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
|
* Also test coq v8.7 on travisGravatar 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
|
* Update .gitignore with compilation outputsGravatar Jason Gross2017-07-08
|
* Fix format warning in gccGravatar Jason Gross2017-07-08
| | | | Part of #227
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
|
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
|
* Stronger contextsGravatar Jason Gross2017-07-07
|
* README: recommend against Coq 8.5Gravatar Andres Erbsen2017-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
|
* Don't remove Adam Langley when anonymizing repoGravatar Jason Gross2017-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
|
* capture.sh require constant TSCGravatar Andres Erbsen2017-07-05
|
* s/bash/shGravatar Andres Erbsen2017-07-05
|
* make benchGravatar Andres Erbsen2017-07-05
|
* fix .h dependencies in makefile (closes #235)Gravatar Andres Erbsen2017-07-05
|
* etc: add scripts to control turbo boost and hyper threadingGravatar Andres Erbsen2017-07-05
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:43:17 +0000