fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
\|
*	tuple: applying functions to tuples of arbitrary length	Andres Erbsen	2016-07-12
\|
*	Merge of fixedlength and master	jadep	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
\| \|
\| *	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.
\| \| *	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
\| * \|	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
\| \|/
\| *	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
\| *	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.
* \| \| \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\| \| \| \|
* \| \| \|	Tuple: lift functions from lists to tuples	Andres Erbsen	2016-07-03
\| \| \| \|
\| \| \| *	Indentation in ZUtil	Jason Gross	2016-07-02
\| \| \| \|
\| \| \| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
* \| \|	Fix for 8.4 evars	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add ZUtil hints	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add more hints to ZUtil	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add more hints in ZUtil	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add more ZUtil hints	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add more hints to ZUtil	Jason Gross	2016-07-01
\| \| \|
* \| \|	Add hint databases and a proof about Z.log2	Jason Gross	2016-07-01
\| \| \|