fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
\| *	move nsatz into tactics directory	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
\| *	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
\| *	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	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
\| *	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
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-19
\|\
\| *	Add a tactic for field inequalities	Jason Gross	2016-04-19
\| \| \| \| \| \| \| \| \| \|	Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
* \|	Cleaned up and revised DoubleAndAdd.	jadep	2016-04-15
\| \|
* \|	Removed old iter_op version and its last dependency.	jadep	2016-04-15
\|/
*	Retrieved updated version of Util/IterAssocOp and modified ↵	jadep	2016-04-14
\| \| \| \|	ExtendedCoordinates and Ed25519 to use it.
*	extended coordinates setoid boilerplate	Andres Erbsen	2016-03-20
\|
*	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Remove [Admitted]; [Qed] is now under a second	Jason Gross	2016-03-08
\|
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
\|
*	ModularArithmetic: [field] tactic that respects opacity, prettify ↵	Andres Erbsen	2016-02-28
\| \| \| \|	ExtendedCoordinates, outline Edwards curve associativity
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵	Jade Philipoom	2016-02-16
\| \| \| \|	CompleteEdwardsCurve, where the precondition is not in scope.
*	cleaned up and ported definition to solve for x ^ 2 in the curve equation	Jade Philipoom	2016-02-16
\|
*	remove Check	Andres Erbsen	2016-02-15
\|
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec	Jade Philipoom	2016-02-15
\|\
* \|	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15
\| \|
\| *	port bounded iter_op and Edwards doubleAndAdd	Andres Erbsen	2016-02-15
\| \|
\| *	CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context	Andres Erbsen	2016-02-15
\|/
*	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-02-13
\|
*	workaround field with typeclass modulus	Andres Erbsen	2016-02-12
\|
*	fix imports	Andres Erbsen	2016-02-12
\|
*	document field issue re-appearing	Andres Erbsen	2016-02-12
\|
*	port some edwards curve theorems	Andres Erbsen	2016-02-12