fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| * \|	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
*	pull changes from desktop	Robert Sloan	2015-10-19
*	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
*	Small PointFormats tweaks while reading through	Adam Chlipala	2015-10-12
*	comment out edwards<->montgomery conversion	Andres Erbsen	2015-10-08
*	refactor point formats to use modules and prove some lemmas	Andres Erbsen	2015-10-07
*	Galois: add broken test	Andres Erbsen	2015-09-22
*	in case of not-on-curve points, extended coordinate addition and twisted coor...	Andres Erbsen	2015-09-21
*	montgomery ladder definition	Andres Erbsen	2015-09-21
*	remove broken code	Robert Sloan	2015-09-20
*	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
\|/
*	Curves: elliptic curve point format record declarations and some invariants	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
*	import VerdiTactics	Andres Erbsen	2015-09-17
*	Removed dependency on proof irrelevance (it turns out we had a redundant exis...	Adam Chlipala	2015-09-17