questions about range check design

[spartucus]

Great work!

I read the latest range check design, and i have several wonderings:

1. still don't get the point of permutation check, I quote:

Using these two columns we can check if some other column in the execution trace is a permutation of values in v. Let's call this other column x. We can compute the running product of x in the same way as we compute the running product for v. Then, we can check that the last value in p0 is the same as the final value for the running product of x(this is the permutation check).

So x is one column from trace, we use permutation check to do mutliset-equal comparison with v? So there will be different vs for different xs?

2. in 'Optimized constraints', for long-traces, we can do over 3n arbitrary 16-bit range-checks. How is this 3n value calculated?

[grjte]

Great questions! I'll respond to the first question about the permutation checks first and then follow up with a separate response to your other question a bit later.

Permutation checks aren’t only used in the range checker, so here’s a general, high-level explanation for why we use them. (I’ll use the bitwise processor as an example, since it’s simpler to illustrate, but the concept is the same).

Essentially, they allow us to offload expensive computations to specialized circuits where things can be done more cheaply while still allowing us to prove correct execution.

For example, instead of directly executing an expensive operation that could take many cycles, such as a bitwise AND, it would be convenient to just look up the value in a table and use whatever value the table gives us. If we could do that, then we could get the result of the bitwise AND in a single cycle by just doing a lookup.

To enable this in the bitwise case, we have a special “Bitwise co-processor” which is our equivalent of a specialized circuit that will return the result of bitwise operations in a way that:

1. allows us to enforce constraints and prove the correctness of the result for the given inputs.
2. allows us to do this more efficiently then if we actually had to execute this without a specialized design.

The co-processor takes in the two inputs and the bitwise operation and then provably computes the result so we could just look it up, which is exactly what we need. (You can read more about that in the bitwise design doc, which you may have seen already).

But now we’re left with a problem - we can prove that the bitwise computation is done correctly, but it’s not connected to our main processor yet, so we still need a way to actually “look up” the value and prove that the value we’re using after our lookup is in fact the correct result from that co-processor for the inputs we specified.

Permutation checks are what allow us to link these different processors and prove that this lookup is being executed correctly.

In theory, this could be done as a permutation check where we generate 2 columns that build up to the same value (but maybe they include their lookup values at different rows), then we prove that their final values are equal. The columns would be built like this:

• In the co-processor where the specialized operation is executed, we’ll include the lookup in a running product column. When nothing changes, we keep the running product value the same, so the value is just copied to the next row. When the co-processor executes an operation, we’ll add the lookup value to the running product column. This lookup value will include all of the values that are required to prove correctness (e.g. for bitwise AND a & b = c we need to include a, b, and c in this lookup value).
• In the processor where the lookup is done, we would keep track of a separate running product column, and every time we perform a lookup, we’ll multiply the running product by the exact same values as we did in the co-processor.

In practice, we reduce this from 2 columns to 1, so that we have 1 running product trace column where:

• lookup values will be multiplied into the product during the co-processor execution
• lookup values divided out when they are “looked up” in the main processor.
  Thus instead of doing a multi-set check between 2 columns we can use boundary constraints to ensure that the running product column started and ended with a value of 1. If that is the case, then all of our lookups must have matched all of the computations that were executed in the co-processor (all of which were provably correct).

The implementation & design of the permutation checks in the range checker are more complicated because the overall design is more complex, but the purpose of the columns is the same, and the implementation follows the same concept (i.e. we use one column instead of two), so in practice we don't actually have separate x and v columns (but in theory, it would be as described above, where x would be the column built in the main processor while v would be the column built in the co-processor).

[spartucus]

Thanks for detailed reply! So do you think that these traces, as well as constraints, are exclusively STARK/AIR? Can they be used on SNARK and Plonkish?

[bobbinth]

These constraints are tailored to STARKs/AIR - so, as is, they probably won't work in other proving systems. But the concepts,
and even significant parts of the design, can probably be adapted to Plonkish arithmetizations. How much effort such an "adaptation" would take is difficult for me to estimate though.

[wangtsiao]

Thanks for the reply, however, I am still confused why the permutation represents the given value x in the range. Could you provide a concrete example, so we can have a better understanding? Thanks.