aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)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
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
| * tuple toolingGravatar Andres Erbsen2016-06-20
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
| * 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
| * generic field definitionGravatar Andres Erbsen2016-06-07
|/
* F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...Gravatar Andres Erbsen2016-05-24
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-04-28
* Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-04-25
* added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...Gravatar jadep2016-04-21
* 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 Z....Gravatar jadep2016-04-19
| * Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
* | 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 organizat...Gravatar Jade Philipoom2016-03-20
|/
* CompleteEdwardsCurveTheorems: associativity proof that times out on QedGravatar Andres Erbsen2016-03-03
* ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...Gravatar Andres Erbsen2016-02-28
* generic binary exponentiation correctness proof in 3 one-linersGravatar Andres Erbsen2016-02-26
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
* proved most of point encoding admits, fixed some build system issues (dead im...Gravatar Jade Philipoom2016-02-16
* 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
* Update build process to use COQPATH & _CoqProjectGravatar Jason Gross2016-02-05
* simple refactor of makefile; commentsGravatar varomodt2016-01-09
* Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...Gravatar Jade Philipoom2016-01-05
* 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-09 09:04:08 +0000