fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
\|
*	Proved lingering lemmas in PointEncodingPre.	jadep	2016-07-06
\|
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
\| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
* \|	merging point encoding port	jadep	2016-06-24
\|\\|
* \|	Ported PointEncodings to parameterize over field rather than modulus.	jadep	2016-06-24
\| \|
\| *	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\| \|
\| *	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
*	Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ↵	jadep	2016-05-25
\| \| \| \|	reason I wasn't affected. Also updated the same file to use E module.
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
\|
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
\|
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	Completed encoding reorganization; factored sign_bit out of PointEncodings ↵	jadep	2016-04-28
\| \| \| \|	and finished encoding admits.
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
\|
*	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-04-25
\| \| \| \|	function.
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-02-16
	imports of PointFormats and Galois things)