feat: add assertion for dynamic lookup

guorong009 commented 3 months ago

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 #224 #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 commented 3 months ago

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 :warning:
...o2_frontend/src/plonk/circuit/constraint_system.rs	97.22%	2 Missing :warning:

Additional details and impacted files

```diff @@ 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 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

guorong009 commented 3 months ago

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

teddav commented 3 months ago

thanks for the PR @guorong009 . it looks good to me, but it doesn't fix https://github.com/privacy-scaling-explorations/halo2/issues/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: https://github.com/privacy-scaling-explorations/halo2/issues/335#issuecomment-2126815115 : 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 commented 3 months ago

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 - https://github.com/privacy-scaling-explorations/halo2/pull/347/commits/c80022ae84114680cae14a5df94ff8593e693b17 ? @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.

guorong009 commented 3 months ago

@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(https://github.com/privacy-scaling-explorations/halo2/pull/347#discussion_r1632991036). The issue is that it still passes, although it should be failed.

guorong009 commented 3 months ago

@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)

privacy-scaling-explorations / halo2