fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	8.5 fixes	Jason Gross	2016-06-10
\|
*	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-05-24
\| \| \| \| \| \| \| \| \| \|	Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work.
*	Retrieved updated version of Util/IterAssocOp and modified ↵	jadep	2016-04-14
\| \| \| \|	ExtendedCoordinates and Ed25519 to use it.
*	Reverting Util/IterAssocOp to an earlier version for compatibility with ↵	jadep	2016-04-12
\| \| \| \|	CompleteEdwardsCurve/ExtendedCoordinates (we don't have testbit defined yet)
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* \|	IterAssocOp: now uses arbitrary representation of scalar that implements testbit	Jade Philipoom	2016-03-08
\| \|
* \|	IterAssocOp : now takes a bound argument instead of just using size of exponent	Jade Philipoom	2016-03-07
\|/
*	IterAssocOp : proved iter_op with function exponential	Jade Philipoom	2016-03-03
\|
*	generic binary exponentiation correctness proof in 3 one-liners	Andres Erbsen	2016-02-26