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

[morganthomas]

This proposal adds Plutus primitives for efficiently computing with Ed25519 curves.

---

(rendered proposal in branch)

[L-as]

I do wonder if we could somehow support arbitrary curves, e.g. some kind of curve point type that is parameterised by the properties of the curve, but I'm not sure how efficient such an implementation could be.

It seems like we can possibly reuse the approach, and possibly also the implementation, of https://hackage.haskell.org/package/elliptic-curve.

CC @michaelpj @iquerejeta

[L-as]

For pairings: https://hackage.haskell.org/package/pairing

https://github.com/orgs/adjoint-io has a lot of work in this field, there's no need for us to reinvent the wheel in a bad way.

[iquerejeta]

https://github.com/orgs/adjoint-io has a lot of work in this field, there's no need for us to reinvent the wheel in a bad way.

We would need to have a closer look to these implementations. For instance, we would need to know the reliability of these implementations. Have they been used elsewhere? Are they audited and by who? Have they been battle tested? Also, are they efficient?

Nonetheless, even if some of the questions above are answered negatively, we could use the same ideas to make the API generic, which uses more efficient backends (and not the haskell one).

[michaelpj]

I think the main barrier to a generic implementation is working out what the interface would look like in PLC and how it would be costed.

I'm a Haskell programmer, I love genericity as much as anyone. But sometimes it's best to do things the dumb way.

[L-as]

We can probably figure out some relation between curve parameters and cost. We should probably at least figure out whether it's feasible or not before adding more curves (after BLS381).

[iquerejeta]

I like the idea of introducing elliptic curve operations in plutus, as this would allow some interesting scripts. Thanks for opening the discussion. I've left some comments to be addressed, but I would also like the feedback from @davidnevadoc or @CPerezz on the motivation around the SNARKs.

On that note, I think it is also important to provide estimates of Halo2 proofs over Edwards25519. It is said that using pasta curves would be too inefficient. Are we sure this is not the case for Halo2 proofs over edwards25519? Do we have numbers of proof sizes and verification times for certain circuit sizes?

[iquerejeta]

Suggested change

	the Ed25519 signing protocol, but it does not enable Plutus to scripts
	the Ed25519 signing protocol, but it does not enable Plutus scripts to

[iquerejeta]

Is this the only application that these build-ins would be used for? If yes, would it be preferable to have the ristretto prime order group or would it be fine to work with the group defined over Edwards25519 which has cofactor 8?

[iquerejeta]

I don't quite understand this terminology of "zk-SNARK produced by theory A". Could you elaborate that a bit more?

[iquerejeta]

But do we need a hash function which is efficient both in-circuit and on-chain? Why would we need plutus scripts to understand the snark friendly hashes? Wouldn't it suffice to have the plutus scripts verify the proofs without requiring any snark friendly hash computation?

[iquerejeta]

Ah, I think I understood. Here you are saying that Cardano would need to understand the snark friendly hashes in order to verify the proof, as FRI based proofs require hash computation during the verify procedure. Is that right?

[iquerejeta]

maybe a link to FRI commitment schemes here, or at least some context of what they are, would be helpful.

[iquerejeta]

We also need a motivation of why we use a curve with cofactor 8 (such as the edwards curve) instead of one with cofactor 1 which is usually safer. This is for efficiency, as edwards curves are much more efficient. Nonetheless, I think it is necessary to explain the danger of having a group with cofactor 8. This makes me wonder if we also need built-in functions to check if the points are part of the prime order group or not. What do you think?

[iquerejeta]

I now see where the "extra" byte comes in from above, but it still should be 33 in compressed form and 65 in uncompressed form. However, I don't think this is the most efficient representation. We can use a representation that requires only 32 and 64 bytes. Also, due to the fact that we need to cost functions, I would stick to a single serialised representation (possibly the compressed one). Otherwise it would be hard to cost the function as the cost would differ for compressed and uncompressed group elements.

[iquerejeta]

