fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \| \|	changed representation definition to require digits vector to be the exact le...	jadep	2016-06-15
* \| \|	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
\| * \|	Add .mailmap	Jason Gross	2016-06-15
\| * \|	Update README so it's good for both github.com and github.mit.edu	Jason Gross	2016-06-15
\|/ /
* \|	Merge	jadep	2016-06-14
\|\ \
* \| \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \| *	refactor nsatz wrappers into algebra file	Andres Erbsen	2016-06-14
\| \| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
* \| \|	reversed modulus_digits and proved a few admits	jadep	2016-06-13
* \| \|	progress on second stage (conditional constant-time subtraction) of canonical...	jadep	2016-06-13
\| \| *	stuck because overloading-by-typeclasses sucks	Andres Erbsen	2016-06-13
\| \| *	indent	Andres Erbsen	2016-06-12
\| * \|	Another fix for an anomaly in 8.4pl2	Jason Gross	2016-06-11
\| * \|	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
\| * \|	Fix for Coq 8.4pl2	Jason Gross	2016-06-11
\| * \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
* \| \|	starting rewrite using different definition of map	jadep	2016-06-11
\| * \|	Minor 8.5 changes	Jason Gross	2016-06-10
\| * \|	More changes for 8.5	Jason Gross	2016-06-10
\| * \|	8.5 fixes	Jason Gross	2016-06-10
\| * \|	Set Asymmetric Patterns	Jason Gross	2016-06-10
\| * \|	Add coqprime that works with 8.5, bundle bedrock	Jason Gross	2016-06-10
\|/ /
\| *	improved generic field library	Andres Erbsen	2016-06-10
\| *	improve generic field library	Andres Erbsen	2016-06-10
\| *	experiment	Andres Erbsen	2016-06-07
\| *	generic field definition	Andres Erbsen	2016-06-07
\| *	ed25519: refactor some Proper	Andres Erbsen	2016-06-06
\| *	rewrite in Let_In binder by tactic	Andres Erbsen	2016-06-04
\| *	Let_In rewriting	Andres Erbsen	2016-06-03
\| *	leibniz equal version of topdown rewriting of sigma types: nicer	Andres Erbsen	2016-06-01
\| *	leibniz equal version of topdown rewriting of sigma types	Andres Erbsen	2016-06-01
\| *	E impl: proper morphisms are hard to dow without setoids	Andres Erbsen	2016-05-30
\| *	ERep add	Andres Erbsen	2016-05-29
\| *	--amend	Andres Erbsen	2016-05-28
\| *	verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep...	Andres Erbsen	2016-05-28
\| *	verify derivation, EdDSA layer: remove unused context variables	Andres Erbsen	2016-05-28
\| *	verify derivation: EdDSA layer	Andres Erbsen	2016-05-28
\| *	right after scalars to F l	Andres Erbsen	2016-05-27
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-05-25
\|\
* \|	Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ...	jadep	2016-05-25
\| *	ed25519: indentation fix	Andres Erbsen	2016-05-24
\| *	ed25519: integrate FRepPow and FRepInv	Andres Erbsen	2016-05-24
\| *	ed25519: continue refactor	Andres Erbsen	2016-05-24
\| *	PrimeFieldTheorems fermat inverse lemma: prove admit	Andres Erbsen	2016-05-24
\| *	Factor some rewrites into a single [autorewrite]	Jason Gross	2016-05-24
\| *	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-05-24
\| *	Fix some issues in Ed25519 tactics	Jason Gross	2016-05-24
\| *	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...	Andres Erbsen	2016-05-24
* \|	First stage of canonicalization proofs complete; proved 3 carry loops reduce ...	jadep	2016-05-20