diff options
author | Jason Gross <jasongross9@gmail.com> | 2017-01-12 13:21:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-01-12 13:21:39 -0500 |
commit | d5c38e6648b30e139782ac67533a1ed54119f87c (patch) | |
tree | fbda082222fbf50679b67790bfe3f8850edf5524 /expansion.md | |
parent | f8577805e1b1cb4276801fa9d4cc051678e808d2 (diff) |
Add link to CEP in expansion.md
Diffstat (limited to 'expansion.md')
-rw-r--r-- | expansion.md | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/expansion.md b/expansion.md index 7161860dc..ddb0c328e 100644 --- a/expansion.md +++ b/expansion.md @@ -21,8 +21,9 @@ go.crypto ed25519 for reference, or maybe go.crypto p256. **Weierstrass** or **Montgomery** curves, spec and associativity-commutativity proofs. This will most likely include writing a nsatz tactic wrapper that takes -into account nonzero-ness hypotheses (specified in a Coq Enhancement proposal by -Jason and Andres) and possibly debugging nsatz itself. +into account nonzero-ness hypotheses (specified in a [Coq Enhancement proposal by +Jason and Andres](https://github.com/coq/ceps/blob/master/text/007-nsatz-inequalities.md)) +and possibly debugging nsatz itself. **homomorphism** from ed25519 to x25519 -- the signing scheme and key agreement system use the same curve but in different coordinates. The ed25519 |