| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
| |
This requires some changes to nonzero, which now needs to unfold
proj1_sig itself.
|
| |
|
|
|
|
| |
src/Specific/X25519/C64/scalarmult.c
|
| |
|
| |
|
|
|
|
|
| |
32-bit ladderstep takes way too long (at least on Coq 8.6), so we don't
add it yet
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
```
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
```
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
passed after fixing some stupid typos in glue code -- no conceptual
issues.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This proof should possibly be factored out and go elsewhere.....
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|