fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	added a few length proofs to ModularBaseSystemProofs to help with tuple conve...	jadep	2016-07-08
* \|	unstuck carry_mul_opt_cps using from_list_default	jadep	2016-07-08
\| *	Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.	jadep	2016-07-07
\| *	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\| \|\
\| * \|	Factored out some proofs that rely only on base being powers of two, and defi...	jadep	2016-07-06
* \| \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
* \| \|	add new interface to ModularBaseSystem	Andres Erbsen	2016-07-03
* \| \|	remove PseudoMersenneRep	Andres Erbsen	2016-07-03
\| \| *	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
\| \| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \|/ \|/\|
\| *	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\| *	encode operation in ModularBaseSystem now uses bitwise operators, taking adva...	jadep	2016-06-29
\| *	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
\|/
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
* \|	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
* \|	Specific version of freeze for GF25519 (automation still needs a little work)	jadep	2016-06-17
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| *	Z is integral domain	Andres Erbsen	2016-06-16
* \|	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...	jadep	2016-06-15
* \|	changed representation definition to require digits vector to be the exact le...	jadep	2016-06-15
* \|	Added canonicalization to ModularBaseSystemOpt.	jadep	2016-06-15
* \|	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