Fixes for less-than instructions: LT32Chip STARK constraints and handling instructions with second operand immediate #166
Conversation
alu_u32/src/lt/stark.rs
Outdated
| // output should be 1 if is_lte & input_1 == input_2 | ||
| let all_flag_sum = flag_sum + local.byte_flag[3]; | ||
| builder | ||
| .when(local.is_lte) |
There was a problem hiding this comment.
Check multiplicity in case of dummy row
There was a problem hiding this comment.
I think this might not be necessary: each of the constraints asserted here passes when the row is all zeros. (each of them either only applies when some flag is nonzero or asserts that the values of two columns are equal). The test_left_imm_ops test in basic/tests/test_prover.rs sends 10 operations to the LT32Chip, so this test includes 6 dummy rows.
…ructions are recognized.
| builder.when(local.byte_flag[i]).assert_eq( | ||
| AB::Expr::from_canonical_u32(256) + local.input_1[i] - local.input_2[i], | ||
| bit_comp.clone(), | ||
| ); | ||
|
|
||
| // ensure that when the n-th byte flag is set, the n-th bytes are actually different |
There was a problem hiding this comment.
This constraint fixes a soundness gap: otherwise, a malicious prover could e.g. set input_1 = [0, 0, 1, 0], input_2 = [0, 0, 1, 1], and set the byte_flag's to [0, 0, 1, 0]. Then the other constraints would have the result depend on the comparison of the 3rd byte (which is equal), when in fact the 4th byte determines the correct value of the comparison.
STARK constraints for signed inequality instructions
The LT32 instructions support a mode
ilt a b cin which operandbis an immediate value and operandcis a memory address offset fromfp. All other instructions which support an immediate mode put the immediate value in operandc, and the CPUChip STARK constraints were enforcing this assumption for all bus instructions.This fixes Issue #131. A minimal example of the bug is the following
.valassembly:Separately, the STARK constraints for the LT32Chip were incorrect, e.g. in picking out the most significant byte in which the two arguments differ. This PR fixes them and adds comprehensive test coverage for the LT32 and LTE32 instructions.