Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | proved most of point encoding admits, fixed some build system issues (dead ↵ | 2016-02-16 | ||
| | | | | imports of PointFormats and Galois things) | |||
* | added point encodings; some admits remain | 2016-02-16 | ||
| | ||||
* | fixed renamed files and added imports for encodings | 2016-02-15 | ||
| | ||||
* | merge | 2016-02-15 | ||
|\ | ||||
* | | added generic encoding spec | 2016-02-15 | ||
| | | ||||
| * | Finish seperating our specs: remove old non-specified code | 2016-02-15 | ||
|/ | ||||
* | Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec | 2016-02-15 | ||
|\ | ||||
* | | ported some of EdDSA25519 to new field framework | 2016-02-15 | ||
| | | ||||
| * | port bounded iter_op and Edwards doubleAndAdd | 2016-02-15 | ||
| | | ||||
| * | CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context | 2016-02-15 | ||
|/ | ||||
* | Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v | 2016-02-13 | ||
| | ||||
* | port some edwards curve theorems | 2016-02-12 | ||
| | ||||
* | Define F m, a replacement for GF with several benefits. | 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 | 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 | 2016-01-09 | ||
| | ||||
* | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still ↵ | 2016-01-05 | ||
| | | | | missing parameters d, H, l, B, and PointEncoding. | |||
* | Code-reviewing EdDSA | 2015-12-29 | ||
| | ||||
* | reorganized lemmas; moved several to ListUtil and ZUtil. | 2015-11-24 | ||
| | ||||
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | 2015-11-17 | ||
| | ||||
* | Merge remote-tracking branch 'jadep/master' | 2015-11-06 | ||
|\ | ||||
* | | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19) | 2015-11-06 | ||
|/ | ||||
* | Beautified BinGF.splitWords | 2015-10-30 | ||
| | ||||
* | word bound propagation examples | 2015-10-30 | ||
| | ||||
* | BaseSystem to Util.ListUtil: separate out generic list lemmas | 2015-10-29 | ||
| | ||||
* | Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto | 2015-10-29 | ||
|\ | ||||
| * | patches for galois | 2015-10-27 | ||
| | | ||||
* | | positional number system equivalence transcribed from pencil-and-paper ↵ | 2015-10-25 | ||
|/ | | | | proofs by <jadep@mit.edu> | |||
* | add morphism-based field impl | 2015-10-22 | ||
| | ||||
* | fix the makefile to not rebuild + module renaming | 2015-10-22 | ||
| | ||||
* | pull changes from desktop | 2015-10-19 | ||
| | ||||
* | gfPlus abstraction | 2015-10-16 | ||
| | ||||
* | make ring decidable + define constants | 2015-09-19 | ||
| | ||||
* | makefile dependency order | 2015-09-18 | ||
| | ||||
* | Curves: elliptic curve point format record declarations and some invariants | 2015-09-18 | ||
| | ||||
* | import VerdiTactics | 2015-09-17 | ||
| | ||||
* | redo module structure + init curve25519 | 2015-09-16 | ||
| | ||||
* | init our centralized repo | 2015-09-10 | ||