CIP-2551? | Ed25519 Elliptic Curve Group Primitives in Plutus Core

CIP-2551/CIP-2551.md

@@ -0,0 +1,271 @@
+---
+CIP: ?
+Title: Ed25519 elliptic curve group primitives
+Authors: Morgan Thomas <[email protected]>
+Discussions-To: <[email protected]>
+Status: Draft
+Type: Standards Track
+Created: 2022-07-27
+* License: Apache-2.0
+---
+
+## Preamble
+
+RFC 822 style headers containing metadata about the CIP, including the CIP
+number, a short descriptive title (limited to a maximum of 44 characters),
+the names, and optionally the contact info for each author, etc.
+
+## Simple Summary
+
+This CIP proposes that Plutus be extended with native code
+implementations of certain mathematical operations which are useful for
+cryptography. These mathematical operations are used in the implementation
+of the Ed25519 public/private key signing protocol. Cardano already
+supports a native code implementation of verifying signatures created by
+the Ed25519 signing protocol, but it does not enable Plutus to scripts
+perform the underlying mathematical operations directly. Being able to do
+this would be useful for implementing other cryptographic protocols based
+on the Ed25519 mathematical operations.  Applications include verifying
+zero-knowledge proofs, such as in the context of implementing zk-rollups.
+
+## Abstract
+
+Extend Plutus with primitives for performing calculations over the
+Ed25519 curve and the corresponding finite field.  These operations are
+to include the basic group and field operations, as well as multiscalar
+multiplication.
+
+## Motivation
+
+CIP-0381 proposes inclusion of the Bls12-381 curve in Plutus. Bls12-381
+is a pairing-friendly curve. Not all applications of elliptic curves
+require a pairing-friendly curve. Choosing a non-pairing-friendly
+curve where a pairing-friendly curve is not required can lead to better
+usage of computing power.  The Ed25519 curve allows for more efficient
+operations as compared to the Bls12-381 curve.  Pairing-friendly curves
+require the use of more bits in order to achieve security (255 bits
+for Ed25519 vs 381 bits for Bls12-381). Therefore it would be helpful,
+for those applications which do not require a pairing-friendly curve,
+to include a non-pairing-friendly curve in Plutus.
+
+An example application of the Ed25519 curve is in verifying
+zk-SNARKs on-chain. Halo 2, for example, can be used with the Ed25519
+curve as the underlying curve. In its standard incarnation, Halo
+2 uses the Pasta curves (Pallas and Vesta). This is a 2-cycle of
+non-pairing-friendly curves.  The Pasta curves are specialized to a
+particular recursive proof strategy, as described in [Section 4.6 of the
+Halo 2 book](https://zcash.github.io/halo2/background/recursion.html/).
+For non-recursive proofs, the Pallas and Vesta curves are not required,
+and the Ed25519 curve suffices.
+
+Halo 2 over the Ed25519 curve offers short proofs and relatively low
+computational complexity of proof verification. These are the
+characteristics we are looking for in a zk-SNARK theory optimized for
+on-chain proof verification.
+
+Recursive proofs are very important in some applications of zk-SNARKs:
+zk-rollups, in particular.  Recursive proofs can be homogeneous (verifying
+a zk-SNARK produced by theory A in a zk-SNARK produced by theory A), or
+heterogeneous (verifying a zk-SNARK produced by theory A in a zk-SNARK
+produced by theory B).
+
+Halo 2's recursive Pasta curves proof strategy is heterogeneous: it
+uses proofs over the Pallas curve to verify proofs over the Vesta curve,
+and proofs over the Vesta curve to verify proofs over the Pallas curve.
+
+Orbis Labs has been researching ways of building recursive proofs
+off-chain and verifying them on-chain, for the purposes of zk-rollups. One
+way to do this is to use FRI-based zk-SNARKs for homogeneous recursive
+proofs. A downside of this is that proof sizes are expected to be
+substantially larger than the Cardano transaction size limit when using
+FRI, necessitating multiple transactions to verify a proof. Another
+downside of this is that for recursive FRI proofs, it makes sense to use
+a circuit-friendly hash (e.g., Poseidon or Rescue), but Cardano does not
+currently support these natively. Cardano-friendly hashes are those which
+are implemented as Plutus primitives: SHA2-256, SHA3-256, and Blake2b-256.
+
+The issue is that currently there is no hash function which efficient
+both in-circuit and on-chain.  A relatively simple workaround for this
+issue with homogeneous FRI recursion is to use heterogeneous recursive
+proofs, where an on-chain proof is generated using FRI with over a
+Cardano-friendly hash function, and it recursively verifies a proof
+generated using FRI over a circuit-friendly hash function. With this
+change of hash function heterogeneous recursive proving pattern, we can
+have efficient hashes both in-circuit and on-chain.
+
+More generally, we can decouple the choice of zk-SNARK theory for on-chain
+proof verification from the choice of zk-SNARK theory for off-chain
+recursive proof building, as long as we can reasonably efficiently
+convert one form of zk-SNARK to the other using recursive proving.
+
+For efficient off-chain proving, it makes sense to use a FRI-based
+zk-SNARK theory, since this leads to relatively fast proving times,
+at the cost of larger proof sizes, compared to Halo 2 for example. This
+also has the advantage that recursive proofs are relatively simpler to
+implement, because they do not require an accumulation scheme over a
+2-cycle of curves. FRI allows for homogeneous recursive proving.
+
+For efficient on-chain proof verification, it would make sense to use
+an elliptic curve based zk-SNARK theory, such as Halo 2, since this
+leads to relatively small proof sizes, potentially allowing for a proof
+to verified in a single Cardano transaction.  However, realizing this
+possibility requires primitives for a suitable choice of elliptic curve,
+one which is amenable to efficient proof verification.
+
+For realizing Halo 2 proof verification on-chain, we would want primitives
+for Pasta curves. However, Pasta curves are not the most ideal choice of
+curve for proofs that will not be recursively input to other proofs. When
+this is not required, the Ed25519 curve is a better choice because using
+it reduces proof size and verification costs. When using FRI for off-chain
+recursive proof composition, this requirement is not present. Instead, we
+would have a zk-SNARK over an elliptic curve which verifies a FRI-based
+zk-SNARK, and that zk-SNARK over the elliptic curve would be the final
+proof in the tree of recursive proofs, the one which is posted and
+verified on-chain.
+
+On-chain Halo 2 proof verification would open the door to on-chain
+verification of more or less all zk-SNARKs, and not just those
+mentioned. Halo 2 is a flexible enough theory to encode computable
+functions and thus the verification algorithms of arbitrary zk-SNARK
+theories. Therefore this CIP should be seen as a step towards efficient
+on-chain verification of zk-SNARKs in general.
+
+That describes our particular motivation for wanting the Ed25519 curve in
+Plutus at Orbis Labs. Furthermore, we believe that the Ed25519 curve is a
+broadly useful cryptographic primitive, when one needs a cryptographically
+secure elliptic curve but one does not need a pairing-friendly curve or
+a 2-cycle of curves.
+
+
+## Specification
+
+Add to Plutus the following types:
+
+ * `Ed25519GElement`: the type of elements of the Ed25519 curve.
+ * `Ed25519FElement`: the type of elements of the finite field of order
+    2^255 - 19.
+
+Add the following functions:
+
+ * Basic group operations:
+    * `Ed25519_G_add :: Ed25519GElement -> Ed25519GElement -> Ed25519GElement`
+    * `Ed25519_G_neg :: Ed25519GElement -> Ed25519GElement`
+ * Basic field operations:
+    * `Ed25519_F_add :: Ed25519FElement -> Ed25519FElement -> Ed25519FElement`
+    * `Ed25519_F_mul :: Ed25519FElement -> Ed25519FElement -> Ed25519FElement`
+    * `Ed25519_F_neg :: Ed25519FElement -> Ed25519FElement`
+    * `Ed25519_F_recip :: Ed25519FElement -> Maybe Ed25519FElement`
+ * Vector space operations:
+    * `Ed25519_scale :: Ed25519FElement -> Ed25519GElement -> Ed25519GElement`
+    * `Ed25519_scale_and_add :: [Ed25519FElement] -> [Ed25519GElement] -> Ed25519GElement`
+ * Conversions:
+    * `Ed25519_G_serialise :: Ed25519GElement -> ByteString`
+    * `Ed25519_G_deserialise :: ByteString -> Maybe Ed25519GElement`
+    * `Ed25519_F_serialise :: Ed25519FElement -> ByteString`
+    * `Ed25519_F_deserialise :: ByteString -> Maybe Ed25519FElement`
+    * `Ed25519_F_to_integer :: Ed25519FElement -> Integer`
+    * `Ed25519_F_from_integer :: Integer -> Ed25519FElement`
+ * Equality comparisons:
+    * `eq :: Ed25519GElement -> Ed25519GElement -> bool`
+    * `eq :: Ed25519FElement -> Ed25519FElement -> bool`
+ * Identities:
+    * `Ed25519_G_zero :: Ed25519GElement`
+    * `Ed25519_F_zero :: Ed25519FElement`
+    * `Ed25519_F_one :: Ed25519FElement`
+
+This makes for two new types, 16 new functions, and three new constants.
+
+This CIP writes the Ed25519 elliptic curve group in additive notation.
+The vector space operations consider the Ed25519 curve as a vector
+space over the scalar field `Ed25519FElement`. This implies that there
+is a scalar multiplication operation, which is `Ed25519_scale`. This
+also implies that we can take linear combinations of vectors of curve
+elements, which is what `Ed25519_scale_and_add` does.
+
+The Ed25519 curve is the elliptic curve defined by the equation:
+
+```
+-x^2 + y^2 = 1 - (121665/121666) * x^2 * y^2
+```
+
+This is a twisted Edwards curve.
+
+Field elements are serialized in big endian notation, taking up 32
+bytes each.  This leaves one unused bit, which should be set to zero.
+
+Group elements can be serialized in compressed form (just the
+x-coordinate), or in uncompressed form (both the x-coordinate and
+the y-coordinate).  A group element encoding consists of 65 bytes in
+compressed form, or 129 bytes in uncompressed form. The first byte should
+have all bits except the three least significant bits set to zero. Let
+b0 denote the least significant bit, b1 the second least significant,
+and b2 the third least significant.
+
+ * b0 is 1 if and only if the group element is in compressed form. 
+ * b1 is 1 if and only if the element is the point at infinity.
+   (The rest of the encoding after b1 should be zero in case b1 1 is 1.)
+ * b2 is 1 if and only if the element is in compressed form and not the
+   point at infinity and the point is "positive," meaning that its y
+   coordinate is lexicographically greater than the y coordinate of the
+   other point on the curve with the same x coordinate.
+
+A compressed group element encoding consists of the one byte
+containing the three flags, followed by field element encoding of the x
+coordinate. An uncompressed group element encoding consists of the one
+byte containing the three flags, followed by two field element encodings,
+first the x coordinate and then the y coordinate.
+
+## Rationale
+
+The inclusion of `Ed25519_scale_and_add` is to allow for an efficient
+implementation of taking linear combinations of group elements. This
+is important for efficient proof verification for Halo 2's inner
+product argument. For example, this operation can be implemented using
+[Pippenger's algorithm](https://jbootle.github.io/Misc/pippenger.pdf).
+Likely, an efficient implementation of this operation would be useful
+for other applications of this curve, too.
+
+
+## Backward Compatibility
+
+There are no expected backward compatibility issues.
+
+## Test Cases
+
+Property test the group, field, and vector space axioms. Also property
+test that `Ed25519_scale_and_add` produces the same result as zipping
+the lists with `Ed25519_scale` and then folding them with `Ed25518_G_add`.
+
+Provide golden tests for serialization and deserialization. These are unit
+tests which provide explicit inputs to serialization and deserialization
+and explicit expectations as to the results. Also provide round trip
+property tests for serialization and deserialization.
+
+Provide round trip property tests for `Ed25519_F_to_integer` and
+`Ed25519_F_from_integer`.  The round trip properties for these functions
+are that
+
+```
+Ed25519_F_from_integer . Ed25519_F_to_integer = id,
+```
+
+and that for all integers `x`,
+
+```
+Ed25519_F_to_integer (Ed25519_F_from_integer x) ≡ x mod 2^255 - 19.
+```
+
+Provide property tests which check that the equality comparisons are
+equivalence relations (relexive, transitive, and symmetric).
+
+## Implementations
+
+Author is not aware of a Haskell binding to a fast and battle tested
+implementation of the Ed25519 curve. The first step to building an
+implementation would be to find or build such a binding. After that,
+the next steps would be to make Plutus depend on this binding and add
+the specified primitives to Plutus.
+
+## Copyright
+
+This CIP is licensed under Apache-2.0 by Orbis Labs (2022).