Constraints for conditionals

[vivekvpandya]

This design is based on OlaVM's cmp builtin.
See source code for constraint at: https://github.com/Sin7Y/olavm/blob/main/circuits/src/builtins/cmp/cmp_stark.rs
How they generate trace at https://github.com/Sin7Y/olavm/blob/main/executor/src/lib.rs#L773 and particularly how they compute abs_diff before converting to field https://github.com/Sin7Y/olavm/blob/main/executor/src/lib.rs#L809

Constraints for BGE/BGEU which checks if opd1 >= op2

let abs_diff = |opd1_value - opd2_value|

let cond = (opd1_value - opd2_value - abs_diff);
let cond_inv = 1/cond;   // 0 if cond is 0
let check  = cond * cond_inv;
 
 (1 - check) * (next_pc - imm_value) + (check) (next_pc - pc - 4)
 
 // so basically when check is 0 it indicates branch is taken so we need to make sure
 // that next_pc is same as imm_value in BGE instruction.
 // If check is 1 that means op1 < op2 so we make sure next_pc is pc + 4

And also we need to range check abs_diff. 

examples

5 > 1 :
cond = (5 - 1 - 4) = 0;
cond_inv = 0;
check = 0
so branch is taken and we constrain accordingly
5 > 8:
cond = (5 - 8 - 3) = -6;
cond_inv = 1/-3;
check = 1;
so branch is not taken and we constrain accordingly
-5 > -1:
cond = (-5 - (-1) - 4) = -8;
cond_inv = 1/-8;
check = 1
...
-5 > -8:
cond = (-5 - (-8) - 3) = 0;
cond_inv = 0
check = 0
...
5 > -1:
cond = (5 - (-1) - 6) = 0;
cond_inv = 0
check = 0
...
-5 > 1:
cond = (-5 - 1 - 6) = -12;
cond_inv = 1/-12;
check = 1
...

Constraints for BLT/BLTU which checks if opd1 < op2

let abs_diff = |opd1_value - opd2_value|

let cond = (opd1_value - opd2_value - abs_diff);
let cond_inv = 1/cond;   // 0 if cond is 0
let check  = cond * cond_inv;
 
 (check) * (next_pc - imm_value) + (1 - check) (next_pc - pc - 4)
 And also we need to range check abs_diff. 

Based on Ola https://github.com/Sin7Y/olavm/blob/main/circuits/src/cpu/cmp.rs

Constraints for BEQ

let abs_diff = |opd1_value - opd2_value|

let abs_diff_inv = 1/abs_diff;   // 0 if abs_diff is 0
let check  = abs_diff * abs_diff_inv;
 
 (1 - check) * (next_pc - imm_value) + (check) (next_pc - pc - 4)
 And also we need to range check abs_diff. 

Constraints for BNE

let abs_diff = |opd1_value - opd2_value|

let abs_diff_inv = 1/abs_diff;   // 0 if abs_diff is 0
let check  = abs_diff * abs_diff_inv;
 
 (check) * (next_pc - imm_value) + (1 - check) (next_pc - pc - 4)
And also we need to range check abs_diff. 

Constraints for SLT/SLTU

let abs_diff = |opd1_value - opd2_value|

let cond = (opd1_value - opd2_value - abs_diff);
let cond_inv = 1/cond;   // 0 if cond is 0
let check  = cond * cond_inv;
 
 (check) * (dst_val - 1) + (1 - check) (dst_val)
 And also we need to range check abs_diff. 

[matthiasgoergens]

We can adapt Ola's technique for BEQ, BGEU and all the other unsigned operations like SLTU. Signed operations need further thought.

[vivekvpandya]

820ac58 Proptest for verifying constraint works for BGE/BGEU