fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	partition -> Partition.partition to prevent confusion with List.partition	jadep	2019-04-03
\|
*	fix imports and qualifiers so everything builds	jadep	2019-04-03
\|
*	split up Arithmetic (imports etc. not yet fixed, does not build)	jadep	2019-04-03
\|
*	Add constr_fail and constr_fail_with	Jason Gross	2019-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	start adapting Montgomery to new glue code	jadep	2019-02-21
\|
*	Use Preconditions: Postconditions:, rather than /\ and ->	Jason Gross	2019-02-02
\|
*	More minor improvements in docstrings	Jason Gross	2019-02-02
\|
*	Rename docstring generator based on Andres' suggestion	Jason Gross	2019-02-02
\|
*	Update with davidben's and Andres' suggestions	Jason Gross	2019-02-02
\|
*	Drop `map λ` bits in docstrings	Jason Gross	2019-02-02
\| \| \| \| \| \| \| \| \|	They are redundant with the bounds pre- and post-conditions in WBW montgomery. Also drop the fiat_p... prefix from the `from_montgomery` bits in most of the docstrings, under the assumption that shorter strings with less repetition are more readable.
*	Address code review comments to improve docstrings	Jason Gross	2019-02-02
\|
*	Add autogenerated docstrings to synthesized code	Jason Gross	2019-02-02
\| \| \| \| \| \| \| \| \|	We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours
*	Also display the carry chain in a comment	Jason Gross	2019-01-26
\|
*	Split up PushButtonSynthesis.v	Jason Gross	2019-01-18
	Closes #497