fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	automate a proof	Andres Erbsen	2016-07-20
*	compute on [F q]!	Andres Erbsen	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
*	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
*	Use update_nth in add_to_nth (#26)	Jason Gross	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
*	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
* \|	added a few length proofs to ModularBaseSystemProofs to help with tuple conve...	jadep	2016-07-08
* \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08
\| *	Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.	jadep	2016-07-07
\| *	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\| \|\
\| * \|	Factored out some proofs that rely only on base being powers of two, and defi...	jadep	2016-07-06
* \| \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
* \| \|	add new interface to ModularBaseSystem	Andres Erbsen	2016-07-03
* \| \|	remove PseudoMersenneRep	Andres Erbsen	2016-07-03
\| \| *	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
\| \| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \|/ \|/\|
\| *	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\| *	encode operation in ModularBaseSystem now uses bitwise operators, taking adva...	jadep	2016-06-29
\| *	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
\|/
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17