Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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. | ||
* | 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 |
|/ | |||
* | 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 ↵ | 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 |
|/ | |||
* | 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 |
| | | | | | | | | | | | | | - F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF. | ||
* | Update build process to use COQPATH & _CoqProject | Jason Gross | 2016-02-05 |
| | | | | | | | | Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.). | ||
* | simple refactor of makefile; comments | varomodt | 2016-01-09 |
| | |||
* | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still ↵ | Jade Philipoom | 2016-01-05 |
| | | | | missing parameters d, H, l, B, and PointEncoding. | ||
* | 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 ↵ | Andres Erbsen | 2015-10-25 |
|/ | | | | proofs by <jadep@mit.edu> | ||
* | add morphism-based field impl | Robert Sloan | 2015-10-22 |
| | |||
* | fix the makefile to not rebuild + module renaming | Robert Sloan | 2015-10-22 |
| | |||
* | pull changes from desktop | Robert Sloan | 2015-10-19 |
| | |||
* | gfPlus abstraction | Robert Sloan | 2015-10-16 |
| | |||
* | make ring decidable + define constants | Robert Sloan | 2015-09-19 |
| | |||
* | makefile dependency order | Andres Erbsen | 2015-09-18 |
| |