search

privacy-scaling-explorations / halo2

https://privacy-scaling-explorations.github.io/halo2/
Other
201 stars 121 forks source link

feat: MockProver cell override #352

Closed teddav closed 2 months ago

teddav commented 3 months ago

This PR adds the ability to modify cells in the MockProver and act like a "malicious prover".
This is related to this issue: https://github.com/zcash/halo2/issues/280

I added a test to show how this can be used. I can add more doc/tests if needed.

This is a first shot at it, I can try to improve it based on comments

adria0 commented 3 months ago

While at first glance it's ok, and soundness is something that needs to be tested, but I'm not sure finding where this could be beneficial if not is a trivial example:

Do you have some specific use case where there methods are usefull?

Let's me say that testing bad witness values are a real pain and needs to be adressed somehow, but probably needs some methodology first and then the according code changes to allow its usage.

Edit: I just seen your nice halo2 impl https://dev.to/teddav/tornado-cash-with-halo2-62b ! Have you tried to apply your PR to test it?

ed255 commented 3 months ago

I want to share my thoughts on @adria0's comment

While at first glance it's ok, and soundness is something that needs to be tested, but I'm not sure finding where this could be beneficial if not is a trivial example:

  • If the developer of the chip / state machine wants to do the test, I think that is just easier to output modified witness

I don't think that's easy, as it needs custom boilerplate in the chip / state machine / gadget just to be able to override values. It can be cumbersome to propagate this override data from the test to the actual assignment code. For example, take a look at this circuit from the zkevm-circuits that performs overrides:

Here's the test itself: https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/fe3a814558fa09951fa40adf07faffe024b47283/zkevm-circuits/src/state_circuit/test.rs#L409-L411 It requires extending the circuit with a field to store the overrides: https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/fe3a814558fa09951fa40adf07faffe024b47283/zkevm-circuits/src/state_circuit.rs#L466 It requires extra code in the synthesize to assign the overrides: https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/fe3a814558fa09951fa40adf07faffe024b47283/zkevm-circuits/src/state_circuit.rs#L595-L607

Having these two extra methods in the MockProver allows following the same pattern for negative testing with less boilerplate on the circuit. And the extra methods for the MockProver are very simple and lightweight, so I think it leads to a more clear negative testing.

  • If you are using an external chip / state machine, it's tricky to guess which column/row you have to poke, and breaks a little bit the encapsulation principle, and, well, tests needs to be part of the component not, something external.

I agree that it can be tricky to guess which column/row to poke, but I don't think this invalidates the MockProver cell override methods. Each chip / component can have negative testing, and they can use the MockProver cell override methods. I think negative testing works much better with unit tests of circuits that contain a single component; so in that case you would not do a negative test of a big circuit by poking an internal component that is defined in a different module.

  • If using some kind of cell manager (cell allocator, chiquito, halo2lib, powdr), no (direct) way to know where is the original column / row is.

I agree, and again I don't think this invalidates this PR. Negative testing requires assigning invalid witnesses, no matter if you're using a cell allocator or not. A component that uses a cell allocator can just collect metadata during assignment that a test can use to know which cells to override, and doing the override is easier with the MockProver support than having a custom assignment code for overrides.

Do you have some specific use case where there methods are usefull?

Just to give examples, one would be the negative testing of the state circuit in zkevm-circuits that I mentioned before.

Another example would be this negative test case for the shuffle API: https://github.com/privacy-scaling-explorations/halo2/blob/32599e898a62b21647c55e93f689e454b093c6fd/halo2_proofs/tests/shuffle.rs#L336 Currently the circuit keeps two list of values (original and shuffled) and the negative test changes the shuffled list. This follows the pattern of the override. In this case the change would be minimal, but I just wanted to show that it's following the same pattern. A real circuit may not have as inputs the original and shuffled list; maybe it has the original list and builds the shuffle by sorting the original; in that case doing an overwrite without MockProver support would be harder.

Overall I agree that having the MockProver cell override doesn't give you the final solution for negative testing in all cases, but I think it's a very useful (necessary even) component to do negative testing!

adria0 commented 3 months ago

Overall I agree that having the MockProver cell override doesn't give you the final solution for negative testing in all cases, but I think it's a very useful (necessary even) component to do negative testing!

This is my main point, I'm not "against" this PR, but I think that does not solve the problem that needs to be solved, that is lack of methodology for negative tests.

IMO we have to check how it works in a real case, in the theoretical side I agree that could be usefull. So, it needs a little of extra checking, I would say.

ed255 commented 3 months ago

Overall I agree that having the MockProver cell override doesn't give you the final solution for negative testing in all cases, but I think it's a very useful (necessary even) component to do negative testing!

This is my main point, I'm not "against" this PR, but I think that does not solve the problem that needs to be solved, that is lack of methodology for negative tests.

That's fair. I agree that this PR doesn't resolve the universal methodology for negative tests but I think:

IMO we have to check how it works in a real case, in the theoretical side I agree that could be usefull. So, it needs a little of extra checking, I would say.

To me, this PR is already useful for real cases. For that reason, and also because I think this is a useful component for more complex negative test cases, I'm in favor of merging this new MockProver feature as is (maybe extending / changing the tests if necessary, even changing the API if necessary). I think it's not fair to put the burden of solving negative testing for all cases on this PR, because then it's very hard to make progress.

Although I agree that with this PR merged, the issue of "universal methodology for negative testing" is not resolved.

teddav commented 3 months ago

@adria0 I completely agree that this is not a final solution, that's what i was saying in my first comment. As @ed255 is saying, this is a way to get started on this topic and introduce tools for negative testing. I'd be happy to have a discussion (on discord?) about how we want to address it and what the next step could be.
Based on @ed255 suggestion, i'm going to add some better tests and I agree that this could be merged as it is and improved after

ed255 commented 2 months ago

@adria0 the coverage github task failed. Maybe it doesn't work with PRs using forked repositories?

adria0 commented 2 months ago

@adria0 the coverage github task failed. Maybe it doesn't work with PRs using forked repositories?

I did not know this, it seems that now needs an CODECOV_TOKEN in the forked repo, some time ago this was not mandatory.

@teddav, please take a look to https://docs.codecov.com/docs/adding-the-codecov-token

teddav commented 2 months ago

thanks for approving the PR 😊 @adria0 i just updated the codecov action to v4 to see if it fixes it. see here: