Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [travis] 8.7.0 -> 8.7.1 | Jason Gross | 2018-01-15 |
| | |||
* | Fix liblow.h for cmovznz64 | Jason Gross | 2018-01-15 |
| | |||
* | Update cmovznz to cmovznz64 in the .c file | Jason Gross | 2018-01-15 |
| | |||
* | Add .c and .log files | Jason Gross | 2018-01-15 |
| | |||
* | Add x25519 donna versions with the new way of generating C code | Jason Gross | 2018-01-15 |
| | |||
* | Combine the zero and non-zero cases together. | David Benjamin | 2018-01-15 |
| | | | | | | This required tending to montladder not being proved Feq-preserving (sidestepped by proving for all P = 0), and then some wrestling with scalarmult to show the right-hand side was indeed zero when x is (0, 0). | ||
* | Add a comment for why Z.peano_rect_strong exists. | David Benjamin | 2018-01-14 |
| | |||
* | Add travis_retry to work around bugs in travis | Jason Gross | 2018-01-10 |
| | | | | https://github.com/travis-ci/travis-ci/issues/8507 | ||
* | Add some fecarry .log files | Jason Gross | 2018-01-10 |
| | |||
* | Add some fecarry .log and .c files | Jason Gross | 2018-01-10 |
| | |||
* | Generate fecarry for solinas | Jason Gross | 2018-01-10 |
| | | | | | | | This is a one-line change in generate_parameters.py (plus some whitespace trimming), and running `make regenerate-curves` This handles part of #294 | ||
* | Factor out fsatz lemmas | Jason Gross | 2018-01-09 |
| | | | | | | | | | 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 | ∞ | ||
* | Replace char_ge_12 with char_ge_3 | Jason Gross | 2018-01-09 |
| | | | | We no longer seem to need the stronger hypothesis. | ||
* | Massively speed up Jacobian | Jason Gross | 2018-01-09 |
| | | | | | | | | 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% | ||
* | Revert "Replace char_ge_12 with char_ge_3" | Jason Gross | 2018-01-09 |
| | | | | | | This reverts commit d33d8be154dbce048ac10d82bc0b39468abd5fdb. Hmm, apparently there's an error on Qed... maybe a bug in fsatz? | ||
* | Replace char_ge_12 with char_ge_3 | Jason Gross | 2018-01-09 |
| | | | | We no longer seem to need the stronger hypothesis. | ||
* | Jabobian.v: par -> all | Andres Erbsen | 2018-01-09 |
| | |||
* | src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_* | Andres Erbsen | 2018-01-09 |
| | |||
* | Move Curves/Weierstrass/Jacobian to curves-proofs | Jason Gross | 2018-01-09 |
| | | | | | 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. | ||
* | @davidben merged Jacobian+affine into Jacobian+Jacobian | Andres Erbsen | 2018-01-09 |
| | |||
* | Jacobian coordinates | Andres Erbsen | 2018-01-09 |
| | |||
* | make src/Specific/solinas64_2e255m19_5limbs/*.c | David Benjamin | 2018-01-08 |
| | | | | | Also refresh things after PR#289. This too just updated the comments, as expected. | ||
* | Prove montladder correct in the zero case. | David Benjamin | 2018-01-08 |
| | |||
* | Add @@ infix notation | Jason Gross | 2018-01-06 |
| | |||
* | make src/Specific/solinas32_2e255m19_10limbs/*.c | David Benjamin | 2018-01-05 |
| | | | | | Refresh things after PR#289, though that just updated the comments, as expected. | ||
* | Fix incorrect overridding of bool notations | Jason Gross | 2018-01-05 |
| | | | | | | | This notation system is fragile and kludgy. This discovered from @davidben's https://github.com/mit-plv/fiat-crypto/pull/289/commits/ff0fb38346dde67abef982d6305595216d18519b#r159793723 | ||
* | Handle the fact that we haven't forbidden TWord 3 | Jason Gross | 2018-01-05 |
| | | | | | We do this by adding notations for addcarryx and subborrow for all of the smaller-than-max-bitwidth sizes of arguments. | ||
* | Remove TWord 3 based addcarryx, subborrow | Jason Gross | 2018-01-05 |
| | | | | This handles bullet 3 of #288 | ||
* | Print bool as uint8_t | Jason Gross | 2018-01-05 |
| | | | | This handles bullet point 1 of #288 | ||
* | make selected-specific-display for permit `TWord 0` | Jason Gross | 2018-01-05 |
| | | | | This handles bullet 2 of #288 | ||
* | Permit `TWord 0` | Jason Gross | 2018-01-05 |
| | | | | This handles bullet 2 of #288 | ||
* | Add support for {addcarryx,subborrow}_u{25,26} | Jason Gross | 2018-01-02 |
| | | | | | | | | | | | 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) ``` | ||
* | Update CNotations | Jason Gross | 2018-01-02 |
| | | | | | | 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 | ||
* | Add some reserved notations for cps stuff | Jason Gross | 2017-12-27 |
| | |||
* | restore fastpath logic in Curves.Montgomery.XZProofs | Andres Erbsen | 2017-12-22 |
| | |||
* | prove montgomery ladder for non-zero inputs | Andres Erbsen | 2017-12-22 |
| | |||
* | Montgomery.XZ, Loops: montladder proof scaffolding | Andres Erbsen | 2017-12-22 |
| | |||
* | specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.v | Andres Erbsen | 2017-12-22 |
| | |||
* | expose missing proof in src/Curves/Montgomery/XZProofs.v | Andres Erbsen | 2017-12-22 |
| | |||
* | clean up src/Curves/Montgomery/XZProofs.v | Andres Erbsen | 2017-12-22 |
| | |||
* | Add pow_ceil_mul_nat_divide_nonzero | Jason Gross | 2017-12-15 |
| | |||
* | Add reserved notation for infix @ for application | Jason Gross | 2017-12-15 |
| | |||
* | organize .gitignore | Andres Erbsen | 2017-12-15 |
| | |||
* | add non-cps version of chained_carries (resolves #283 again) | jadep | 2017-12-14 |
| | |||
* | add non-cps carry to experimental pipeline (this resolves #283) | jadep | 2017-12-14 |
| | |||
* | Also display timing on .log files | Jason Gross | 2017-12-14 |
| | |||
* | Also build non-specific on smithers | Jason Gross | 2017-12-13 |
| | |||
* | Add missing file from previous commit | Jason Gross | 2017-12-13 |
| | |||
* | [travis] remove autogenerated files from _CoqProject | Jason Gross | 2017-12-13 |
| | | | | This will hopefully work better than kludging around coqdep | ||
* | Apparently ln -s is too slow on travis, so we fake it when we're not ↵ | Jason Gross | 2017-12-13 |
| | | | | building things |