fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	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
* \| \|	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