fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	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