aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Attempt to build travis in stagesGravatar Jason Gross2018-01-16
| | | | | | | | | | | | Hopefully this will lead to overall faster builds Also: - try to allow failures - Version-specific vo caches - Make archives stage-specific This way, if multiple branches are running stages at the same time, they don't have as much a chance of clobbering each others builds.
* Add separate targets to build but not run test/benchGravatar Jason Gross2018-01-16
|
* [travis] 8.7.0 -> 8.7.1Gravatar Jason Gross2018-01-15
|
* Fix liblow.h for cmovznz64Gravatar Jason Gross2018-01-15
|
* Update cmovznz to cmovznz64 in the .c fileGravatar Jason Gross2018-01-15
|
* Add .c and .log filesGravatar Jason Gross2018-01-15
|
* Add x25519 donna versions with the new way of generating C codeGravatar Jason Gross2018-01-15
|
* Combine the zero and non-zero cases together.Gravatar David Benjamin2018-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.Gravatar David Benjamin2018-01-14
|
* Add travis_retry to work around bugs in travisGravatar Jason Gross2018-01-10
| | | | https://github.com/travis-ci/travis-ci/issues/8507
* Add some fecarry .log filesGravatar Jason Gross2018-01-10
|
* Add some fecarry .log and .c filesGravatar Jason Gross2018-01-10
|
* Generate fecarry for solinasGravatar Jason Gross2018-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 lemmasGravatar Jason Gross2018-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_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Massively speed up JacobianGravatar Jason Gross2018-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"Gravatar Jason Gross2018-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_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Jabobian.v: par -> allGravatar Andres Erbsen2018-01-09
|
* src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*Gravatar Andres Erbsen2018-01-09
|
* Move Curves/Weierstrass/Jacobian to curves-proofsGravatar Jason Gross2018-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+JacobianGravatar Andres Erbsen2018-01-09
|
* Jacobian coordinatesGravatar Andres Erbsen2018-01-09
|
* make src/Specific/solinas64_2e255m19_5limbs/*.cGravatar David Benjamin2018-01-08
| | | | | Also refresh things after PR#289. This too just updated the comments, as expected.
* Prove montladder correct in the zero case.Gravatar David Benjamin2018-01-08
|
* Add @@ infix notationGravatar Jason Gross2018-01-06
|
* make src/Specific/solinas32_2e255m19_10limbs/*.cGravatar David Benjamin2018-01-05
| | | | | Refresh things after PR#289, though that just updated the comments, as expected.
* Fix incorrect overridding of bool notationsGravatar Jason Gross2018-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 3Gravatar Jason Gross2018-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, subborrowGravatar Jason Gross2018-01-05
| | | | This handles bullet 3 of #288
* Print bool as uint8_tGravatar Jason Gross2018-01-05
| | | | This handles bullet point 1 of #288
* make selected-specific-display for permit `TWord 0`Gravatar Jason Gross2018-01-05
| | | | This handles bullet 2 of #288
* Permit `TWord 0`Gravatar Jason Gross2018-01-05
| | | | This handles bullet 2 of #288
* Add support for {addcarryx,subborrow}_u{25,26}Gravatar Jason Gross2018-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 CNotationsGravatar Jason Gross2018-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 stuffGravatar Jason Gross2017-12-27
|
* restore fastpath logic in Curves.Montgomery.XZProofsGravatar Andres Erbsen2017-12-22
|
* prove montgomery ladder for non-zero inputsGravatar Andres Erbsen2017-12-22
|
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
|
* specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* expose missing proof in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* clean up src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* Add pow_ceil_mul_nat_divide_nonzeroGravatar Jason Gross2017-12-15
|
* Add reserved notation for infix @ for applicationGravatar Jason Gross2017-12-15
|
* organize .gitignoreGravatar Andres Erbsen2017-12-15
|
* add non-cps version of chained_carries (resolves #283 again)Gravatar jadep2017-12-14
|
* add non-cps carry to experimental pipeline (this resolves #283)Gravatar jadep2017-12-14
|
* Also display timing on .log filesGravatar Jason Gross2017-12-14
|
* Also build non-specific on smithersGravatar Jason Gross2017-12-13
|
* Add missing file from previous commitGravatar Jason Gross2017-12-13
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:22:13 +0000