fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Removed lingering print statement.	jadep	2016-07-21
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
*	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
*	Fixed unsimplified multiplication definitions in Specific by separating out t...	jadep	2016-07-18
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
*	re-cleaned operations in Specific and updated GF25519 to match GF1305	jadep	2016-07-12
*	cleaned Specific operations so they produce code without proof terms, and pro...	jadep	2016-07-12
*	pushing through a tweak to the arguments of [sub], and defining a field over ...	jadep	2016-07-12
*	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
*	defined some group operations, stated group lemma for tuple-based [add] (in t...	jadep	2016-07-08
*	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
*	GF25519: quiet	Andres Erbsen	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...	jadep	2016-06-15
* \|	Another fix for an anomaly in 8.4pl2	Jason Gross	2016-06-11
* \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
\| *	ed25519: refactor some Proper	Andres Erbsen	2016-06-06
\| *	rewrite in Let_In binder by tactic	Andres Erbsen	2016-06-04
\| *	Let_In rewriting	Andres Erbsen	2016-06-03
\| *	leibniz equal version of topdown rewriting of sigma types: nicer	Andres Erbsen	2016-06-01
\| *	leibniz equal version of topdown rewriting of sigma types	Andres Erbsen	2016-06-01
\| *	E impl: proper morphisms are hard to dow without setoids	Andres Erbsen	2016-05-30
\| *	ERep add	Andres Erbsen	2016-05-29
\| *	--amend	Andres Erbsen	2016-05-28
\| *	verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep...	Andres Erbsen	2016-05-28
\| *	verify derivation, EdDSA layer: remove unused context variables	Andres Erbsen	2016-05-28
\| *	verify derivation: EdDSA layer	Andres Erbsen	2016-05-28
\| *	right after scalars to F l	Andres Erbsen	2016-05-27
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	ed25519: indentation fix	Andres Erbsen	2016-05-24
*	ed25519: integrate FRepPow and FRepInv	Andres Erbsen	2016-05-24
*	ed25519: continue refactor	Andres Erbsen	2016-05-24
*	Factor some rewrites into a single [autorewrite]	Jason Gross	2016-05-24
*	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-05-24
*	Fix some issues in Ed25519 tactics	Jason Gross	2016-05-24
*	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...	Andres Erbsen	2016-05-24
*	unifiedAddM1Rep_sig: almost there	Andres Erbsen	2016-05-18
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
*	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-04-29
*	Completed encoding reorganization; factored sign_bit out of PointEncodings an...	jadep	2016-04-28
*	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-04-25
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-25
\|\
* \|	Reorganization and revision of Encoding code and redefinition of sign_bit fun...	jadep	2016-04-25
\| *	refactor field lemmas out of ed25519	Andres Erbsen	2016-04-25