fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	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
\| *	More 8.4 Admitted fixes	Jason Gross	2016-08-17
\| *	More fixes for 8.4	Jason Gross	2016-08-17
\|/
*	More 8.4 compat	Jason Gross	2016-08-16
*	Fixes for Coq 8.4	Jason Gross	2016-08-16
*	Add some list util, and decode'_map_mul	Jason Gross	2016-08-16
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-16
\|\
* \	Merge of conversion development branch with master	jadep	2016-08-16
\|\ \
\| * \|	Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. Furt...	jadep	2016-08-16
\| \| *	Add decode_shift_app	Jason Gross	2016-08-16
\| \|/ \|/\|
\| *	Instantiated conversion both to (pack) and from (unpack) another set of limb ...	jadep	2016-08-16
\| *	Pow2BaseProofs.v : removed Z lemmas that are now in ZUtil, updated the way [c...	jadep	2016-08-16
* \|	Factor decode_shift_uniform	Jason Gross	2016-08-15
\| *	Proved remaining lemmas directly about conversion loop; still need to prove l...	jadep	2016-08-14
\| *	Conversion: main step proof done	jadep	2016-08-13
* \|	Add decode_nonneg	Jason Gross	2016-08-12
* \|	Add upper_bound_uniform	Jason Gross	2016-08-12
* \|	Weaker UniformBase assumptions	Jason Gross	2016-08-12
* \|	Add length lemmas	Jason Gross	2016-08-12
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-12
\|\ \
* \| \|	added convenience lemma about [bounded] and [upper_bound] in Pow2BaseProofs.v	jadep	2016-08-12
\| \| *	New and improved conversion proofs (final conditions proven, invariant step u...	jadep	2016-08-12
\| \|/ \|/\|
\| *	Fix build for Coq < 8.6	Jason Gross	2016-08-12