| Commit message (Collapse) | Author | Age |
|
|
|
| |
Remove Util/NUtil.v and Util/WordUtil.v. This code is no longer in use.
|
|
|
|
|
|
| |
Remove Util/BoundedWord.v and its reverse dependencies
Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no
longer in use.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
This way we can pick it up based on the bool, and not just on the Prop.
This allows us to `apply Reflect.reflect_bool in H` for `H : negb (_ =?
_) = true` and have it work.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Rather than taking the convention that failures during constr
construction emit a type error from `I : I` with the actual error
message `idtac`d above them (because Coq has no way to emit multiple
things on stderr), we instead factor everything through a new
`constr_fail` or `constr_fail_with msg_tac`, which emit more helpful
messages instructing the user to look in `*coq*` or to use `Fail`/`try`
to see the more informative error message. When we can make our own
version that does both `idtac` and `fail` (c.f.
https://github.com/coq/coq/issues/3913), then we can do something a bit
more sane, hopefully.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
It turns out they don't actually work. See
https://github.com/coq/coq/issues/9719,
https://github.com/coq/coq/issues/9718,
https://github.com/coq/coq/issues/9717,
https://github.com/coq/coq/issues/9462#issuecomment-470822923
|
|
|
|
| |
It previously required progress on all goals, rather than any goal
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
These will be useful for extending the AST with `option` types.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
It was colliding with the ?[a] notation for fresh evars
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Copied verbatim from
https://github.com/mit-plv/fiat/blob/master/src/Common/String_as_OT.v
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 | ∞
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|