From 31d577c84f2b987ac040565b7a2dd392a58e851a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 15 Nov 2016 15:46:47 -0500 Subject: remove outdated files: roadmap and to_gallina --- roadmap.md | 47 ----------------------------------------------- to_gallina.md | 7 ------- 2 files changed, 54 deletions(-) delete mode 100644 roadmap.md delete mode 100644 to_gallina.md diff --git a/roadmap.md b/roadmap.md deleted file mode 100644 index ecace18a7..000000000 --- a/roadmap.md +++ /dev/null @@ -1,47 +0,0 @@ -# Roadmap - -A brief overview of possible long-term targets: - -- Ed25519 Signing - * Simplistic implementation: constant-time scalar multiplication - * Fast implementation: fixed-base precomputed constant-time scalar multiplication (big tables) - * Hardest part: ModularBaseSystem for exponent field (non-pseudomersenne modular arithmetic) -- Ed25519 Verification - * Simplistic implementation: two non-constant time scalar multiplications, one addition (probably best thing to work on now) - * Fast implemetation: double-scalar multiplication - * Hardest part: optimizing double-scalar multiplication -- Ed25519 Batch Verification - * Simplistic implementation: many single verifications - * Fast implemetation: multi-scalar multiplication - * Hardest part: max-heap of exponent scalars -- Key agreement (X25519) - * X-coordinate-only Montgomery ladder (similar to square-and-multiply, but not identical) - * Hardest part: proving correctness of differential addition (requires field, nontrivial proof) - -## Common Subgoals - -- Synthesis of optimized modular arithmetic (ModularBaseSystem) -- necessary for all targets - * expression simplification (plus 0, times 1, etc.) - * bounds/no-overflow proofs - * automatic carry-chain synthesis (depends on bounds automation) - * selection (bx + (not b)y) -- necessary for signing and key agreement -- Scalar arithmetic for exponents (non-pseudomersenne modular arithmetic) -- necessary for signing, batch verification - * less performance-critical than ModularBaseSystem for pseudomersenne primes - * constant-time for signing - * add, sub, mul, reduce -- General theorems about elliptic curve arithmetic (requires field; proofs are hard and rely extensively on existing literature) - * addition is commutative - * our representations are interchangable (except MontgomeryX) -- Gallina with Words to Qhasm translation - * simple expressions -- necessary for all targets - * bounded loops -- necessary for all targets - * lookup tables -- necessary for fast signing - * function abstraction -- would improve performance of all targets, most important for fast verification/batch verification -- Wire format specification -- necessary for all targets - * little byte-Endian integers - * point compression -- Wire format decoding -- necessary for all targets - * converting between BaseSystems whose digit weights are different sequences of powers of 2 - * single-coordinate point recovery (use X and a single bit to recover (X, Y)); needs field tactic -- Interfacing with hash functions -- necessary for all signature targets - * no specific properties, just that output is determined by input diff --git a/to_gallina.md b/to_gallina.md deleted file mode 100644 index 1ac5075ef..000000000 --- a/to_gallina.md +++ /dev/null @@ -1,7 +0,0 @@ -Remaining work needed for Gallina verification code ---------------------------------------------------- -+ efficient GF exponentiation -+ efficient GF inverse -+ make EdDSA point addition use ModularBaseSystem -+ represent scalars (Fl) in ModularBaseSystem (large c) -+ canonical representations of field elements -- cgit v1.2.3