fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Add correctness theorems to Montgomery.ZBounded	Jason Gross	2016-08-31
*	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
*	Add congruence_option tactic	Jason Gross	2016-08-31
*	updated GF25519 to match new exponentiation chain code	jadep	2016-08-31
*	Added square roots to GF1305, started reworking freeze_opt in preparation for...	jadep	2016-08-31
*	Generalized exponentiation chains so inverse and square roots can use the sam...	jadep	2016-08-31
*	Removed some commented-out code that will probably not be needed.	jadep	2016-08-31
*	Compatibility for 8.5; clear assumptions for an admitted canonicalization proof.	jadep	2016-08-31
*	Removed lingering SearchAbout.	jadep	2016-08-31
*	Proofs for MBS square roots.	jadep	2016-08-31
*	fixed typo; extra argument	jadep	2016-08-31
*	Parameterized square roots for primes that are 5 mod 8 over any computation o...	jadep	2016-08-31
*	Reworked square root theorems to prove they are valid iff a square root exist...	jadep	2016-08-31
*	Add runtime equality comparison and square root functions to ModularBaseSystem.	jadep	2016-08-31
*	fix duplicate name in PrimeFieldTheorems	jadep	2016-08-31
*	square roots modulo p for [p mod 4 = 3]; we now have modular sqrt for all pri...	jadep	2016-08-31
*	Defined an equality comparison for tuples that uses bool instead of Prop (lik...	jadep	2016-08-31
*	Add reduce via partial to Montgomery ZBounded	Jason Gross	2016-08-29
*	Merge pull request #52 from JasonGross/bounded-interface	Jason Gross	2016-08-25
\|\
\| *	Integrate suggestions from Andres	Jason Gross	2016-08-25
* \|	Changed definition of [sub] to require proof that the modulus multiple actual...	jadep	2016-08-25
* \|	Proper proofs for all ModularBaseSystem operations except [sub]	jadep	2016-08-24
* \|	Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem...	jadep	2016-08-24
\| *	Rework bounded proofs	Jason Gross	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	More zarith	Jason Gross	2016-08-24
* \|	Add more reserved notations	Jason Gross	2016-08-24
* \|	Fewer side-conditions on zsimplify	Jason Gross	2016-08-24
\| *	More slight cleanups	Jason Gross	2016-08-24
\| *	Clean up DoubleBounded	Jason Gross	2016-08-24
* \|	Added rewrite hints for two ListUtil lemmas	jadep	2016-08-24
* \|	Moved a tactic to Util/Tactics.v	jadep	2016-08-24
* \|	Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6	jadep	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	Fix a typo	Jason Gross	2016-08-24
\| *	Merge remote-tracking branch 'upstream/master' into bounded-interface	Jason Gross	2016-08-24
\| \|\ \| \|/ \|/\|
* \|	Add map_cons from Coq 8.6	Jason Gross	2016-08-24
\| *	Coq 8.4 fixes	Jason Gross	2016-08-24
* \|	Merge branch 'fast-inverse'	jadep	2016-08-24
\|\ \
\| * \|	Removed now-obsolete ModularBaseSystemField.v; field lemmas for ModularBaseSy...	jadep	2016-08-24
\| * \|	Added optimized [inv] operation to Specific, and removed dependencies on Modu...	jadep	2016-08-24
\| \| *	Weaken the condition on smaller_bound	Jason Gross	2016-08-23
\| \| *	Hook up the bounded interface, finish proofs	Jason Gross	2016-08-23
\| \| *	Revert "Add _valid properties"	Jason Gross	2016-08-23
\| \| *	Add _valid properties	Jason Gross	2016-08-23
\| \| *	Fix some things	Jason Gross	2016-08-23
\| \| *	Add TODO	Jason Gross	2016-08-23
\| \| *	Rework interface to support rewriting database	Jason Gross	2016-08-23
\| \| *	alternative machine interface specification proposal	Andres Erbsen	2016-08-23
\| \| *	Initial work on an architecture interface for ℤ/nℤ	Jason Gross	2016-08-23
\| \|/ \|/\|