Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | 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 | |
|/ | ||||
* | 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 | |
| | ||||
* | Curves: elliptic curve point format record declarations and some invariants | Andres Erbsen | 2015-09-18 | |
| | ||||
* | import VerdiTactics | Andres Erbsen | 2015-09-17 | |
| | ||||
* | redo module structure + init curve25519 | Robert Sloan | 2015-09-16 | |
| | ||||
* | init our centralized repo | Robert Sloan | 2015-09-10 | |