Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 | ||
* | | CompleteEdwardsCurveTheorems: associativity proof that times out on Qed | Andres Erbsen | 2016-03-03 |
| | | |||
* | | ModularArithmetic: [field] tactic that respects opacity, prettify ↵ | Andres Erbsen | 2016-02-28 |
| | | | | | | | | ExtendedCoordinates, outline Edwards curve associativity | ||
* | | 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 |
|/ | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | proved most of point encoding admits, fixed some build system issues (dead ↵ | Jade Philipoom | 2016-02-16 |
| | | | | imports of PointFormats and Galois things) | ||
* | 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 |
|/ |