fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	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
\| *	Merge into rsloan-phoas	Robert Sloan	2016-08-26
\| *	Merge into rsloan-phoas	Robert Sloan	2016-08-26
\| \|\
\| * \|	Much tighter bounds in Evaluables.v	Robert Sloan	2016-08-26
\| \| *	Add an example of bounds checking going wrong	Adam Chlipala	2016-08-26
\| \|/
\| *	Full GF25519 Bounds-check	Robert Sloan	2016-08-25
\| *	Removed nat arguments to Evaluable operations	Robert Sloan	2016-08-25
\| *	Finishing tactical machinery for bound-computing	Robert Sloan	2016-08-24
\| *	In-place input AST conversion in SpecificCurve25519	Robert Sloan	2016-08-23
\| *	Type requirements for in-place AST conversion in SpecificCurve25519	Robert Sloan	2016-08-23
* \|	remove eq_dec from Monoid	Andres Erbsen	2016-08-23
\| *	Experimental requirements for rsloan-phoas	Robert Sloan	2016-08-23
\| *	correct the notation in generated code	Andres Erbsen	2016-08-08
\| *	SpecificCurve25519.v: correct confusing notation	Andres Erbsen	2016-08-08
\| *	fixups (h/t jgross)	Andres Erbsen	2016-08-08
\| *	compiler output and claimed timings	Andres Erbsen	2016-08-08
\| *	PHOAS-based reflective simplification of specific code	Andres Erbsen	2016-08-08
\|/
*	Merge branch 'modular-arithmetic-refactor'	Andres Erbsen	2016-08-08
\|\
* \|	Instantiated twisted [d] using ModularBaseSystem	jadep	2016-08-07
\| *	[F] has its own module now	Andres Erbsen	2016-08-05
\| *	address code review comments	Andres Erbsen	2016-08-04
\| *	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\|/
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
*	ed25519 spec: small cleanup	Andres Erbsen	2016-07-21
*	compute on [F q]!	Andres Erbsen	2016-07-20
*	experiments wd25519: simplify proof for a	Andres Erbsen	2016-07-20
*	Silence a warning	Jason Gross	2016-07-18
*	Remove a nested proof	Jason Gross	2016-07-18
*	ported IterAssocOp to use monoid rather than a billion context variables that...	jadep	2016-07-18
*	Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s	Andres Erbsen	2016-07-13
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
\| *	added proofs about addition chain exponentiation for later use in ModularBase...	jadep	2016-07-10
* \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\|/
*	EdDSARefinement: work around rewrite_strat for 8.4	Andres Erbsen	2016-06-28