fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
\| \| \| \|	We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5
*	EdDSA.v: resolve ambiguity based on ed25519.py	Andres Erbsen	2016-06-21
\|
*	Whitespace change	Jason Gross	2016-06-21
\|
*	Fix a missing mod resolution	Jason Gross	2016-06-21
\| \| \| \|	Apparently this only triggered in 8.4
*	NPeano.modulo became Nat.modulo in 8.5	Jason Gross	2016-06-21
\|
*	Import omega for 8.5	Jason Gross	2016-06-21
\|
*	Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5	Jason Gross	2016-06-21
\|
*	Use Admitted, not Qed, when a proof has admit	Jason Gross	2016-06-21
\| \| \| \| \| \| \| \|	[admit] is the same as [shelve] / [give_up] in Coq 8.5. Error: Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed. (in proof edwards_acurve_abelian_group)
*	Fix [Proper_add] in 8.5	Jason Gross	2016-06-21
\| \| \| \|	Not sure why eauto depth matters...
*	Make [bash] tactic easier to debug	Jason Gross	2016-06-21
\| \| \| \|	Now you don't have to copy/paste the [match goal with ... end].
*	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
\|
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	Algebra: change a aliasing definition into an aliasing lemma to appease ↵	Andres Erbsen	2016-06-20
\| \| \| \|	implicit argument resolution
*	parenthesize Ltac [constr:] arguments	Andres Erbsen	2016-06-20
\|
*	Fix nsatz_compute for 8.4	Jason Gross	2016-06-20
\|
*	More missing scopes for 8.5?	Jason Gross	2016-06-20
\|
*	More 8.5 fixes	Jason Gross	2016-06-20
\| \| \| \|	Changing scopes?
*	Variosu 8.5 fixes	Jason Gross	2016-06-20
\| \| \| \| \| \| \|	- nsatz/field seem to do less unfolding (need eauto with field_nonzero more) - intuition doesn't destruct things (need dintuition (8.5 only) or manual destruct)
*	Fix for Coq 8.4pl2	Jason Gross	2016-06-20
\|
*	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
\| \| \|