| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
This is a one-line change in generate_parameters.py (plus some
whitespace trimming), and running `make regenerate-curves`
This handles part of #294
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
-------------------------------------------------------------------------
1m11.42s | Total | 1m53.75s || -0m42.33s | -37.21%
-------------------------------------------------------------------------
1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96%
0m05.40s | Util/FsatzAutoLemmas | N/A || +0m05.40s | ∞
|
|
|
|
| |
We no longer seem to need the stronger hypothesis.
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
---------------------------------------------------------------------------
1m52.31s | Total | 13m36.75s || -11m44.44s | -86.24%
---------------------------------------------------------------------------
1m52.31s | Curves/Weierstrass/Jacobian | 13m36.75s || -11m44.44s | -86.24%
|
|
|
|
|
|
| |
This reverts commit d33d8be154dbce048ac10d82bc0b39468abd5fdb.
Hmm, apparently there's an error on Qed... maybe a bug in fsatz?
|
|
|
|
| |
We no longer seem to need the stronger hypothesis.
|
| |
|
| |
|
|
|
|
|
| |
We have about 15 minutes to spare on the curves-proofs travis job, so we
move Jacobian.vo from no-curves-proofs-non-specific to there.
|
| |
|
| |
|
|
|
|
|
| |
Also refresh things after PR#289. This too just updated the comments, as
expected.
|
| |
|
| |
|
|
|
|
|
| |
Refresh things after PR#289, though that just updated the comments, as
expected.
|
|
|
|
|
|
|
| |
This notation system is fragile and kludgy.
This discovered from @davidben's
https://github.com/mit-plv/fiat-crypto/pull/289/commits/ff0fb38346dde67abef982d6305595216d18519b#r159793723
|
|
|
|
|
| |
We do this by adding notations for addcarryx and subborrow for all of
the smaller-than-max-bitwidth sizes of arguments.
|
|
|
|
| |
This handles bullet 3 of #288
|
|
|
|
| |
This handles bullet point 1 of #288
|
|
|
|
| |
This handles bullet 2 of #288
|
|
|
|
| |
This handles bullet 2 of #288
|
|
|
|
|
|
|
|
|
|
|
| |
This closes #286
This is actually a +1,-1 diff in the python script generating the
notations, plus running it and rebuilding:
```diff
-ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 51)
+ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 25, 26, 51)
```
|
|
|
|
|
|
| |
This makes it easier to add support for more kinds of addcarryx, etc,
and also add `: expr_scope` to work around changes from
https://github.com/coq/coq/pull/873
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This will hopefully work better than kludging around coqdep
|
|
|
|
| |
building things
|
| |
|
| |
|
|
|
|
|
|
|
| |
Also add a kludge to override the .v.d targets of the relevant files.
It unfortunately spews a lot of makefile output, but it's better than
the target not working at all. When the target is not passed, the
behavior is unchanged.
|
|
|
|
| |
* clean up src/Experiments/Loops.v, add While and For
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|