Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed

Conversation

morganthomas
Copy link

@morganthomas morganthomas commented Jul 27, 2022

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


(rendered proposal in branch)

@L-as
Copy link
Contributor

L-as commented Jul 28, 2022

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
Copy link
Contributor

L-as commented Jul 28, 2022

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
Copy link
Contributor

iquerejeta commented Aug 1, 2022

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
Copy link
Contributor

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
Copy link
Contributor

L-as commented Aug 1, 2022

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).

@KtorZ KtorZ changed the title CIP-2551? | Ed25519 curve CIP-2551? | Ed25519 Elliptic Curve Group Primitives in Plutus Core Aug 2, 2022
Copy link
Contributor

@iquerejeta iquerejeta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Comment on lines +68 to +70
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).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Comment on lines +87 to +88
The issue is that currently there is no hash function which efficient
both in-circuit and on-chain. A relatively simple workaround for this
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?


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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

multiplication.

## Motivation

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Comment on lines +204 to +210
* 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

```

Provide property tests which check that the equality comparisons are
equivalence relations (relexive, transitive, and symmetric).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

and that for all integers `x`,

```
Ed25519_F_to_integer (Ed25519_F_from_integer x) ≡ x mod 2^255 - 19.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@L-as
Copy link
Contributor

L-as commented Aug 2, 2022

What's up with the horrible CIP enumeration scheme?

@iquerejeta
Copy link
Contributor

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.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@KtorZ KtorZ added the State: Waiting for Author Proposal showing lack of documented progress by authors. label Nov 30, 2022
@L-as
Copy link
Contributor

L-as commented Dec 28, 2022

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

@perturbing
Copy link
Collaborator

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
Copy link
Contributor

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
Copy link
Member

KtorZ commented Jan 17, 2023

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

@KtorZ KtorZ closed this Jan 17, 2023
@KtorZ
Copy link
Member

KtorZ commented Jan 17, 2023

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

@rphair
Copy link
Collaborator

rphair commented Jan 31, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
State: Waiting for Author Proposal showing lack of documented progress by authors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants