Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵ | jadep | 2016-07-21 |
| | | | | organization of reasoning. | ||
* | restructured ModularBaseSystem pipeline to put tuple conversion before ↵ | jadep | 2016-07-20 |
| | | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt | ||
* | Fixed unsimplified multiplication definitions in Specific by separating out ↵ | jadep | 2016-07-18 |
| | | | | the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions. | ||
* | more changes to Specific for 8.4 compatibility | jadep | 2016-07-15 |
| | |||
* | re-cleaned operations in Specific and updated GF25519 to match GF1305 | jadep | 2016-07-12 |
| | |||
* | pushing through a tweak to the arguments of [sub], and defining a field over ↵ | jadep | 2016-07-12 |
| | | | | ModularBaseSystemInterface using some placeholder operations. | ||
* | ported Specific files to use ModularBaseSystemInterface | jadep | 2016-07-11 |
| | |||
* | Aggregate all level specifications not in Spec/* | Jason Gross | 2016-06-22 |
| | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation). | ||
* | remove obsolete rep mechanism | Andres Erbsen | 2016-06-20 |
| | |||
* | GF25519: quiet | Andres Erbsen | 2016-06-20 |
| | |||
* | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
|\ | | | | | | | includes broken files to be removed in next commit | ||
* | | Canonicalization is now automated in GF25519 and added to GF1305. | jadep | 2016-06-17 |
| | | |||
* | | Specific version of freeze for GF25519 (automation still needs a little work) | jadep | 2016-06-17 |
| | | |||
* | | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵ | jadep | 2016-06-15 |
| | | | | | | | | base-length digit vectors) | ||
* | | Work around bug #4811 (slow f_equal) | Jason Gross | 2016-06-11 |
| | | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev) | ||
| * | ed25519: refactor some Proper | Andres Erbsen | 2016-06-06 |
|/ | |||
* | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵ | Andres Erbsen | 2016-05-24 |
| | | | | broken... | ||
* | Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵ | jadep | 2016-05-09 |
| | | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want. | ||
* | automated most of the code in GF25519 | jadep | 2016-04-21 |
| | |||
* | Cleanup of GF25519 | jadep | 2016-04-20 |
| | |||
* | Pulled generalized code out of GF25519 so that it can be used for other moduli | jadep | 2016-04-20 |
| | |||
* | GF25519 addition | jadep | 2016-04-20 |
| | |||
* | GF25519: boring stuff -- fixed indentation and removed commented-out code | jadep | 2016-04-20 |
| | |||
* | Finished refactor of GF25519 (partial evaluation); code builds but needs to ↵ | jadep | 2016-04-12 |
| | | | | be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/. | ||
* | Merge and refactor of GF25519 | jadep | 2016-04-11 |
| | |||
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-03-30 |
|\ | |||
* | | fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams | Jade Philipoom | 2016-03-20 |
| | | |||
| * | 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 ``` | ||
* | proved most of point encoding admits, fixed some build system issues (dead ↵ | Jade Philipoom | 2016-02-16 |
| | | | | imports of PointFormats and Galois things) | ||
* | port ModularBaseSystem.v and GF25519.v to F m | Andres Erbsen | 2016-02-14 |
| | |||
* | remove a dangling About | Andres Erbsen | 2016-02-07 |
| | |||
* | Specific/GF25519: factor out lemmas | Andres Erbsen | 2016-02-07 |
| | |||
* | Do some work pair-programming with Andres on opts | Jason Gross | 2016-02-05 |
| | | | | Partially pre-compile various optimizations in GF25519. | ||
* | simple refactor of makefile; comments | varomodt | 2016-01-09 |
| | |||
* | fix letify to only insert a term once | Andres Erbsen | 2016-01-06 |
| | |||
* | prettier GF25519 derivation that runs out of memory | Andres Erbsen | 2016-01-04 |
| | |||
* | UNTESTED simplification of specific GF25519 derivation | Andres Erbsen | 2016-01-02 |
| | |||
* | Remove redundancy in lemma statement | Adam Chlipala | 2015-12-09 |
| | |||
* | Specific/GF25519: explicit formula for multiplication | Andres Erbsen | 2015-12-05 |
| | |||
* | GF25519: synthesize explicit formula for multiplication (no reduction yet) | Andres Erbsen | 2015-12-05 |
| | |||
* | Specific/GF25519: Updated to match new PseudoMersenneBaseParams spec. | Jade Philipoom | 2015-11-24 |
| | |||
* | ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ↵ | Jade Philipoom | 2015-11-20 |
| | | | | carry_rep. | ||
* | BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ↵ | Jade Philipoom | 2015-11-10 |
| | | | | (first element of base is 1). | ||
* | ModularBaseSystem: finish base_good | Andres Erbsen | 2015-11-07 |
| | |||
* | ModularBaseSystem: prove some admits in mase system extension | Andres Erbsen | 2015-11-07 |
| | |||
* | Specific: PseudoMersenneBaseParams for GF25519Base25Point5. | Andres Erbsen | 2015-11-06 |
| | |||
* | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19) | Andres Erbsen | 2015-11-06 |
| | |||
* | src/Specific/GF25519.v: more complicated example for BaseSystem | Andres Erbsen | 2015-11-05 |