feat: MockProver cell override #352
Conversation
|
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? |
halo2_frontend/src/dev.rs
Outdated
|
|
||
| region.assign_advice(|| "a0", config.a, 0, || Value::known(Fp::from(3)))?; | ||
| region.assign_advice(|| "a1", config.a, 1, || Value::known(Fp::from(9)))?; | ||
| region.assign_advice(|| "a2", config.a, 2, || Value::known(Fp::from(10))) |
There was a problem hiding this comment.
I would suggest having a circuit that assigns a correct witness, make sure the mock prover can verify it, and then start manipulating the advices / instances to check that it now gives errors when verifying with the mock prover.
This flow better shows how a negative test would go: start from a correct assignment that passes, make a hypothesis about a witness that should not pass, and make sure it doesn't.
|
I want to share my thoughts on @adria0's comment
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: 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.
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.
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.
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: halo2/halo2_proofs/tests/shuffle.rs Line 336 in 32599e8 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! |
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. |
That's fair. I agree that this PR doesn't resolve the universal methodology for negative tests but I think:
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. |
|
@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. |
teddav
force-pushed
the
mockprover-cell-override
branch
from
70182aa
to
7398d58
Compare
| // and now we try to trick the verifier | ||
| // we assign on row 0 `Fp - 3`, which is also a square root of 9 | ||
| // but will overflow the prime field | ||
| let sqrt_9 = Fp::zero() - Fp::from(3); |
|
@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 @teddav, please take a look to https://docs.codecov.com/docs/adding-the-codecov-token |
teddav
force-pushed
the
mockprover-cell-override
branch
from
7398d58
to
851b54f
Compare
|
thanks for approving the PR 😊 |
This PR adds the ability to modify cells in the MockProver and act like a "malicious prover".
This is related to this issue: zcash#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