Range checks

[weijiekoh]

This pull request implements the range_check language feature. It allows the programmer to ensure that some expression val is less than some constant t. For instance:

fn main() {
        x = 1;
        y = 3;
        val = x * y;
        range_check(val, 5);
}

The above program can be executed and proven as long as val < 5, but not if val >= 5.

t must be less than or equal to 2 ** 16.

Theory

See section 2.5.3 of minimal_zkVM.pdf for a full explanation of how the technique works.

Approach

Each range check inserts 3 opcodes: deref, add, and deref:

1. Using DEREF, set m[fp + i] to m[m[fp + x]].

   • Since this will fail if m[fp + x] >= M, we ensure that m[fp + x] < M.

2. Using ADD, ensure (via constraint-solving): m[fp + j] + m[m[fp + x]] = (t - 1).

3. Using DEREF, ensure m[m[fp + j]] = m[fp + k].

   • Since this will fail if m[fp + j] >= M, we ensure that (t - 1) - m[fp + x] < M.

Auxiliary variables

During compilation, 3 stack slots are reserved for the auxiliary variables i, j, and k.

Modifications to the runner

I modified the DEREF opcode to have a for_range_check flag. If the runner encounters a DEREF with this flag set to true, it will ignore any UndefinedMemory errors, which is intentional.

Modifications to the prover

If the prover encounters a DEREF instruction where m[fp + x] >= M or m[fp + j] >= M, it should not be able to generate a proof. I modified the get_execution_trace() function to default value_a, value_b and value_c to F::ZERO if their respective address is beyond M, but the COL_INDEX_MEM_ADDRESS_{A,B,C} column will contain a value beyond M. I also modified the prove_execution() function to return a ProveExecutionError::MemoryError if base_memory_indexes contains any oversized index.

Tests

To run the tests:

cargo test --release --package lean_prover test_range_check

[TomWambsgans]

I don't think compile_program should have public_input and private_input as parameters, because the compiled program shouldn't depend on the future inputs it will run on, if that makes sense

[weijiekoh]

@TomWambsgans clarified that the prover is agnostic to whether a deref instruction specifies 2 undefined memory cells. This allows the range check technique to work without the compiler having to know the public/private inputs ahead of time. The runner just needs to distinguish between derefs that are used for the range check and derefs which are not, and ignore UndefinedMemory errors for the former.

I rewrote this PR to:

• Have each range_check hint compile into 3 opcodes (deref, add, deref) in-place, not the end
• Use the stack for the auxillary i, j, and k variable
• Have the runner ignore UndefinedMemory errors from range check derefs. I did so by adding a for_range_check boolean field to the Deref enum, and modifying the instruction execution logic.

I've pushed my work in progress. Currently, tests are slow because the prover doesn't work with small programs and emits a TODO small GKR, no packing error. Anyway, I'll write more tests and post updates.

[TomWambsgans]

The bug TODO small GKR, no packing should be now be fixed, sorry for that

[weijiekoh]

I've completed this PR and it's ready for review. I've also edited the parent comment to describe how the range check statement works and what changes this PR makes. Thanks for the help making this possible!

[TomWambsgans]

Review in progress, thanks! I will also try to add some logic to the runner: to make 'v < t' work even if m[v] (or m[t - v] are undefined at the time of execution of the range check (and are filled later / or never filled at all). When we will have that, we should be able to use it in the XMSS verification program. Bonus: I also would like to implem the following opti: in case of many consecutive range checks (as it's the case in the encoding for XMSS currently), if t is small enough, and if, by convention, our memory starts with a bunch of zeros, we can assume m[v] = 0 and m[t-v] = 0, which (after having set 1 memory cell to 0 in the current memory frame), allows us to use DEREF without using additional memory, i.e. we could do range checks in 3 cycles + 1 memory cells (instead of 3 cycles + 3 memory cells).

[weijiekoh]

I've fixed this PR to make the prover fill in any undefined cells which are ignored by range-check DEREFs. The changes are as such:

• During execution, the runner keeps track of range-check DEREFs where both source and destination cells are undefined (e.g. m[value] for step 1), and stores the address of res and the corresponding address of fp + shift_0 in the execution context. The source memory cell may be filled by a future instruction.
• During proof generation, the prover iterates through the abovementioned tuples, fetches the value of each source cell (or defaults to 0), and sets it to the destination in memory.