fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
*	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
*	Fixed unsimplified multiplication definitions in Specific by separating out t...	jadep	2016-07-18
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
*	re-cleaned operations in Specific and updated GF25519 to match GF1305	jadep	2016-07-12
*	pushing through a tweak to the arguments of [sub], and defining a field over ...	jadep	2016-07-12
*	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
*	GF25519: quiet	Andres Erbsen	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
* \|	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
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...	jadep	2016-06-15
* \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
\| *	ed25519: refactor some Proper	Andres Erbsen	2016-06-06
\|/
*	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...	Andres Erbsen	2016-05-24
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	automated most of the code in GF25519	jadep	2016-04-21
*	Cleanup of GF25519	jadep	2016-04-20
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-04-20
*	GF25519 addition	jadep	2016-04-20
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	jadep	2016-04-20
*	Finished refactor of GF25519 (partial evaluation); code builds but needs to b...	jadep	2016-04-12
*	Merge and refactor of GF25519	jadep	2016-04-11
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
* \|	fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams	Jade Philipoom	2016-03-20
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\|/
*	proved most of point encoding admits, fixed some build system issues (dead im...	Jade Philipoom	2016-02-16
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-02-14
*	remove a dangling About	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
*	simple refactor of makefile; comments	varomodt	2016-01-09
*	fix letify to only insert a term once	Andres Erbsen	2016-01-06
*	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
*	GF25519: synthesize explicit formula for multiplication (no reduction yet)	Andres Erbsen	2015-12-05
*	Specific/GF25519: Updated to match new PseudoMersenneBaseParams spec.	Jade Philipoom	2015-11-24
*	ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ca...	Jade Philipoom	2015-11-20
*	BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ...	Jade Philipoom	2015-11-10
*	ModularBaseSystem: finish base_good	Andres Erbsen	2015-11-07
*	ModularBaseSystem: prove some admits in mase system extension	Andres Erbsen	2015-11-07
*	Specific: PseudoMersenneBaseParams for GF25519Base25Point5.	Andres Erbsen	2015-11-06
*	instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)	Andres Erbsen	2015-11-06
*	src/Specific/GF25519.v: more complicated example for BaseSystem	Andres Erbsen	2015-11-05