fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| \| * \|	Removed old iter_op version and its last dependency.	jadep	2016-04-15
\| \| \|/
* \| \|	Breaking out State into its own file	Robert Sloan	2016-04-04
\| \| *	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\| \| \|\
* \| \| \|	add Assembly to CoqProject	Robert Sloan	2016-03-29
* \| \| \|	merge with plv/master	Robert Sloan	2016-03-29
\| \|_\|/ \|/\| \|
* \| \|	state top-level derivation for Ed25519.verify	Andres Erbsen	2016-03-20
\| \| *	refactor of Basesystem and ModularBaseSystem; includes general code organizat...	Jade Philipoom	2016-03-20
\| \|/ \|/\|
* \|	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
* \|	ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...	Andres Erbsen	2016-02-28
* \|	generic binary exponentiation correctness proof in 3 one-liners	Andres Erbsen	2016-02-26
* \|	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\|/
*	proved most of point encoding admits, fixed some build system issues (dead im...	Jade Philipoom	2016-02-16
*	added point encodings; some admits remain	Jade Philipoom	2016-02-16
*	fixed renamed files and added imports for encodings	Jade Philipoom	2016-02-15
*	merge	Jade Philipoom	2016-02-15
\|\
* \|	added generic encoding spec	Jade Philipoom	2016-02-15
\| *	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\|/
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec	Jade Philipoom	2016-02-15
\|\
* \|	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15
\| *	port bounded iter_op and Edwards doubleAndAdd	Andres Erbsen	2016-02-15
\| *	CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context	Andres Erbsen	2016-02-15
\|/
*	Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v	Andres Erbsen	2016-02-13
*	port some edwards curve theorems	Andres Erbsen	2016-02-12
*	Define F m, a replacement for GF with several benefits.	Andres Erbsen	2016-02-11
*	Update build process to use COQPATH & _CoqProject	Jason Gross	2016-02-05
*	simple refactor of makefile; comments	varomodt	2016-01-09
*	Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...	Jade Philipoom	2016-01-05
*	Code-reviewing EdDSA	Adam Chlipala	2015-12-29
*	reorganized lemmas; moved several to ListUtil and ZUtil.	Jade Philipoom	2015-11-24
*	ModularBaseSystem.carry: implement, state lemmas, some progress on proofs	Andres Erbsen	2015-11-17
*	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
\|/
*	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
\|\
\| *	patches for galois	Robert Sloan	2015-10-27
* \|	positional number system equivalence transcribed from pencil-and-paper proofs...	Andres Erbsen	2015-10-25
\|/
*	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
*	gfPlus abstraction	Robert Sloan	2015-10-16
*	make ring decidable + define constants	Robert Sloan	2015-09-19
*	makefile dependency order	Andres Erbsen	2015-09-18
*	Curves: elliptic curve point format record declarations and some invariants	Andres Erbsen	2015-09-18
*	import VerdiTactics	Andres Erbsen	2015-09-17
*	redo module structure + init curve25519	Robert Sloan	2015-09-16
*	init our centralized repo	Robert Sloan	2015-09-10