| Commit message (Expand) | Author | Age |
* | tuple tooling | Andres Erbsen | 2016-06-20 |
* | port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer... | Andres Erbsen | 2016-06-18 |
* | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | Andres Erbsen | 2016-06-17 |
* | nsatz: reimplement, integrate, demonstrate | Andres Erbsen | 2016-06-15 |
* | [field] and [nsatz] do things now again | Andres Erbsen | 2016-06-14 |
* | generic field definition | Andres Erbsen | 2016-06-07 |
* | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok... | Andres Erbsen | 2016-05-24 |
* | Completed encoding reorganization; factored sign_bit out of PointEncodings an... | jadep | 2016-04-28 |
* | Reorganization and revision of Encoding code and redefinition of sign_bit fun... | jadep | 2016-04-25 |
* | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ... | jadep | 2016-04-21 |
* | Pulled generalized code out of GF25519 so that it can be used for other moduli | jadep | 2016-04-20 |
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-04-19 |
|\ |
|
* | | Defined a testbit variant for BaseSystem vectors and proved equivalence to Z.... | jadep | 2016-04-19 |
| * | Add a tactic for field inequalities | Jason Gross | 2016-04-19 |
* | | Removed old iter_op version and its last dependency. | jadep | 2016-04-15 |
|/ |
|
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-03-30 |
|\ |
|
| * | state top-level derivation for Ed25519.verify | Andres Erbsen | 2016-03-20 |
* | | refactor of Basesystem and ModularBaseSystem; includes general code organizat... | Jade Philipoom | 2016-03-20 |
|/ |
|
* | CompleteEdwardsCurveTheorems: associativity proof that times out on Qed | Andres Erbsen | 2016-03-03 |
* | ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo... | Andres Erbsen | 2016-02-28 |
* | generic binary exponentiation correctness proof in 3 one-liners | Andres Erbsen | 2016-02-26 |
* | Factor out some bedrock dependencies into WordUtil | Jason Gross | 2016-02-25 |
* | proved most of point encoding admits, fixed some build system issues (dead im... | Jade Philipoom | 2016-02-16 |
* | added point encodings; some admits remain | Jade Philipoom | 2016-02-16 |
* | fixed renamed files and added imports for encodings | Jade Philipoom | 2016-02-15 |
* | merge | Jade Philipoom | 2016-02-15 |
|\ |
|
* | | added generic encoding spec | Jade Philipoom | 2016-02-15 |
| * | Finish seperating our specs: remove old non-specified code | Andres Erbsen | 2016-02-15 |
|/ |
|
* | Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec | Jade Philipoom | 2016-02-15 |
|\ |
|
* | | ported some of EdDSA25519 to new field framework | Jade Philipoom | 2016-02-15 |
| * | port bounded iter_op and Edwards doubleAndAdd | Andres Erbsen | 2016-02-15 |
| * | CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context | Andres Erbsen | 2016-02-15 |
|/ |
|
* | Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v | Andres Erbsen | 2016-02-13 |
* | port some edwards curve theorems | Andres Erbsen | 2016-02-12 |
* | Define F m, a replacement for GF with several benefits. | Andres Erbsen | 2016-02-11 |
* | Update build process to use COQPATH & _CoqProject | Jason Gross | 2016-02-05 |
* | simple refactor of makefile; comments | varomodt | 2016-01-09 |
* | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m... | Jade Philipoom | 2016-01-05 |
* | Code-reviewing EdDSA | Adam Chlipala | 2015-12-29 |
* | reorganized lemmas; moved several to ListUtil and ZUtil. | Jade Philipoom | 2015-11-24 |
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | Andres Erbsen | 2015-11-17 |
* | Merge remote-tracking branch 'jadep/master' | Andres Erbsen | 2015-11-06 |
|\ |
|
* | | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19) | Andres Erbsen | 2015-11-06 |
|/ |
|
* | Beautified BinGF.splitWords | Adam Chlipala | 2015-10-30 |
* | word bound propagation examples | Andres Erbsen | 2015-10-30 |
* | BaseSystem to Util.ListUtil: separate out generic list lemmas | Andres Erbsen | 2015-10-29 |
* | Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto | Andres Erbsen | 2015-10-29 |
|\ |
|
| * | patches for galois | Robert Sloan | 2015-10-27 |
* | | positional number system equivalence transcribed from pencil-and-paper proofs... | Andres Erbsen | 2015-10-25 |
|/ |
|
* | add morphism-based field impl | Robert Sloan | 2015-10-22 |