IntersectMBO / plutus

The Plutus language implementation and tools
Apache License 2.0
1.57k stars 479 forks source link

Halo 2 support in interpreter #4261

Closed L-as closed 1 year ago

L-as commented 2 years ago

Describe the feature you'd like

Support for verifying Sonic zk-SNARKs Halo 2 proofs on-chain.

Describe the approach you would take to implement this

Somehow integrate https://github.com/adjoint-io/sonic? https://github.com/zcash/halo2

Additional context / screenshots

If possible, we (MLabs) would like to cooperate with IOHK on this, as we want to make use of ZKPs on-chain, i.e. we are willing to do the full work required for this feature.

L-as commented 2 years ago

After thinking about this some more, it doesn't have to be Sonic. It could be PLONK, or whatever IOHK thinks fits best.

michaelpj commented 2 years ago

Supporting a ZK primitive seems like a good idea indeed. It looks like PLONK is probably the way forward. But someone who knows about it needs to actually propose what the primitive should be and how people would use it.

L-as commented 2 years ago

I've looked into this for a few more days, and in the end, I believe that Halo 2 is the best choice. The biggest reason by far is that it doesn't necessitate trusted setups, which means a huge reduction in the complexity of a possible implementation for Cardano compared to PLONK AFAICT. In addition, it supports recursive proofs, which is a very powerful tool. The proof sizes are seemingly bigger, but I currently believe that the trade-off is worth it.

The biggest issue is that the current implementation for Zcash appears not to be completely ready, although they're using it in Orchard.

They're supposed to use this in production on 2022-01-17 (https://z.cash/support/schedule/), and in that case, I assume that it's ready enough for usage in Cardano.

Darlin is another possible solution, but they seemingly do not have an implementation yet.

Pickles also exists, and they seemingly have an OCaml implementation that is used today, but I couldn't find much documentation on it. Making bindings to Zcash's Halo 2 implementation will likely also be easier, since it's Rust.

Some references:

L-as commented 2 years ago

I am still not completely sure how a possible integration into Plutus would look, but I'll try making some bindings to it, and see how it works.

michaelpj commented 2 years ago

I'd like to see some consultation with other potential users of ZK primitives before we go with something.

L-as commented 2 years ago

Definitely. Looking at https://iohk.io/en/research/library/ I can see that IOHK already has a couple of papers in this subject. Perhaps someone at IOHK has some strong opinions?

morganthomas commented 2 years ago

I think it would be helpful to include the following cryptographic primitives:

morganthomas commented 2 years ago

Another primitive that could be helpful here is polynomial division for rings of polynomials over finite fields of prime order.

michaelpj commented 2 years ago

Please open another issue if you want to talk about other primitives than ZK ones.

morganthomas commented 2 years ago

I think there may have been a misunderstanding here . What I'm suggesting is that what I listed above are suitable primitives for implementing ZKPs on Cardano. An alternative would be to provide a verifier primitive for a specific ZKP strategy. On the one hand, the latter approach would probably be more efficient, but on the other hand, it would tie users to a specific choice of ZKP strategy.

morganthomas commented 2 years ago

That said, I would be happy with a single additional primitive which is a verifier for PLONK zkSNARKs.

morganthomas commented 2 years ago

I am willing to assign one of the engineers working under me to add a Halo 2 proof validator primitive to Plutus, consistent with what @L-as and I asked for here.

michaelpj commented 2 years ago

A change like this needs a proper proposal. At least we need:

michaelpj commented 2 years ago

Alternatively, if you could make a similar proposal for the corresponding numeric primitives that you want, that might also be viable.