fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	use [positive] for [F] modulus, char_ge_C instead of char_gt_C	Andres Erbsen	2017-03-02
\|
*	prove testbit_sub_pow2	Andres Erbsen	2016-10-29
\|
*	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
\| \| \| \|	This way we will have a faster build of reification things
*	Created separate definitions for cmovne and cmovl for reification	jadep	2016-10-23
\|
*	Modified [freeze] to be more reifyable	jadep	2016-10-22
\|
*	Moved conversion logic out of Pow2BaseProofs into its own file	jadep	2016-10-06
\|
*	Finished remaining admits in [freeze] proofs	jadep	2016-09-23
\|
*	Reorganization, moving of lemmas to correct files, and 8.4 compatibility	jadep	2016-09-21
\|
*	Proved specification of constant-time modulus comparison (except for one ↵	jadep	2016-09-21
\| \| \| \|	ZUtil lemma)
*	Move side lemmas to appropriate files	jadep	2016-09-17
\|
*	Fully qualify [Require]s	Jason Gross	2016-09-08
\| \| \| \|	This way they won't become ambiguous if we add new files
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], ↵	jadep	2016-09-06
\| \| \| \|	cleaning up freeze-related organization and definitions along the way
*	Instantiated conversion both to (pack) and from (unpack) another set of limb ↵	jadep	2016-08-16
\| \| \| \|	widths in ModularBaseSystem
*	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this ↵	jadep	2016-07-25
\| \| \| \|	change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
*	merge	jadep	2016-07-20
\|
*	restructured ModularBaseSystem pipeline to put tuple conversion before ↵	jadep	2016-07-20
	ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt