| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change
---------------------------------------------------------------------------------------
10m34.32s | Total | 11m10.14s || -0m35.81s
---------------------------------------------------------------------------------------
0m04.75s | Compilers/Z/Bounds/Pipeline/Definition | 0m41.89s || -0m37.14s
1m24.64s | Specific/IntegrationTestKaratsubaMul | 1m20.20s || +0m04.43s
1m59.10s | Specific/X25519/C64/ladderstep | 2m00.27s || -0m01.17s
1m14.55s | Specific/IntegrationTestLadderstep130 | 1m13.12s || +0m01.42s
0m49.89s | Specific/X25519/C32/femul | 0m51.34s || -0m01.45s
0m26.72s | Specific/X25519/C32/fesquare | 0m27.79s || -0m01.07s
1m51.04s | Specific/NISTP256/AMD64/femul | 1m50.92s || +0m00.11s
0m25.48s | Specific/IntegrationTestMontgomeryP256_128 | 0m24.72s || +0m00.76s
0m18.54s | Specific/NISTP256/AMD64/fesub | 0m18.60s || -0m00.06s
0m15.57s | Specific/NISTP256/AMD64/feadd | 0m15.78s || -0m00.20s
0m14.93s | Specific/NISTP256/AMD64/feopp | 0m15.09s || -0m00.16s
0m12.13s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.34s || -0m00.20s
0m11.78s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.35s || -0m00.57s
0m11.06s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.24s || -0m00.17s
0m10.16s | Specific/X25519/C64/femul | 0m10.18s || -0m00.01s
0m09.78s | Specific/NISTP256/AMD64/fenz | 0m10.10s || -0m00.32s
0m09.06s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.26s || -0m00.19s
0m08.63s | Specific/IntegrationTestSub | 0m08.32s || +0m00.31s
0m07.84s | Specific/IntegrationTestFreeze | 0m07.87s || -0m00.03s
0m07.27s | Specific/X25519/C64/fesquare | 0m07.25s || +0m00.01s
0m00.80s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.81s || -0m00.01s
0m00.61s | Compilers/Z/Bounds/Pipeline | 0m00.70s || -0m00.08s
|
|
|
|
|
| |
This is a faster version of [autorewrite with reflective_interp] on
large chains of expressions.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
I'm very confused about how and when it was introduced...
|
| |
|
| |
|
|
|
|
| |
This makes it easier to extend the bounds analysis framework.
|
|
|
|
|
| |
Hopefully this will help with extending the framework. Also remove
[t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 closes #228
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Actually this time
|
|
|
|
|
|
| |
This reverts commit ecff47dbc867261b81c6e268eca99e5b5ab28805.
It was wrong
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5615, Ltac should be
able to bind references and not just names, in which names are slippery,
slippery objects.
|
|
|
|
| |
This is needed when we're subtracting 0 >.>
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
Might have something to do with #213.
Also, RewriteAddToAdcInterp is now a bit more stable under changes to
the rewriting strategy (the parts are now more separate).
|