fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	move nsatz into tactics directory	Andres Erbsen	2016-06-20
\|
*	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
\|
*	GF25519: quiet	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
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| \|
\| *	port EdDSA spec	Andres Erbsen	2016-06-20
\| \|
\| *	tuple tooling	Andres Erbsen	2016-06-20
\| \|
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵	Andres Erbsen	2016-06-18
\| \| \| \| \| \| \| \|	fewer nonzero ports. remove FField and FNsatz
* \|	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
\| \|
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \|
\| *	Z is integral domain	Andres Erbsen	2016-06-16
\| \|
\| *	port edwards curve spec	Andres Erbsen	2016-06-16
\| \|
\| *	edwards curve addition respects field homomorphism	Andres Erbsen	2016-06-16
\| \|
\| *	algebra: add homomorphisms	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
\| \|
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵	jadep	2016-06-15
\| \| \| \| \| \| \| \|	base-length digit vectors)
* \|	changed representation definition to require digits vector to be the exact ↵	jadep	2016-06-15
\| \| \| \| \| \| \| \|	length of the base vector
* \|	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
\| \|
* \|	Merge	jadep	2016-06-14
\|\ \
* \| \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \| \|
\| \| *	refactor nsatz wrappers into algebra file	Andres Erbsen	2016-06-14
\| \| \|
\| \| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
\| \| \|
* \| \|	reversed modulus_digits and proved a few admits	jadep	2016-06-13
\| \| \|
* \| \|	progress on second stage (conditional constant-time subtraction) of ↵	jadep	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \|	canonicalization proofs
\| \| *	stuck because overloading-by-typeclasses sucks	Andres Erbsen	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Using typeclasses for overloading clutters all users of the typeclass with an extra layer of indirection that would need to be unfolded in all proofs. Condemning all downstream Ltac to handling a new layer of definitions that have no semantic dignificance is suboptimal design (and encourages even worse design decisions like unfolding during rewriting). Overloading should be fully resolved during type inference, the resulting code must not be distinguishable from having the overloading resolved manually before entering the code.
\| \| *	indent	Andres Erbsen	2016-06-12
\| \| \|
\| * \|	Another fix for an anomaly in 8.4pl2	Jason Gross	2016-06-11
\| \| \|
\| * \|	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
\| \| \|
\| * \|	Fix for Coq 8.4pl2	Jason Gross	2016-06-11
\| \| \|
\| * \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev)
* \| \|	starting rewrite using different definition of map	jadep	2016-06-11
\| \| \|
\| * \|	Minor 8.5 changes	Jason Gross	2016-06-10
\| \| \|
\| * \|	More changes for 8.5	Jason Gross	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \|	[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
\| * \|	8.5 fixes	Jason Gross	2016-06-10
\|/ /
\| *	improved generic field library	Andres Erbsen	2016-06-10
\| \|
\| *	improve generic field library	Andres Erbsen	2016-06-10
\| \|
\| *	experiment	Andres Erbsen	2016-06-07
\| \|
\| *	generic field definition	Andres Erbsen	2016-06-07
\| \|
\| *	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
\| \|