fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| *	Work around bad design in Coq	Jason Gross	2016-07-19
\| *	Add a distr_length database	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
\| \| *	Add a lemma about sum_firstn	Jason Gross	2016-07-18
\| \| *	Add a ListUtil lemma	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
\| \| *	Silence a warning	Jason Gross	2016-07-18
\| \| *	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| *	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
\| \| *	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
\| \| *	Add more distr_length proofs in BaseSystemProofs	Jason Gross	2016-07-18
\| \| *	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
\| \| *	Add more NatUtil lemmas	Jason Gross	2016-07-18
\| \| *	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
\| \| *	Fix some typos in the previous commit	Jason Gross	2016-07-18
\| \| *	Add some lemmas about nth_default in bounds	Jason Gross	2016-07-18
\| \| *	Remove a nested proof	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
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
*	Fixed unsimplified multiplication definitions in Specific by separating out t...	jadep	2016-07-18
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-15
\|\
* \|	proved an admit in field homomorphisms that turned out to be unprovable; I ad...	jadep	2016-07-15
* \|	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
\| *	Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s	Andres Erbsen	2016-07-13
\| *	tuple: applying functions to tuples of arbitrary length	Andres Erbsen	2016-07-12
\|/
*	re-cleaned operations in Specific and updated GF25519 to match GF1305	jadep	2016-07-12
*	cleaned Specific operations so they produce code without proof terms, and pro...	jadep	2016-07-12
*	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
*	prove that if something is isomorphic to a field, it is a field	jadep	2016-07-11
*	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
\| *	s/conservative_common_denominator/common_denominator/g	Andres Erbsen	2016-07-11
\| *	rename [common_denominator] to [field_simplify_if_div]	Andres Erbsen	2016-07-11
\| *	remove field_algebra	Andres Erbsen	2016-07-11