fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Add Pseudize, Vectorize, Wordize to the build process	Robert Sloan	2016-06-22
*	Make Assembly modules 8.5-compatible	Robert Sloan	2016-06-22
*	Merge with public master	Robert Sloan	2016-06-22
\|\
\| *	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\| *	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\| *	Fix missing notations	Jason Gross	2016-06-22
\| *	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| *	Fix for broken abstract	Jason Gross	2016-06-22
* \|	Replace NPeano -> Nat in src/Spec/EdDSA	Robert Sloan	2016-06-22
\| *	Add decidability util file	Jason Gross	2016-06-22
\| *	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
* \|	Merge with plv/master	Robert Sloan	2016-06-22
\|\\|
* \|	Merging Pipeline.v	Robert Sloan	2016-06-22
\|\ \
* \ \	squash commits + revert makefile	Robert Sloan	2016-06-22
\|\ \ \
* \| \| \|	Fix build process	Robert Sloan	2016-06-22
* \| \| \|	Full automation for relevant parts of pseudo conversion except lets	Robert Sloan	2016-06-22
* \| \| \|	Reorganization of wordize.v	Robert Sloan	2016-06-22
* \| \| \|	Merging wordization and bounding together in Wordize.v	Robert Sloan	2016-06-22
* \| \| \|	Really complex derivation of wand correctness	Robert Sloan	2016-06-22
* \| \| \|	Proper word-based vectorization	Robert Sloan	2016-06-22
* \| \| \|	ed25519: indentation fix	Andres Erbsen	2016-06-22
* \| \| \|	ed25519: integrate FRepPow and FRepInv	Andres Erbsen	2016-06-22
* \| \| \|	ed25519: continue refactor	Andres Erbsen	2016-06-22
* \| \| \|	PrimeFieldTheorems fermat inverse lemma: prove admit	Andres Erbsen	2016-06-22
* \| \| \|	Factor some rewrites into a single [autorewrite]	Jason Gross	2016-06-22
* \| \| \|	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-06-22
* \| \| \|	Fix some issues in Ed25519 tactics	Jason Gross	2016-06-22
* \| \| \|	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...	Andres Erbsen	2016-06-22
* \| \| \|	F: pow_nat_iter_op_correct	Andres Erbsen	2016-06-22
* \| \| \|	F: fermat inversion lemma refactor	Andres Erbsen	2016-06-22
* \| \| \|	unifiedAddM1Rep_sig: almost there	Andres Erbsen	2016-06-22
* \| \| \|	slightly nicer edwards curve extended coordinates addition	Andres Erbsen	2016-06-22
* \| \| \|	Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ...	jadep	2016-06-22
* \| \| \|	First stage of canonicalization proofs complete; proved 3 carry loops reduce ...	jadep	2016-06-22
* \| \| \|	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-06-22
* \| \| \|	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-06-22
* \| \| \|	Moved sign_bit definition to Spec.	jadep	2016-06-22
* \| \| \|	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-06-22
* \| \| \|	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...	jadep	2016-06-22
* \| \| \|	Completed encoding reorganization; factored sign_bit out of PointEncodings an...	jadep	2016-06-22
* \| \| \|	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-06-22
* \| \| \|	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-06-22
* \| \| \|	refactor field lemmas out of ed25519	Andres Erbsen	2016-06-22
* \| \| \|	reduce admits related to point negation	Andres Erbsen	2016-06-22
* \| \| \|	Reorganization and revision of Encoding code and redefinition of sign_bit fun...	jadep	2016-06-22
* \| \| \|	point_eq_dec	Andres Erbsen	2016-06-22
* \| \| \|	finished last cases of nonzero proofs for associativity	jadep	2016-06-22
* \| \| \|	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...	jadep	2016-06-22
* \| \| \|	automated most of the code in GF25519	jadep	2016-06-22
* \| \| \|	Cleanup of GF25519	jadep	2016-06-22