fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Absolutize some imports	Jason Gross	2017-01-31
*	Absolutize some imports	Jason Gross	2017-01-31
*	Not quite done with WordUtil lemmas.	Robert Sloan	2016-11-08
\|\
* \|	More of jgross admits, less neg and the cmovs	Rob Sloan	2016-11-01
\| *	Switch to reflective bounded word in Ed25519	Jason Gross	2016-10-31
* \|	most of jgross' admits	Rob Sloan	2016-10-31
\| *	Silence a warning	Jason Gross	2016-10-31
\| *	Significantly faster wordToN, I hope	Jason Gross	2016-10-31
\|/
*	Disable extraction in src/Assembly/GF25519.v	Jason Gross	2016-10-29
*	Disable some printing	Jason Gross	2016-10-29
*	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\|\
* \|	Fixes for Coq 8.4	Jason Gross	2016-10-27
* \|	Strip function extensionality, enable printing of sub, mul, opp, freeze	Jason Gross	2016-10-27
* \|	Tactics to manually remove Z.to/of_N and such	Robert Sloan	2016-10-26
* \|	Refactors to remove intermediate conversions	Robert Sloan	2016-10-26
\| *	Switch to bounded Z	Jason Gross	2016-10-25
* \|	Refactors to remove intermediate conversions in HLConversions	Robert Sloan	2016-10-25
* \|	Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas	Robert Sloan	2016-10-24
\|\ \
* \| \|	Use HL conversions for all data types + Pipeline.v refactors	Robert Sloan	2016-10-24
\| \| *	Add pack, unpack, ge_modulus to axioms to be reified	Jason Gross	2016-10-24
\| \| *	Fix for weaker pattern matching in < 8.4pl4	Jason Gross	2016-10-22
\| \| *	Fix for weaker pattern matching in < 8.4pl4	Jason Gross	2016-10-22
\| * \|	More Coq 8.4 fixes	Jason Gross	2016-10-22
\| * \|	Fix 8.4 build	Jason Gross	2016-10-22
\| * \|	cbn does not exist in 8.4	Jason Gross	2016-10-22
\| * \|	Fix 8.4 build	Jason Gross	2016-10-22
\| * \|	Fix build failure in 8.6	Jason Gross	2016-10-22
\| * \|	Merge branch 'master' into pr/84	Jason Gross	2016-10-22
\|/\| \| \| \|/
\| *	Unfold interp stuff in Assembly/GF25519BoundedInstantiation	Jason Gross	2016-10-22
\| *	Interpret LetIn to Let_In for better control of interp	Jason Gross	2016-10-22
* \|	Make lower bounds work by using HL conversions	Robert Sloan	2016-10-21
* \|	merge rsloan-phoas refactors into master	Robert Sloan	2016-10-21
\|\ \
* \ \	merge rsloan-phoas refactors into master	Robert Sloan	2016-10-21
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	committing unstable refactors to patch master	Robert Sloan	2016-10-21
\| * \|	Instantiate some things with bounded things	Jason Gross	2016-10-21
\| \| *	committing unstable refactors to patch master	Robert Sloan	2016-10-21
\| \|/ \|/\|
\| *	A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant...	Jason Gross	2016-10-20
\| *	Plug bounded into assembly stuff	Jason Gross	2016-10-20
\| *	Adjust bounds in assembly	Jason Gross	2016-10-20
\| *	Split up GF25519Bounded to avoid circular dependencies	Jason Gross	2016-10-20
\| *	Various fixes for Coq 8.4	Jason Gross	2016-10-20
\| *	Use carry versions of operations	Jason Gross	2016-10-20
\| *	rfreeze, not rinv; update to saner boundedness requirements	Jason Gross	2016-10-20
\| *	Start instantiating boundedness things	Jason Gross	2016-10-19
\|/
*	Fast bounds-checking machinery but lower-bounds are broken	Robert Sloan	2016-10-18
*	Converting to bounded machinery	Robert Sloan	2016-10-17
*	More of the Conversions.v correctness proofs	Robert Sloan	2016-10-14
*	Use 64-bit limbs in Pipelines	Robert Sloan	2016-10-14
*	Making sub bounds actually tight	Robert Sloan	2016-10-14
*	Moved to non-extended operations + Extraction + Bounds-checking	Robert Sloan	2016-10-14