diff --git a/air-script/tests/bitwise/bitwise.air b/air-script/tests/bitwise/bitwise.air index 787c98d8..ae5270ab 100644 --- a/air-script/tests/bitwise/bitwise.air +++ b/air-script/tests/bitwise/bitwise.air @@ -58,4 +58,4 @@ integrity_constraints: # enforced when s = 1. Because the selectors for the AND and XOR operations are mutually # exclusive, the constraints for different operations can be aggregated into the same result # indices. - enf (1 - s) * (z - (zp * 16 + 2^0 * a0 * b0 + 2^1 * a1 * b1 + 2^2 * a2 * b2 + 2^3 * a3 * b3)) + s * (z - (zp * 16 + 2^0 * (a0 + b0 - 2 * a0 * b0) + 2^1 * (a1 + b1 - 2 * a1 * b1) + 2^2 * (a2 + b2 - 2 * a2 * b2) + 2^3 * (a3 + b3 - 2 * a3 * b3))) = 0 \ No newline at end of file + enf (1 - s) * (z - (zp * 16 + 2^0 * a0 * b0 + 2^1 * a1 * b1 + 2^2 * a2 * b2 + 2^3 * a3 * b3)) + s * (z - (zp * 16 + 2^0 * (a0 + b0 - 2 * a0 * b0) + 2^1 * (a1 + b1 - 2 * a1 * b1) + 2^2 * (a2 + b2 - 2 * a2 * b2) + 2^3 * (a3 + b3 - 2 * a3 * b3))) = 0 diff --git a/constraints/miden-vm/bitwise.air b/constraints/miden-vm/bitwise.air new file mode 100644 index 00000000..d7a56088 --- /dev/null +++ b/constraints/miden-vm/bitwise.air @@ -0,0 +1,70 @@ +def BitwiseAir + +# Enforces that column must be binary +ev check_binary(main: [a]): + enf a^2 - a = 0 + +# Returns value aggregated from limbs +fn aggregate(limb: vector[4]) -> scalar: + return sum([2^i * a for (i, a) in (0..4, limb)]) + + +public_inputs: + stack_inputs: [16] + +trace_columns: + main: [s, a, b, a_limb[4], b_limb[4], zp, z, dummy] + +periodic_columns: + k0: [1, 0, 0, 0, 0, 0, 0, 0] + k1: [1, 1, 1, 1, 1, 1, 1, 0] + +boundary_constraints: + # This is a dummy trace column to satisfy requirement of at least one boundary constraint. + enf dummy.first = 0 + +integrity_constraints: + # Enforce that selector must be binary + enf check_binary([s]) + + # Enforce that selector should stay the same throughout the cycle. + enf s' = s when k1 + + # Enforce that the input is decomposed into valid bits + enf check_binary([a]) for a in a_limb + enf check_binary([b]) for b in b_limb + + # Enforce that the value in the first row of column `a` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `a_limb`. + enf a = aggregate([a_limb]) when k0 + + # Enforce that the value in the first row of column `b` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `b_limb`. + enf b = aggregate([b_limb]) when k0 + + # Enforce that for all rows in an 8-row cycle, except for the last one, the values in a and b + # columns are increased by the values contained in the individual bit columns a_limb and + # b_limb. + enf a' = a * 16 + a_aggr when k1 + enf b' = b * 16 + b_aggr when k1 + + # Enforce that in the first row, the aggregated output value of the previous row should be 0. + enf zp = 0 when k0 + + # Enforce that for each row except the last, the aggregated output value must equal the + # previous aggregated output value in the next row. + enf z = zp' when k1 + + # Enforce that for all rows the value in the z column is computed by multiplying the previous + # output value (from the zp column in the current row) by 16 and then adding it to the bitwise + # operation applied to the row's set of bits of a_limb and b_limb. The entire constraint must + # also be multiplied by the operation selector flag to ensure it is only applied for the + # appropriate operation. The constraint for AND is enforced when s = 0 and the constraint for + # XOR is enforced when s = 1. Because the selectors for the AND and XOR operations are mutually + # exclusive, the constraints for different operations can be aggregated into the same result + # indices. + let a_and_b = sum([2^i * a * b for (i, a, b) in (0..4, a_limb, b_limb)]) + let a_xor_b = sum([2^i * (a + b - 2 * a * b) for (i, a, b) in (0..4, a_limb, b_limb)]) + match enf: + z = zp * 16 + a_xor_b when s + z = zp * 16 + a_and_b when !s \ No newline at end of file