| Commit message (Expand) | Author | Age |
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ... | jadep | 2016-07-21 |
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-07-20 |
|\ |
|
| * | Move mul_rep_extended (do we actually care about this?) | Jason Gross | 2016-07-20 |
* | | restructured ModularBaseSystem pipeline to put tuple conversion before Modula... | jadep | 2016-07-20 |
* | | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples. | jadep | 2016-07-19 |
|/ |
|
* | Experiments/SpecificCurve25519.v: curve25519 addition using small Z-s | Andres Erbsen | 2016-07-13 |
* | Merge of fixedlength and master | jadep | 2016-07-11 |
|\ |
|
| * | wrap nsatz in Algebra | Andres Erbsen | 2016-07-11 |
| * | Merged changes, including new ZUtil conventions. | jadep | 2016-07-06 |
| |\ |
|
| * | | Factored out some proofs that rely only on base being powers of two, and defi... | jadep | 2016-07-06 |
* | | | add new interface to ModularBaseSystem | Andres Erbsen | 2016-07-03 |
|/ / |
|
| * | Define the spec of Weierstrass curves (#6) | Jason Gross | 2016-07-03 |
| * | Implement and prove Barrett reduction on Z (#18) | Jason Gross | 2016-07-03 |
|/ |
|
* | EdDSA: prove things about spec | Andres Erbsen | 2016-06-25 |
* | Update _CoqProject | Jason Gross | 2016-06-23 |
* | Remove vestigal BoundedWord machinery | Robert Sloan | 2016-06-23 |
* | Update _CoqProject | Robert Sloan | 2016-06-23 |
* | Remove unstable Pipeline.v examples from _CoqProject | Robert Sloan | 2016-06-23 |
* | Add Language.v, Conversion.v to _CoqProject | Robert Sloan | 2016-06-23 |
* | Add Pseudize, Vectorize, Wordize to the build process | Robert Sloan | 2016-06-22 |
* | Merge with public master | Robert Sloan | 2016-06-22 |
|\ |
|
| * | Aggregate all level specifications not in Spec/* | Jason Gross | 2016-06-22 |
| * | Update _CoqProject | Jason Gross | 2016-06-22 |
* | | Merge with plv/master | Robert Sloan | 2016-06-22 |
|\| |
|
| * | move nsatz into tactics directory | Andres Erbsen | 2016-06-20 |
| * | remove obsolete rep mechanism | Andres Erbsen | 2016-06-20 |
| * | Remove anything incompatible with new algebraic hierarcy | Andres Erbsen | 2016-06-20 |
| * | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
| |\ |
|
| | * | 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 |
| * | | Add coqprime that works with 8.5, bundle bedrock | Jason Gross | 2016-06-10 |
| | * | generic field definition | Andres Erbsen | 2016-06-07 |
| |/ |
|
* | | Meshing Assembly machinery into the Makefile | Robert Sloan | 2016-06-06 |
* | | merging with master | Robert Sloan | 2016-06-06 |
|\| |
|
* | | merging with master | Robert Sloan | 2016-06-06 |
|\ \ |
|
* | | | PseudoMedialConversion done | Robert Sloan | 2016-05-31 |
| | * | 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 |
| | |/ |
|
* | | | Breaking out State into its own file | Robert Sloan | 2016-04-04 |
| | * | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 2016-03-30 |
| | |\ |
|