fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
*	Fix 8.6 build	Jason Gross	2016-07-26
*	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
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\
* \|	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
\| *	Split up proof in BarrettReduction.Z	Jason Gross	2016-07-21
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	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
\| *	automate a proof	Andres Erbsen	2016-07-20
\| *	compute on [F q]!	Andres Erbsen	2016-07-20
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-20
\|\\|
* \|	merge	jadep	2016-07-20
\|\ \
\| \| *	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
\| \|/
\| *	Don't use auto with *	Jason Gross	2016-07-20
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
\| *	Absolutize some imports	Jason Gross	2016-07-20
\| *	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\| *	Use a proof that doesn't require as many assumptions in extended_base_length	Jason Gross	2016-07-20
\| *	Work around bad design in Coq	Jason Gross	2016-07-19
\| *	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| *	{base} -> base	Jason Gross	2016-07-19
\| *	Move two_k_nonzero to PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| *	Fix side-condition from previous commit	Jason Gross	2016-07-19
\| *	Add another lemma to distr_length	Jason Gross	2016-07-19
* \|	merge	jadep	2016-07-19
\|\\|
* \|	Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.	jadep	2016-07-19
\| *	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
* \|	merge	jadep	2016-07-19
\|\ \
\| \| *	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\| \| *	Add a lemma about base_from_limb_widths and app	Jason Gross	2016-07-18
\| \| *	Move more proofs earlier	Jason Gross	2016-07-18
\| \| *	Make Pow2BaseProofs independent of the def of add_to_nth	Jason Gross	2016-07-18
\| \| *	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \|/
* \|	changed base notation	jadep	2016-07-18
\| *	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\|/
*	ported IterAssocOp to use monoid rather than a billion context variables that...	jadep	2016-07-18
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ...	jadep	2016-07-18
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
*	removing experimental file accidentally included in last commit	jadep	2016-07-12
*	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
\|\
* \|	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
* \|	proved correctness of [add] operation in ModularBaseSystemInterface	jadep	2016-07-08
* \|	defined some group operations, stated group lemma for tuple-based [add] (in t...	jadep	2016-07-08