fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	reduce admits related to point negation	Andres Erbsen	2016-06-22
*	Reorganization and revision of Encoding code and redefinition of sign_bit fun...	jadep	2016-06-22
*	point_eq_dec	Andres Erbsen	2016-06-22
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...	jadep	2016-06-22
*	automated most of the code in GF25519	jadep	2016-06-22
*	Cleanup of GF25519	jadep	2016-06-22
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-06-22
*	GF25519 addition	jadep	2016-06-22
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	jadep	2016-06-22
*	ed25519 derivation: down to final encoding	Andres Erbsen	2016-06-22
*	ed25519 derivation: use representation of F	Andres Erbsen	2016-06-22
*	ed25519 derivation: wrangle non-unique representations	Andres Erbsen	2016-06-22
*	ed25519 derivation: stuck at main loop	Andres Erbsen	2016-06-22
*	ed25519 derivation down to word until main equation	Andres Erbsen	2016-06-22
*	Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...	jadep	2016-06-22
*	Fixed syntax error (missing bracket) in Ed25519 to make merge build	jadep	2016-06-22
*	ed25519: continue derivation	Andres Erbsen	2016-06-22
*	Finished refactor of GF25519 (partial evaluation); code builds but needs to b...	jadep	2016-06-22
*	Merge and refactor of GF25519	jadep	2016-06-22
*	Drop second projections in Ed25519	Jason Gross	2016-06-22
*	fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams	Jade Philipoom	2016-06-22
*	ed25519 derivation: pair programming with jgross... slow progress	Andres Erbsen	2016-06-22
*	nicer verify() derivation starter	Andres Erbsen	2016-06-22
*	state top-level derivation for Ed25519.verify	Andres Erbsen	2016-06-22
*	Finish absolutizing imports	Jason Gross	2016-06-22
*	proved most of point encoding admits, fixed some build system issues (dead im...	Jade Philipoom	2016-06-22
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-06-22
*	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-06-22
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-06-22
*	EdDSA25519: progress on proving PointEncoding admits; code still unorganized	Jade Philipoom	2016-06-22
*	port several theorems from GF to F	Andres Erbsen	2016-06-22
*	remove a dangling About	Andres Erbsen	2016-06-22
*	removed lingering Check/SearchAbout statements	Jade Philipoom	2016-06-22
*	Specific/GF25519: factor out lemmas	Andres Erbsen	2016-06-22
*	Do some work pair-programming with Andres on opts	Jason Gross	2016-06-22
*	EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and th...	Jade Philipoom	2016-06-22
*	PointFOrmats,EdDSA: remove redundant axioms	Andres Erbsen	2016-01-16
*	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
* \| \|	simple refactor of makefile; comments	varomodt	2016-01-09
\| \|/ \|/\|
* \|	Merge branch 'specific-rewrite'	Andres Erbsen	2016-01-06
\|\ \ \| \|/ \|/\|
\| *	fix letify to only insert a term once	Andres Erbsen	2016-01-06
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-01-05
\|\ \
* \| \|	Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...	Jade Philipoom	2016-01-05
\| * \|	remove comment	Andres Erbsen	2016-01-04
\|/ /
\| *	prettier GF25519 derivation that runs out of memory	Andres Erbsen	2016-01-04
\| *	UNTESTED simplification of specific GF25519 derivation	Andres Erbsen	2016-01-02
\|/
*	Remove redundancy in lemma statement	Adam Chlipala	2015-12-09
*	Specific/GF25519: explicit formula for multiplication	Andres Erbsen	2015-12-05