| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
This requires some changes to nonzero, which now needs to unfold
proj1_sig itself.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Not sure if it actually does anything in this case... The intent is to
prevent tc resolution from unfolding [reify] and [reify_internal] /
picking up one when looking for the other.
After | File Name | Before || Change
---------------------------------------------------------------------------------------
13m02.51s | Total | 13m01.90s || +0m00.60s
---------------------------------------------------------------------------------------
1m30.27s | Specific/IntegrationTestKaratsubaMul | 1m25.34s || +0m04.92s
2m50.80s | Specific/X25519/C64/ladderstep | 2m53.74s || -0m02.93s
2m21.34s | Specific/NISTP256/AMD64/femul | 2m21.37s || -0m00.03s
1m12.30s | Specific/X25519/C32/femul | 1m12.04s || +0m00.26s
1m09.50s | Specific/IntegrationTestLadderstep130 | 1m09.66s || -0m00.15s
0m41.30s | Specific/X25519/C32/fesquare | 0m41.27s || +0m00.02s
0m27.08s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.13s || -0m00.05s
0m17.64s | Specific/NISTP256/AMD64/fesub | 0m18.06s || -0m00.41s
0m16.45s | Specific/IntegrationTestFreeze | 0m17.36s || -0m00.91s
0m15.94s | Specific/NISTP256/AMD64/feadd | 0m16.02s || -0m00.08s
0m14.74s | Specific/NISTP256/AMD64/feopp | 0m14.42s || +0m00.32s
0m14.33s | Specific/X25519/C64/femul | 0m13.97s || +0m00.35s
0m12.41s | Specific/IntegrationTestSub | 0m12.44s || -0m00.02s
0m11.91s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.06s || -0m00.15s
0m11.61s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.39s
0m10.95s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.82s || +0m00.12s
0m10.28s | Specific/X25519/C64/fesquare | 0m10.46s || -0m00.18s
0m09.68s | Specific/NISTP256/AMD64/fenz | 0m09.76s || -0m00.08s
0m09.28s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.30s || -0m00.02s
0m03.54s | Compilers/TestCase | 0m03.41s || +0m00.12s
0m03.04s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.20s || -0m00.16s
0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m02.99s || +0m00.00s
0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.20s || -0m00.04s
0m00.82s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || +0m00.01s
0m00.70s | Compilers/Z/Bounds/Pipeline | 0m00.66s || +0m00.03s
0m00.57s | Compilers/Z/Reify | 0m00.53s || +0m00.03s
0m00.50s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || -0m00.04s
0m00.38s | Compilers/Reify | 0m00.36s || +0m00.02s
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This helps a lot more in C32 ladderstep; we eliminate useless typeclass
unification against hypotheses by separating out the typeclass used for
external overloading and posing hypotheses, and the typeclass used for
recursion under binders.
After | File Name | Before || Change
---------------------------------------------------------------------------------------
12m49.58s | Total | 13m04.75s || -0m15.16s
---------------------------------------------------------------------------------------
2m48.67s | Specific/X25519/C64/ladderstep | 2m58.05s || -0m09.37s
2m21.65s | Specific/NISTP256/AMD64/femul | 2m16.64s || +0m05.01s
1m25.60s | Specific/IntegrationTestKaratsubaMul | 1m30.00s || -0m04.40s
1m08.01s | Specific/X25519/C32/femul | 1m12.17s || -0m04.15s
1m08.25s | Specific/IntegrationTestLadderstep130 | 1m11.61s || -0m03.35s
0m39.67s | Specific/X25519/C32/fesquare | 0m39.16s || +0m00.51s
0m27.09s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.02s || +0m00.07s
0m17.74s | Specific/NISTP256/AMD64/fesub | 0m18.34s || -0m00.60s
0m17.21s | Specific/IntegrationTestFreeze | 0m16.37s || +0m00.83s
0m15.89s | Specific/NISTP256/AMD64/feadd | 0m15.31s || +0m00.58s
0m14.78s | Specific/NISTP256/AMD64/feopp | 0m14.73s || +0m00.04s
0m14.47s | Specific/X25519/C64/femul | 0m14.39s || +0m00.08s
0m12.07s | Specific/IntegrationTestSub | 0m11.76s || +0m00.31s
0m12.07s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.93s || +0m00.14s
0m11.79s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.21s
0m10.84s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.90s || -0m00.06s
0m10.08s | Specific/X25519/C64/fesquare | 0m10.61s || -0m00.52s
0m09.66s | Specific/NISTP256/AMD64/fenz | 0m09.68s || -0m00.01s
0m09.27s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.28s || -0m00.00s
0m03.51s | Compilers/TestCase | 0m03.49s || +0m00.01s
0m03.08s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.23s || -0m00.14s
0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m03.00s || -0m00.00s
0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.15s || +0m00.01s
0m00.86s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.84s || +0m00.02s
0m00.68s | Compilers/Z/Bounds/Pipeline | 0m00.61s || +0m00.07s
0m00.56s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || +0m00.02s
0m00.54s | Compilers/Z/Reify | 0m00.54s || +0m00.00s
0m00.40s | Compilers/Reify | 0m00.41s || -0m00.00s
|
| |
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
```
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.
|
| |
|
| |
|
| |
|