fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	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
*	Merge pull request #21 from JasonGross/base-log-cap-notations	jadephilipoom	2016-07-11
\|\
* \|	An attempt at fixing 8.5pl2	Jason Gross	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
\| *	Merge pull request #22 from mit-plv/wrap-nsatz	Andres Erbsen	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
\| \| *	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
\| \| *	pose proof fails where specialize works (typeclass resolution / unification?)	Andres Erbsen	2016-07-11
\| \| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| \|/
\| *	[congruence] is more powerful in 8.5 than in 8.4	Andres Erbsen	2016-07-11
\| *	Add 8.5pl2 to travis	Jason Gross	2016-07-11
\| *	merge	jadep	2016-07-10
\| \|\
\| * \|	added proofs about addition chain exponentiation for later use in ModularBase...	jadep	2016-07-10
\| \| *	Update .gitignore	Jason Gross	2016-07-10
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-10
\| \| *	Update ListUtil	Jason Gross	2016-07-08
\| \| *	Fix NatUtil for 8.4	Jason Gross	2016-07-08
\| \| *	Add useful tactics and util lemmas	Jason Gross	2016-07-08
* \| \|	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
\| \| *	Add a NatUtil lemma and db	Jason Gross	2016-07-08
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-08
\| \| *	Add Z.div_0_l to ZUtil	Jason Gross	2016-07-08
* \| \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-08
* \| \|	Util/Tuple: added a version of from_list that doesn't require a proof of leng...	jadep	2016-07-08
\| * \|	Util/Tuple: added a version of from_list that doesn't require a proof of leng...	jadep	2016-07-08
\| * \|	Added mod case to zero_bounds	jadep	2016-07-08
\| \| *	Add update_nth out of bounds	Jason Gross	2016-07-07
\| \| *	Add hint db in ListUtil	Jason Gross	2016-07-07
\| \| *	More ListUtil facts	Jason Gross	2016-07-07
\| \| *	Slightly better arguments in ListUtil	Jason Gross	2016-07-07
\| \| *	Correct hintdb names	Jason Gross	2016-07-07
\| \| *	Add more about firstn to listutil	Jason Gross	2016-07-07
\| \| *	Add more update_nth to ListUtil	Jason Gross	2016-07-07
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-07