| Commit message (Collapse) | Author | Age |
... | |
| |
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 | ∞
|
| |
|
| |
|
|
|
|
| |
`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 | ∞
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
rewrite rules (too-tight bound on RSHI and ADDC (0,x,y) not being converted to ADD (x,y)
|
| | |
|
| |
| |
| |
| | |
of_Expr : expand valid_ident
|
| | |
|
| | |
|
| | |
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Unfortunately, the proof is rather slow :-(
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
22m46.26s | Total | 22m03.36s || +0m42.90s | +3.24%
--------------------------------------------------------------------------------------------------------------------
1m57.06s | Experiments/NewPipeline/Arithmetic.vo | 1m15.08s || +0m41.98s | +55.91%
0m42.39s | p521_32.c | 0m39.92s || +0m02.46s | +6.18%
0m35.40s | p521_64.c | 0m33.02s || +0m02.37s | +7.20%
3m15.80s | p384_32.c | 3m17.10s || -0m01.29s | -0.65%
6m19.46s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.91s || +0m00.54s | +0.14%
4m34.80s | Experiments/NewPipeline/Toplevel1.vo | 4m35.56s || -0m00.75s | -0.27%
1m36.64s | Experiments/NewPipeline/Toplevel2.vo | 1m36.64s || +0m00.00s | +0.00%
0m43.22s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.18s || -0m00.96s | -2.17%
0m29.24s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.83s || -0m00.58s | -1.97%
0m22.83s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.87s || -0m00.04s | -0.17%
0m16.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.73s || -0m00.62s | -3.70%
0m14.24s | p256_32.c | 0m13.75s || +0m00.49s | +3.56%
0m14.22s | secp256k1_32.c | 0m14.19s || +0m00.03s | +0.21%
0m11.01s | p384_64.c | 0m10.50s || +0m00.50s | +4.85%
0m09.71s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.86s || -0m00.14s | -1.52%
0m09.69s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.35s || -0m00.66s | -6.37%
0m07.41s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.74s || -0m00.33s | -4.26%
0m06.65s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.52s || +0m00.13s | +1.99%
0m06.50s | p224_32.c | 0m06.47s || +0m00.03s | +0.46%
0m06.24s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.38s || -0m00.13s | -2.19%
0m05.10s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.97s || +0m00.12s | +2.61%
0m04.82s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.04s || -0m00.21s | -4.36%
0m03.95s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.02s || -0m00.06s | -1.74%
0m02.31s | curve25519_32.c | 0m02.24s || +0m00.06s | +3.12%
0m02.03s | p224_64.c | 0m01.92s || +0m00.10s | +5.72%
0m01.91s | secp256k1_64.c | 0m02.00s || -0m00.09s | -4.50%
0m01.90s | p256_64.c | 0m01.86s || +0m00.03s | +2.15%
0m01.54s | curve25519_64.c | 0m01.61s || -0m00.07s | -4.34%
0m01.51s | Experiments/NewPipeline/CLI.vo | 0m01.49s || +0m00.02s | +1.34%
0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.29s || +0m00.00s | +0.00%
0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.32s || -0m00.04s | -3.03%
|
|
|
|
|
| |
This option is soon going to be turned off by default. See
https://github.com/coq/coq/pull/9270
|
|
|
|
| |
autorewrite is slow and not customiziable enough.
|
|
|
|
|
| |
This allows us to push the evaluations with just `autorewrite with
push_eval`
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
sticky point
|
| |
|
| |
|
| |
|
| |
|
| |
|