fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
*	most of feEnc correctness proof	jadep	2016-10-27
*	removed lingering TODO	jadep	2016-10-27
*	Fix for Coq 8.4 (f_equiv changed behavior)	Jason Gross	2016-10-26
*	Initial work on filling ed25519 with bounded things	Jason Gross	2016-10-25
*	prove SRepMul admit	Andres Erbsen	2016-10-25
*	Proved homomorphism between curve groups (Twisted Edwards Curve representatio...	jadep	2016-10-24
*	Freeze before packing to get canonical encodings	jadep	2016-10-24
*	ed25519: prove some admits	Andres Erbsen	2016-10-24
*	Modify point_phi (from PointEncodings) to use ref_phi	jadep	2016-10-23
*	Fix a typo	Jason Gross	2016-10-23
*	Prove onCurve_ERepB	Jason Gross	2016-10-23
*	Finish twedprm_ERep proof	Jason Gross	2016-10-23
*	Made field-element encodings canonicalize elements before encoding them	jadep	2016-10-22
*	Fix src/Experiments/Ed25519.v for Coq 8.4	Jason Gross	2016-10-22
*	final touches/fixes for freeze restructuring	jadep	2016-10-22
*	extraction: use more Haskell functions	Andres Erbsen	2016-10-21
*	fiddle with [rewrite <-!(field_div_definition)], maybe fix build	Andres Erbsen	2016-10-21
*	Edwards.Extended.to_twisted: only one inversion, improve extraction	Andres Erbsen	2016-10-21
*	Fix build failure	Jason Gross	2016-10-21
*	extraction of [sign] using Haskell [Integer]s for limbs	Andres Erbsen	2016-10-21
*	Merge branch 'master' into instantiation-rsloan-phoas	Jason Gross	2016-10-20
\|\
\| *	Fill in some things in Ed25519 from SC25519	Jason Gross	2016-10-19
\| *	Fix for change in precedence of <-> vs -> in 8.4/8.5	Jason Gross	2016-10-19
\| *	Work around out of memory error in 8.5, 8.5pl1	Jason Gross	2016-10-18
\| *	Fix for 8.4 unification being unhappy in Ed25519 (nats are terrible)	Jason Gross	2016-10-17
\| *	Various Ed25519 8.4 fixes	Jason Gross	2016-10-17
\| *	refactor scalar multiplication thoery, implement SRepERepMul	Andres Erbsen	2016-10-12
\| *	Fixed naming issue	jadep	2016-10-12
\| *	defined sign operation on field elements	jadep	2016-10-12
\| *	Fixing merge conflict	jadep	2016-10-12
\| *	integrate bitwise operations	Andres Erbsen	2016-10-12
\| *	remove Experiments.EncodingLemmas (superseded by Jade's recent work)	Andres Erbsen	2016-10-12
\| *	Add Ed25519 to _CoqProject	Jason Gross	2016-10-12
\| *	Starting to fill in Ed25519 context variables	jadep	2016-10-10
* \|	Merge _CoqProject	Rob Sloan	2016-10-06
\|\ \ \| \|/ \|/\|
* \|	Silence warnings about Require in GenericFieldPow	Jason Gross	2016-09-30
* \|	montgomery-curve	Andres Erbsen	2016-09-28
\| *	Fix merge with master	Robert Sloan	2016-09-24
\| \|\ \| \|/ \|/\|
\| *	Large-scale refactoring of src/Assembly	Robert Sloan	2016-09-24
* \|	move eddsa rep change	Andres Erbsen	2016-09-22
* \|	alternative signing derivation	Andres Erbsen	2016-09-22
* \|	deduplicate Let_In into src/Util/LetIn.v	Andres Erbsen	2016-09-17
* \|	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
* \|	IterAssocOp: parameters before arguments	Andres Erbsen	2016-09-16
\| *	Most of a more efficient WordRangeOpt	Robert Sloan	2016-09-13
\| *	Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas	Robert Sloan	2016-08-30
\| \|\
\| * \|	Pieces of a correctness lemma	Robert Sloan	2016-08-30
\| \| *	Added some more test cases for bounds checking	Adam Chlipala	2016-08-28
\| \|/
\| *	Comment out computation of Curve25519	Robert Sloan	2016-08-26
\| *	Fix evalWordRangeOpt	Robert Sloan	2016-08-26