Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | improve some fragile proofs (built on 8.4) | Andres Erbsen | 2016-11-02 |
| | |||
* | prove Proper_SRepERepMul | Andres Erbsen | 2016-10-29 |
| | |||
* | prove SRepMul admit | Andres Erbsen | 2016-10-25 |
| | |||
* | refactor scalar multiplication thoery, implement SRepERepMul | Andres Erbsen | 2016-10-12 |
| | |||
* | IterAssocOp: parameters before arguments | Andres Erbsen | 2016-09-16 |
| | |||
* | 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 |