Dhole / polyexen

Polynomial Expression Engine
34 stars 8 forks source link

Support challenges #6

Open georgwiese opened 5 months ago

georgwiese commented 5 months ago

It seems challenges are implemented for the most part, but some code is commented out (and instead of querying a challenge from Halo2, it returns a constant).

I tried just commenting it in and it compiles and looks like it could work! I'm wondering what's needed to finish it?

Dhole commented 5 months ago

I guess you mean you "uncommented" the code and it seemed to work. I've checked it myself and it seems correct, I'm not sure why I left it commented. Nevertheless there could be an inconsistency: you specify a list of challenges in Plaf.info where you set the phase of each one, and then you can also set the phase in the Var::Challenge used in an expression. I've added an assert to catch this situation (and perhaps it would be better to remove the phase field from Var::Challenge in the future).

I haven't tested this; I would like to do that but I'm a bit busy this week and next week, but you can test it yourself from this branch: https://github.com/Dhole/polyexen/tree/feature/halo2-backend-challenge (which is just the uncommented code and the assert).

I don't think there's anything else needed to finish this, but I can't really confirm that yet as I'd like to test in in two weeks.

georgwiese commented 5 months ago

I tested it and it seems like everything is working as I'd expect! See https://github.com/powdr-labs/powdr/pull/1050.

In this prototype, I'm assuming that I know the challenge in advance, so I can pass the entire witness to PlafH2Circuit which is then passed to Halo2, which then calls synthesize once for each phase.

Have you thought about how that could be done properly? We would need some way to do the second-phase witness generation after the first challenges are available. For example, PlafH2Circuit could store a callback that it calls with the available challenges and returns additional witness columns. That sounds like a bigger API change though.

Dhole commented 5 months ago

In this prototype, I'm assuming that I know the challenge in advance, so I can pass the entire witness to PlafH2Circuit which is then passed to Halo2, which then calls synthesize once for each phase.

Ah, that must have been the reason why I left the code commented, because there's no way to properly calculate the witness without knowing the challenge, so I hardcoded a mock challenge!

In a real circuit you will not know the challenge in advance, you'll only know it after committing to the witnesses of all phases up to each challenge.

Have you thought about how that could be done properly? We would need some way to do the second-phase witness generation after the first challenges are available. For example, PlafH2Circuit could store a callback that it calls with the available challenges and returns additional witness columns. That sounds like a bigger API change though.

You're totally right, to do this properly we require a back and forth between the frontend (powdr) and the backend (halo2 proving system). The callback is an option, although I'm more inclined on doing multiple calls like this:

-> Send witness phase 0
<- Get challenges after phase 0
-> Send witness phase 1
<- Get challenges after phase 1
...
-> Request calculate proof
<- zk proof

This approach can't easily be done with the legacy halo2 API, but it's easy to do with the new frontend-backend split API https://github.com/privacy-scaling-explorations/halo2/pull/254 although this new API hasn't been tested enough yet.

Also it requires an API change to Plaf as well.

I can work on updating Plaf to work with the new frontend-backend split API and also adding support for multi-phase proving in two weeks.

leonardoalt commented 5 months ago

Do you only depend on halo2 via the polyexen crate? Or do you import halo2 from other paths as well?

We use polyexen/Plaf for the circuit part, and then use PSE's halo2_proofs directly for proof and verification.

@Dhole do you think it makes more sense for us to do this directly via PSE's Halo2 new frontend-backend split, or via polyexen?

Dhole commented 5 months ago

@Dhole do you think it makes more sense for us to do this directly via PSE's Halo2 new frontend-backend split, or via polyexen?

This is a good point. Perhaps you can skip Plaf (and thus polyexen) and directly connect to the halo2 backend. You'll end up with a lighter implementation and reduce the number of dependencies. The Plaf struct and the struct that the halo2 backend receives are not too different. You can take a look at an example of how the frontend-backend split API is used here: https://github.com/privacy-scaling-explorations/halo2/blob/0b75a92a1c9c59b19304632e0bac6c788190a3aa/halo2_proofs/tests/frontend_backend_split.rs#L590-L594

In particular, this is the struct that contains the circuit definition that the backend expects, and the rest is just passing witnesses as vectors during proving time. https://github.com/privacy-scaling-explorations/halo2/blob/0b75a92a1c9c59b19304632e0bac6c788190a3aa/halo2_middleware/src/circuit.rs#L159

The only downside to going that route now is that the frontend-backend split is very recent and not very tested, and may suffer updates in the short term requiring changes in your integration (hopefully not many changes). But for the mid term I think transitioning to using directly the halo2 backend makes a lot of sense.