aboutsummaryrefslogtreecommitdiff
path: root/expansion.md
diff options
context:
space:
mode:
authorGravatar Jason Gross <jasongross9@gmail.com>2017-01-12 13:21:39 -0500
committerGravatar GitHub <noreply@github.com>2017-01-12 13:21:39 -0500
commitd5c38e6648b30e139782ac67533a1ed54119f87c (patch)
treefbda082222fbf50679b67790bfe3f8850edf5524 /expansion.md
parentf8577805e1b1cb4276801fa9d4cc051678e808d2 (diff)
Add link to CEP in expansion.md
Diffstat (limited to 'expansion.md')
-rw-r--r--expansion.md5
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