or Strauss algorithm would also be an option, depending on the size of the vector size.

[iquerejeta]

Suggested change

	equivalence relations (relexive, transitive, and symmetric).
	equivalence relations (reflexive, transitive, and symmetric).

[iquerejeta]

So from integer computes the modular reduction? If that is the case, it should be mentioned.

[L-as]

What's up with the horrible CIP enumeration scheme?

[iquerejeta]

The numbers are only settled once the PR is accepted and merged. See here. As far as we are concerned, the numbering of this CIP is just temporal while we are doing the PR.

[michaelpj]

How many EC operations are needed to implement Halo proof verification? This was a concern already with the Bls primitives: the primitives themselves are already expensive, and if we need many of them to actually perform Halo verification, then we may still not have enough resources to do so. It would be sad to implement these primitives and then find out we still couldn't do the thing we actually wanted to do.

I'd also be interested in knowing how long it takes to verify a typical Halo 2 proof on typical consumer hardware. If it's in the order of milliseconds then we are in trouble.

[L-as]

@KtorZ I don't think @morganthomas is interested in pushing this further along.

[perturbing]

For fun and profit, I made a naive Ed25519 implementation in plutus from the other builtins as described in this proposal.

In general, I made the field as a Ring instance in plutus and the EC curve as an additiveGroup instance (this does not add the field recip function natively). I might add some El Gamal stuff with some zk proofs. The proofs I want to try onchain are: proof of correct encryption (DLEQ), and proof of knowing a private key of a public key (DLOG). I think these are viable since these require only comparing and adding EC points and hashes. And if not, they might be only viable in a hydra head, it has some application for games.

I implemented most tests but stopped at the benchmarking of the implementation since it is not clear to me what operations will be used onchain for a Halo 2 proof. I hope that the scale function (adding the base point n times to itself) is not needed in these proofs, as this is a costly function onchain! Furthermore, I suppose this is not the case since it is only used for key generation? To reiterate, it's not a good idea to use this naive implementation for key generation.

I might improve the implementation by considering the projective representation of the points (I read that this is computational better). @iquerejeta maybe you know if this true/significant?

[iquerejeta]

That's supper cool. Curious to see the outcome of the benchmarks.

With respect to the point representation for scalar multiplication, current implementations do not use a single representation, but instead mix coordinate systems for more efficiency. Projective points allow for more efficient doubling of points, while 'extended representation' allow for more efficient addition. Therefore, when performing a scalar multiplication (computed out of a series of doubling and additions), one switches between the different representations. Another efficiency trick that one can find in current implementations, is that scalar multiplication with variable base (same holds with the base point), one first calculates a lookup table, and then proceeds with a series of point doublings and additions (see here for example). Some of these tricks are mentioned in the original ed25519 paper, but you can also find more details in some of the implementations (I usually look dalek's implementation, which is very well documented, or libsodium, which is based in DJB's reference implementation). These tricks should give you a considerable improvement, and some of these tricks are also useful for computing multiscalar multiplication efficiently (a_1 * P_1 + a_2 * P_2 + ... + a_n * P_n, where a_i and P_i are scalars and points respectively).

With respect to the scale function (n * P, or adding P n times to itself), these operations are required in both Halo2 and simpler zk proofs (such as DLEQ or DLOG). When you verify a DLOG proof, for H = x * B, the final check is s * B ?= c * H + R, where R, c, s are the announcement, challenge and response of the zk proof (or sigma-protocol), and ?= is an equality check.

[KtorZ]

Closing this PR for the sake of housekeeping. @morganthomas if you have any interest in pursuing this please re-open.

[KtorZ]

@iquerejeta you may also have an interest in championing this CIP instead?

[rphair]

Note @iquerejeta @KtorZ @imikushin there's some interest expressed on the Cardano Forum in reviving this proposal: https://forum.cardano.org/t/cip-elliptic-curve-operations-and-other-math-useful-for-zk-proof-verification-in-plutus/113624/6