feat: add assertion for dynamic lookup #347

guorong009 · 2024-06-04T03:07:17Z

Description

Dynamic lookup, which uses the lookup_any, should have the assertion to prevent use of Advice/Instance column without extra Fixed column or Selector.
This PR adds assertion to lookup_any api.

Related issues

Resolve Add an assertion to prevent dynamic lookups without selectors/fixed #224 Possible bug in Lookup-any API #335

Changes

add assertion of table_expression containing fixed col or selector in lookup_any api
add extra check that table_expression should NOT be one simple fixed col, in lookup_any api
update/add the unit tests

codecov-commenter · 2024-06-04T03:08:43Z

Codecov Report

Attention: Patch coverage is 97.19222% with 13 lines in your changes missing coverage. Please review.

Project coverage is 82.68%. Comparing base (b4d1c4c) to head (6205dfc).
Report is 4 commits behind head on main.

Files	Patch %	Lines
halo2_frontend/src/dev.rs	96.94%	11 Missing ⚠️
...o2_frontend/src/plonk/circuit/constraint_system.rs	97.22%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #347      +/-   ##
==========================================
+ Coverage   81.89%   82.68%   +0.79%     
==========================================
  Files          82       83       +1     
  Lines       17010    17955     +945     
==========================================
+ Hits        13930    14846     +916     
- Misses       3080     3109      +29

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

teddav · 2024-06-04T17:33:53Z

halo2_frontend/src/plonk/circuit/constraint_system.rs

