fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
\| *	Drop CSE from Fancy Machine	Jason Gross	2016-09-22
\|/
*	alternative signing derivation	Andres Erbsen	2016-09-22
*	Reorganization, moving of lemmas to correct files, and 8.4 compatibility	jadep	2016-09-21
*	Proved specification of constant-time modulus comparison (except for one ZUti...	jadep	2016-09-21
*	Fix the 8.4 build by changing a couple standard library names	jadep	2016-09-18
*	Add reserved notation for Let, change #	Jason Gross	2016-09-17
*	Move side lemmas to appropriate files	jadep	2016-09-17
*	Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...	jadep	2016-09-17
*	Proved bounds for [encode] results; fleshed out some structure for [freeze] p...	jadep	2016-09-17
*	Fix missing parenthesis	jadep	2016-09-17
*	Remove unused lemma and standardized use of notations for [freeze] proofs	jadep	2016-09-17
*	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
*	ModularArithmetic: conversions between [F] and [nat]	Andres Erbsen	2016-09-16
*	Tweaked automation for 8.4 compatibility	jadep	2016-09-14
*	Automated and cleaned up [freeze] carry-loop proofs	jadep	2016-09-13
*	Update old carry loop bounds proof; now is automated and also has analogous s...	jadep	2016-09-13
*	Moved lemmas to ZUtil	jadep	2016-09-13
*	Finished off last admits for proofs of bounds after 3 carry loops.	jadep	2016-09-13
*	[freeze] proofs : Mostly-complete proofs of bounds after 3 carry loops	jadep	2016-09-13
*	[freeze] proofs : proved bounds for second carry loop.	jadep	2016-09-13
*	Fully qualify [Require]s	Jason Gross	2016-09-08
*	Better spec in Montgomery.ZBounded	Jason Gross	2016-09-07
*	Finished sqrt in GF25519	jadep	2016-09-06
*	Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...	jadep	2016-09-06
*	Add correctness theorems to Montgomery.ZBounded	Jason Gross	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
*	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
*	Add reduce via partial to Montgomery ZBounded	Jason Gross	2016-08-29
*	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
*	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
*	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
*	Shifted around some of the proofs in ModularBaseSystemField.v and propagated ...	jadep	2016-08-23
*	Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing plac...	jadep	2016-08-23
*	Proved homomorphism between ModularBaseSystem field and F q	jadep	2016-08-22
*	Merge.	jadep	2016-08-21
\|\
* \|	Proved some leftover admits in Pow2BaseProofs.v	jadep	2016-08-21
* \|	Finished [split_index] proofs and reworked conversion proofs to match.	jadep	2016-08-21