fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	revived accidentally deleted lemma	jadep	2016-10-30
*	More zsimplify lemmas, stronger Ztestbit	Jason Gross	2016-10-07
*	Moved lemma to ZUtil and added an extra lemma jgross needed	jadep	2016-10-06
*	Moved conversion logic out of Pow2BaseProofs into its own file	jadep	2016-10-06
*	Add reserved notation for Let, change #	Jason Gross	2016-09-17
*	Move side lemmas to appropriate files	jadep	2016-09-17
*	Moved a tactic to Util/Tactics.v	jadep	2016-08-24
*	Merge.	jadep	2016-08-21
\|\
* \|	Proved some leftover admits in Pow2BaseProofs.v	jadep	2016-08-21
* \|	Finished [split_index] proofs and reworked conversion proofs to match.	jadep	2016-08-21
\| *	More 8.4 Admitted fixes	Jason Gross	2016-08-17
\| *	More fixes for 8.4	Jason Gross	2016-08-17
\|/
*	More 8.4 compat	Jason Gross	2016-08-16
*	Fixes for Coq 8.4	Jason Gross	2016-08-16
*	Add some list util, and decode'_map_mul	Jason Gross	2016-08-16
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-16
\|\
* \	Merge of conversion development branch with master	jadep	2016-08-16
\|\ \
\| \| *	Add decode_shift_app	Jason Gross	2016-08-16
\| \|/ \|/\|
\| *	Pow2BaseProofs.v : removed Z lemmas that are now in ZUtil, updated the way [c...	jadep	2016-08-16
* \|	Factor decode_shift_uniform	Jason Gross	2016-08-15
\| *	Proved remaining lemmas directly about conversion loop; still need to prove l...	jadep	2016-08-14
\| *	Conversion: main step proof done	jadep	2016-08-13
* \|	Add decode_nonneg	Jason Gross	2016-08-12
* \|	Add upper_bound_uniform	Jason Gross	2016-08-12
* \|	Weaker UniformBase assumptions	Jason Gross	2016-08-12
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-12
\|\ \
* \| \|	added convenience lemma about [bounded] and [upper_bound] in Pow2BaseProofs.v	jadep	2016-08-12
\| \| *	New and improved conversion proofs (final conditions proven, invariant step u...	jadep	2016-08-12
\| \|/ \|/\|
\| *	Don't take advantage of design flaws (auto with *)	Jason Gross	2016-08-11
\|/
*	merge	jadep	2016-08-11
\|\
* \|	Tweaks for 8.4 compatibility	jadep	2016-08-11
* \|	Removed old conversion cruft and fixed Testbit to fit new decode_bitwise proofs	jadep	2016-08-11
* \|	removed defunct lemmas/admits, proved helper function for conversion is correct	jadep	2016-08-10
\| *	Add ext_limb_widths_upper_bound	Jason Gross	2016-08-10
* \|	Made decode_bitwise proofs go away, and proved sane lemmas about Z.testbit (B...	jadep	2016-08-10
* \|	Convert defined and mostly proven, modulo several admitted lemmas about Z ope...	jadep	2016-08-09
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-25
\|\
* \|	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...	jadep	2016-07-25
\| *	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
\|/
*	Changed name of [carry_and_reduce_single] to [carry_single], since it does no...	jadep	2016-07-21
*	merge	jadep	2016-07-20
\|\
\| *	Remove stuff from 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
\|\\|
* \|	merge	jadep	2016-07-19
\|\ \
\| \| *	Add a lemma about base_from_limb_widths and app	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
\| \|/
* \|	changed base notation	jadep	2016-07-18