From Program to Constraints.

[ Rust Program ]
↓
[ Compile to Executable (e.g., ELF, WASM, custom ISA) ]
↓
[ Run on zkVM interpreter or emulator ]
↓
[ Execution Trace (opcodes, memory, registers, etc.) ]
↓
[ Encode Execution Trace into Algebraic Constraints ]
↓
[ Prover proves that trace satisfies the constraints ]

More RISCV instructions found here

let’s see these steps with code:

Start with the example of single_xor:

powdr->openvm -> tests-> apc_builder

assert_machine_output -> compile

compile:

the airs() function should be where opcode and constraints generated.

see:

from instruction_allowlist you can find all the instructions and opcodes:

continue the air function, you can find where the apc is built:

compile -> apc build -> where SymbolicMachine is built without optimizing

The optimizer is here

now let’s check without optimizer, what the constraints looks like ( I comment out this optimizer code), all the expression are listed here.

The optimized constraints are listed here

Constraint Analysis

Algebraic constraints

Binary Constraint:

these restrict each opcode flag is either 0 or 1.

opcode_add_flag_0 * (opcode_add_flag_0 - 1) = 0
opcode_sub_flag_0 * (opcode_sub_flag_0 - 1) = 0
opcode_xor_flag_0 * (opcode_xor_flag_0 - 1) = 0
opcode_or_flag_0 * (opcode_or_flag_0 - 1) = 0
opcode_and_flag_0 * (opcode_and_flag_0 - 1) = 0

make sure only one flag set at a time, or none of them set

(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0 - 1) = 0

Memory buses

mult=2013265920 * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0), args=[1, rs1_ptr_0, b__0_0, b__1_0, b__2_0, b__3_0, reads_aux__0__base__prev_timestamp_0]

mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[1, rs1_ptr_0, b__0_0, b__1_0, b__2_0, b__3_0, from_state__timestamp_0 + 0]

mult=2013265920 * rs2_as_0, args=[rs2_as_0, rs2_0, c__0_0, c__1_0, c__2_0, c__3_0, reads_aux__1__base__prev_timestamp_0]

mult=rs2_as_0, args=[rs2_as_0, rs2_0, c__0_0, c__1_0, c__2_0, c__3_0, from_state__timestamp_0 + 1]

mult=2013265920 * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0), args=[1, rd_ptr_0, writes_aux__prev_data__0_0, writes_aux__prev_data__1_0, writes_aux__prev_data__2_0, writes_aux__prev_data__3_0, writes_aux__base__prev_timestamp_0]

mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[1, rd_ptr_0, a__0_0, a__1_0, a__2_0, a__3_0, from_state__timestamp_0 + 2]

let’s pay attention to the last parameter of args, which is the time stamp, in these 6 bueses, the time stamps are

reads_aux__0__base__prev_timestamp_0
from_state__timestamp_0 + 0

reads_aux__1__base__prev_timestamp_0
from_state__timestamp_0 + 1

writes_aux__prev_data__3_0
from_state__timestamp_0 + 2

according to memory checking rules, timestamp are incremental, that means

from_state__timestamp_0 > reads_aux__0__base__prev_timestamp_0

the following constraint guarantee this condition (condition 1):

(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * (from_state__timestamp_0 + 0 - reads_aux__0__base__prev_timestamp_0 - 1 - (0 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 * 1 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 * 131072)) = 0

131072 is \(2^{17}\), simplify the above constraint, it becomes:

(0 or 1 if flag set) * (from_state__timestamp_0 - reads_aux__0__base__prev_timestamp_0 - 1 - reads_aux__0__base__timestamp) = 0

now we need to prove reads_aux__0__base__timestamp is a positive number

range checker is here, reads_aux__0__base__timestamp is split to a 17 digits and 12 digits number.

mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0, 17]

mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0, 12]

we can do further simplification, see condition 1:

(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * (from_state__timestamp_0 + 0 - reads_aux__0__base__prev_timestamp_0 - 1 - (0 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 * 1 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 * 131072)) = 0

(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)   set to 1, as known

from_state__timestamp_0 - reads_aux__0__base__prev_timestamp_0 - 1 - (reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 * 1 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 * 131072) = 0

observe reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 needs to be put into range checker, from the above equation, it can be represented as

reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 = -1/131072 (reads_aux__0__base__prev_timestamp_0 - from_state__timestamp_0 + 1 + reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0)

the inverse of -131072 in babybear field is 15360, the above equation can then be directly plugged into range checker as here