fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	update F Coercions and tutorial	Andres Erbsen	2016-02-14
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-02-14
*	Spec/EdDSA: comments, remove prehashing	Andres Erbsen	2016-02-13
*	Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v	Andres Erbsen	2016-02-13
*	prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Cl...	Andres Erbsen	2016-02-13
*	Merge branch 'master' into spec	Jade Philipoom	2016-02-13
\|\
\| *	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-02-13
* \|	implement F_opp	Andres Erbsen	2016-02-12
\| *	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-02-12
\| \|\ \| \|/ \|/\|
\| *	EdDSA25519: progress on proving PointEncoding admits; code still unorganized	Jade Philipoom	2016-02-12
* \|	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
* \|	make field on F automatically clean up the constant-vomit it expands	Andres Erbsen	2016-02-11
* \|	port some Edwards curve stuff from GF to F	Andres Erbsen	2016-02-11
* \|	port several theorems from GF to F	Andres Erbsen	2016-02-11
* \|	Define F m, a replacement for GF with several benefits.	Andres Erbsen	2016-02-11
* \|	fresh take at specifications using implicit arguments instead of module param...	Andres Erbsen	2016-02-07
* \|	remove a dangling About	Andres Erbsen	2016-02-07
\|/
*	removed lingering Check/SearchAbout statements	Jade Philipoom	2016-02-07
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-02-07
\|\
* \|	EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and th...	Jade Philipoom	2016-02-07
\| *	PointFormats: prove dangling admit	Andres Erbsen	2016-02-07
\| *	Specific/GF25519: factor out lemmas	Andres Erbsen	2016-02-07
\| *	Do some work pair-programming with Andres on opts	Jason Gross	2016-02-05
\| *	Update build process to use COQPATH & _CoqProject	Jason Gross	2016-02-05
* \|	GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. NumT...	Jade Philipoom	2016-02-02
\| *	recursive-build coqprime	Rob Sloan	2016-01-28
\| *	recursive-build coqprime	Rob Sloan	2016-01-28
* \|	ModualrBaseSystem: proved lingering admit in subtraction proof.	Jade Philipoom	2016-01-25
\|/
*	NumTheoryUtil: proved Fermat's Little Theorem.	Jade Philipoom	2016-01-23
*	NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.	Jade Philipoom	2016-01-23
*	Import coqprime; use it to prove Euler's criterion.	Jade Philipoom	2016-01-20
*	PointFOrmats,EdDSA: remove redundant axioms	Andres Erbsen	2016-01-16
*	remove duplicate axiom	Andres Erbsen	2016-01-16
*	PointFormats: extended coordinates equivalence proofs	Andres Erbsen	2016-01-16
*	remove fiat dependency	Andres Erbsen	2016-01-16
*	Merge pull request #2 from rsloan/master	Robert Sloan	2016-01-14
\|\
\| *	fix merge conflicts + PointFormats proofs	Robert Sloan	2016-01-14
\| \|\ \| \|/ \|/\|
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-01-13
\|\ \
* \| \|	euler's criterion reduced to fermat's little theorem and two lemmas about pri...	Jade Philipoom	2016-01-13
\| \| *	Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto	Rob Sloan	2016-01-11
\| \| \|\
\| \| * \|	simple tactic rule	Rob Sloan	2016-01-11
\| \| * \|	assumption lemmas in PointFormats	Rob Sloan	2016-01-11
\| \| \| *	assumption lemmas in PointFormats	varomodt	2016-01-11
\| \| \|/
\| \| *	simple refactor of makefile; comments	varomodt	2016-01-09
\| * \|	cleanup	Andres Erbsen	2016-01-08
\| \|/
\| *	PointFormats: factor out admits	Andres Erbsen	2016-01-08
\| *	PointFormats: no zero denominators in Edwards addition	Andres Erbsen	2016-01-08