Remove old EC / ECDSA implementations

Common/EC/PrimeField/P192.cry → Common/EC/PrimeField/Instantiations/P192.cry

@@ -13,7 +13,7 @@ encrypted data.
 
 */
 
-module Common::EC::PrimeField::P192 =
+module Common::EC::PrimeField::Instantiations::P192 =
        Common::EC::PrimeField::PFEC where
 type P = 6277101735386680763835789423207666416083908700390324961279
 type n' =  6277101735386680763835789423176059013767194773182842284081

Common/EC/PrimeField/P224.cry → Common/EC/PrimeField/Instantiations/P224.cry

@@ -7,7 +7,7 @@ Also standardized as "secp224r1" in [SEC2-v2] Section 2.3.2.
 @author Max Orhai
 */
 
-module Common::EC::PrimeField::P224 =
+module Common::EC::PrimeField::Instantiations::P224 =
        Common::EC::PrimeField::PFEC where
 type P = 26959946667150639794667015087019630673557916260026308143510066298881
 type n' = 26959946667150639794667015087019625940457807714424391721682722368061

Common/EC/PrimeField/P256.cry → Common/EC/PrimeField/Instantiations/P256.cry

@@ -7,7 +7,7 @@ Also standardized as "secp256r1" in [SEC2-v2] Section 2.4.2.
 @author Max Orhai
 */
 
-module Common::EC::PrimeField::P256 =
+module Common::EC::PrimeField::Instantiations::P256 =
        Common::EC::PrimeField::PFEC where
 type P = 115792089210356248762697446949407573530086143415290314195533631308867097853951
 type n' = 115792089210356248762697446949407573529996955224135760342422259061068512044369

Common/EC/PrimeField/P384.cry → Common/EC/PrimeField/Instantiations/P384.cry

@@ -7,7 +7,7 @@ Also standardized as "secp384r1" in [SEC2-v2] Section 2.5.1.
 @author Max Orhai
 */
 
-module Common::EC::PrimeField::P384 =
+module Common::EC::PrimeField::Instantiations::P384 =
        Common::EC::PrimeField::PFEC where
 type P = 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319
 type n' = 39402006196394479212279040100143613805079739270465446667946905279627659399113263569398956308152294913554433653942643

Common/EC/PrimeField/P521.cry → Common/EC/PrimeField/Instantiations/P521.cry

@@ -7,7 +7,7 @@ Also standardized as "secp521r1" in [SEC2-v2] Section 2.6.1.
 @author Max Orhai
 */
 
-module Common::EC::PrimeField::P521 =
+module Common::EC::PrimeField::Instantiations::P521 =
        Common::EC::PrimeField::PFEC where
 type P = 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151
 type n' = 6864797660130609714981900799081393217269435300143305409394463459185543183397655394245057746333217197532963996371363321113864768612440380340372808892707005449

Common/EC/Tests/P192.cry → Common/EC/PrimeField/Tests/P192.cry

@@ -9,7 +9,7 @@ From [MATH-2008] Section 4.1.2.
 
 */
 
-import Common::EC::PrimeField::P192 as P192
+import Common::EC::PrimeField::Instantiations::P192 as P192
 import Common::utils(BVtoZ)
 
 // NB: We haven't implemented the point compression functions yet, but if we

Common/EC/Tests/P224.cry → Common/EC/PrimeField/Tests/P224.cry

@@ -9,7 +9,7 @@ From [MATH-2008] Section 4.2.2.
 
 */
 
-import Common::EC::PrimeField::P224 as P224
+import Common::EC::PrimeField::Instantiations::P224 as P224
 import Common::utils(BVtoZ)
 
 // NB: We haven't implemented the point compression functions yet, but if we

Common/EC/Tests/P256.cry → Common/EC/PrimeField/Tests/P256.cry

@@ -9,7 +9,7 @@ From [MATH-2008] Section 4.3.2.
 
 */
 
-import Common::EC::PrimeField::P256 as P256
+import Common::EC::PrimeField::Instantiations::P256 as P256
 import Common::utils(BVtoZ)
 
 // NB: We haven't implemented the point compression functions yet, but if we

Common/EC/Tests/P384.cry → Common/EC/PrimeField/Tests/P384.cry

@@ -9,7 +9,7 @@ From [MATH-2008] Section 4.4.2.
 
 */
 
-import Common::EC::PrimeField::P384 as P384
+import Common::EC::PrimeField::Instantiations::P384 as P384
 import Common::utils(BVtoZ)
 
 // NB: We haven't implemented the point compression functions yet, but if we

Common/EC/Tests/P521.cry → Common/EC/PrimeField/Tests/P521.cry

