diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 11:27:24 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-04-06 11:27:24 -0400 |
| commit | 28e6f4561a1d3084b8a1aa5be3fbb227abadbb20 (patch) | |
| tree | 9fb2c12edce8473b1e3023d3420e80a12d97f1e7 /expansion.md | |
| parent | 1b0002e54c18baa4330820aa754211039dadc5c2 (diff) | |
Remove done tasks from `expansion.md`
Diffstat (limited to 'expansion.md')
| -rw-r--r-- | expansion.md | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/expansion.md b/expansion.md index 8e2b34c95..15e3b7e3d 100644 --- a/expansion.md +++ b/expansion.md @@ -19,12 +19,6 @@ implementing unsigned-to-signed conversion for bignums. binary exponentiation (window of 1 bit), but 4 would be much faster. See 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](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 fixed-basepoint scalar multiplication with precomputed tables is faster than @@ -55,20 +49,6 @@ for some existing curve for to test it; the real target would be p256. may or may not be better than our current one, but it very well might be less code+proof. -**striping** for poly1305 -- evaluating a polynomial by splitting it into, for -example, 4 polynomials such that coefficient i is in polynomial i mod 4 and -evaluating the 4 polynomials in parallel, then combining results. - -**saturated-limb** arithmetic synthesis -- we currently have some support for -synthesizing "multi-word" fixed-size integers using saturated techniques, but -such code is separate from our main BaseSystem, is not as complete, and has had -synthesis performance issues. We should investigate whether the saturated-limb -and unsaturated-limb synthesis systems can be unified (e g try to define -add-get-carry in terms of integer addition and the NewBaseSystem split -operation). If not, improve the multi-word code so that it can synthesize -arithmetic modulo p256 and order of curve25519 using existing Montgomery and -Barrett reduction formulas respectively. - **refined Montgomery multiplication** for p256 and maybe RSA. Model after the work of Shay Gueron and Vlad Krasnov -- the code is in OpenSSL ("rsaz" and "p256z" assembly for AMD64) and there are papers as well. Note that we already |