# Range gadget
This gadget can be found in the halo2wrong repo [here](https://github.com/privacy-scaling-explorations/halo2wrong/tree/master/maingate). 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](https://github.com/EDGDrummond/EF-grant/tree/main/halo2/tests).
### 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.
### Benchmark
Now is a good time to provide some benchmark figures for this gadget in both Halo2 and groth16 for comparison.
The following Halo2 times were taken on a 2020 M1 macbook air with 16GB RAM.
| Process | 2^14 constraints | 2^18 constraints |
| ----------------------- | ---------------- | ---------------- |
| Verifier key generation | 345ms | 3.6s |
| Prover key generation | 215ms | 4.2s |
| Proof generation | 1.23s | 17.3s |
| Proof verification | 4.3ms | 12.8ms |
The following groth16 times were taken on a 2020 M1 macbook air with 16GB RAM.
| Process | 2^14 constraints | 2^18 constraints |
| ------------------- | ---------------- | ---------------- |
| Circuit compilation | 630ms | 9.6s |
| Witness generation | 110ms | 106ms |
| Circuit set-up | 43s | 4m |
| Proof generation | 955ms | 11.8s |
| Proof verification | 438ms | 459ms |
