fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
*	make 8.4 happier	jadep	2016-09-06
*	Finished sqrt in GF25519	jadep	2016-09-06
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...	jadep	2016-09-06
*	updated GF25519 to match new exponentiation chain code	jadep	2016-08-31
*	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
*	Added optimized [inv] operation to Specific, and removed dependencies on Modu...	jadep	2016-08-24
*	Speed up src/Specific/GF25519.v (#54)	Jason Gross	2016-08-18
*	Updated GF files to reflect change in [repeat]	jadep	2016-08-16
*	Merge of conversion development branch with master	jadep	2016-08-16
\|\
\| *	Added specific versions of [pack] and [unpack] to GF25519	jadep	2016-08-16
\|/
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
*	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