fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| *	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
\|\ \
\| * \|	Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. Furt...	jadep	2016-08-16
\| \| *	Add decode_shift_app	Jason Gross	2016-08-16
\| \|/ \|/\|
\| *	Instantiated conversion both to (pack) and from (unpack) another set of limb ...	jadep	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
* \|	Add length lemmas	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
\| \|/ \|/\|
\| *	Fix build for Coq < 8.6	Jason Gross	2016-08-12
\| *	Don't take advantage of design flaws (auto with *)	Jason Gross	2016-08-11
\|/
*	merge	jadep	2016-08-11
\|\
* \	Merge conversion development branch to give jgross better lemmas	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
\| \| *	Merge pull request #49 from JasonGross/bounded-z-like	Jason Gross	2016-08-10
\| \| \|\
\| * \| \|	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
\| \| * \|	Add ext_limb_widths_nonneg	Jason Gross	2016-08-10
\| \| * \|	Add carry_simple_sub	Jason Gross	2016-08-10
\| \| \| *	Work around bug #4165 (broken context) in 8.4	Jason Gross	2016-08-10
\| * \| \|	Made decode_bitwise proofs go away, and proved sane lemmas about Z.testbit (B...	jadep	2016-08-10
\| \| \| *	Remove unused code (still in vcs history, in case we want it later)	Jason Gross	2016-08-09
\| \| \| *	Specify a type of bounded integers for mod arith	Jason Gross	2016-08-09
\| \| \|/
\| \| *	Work around broken lia in 8.4	Jason Gross	2016-08-09
\| \| *	Add alternate form of Montgomery, which does better about bounds	Jason Gross	2016-08-09
\| \|/ \|/\|
* \|	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
\| *	Convert defined and mostly proven, modulo several admitted lemmas about Z ope...	jadep	2016-08-09
* \|	Montgomery: Add a variant that does reduction through partial_reduce	Jason Gross	2016-08-08
* \|	Massively speed up construct_params (#48)	Jason Gross	2016-08-08
* \|	ModularArithmetic: remove [demod], use [pull_Zmod] instead	Andres Erbsen	2016-08-08
* \|	Merge branch 'modular-arithmetic-refactor'	Andres Erbsen	2016-08-08
\|\ \ \| \|/ \|/\|
\| *	remove unused Z lemmas from ModularArithmeticTheorems	Andres Erbsen	2016-08-08
* \|	Handle [_ mod 0] in pull_Zmod	Jason Gross	2016-08-05
* \|	Fix a comment	Jason Gross	2016-08-05
* \|	Define Montgomery reduction / multiplication on Z (#42)	Jason Gross	2016-08-05
\| *	[F] has its own module now	Andres Erbsen	2016-08-05
* \|	Implement Barrett Reduction following HAC 14.42 (#45)	Jason Gross	2016-08-04