Update bitwise chiplet constraints

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
+    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

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