Range gadget

This gadget can be found in the halo2wrong repo here. We want to point out here to save you the confusion we had, wrong here refers to the 'wrong' field. This repo allows you to emulate other finite fields within the proof, so you can make proofs about range checks in any field - the field you are emulating is the 'wrong' field because it is not the native field.

With that out of the way, let's dig in.

The code included here can be found here.

Gadget design

The way this gadget works is by decomposing a value value into chunks of bits of length composition_bit_lens, where the last chunk may instead have a smaller bit length of overflow_bit_lens.

If you wanted to assert that your value was under 2^65 then you can break value into 8 chunks of 2^8 and an overflow chunk of 2^1 (alternatively we could do7 chunks of 2^9 and an overflow of 2^2). In the circuit the decomposition would be checked to be valid, and then range tables would be used to check that each chunk is indeed within its specified size (representable by composition_bit_lens bits).

We can look to the Instructions to see what functions are available to use; there are three such instruction functions.

decompose: this function is to assign a witness value representing the number to be decomposed to the constraint system, it then decomposes this value, assigning the decomposition to the constraint system too, before returning both the assigned value and the decomposed values as AssignedValue's.

assign: this function is to decompose a value and add both the decomposition to the constraint system along with the decomposed value - the only difference to above is that it only return the assigned value and not the decomposition (it's implementation just calls the decompose function above.

load_table: this will load the range tables that are specified in the configuration section; they should of course be tailored to the context of the range gate (e.g. if you want to prove x is at most 68 bits and you do limbs of length 8 bits, then you need tables for 8 bit limbs, and 2 bit limbs for the overflow).

Example

Let's say that we want to range check some values to be less than 2^67 and 2^68. Firstly we can build a test circuit config with the range config. (we will need to build some general infrastructure within which to show you one way to use the gadget)

For simplicity we also want to create an Input struct to carry information about the values we want to decompose and range check, such as their maximum sizes and the limb lengths.

Now we can create a test circuit that takes in the relevant starting data. We included range_repeats as a way to repeat iterations of this gadget in order to bench larger circuit sizes including it.

without_witness and configure are straightforward implementations, but then of course we have some work to do in synthesize to define our circuit.

What we want the circuit to do is decompose the input values, then compose the limbs back into the values and check that the starting and ending values are indeed the same. This is essentially the code found in the test for the gadget because it wants to check that the gadget is running correctly - in real use cases you wouldn't need to check that the composed value matches the value that was decomposed because the gadget functions as it is supposed to.

In a real scenario you may for example want to show that a value can be broken down into x limbs of 8 bits and no overflow limb - if your value didn't fit then the proof would fail (actually the code would throw an error and not return a proof, but any attempted such proof would fail). In the code we have such an input, if you uncomment this code you will see it fail.

In the code below you can see that our constructor will iterate through each value in inputs and do the described checks above (decompose, recompose and compare). We also assign the value before decomposing it and check equality of the decomposed value and the assigned value. In total we are making 4 calls to instructions on our chips, decompose, assign_value and two lots of assert_equal (well, per value in inputs rather than in total on the chip). All other variables are helper items to construct this. Finally we have to ensure we run load_table before the end to insert the relevant tables used for the decomposition.

load_table constructs tables to be used in the decomposition to ensure that each limb really is in the right range; for example if we have limb_bit_lens set to 8, then each normal limb is actually between 0 and 2^8 (similarly for overflow_bit_len).

We have now created the test circuit, all the required helper functions and defined what the circuit itself should look like. Now let's go through the code that runs it.

Firstly we initialise the constants that contain info about bit length in the same code area as the tutorial circuit code as it needs to be accessed there. The values in the constants are based on the how we want to break down our input values.

We set k to create the right sized circuit, first and second values to determine how large our input values will be, and then we create the actual input values. Finally, we put these inputs into a test circuit.

Now we're ready to create the proof. Initialise an empty PI vector, make the proof and check it. After this we insert a value that is larger than claimed, and as expected the proof fails.