CPerezz commented 6 months ago

I've seen this message in the Halo2Ecosystem Discord (the guy also posted it in the PSE Discord):

Basically, it seems like 0 values are discarded and not checked against lookup tables. So if I want to check some values against a lookup table and one of those values is 0, the check is going to pass even if 0 is not in the lookup table. I wrote a quick poc to show it: https://github.com/teddav/poc-underconstrained-halo2/blob/main/tests/prove.rs

Thanks in advance @teddav for the ping.

We should analyze and confirm the bug indeed exists and move on from there.

cc: @davidnevadoc @ed255

teddav commented 6 months ago

thanks @CPerezz, let me know if you can confirm (or not).
just to add to the issue: the poc is just showing the issue for the MockProver but it's also present in the real prover
here's the original discord message

if you're ok with it (and maybe with a bit of help), i'd love to push the fix and make my first contribution to halo2 😊

ed255 commented 6 months ago

I think this is what's going on: In your test you set k=4, which means each column has 2^4 = 16 rows On the rangecheck_config.lookup_table you're only assigning 6 rows, and the remaining rows get the default value which is 0.

So the result is this:	offset	advice
0	a	2
1	b	3
2	c	4
3	0	5
4	0	6
5	0	7
6	0	0
7	0	0
8	0	0
9	0	0
10	blind	0
11	blind	0
12	blind	0
13	blind	0
14	blind	0
15	blind	0

And the lookup constraint is like for every i, advice[i] in lookup_table Since the lookup table contains zeroes, and advice that is zero fulfills the lookup.

This would explain why you can set 0 in a, b or c and the lookup check still passes.

Nevertheless there's something I'm a bit clueless about right now: halo2 adds blinding values a the bottom of advice columns. From the way the lookup is defined in your circuit, it should fail on the blinding rows. But it doesn't fail (I also tried running the test_pass using the real prover and it passes. I don't understand why, so I must be missing something.

I found what's going on. It's explained here https://zcash.github.io/halo2/design/proving-system/lookup.html#zero-knowledge-adjustment Basically the lookup argument that halo2 generates introduces an extra selector expression that enables it only on the non-blinding rows. This means that following the previous table, the lookup constraint would be more like this: for every i in 0..10, advice[i] in lookup_table[0..10].

Proposed solution

From my point of view the bug is not in the lookup_any API, but instead it's in your circuit because the constraints it defines don't achieve your intention. Notice that your constraints don't say that only advice rows 0, 1 and 2 should be range constrained, it says that all advice rows should be range constrained, and the advice has many zeroes after row 2.

So I propose 2 changes.

Only enable the lookup at rows 0,1,2

You can achieve this by introducing a fixed column that is 1 at rows 0,1,2 and 0 otherwise. And use it as a selector for the lookup input expression

a) Pad the lookup table

So that it doesn't have 0 values in the non-blinding rows, and then the lookup won't succeed with the 0 input value.

b) Accept 0 in the lookup table

Redesign the circuit such that 0 is a valid number in your lookup table. This way you don't need to think about the number of non-blinding rows.

Solution A

offset	s	advice	lookup_table
0	1	a	2
1	1	b	3
2	1	c	4
3	0	0	5
4	0	0	6
5	0	0	7
6	0	0	7
7	0	0	7
8	0	0	7
9	0	0	7
10	0	blind	0
11	0	blind	0
12	0	blind	0
13	0	blind	0
14	0	blind	0
15	0	blind	0

Lookup: [s * advice, lookup_table] Notice that lookup table repeats the last value until the last usable row

Solution B

offset	s	advice	lookup_table
0	1	a	0
1	1	b	1
2	1	c	2
3	0	0	3
4	0	0	4
5	0	0	5
6	0	0	0
7	0	0	0
8	0	0	0
9	0	0	0
10	0	blind	0
11	0	blind	0
12	0	blind	0
13	0	blind	0
14	0	blind	0
15	0	blind	0

Lookup: [s * (advice - 2), lookup_table] Notice the -2 shift which moves the range 2..8 to 0..6 to match the lookup table.

teddav commented 6 months ago

I had a discussion with @ed255 to understand what we could do.
The issue is indeed present in lookup_any but not in lookup. The reason is that we should consider lookup_any as an "insecure" version of lookup.
lookup uses TableColumn which adds many more checks, and pads the column if it's not full.
lookup_any was made to work on any type of column and therefore cannot have the same checks

What could we do? Easy:

add a warning (where?) when using lookup_any so that users are aware of it. Especially if the user is using it with a Fixed column (in that case it makes more sense to use lookup)
make it more clear in the doc (maybe add some more code examples too)

Harder/To discuss: see how we could make lookup_any more secure by adding some checks

I do still think there is something to be improved in the lookup_any because of the fact that Unassigned cells in the lookup table are considered to be 0 (that's part of where the bug comes from)

ed255 commented 5 months ago

In this PR https://github.com/privacy-scaling-explorations/halo2/pull/347 we added a check for this particular case (which can be disabled): https://github.com/privacy-scaling-explorations/halo2/blob/d7c6279d6d9fe7904ac6e50beae51ba17e7b02d8/halo2_frontend/src/plonk/circuit/constraint_system.rs#L441-L443 So this issue should be resolved now

privacy-scaling-explorations / halo2