| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
If, e.g., we know from bounds analysis that the result of an operation
fits in the range r[0~>0], we now just replace it with the literal
constant.
Fixes #493
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05%
--------------------------------------------------------------------------------------------
4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23%
3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11%
2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28%
1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42%
1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31%
1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20%
0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06%
0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38%
0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38%
0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39%
0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65%
0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49%
0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11%
0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75%
0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35%
0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94%
0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00%
0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09%
0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08%
0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39%
0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42%
0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59%
0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50%
0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33%
0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75%
0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57%
0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40%
0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49%
0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45%
0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33%
0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74%
0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73%
0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00%
0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14%
0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
|
| |
|
|
| |
The minimum is -2^(bitwidth-1), not -2^bitwidth. Oops.
|
| |
|
|
|
|
|
|
|
|
|
| |
Unfortunately, signed->unsigned casts do not commute with shifts. We
take care to only extend the range when it needs extending, now. This
was previously causing issues with subborrow.
We should really get proofs about casts in C semantics at some point
soon.
Fixes #489
|
|
|
This allows us to support primes which are not a power of 2.
We also add p484 as an example.
To support this, I added a small parser combinator library which can
parse arithmetic expressions involving `()^*/+-` and decimal digits.
Closes #486
Closes #342
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61%
--------------------------------------------------------------------------------------------
9m41.91s | p484_32.c | N/A || +9m41.90s | ∞
0m11.51s | p484_64.c | N/A || +0m11.50s | ∞
3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18%
4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80%
0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35%
0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05%
0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06%
0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03%
0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12%
0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17%
0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47%
0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76%
0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39%
0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06%
0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75%
0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16%
0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18%
0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50%
0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80%
0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93%
0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40%
0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72%
0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14%
0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40%
0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28%
0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70%
0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28%
0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12%
0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43%
0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03%
0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞
|
Jason Gross