fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
*	Update _CoqProject	Jason Gross	2016-06-23
*	Remove vestigal BoundedWord machinery	Robert Sloan	2016-06-23
*	Update _CoqProject	Robert Sloan	2016-06-23
*	Remove unstable Pipeline.v examples from _CoqProject	Robert Sloan	2016-06-23
*	Add Language.v, Conversion.v to _CoqProject	Robert Sloan	2016-06-23
*	Add Pseudize, Vectorize, Wordize to the build process	Robert Sloan	2016-06-22
*	Merge with public master	Robert Sloan	2016-06-22
\|\
\| *	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| *	Update _CoqProject	Jason Gross	2016-06-22
* \|	Merge with plv/master	Robert Sloan	2016-06-22
\|\\|
\| *	move nsatz into tactics directory	Andres Erbsen	2016-06-20
\| *	remove obsolete rep mechanism	Andres Erbsen	2016-06-20
\| *	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
\| *	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\| \|\
\| \| *	tuple tooling	Andres Erbsen	2016-06-20
\| \| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
\| \| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \| *	nsatz: reimplement, integrate, demonstrate	Andres Erbsen	2016-06-15
\| \| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
\| * \|	Add coqprime that works with 8.5, bundle bedrock	Jason Gross	2016-06-10
\| \| *	generic field definition	Andres Erbsen	2016-06-07
\| \|/
* \|	Meshing Assembly machinery into the Makefile	Robert Sloan	2016-06-06
* \|	merging with master	Robert Sloan	2016-06-06
\|\\|
* \|	merging with master	Robert Sloan	2016-06-06
\|\ \
* \| \|	PseudoMedialConversion done	Robert Sloan	2016-05-31
\| \| *	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...	Andres Erbsen	2016-05-24
\| \| *	Completed encoding reorganization; factored sign_bit out of PointEncodings an...	jadep	2016-04-28
\| \| *	Reorganization and revision of Encoding code and redefinition of sign_bit fun...	jadep	2016-04-25
\| \| *	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...	jadep	2016-04-21
\| \| *	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-04-20
\| \| *	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-19
\| \| \|\
\| \| * \|	Defined a testbit variant for BaseSystem vectors and proved equivalence to Z....	jadep	2016-04-19
\| \| \| *	Add a tactic for field inequalities	Jason Gross	2016-04-19
\| \| * \|	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