fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
*	Fix 8.6 build	Jason Gross	2016-07-26
*	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
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-20
\|\
* \	merge	jadep	2016-07-20
\|\ \
\| \| *	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
\| \|/
\| *	Don't use auto with *	Jason Gross	2016-07-20
\| *	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\| *	Work around bad design in Coq	Jason Gross	2016-07-19
\| *	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
* \|	merge	jadep	2016-07-19
\|\\|
* \|	Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.	jadep	2016-07-19
\| *	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\| *	Move more proofs earlier	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
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ...	jadep	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
\|\
* \|	added a few length proofs to ModularBaseSystemProofs to help with tuple conve...	jadep	2016-07-08
\| *	Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.	jadep	2016-07-07
\| *	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
* \| \|	add new interface to ModularBaseSystem	Andres Erbsen	2016-07-03
\| \| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \|/ \|/\|
\| *	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\| *	encode operation in ModularBaseSystem now uses bitwise operators, taking adva...	jadep	2016-06-29
\| *	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
\|/
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	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
*	Merge	jadep	2016-06-14
\|\
* \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
* \|	reversed modulus_digits and proved a few admits	jadep	2016-06-13
* \|	progress on second stage (conditional constant-time subtraction) of canonical...	jadep	2016-06-13
\| *	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
* \|	starting rewrite using different definition of map	jadep	2016-06-11
\|/
*	First stage of canonicalization proofs complete; proved 3 carry loops reduce ...	jadep	2016-05-20
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...	jadep	2016-04-28
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
*	Merge and refactor of GF25519	jadep	2016-04-11
*	made BaseVector instance global	Jade Philipoom	2016-03-20
*	refactor of Basesystem and ModularBaseSystem; includes general code organizat...	Jade Philipoom	2016-03-20