fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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 ↵	jadep	2016-07-10
\| \| \| \| \| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
\| *	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
\| \|
\| *	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
\| \|
\| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-08
\| \| \| \| \| \| \| \| \| \|	[rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only accepts one database in 8.4.
* \|	Util/Tuple: added a version of from_list that doesn't require a proof of ↵	jadep	2016-07-08
\| \| \| \| \| \| \| \|	length equality
* \|	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
\| \|
\| *	Add pow2_mod to ZUtil	Jason Gross	2016-07-07
\|/
*	Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.	jadep	2016-07-07
\|
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-07
\|\
\| *	Fix notations, add &	Jason Gross	2016-07-06
\| \|
\| *	Add [update_nth] to ListUtil, change [set_nth]	Jason Gross	2016-07-06
\| \| \| \| \| \| \| \|	Define [set_nth] in terms of [update_nth]
\| *	Add notations for Z.shift{r,l} to ZUtil	Jason Gross	2016-07-06
\| \|
\| *	Improve some reserved notations	Jason Gross	2016-07-06
\| \| \| \| \| \| \| \|	Compatibility with theories/Numbers/NatInt/NZBits.v
\| *	Add a TODO comment	Jason Gross	2016-07-06
\| \| \| \| \| \| \| \|	For jadep, or for me, after the 8.5 build is fixed.
* \|	Proved lingering lemmas in PointEncodingPre.	jadep	2016-07-06
\| \|
\| *	Clean up the makefile a bit	Jason Gross	2016-07-06
\| \|
\| *	Fix coqprime clean, install targets, add cleanall	Jason Gross	2016-07-06
\| \|
\| *	Fix for broken 8.5 build in ListUtil	Jason Gross	2016-07-06
\|/
*	fixed indentation for new lemmas in ZUtil	jadep	2016-07-06
\|
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
* \	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-07-06
\|\ \
* \| \|	Factored out some proofs that rely only on base being powers of two, and ↵	jadep	2016-07-06
\| \| \| \| \| \| \| \| \| \| \| \|	defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
\| \| *	Define the spec of Weierstrass curves (#6)	Jason Gross	2016-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Define the spec of Weierstrass curves This is the start of work on P256.
\| \| *	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).
\| \| *	Merge pull request #19 from JasonGross/rename-z-lemmas	Jason Gross	2016-07-03
\| \| \|\ \| \| \| \| \| \| \| \|	Rename lemmas about Z in ZUtil
\| \| * \	Merge pull request #12 from mit-plv/license	Andres Erbsen	2016-07-02
\| \| \|\ \ \| \| \| \| \| \| \| \| \| \|	update licensing information for #5