fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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
*	ed25519 spec: small cleanup	Andres Erbsen	2016-07-21
\|
*	compute on [F q]!	Andres Erbsen	2016-07-20
\|
*	experiments wd25519: simplify proof for a	Andres Erbsen	2016-07-20
\|
*	Remove a nested proof	Jason Gross	2016-07-18
\| \| \| \| \|	Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated]
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
\|
*	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
	- PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway