fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
*	ModualrBaseSystem: proved lingering admit in subtraction proof.	Jade Philipoom	2016-01-25
*	EdDSA: mostly-complete spec and preliminary structure.	Jade Philipoom	2015-12-12
*	reorganized lemmas; moved several to ListUtil and ZUtil.	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.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
*	BaseSystem: implemented and proved subtraction.	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
*	BaseSystem: removed confusing notations and added mul_length lemma (currently...	Jade Philipoom	2015-11-07
*	Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem.	Jade Philipoom	2015-11-05
*	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
\|\
\| *	BaseSystem to Util.ListUtil: separate out generic list lemmas	Andres Erbsen	2015-10-29
\| *	remove SearchAbouts	Andres Erbsen	2015-10-28
* \|	BaseSystem: removed axiom b0_1.	Jade Philipoom	2015-10-28
* \|	Merge branch 'master' into jade	Jade Philipoom	2015-10-28
\|\\|
* \|	BaseSystem: proved all admits.	Jade Philipoom	2015-10-28
\| *	Proof improvements in BaseSystem	Adam Chlipala	2015-10-28
* \|	Proved add_same_length lemma.	Jade Philipoom	2015-10-27
* \|	Multiply rep mostly proven, working on admits.	Jade Philipoom	2015-10-27
* \|	More work on proving linearity of multiply.	Jade Philipoom	2015-10-26
* \|	Modified to use formal preconditions for b0_1 and base_positive.	Jade Philipoom	2015-10-25
\| *	pos_pow_nat_pos	Andres Erbsen	2015-10-25
\| *	nth_tac	Andres Erbsen	2015-10-25
* \|	Merge branch 'base0_1' into jade	Jade Philipoom	2015-10-25
\|\ \
* \ \	Merge https://github.com/mit-plv/fiat-crypto into jade	Jade Philipoom	2015-10-25
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	base[0] = 1	Andres Erbsen	2015-10-25
\| \|/
\| *	slight refactoring of BaseSystem	Andres Erbsen	2015-10-25
* \|	progress on proving properties about multiplication in positional number system	Jade Philipoom	2015-10-25
* \|	progress on proving properties about multiplication in positional number system	Jade Philipoom	2015-10-25
\| *	bounds checks	Andres Erbsen	2015-10-25
\|/
*	positional number system equivalence transcribed from pencil-and-paper proofs...	Andres Erbsen	2015-10-25
*	primitive positional numeral system definition on top of Z	Andres Erbsen	2015-10-24