Instructions: XOR rd_ptr = 8, rs1_ptr = 7, rs2 = 5, rs2_as = 1 APC advantage: - Main columns: 36 -> 37 (0.97x reduction) - Bus interactions: 20 -> 20 (1.00x reduction) - Constraints: 22 -> 53 (0.42x reduction) Symbolic machine using 37 unique main columns: from_state__pc_0 from_state__timestamp_0 rd_ptr_0 rs1_ptr_0 rs2_0 rs2_as_0 reads_aux__0__base__prev_timestamp_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__0_0 reads_aux__0__base__timestamp_lt_aux__lower_decomp__1_0 reads_aux__1__base__prev_timestamp_0 reads_aux__1__base__timestamp_lt_aux__lower_decomp__0_0 reads_aux__1__base__timestamp_lt_aux__lower_decomp__1_0 writes_aux__base__prev_timestamp_0 writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 writes_aux__base__timestamp_lt_aux__lower_decomp__1_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 a__0_0 a__1_0 a__2_0 a__3_0 b__0_0 b__1_0 b__2_0 b__3_0 c__0_0 c__1_0 c__2_0 c__3_0 opcode_add_flag_0 opcode_sub_flag_0 opcode_xor_flag_0 opcode_or_flag_0 opcode_and_flag_0 is_valid // Bus 0 (EXECUTION_BRIDGE): mult=-(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0), args=[from_state__pc_0, from_state__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=[from_state__pc_0 + 4, from_state__timestamp_0 + 3] // Bus 1 (MEMORY): 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] // Bus 2 (PC_LOOKUP): mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[from_state__pc_0, 512 + (0 + opcode_add_flag_0 * 0 + opcode_sub_flag_0 * 1 + opcode_xor_flag_0 * 2 + opcode_or_flag_0 * 3 + opcode_and_flag_0 * 4), rd_ptr_0, rs1_ptr_0, rs2_0, 1, rs2_as_0, 0, 0] // Bus 3 (VARIABLE_RANGE_CHECKER): 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] mult=rs2_as_0, args=[reads_aux__1__base__timestamp_lt_aux__lower_decomp__0_0, 17] mult=rs2_as_0, args=[reads_aux__1__base__timestamp_lt_aux__lower_decomp__1_0, 12] mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[writes_aux__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=[writes_aux__base__timestamp_lt_aux__lower_decomp__1_0, 12] // Bus 6 (BITWISE_LOOKUP): mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[(1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__0_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * b__0_0, (1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__0_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * c__0_0, opcode_xor_flag_0 * a__0_0 + opcode_or_flag_0 * (2 * a__0_0 - b__0_0 - c__0_0) + opcode_and_flag_0 * (b__0_0 + c__0_0 - 2 * a__0_0), 1] mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[(1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__1_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * b__1_0, (1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__1_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * c__1_0, opcode_xor_flag_0 * a__1_0 + opcode_or_flag_0 * (2 * a__1_0 - b__1_0 - c__1_0) + opcode_and_flag_0 * (b__1_0 + c__1_0 - 2 * a__1_0), 1] mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[(1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__2_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * b__2_0, (1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__2_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * c__2_0, opcode_xor_flag_0 * a__2_0 + opcode_or_flag_0 * (2 * a__2_0 - b__2_0 - c__2_0) + opcode_and_flag_0 * (b__2_0 + c__2_0 - 2 * a__2_0), 1] mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0, args=[(1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__3_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * b__3_0, (1 - (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) * a__3_0 + (opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) * c__3_0, opcode_xor_flag_0 * a__3_0 + opcode_or_flag_0 * (2 * a__3_0 - b__3_0 - c__3_0) + opcode_and_flag_0 * (b__3_0 + c__3_0 - 2 * a__3_0), 1] mult=0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0 - rs2_as_0, args=[c__0_0, c__1_0, 0, 0] // Algebraic constraints: 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 (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 opcode_add_flag_0 * (2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0) * (2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0) - 1)) = 0 opcode_sub_flag_0 * (2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0) * (2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0) - 1)) = 0 opcode_add_flag_0 * (2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0)) * (2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0)) - 1)) = 0 opcode_sub_flag_0 * (2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0)) * (2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0)) - 1)) = 0 opcode_add_flag_0 * (2005401601 * (b__2_0 + c__2_0 - a__2_0 + 2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0))) * (2005401601 * (b__2_0 + c__2_0 - a__2_0 + 2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0))) - 1)) = 0 opcode_sub_flag_0 * (2005401601 * (a__2_0 + c__2_0 - b__2_0 + 2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0))) * (2005401601 * (a__2_0 + c__2_0 - b__2_0 + 2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0))) - 1)) = 0 opcode_add_flag_0 * (2005401601 * (b__3_0 + c__3_0 - a__3_0 + 2005401601 * (b__2_0 + c__2_0 - a__2_0 + 2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0)))) * (2005401601 * (b__3_0 + c__3_0 - a__3_0 + 2005401601 * (b__2_0 + c__2_0 - a__2_0 + 2005401601 * (b__1_0 + c__1_0 - a__1_0 + 2005401601 * (b__0_0 + c__0_0 - a__0_0 + 0)))) - 1)) = 0 opcode_sub_flag_0 * (2005401601 * (a__3_0 + c__3_0 - b__3_0 + 2005401601 * (a__2_0 + c__2_0 - b__2_0 + 2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0)))) * (2005401601 * (a__3_0 + c__3_0 - b__3_0 + 2005401601 * (a__2_0 + c__2_0 - b__2_0 + 2005401601 * (a__1_0 + c__1_0 - b__1_0 + 2005401601 * (a__0_0 + c__0_0 - b__0_0 + 0)))) - 1)) = 0 rs2_as_0 * (rs2_as_0 - 1) = 0 (1 - rs2_as_0) * (rs2_0 - (c__0_0 + c__1_0 * 256 + c__2_0 * 65536)) = 0 (1 - rs2_as_0) * (c__2_0 - c__3_0) = 0 (1 - rs2_as_0) * (c__2_0 * (255 - c__2_0)) = 0 (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 rs2_as_0 * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0 - 1) = 0 rs2_as_0 * (from_state__timestamp_0 + 1 - reads_aux__1__base__prev_timestamp_0 - 1 - (0 + reads_aux__1__base__timestamp_lt_aux__lower_decomp__0_0 * 1 + reads_aux__1__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) * (from_state__timestamp_0 + 2 - writes_aux__base__prev_timestamp_0 - 1 - (0 + writes_aux__base__timestamp_lt_aux__lower_decomp__0_0 * 1 + writes_aux__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) + 1 * is_valid = 0 from_state__pc_0 - 0 = 0 512 * is_valid + (0 + opcode_add_flag_0 * 0 + opcode_sub_flag_0 * 1 + opcode_xor_flag_0 * 2 + opcode_or_flag_0 * 3 + opcode_and_flag_0 * 4) - 514 * is_valid = 0 rd_ptr_0 - 8 * is_valid = 0 rs1_ptr_0 - 7 * is_valid = 0 rs2_0 - 5 * is_valid = 0 1 - 1 = 0 rs2_as_0 - 1 * is_valid = 0 0 - 0 = 0 0 - 0 = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0 - rs2_as_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (2013265920 * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * rs2_as_0 = 0 (1 - is_valid) * rs2_as_0 = 0 (1 - is_valid) * (2013265920 * rs2_as_0) = 0 (1 - is_valid) * rs2_as_0 = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (2013265920 * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0)) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * -(0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 (1 - is_valid) * (0 + opcode_add_flag_0 + opcode_sub_flag_0 + opcode_xor_flag_0 + opcode_or_flag_0 + opcode_and_flag_0) = 0 is_valid * (is_valid - 1) = 0