fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	reorganized lemmas; moved several to ListUtil and ZUtil.	Jade Philipoom	2015-11-24
*	ModularBaseSystem: added definition to perform a specific sequence of carries...	Jade Philipoom	2015-11-24
*	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
*	Added base_succ precondition to BaseSystem to help prove carrying.	Jade Philipoom	2015-11-19
*	ModularBaseSystem: proving reduce case of carry_rep.	Jade Philipoom	2015-11-18
*	ModularBaseSystem: carry_rep has boring modular arithmetic proofs	Andres Erbsen	2015-11-17
*	ModularBaseSystem: introduced lemmas about breaking lists; working on carry_r...	Jade Philipoom	2015-11-17
*	ModularBaseSystem.carry: implement, state lemmas, some progress on proofs	Andres Erbsen	2015-11-17
*	BaseSystem: finish first pass of prettifying proofs	Andres Erbsen	2015-11-11
*	BaseSystem: more prettyfication	Andres Erbsen	2015-11-10
*	ModularBaseSystem: Implemented and proved subtraction, completing implementat...	Jade Philipoom	2015-11-10
*	BaseSystem: implemented and proved subtraction.	Jade Philipoom	2015-11-10
*	ModularBaseSystem: implemented fromGF and proved correct, moved inline admits...	Jade Philipoom	2015-11-10
*	Merge of local changes and most recent changes in mit-plv master	Jade Philipoom	2015-11-10
\|\
* \|	BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ...	Jade Philipoom	2015-11-10
\| *	BaseSystem: more boring	Andres Erbsen	2015-11-10
\| *	BaseSystem: more hints, more boring	Andres Erbsen	2015-11-10
\|/
*	ModularBaseSystem: finished most admits for addition and multiplication, move...	Jade Philipoom	2015-11-09
*	ModularBaseSystem: proved addition and multiplication.	Jade Philipoom	2015-11-07
*	BaseSystem: removed confusing notations and added mul_length lemma (currently...	Jade Philipoom	2015-11-07
*	ModularBaseSystem: finish base_good	Andres Erbsen	2015-11-07
*	ModularBaseSystem: prove some admits in mase system extension	Andres Erbsen	2015-11-07
*	ModularBaseSystem: continuing to prove base_good.	Jade Philipoom	2015-11-07
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2015-11-06
\|\
* \|	Starting to prove base_good in ModularBaseSystem	Jade Philipoom	2015-11-06
\| *	Specific: PseudoMersenneBaseParams for GF25519Base25Point5.	Andres Erbsen	2015-11-06
\| *	Merge remote-tracking branch 'jadep/master'	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
* \|	ModularBaseSystem: finished proving all admits for reduce_rep; proved base_po...	Jade Philipoom	2015-11-05
* \|	Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem.	Jade Philipoom	2015-11-05
* \|	ModularBaseSystem: Implemented reduce and proved reduce_rep, currently workin...	Jade Philipoom	2015-11-05
* \|	ModularBaseSystem: defined an extended base system to represent unreduced pro...	Jade Philipoom	2015-11-04
* \|	Relocated boring tactic to ListUtil and added combine_truncate lemma.	Jade Philipoom	2015-11-04
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2015-11-03
\|\\|
\| *	set_nth_splice case coverage	Andres Erbsen	2015-11-03
\| *	more set_nth	Andres Erbsen	2015-11-03
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2015-11-03
\|\\|
\| *	set_nth	Andres Erbsen	2015-11-01
* \|	ModularBaseSystem skeleton	Andres Erbsen	2015-10-30
\| *	Beautified BinGF.splitWords	Adam Chlipala	2015-10-30
\| *	word bound propagation examples	Andres Erbsen	2015-10-30
\| *	BaseSystem to Util.ListUtil: separate out generic list lemmas	Andres Erbsen	2015-10-29
\| *	Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto	Andres Erbsen	2015-10-29
\| \|\
\| \| *	bingf	Robert Sloan	2015-10-29
\| * \|	Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto	Andres Erbsen	2015-10-29
\| \|\\|
\| * \|	remove resolved todo	Andres Erbsen	2015-10-28
\| * \|	remove SearchAbouts	Andres Erbsen	2015-10-28
* \| \|	BaseSystem: removed axiom b0_1.	Jade Philipoom	2015-10-28