fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	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
*	gfPlus abstraction	Robert Sloan	2015-10-16
*	Galois: add broken test	Andres Erbsen	2015-09-22
*	merge with master	Robert Sloan	2015-09-19
\|\
* \|	make ring decidable + define constants	Robert Sloan	2015-09-19
\| *	make `field` work when GaloisField and GaloisFieldTheory are imported at the ...	Andres Erbsen	2015-09-18
\|/
*	GaloisFieldTheory: add scope delimiter	Andres Erbsen	2015-09-18
*	GaloisFieldTheory: scoped notation that coincides with Z	Andres Erbsen	2015-09-18
*	overlflow-checking ZToGF function	Andres Erbsen	2015-09-17
*	Removed dependency on proof irrelevance (it turns out we had a redundant exis...	Adam Chlipala	2015-09-17
*	Beautified remaining GaloisFieldTheory proofs	Adam Chlipala	2015-09-17
*	Got most of the way through new GaloisField code	Adam Chlipala	2015-09-17
*	fix module structure + add assembly placeholder	Robert Sloan	2015-09-17
*	redo module structure + init curve25519	Robert Sloan	2015-09-16