Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merged changes, including new ZUtil conventions. | 2016-07-06 | |
|\ | |||
* | | Factored out some proofs that rely only on base being powers of two, and ↵ | 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. | ||
| * | Define the spec of Weierstrass curves (#6) | 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) | 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 | 2016-06-25 | |
| | |||
* | Update _CoqProject | 2016-06-23 | |
| | |||
* | Remove vestigal BoundedWord machinery | 2016-06-23 | |
| | |||
* | Update _CoqProject | 2016-06-23 | |
| | |||
* | Remove unstable Pipeline.v examples from _CoqProject | 2016-06-23 | |
| | |||
* | Add Language.v, Conversion.v to _CoqProject | 2016-06-23 | |
| | |||
* | Add Pseudize, Vectorize, Wordize to the build process | 2016-06-22 | |
| | |||
* | Merge with public master | 2016-06-22 | |
|\ | |||
| * | Aggregate all level specifications not in Spec/* | 2016-06-22 | |
| | | | | | | | | | | This prevents notation conflicts (see comment in Notations.v for more explanation). | ||
| * | Update _CoqProject | 2016-06-22 | |
| | | |||
* | | Merge with plv/master | 2016-06-22 | |
|\| | |||
| * | move nsatz into tactics directory | 2016-06-20 | |
| | | |||
| * | remove obsolete rep mechanism | 2016-06-20 | |
| | | |||
| * | Remove anything incompatible with new algebraic hierarcy | 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' | 2016-06-20 | |
| |\ | | | | | | | | | | includes broken files to be removed in next commit | ||
| | * | tuple tooling | 2016-06-20 | |
| | | | |||
| | * | port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵ | 2016-06-18 | |
| | | | | | | | | | | | | fewer nonzero ports. remove FField and FNsatz | ||
| | * | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | 2016-06-17 | |
| | | | |||
| | * | nsatz: reimplement, integrate, demonstrate | 2016-06-15 | |
| | | | |||
| | * | [field] and [nsatz] do things now again | 2016-06-14 | |
| | | | |||
| * | | Add coqprime that works with 8.5, bundle bedrock | 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 | 2016-06-07 | |
| |/ | |||
* | | Meshing Assembly machinery into the Makefile | 2016-06-06 | |
| | | |||
* | | merging with master | 2016-06-06 | |
|\| | |||
* | | merging with master | 2016-06-06 | |
|\ \ | |||
* | | | PseudoMedialConversion done | 2016-05-31 | |
| | | | |||
| | * | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵ | 2016-05-24 | |
| | | | | | | | | | | | | broken... | ||
| | * | Completed encoding reorganization; factored sign_bit out of PointEncodings ↵ | 2016-04-28 | |
| | | | | | | | | | | | | and finished encoding admits. | ||
| | * | Reorganization and revision of Encoding code and redefinition of sign_bit ↵ | 2016-04-25 | |
| | | | | | | | | | | | | function. | ||
| | * | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵ | 2016-04-21 | |
| | | | | | | | | | | | | weight 2^26) | ||
| | * | Pulled generalized code out of GF25519 so that it can be used for other moduli | 2016-04-20 | |
| | | | |||
| | * | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | 2016-04-19 | |
| | |\ | |||
| | * | | Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵ | 2016-04-19 | |
| | | | | | | | | | | | | | | | | Z.testbit. | ||
| | | * | Add a tactic for field inequalities | 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. | 2016-04-15 | |
| | |/ | |||
* | | | Breaking out State into its own file | 2016-04-04 | |
| | | | |||
| | * | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | 2016-03-30 | |
| | |\ | |||
* | | | | add Assembly to CoqProject | 2016-03-29 | |
| | | | | |||
* | | | | merge with plv/master | 2016-03-29 | |
| |_|/ |/| | | |||
* | | | state top-level derivation for Ed25519.verify | 2016-03-20 | |
| | | | |||
| | * | refactor of Basesystem and ModularBaseSystem; includes general code ↵ | 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 | 2016-03-03 | |
| | | |||
* | | ModularArithmetic: [field] tactic that respects opacity, prettify ↵ | 2016-02-28 | |
| | | | | | | | | ExtendedCoordinates, outline Edwards curve associativity | ||
* | | generic binary exponentiation correctness proof in 3 one-liners | 2016-02-26 | |
| | | |||
* | | Factor out some bedrock dependencies into WordUtil | 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 ↵ | 2016-02-16 | |
| | | | | imports of PointFormats and Galois things) |