fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	separate freeze into two parts	jadep	2016-11-11
*	Silence a warning about name collision	Jason Gross	2016-11-09
*	Make [freeze] proofs consider machine integer width and hard input bounds sep...	jadep	2016-11-03
*	Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...	jadep	2016-11-02
*	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
*	Slightly loosen freeze preconditions (in particular, I had failed to properly...	jadep	2016-10-27
*	Created separate definitions for cmovne and cmovl for reification	jadep	2016-10-23
*	final touches/fixes for freeze restructuring	jadep	2016-10-22
*	Modified [freeze] to be more reifyable	jadep	2016-10-22
*	Define carry_opp in terms of carry_sub	Jason Gross	2016-10-19
*	Add opt versions of add, sub, opp	Jason Gross	2016-10-19
*	Added top-level modulus comparison operation so field-element decoding can re...	jadep	2016-10-12
*	Fix compatibility with sigT notation	Jason Gross	2016-10-10
*	Moved conversion logic out of Pow2BaseProofs into its own file	jadep	2016-10-06
*	map -> List.map (not Tuple.map)	Jason Gross	2016-09-29
*	Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...	jadep	2016-09-17
*	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
*	Finished sqrt in GF25519	jadep	2016-09-06
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...	jadep	2016-09-06
*	Added square roots to GF1305, started reworking freeze_opt in preparation for...	jadep	2016-08-31
*	Generalized exponentiation chains so inverse and square roots can use the sam...	jadep	2016-08-31
*	Removed some commented-out code that will probably not be needed.	jadep	2016-08-31
*	Changed definition of [sub] to require proof that the modulus multiple actual...	jadep	2016-08-25
*	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
*	Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6	jadep	2016-08-24
*	Added optimized [inv] operation to Specific, and removed dependencies on Modu...	jadep	2016-08-24
*	Shifted around some of the proofs in ModularBaseSystemField.v and propagated ...	jadep	2016-08-23
*	Merge of conversion development branch with master	jadep	2016-08-16
\|\
\| *	Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. Furt...	jadep	2016-08-16
* \|	Add length lemmas	Jason Gross	2016-08-12
\|/
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
*	Massively speed up construct_params (#48)	Jason Gross	2016-08-08
*	Fix 8.4 build.	jadep	2016-07-25
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-25
\|\
* \|	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...	jadep	2016-07-25
\| *	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
\|/
*	Fix 8.4{pl1,pl2} builds	jadep	2016-07-21
*	Changed name of [carry_and_reduce_single] to [carry_single], since it does no...	jadep	2016-07-21
*	Fixes #29	jadep	2016-07-21
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
*	merge	jadep	2016-07-20
\|\
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
\| *	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\|/
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
*	pushing through a tweak to the arguments of [sub], and defining a field over ...	jadep	2016-07-12
*	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
* \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08