Nondeterministic jumps

We can now describe a code pattern, called “nondeterministic jumps”, that combines Conditional jumps and Hints. A nondeterministic jump is a jump instruction that may or may not be executed, according to the prover’s decision (rather than according to a condition on values which were computed before). To do this, use the Cairo instruction:

jmp label if [ap] != 0, ap++;

The idea is to use an unused memory cell ([ap]) to decide whether or not to jump. Do not forget to increase ap to make sure the following instructions will not use this memory cell.

As with every nondeterministic instruction, a hint must be attached to let the prover know whether to jump or not. For example:

%{ memory[ap] = 1 if x > 10 else 0 %}
jmp label if [ap] != 0, ap++;

Exercise

The following code tries to compute the expression \(\lfloor x / 2 \rfloor\) using the formula

\[\begin{split}\lfloor x / 2 \rfloor = \begin{cases} x / 2, & \text{$x$ is even} \\ (x - 1) / 2, & \text{$x$ is odd} \\ \end{cases}\end{split}\]

(recall that since we’re working in a field, the operation / 2 is division by 2 in the field, rather than integer division).

Can you explain what’s wrong with the following code?

func div2(x) {
    %{ memory[ap] = ids.x % 2 %}
    jmp odd if [ap] != 0, ap++;

    even:
    // Case x % 2 == 0.
    [ap] = x / 2, ap++;
    ret;

    odd:
    // Case x % 2 == 1.
    [ap] = x - 1, ap++;
    [ap] = [ap - 1] / 2, ap++;
    ret;
}

In Integer division you will see how to implement this function using the range-check builtin.

Hint

Consider the verifier point of view. Can you give an example of what a malicious prover can do so that div2 will return the wrong value?

Hint2

Try to change the hint to %{ memory[ap] = 1 - (ids.x % 2) %} and see what happens when you call div2(2). Do you get the expected result (1)?