aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
|
* remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
|
* Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-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'Gravatar Andres Erbsen2016-06-20
|\ | | | | | | includes broken files to be removed in next commit
| * tuple toolingGravatar Andres Erbsen2016-06-20
| |
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵Gravatar Andres Erbsen2016-06-18
| | | | | | | | fewer nonzero ports. remove FField and FNsatz
| * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| |
| * nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
| |
| * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
| |
* | Add coqprime that works with 8.5, bundle bedrockGravatar Jason Gross2016-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 definitionGravatar Andres Erbsen2016-06-07
|/
* F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵Gravatar Andres Erbsen2016-05-24
| | | | broken...
* Completed encoding reorganization; factored sign_bit out of PointEncodings ↵Gravatar jadep2016-04-28
| | | | and finished encoding admits.
* Reorganization and revision of Encoding code and redefinition of sign_bit ↵Gravatar jadep2016-04-25
| | | | function.
* added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵Gravatar jadep2016-04-21
| | | | weight 2^26)
* Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-04-20
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-19
|\
* | Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵Gravatar jadep2016-04-19
| | | | | | | | Z.testbit.
| * Add a tactic for field inequalitiesGravatar Jason Gross2016-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.Gravatar jadep2016-04-15
|/
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\
| * state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-03-20
| |
* | refactor of Basesystem and ModularBaseSystem; includes general code ↵Gravatar Jade Philipoom2016-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 QedGravatar Andres Erbsen2016-03-03
|
* ModularArithmetic: [field] tactic that respects opacity, prettify ↵Gravatar Andres Erbsen2016-02-28
| | | | ExtendedCoordinates, outline Edwards curve associativity
* generic binary exponentiation correctness proof in 3 one-linersGravatar Andres Erbsen2016-02-26
|
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-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 ↵Gravatar Jade Philipoom2016-02-16
| | | | imports of PointFormats and Galois things)
* added point encodings; some admits remainGravatar Jade Philipoom2016-02-16
|
* fixed renamed files and added imports for encodingsGravatar Jade Philipoom2016-02-15
|
* mergeGravatar Jade Philipoom2016-02-15
|\
* | added generic encoding specGravatar Jade Philipoom2016-02-15
| |
| * Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
|/
* Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into specGravatar Jade Philipoom2016-02-15
|\
* | ported some of EdDSA25519 to new field frameworkGravatar Jade Philipoom2016-02-15
| |
| * port bounded iter_op and Edwards doubleAndAddGravatar Andres Erbsen2016-02-15
| |
| * CompleteEdwardsCurve: unifiedAddM1: Closed Under Global ContextGravatar Andres Erbsen2016-02-15
|/
* Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.vGravatar Andres Erbsen2016-02-13
|
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12
|
* Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-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 & _CoqProjectGravatar Jason Gross2016-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; commentsGravatar varomodt2016-01-09
|
* Specific/EdDSA25519: created most of specific instantiation of EdDSA; still ↵Gravatar Jade Philipoom2016-01-05
| | | | missing parameters d, H, l, B, and PointEncoding.
* Code-reviewing EdDSAGravatar Adam Chlipala2015-12-29
|
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
|
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
|
* Merge remote-tracking branch 'jadep/master'Gravatar Andres Erbsen2015-11-06
|\
* | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)Gravatar Andres Erbsen2015-11-06
|/
* Beautified BinGF.splitWordsGravatar Adam Chlipala2015-10-30
|
* word bound propagation examplesGravatar Andres Erbsen2015-10-30
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 06:29:57 +0000