fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	map -> List.map (not Tuple.map)	Jason Gross	2016-09-29
*	Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...	jadep	2016-09-17
*	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
*	Finished sqrt in GF25519	jadep	2016-09-06
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...	jadep	2016-09-06
*	Added square roots to GF1305, started reworking freeze_opt in preparation for...	jadep	2016-08-31
*	Generalized exponentiation chains so inverse and square roots can use the sam...	jadep	2016-08-31
*	Removed some commented-out code that will probably not be needed.	jadep	2016-08-31
*	Changed definition of [sub] to require proof that the modulus multiple actual...	jadep	2016-08-25
*	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
*	Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6	jadep	2016-08-24
*	Added optimized [inv] operation to Specific, and removed dependencies on Modu...	jadep	2016-08-24
*	Shifted around some of the proofs in ModularBaseSystemField.v and propagated ...	jadep	2016-08-23
*	Merge of conversion development branch with master	jadep	2016-08-16
\|\
\| *	Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. Furt...	jadep	2016-08-16
* \|	Add length lemmas	Jason Gross	2016-08-12
\|/
*	Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci...	jadep	2016-08-09
*	Massively speed up construct_params (#48)	Jason Gross	2016-08-08
*	Fix 8.4 build.	jadep	2016-07-25
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-25
\|\
* \|	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...	jadep	2016-07-25
\| *	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
\|/
*	Fix 8.4{pl1,pl2} builds	jadep	2016-07-21
*	Changed name of [carry_and_reduce_single] to [carry_single], since it does no...	jadep	2016-07-21
*	Fixes #29	jadep	2016-07-21
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
*	merge	jadep	2016-07-20
\|\
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
\| *	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\|/
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
*	pushing through a tweak to the arguments of [sub], and defining a field over ...	jadep	2016-07-12
*	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
* \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08
\| *	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\| \|\
\| * \|	Factored out some proofs that rely only on base being powers of two, and defi...	jadep	2016-07-06
* \| \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
* \| \|	remove PseudoMersenneRep	Andres Erbsen	2016-07-03
\| \| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \|/ \|/\|
\| *	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
\|/
*	remove trailing whitespace from src/	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
*	changed representation definition to require digits vector to be the exact le...	jadep	2016-06-15
*	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
*	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