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
\| *	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
* \|	starting rewrite using different definition of map	jadep	2016-06-11
\| *	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
\|\
\| *	PrimeFieldTheorems fermat inverse lemma: prove admit	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
\|/
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...	jadep	2016-05-09
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...	jadep	2016-04-28
*	refactor field lemmas out of ed25519	Andres Erbsen	2016-04-25
*	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
*	Add a tactic for field inequalities	Jason Gross	2016-04-19
*	Merge and refactor of GF25519	jadep	2016-04-11
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
\| *	Ed25519: d is nonsquare	Andres Erbsen	2016-03-20
* \|	made BaseVector instance global	Jade Philipoom	2016-03-20
* \|	refactor of Basesystem and ModularBaseSystem; includes general code organizat...	Jade Philipoom	2016-03-20
* \|	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-03-11
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\| *	Use [rewrite] rather than [change] to speed up Qed	Jason Gross	2016-03-08
\|/
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
*	Instance Fq_Integral_domain : @Integral_domain (F q) ...	Andres Erbsen	2016-02-28
*	Makefile: single-quotes for shell globbing	Andres Erbsen	2016-02-28
*	ModularArithmetic: reasonable-time FieldToZ inv implementation	Andres Erbsen	2016-02-26
*	efficient powmod	Andres Erbsen	2016-02-17
*	update ModularArithmetic tutorial	Andres Erbsen	2016-02-17
*	proved sqrt_solutions, the last remaining admit for point encodings	Jade Philipoom	2016-02-16
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...	Jade Philipoom	2016-02-16
*	proved most of point encoding admits, fixed some build system issues (dead im...	Jade Philipoom	2016-02-16
*	merge	Jade Philipoom	2016-02-15
\|\
* \|	moved two non-primality-dependent lemmas to ModularArithmeticTheorems from Pr...	Jade Philipoom	2016-02-15
\| *	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\|/
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec	Jade Philipoom	2016-02-15
\|\
* \|	added square roots and an assortment of lemmas about prime fields/rings	Jade Philipoom	2016-02-15
* \|	changed the name of the ring to ring, not field	Jade Philipoom	2016-02-15
\|/
*	update F Coercions and tutorial	Andres Erbsen	2016-02-14
*	prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Cl...	Andres Erbsen	2016-02-13
*	implement F_opp	Andres Erbsen	2016-02-12
*	document field issue re-appearing	Andres Erbsen	2016-02-12
*	port some edwards curve theorems	Andres Erbsen	2016-02-12
*	make field on F automatically clean up the constant-vomit it expands	Andres Erbsen	2016-02-11