fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Fix _CoqProject	Jason Gross	2016-09-05
*	Remove ReifyDirect	Jason Gross	2016-09-05
*	A helper lemma for [Wf]	Jason Gross	2016-09-05
*	PHOAS syntax	Jason Gross	2016-09-05
*	Add a file about pointed Props	Jason Gross	2016-09-05
*	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
*	Integrate suggestions from Andres	Jason Gross	2016-08-25
*	Rework bounded proofs	Jason Gross	2016-08-24
*	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\|\
\| *	Removed now-obsolete ModularBaseSystemField.v; field lemmas for ModularBaseSy...	jadep	2016-08-24
* \|	Update _CoqProject	Jason Gross	2016-08-23
* \|	Hook up the bounded interface, finish proofs	Jason Gross	2016-08-23
* \|	Initial work on an architecture interface for ℤ/nℤ	Jason Gross	2016-08-23
\|/
*	Specify a type of bounded integers for mod arith	Jason Gross	2016-08-09
*	Define Montgomery reduction / multiplication on Z (#42)	Jason Gross	2016-08-05
*	Implement Barrett Reduction following HAC 14.42 (#45)	Jason Gross	2016-08-04
*	Add a generalized version of Barrett Reduction (#44)	Jason Gross	2016-08-04
*	Add ZUtil lemmas, and Util.Bool	Jason Gross	2016-08-03
*	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