feat: write u32 operations constraints

Author: Fumuran

constraints/miden-vm/stack.air

@@ -498,15 +498,26 @@ ev is_binary(main: [a]):
     enf a^2 = a
 
 
-ev range_check_16bit()
+ev range_check_16bit(aux: [helper[6], b_range]):
+    enf b_range' * (alpha[0] + helper[0]) * (alpha[1] * helper[1]) * (alpha[2] + helper[2]) * (alpha[3] * helper[3]) = b_range
+
+
+ev check_element_validity(aux: [helper[6]]):
+    let m = helper[4]
+    let v_hi = 2^16 * helper[3] + helper[2]
+    let v_lo = 2^16 * helper[1] + helper[0]
+    enf (1 - m * (2^32 - 1 - v_hi)) * v_lo = 0
 
 
 ### Stack Air Constraints #########################################################################
 
 # Enforces the constraints on the stack.
 # TODO: add docs for columns
-ev stack_constraints(main: [stack[16], bookkeeping[2], h0], aux: [op_bits[7], extra, hasher5, fmp, helper[3], clk, b_chip]):
+ev stack_constraints(main: [stack[16], bookkeeping[2], h0], aux: [op_bits[7], extra, hasher5, fmp, helper[6], clk, b_chip, b_range]):
     let op_flags = compute_op_flags(op_bits, extra)
+
+    enf range_check_16bit([helper, b_range]) when f_u32rc([stack])
+
     match enf:
         noop([stack]) when op_flags[0]
         eqz([stack, h0]) when op_flags[1]
@@ -555,7 +566,7 @@ ev stack_constraints(main: [stack[16], bookkeeping[2], h0], aux: [op_bits[7], ex
         cswap([stack]) when op_flags[42]
         cswapw([stack]) when op_flags[43]
         mloadw([stack], [clk, b_chip]) when op_flags[44]
-        mstore([stack], [helper[3], clk, b_chip]) when op_flags[45]
+        mstore([stack], [helper, clk, b_chip]) when op_flags[45]
         mstorew([stack], [clk, b_chip]) when op_flags[46]
         fmpupdate([stack], [fmp]) when op_flags[47]
 
@@ -612,8 +623,8 @@ ev fmpadd(main: [s[16]], aux: [fmp]):
 # WARNING: not sure that I got the constraint right
 # What are the "helper" columns? Is it just a different name for hasher decoder columns, or they 
 # are unique for i/o ops?
-ev mload(main: [s[16]], aux: [helper[3], clk, b_chip]):
-    let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]'])
+ev mload(main: [s[16]], aux: [helper[6], clk, b_chip]):
+    let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]' for i in 1..4])
     let op_mem_read = 12
     let u_mem = alpha[0] + alpha[1] * op_mem_read + alpha[3] * s[0] + alpha[4] * clk + v
     enf b_chip' * u_mem = b_chip
@@ -803,7 +814,7 @@ ev mloadw(main: [s[16]], aux: [clk, b_chip]):
     enf b_chip' * u_mem = b_chip
     enf s[i]' = s[i + 1] for i in 4..15
 
-ev mstore(main: [s[16]], aux: [helper[3], clk, b_chip]):
+ev mstore(main: [s[16]], aux: [helper[6], clk, b_chip]):
     let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]' for i in 1..4])
     let op_mem_write = 4
     let u_mem = alpha[0] + alpha[1] * op_mem_write + alpha[3] * s[0] + alpha[4] * clk + v
@@ -886,3 +897,56 @@ ev sdepth(main: [s[16], bookkeeping[2]]):
 ev clk(main: [s[16]], aux: [clk]):
     enf s[0]' = clk
     enf s[i + 1]' = s[i] for i in 0..15
+
+
+# u32 operations
+
+ev u32add(main: [s[16]], aux: [helper[6]]):
+    enf s[0] + s[1] = 2^32 * helper[2] + 2^16 * helper[1] + helper[0]
+    enf s[0]' = helper[2]
+    enf s[1]' = 2^16 8 helper[1] + helper[0]
+    enf delta(s[i]) = 0 for i in 2..16
+
+ev u32sub(main: [s[16]], aux: [helper[6]]):
+    enf s[1] = s[0] + s[1]' + 2^32 * s[0]'
+    enf (s[0]')^2 - s[0]' = 0
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf delta(s[i]) = 0 for i in 2..16
+
+ev u32mul(main: [s[16]], aux: [helper[6]]):
+    enf s[0] * s[1] = 2^48 * helper[3] + 2^32 * helper[2] + 2^16 * helper[1] + helper[0]
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf s[0]' = 2^16 * helper[3] + helper[2]
+    enf check_element_validity([helper])
+    enf delta(s[i]) = 0 for i in 2..16
+
+ev u32div(main: [s[16]], aux: [helper[6]]):
+    enf s[1] = s[0] * s[1]' + s[0]'
+    enf s[1] - s[1]' = 2^16 * helper[1] + helper[0]
+    enf s[0] - s[0]' - 1 = 2^16 * helper[2] + helper[3]
+    enf delta(s[i]) = 0 for i in 2..16
+
+ev u32split(main: [s[16]], aux: [helper[6]]):
+    enf s[0] = 2^48 * helper[3] + 2^32 * helper[2] + 2^16 * helper[1] + helper[0]
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf s[0]' = 2^16 * helper[3] + helper[2]
+    enf check_element_validity([helper])
+    enf s[i + 1]' = s[i] for i in 1..15
+
+ev u32assert2(main: [s[16]], aux: [helper[6]]):
+    enf s[0]' = 2^16 * helper[3] + helper[2]
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf delta(elem) = 0 for elem in s
+
+ev u32add3(main: [s[16]], aux: [helper[6]]):
+    enf s[0] + s[1] + s[2] = 2^32 * helper[2] + 2^16 * helper[1] + helper[0]
+    enf s[0]' = helper[2]
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf s[i]' = s[i + 1] for i in 2..15
+
+ev u32madd(main: [s[16]], aux: [helper[6]]):
+    enf s[0] * s[1] + s[2] = 2^48 * helper[3] + 2^32 * helper[2] + 2^16 * helper[1] + helper[0]
+    enf s[1]' = 2^16 * helper[1] + helper[0]
+    enf s[0]' = 2^16 * helper[3] + helper[2]
+    enf check_element_validity([helper])
+    enf s[i]' = s[i + 1] for i in 2..15