fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fully qualify [Require]s	Jason Gross	2016-09-08
\| \| \| \|	This way they won't become ambiguous if we add new files
*	Removed lingering SearchAbout.	jadep	2016-08-31
\|
*	Updated AdditionChainExponentiation.v such that the exponentiation ↵	jadep	2016-08-23
\| \| \| \|	correctness is in terms of N rather than nat; this allows us to compute the correctness proof for large exponents.
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
	ModularBaseSystem [pow], which we need for sqrt and inversion.