aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
...
| * reduce admits related to point negationGravatar Andres Erbsen2016-04-25
|/
* point_eq_decGravatar Andres Erbsen2016-04-22
|
* added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵Gravatar jadep2016-04-21
| | | | weight 2^26)
* automated most of the code in GF25519Gravatar jadep2016-04-21
|
* Cleanup of GF25519Gravatar jadep2016-04-20
|
* Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-04-20
|
* GF25519 additionGravatar jadep2016-04-20
|
* GF25519: boring stuff -- fixed indentation and removed commented-out codeGravatar jadep2016-04-20
|
* ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-04-17
|
* ed25519 derivation: use representation of FGravatar Andres Erbsen2016-04-17
|
* ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-04-16
|
* ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-04-16
|
* ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-04-16
|
* Retrieved updated version of Util/IterAssocOp and modified ↵Gravatar jadep2016-04-14
| | | | ExtendedCoordinates and Ed25519 to use it.
* Fixed syntax error (missing bracket) in Ed25519 to make merge buildGravatar jadep2016-04-12
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-12
|\
* | Finished refactor of GF25519 (partial evaluation); code builds but needs to ↵Gravatar jadep2016-04-12
| | | | | | | | be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/.
* | Merge and refactor of GF25519Gravatar jadep2016-04-11
| |
| * ed25519: continue derivationGravatar Andres Erbsen2016-04-08
| |
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\|
| * Drop second projections in Ed25519Gravatar Jason Gross2016-03-29
| |
| * ed25519 derivation: pair programming with jgross... slow progressGravatar Andres Erbsen2016-03-24
| |
| * nicer verify() derivation starterGravatar Andres Erbsen2016-03-21
| |
| * state top-level derivation for Ed25519.verifyGravatar Andres Erbsen2016-03-20
| |
* | fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParamsGravatar Jade Philipoom2016-03-20
| |
| * Finish absolutizing importsGravatar Jason Gross2016-03-10
|/ | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* proved most of point encoding admits, fixed some build system issues (dead ↵Gravatar Jade Philipoom2016-02-16
| | | | imports of PointFormats and Galois things)
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
|
* ported some of EdDSA25519 to new field frameworkGravatar Jade Philipoom2016-02-15
|
* port ModularBaseSystem.v and GF25519.v to F mGravatar Andres Erbsen2016-02-14
|
* Merge branch 'spec' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-02-12
|\
* | EdDSA25519: progress on proving PointEncoding admits; code still unorganizedGravatar Jade Philipoom2016-02-12
| |
| * port several theorems from GF to FGravatar Andres Erbsen2016-02-11
| |
| * remove a dangling AboutGravatar Andres Erbsen2016-02-07
|/
* removed lingering Check/SearchAbout statementsGravatar Jade Philipoom2016-02-07
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-02-07
|\
* | EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and ↵Gravatar Jade Philipoom2016-02-07
| | | | | | | | the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats).
| * Specific/GF25519: factor out lemmasGravatar Andres Erbsen2016-02-07
| |
| * Do some work pair-programming with Andres on optsGravatar Jason Gross2016-02-05
|/ | | | Partially pre-compile various optimizations in GF25519.
* PointFOrmats,EdDSA: remove redundant axiomsGravatar Andres Erbsen2016-01-16
|
* fix merge conflicts + PointFormats proofsGravatar Robert Sloan2016-01-14
|\
| * Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-13
| |\
| * | euler's criterion reduced to fermat's little theorem and two lemmas about ↵Gravatar Jade Philipoom2016-01-13
| | | | | | | | | | | | primitive roots.
* | | simple refactor of makefile; commentsGravatar varomodt2016-01-09
| |/ |/|
* | Merge branch 'specific-rewrite'Gravatar Andres Erbsen2016-01-06
|\ \ | |/ |/|
| * fix letify to only insert a term onceGravatar Andres Erbsen2016-01-06
| |
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-05
|\ \
* | | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still ↵Gravatar Jade Philipoom2016-01-05
| | | | | | | | | | | | missing parameters d, H, l, B, and PointEncoding.
| * | remove commentGravatar Andres Erbsen2016-01-04
|/ /
| * prettier GF25519 derivation that runs out of memoryGravatar Andres Erbsen2016-01-04
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 15:45:13 +0000