+                // this check ensures that one dedicated `Fixed` column or `Selector` is used
+                // for enabling the real table rows of the column, which is used as `TableColumn` role.
+                // otherwise, we get the soundness error, like https://github.com/privacy-scaling-explorations/halo2/issues/335
+                if table.degree() < 2 {


sorry if im wrong, but i don't understand how the degree should be more than 2?
shouldn't it be the opposite? we want it to be <2

halo2/halo2_frontend/src/plonk/circuit/expression.rs

Line 869 in b4d1c4c

pub fn degree(&self) -> usize {

you say in the comment that you expect the column to be "Fixed column or Selector" but I thought the purpose of lookup_any was to allow a lookup into Advice column. If we're looking up into a Fixed column, we might as well use regular lookup()

shouldn't it be the opposite?

No, the degree of table expression should be 2.
In other words, it should be like following:

meta.lookup_any(|cells| { let default = Expression::constant(F::ONE); let s_lookup = meta.query_selector(...); let to_lookup = meta.query_advice(...); let s_ltable = meta.query_selector(...); let ltable = meta.query_advice(...); vec![ ( s_lookup * to_lookup + (Expression::constant(F::ONE) - s_lookup) * default, s_ltable * ltable ) ] }

In the example, the degree of s_ltable * ltable is 2. Since the degree of selector & advice column is 1, and the degree of its product is sum of degrees.

you say in the comment that you expect the column to be "Fixed column or Selector" but I thought the purpose of lookup_any was to allow a lookup into Advice column.

I meant that extra fixed column or selector SHOULD be accompanied with table column(in lookup_any, the advice column).
In other words, when using lookup_any, the advice/fixed column used for table role should be accompanied with another fixed column or selector to indicate which rows are used as table rows.

ed255 · 2024-06-06T13:36:09Z

halo2_frontend/src/dev.rs

+                    //      `Selector` is required to be enabled, in order to indicate the lookup table values.
+                    //
+                    //  The following diagram shows the example circuit.
+                    //  (This is NOT a real `FaultyCircuit` instantiation we have in this test. Just borrow of its config.)


I'm a bit confused by this statement. Could you clarify this?

Also I'm a bit confused about this test 😅, it assigns two regions, and the table is assigned twice (once per region). I think it would be more clear with 3 regions:

1 region to assign the table once

1 region to enable q and assign the inputs a: "good"

1 region to enable q without assignment of a: "faulty"

Anyway, I guess you updated this test so that the the new failure check doesn't trigger, right?

Thanks for letting me know! @ed255

I'm a bit confused by this statement. Could you clarify this?

Yes, I see that the new test and example circuit explanation confuses people. 😅
I will improve the statement.

Anyway, I guess you updated this test so that the the new failure check doesn't trigger, right?

Yes, I updated the test so that it does lead to wrong assignment error, not the lookup_any check error.

ed255 · 2024-06-06T13:45:50Z

halo2_frontend/src/plonk/circuit/constraint_system.rs

+                // this check ensures that one extra, dedicated `Fixed` column or `Selector` is used
+                // for enabling the real table rows of the column, which is used as `TableColumn`.
+                // otherwise, we get the soundness error, like https://github.com/privacy-scaling-explorations/halo2/issues/335
+                if table.degree() < 2 {


I think this check is not effective in certain scenarios.

For example, let's say you build a table expression by multiplying two advice queries. The degree is 2, but it's still problematic. This would be a false negative.

Imagine you have a dynamic table that combines fixed and advice columns. In that case it can be OK for some table expressions to be degree 1. This would be a false positive.

As an example of the second case, take a look at the block_table from the zkEVM CE project: https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/specs/tables.md#block_table
The tag and index columns are fixed and the valueLo and valueHi are advice.
Assume that the tag values go from 1 to N (and the assignments to the unused rows are 0)

now we want to do a lookup to Time for example. The input expression would be [q * Time, 0, q * in_value, 0] and the table expression would be [Time, 0, value, 0]. This table expression can only match a valid row, because invalid rows have Tag=0 so they are [0, ... ], and Time != 0.

So I think the proper check would be to make sure that at least 1 fixed query exists in some of the table expressions. Then we must forbid that all table expressions have 0 fixed queries.

Ah, thanks for pointing out specific cases.
Yes, I totally agree with your idea.
Will improve the check.

guorong009 · 2024-06-07T06:21:21Z

@ed255 @teddav
I updated the assertion check - table_expression must include either fixed col or selector.
Pls re-check the updates.

teddav · 2024-06-07T09:52:11Z

thanks for the PR @guorong009 . it looks good to me, but it doesn't fix #335 , right?
because if you're using a fixed column as the lookup table, the check selector | fixed still passes and no selector is needed.
maybe it could be a good PR to also add the warning i was talking about here: #335 (comment) : if the lookup is a fixed column, and there is no selector -> display a warning saying it's better to use lookup() instead of lookup_any()

guorong009 · 2024-06-10T03:23:35Z

thanks for the PR @guorong009 . it looks good to me, but it doesn't fix #335 , right? because if you're using a fixed column as the lookup table, the check selector | fixed still passes and no selector is needed. maybe it could be a good PR to also add the warning i was talking about here: #335 (comment) : if the lookup is a fixed column, and there is no selector -> display a warning saying it's better to use lookup() instead of lookup_any()

How about this patch - c80022a ? @teddav @ed255
I think it is insufficient to just give off warning message.
For example, this example causes soundness error, if not panic in configure stage.
In other words, if I put simple warning message here, the circuit still passes all the check & produces verification success.
It could be worse, since essentially it should not succeed to verify.
Hence, I add the panic when the table column of lookup_any api has only fixed column.

ed255 · 2024-06-10T10:03:40Z

halo2_proofs/tests/frontend_backend_split.rs

@@ -42,7 +42,7 @@ struct MyCircuitConfig {

    // Copy constraints between columns (a, b) and (a, d)

-    // A dynamic lookup: s_lookup * [1, a[0], b[0]] in s_ltable * [1, d[0], c[0]]
+    // A dynamic lookup: s_lookup * [a[0], b[0]] in s_ltable * [d[0], c[0]]


Sorry but I think my suggestion here #347 (comment) is not complete.

Take a look at this example based on the updated lookup expressions of this circuit:

offset s_lookup a b s_ltable c d

0 1 0 0 1 2 4

1 1 2 4 1 3 9

2 0 0 0 0 0 0

At offset 0 we have input 1 * [0, 0] = [0, 0] which matches the table at offset 2 0 * [0, 0] = [0, 0] but that's undesirable, because we are matching a table entry that has s_ltable = 0.

So checking that at least one table expression uses a selector/fixed is not enough. Maybe the correct check is that at least one table expression is a selector/fixed.

Thanks for catch! @ed255
So, I think we reached a point that the lookup_any api should include the table expression which is a selector/fixed.
Otherwise, it can be used for soundness error by malicious prover.
Also, from #335 & #347 (comment), we can see that when the single fixed col is used for lookup_any api, we should recommend user to use the lookup api.
Then, the summary is that we don't have any way to prevent the abuse of lookup_any api use, and should remove lookup_any api. right?

ed255 · 2024-06-10T10:07:10Z

halo2_frontend/src/plonk/circuit/constraint_system.rs

+                if table.degree() == 1 {
+                    panic!("table expression containing only fixed column supplied to lookup_any argument, should use `lookup` api instead of `lookup_any`");
+                }


Note that this is checking a condition for any table expressions. But actually we want to check that all table expressions are a fixed/selector column query.

Hmm, I think the current checks on lookup_any api are for all table expressions. Am I wrong?

pub fn lookup_any<S: AsRef<str>>( &mut self, name: S, table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, Expression<F>)>, ) -> usize { let mut cells = VirtualCells::new(self); let table_map = table_map(&mut cells) .into_iter() .map(|(mut input, mut table)| { if input.contains_simple_selector() { panic!("expression containing simple selector supplied to lookup argument"); } if table.contains_simple_selector() { panic!("expression containing simple selector supplied to lookup argument"); } if !table.contains_fixed_col_or_selector() { panic!( "table expression supplied to lookup_any argument must include fixed column or selector" ); } if table.degree() == 1 { panic!("table expression containing only fixed column supplied to lookup_any argument, should use `lookup` api instead of `lookup_any`"); } input.query_cells(&mut cells); table.query_cells(&mut cells); (input, table) }) .collect(); let index = self.lookups.len(); self.lookups .push(lookup::Argument::new(name.as_ref(), table_map)); index }

It iterates every input and table expressions, and do the check.
So, if any of table expression do not match the check, it panics.

guorong009 · 2024-06-11T14:27:07Z

@ed255
I add the recommended checks for lookup_any here.
I think we still have undesirable behavior you mentioned in comment.
For example, this test tries to simulate the case you mentioned(#347 (comment)).
The issue is that it still passes, although it should be failed.

guorong009 · 2024-06-12T05:37:05Z

@ed255 @teddav
I think I didn't bring all the trick mentioned here.
The main point in this PR is that:

add the fixed columns for tagging, one for to_lookup and another one for lookup_table
add the pair of tagging column queries([(key_is_enabled, table_is_enabled)]) to the lookup_any constraints

If you read the PR description and its changes(especially, this one), it will be clear what we are missing.

Hence, I updated the assertion checks.
They are:

If all of table_expr are single fixed col, the api panicks & recommends to use lookup api
If any of input_expr does not have selector/fixed col for tagging, the api panicks with message
If any of table_expr does not have selector/fixed col for tagging, the api panicks with message
If the pair of (input_expr(single fixed/selector query for tagging to_lookup rows), table_expr(single fixed/selector query for tagging table rows)) does not exist, the api panicks

Pls re-review the new updates, with mentioned PR.
(These assertions catch the error case that @ed255 mentioned here)

ed255 · 2024-06-14T10:23:51Z

halo2_proofs/tests/frontend_backend_split.rs

@@ -182,7 +182,7 @@ impl<F: Field + From<u64>, const WIDTH_FACTOR: usize> MyCircuit<F, WIDTH_FACTOR>
            let d = meta.query_fixed(d, Rotation::cur());
            let lhs = [one.clone(), a, b].map(|c| c * s_lookup.clone());
            let rhs = [one.clone(), d, c].map(|c| c * s_ltable.clone());
-            lhs.into_iter().zip(rhs).collect()
+            zip(lhs, rhs).chain([(s_lookup, s_ltable)]).collect()


Previously this was:
s_lookup * [1, a, b] in s_ltable * [1, d, c] <->
[s_lookup*1, s_lookup*a, s_lookup*b] in [s_ltable*1, s_ltable*d, s_ltable*c]

Now it's:
[s_lookup*1, s_lookup*a, s_lookup*b, s_lookup] in [s_ltable*1, s_ltable*d, s_ltable*c, s_ltable]

Isn't the first pair (input_expr[0], table_expr[0]) redundant with the last one (input_expr[3], table_expr[3])?

The answer is no. (starting from my understanding) @ed255

I understood the original constraints as lookup of [1, 1], [a, d], [b, c].
In other words, [1, 1] pair is one part of whole lookup, NOT as the pair of selectors.
At first, I thought this is redundant to lookup constants [1, 1], but didn't want to change them.
I just wanted to add the new updates to the circuit, not changing any of original code.
That's why I kept the original constraints, just add the extra pair of selectors at the end.

The answer is no. (starting from my understanding) @ed255

I understood the original constraints as lookup of [1, 1], [a, d], [b, c]. In other words, [1, 1] pair is one part of whole lookup, NOT as the pair of selectors. At first, I thought this is redundant to lookup constants [1, 1], but didn't want to change them.

That would be the case if we had

let lhs = [one.clone(), a, b];

But we actually had

let lhs = [one.clone(), a, b].map(|c| c * s_lookup.clone());

So originally it was [s_lookup*1, s_ltable*1], [s_lookup*a, s_ltable*d], [s_lookup*b, s_ltable*c]

Or I'm missing something?

No, you don't miss anything.
Originally, it was [s_lookup*1, s_ltable*1], [s_lookup*a, s_ltable*d], [s_lookup*b, s_ltable*c].
Now, I add the [s_lookup, s_ltable] at the end.
Even though the expressions share the same value, their meanings are different.
I mean (input_expr[0], table_expr[0]) != (input_expr[3], table_expr[3]) <-> [s_lookup*1, s_ltable*1] != [s_lookup, s_ltable]
The reason is, the goal of newly-added expression pair is to check lookup_activator = table_activator = 1(enabled).
On the other hand, the goal of first expression pair is to lookup/check 1 = 1.

@ed255
I believe I misunderstand the issue behind this redundancy.
Here, I add the patch to correct the mistake. cdb157b

ed255 · 2024-06-17T12:14:24Z

halo2_frontend/src/plonk/circuit/constraint_system.rs

+            if is_all_table_expr_single_fixed {
+                panic!("all table expressions contain only fixed query, should use `lookup` api instead of `lookup_any`");
+            }
+            if !is_all_table_expr_contain_fixed_or_selector {
+                panic!("all table expressions need selector/fixed query for tagging");
+            }
+            if !is_tagging_exprs_pair_exists {
+                panic!("pair of tagging expressions(query of the tag columns or mutiple query combinations) should be included");
+            }


I propose that the #[cfg(feature = "lookup-any-sanity-checks")] only applies to these if cases that panic.

The rest of the code doesn't need cfg(...) / cfg(not(...))`

And I have an extra suggestion. I would add the following comment before this section

NOTE: These checks try to detect unsound cases of lookups and are only active with the `lookup-any-sanity-checks`. False positives may exist: in some particular scenarios the lookup can be sound but these checks will not pass, leading to panics. For those cases you can disable the `lookup-any-sanity-checks` feature. We will appreciate it if you report false positives by opening issues on the repository.

ed255

Now that there's a feature that can be disabled I have more confidence in moving forward!
I think there are false positives, but that should not be an issue now because the check can be disabled; and maybe we can't do the perfect check.

I've written two "final" small requests, and after that this will look good to me!

ed255 · 2024-06-17T12:25:34Z

halo2_frontend/src/plonk/circuit/constraint_system.rs

+            if is_all_table_expr_single_fixed {
+                panic!("all table expressions contain only fixed query, should use `lookup` api instead of `lookup_any`");
+            }
+            if !is_all_table_expr_contain_fixed_or_selector {
+                panic!("all table expressions need selector/fixed query for tagging");
+            }
+            if !is_tagging_exprs_pair_exists {
+                panic!("pair of tagging expressions(query of the tag columns or mutiple query combinations) should be included");
+            }


And I have an extra suggestion. I would add the following comment before this section

NOTE: These checks try to detect unsound cases of lookups and are only active with the `lookup-any-sanity-checks`. False positives may exist: in some particular scenarios the lookup can be sound but these checks will not pass, leading to panics. For those cases you can disable the `lookup-any-sanity-checks` feature. We will appreciate it if you report false positives by opening issues on the repository.

ed255

LGTM! Nice work!

guorong009 added 4 commits June 3, 2024 23:31

fix: add assertion of "table" degree in "lookup_any"

93025b4

chore: fix the unit tests related to "lookup_any"

db03d93

doc: add comment for "lookup_any"

e88b706

chore: fmt + clippy

67842f3

guorong009 self-assigned this Jun 4, 2024

guorong009 requested review from adria0, davidnevadoc, ed255 and CPerezz June 4, 2024 03:07

chore: fix the comments

3a2018a

teddav reviewed Jun 4, 2024

View reviewed changes

chore: update the comments

88b2cc8

guorong009 requested a review from teddav June 5, 2024 07:23

ed255 reviewed Jun 6, 2024

View reviewed changes

guorong009 added 2 commits June 7, 2024 14:16

feat: improve the assertion check

4efb9d3

chore: improve the tests

48168ad

chore: improve naming

efd0621

guorong009 requested a review from ed255 June 7, 2024 07:09

patch: add extra check in "lookup_any" api

c80022a

ed255 reviewed Jun 10, 2024

View reviewed changes

guorong009 requested a review from ed255 June 11, 2024 02:12

temp

4b718fd

guorong009 added 2 commits June 12, 2024 13:21

feat: improve the "lookup_any" assertion checks

037cc13

chore: update the unit tests

ba526ef

chore: fmt + clippy

0690751

guorong009 added 2 commits June 12, 2024 14:15

patch: remove unnecessary assertion checks

612e2a1

patch: roll back removed assertion checks

0cdbda8

ed255 reviewed Jun 14, 2024

View reviewed changes

guorong009 added 3 commits June 15, 2024 15:27

fix: remove redundancy in one of "lookup_any" example

cdb157b

patch: improve the "lookup_any" assertions

20ca124

feat: add new feature "lookup-any-sanity-checks"

6205dfc

guorong009 requested a review from ed255 June 17, 2024 01:57

ed255 reviewed Jun 17, 2024

View reviewed changes

doc: add comments for new feature checks

e385217

ed255 approved these changes Jun 17, 2024

View reviewed changes

guorong009 merged commit d7c6279 into main Jun 17, 2024
18 checks passed

guorong009 deleted the gr@dynamic-lookup-assertion branch June 17, 2024 13:33

ed255 mentioned this pull request Jun 18, 2024

Possible bug in Lookup-any API #335

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add assertion for dynamic lookup #347

feat: add assertion for dynamic lookup #347

guorong009 commented Jun 4, 2024 •

edited

Loading

codecov-commenter commented Jun 4, 2024 •

edited

Loading

teddav Jun 4, 2024

guorong009 Jun 5, 2024 •

edited

Loading

ed255 Jun 6, 2024

guorong009 Jun 7, 2024

ed255 Jun 6, 2024

guorong009 Jun 7, 2024

guorong009 commented Jun 7, 2024

teddav commented Jun 7, 2024 •

edited

Loading

guorong009 commented Jun 10, 2024 •

edited

Loading

ed255 Jun 10, 2024

guorong009 Jun 11, 2024 •

edited

Loading

ed255 Jun 10, 2024

guorong009 Jun 11, 2024

guorong009 commented Jun 11, 2024

guorong009 commented Jun 12, 2024 •

edited

Loading

ed255 Jun 14, 2024

guorong009 Jun 14, 2024

ed255 Jun 14, 2024

guorong009 Jun 14, 2024 •

edited

Loading

guorong009 Jun 17, 2024

ed255 Jun 17, 2024

ed255 Jun 17, 2024

ed255 left a comment

ed255 Jun 17, 2024

ed255 left a comment

feat: add assertion for dynamic lookup #347

feat: add assertion for dynamic lookup #347

Conversation

guorong009 commented Jun 4, 2024 • edited Loading

Description

Related issues

Changes

codecov-commenter commented Jun 4, 2024 • edited Loading

Codecov Report

Choose a reason for hiding this comment

guorong009 Jun 5, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

guorong009 commented Jun 7, 2024

teddav commented Jun 7, 2024 • edited Loading

guorong009 commented Jun 10, 2024 • edited Loading

Choose a reason for hiding this comment

guorong009 Jun 11, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

guorong009 commented Jun 11, 2024

guorong009 commented Jun 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

guorong009 Jun 14, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ed255 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ed255 left a comment

Choose a reason for hiding this comment

guorong009 commented Jun 4, 2024 •

edited

Loading

codecov-commenter commented Jun 4, 2024 •

edited

Loading

guorong009 Jun 5, 2024 •

edited

Loading

teddav commented Jun 7, 2024 •

edited

Loading

guorong009 commented Jun 10, 2024 •

edited

Loading

guorong009 Jun 11, 2024 •

edited

Loading

guorong009 commented Jun 12, 2024 •

edited

Loading

guorong009 Jun 14, 2024 •

edited

Loading