fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
*	proved an admit in field homomorphisms that turned out to be unprovable; I ad...	jadep	2016-07-15
*	s/conservative_common_denominator/common_denominator/g	Andres Erbsen	2016-07-11
*	remove field_algebra	Andres Erbsen	2016-07-11
*	port CompleteEdwardsCurveTheorems (builds again)	Andres Erbsen	2016-07-11
*	pose proof fails where specialize works (typeclass resolution / unification?)	Andres Erbsen	2016-07-11
*	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
*	added proofs about addition chain exponentiation for later use in ModularBase...	jadep	2016-07-10
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-06-27
\|\
\| *	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
* \|	update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file	jadep	2016-06-25
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_port	jadep	2016-06-24
\|\\|
* \|	merging point encoding port	jadep	2016-06-24
\|\ \
* \| \|	Ported PointEncodings to parameterize over field rather than modulus.	jadep	2016-06-24
\| \| *	Remove a useless intro	Jason Gross	2016-06-24
\| \|/
\| *	ExtendedCoordinates: group.	Andres Erbsen	2016-06-24
\| *	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| *	Pseudize Let_In	Robert Sloan	2016-06-23
\| *	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\| *	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| *	Use Admitted, not Qed, when a proof has admit	Jason Gross	2016-06-21
\| *	Fix [Proper_add] in 8.5	Jason Gross	2016-06-21
\| *	Make [bash] tactic easier to debug	Jason Gross	2016-06-21
\| *	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
\| *	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\| *	move nsatz into tactics directory	Andres Erbsen	2016-06-20
\| *	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
\| *	tuple tooling	Andres Erbsen	2016-06-20
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| *	edwards curve addition respects field homomorphism	Andres Erbsen	2016-06-16
\| *	prove ring admits	Andres Erbsen	2016-06-16
\| *	edwards curve preliminaries: replace oncurve proof with nsatz	Andres Erbsen	2016-06-16
\| *	nsatz: reimplement, integrate, demonstrate	Andres Erbsen	2016-06-15
\| *	refactor nsatz wrappers into algebra file	Andres Erbsen	2016-06-14
\| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
\| *	stuck because overloading-by-typeclasses sucks	Andres Erbsen	2016-06-13
* \|	Minor 8.5 changes	Jason Gross	2016-06-10
* \|	More changes for 8.5	Jason Gross	2016-06-10
\| *	generic field definition	Andres Erbsen	2016-06-07
\| *	ERep add	Andres Erbsen	2016-05-29
\| *	verify derivation: EdDSA layer	Andres Erbsen	2016-05-28
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	slightly nicer edwards curve extended coordinates addition	Andres Erbsen	2016-05-18
*	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-04-25
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
*	point_eq_dec	Andres Erbsen	2016-04-22
*	finished last cases of nonzero proofs for associativity	jadep	2016-04-21