fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Add HProp, Isomorphism	Jason Gross	2016-07-29
*	Set Asymmetric Patterns, add util lemmas about sig	Jason Gross	2016-07-29
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-20
\|\
\| *	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
* \|	Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.	jadep	2016-07-19
\|/
*	Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s	Andres Erbsen	2016-07-13
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
\| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| *	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\| \|\
\| * \|	Factored out some proofs that rely only on base being powers of two, and defi...	jadep	2016-07-06
* \| \|	add new interface to ModularBaseSystem	Andres Erbsen	2016-07-03
\|/ /
\| *	Define the spec of Weierstrass curves (#6)	Jason Gross	2016-07-03
\| *	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
\|/
*	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