fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	Merge pull request #52 from JasonGross/bounded-interface	Jason Gross	2016-08-25
\|\
\| *	Integrate suggestions from Andres	Jason Gross	2016-08-25
* \|	Changed definition of [sub] to require proof that the modulus multiple actual...	jadep	2016-08-25
* \|	Proper proofs for all ModularBaseSystem operations except [sub]	jadep	2016-08-24
* \|	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
\| *	Rework bounded proofs	Jason Gross	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	More zarith	Jason Gross	2016-08-24
* \|	Add more reserved notations	Jason Gross	2016-08-24
* \|	Fewer side-conditions on zsimplify	Jason Gross	2016-08-24
\| *	More slight cleanups	Jason Gross	2016-08-24
\| *	Clean up DoubleBounded	Jason Gross	2016-08-24
* \|	Added rewrite hints for two ListUtil lemmas	jadep	2016-08-24
* \|	Moved a tactic to Util/Tactics.v	jadep	2016-08-24
* \|	Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6	jadep	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	Fix a typo	Jason Gross	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	Add map_cons from Coq 8.6	Jason Gross	2016-08-24
\| *	Coq 8.4 fixes	Jason Gross	2016-08-24
* \|	Merge branch 'fast-inverse'	jadep	2016-08-24
\|\ \
\| * \|	Removed now-obsolete ModularBaseSystemField.v; field lemmas for ModularBaseSy...	jadep	2016-08-24
\| * \|	Added optimized [inv] operation to Specific, and removed dependencies on Modu...	jadep	2016-08-24
\| \| *	Weaken the condition on smaller_bound	Jason Gross	2016-08-23
\| \| *	Hook up the bounded interface, finish proofs	Jason Gross	2016-08-23
\| \| *	Revert "Add _valid properties"	Jason Gross	2016-08-23
\| \| *	Add _valid properties	Jason Gross	2016-08-23
\| \| *	Fix some things	Jason Gross	2016-08-23
\| \| *	Add TODO	Jason Gross	2016-08-23
\| \| *	Rework interface to support rewriting database	Jason Gross	2016-08-23
\| \| *	alternative machine interface specification proposal	Andres Erbsen	2016-08-23
\| \| *	Initial work on an architecture interface for ℤ/nℤ	Jason Gross	2016-08-23
\| \|/ \|/\|
* \|	remove eq_dec from Monoid	Andres Erbsen	2016-08-23
* \|	Fix a Hint Resolve typo	Jason Gross	2016-08-23
* \|	More ZUtil	Jason Gross	2016-08-23
* \|	More ZUtil	Jason Gross	2016-08-23
\| *	Shifted around some of the proofs in ModularBaseSystemField.v and propagated ...	jadep	2016-08-23
\| *	Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing plac...	jadep	2016-08-23
\| *	Updated AdditionChainExponentiation.v such that the exponentiation correctnes...	jadep	2016-08-23
\| *	fast-inverse rebase	jadep	2016-08-22
\|/
*	Proved homomorphism between ModularBaseSystem field and F q	jadep	2016-08-22
*	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
* \|	ListUtil.v : new proofs about sum_firstn for lists with nonnegative elements	jadep	2016-08-21
\| *	Add Z.rewrite_mod_small	Jason Gross	2016-08-19
\| *	More powerful Z.div_mod_to_quot_rem	Jason Gross	2016-08-19
\| *	More ZUtil	Jason Gross	2016-08-18
\| *	Add ZUtil	Jason Gross	2016-08-18
\| *	Add a ZUtil hint	Jason Gross	2016-08-18