aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
* ed25519: indentation fixGravatar Andres Erbsen2016-06-22
* ed25519: integrate FRepPow and FRepInvGravatar Andres Erbsen2016-06-22
* ed25519: continue refactorGravatar Andres Erbsen2016-06-22
* Factor some rewrites into a single [autorewrite]Gravatar Jason Gross2016-06-22
* Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-06-22
* Fix some issues in Ed25519 tacticsGravatar Jason Gross2016-06-22
* F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...Gravatar Andres Erbsen2016-06-22
* unifiedAddM1Rep_sig: almost thereGravatar Andres Erbsen2016-06-22
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-06-22
* Moved sign_bit definition to Spec.Gravatar jadep2016-06-22
* Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-06-22
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-06-22
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-06-22
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-06-22
* refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-06-22
* reduce admits related to point negationGravatar Andres Erbsen2016-06-22
* Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-06-22
* point_eq_decGravatar Andres Erbsen2016-06-22
* added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...Gravatar jadep2016-06-22
* automated most of the code in GF25519Gravatar jadep2016-06-22
* Cleanup of GF25519Gravatar jadep2016-06-22
* Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-06-22
* GF25519 additionGravatar jadep2016-06-22
* GF25519: boring stuff -- fixed indentation and removed commented-out codeGravatar jadep2016-06-22
* ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-06-22
* ed25519 derivation: use representation of FGravatar Andres Erbsen2016-06-22
* ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-06-22
* ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-06-22
* ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-06-22
* Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...Gravatar jadep2016-06-22
* Fixed syntax error (missing bracket) in Ed25519 to make merge buildGravatar jadep2016-06-22
* ed25519: continue derivationGravatar Andres Erbsen2016-06-22
* Finished refactor of GF25519 (partial evaluation); code builds but needs to b...Gravatar jadep2016-06-22
* Merge and refactor of GF25519Gravatar jadep2016-06-22
* Drop second projections in Ed25519Gravatar Jason Gross2016-06-22
* fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParamsGravatar Jade Philipoom2016-06-22
* ed25519 derivation: pair programming with jgross... slow progressGravatar Andres Erbsen2016-06-22
* nicer verify() derivation starterGravatar Andres Erbsen2016-06-22
* state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-06-22
* Finish absolutizing importsGravatar Jason Gross2016-06-22
* proved most of point encoding admits, fixed some build system issues (dead im...Gravatar Jade Philipoom2016-06-22
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-06-22
* ported some of EdDSA25519 to new field frameworkGravatar Jade Philipoom2016-06-22
* port ModularBaseSystem.v and GF25519.v to F mGravatar Andres Erbsen2016-06-22
* EdDSA25519: progress on proving PointEncoding admits; code still unorganizedGravatar Jade Philipoom2016-06-22
* port several theorems from GF to FGravatar Andres Erbsen2016-06-22
* remove a dangling AboutGravatar Andres Erbsen2016-06-22
* removed lingering Check/SearchAbout statementsGravatar Jade Philipoom2016-06-22
* Specific/GF25519: factor out lemmasGravatar Andres Erbsen2016-06-22
* Do some work pair-programming with Andres on optsGravatar Jason Gross2016-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 22:17:47 +0000