diff --git a/constraints/miden-vm/bitwise.air b/constraints/miden-vm/bitwise.air index f7ca00f7..57253733 100644 --- a/constraints/miden-vm/bitwise.air +++ b/constraints/miden-vm/bitwise.air @@ -1,5 +1,15 @@ 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: + let result = sum([2^i * a for (i, a) in (0..4, limb)]) + result + + public_inputs: stack_inputs: [16] @@ -15,33 +25,24 @@ boundary_constraints: enf dummy.first = 0 integrity_constraints: - # 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: - let result = sum([2^i * a for (i, a) in (0..4, limb)]) - result - # Enforce that selector must be binary - enf check_binary(s) + enf check_binary([s]) # Enforce that selector should stay the same throughout the cycle. enf k1 * (s' - s) = 0 # Enforce that the input is decomposed into valid bits - enf check_binary(a_limb[i]) for i in 0..4 - enf check_binary(b_limb[i]) for i in 0..4 + enf check_binary([a_limb[i]]) for i in 0..4 + enf check_binary([b_limb[i]]) for i in 0..4 # 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`. - let a_aggr = aggregate(a_limb) + let a_aggr = aggregate([a_limb]) enf k0 * (a - a_aggr) = 0 # 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`. - let b_aggr = aggregate(b_limb) + let b_aggr = aggregate([b_limb]) enf k0 * (b - b_aggr) = 0 # Enforce that for all rows in an 8-row cycle, except for the last one, the values in a and b