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
(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 n % 2 == 0.
[ap] = x / 2; ap++
ret
odd:
# Case n % 2 == 1.
[ap] = x - 1; ap++
[ap] = [ap - 1] / 2; ap++
ret
end
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)?