fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	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
\| \|\ \| \|/ \|/\|
* \|	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
\|\\|
* \|	ModularBaseSystem skeleton	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
\| \|\
\| * \|	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
\| \| *	patches for galois	Robert Sloan	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
\|/
*	add morphism-based field impl	Robert Sloan	2015-10-22
*	fix the makefile to not rebuild + module renaming	Robert Sloan	2015-10-22
*	pull changes from desktop	Robert Sloan	2015-10-19
*	pull changes from desktop	Robert Sloan	2015-10-19