From d5c38e6648b30e139782ac67533a1ed54119f87c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 12 Jan 2017 13:21:39 -0500 Subject: Add link to CEP in expansion.md --- expansion.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'expansion.md') 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 -- cgit v1.2.3