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
* \|	Update _CoqProject	Jason Gross	2016-06-22
* \|	Add decidability util file	Jason Gross	2016-06-22
* \|	Flip the sense of the conditional in the makefile	Jason Gross	2016-06-22
* \|	Make Coq 8.5 the default target for Fiat-Crypto	Jason Gross	2016-06-22
* \|	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
* \|	Add coq-scripts submodule for timing scripts	Jason Gross	2016-06-22
* \|	Also build with Coq 8.5 on travis	Jason Gross	2016-06-22
\| *	Merge with plv/master	Robert Sloan	2016-06-22
\| \|\ \| \|/ \|/\|
\| *	Revert makefile to 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
\| * \| \|	Meshing Assembly machinery into the Makefile	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
\| * \| \|	removed subtraction from todo	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
\| * \| \|	remove line from todo	Andres Erbsen	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