| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We port the computation of the carry chain from generate_parameters.py
to Coq, for unsaturated solinas.
Note that while we now bounds-check p448, we do not yet support
goldilocks nor karatsuba.
However, there is still an issue with the synthesized p448 code, which
is that on 64-bit, it tries to use 256-bit and 512-bit integers. I'm
not sure what's up with that.
Partial progress towards #507
After | File Name | Before || Change | % Change
------------------------------------------------------------------------------------------
8m51.64s | Total | 8m34.60s || +0m17.04s | +3.31%
------------------------------------------------------------------------------------------
0m15.16s | p448_solinas_64.c | N/A || +0m15.16s | ∞
3m09.12s | p384_32.c | 3m09.36s || -0m00.24s | -0.12%
0m44.99s | ExtractionHaskell/word_by_word_montgomery | 0m44.91s || +0m00.08s | +0.17%
0m39.58s | p521_32.c | 0m39.22s || +0m00.35s | +0.91%
0m32.54s | p521_64.c | 0m32.49s || +0m00.04s | +0.15%
0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m31.04s || -0m00.16s | -0.54%
0m24.31s | ExtractionHaskell/saturated_solinas | 0m24.32s || -0m00.01s | -0.04%
0m18.62s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m17.90s || +0m00.72s | +4.02%
0m17.53s | ExtractionOCaml/word_by_word_montgomery | 0m17.44s || +0m00.08s | +0.51%
0m13.36s | secp256k1_32.c | 0m13.58s || -0m00.22s | -1.62%
0m13.21s | p256_32.c | 0m13.15s || +0m00.06s | +0.45%
0m11.47s | p484_64.c | 0m11.39s || +0m00.08s | +0.70%
0m11.27s | ExtractionOCaml/unsaturated_solinas | 0m10.71s || +0m00.55s | +5.22%
0m10.48s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || +0m00.14s | +1.35%
0m07.97s | ExtractionOCaml/saturated_solinas | 0m07.98s || -0m00.01s | -0.12%
0m07.05s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.98s || +0m00.06s | +1.00%
0m06.58s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.48s || +0m00.09s | +1.54%
0m06.09s | p224_32.c | 0m06.04s || +0m00.04s | +0.82%
0m05.24s | p384_64.c | 0m05.34s || -0m00.09s | -1.87%
0m05.13s | ExtractionOCaml/saturated_solinas.ml | 0m05.19s || -0m00.06s | -1.15%
0m05.00s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.01s | +0.40%
0m04.14s | ExtractionHaskell/saturated_solinas.hs | 0m04.04s || +0m00.09s | +2.47%
0m02.22s | curve25519_32.c | 0m02.22s || +0m00.00s | +0.00%
0m01.49s | curve25519_64.c | 0m01.53s || -0m00.04s | -2.61%
0m01.46s | CLI.vo | 0m01.44s || +0m00.02s | +1.38%
0m01.29s | SlowPrimeSynthesisExamples.vo | 0m01.24s || +0m00.05s | +4.03%
0m01.08s | p256_64.c | 0m01.00s || +0m00.08s | +8.00%
0m01.06s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.10s | +10.41%
0m01.06s | secp256k1_64.c | 0m01.17s || -0m00.10s | -9.40%
0m01.02s | p224_64.c | 0m01.08s || -0m00.06s | -5.55%
0m00.99s | StandaloneHaskellMain.vo | 0m01.08s || -0m00.09s | -8.33%
0m00.27s | TAPSort.vo | N/A || +0m00.27s | ∞
|
| |
|
| |
|
| |
|
|
|
|
| |
This is in preparation for coq/coq#9274.
|
| |
|
| |
|
|
|
|
| |
Closes #497
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We no longer accept `1,1` as a valid bitwidth.
This closes #488. It does not quite fix the issue as stated, but it
resolves the underlying confusion that generated it (the difference
between passing `1,1` as a `c` vs passing `1,1` as a bitwidth). It
still might be nice to someday emit warnings as suggested in the bug
report.
I've also factored out a bit of code to make it easier to report parse
failures, by folding over a list of parses.
|
|
|
|
|
|
|
|
| |
This disables the optimization that was recently introduced for
replacing things known to be 0 from the bounds analyzer with the
constant 0. It was messing up some of the other fancy synthesis stages.
Fixes #498
|
|
|
|
| |
It was colliding with the ?[a] notation for fresh evars
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43%
--------------------------------------------------------------------------------------------
4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88%
3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68%
2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22%
1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27%
1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01%
1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77%
0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34%
0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63%
0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25%
0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73%
0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80%
0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28%
0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28%
0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45%
0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75%
0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35%
0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77%
0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37%
0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09%
0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12%
0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73%
0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63%
0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18%
0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32%
0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01%
0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93%
0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40%
0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73%
0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88%
0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16%
0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35%
0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58%
0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78%
0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22%
0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Copied verbatim from
https://github.com/mit-plv/fiat/blob/master/src/Common/String_as_OT.v
|
|
|
|
| |
As per https://github.com/mit-plv/fiat-crypto/pull/490/files#r247737121
|
|
|
|
| |
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
|
|
|
| |
It's too slow to generate each time
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 | ∞
|
|
|
|
| |
Or else it doesn't build anything at all
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
`2: {` is not valid in 8.7
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
WIP
Try to remove assumption that s = weight n
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
14m03.04s | Total | 20m54.46s || -6m51.41s | -32.79%
--------------------------------------------------------------------------------------------------------------------
0m01.18s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.83s || -6m17.64s | -99.68%
N/A | Experiments/NewPipeline/Toplevel1.vo | 4m36.32s || -4m36.31s | -100.00%
4m17.06s | Experiments/NewPipeline/PushButtonSynthesis.vo | N/A || +4m17.06s | ∞
1m28.64s | Experiments/NewPipeline/Toplevel2.vo | 1m38.21s || -0m09.57s | -9.74%
3m10.57s | p384_32.c | 3m18.05s || -0m07.48s | -3.77%
0m06.36s | Experiments/NewPipeline/BoundsPipeline.vo | N/A || +0m06.36s | ∞
0m06.16s | Experiments/NewPipeline/COperationSpecifications.vo | N/A || +0m06.16s | ∞
0m05.66s | p384_64.c | 0m10.80s || -0m05.14s | -47.59%
0m38.24s | p521_32.c | 0m41.31s || -0m03.07s | -7.43%
0m31.64s | p521_64.c | 0m33.94s || -0m02.29s | -6.77%
0m45.06s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.83s || +0m01.23s | +2.80%
0m30.57s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.56s || +0m01.01s | +3.41%
0m13.52s | secp256k1_32.c | 0m14.60s || -0m01.08s | -7.39%
0m01.00s | p256_64.c | 0m02.03s || -0m01.02s | -50.73%
0m24.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m23.62s || +0m00.57s | +2.41%
0m16.66s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.40s || +0m00.26s | +1.58%
0m13.34s | p256_32.c | 0m14.00s || -0m00.66s | -4.71%
0m10.40s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.08s || +0m00.32s | +3.17%
0m10.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.81s || +0m00.29s | +3.05%
0m07.84s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.66s || +0m00.17s | +2.34%
0m07.09s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.62s || +0m00.46s | +7.09%
0m06.89s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || +0m00.46s | +7.32%
0m06.26s | p224_32.c | 0m06.54s || -0m00.28s | -4.28%
0m05.24s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.99s || +0m00.25s | +5.01%
0m04.96s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.94s || +0m00.01s | +0.40%
0m04.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.09s | +2.19%
0m02.13s | curve25519_32.c | 0m02.30s || -0m00.16s | -7.39%
0m01.46s | curve25519_64.c | 0m01.65s || -0m00.18s | -11.51%
0m01.44s | Experiments/NewPipeline/CLI.vo | 0m01.37s || +0m00.06s | +5.10%
0m01.31s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.30s || +0m00.01s | +0.76%
0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.01s | +0.80%
0m01.15s | secp256k1_64.c | 0m01.91s || -0m00.76s | -39.79%
0m01.03s | p224_64.c | 0m02.02s || -0m00.99s | -49.00%
0m00.44s | Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.vo | N/A || +0m00.44s | ∞
|