fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Merge	jadep	2016-06-14
\|\
* \|	Finished admits for canonicalization proofs.	jadep	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
\| *	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
\|/
*	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
\| *	F: pow_nat_iter_op_correct	Andres Erbsen	2016-05-18
\| *	F: fermat inversion lemma refactor	Andres Erbsen	2016-05-18
\| *	unifiedAddM1Rep_sig: almost there	Andres Erbsen	2016-05-18
\| *	slightly nicer edwards curve extended coordinates addition	Andres Erbsen	2016-05-18
\|/
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
*	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-04-29
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...	jadep	2016-04-28
*	Completed encoding reorganization; factored sign_bit out of PointEncodings an...	jadep	2016-04-28
*	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-04-25
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-25
\|\
* \|	Reorganization and revision of Encoding code and redefinition of sign_bit fun...	jadep	2016-04-25
\| *	refactor field lemmas out of ed25519	Andres Erbsen	2016-04-25
\| *	reduce admits related to point negation	Andres Erbsen	2016-04-25
\|/
*	point_eq_dec	Andres Erbsen	2016-04-22
*	finished last cases of nonzero proofs for associativity	jadep	2016-04-21
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...	jadep	2016-04-21
*	automated most of the code in GF25519	jadep	2016-04-21
*	Cleanup of GF25519	jadep	2016-04-20
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-04-20
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
*	GF25519 addition	jadep	2016-04-20
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	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