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
\|\\|
\| *	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
\|\ \
\| \| *	Merge pull request #1 from plv/master	Robert Sloan	2015-11-02
\| \| \|\ \| \| \|/ \| \|/\|
\| * \|	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
* \| \|	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
\| * \|	Tiny module-system tweaks in PointFormats	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
\|\
* \|	fix the makefile to not rebuild + module renaming	Robert Sloan	2015-10-22
\| *	disable Curve25519 until PointFormats is parametric or we give up and retry	Andres Erbsen	2015-10-22
\| *	refactor pointformats to use have a module type of correct implementations	Andres Erbsen	2015-10-22
\|/
*	word equiv	Robert Sloan	2015-10-20
\|\
* \	word equiv	Robert Sloan	2015-10-20
\|\ \
* \| \|	word equiv	Robert Sloan	2015-10-20
\| \| *	Delete WordEquivalence.v	Robert Sloan	2015-10-19
\| \|/ \|/\|
\| *	Delete WordEquivalence.v	Robert Sloan	2015-10-19
\|/