fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Merge pull request #49 from JasonGross/bounded-z-like	Jason Gross	2016-08-10
\|\
* \|	Add [especialize], [forward], [eforward]	Jason Gross	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
\| *	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
*	More ZUtil	Jason Gross	2016-08-09
*	Add tactics to simplify repeated conditions	Jason Gross	2016-08-09
*	More ZUtil	Jason Gross	2016-08-09
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
*	More ZUtil	Jason Gross	2016-08-09
*	zsimplify: Better support for existentials	Jason Gross	2016-08-08
*	Montgomery: Add a variant that does reduction through partial_reduce	Jason Gross	2016-08-08
*	Add lemma in 8.6 std lib to ListUtil for 8.4	Jason Gross	2016-08-08
*	More zarith hints	Jason Gross	2016-08-08
*	Massively speed up construct_params (#48)	Jason Gross	2016-08-08
*	Add a ListUtil lemma	Jason Gross	2016-08-08
*	Add ZUtil lemmas	Jason Gross	2016-08-08
*	Remove unnecessary pseudo notations (#47)	Rob Sloan	2016-08-08
*	Add erewrite_hyp tactics	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
\| *	[cbv beta] in the beginning of Obligation Tactic for 8.5	Andres Erbsen	2016-08-08
* \|	Deleted Conversion file (maybe temporarily, maybe not) because of conflict wi...	jadep	2016-08-07
* \|	Instantiated twisted [d] using ModularBaseSystem	jadep	2016-08-07
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-07
\|\ \
\| * \|	Handle [_ mod 0] in pull_Zmod	Jason Gross	2016-08-05
\| * \|	Add Z.mod_mod case to 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
\| * \|	Handle [((-_) mod n) mod n] in {push,pull}_Zmod	Jason Gross	2016-08-04
\| * \|	Implement Barrett Reduction following HAC 14.42 (#45)	Jason Gross	2016-08-04
\| * \|	Add a generalized version of Barrett Reduction (#44)	Jason Gross	2016-08-04
\| \| *	address code review comments	Andres Erbsen	2016-08-04
\| \| *	decidability hack	Andres Erbsen	2016-08-04
\| \| *	prove eqsig_eq using hprop in Decidable.v	Andres Erbsen	2016-08-04
\| \| *	Util.Equality on 8.4	Andres Erbsen	2016-08-04
\| \| *	prove an admit	Andres Erbsen	2016-08-04
\| \| *	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \|/
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-04
\|\\|
\| *	More zsimplify	Jason Gross	2016-08-03
\| *	Add some autogenerated zsimplify lemmas	Jason Gross	2016-08-03
\| *	Better Zmod manipulation	Jason Gross	2016-08-03
\| *	Remove Bool.absorption_andb Bool.absorption_orb, not present in < 8.4pl5	Jason Gross	2016-08-03