There is no commentSelect some text and then click Comment, or simply add a comment to this page from below to start a discussion.
Lookup argument for folding
Example Assume in lookup arguments, we have two columns , and try to lookup . Firstly, we cannot directly fold two such instances, e.g. with random factor : Obviously will not work. And since the lookup is arbitrary, we probably will not have any explicit formula to make the folding of work.
Attempt 1 Assume we want to calcualte a function . Instead of writing circuit for , we do lookup argument that . Here .
Encoding: we use encoder to encode to be a field element, i.e. Now the table is . When we do lookup of row across two columns , we first encode as and prove .
In the following, we will only consider the case that is closed under linear combination, i.e. , we have . In this case, we say the table is closed.
Assume we have two instances: , , where , .
We define folded instances of and as: Notice that table is closed by our assumption, we have . The folding prover needs to recalculate the new value .
During in folding, the prover will first fold input value , then calculate and fill it into corresponding advice column.
There are kinds of columns, one type is for folding (like Sangria and Nova); one type is advice column calculated by applying on folded lookup key (it seems we can prove the soundness for this type); one type is fixed table column (i.e. will not change during folding). However, even this approach work, this is only suitable for hash, bit operation but not for range check (range check table is not closed).
Attempt 2 We can try to fold two instances such that the polynomial constraints below are still satisfied:
As example, let's fold the second relation. First rewrite it as: Take two instances , . Thus, we need modify the second relation as Then the folding will stay the same format. i.e.