Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Move mul_rep_extended (do we actually care about this?) | Jason Gross | 2016-07-20 |
| | |||
* | 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 ↵ | jadep | 2016-07-06 |
| | | | | | | | | | | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util. | ||
* | | | add new interface to ModularBaseSystem | Andres Erbsen | 2016-07-03 |
|/ / | |||
| * | Define the spec of Weierstrass curves (#6) | Jason Gross | 2016-07-03 |
| | | | | | | | | | | Define the spec of Weierstrass curves This is the start of work on P256. | ||
| * | Implement and prove Barrett reduction on Z (#18) | Jason Gross | 2016-07-03 |
|/ | | | | | | | | Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia). | ||
* | 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 |
| | | | | | | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation). | ||
| * | 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 |
| | | | | | | | | | | | | - PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway | ||
| * | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
| |\ | | | | | | | | | | includes broken files to be removed in next commit | ||
| | * | tuple tooling | Andres Erbsen | 2016-06-20 |
| | | | |||
| | * | port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵ | Andres Erbsen | 2016-06-18 |
| | | | | | | | | | | | | fewer nonzero ports. remove FField and FNsatz | ||
| | * | 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 |
| | | | | | | | | | | | | | | | | | | This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build. | ||
| | * | 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 ↵ | Andres Erbsen | 2016-05-24 |
| | | | | | | | | | | | | broken... | ||
| | * | Completed encoding reorganization; factored sign_bit out of PointEncodings ↵ | jadep | 2016-04-28 |
| | | | | | | | | | | | | and finished encoding admits. | ||
| | * | Reorganization and revision of Encoding code and redefinition of sign_bit ↵ | jadep | 2016-04-25 |
| | | | | | | | | | | | | function. | ||
| | * | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵ | jadep | 2016-04-21 |
| | | | | | | | | | | | | weight 2^26) | ||
| | * | 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 ↵ | jadep | 2016-04-19 |
| | | | | | | | | | | | | | | | | Z.testbit. | ||
| | | * | Add a tactic for field inequalities | Jason Gross | 2016-04-19 |
| | | | | | | | | | | | | | | | | | | | | Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc. | ||
| | * | | 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 |
| | |\ | |||
* | | | | add Assembly to CoqProject | Robert Sloan | 2016-03-29 |
| | | | | |||
* | | | | merge with plv/master | Robert Sloan | 2016-03-29 |
| |_|/ |/| | | |||
* | | | state top-level derivation for Ed25519.verify | Andres Erbsen | 2016-03-20 |
| | | | |||
| | * | refactor of Basesystem and ModularBaseSystem; includes general code ↵ | Jade Philipoom | 2016-03-20 |
| |/ |/| | | | | | organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division |