@@ -9,7 +9,7 @@ From [MATH-2008] Section 4.5.2.
 
 */
 
-import Common::EC::PrimeField::P521 as P521
+import Common::EC::PrimeField::Instantiations::P521 as P521
 import Common::utils(BVtoZ)
 
 // NB: We haven't implemented the point compression functions yet, but if we

Common/EC/README.md

@@ -2,40 +2,12 @@
 
 Elliptic-curve cryptography uses the structure of elliptic curves over finite fields to solve cryptographic problems. Unlike many algorithms in this repository, elliptic curves do not have a single point of truth specification describing all their potentially useful routines; there are several types of curves that are suitable for use in cryptographic applications and many choices for parameters. The elliptic curve interface in `ECInterface.cry` aims to capture the generic functionality of a curve for use in elliptic-curve cryptography.
 
-There are [many curves that have been proposed](http://safecurves.cr.yp.to/index.html) for use in cryptography. At this time, this repository contains three implementations of the NIST-standardized prime field elliptic curves. These curves are notable because they are the only standardized, non-deprecated curves recommended for use in ECDSA and ECDH, and also because their domain parameters are chosen to allow more optimized implementations of some common curve operations. The specification [SP 800-186](https://doi.org/10.6028/NIST.SP.800-186) sets the domain parameters that define the curve, but does not define concrete routines to implement useful curve operations; these are drawn from various other sources.
+There are [many curves that have been proposed](http://safecurves.cr.yp.to/index.html) for use in cryptography. At this time, this repository contains one implementation of the NIST-standardized prime field elliptic curves. These curves are notable because they are the only standardized, non-deprecated curves recommended for use in ECDSA and ECDH, and also because their domain parameters are chosen to allow more optimized implementations of some common curve operations. The specification [SP 800-186](https://doi.org/10.6028/NIST.SP.800-186) sets the domain parameters that define the curve, but does not define concrete routines to implement useful curve operations; these are drawn from various other sources.
 
-The first implementation aims to closely implement the specification and sources for routines. It instantiates the elliptic curve interface.
-```
-Common/EC/
-+ PrimeField/
-  + PFEC.cry
-  + P192.cry
-  + P224.cry
-  + P256.cry
-  + P384.cry
-  + P521.cry
-+ Tests/
-  + P192.cry
-  + P224.cry
-  + P256.cry
-  + P384.cry
-  + P521.cry
-```
+Structurally, the curve implementation is generic over concrete parameters but with several assumptions that tie it to the NIST curves specifically. This can be found in `PFEC.cry`. Instantiations for specific parameters are in `Instantiations/` and concrete test vectors for each instantiated curve are in `Tests/`. Additional properties of the NIST curves are specified in the generic implementation and can be checked by loading a specific curve and using `:check-docstrings` to evaluate all the properties.
 
-The second is optimized for SAW proofs against a Java implementation. It has some generic components but is only fully instantiated for the P-384 curve. It has a corresponding ECDSA implementation in `Primitive/Asymmetric/Signature/ecdsa.cry`. It does not instantiate the elliptic curve interface.
-```
-Common/EC/
-+ ec_point_ops.cry
-+ p384_ec_mul.cry
-+ p384_ec_point_ops.cry
-+ p384_field.cry
-+ ref_ec_mul.cry
-```
+This is one of many, many implementations of the NIST prime field curves that have been written in Cryptol over the years. One grandparent of particular interest is a 2011 curve implementation that was used to verify a Java implementation of ECDSA in combination with [SAWScript](https://github.com/GaloisInc/saw-script/). This implementation no longer lives in this repo, but it can be seen together with the Java code and the SAW scripts used in the full verification toolchain [in the examples directory of the SAWScript repository](https://github.com/GaloisInc/saw-script/tree/master/examples/ecdsa).
 
-The third is standalone. At time of writing, I don't know if it's used for anything. It does not instantiate the elliptic curve interface.
-```
-Common/EC/
-+ EC_P384.cry
-```
+Several other implementations of elliptic curves used to live in this repository. If you would like to explore these, they were removed in the commit with hash:
+> [9ae493eeb6eb0df0a149b416c5f1ccb6a1de5fc5](https://github.com/GaloisInc/cryptol-specs/commit/9ae493eeb6eb0df0a149b416c5f1ccb6a1de5fc5)
 
-There is a fourth implementation of the NIST prime field elliptic curves. It lives in `Primitives/Asymmetric/Signature/ECDSA` and is closely entwined with one of the implementations of ECDSA. Many of the routines in this implementation were ported to the more generic `PFEC` implementation above.