From 32abe71cbb504e2ee17996f46607b368e97f722a Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Thu, 30 Mar 2023 03:46:02 +0300 Subject: [PATCH 01/12] feat: write functions for flags --- constraints/miden-vm/stack.air | 404 +++++++++++++++++++++++++++++++++ 1 file changed, 404 insertions(+) create mode 100644 constraints/miden-vm/stack.air diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air new file mode 100644 index 000000000..367085d44 --- /dev/null +++ b/constraints/miden-vm/stack.air @@ -0,0 +1,404 @@ +mod StacktAir + +### Helper functions ############################################################################## + +fn delta(v: scalar) -> scalar: + return v' - v + + +# Flags for the first bits (b[6], b[5], b[4]) + +fn f_000(b: vector[7]) -> scalar: + return !b[6] & !b[5] & !b[4] + +fn f_001(b: vector[7]) -> scalar: + return !b[6] & !b[5] & b[4] + +fn f_010(b: vector[7]) -> scalar: + return !b[6] & b[5] & !b[4] + +fn f_011(b: vector[7]) -> scalar: + return !b[6] & b[5] & b[4] + +# This flag is equal to f_100 +fn f_u32rc(b: vector[7]) -> scalar: + return b[6] & !b[5] & !b[4] + +fn f_101(b: vector[7]) -> scalar: + return b[6] & !b[5] & b[4] + + +# Flags for the four last bits (b[3], b[2], b[1], b[0]) + +fn f_x0000(b: vector[7]) -> scalar: + return !b[3] & !b[2] & !b[1] & !b[0] + +fn f_x0001(b: vector[7]) -> scalar: + return !b[3] & !b[2] & !b[1] & b[0] + +fn f_x0010(b: vector[7]) -> scalar: + return !b[3] & !b[2] & b[1] & !b[0] + +fn f_x0011(b: vector[7]) -> scalar: + return !b[3] & !b[2] & b[1] & b[0] + +fn f_x0100(b: vector[7]) -> scalar: + return !b[3] & b[2] & !b[1] & !b[0] + +fn f_x0101(b: vector[7]) -> scalar: + return !b[3] & b[2] & !b[1] & b[0] + +fn f_x0110(b: vector[7]) -> scalar: + return !b[3] & b[2] & b[1] & !b[0] + +fn f_x0111(b: vector[7]) -> scalar: + return !b[3] & b[2] & b[1] & b[0] + +fn f_x1000(b: vector[7]) -> scalar: + return b[3] & !b[2] & !b[1] & !b[0] + +fn f_x1001(b: vector[7]) -> scalar: + return b[3] & !b[2] & !b[1] & b[0] + +fn f_x1010(b: vector[7]) -> scalar: + return b[3] & !b[2] & b[1] & !b[0] + +fn f_x1011(b: vector[7]) -> scalar: + return b[3] & !b[2] & b[1] & b[0] + +fn f_x1100(b: vector[7]) -> scalar: + return b[3] & b[2] & !b[1] & !b[0] + +fn f_x1101(b: vector[7]) -> scalar: + return b[3] & b[2] & !b[1] & b[0] + +fn f_x1110(b: vector[7]) -> scalar: + return b[3] & b[2] & b[1] & !b[0] + +fn f_x1111(b: vector[7]) -> scalar: + return b[3] & b[2] & b[1] & b[0] + + +# No stack shift operations + +fn f_noop(b: vector[7]) -> scalar: + return f_000(b) & f_x0000(b) + +fn f_eqz(b: vector[7]) -> scalar: + return f_000(b) & f_x0001(b) + +fn f_neg(b: vector[7]) -> scalar: + return f_000(b) & f_x0010(b) + +fn f_inv(b: vector[7]) -> scalar: + return f_000(b) & f_x0011(b) + +fn f_incr(b: vector[7]) -> scalar: + return f_000(b) & f_x0100(b) + +fn f_not(b: vector[7]) -> scalar: + return f_000(b) & f_x0101(b) + +fn f_fmpadd(b: vector[7]) -> scalar: + return f_000(b) & f_x0110(b) + +fn f_mload(b: vector[7]) -> scalar: + return f_000(b) & f_x0111(b) + +fn f_swap(b: vector[7]) -> scalar: + return f_000(b) & f_x1000(b) + +fn f_caller(b: vector[7]) -> scalar: + return f_000(b) & f_x1001(b) + +fn f_movup2(b: vector[7]) -> scalar: + return f_000(b) & f_x1010(b) + +fn f_movdn2(b: vector[7]) -> scalar: + return f_000(b) & f_x1011(b) + +fn f_movup3(b: vector[7]) -> scalar: + return f_000(b) & f_x1100(b) + +fn f_movdn3(b: vector[7]) -> scalar: + return f_000(b) & f_x1101(b) + +fn f_advpopw(b: vector[7]) -> scalar: + return f_000(b) & f_x1110(b) + +fn f_expacc(b: vector[7]) -> scalar: + return f_000(b) & f_x1111(b) + + +fn f_movup4(b: vector[7]) -> scalar: + return f_001(b) & f_x0000(b) + +fn f_movdn4(b: vector[7]) -> scalar: + return f_001(b) & f_x0001(b) + +fn f_movup5(b: vector[7]) -> scalar: + return f_001(b) & f_x0010(b) + +fn f_movdn5(b: vector[7]) -> scalar: + return f_001(b) & f_x0011(b) + +fn f_movup6(b: vector[7]) -> scalar: + return f_001(b) & f_x0100(b) + +fn f_movdn6(b: vector[7]) -> scalar: + return f_001(b) & f_x0101(b) + +fn f_movup7(b: vector[7]) -> scalar: + return f_001(b) & f_x0110(b) + +fn f_movdn7(b: vector[7]) -> scalar: + return f_001(b) & f_x0111(b) + +fn f_swapw(b: vector[7]) -> scalar: + return f_001(b) & f_x1000(b) + +fn f_ext2mul(b: vector[7]) -> scalar: + return f_001(b) & f_x1001(b) + +fn f_movup8(b: vector[7]) -> scalar: + return f_001(b) & f_x1010(b) + +fn f_movdn8(b: vector[7]) -> scalar: + return f_001(b) & f_x1011(b) + +fn f_swapw2(b: vector[7]) -> scalar: + return f_001(b) & f_x1100(b) + +fn f_swapw3(b: vector[7]) -> scalar: + return f_001(b) & f_x1101(b) + +fn f_swapdw(b: vector[7]) -> scalar: + return f_001(b) & f_x1110(b) + + +# Left stack shift operations + +fn f_assert(b: vector[7]) -> scalar: + return f_010(b) & f_x0000(b) + +fn f_eq(b: vector[7]) -> scalar: + return f_010(b) & f_x0001(b) + +fn f_add(b: vector[7]) -> scalar: + return f_010(b) & f_x0010(b) + +fn f_mul(b: vector[7]) -> scalar: + return f_010(b) & f_x0011(b) + +fn f_and(b: vector[7]) -> scalar: + return f_010(b) & f_x0100(b) + +fn f_or(b: vector[7]) -> scalar: + return f_010(b) & f_x0101(b) + +fn f_u32and(b: vector[7]) -> scalar: + return f_010(b) & f_x0110(b) + +fn f_u32xor(b: vector[7]) -> scalar: + return f_010(b) & f_x0111(b) + +fn f_frie2f4(b: vector[7]) -> scalar: + return f_010(b) & f_x1000(b) + +fn f_drop(b: vector[7]) -> scalar: + return f_010(b) & f_x1001(b) + +fn f_cswap(b: vector[7]) -> scalar: + return f_010(b) & f_x1010(b) + +fn f_cswapw(b: vector[7]) -> scalar: + return f_010(b) & f_x1011(b) + +fn f_mloadw(b: vector[7]) -> scalar: + return f_010(b) & f_x1100(b) + +fn f_mstore(b: vector[7]) -> scalar: + return f_010(b) & f_x1101(b) + +fn f_mstorew(b: vector[7]) -> scalar: + return f_010(b) & f_x1110(b) + +fn f_fmpupdate(b: vector[7]) -> scalar: + return f_010(b) & f_x1111(b) + + +# Right stack shift operations + +fn f_pad(b: vector[7]) -> scalar: + return f_011(b) & f_x0000(b) + +fn f_dup(b: vector[7]) -> scalar: + return f_011(b) & f_x0001(b) + +fn f_dup1(b: vector[7]) -> scalar: + return f_011(b) & f_x0010(b) + +fn f_dup2(b: vector[7]) -> scalar: + return f_011(b) & f_x0011(b) + +fn f_dup3(b: vector[7]) -> scalar: + return f_011(b) & f_x0100(b) + +fn f_dup4(b: vector[7]) -> scalar: + return f_011(b) & f_x0101(b) + +fn f_dup5(b: vector[7]) -> scalar: + return f_011(b) & f_x0110(b) + +fn f_dup6(b: vector[7]) -> scalar: + return f_011(b) & f_x0111(b) + +fn f_dup7(b: vector[7]) -> scalar: + return f_011(b) & f_x1000(b) + +fn f_dup9(b: vector[7]) -> scalar: + return f_011(b) & f_x1001(b) + +fn f_dup11(b: vector[7]) -> scalar: + return f_011(b) & f_x1010(b) + +fn f_dup13(b: vector[7]) -> scalar: + return f_011(b) & f_x1011(b) + +fn f_dup15(b: vector[7]) -> scalar: + return f_011(b) & f_x1100(b) + +fn f_advpop(b: vector[7]) -> scalar: + return f_011(b) & f_x1101(b) + +fn f_sdepth(b: vector[7]) -> scalar: + return f_011(b) & f_x1110(b) + +fn f_clk(b: vector[7]) -> scalar: + return f_011(b) & f_x1111(b) + + +# u32 operations + +fn f_u32add(b: vector[7]) -> scalar: + return f_u32rc(b) & !b[3] & !b[2] & !b[1] + +fn f_u32sub(b: vector[7]) -> scalar: + return f_u32rc(b) & !b[3] & !b[2] & b[1] + +fn f_u32mul(b: vector[7]) -> scalar: + return f_u32rc(b) & !b[3] & b[2] & !b[1] + +fn f_u32div(b: vector[7]) -> scalar: + return f_u32rc(b) & !b[3] & b[2] & b[1] + +fn f_u32split(b: vector[7]) -> scalar: + return f_u32rc(b) & b[3] & !b[2] & !b[1] + +fn f_u32assert2(b: vector[7]) -> scalar: + return f_u32rc(b) & b[3] & !b[2] & b[1] + +fn f_u32add3(b: vector[7]) -> scalar: + return f_u32rc(b) & b[3] & b[2] & !b[1] + +fn f_madd(b: vector[7]) -> scalar: + return f_u32rc(b) & b[3] & b[2] & b[1] + + +# High-degree operations + +fn f_hperm(b: vector[7]) -> scalar: + return f_101(b) & !b[3] & !b[2] & !b[1] + +fn f_mpverify(b: vector[7]) -> scalar: + return f_101(b) & !b[3] & !b[2] & b[1] + +fn f_pipe(b: vector[7]) -> scalar: + return f_101(b) & !b[3] & b[2] & !b[1] + +fn f_mstream(b: vector[7]) -> scalar: + return f_101(b) & !b[3] & b[2] & b[1] + +fn f_span(b: vector[7]) -> scalar: + return f_101(b) & b[3] & !b[2] & !b[1] + +fn f_join(b: vector[7]) -> scalar: + return f_101(b) & b[3] & !b[2] & b[1] + +fn f_split(b: vector[7]) -> scalar: + return f_101(b) & b[3] & b[2] & !b[1] + +fn f_loop(b: vector[7]) -> scalar: + return f_101(b) & b[3] & b[2] & b[1] + + +# Very high-degree operations + +fn f_mrupdate(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & !b[3] & !b[2] + +fn f_push(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & !b[3] & b[2] + +fn f_syscall(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & b[3] & !b[2] + +fn f_call(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & b[3] & b[2] + +fn f_end(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & !b[3] & !b[2] + +fn f_repeat(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & !b[3] & b[2] + +fn f_respan(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & b[3] & !b[2] + +fn f_halt(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & b[3] & b[2] + + +# Composite flags + +fn f_shr(b: vector[7], extra: scalar) -> scalar: + return !b[6] & b[5] & b[4] + f_u32split(b) + f_push(b, extra) + +fn f_shl(b: vector[7], extra: scalar, h5: scalar) -> scalar: + let f_add3_mad = b[6] & !b[5] & !b[4] & b[3] & b[2] + let f_split_loop = b[6] & !b[5] & b[4] & b[3] & b[2] + return !b[6] & b[5] & !b[4] + f_add3_mad + f_split_loop + f_repeat(b, extra) + f_end(b, extra) * h5 + +fn f_ctrl(b: vector[7], extra: scalar) -> scalar: + # flag for SPAN, JOIN, SPLIT, LOOP + let f_sjsl = b[6] & !b[5] & b[4] & b[3] + + # flag for END, REPEAT, RESPAN, HALT + let f_errh = b[6] & b[5] & b[4] + + return f_sjsl + f_errh + f_call(b, extra) + f_syscall(b, extra) + + +### Helper evaluators ############################################################################# + +# Enforces that the provided columns must be zero. +ev is_zero(main: [values[4]]): + enf v = 0 for v in values + + +# Enforces that values in the columns in the current row must be equal to the values in the next +# row. +ev is_unchanged(main: [values[4]]): + enf v' = v for v in values + + +# Enforces that the provided columns must be binary. +ev is_binary(main: [a]): + enf a^2 = a + + +0###################################################################### + +# Enforces the constraints on the stack. +# TODO: add docs for columns +ev stack_constraints(main: [stack[16], bookkeeping[2], helper], aux: [op_bits[7], extra, hasher5]): From eb353c1a6ce99089387daaf3349eccf3928afd54 Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Fri, 31 Mar 2023 05:25:40 +0300 Subject: [PATCH 02/12] feat: write constraints for no stack shift ops --- constraints/miden-vm/stack.air | 159 ++++++++++++++++++++++++++++++++- 1 file changed, 158 insertions(+), 1 deletion(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 367085d44..f410c761a 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -401,4 +401,161 @@ ev is_binary(main: [a]): # Enforces the constraints on the stack. # TODO: add docs for columns -ev stack_constraints(main: [stack[16], bookkeeping[2], helper], aux: [op_bits[7], extra, hasher5]): +# ev stack_constraints(main: [stack[16], bookkeeping[2], helper], aux: [op_bits[7], extra, hasher5]): + +ev noop(main: [s[16]], aux: [b[7]]): + enf f_dup(b) * delta(elem) = 0 for elem in stack + +ev eqz(main: [s[16], helper], aux: [b[7]]): + enf f_eqz(b) * (s[0]' * s[0]) = 0 + enf f_eqz(b) * (s[0]' - (1 - s[0] * helper)) + enf f_eqz(b) * delta(s[i]) = 0 for i in 1..16 + +ev neg(main: [s[16]], aux: [b[7]]): + enf f_neg(b) * (s[0]' + s[0]) = 0 + enf f_neg(b) * delta(s[i]) = 0 for i in 1..16 + +ev inv(main: [s[16]], aux: [b[7]]): + enf f_inv(b) * (1 - s[0]' * s[0]) = 0 + enf f_inv(b) * delta(s[i]) = 0 for i in 1..16 + +ev incr(main: [s[16]], aux: [b[7]]): + enf f_incr(b) * (s[0]' - s[0] - 1) = 0 + enf f_incr(b) * delta(s[i]) = 0 for i in 1..16 + +ev not(main: [s[16]], aux: [b[7]]): + enf f_not(b) * is_binary([s[0]]) + enf f_not(b) * (s[0]' - !s[0]) = 0 + enf f_not(b) * delta(s[i]) = 0 for i in 1..16 + +ev fmpadd(main: [s[16]], aux: [b[7], fmp]): + enf f_fmpadd(b) * (s[0]' - s[0] - fmp) = 0 + enf f_fmpadd(b) * delta(s[i]) = 0 for i in 1..16 + +# 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: [b[7], helper[3], clk, b_chip]): + let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]']) + let op_mem_read = 12 + let u_mem = alpha[0] + alpha[1] * op_mem_read + alpha[3] * s[0] + alpha[4] * clk + v + enf f_mload(b) * (b_chip' * u_mem - b_chip) = 0 + enf f_mload(b) * delta(s[i]) = 0 for i in 1..16 + +ev swap(main: [s[16]], aux: [b[7]]): + enf f_swap(b) * (s[0]' - s[1]) = 0 + enf f_swap(b) * (s[1]' - s[0]) = 0 + enf f_swap(b) * delta(s[i]) = 0 for i in 2..16 + +# TODO: add constraints +ev caller(main: [s[16]], aux: [b[7]]): + +ev movup2(main: [s[16]], aux: [b[7]]): + enf f_movup2(b) * (s[0]' - s[2]) = 0 + enf f_movup2(b) * (s[i + 1]' - s[i]) = 0 for i in 0..2 + enf f_movup2(b) * delta(s[i]) = 0 for i in 3..16 + +ev movdn2(main: [s[16]], aux: [b[7]]): + enf f_movdn2(b) * (s[2]' - s[0]) = 0 + enf f_movdn2(b) * (s[i]' - s[i + 1]) = 0 for i in 0..2 + enf f_movdn2(b) * delta(s[i]) = 0 for i in 3..16 + +ev movup3(main: [s[16]], aux: [b[7]]): + enf f_movup3(b) * (s[0]' - s[3]) = 0 + enf f_movup3(b) * (s[i + 1]' - s[i]) = 0 for i in 0..3 + enf f_movup3(b) * delta(s[i]) = 0 for i in 4..16 + +ev movdn3(main: [s[16]], aux: [b[7]]): + enf f_movdn3(b) * (s[3]' - s[0]) = 0 + enf f_movdn3(b) * (s[i]' - s[i + 1]) = 0 for i in 0..3 + enf f_movdn3(b) * delta(s[i]) = 0 for i in 4..16 + +ev advpopw(main: [s[16]], aux: [b[7]]): + enf f_advpopw(b) * delta(s[i]) = 0 for i in 4..16 + +ev expacc(main: [s[16]], aux: [b[7], helper]): + enf f_expacc(b) * is_binary(s[0]') + enf f_expacc(b) * (s[1]' - s[1]^2) = 0 + enf f_expacc(b) * (helper - ((s[1] - 1) * s[0]' + 1)) = 0 + enf f_expacc(b) * (s[2]' - s[2] * helper) = 0 + enf f_expacc(b) * (s[3]' - (s[3] * 2 + s[0]')) = 0 + enf f_expacc(b) * delta(s[i]) = 0 for i in 4..16 + +ev movup4(main: [s[16]], aux: [b[7]]): + enf f_movup4(b) * (s[0]' - s[4]) = 0 + enf f_movup4(b) * (s[i + 1]' - s[i]) = 0 for i in 0..4 + enf f_movup4(b) * delta(s[i]) = 0 for i in 5..16 + +ev movdn4(main: [s[16]], aux: [b[7]]): + enf f_movdn4(b) * (s[4]' - s[0]) = 0 + enf f_movdn4(b) * (s[i]' - s[i + 1]) = 0 for i in 0..4 + enf f_movdn4(b) * delta(s[i]) = 0 for i in 5..16 + +ev movup5(main: [s[16]], aux: [b[7]]): + enf f_movup5(b) * (s[0]' - s[5]) = 0 + enf f_movup5(b) * (s[i + 1]' - s[i]) = 0 for i in 0..5 + enf f_movup5(b) * delta(s[i]) = 0 for i in 6..16 + +ev movdn5(main: [s[16]], aux: [b[7]]): + enf f_movdn5(b) * (s[5]' - s[0]) = 0 + enf f_movdn5(b) * (s[i]' - s[i + 1]) = 0 for i in 0..5 + enf f_movdn5(b) * delta(s[i]) = 0 for i in 6..16 + +ev movup6(main: [s[16]], aux: [b[7]]): + enf f_movup6(b) * (s[0]' - s[6]) = 0 + enf f_movup6(b) * (s[i + 1]' - s[i]) = 0 for i in 0..6 + enf f_movup6(b) * delta(s[i]) = 0 for i in 7..16 + +ev movdn6(main: [s[16]], aux: [b[7]]): + enf f_movdn6(b) * (s[6]' - s[0]) = 0 + enf f_movdn6(b) * (s[i]' - s[i + 1]) = 0 for i in 0..6 + enf f_movdn6(b) * delta(s[i]) = 0 for i in 7..16 + +ev movup7(main: [s[16]], aux: [b[7]]): + enf f_movup7(b) * (s[0]' - s[7]) = 0 + enf f_movup7(b) * (s[i + 1]' - s[i]) = 0 for i in 0..7 + enf f_movup7(b) * delta(s[i]) = 0 for i in 8..16 + +ev movdn7(main: [s[16]], aux: [b[7]]): + enf f_movdn7(b) * (s[7]' - s[0]) = 0 + enf f_movdn7(b) * (s[i]' - s[i + 1]) = 0 for i in 0..7 + enf f_movdn7(b) * delta(s[i]) = 0 for i in 8..16 + +ev swapw(main: [s[16]], aux: [b[7]]): + enf f_swapw(b) * (s[i]' - s[i + 4]) = 0 for i in 0..4 + enf f_swapw(b) * (s[i + 4]' - s[i]) = 0 for i in 0..4 + enf f_swapw(b) * delta(s[i]) = 0 for i in 8..16 + +ev ext2mul(main: [s[16]], aux: [b[7]]): + enf f_ext2mul(b) * (s[0]' - s[0]) = 0 + enf f_ext2mul(b) * (s[1]' - s[1]) = 0 + enf f_ext2mul(b) * (s[2]' - (s[0] + s[1]) * (s[2] + s[3]) + s[0] * s[2]) = 0 + enf f_ext2mul(b) * (s[3]' - s[1] * s[3] + 2 * s[0] * s[2]) = 0 + enf f_ext2mul(b) * delta(s[i]) = 0 for i in 4..16 + +ev movup8(main: [s[16]], aux: [b[7]]): + enf f_movup8(b) * (s[0]' - s[8]) = 0 + enf f_movup8(b) * (s[i + 1]' - s[i]) = 0 for i in 0..8 + enf f_movup8(b) * delta(s[i]) = 0 for i in 9..16 + +ev movdn8(main: [s[16]], aux: [b[7]]): + enf f_movdn8(b) * (s[8]' - s[0]) = 0 + enf f_movdn8(b) * (s[i]' - s[i + 1]) = 0 for i in 0..8 + enf f_movdn8(b) * delta(s[i]) = 0 for i in 9..16 + +ev swapw2(main: [s[16]], aux: [b[7]]): + enf f_swapw2(b) * (s[i]' - s[i + 8]) = 0 for i in 0..4 + enf f_swapw2(b) * (s[i + 8]' - s[i]) = 0 for i in 0..4 + enf f_swapw2(b) * delta(s[i]) = 0 for i in 4..8 + enf f_swapw2(b) * delta(s[i]) = 0 for i in 12..16 + +# Should we enforce that elements in position grater than 15 do not change? +ev swapw3(main: [s[16]], aux: [b[7]]): + enf f_swapw3(b) * (s[i]' - s[i + 12]) = 0 for i in 0..4 + enf f_swapw3(b) * (s[i + 12]' - s[i]) = 0 for i in 0..4 + enf f_swapw3(b) * delta(s[i]) = 0 for i in 4..12 + +# Should we enforce that elements in position grater than 15 do not change? +ev swapdw(main: [s[16]], aux: [b[7]]): + enf f_swapdw(b) * (s[i]' - s[i + 8]) = 0 for i in 0..8 + enf f_swapdw(b) * (s[i + 8]' - s[i]) = 0 for i in 0..8 From 141f0f20c6a340239f43941bfe545dc875654609 Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Sat, 1 Apr 2023 02:19:14 +0300 Subject: [PATCH 03/12] feat: write left and right shift constraints --- constraints/miden-vm/stack.air | 166 +++++++++++++++++++++++++++++++-- 1 file changed, 160 insertions(+), 6 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index f410c761a..311c7cc0c 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -379,6 +379,10 @@ fn f_ctrl(b: vector[7], extra: scalar) -> scalar: return f_sjsl + f_errh + f_call(b, extra) + f_syscall(b, extra) +fn binary_check_sub(elem: scalar) -> scalar: + return elem^2 - elem + + ### Helper evaluators ############################################################################# # Enforces that the provided columns must be zero. @@ -392,17 +396,17 @@ ev is_unchanged(main: [values[4]]): enf v' = v for v in values -# Enforces that the provided columns must be binary. -ev is_binary(main: [a]): - enf a^2 = a +ev range_check_16bit() -0###################################################################### +### Stack Air Constraints ######################################################################### # Enforces the constraints on the stack. # TODO: add docs for columns # ev stack_constraints(main: [stack[16], bookkeeping[2], helper], aux: [op_bits[7], extra, hasher5]): +# No stack shift operations + ev noop(main: [s[16]], aux: [b[7]]): enf f_dup(b) * delta(elem) = 0 for elem in stack @@ -424,7 +428,7 @@ ev incr(main: [s[16]], aux: [b[7]]): enf f_incr(b) * delta(s[i]) = 0 for i in 1..16 ev not(main: [s[16]], aux: [b[7]]): - enf f_not(b) * is_binary([s[0]]) + enf f_not(b) * binary_check_sub(s[0]) enf f_not(b) * (s[0]' - !s[0]) = 0 enf f_not(b) * delta(s[i]) = 0 for i in 1..16 @@ -474,7 +478,7 @@ ev advpopw(main: [s[16]], aux: [b[7]]): enf f_advpopw(b) * delta(s[i]) = 0 for i in 4..16 ev expacc(main: [s[16]], aux: [b[7], helper]): - enf f_expacc(b) * is_binary(s[0]') + enf f_expacc(b) * binary_check_sub(s[0]') enf f_expacc(b) * (s[1]' - s[1]^2) = 0 enf f_expacc(b) * (helper - ((s[1] - 1) * s[0]' + 1)) = 0 enf f_expacc(b) * (s[2]' - s[2] * helper) = 0 @@ -559,3 +563,153 @@ ev swapw3(main: [s[16]], aux: [b[7]]): ev swapdw(main: [s[16]], aux: [b[7]]): enf f_swapdw(b) * (s[i]' - s[i + 8]) = 0 for i in 0..8 enf f_swapdw(b) * (s[i + 8]' - s[i]) = 0 for i in 0..8 + + +# Left stack shift operationds + +ev assert(main: [s[16]], aux: [b[7]]): + enf f_assert(b) * (s[0] - 1) = 0 + enf f_assert(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + +ev eq(main: [s[16]], aux: [b[7], helper]): + enf f_eq(b) * (s[0]' * (s[0] - s[1])) = 0 + enf f_eq(b) * (s[0]' - (1 - (s[0] - s[1]) * helper)) = 0 + enf f_eq(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev add(main: [s[16]], aux: [b[7]]): + enf f_add(b) * (s[0]' - (s[0] + s[1])) = 0 + enf f_eq(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev mul(main: [s[16]], aux: [b[7]]): + enf f_mul(b) * (s[0]' - s[0] * s[1]) = 0 + enf f_mul(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev and(main: [s[16]], aux: [b[7]]): + enf f_and(b) * binary_check_sub(s[i]) = 0 for i in 0..2 + enf f_and(b) * (s[0]' - s[0] * s[1]) = 0 + enf f_and(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev or(main: [s[16]], aux: [b[7]]): + enf f_or(b) * binary_check_sub(s[i]) = 0 for i in 0..2 + enf f_or(b) * (s[0]' - (s[1] + s[0] - s[1] * s[0])) = 0 + enf f_or(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev u32and(main: [s[16]], aux: [b[7], b_chip]): + let op_u32and = 2 + enf f_u32and(b) * b_chip' * (alpha[0] + alpha[1] * op_u32and + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf f_u32and(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +ev u32xor(main: [s[16]], aux: [b[7], b_chip]): + let op_u32xor = 6 + enf f_u32xor(b) * b_chip' * (alpha[0] + alpha[1] * op_u32xor + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf f_u32xor(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + +# TODO: add constraints +ev frie2f4(main: [s[16]], aux: [b[7]]): + + +ev drop(main: [s[16]], aux: [b[7]]): + enf f_drop(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + +ev cswap(main: [s[16]], aux: [b[7]]): + enf f_cswap(b) * binary_check_sub(s[0]) = 0 + enf f_cswap(b) * (s[0]' - s[0] * s[2] - (1 - s[0]) * s[1]) = 0 + enf f_cswap(b) * (s[1]' - s[0] * s[1] - (1 - s[0]) * s[2]) = 0 + enf f_cswap(b) * (s[i]' - s[i + 1]) = 0 for i in 2..15 + +ev cswapw(main: [s[16]], aux: [b[7]]): + enf f_cswapw(b) * binary_check_sub(s[0]) = 0 + enf f_cswapw(b) * (s[i]' - s[0] * s[i + 5] - (1 - s[0]) * s[i + 1]) = 0 for i in 0..4 + enf f_cswapw(b) * (s[i + 4]' - s[0] * s[i + 1] + (1 - s[0]) * s[i + 5]) = 0 for i in 0..4 + enf f_cswapw(b) * (s[i]' - s[i + 1]) = 0 for i in 8..15 + +ev mloadw(main: [s[16]], aux: [b[7], b_chip, clk]): + let v = sum([alpha[i + 5] * s[3 - i]' for i in 0..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 f_mloadw(b) * (b_chip' * u_mem - b_chip) = 0 + enf f_mloadw(b) * (s[i]' - s[i + 1]) = 0 for i in 4..15 + +ev mstore(main: [s[16]], aux: [b[7], helper[3], 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 + enf f_mstore(b) * (b_chip' * u_mem - b_chip) = 0 + enf f_mstore(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + +ev mstorew(main: [s[16]], aux: [b[7]]): + let v = sum([alpha[i + 5] * s[3 - i]']) for i in 0..4 + let op_mem_write = 4 + let u_mem = alpha[0] + alpha[1] * op_mem_write + alpha[3] * s[0] + alpha[4] * clk + v + enf f_mstorew(b) * (b_chip' * u_mem - b_chip) = 0 + enf f_mstore(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + +ev fmpupdate(main: [s[16]], aux: [b[7], fmp]): + enf f_fmpupdate(b) * (fmp' - (fmp + s[0])) = 0 + enf f_fmpupdate(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + + +# Right stack shift operations + +ev pad(main: [s[16]], aux: [b[7]]): + enf f_pad(b) * s[0]' = 0 + enf f_pad(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup(main: [s[16]], aux: [b[7]]): + enf f_dup(b) * (s[0]' - s[0]) = 0 + enf f_dup(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup1(main: [s[16]], aux: [b[7]]): + enf f_dup1(b) * (s[0]' - s[1]) = 0 + enf f_dup1(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup2(main: [s[16]], aux: [b[7]]): + enf f_dup2(b) * (s[0]' - s[2]) = 0 + enf f_dup2(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup3(main: [s[16]], aux: [b[7]]): + enf f_dup3(b) * (s[0]' - s[3]) = 0 + enf f_dup3(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup4(main: [s[16]], aux: [b[7]]): + enf f_dup4(b) * (s[0]' - s[4]) = 0 + enf f_dup4(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup5(main: [s[16]], aux: [b[7]]): + enf f_dup5(b) * (s[0]' - s[5]) = 0 + enf f_dup5(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup6(main: [s[16]], aux: [b[7]]): + enf f_dup6(b) * (s[0]' - s[6]) = 0 + enf f_dup6(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup7(main: [s[16]], aux: [b[7]]): + enf f_dup7(b) * (s[0]' - s[7]) = 0 + enf f_dup7(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup9(main: [s[16]], aux: [b[7]]): + enf f_dup9(b) * (s[0]' - s[9]) = 0 + enf f_dup9(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup11(main: [s[16]], aux: [b[7]]): + enf f_dup11(b) * (s[0]' - s[11]) = 0 + enf f_dup11(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup13(main: [s[16]], aux: [b[7]]): + enf f_dup13(b) * (s[0]' - s[13]) = 0 + enf f_dup13(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev dup15(main: [s[16]], aux: [b[7]]): + enf f_dup15(b) * (s[0]' - s[15]) = 0 + enf f_dup15(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev advpop(main: [s[16]], aux: [b[7]]): + enf f_advpop(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev sdepth(main: [s[16], bookkeeping[2]], aux: [b[7]]): + enf f_sdepth(b) * (s[0]' - b[0]) = 0 + enf f_sdepth(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 + +ev clk(main: [s[16]], aux: [b[7], clk]): + enf f_clk(b) * (s[0]' - clk) = 0 + enf f_clk(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 From 85f28c0bf186147121e508bee8ecbc30fe4d4281 Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Tue, 4 Apr 2023 02:00:26 +0300 Subject: [PATCH 04/12] refactor: add match, remove flags from evaluators --- constraints/miden-vm/stack.air | 649 +++++++++++++++++++++------------ 1 file changed, 411 insertions(+), 238 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 311c7cc0c..f982c6d06 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -175,6 +175,9 @@ fn f_swapw3(b: vector[7]) -> scalar: fn f_swapdw(b: vector[7]) -> scalar: return f_001(b) & f_x1110(b) +fn f_001_1111() -> scalar: + return 0 + # Left stack shift operations @@ -379,8 +382,102 @@ fn f_ctrl(b: vector[7], extra: scalar) -> scalar: return f_sjsl + f_errh + f_call(b, extra) + f_syscall(b, extra) -fn binary_check_sub(elem: scalar) -> scalar: - return elem^2 - elem +fn compute_op_flags(b: vector[7], extra: scalar) -> vector[88]: + return [ + f_noop(b), + f_eqz(b), + f_neg(b), + f_inv(b), + f_incr(b), + f_not(b), + f_fmpadd(b), + f_mload(b), + f_swap(b), + f_caller(b), + f_movup2(b), + f_movdn2(b), + f_movup3(b), + f_movdn3(b), + f_advpopw(b), + f_expacc(b), + f_movup4(b), + f_movdn4(b), + f_movup5(b), + f_movdn5(b), + f_movup6(b), + f_movdn6(b), + f_movup7(b), + f_movdn7(b), + f_swapw(b), + f_ext2mul(b), + f_movup8(b), + f_movdn8(b), + f_swapw2(b), + f_swapw3(b), + f_swapdw(b), + f_001_1111(b), + + f_assert(b), + f_eq(b), + f_add(b), + f_mul(b), + f_and(b), + f_or(b), + f_u32and(b), + f_u32xor(b), + f_frie2f4(b), + f_drop(b), + f_cswap(b), + f_cswapw(b), + f_mloadw(b), + f_mstore(b), + f_mstorew(b), + f_fmpupdate(b), + + f_pad(b), + f_dup(b), + f_dup1(b), + f_dup2(b), + f_dup3(b), + f_dup4(b), + f_dup5(b), + f_dup6(b), + f_dup7(b), + f_dup9(b), + f_dup11(b), + f_dup13(b), + f_dup15(b), + f_advpop(b), + f_sdepth(b), + f_clk(b), + + f_u32add(b), + f_u32sub(b), + f_u32mul(b), + f_u32div(b), + f_u32split(b), + f_u32assert2(b), + f_u32add3(b), + f_madd(b), + + f_hperm(b), + f_mpverify(b), + f_pipe(b), + f_mstream(b), + f_span(b), + f_join(b), + f_split(b), + f_loop(b), + + f_mrupdate(b, extra), + f_push(b, extra), + f_syscall(b, extra), + f_call(b, extra), + f_end(b, extra), + f_repeat(b, extra), + f_respan(b, extra), + f_halt(b, extra) + ] ### Helper evaluators ############################################################################# @@ -396,6 +493,11 @@ ev is_unchanged(main: [values[4]]): enf v' = v for v in values +# Enforces that the provided columns must be binary. +ev is_binary(main: [a]): + enf a^2 = a + + ev range_check_16bit() @@ -403,313 +505,384 @@ ev range_check_16bit() # Enforces the constraints on the stack. # TODO: add docs for columns -# ev stack_constraints(main: [stack[16], bookkeeping[2], helper], aux: [op_bits[7], extra, hasher5]): +ev stack_constraints(main: [stack[16], bookkeeping[2], h0], aux: [op_bits[7], extra, hasher5, fmp, helper[3], clk, b_chip]): + let op_flags = compute_op_flags(op_bits, extra) + match enf: + noop([stack]) when op_flags[0] + eqz([stack, h0]) when op_flags[1] + neg([stack]) when op_flags[2] + inv([stack]) when op_flags[3] + incr([stack]) when op_flags[4] + not([stack]) when op_flags[5] + fmpadd([stack], [fmp]) when op_flags[6] + mload([stack], [helper, clk, b_chip]) when op_flags[7] + swap([stack]) when op_flags[8] + # TODO: add match variant for caller + caller() + movup2([stack]) when op_flags[10] + movdn2([stack]) when op_flags[11] + movup3([stack]) when op_flags[12] + movdn3([stack]) when op_flags[13] + advpopw([stack]) when op_flags[14] + expacc([stack], [h0]) when op_flags[15] + movup4([stack]) when op_flags[16] + movdn4([stack]) when op_flags[17] + movup5([stack]) when op_flags[18] + movdn5([stack]) when op_flags[19] + movup6([stack]) when op_flags[20] + movdn6([stack]) when op_flags[21] + movup7([stack]) when op_flags[22] + movdn7([stack]) when op_flags[23] + swapw([stack]) when op_flags[24] + ext2mul([stack]) when op_flags[25] + movup8([stack]) when op_flags[26] + movdn8([stack]) when op_flags[27] + swapw2([stack]) when op_flags[28] + swapw3([stack]) when op_flags[29] + swapdw([stack]) when op_flags[30] + + assert([stack]) when op_flags[32] + eq([stack], [h0]) when op_flags[33] + add([stack]) when op_flags[34] + mul([stack]) when op_flags[35] + and([stack]) when op_flags[36] + or([stack]) when op_flags[37] + u32and([stack], [b_chip]) when op_flags[38] + u32xor([stack], [b_chip]) when op_flags[39] + # TODO: add match variant for caller + frie2f4() + drop([stack]) when op_flags[41] + 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] + mstorew([stack], [clk, b_chip]) when op_flags[46] + fmpupdate([stack], [fmp]) when op_flags[47] + + pad([stack]) when op_flags[48] + dup([stack]) when op_flags[49] + dup1([stack]) when op_flags[50] + dup2([stack]) when op_flags[51] + dup3([stack]) when op_flags[52] + dup4([stack]) when op_flags[53] + dup5([stack]) when op_flags[54] + dup6([stack]) when op_flags[55] + dup7([stack]) when op_flags[56] + dup9([stack]) when op_flags[57] + dup11([stack]) when op_flags[58] + dup13([stack]) when op_flags[59] + dup15([stack]) when op_flags[60] + advpop([stack]) when op_flags[61] + sdepth([stack, bookkeeping]) when op_flags[62] + clk([stack], [clk]) when op_flags[63] + + # No stack shift operations -ev noop(main: [s[16]], aux: [b[7]]): - enf f_dup(b) * delta(elem) = 0 for elem in stack +ev noop(main: [s[16]]): + enf delta(elem) = 0 for elem in s -ev eqz(main: [s[16], helper], aux: [b[7]]): - enf f_eqz(b) * (s[0]' * s[0]) = 0 - enf f_eqz(b) * (s[0]' - (1 - s[0] * helper)) - enf f_eqz(b) * delta(s[i]) = 0 for i in 1..16 +ev eqz(main: [s[16], h0]): + enf s[0]' * s[0] = 0 + enf s[0]' = 1 - s[0] * h0 + enf delta(s[i]) = 0 for i in 1..16 -ev neg(main: [s[16]], aux: [b[7]]): - enf f_neg(b) * (s[0]' + s[0]) = 0 - enf f_neg(b) * delta(s[i]) = 0 for i in 1..16 +ev neg(main: [s[16]]): + enf s[0]' + s[0] = 0 + enf delta(s[i]) = 0 for i in 1..16 -ev inv(main: [s[16]], aux: [b[7]]): - enf f_inv(b) * (1 - s[0]' * s[0]) = 0 - enf f_inv(b) * delta(s[i]) = 0 for i in 1..16 +ev inv(main: [s[16]]): + enf s[0]' * s[0] = 1 + enf delta(s[i]) = 0 for i in 1..16 -ev incr(main: [s[16]], aux: [b[7]]): - enf f_incr(b) * (s[0]' - s[0] - 1) = 0 - enf f_incr(b) * delta(s[i]) = 0 for i in 1..16 +ev incr(main: [s[16]]): + enf s[0]' = s[0] + 1 + enf delta(s[i]) = 0 for i in 1..16 -ev not(main: [s[16]], aux: [b[7]]): - enf f_not(b) * binary_check_sub(s[0]) - enf f_not(b) * (s[0]' - !s[0]) = 0 - enf f_not(b) * delta(s[i]) = 0 for i in 1..16 +ev not(main: [s[16]]): + enf is_binary([s[0]]) + enf s[0]' = !s[0] + enf delta(s[i]) = 0 for i in 1..16 -ev fmpadd(main: [s[16]], aux: [b[7], fmp]): - enf f_fmpadd(b) * (s[0]' - s[0] - fmp) = 0 - enf f_fmpadd(b) * delta(s[i]) = 0 for i in 1..16 +ev fmpadd(main: [s[16]], aux: [fmp]): + enf s[0]' = s[0] + fmp + enf delta(s[i]) = 0 for i in 1..16 # 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: [b[7], helper[3], clk, b_chip]): +ev mload(main: [s[16]], aux: [helper[3], clk, b_chip]): let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]']) let op_mem_read = 12 let u_mem = alpha[0] + alpha[1] * op_mem_read + alpha[3] * s[0] + alpha[4] * clk + v - enf f_mload(b) * (b_chip' * u_mem - b_chip) = 0 - enf f_mload(b) * delta(s[i]) = 0 for i in 1..16 + enf b_chip' * u_mem = b_chip + enf delta(s[i]) = 0 for i in 1..16 -ev swap(main: [s[16]], aux: [b[7]]): - enf f_swap(b) * (s[0]' - s[1]) = 0 - enf f_swap(b) * (s[1]' - s[0]) = 0 - enf f_swap(b) * delta(s[i]) = 0 for i in 2..16 +ev swap(main: [s[16]]): + enf s[0]' = s[1] + enf s[1]' = s[0] + enf delta(s[i]) = 0 for i in 2..16 # TODO: add constraints -ev caller(main: [s[16]], aux: [b[7]]): - -ev movup2(main: [s[16]], aux: [b[7]]): - enf f_movup2(b) * (s[0]' - s[2]) = 0 - enf f_movup2(b) * (s[i + 1]' - s[i]) = 0 for i in 0..2 - enf f_movup2(b) * delta(s[i]) = 0 for i in 3..16 - -ev movdn2(main: [s[16]], aux: [b[7]]): - enf f_movdn2(b) * (s[2]' - s[0]) = 0 - enf f_movdn2(b) * (s[i]' - s[i + 1]) = 0 for i in 0..2 - enf f_movdn2(b) * delta(s[i]) = 0 for i in 3..16 - -ev movup3(main: [s[16]], aux: [b[7]]): - enf f_movup3(b) * (s[0]' - s[3]) = 0 - enf f_movup3(b) * (s[i + 1]' - s[i]) = 0 for i in 0..3 - enf f_movup3(b) * delta(s[i]) = 0 for i in 4..16 - -ev movdn3(main: [s[16]], aux: [b[7]]): - enf f_movdn3(b) * (s[3]' - s[0]) = 0 - enf f_movdn3(b) * (s[i]' - s[i + 1]) = 0 for i in 0..3 - enf f_movdn3(b) * delta(s[i]) = 0 for i in 4..16 - -ev advpopw(main: [s[16]], aux: [b[7]]): - enf f_advpopw(b) * delta(s[i]) = 0 for i in 4..16 - -ev expacc(main: [s[16]], aux: [b[7], helper]): - enf f_expacc(b) * binary_check_sub(s[0]') - enf f_expacc(b) * (s[1]' - s[1]^2) = 0 - enf f_expacc(b) * (helper - ((s[1] - 1) * s[0]' + 1)) = 0 - enf f_expacc(b) * (s[2]' - s[2] * helper) = 0 - enf f_expacc(b) * (s[3]' - (s[3] * 2 + s[0]')) = 0 - enf f_expacc(b) * delta(s[i]) = 0 for i in 4..16 - -ev movup4(main: [s[16]], aux: [b[7]]): - enf f_movup4(b) * (s[0]' - s[4]) = 0 - enf f_movup4(b) * (s[i + 1]' - s[i]) = 0 for i in 0..4 - enf f_movup4(b) * delta(s[i]) = 0 for i in 5..16 - -ev movdn4(main: [s[16]], aux: [b[7]]): - enf f_movdn4(b) * (s[4]' - s[0]) = 0 - enf f_movdn4(b) * (s[i]' - s[i + 1]) = 0 for i in 0..4 - enf f_movdn4(b) * delta(s[i]) = 0 for i in 5..16 - -ev movup5(main: [s[16]], aux: [b[7]]): - enf f_movup5(b) * (s[0]' - s[5]) = 0 - enf f_movup5(b) * (s[i + 1]' - s[i]) = 0 for i in 0..5 - enf f_movup5(b) * delta(s[i]) = 0 for i in 6..16 - -ev movdn5(main: [s[16]], aux: [b[7]]): - enf f_movdn5(b) * (s[5]' - s[0]) = 0 - enf f_movdn5(b) * (s[i]' - s[i + 1]) = 0 for i in 0..5 - enf f_movdn5(b) * delta(s[i]) = 0 for i in 6..16 - -ev movup6(main: [s[16]], aux: [b[7]]): - enf f_movup6(b) * (s[0]' - s[6]) = 0 - enf f_movup6(b) * (s[i + 1]' - s[i]) = 0 for i in 0..6 - enf f_movup6(b) * delta(s[i]) = 0 for i in 7..16 - -ev movdn6(main: [s[16]], aux: [b[7]]): - enf f_movdn6(b) * (s[6]' - s[0]) = 0 - enf f_movdn6(b) * (s[i]' - s[i + 1]) = 0 for i in 0..6 - enf f_movdn6(b) * delta(s[i]) = 0 for i in 7..16 - -ev movup7(main: [s[16]], aux: [b[7]]): - enf f_movup7(b) * (s[0]' - s[7]) = 0 - enf f_movup7(b) * (s[i + 1]' - s[i]) = 0 for i in 0..7 - enf f_movup7(b) * delta(s[i]) = 0 for i in 8..16 - -ev movdn7(main: [s[16]], aux: [b[7]]): - enf f_movdn7(b) * (s[7]' - s[0]) = 0 - enf f_movdn7(b) * (s[i]' - s[i + 1]) = 0 for i in 0..7 - enf f_movdn7(b) * delta(s[i]) = 0 for i in 8..16 - -ev swapw(main: [s[16]], aux: [b[7]]): - enf f_swapw(b) * (s[i]' - s[i + 4]) = 0 for i in 0..4 - enf f_swapw(b) * (s[i + 4]' - s[i]) = 0 for i in 0..4 - enf f_swapw(b) * delta(s[i]) = 0 for i in 8..16 - -ev ext2mul(main: [s[16]], aux: [b[7]]): - enf f_ext2mul(b) * (s[0]' - s[0]) = 0 - enf f_ext2mul(b) * (s[1]' - s[1]) = 0 - enf f_ext2mul(b) * (s[2]' - (s[0] + s[1]) * (s[2] + s[3]) + s[0] * s[2]) = 0 - enf f_ext2mul(b) * (s[3]' - s[1] * s[3] + 2 * s[0] * s[2]) = 0 - enf f_ext2mul(b) * delta(s[i]) = 0 for i in 4..16 - -ev movup8(main: [s[16]], aux: [b[7]]): - enf f_movup8(b) * (s[0]' - s[8]) = 0 - enf f_movup8(b) * (s[i + 1]' - s[i]) = 0 for i in 0..8 - enf f_movup8(b) * delta(s[i]) = 0 for i in 9..16 - -ev movdn8(main: [s[16]], aux: [b[7]]): - enf f_movdn8(b) * (s[8]' - s[0]) = 0 - enf f_movdn8(b) * (s[i]' - s[i + 1]) = 0 for i in 0..8 - enf f_movdn8(b) * delta(s[i]) = 0 for i in 9..16 - -ev swapw2(main: [s[16]], aux: [b[7]]): - enf f_swapw2(b) * (s[i]' - s[i + 8]) = 0 for i in 0..4 - enf f_swapw2(b) * (s[i + 8]' - s[i]) = 0 for i in 0..4 - enf f_swapw2(b) * delta(s[i]) = 0 for i in 4..8 - enf f_swapw2(b) * delta(s[i]) = 0 for i in 12..16 +ev caller(main: [s[16]]): + +ev movup2(main: [s[16]]): + enf s[0]' = s[2] + enf s[i + 1]' = s[i] for i in 0..2 + enf delta(s[i]) = 0 for i in 3..16 + +ev movdn2(main: [s[16]]): + enf s[2]' = s[0] + enf s[i]' = s[i + 1] for i in 0..2 + enf delta(s[i]) = 0 for i in 3..16 + +ev movup3(main: [s[16]]): + enf s[0]' = s[3] + enf s[i + 1]' = s[i] for i in 0..3 + enf delta(s[i]) = 0 for i in 4..16 + +ev movdn3(main: [s[16]]): + enf s[3]' = s[0] + enf s[i]' = s[i + 1] for i in 0..3 + enf delta(s[i]) = 0 for i in 4..16 + +ev advpopw(main: [s[16]]): + enf delta(s[i]) = 0 for i in 4..16 + +ev expacc(main: [s[16]], aux: [h0]): + enf is_binary([s[0]']) + enf s[1]' = s[1]^2 + enf h0 = (s[1] - 1) * s[0]' + 1 + enf s[2]' = s[2] * h0 + enf s[3]' = s[3] * 2 + s[0]' + enf delta(s[i]) = 0 for i in 4..16 + +ev movup4(main: [s[16]]): + enf s[0]' = s[4] + enf s[i + 1]' = s[i] for i in 0..4 + enf delta(s[i]) = 0 for i in 5..16 + +ev movdn4(main: [s[16]]): + enf s[4]' = s[0] = 0 + enf s[i]' = s[i + 1] for i in 0..4 + enf delta(s[i]) = 0 for i in 5..16 + +ev movup5(main: [s[16]]): + enf s[0]' = s[5] + enf s[i + 1]' = s[i] for i in 0..5 + enf delta(s[i]) = 0 for i in 6..16 + +ev movdn5(main: [s[16]]): + enf s[5]' = s[0] + enf s[i]' = s[i + 1] for i in 0..5 + enf delta(s[i]) = 0 for i in 6..16 + +ev movup6(main: [s[16]]): + enf s[0]' = s[6] + enf s[i + 1]' = s[i] for i in 0..6 + enf delta(s[i]) = 0 for i in 7..16 + +ev movdn6(main: [s[16]]): + enf s[6]' = s[0] + enf s[i]' = s[i + 1] for i in 0..6 + enf delta(s[i]) = 0 for i in 7..16 + +ev movup7(main: [s[16]]): + enf s[0]' = s[7] = 0 + enf s[i + 1]' = s[i] for i in 0..7 + enf delta(s[i]) = 0 for i in 8..16 + +ev movdn7(main: [s[16]]): + enf s[7]' = s[0] + enf s[i]' = s[i + 1] for i in 0..7 + enf delta(s[i]) = 0 for i in 8..16 + +ev swapw(main: [s[16]]): + enf s[i]' = s[i + 4] for i in 0..4 + enf s[i + 4]' = s[i] for i in 0..4 + enf delta(s[i]) = 0 for i in 8..16 + +ev ext2mul(main: [s[16]]): + enf s[0]' = s[0] + enf s[1]' = s[1] + enf s[2]' = (s[0] + s[1]) * (s[2] + s[3]) - s[0] * s[2] + enf s[3]' = s[1] * s[3] - 2 * s[0] * s[2] + enf delta(s[i]) = 0 for i in 4..16 + +ev movup8(main: [s[16]]): + enf s[0]' = s[8] + enf s[i + 1]' = s[i] for i in 0..8 + enf delta(s[i]) = 0 for i in 9..16 + +ev movdn8(main: [s[16]]): + enf s[8]' = s[0] + enf s[i]' = s[i + 1] for i in 0..8 + enf delta(s[i]) = 0 for i in 9..16 + +ev swapw2(main: [s[16]]): + enf s[i]' = s[i + 8] for i in 0..4 + enf s[i + 8]' = s[i] for i in 0..4 + enf delta(s[i]) = 0 for i in 4..8 + enf delta(s[i]) = 0 for i in 12..16 # Should we enforce that elements in position grater than 15 do not change? -ev swapw3(main: [s[16]], aux: [b[7]]): - enf f_swapw3(b) * (s[i]' - s[i + 12]) = 0 for i in 0..4 - enf f_swapw3(b) * (s[i + 12]' - s[i]) = 0 for i in 0..4 - enf f_swapw3(b) * delta(s[i]) = 0 for i in 4..12 +ev swapw3(main: [s[16]]): + enf s[i]' = s[i + 12] for i in 0..4 + enf s[i + 12]' = s[i] for i in 0..4 + enf delta(s[i]) = 0 for i in 4..12 # Should we enforce that elements in position grater than 15 do not change? -ev swapdw(main: [s[16]], aux: [b[7]]): - enf f_swapdw(b) * (s[i]' - s[i + 8]) = 0 for i in 0..8 - enf f_swapdw(b) * (s[i + 8]' - s[i]) = 0 for i in 0..8 +ev swapdw(main: [s[16]]): + enf s[i]' = s[i + 8] for i in 0..8 + enf s[i + 8]' = s[i] for i in 0..8 # Left stack shift operationds -ev assert(main: [s[16]], aux: [b[7]]): - enf f_assert(b) * (s[0] - 1) = 0 - enf f_assert(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 +ev assert(main: [s[16]]): + enf s[0] = 1 + enf s[i]' = s[i + 1] for i in 0..15 -ev eq(main: [s[16]], aux: [b[7], helper]): - enf f_eq(b) * (s[0]' * (s[0] - s[1])) = 0 - enf f_eq(b) * (s[0]' - (1 - (s[0] - s[1]) * helper)) = 0 - enf f_eq(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 +ev eq(main: [s[16]], aux: [h0]): + enf s[0]' * (s[0] - s[1]) = 0 + enf s[0]' = 1 - (s[0] - s[1]) * h0 + enf s[i]' = s[i + 1] for i in 1..15 -ev add(main: [s[16]], aux: [b[7]]): - enf f_add(b) * (s[0]' - (s[0] + s[1])) = 0 - enf f_eq(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 +ev add(main: [s[16]]): + enf s[0]' = s[0] + s[1] + enf s[i]' = s[i + 1] for i in 1..15 -ev mul(main: [s[16]], aux: [b[7]]): - enf f_mul(b) * (s[0]' - s[0] * s[1]) = 0 - enf f_mul(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 +ev mul(main: [s[16]]): + enf s[0]' = s[0] * s[1] + enf s[i]' = s[i + 1] for i in 1..15 -ev and(main: [s[16]], aux: [b[7]]): - enf f_and(b) * binary_check_sub(s[i]) = 0 for i in 0..2 - enf f_and(b) * (s[0]' - s[0] * s[1]) = 0 - enf f_and(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 +ev and(main: [s[16]]): + enf is_binary([s[i]]) = 0 for i in 0..2 + enf s[0]' = s[0] * s[1] + enf s[i]' = s[i + 1] for i in 1..15 -ev or(main: [s[16]], aux: [b[7]]): - enf f_or(b) * binary_check_sub(s[i]) = 0 for i in 0..2 - enf f_or(b) * (s[0]' - (s[1] + s[0] - s[1] * s[0])) = 0 - enf f_or(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 +ev or(main: [s[16]]): + enf is_binary([s[i]]) = 0 for i in 0..2 + enf s[0]' = s[1] + s[0] - s[1] * s[0] + enf s[i]' = s[i + 1] for i in 1..15 -ev u32and(main: [s[16]], aux: [b[7], b_chip]): +ev u32and(main: [s[16]], aux: [b_chip]): let op_u32and = 2 - enf f_u32and(b) * b_chip' * (alpha[0] + alpha[1] * op_u32and + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip - enf f_u32and(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + enf b_chip' * (alpha[0] + alpha[1] * op_u32and + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf s[i]' = s[i + 1] for i in 1..15 -ev u32xor(main: [s[16]], aux: [b[7], b_chip]): +ev u32xor(main: [s[16]], aux: [b_chip]): let op_u32xor = 6 - enf f_u32xor(b) * b_chip' * (alpha[0] + alpha[1] * op_u32xor + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip - enf f_u32xor(b) * (s[i]' - s[i + 1]) = 0 for i in 1..15 + enf b_chip' * (alpha[0] + alpha[1] * op_u32xor + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf s[i]' = s[i + 1] for i in 1..15 # TODO: add constraints -ev frie2f4(main: [s[16]], aux: [b[7]]): +ev frie2f4(main: [s[16]]): -ev drop(main: [s[16]], aux: [b[7]]): - enf f_drop(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 +ev drop(main: [s[16]]): + enf s[i]' = s[i + 1] for i in 0..15 -ev cswap(main: [s[16]], aux: [b[7]]): - enf f_cswap(b) * binary_check_sub(s[0]) = 0 - enf f_cswap(b) * (s[0]' - s[0] * s[2] - (1 - s[0]) * s[1]) = 0 - enf f_cswap(b) * (s[1]' - s[0] * s[1] - (1 - s[0]) * s[2]) = 0 - enf f_cswap(b) * (s[i]' - s[i + 1]) = 0 for i in 2..15 +ev cswap(main: [s[16]]): + enf is_binary([s[0]]) = 0 + enf s[0]' = s[0] * s[2] + (1 - s[0]) * s[1] + enf s[1]' = s[0] * s[1] + (1 - s[0]) * s[2] + enf s[i]' = s[i + 1] for i in 2..15 -ev cswapw(main: [s[16]], aux: [b[7]]): - enf f_cswapw(b) * binary_check_sub(s[0]) = 0 - enf f_cswapw(b) * (s[i]' - s[0] * s[i + 5] - (1 - s[0]) * s[i + 1]) = 0 for i in 0..4 - enf f_cswapw(b) * (s[i + 4]' - s[0] * s[i + 1] + (1 - s[0]) * s[i + 5]) = 0 for i in 0..4 - enf f_cswapw(b) * (s[i]' - s[i + 1]) = 0 for i in 8..15 +ev cswapw(main: [s[16]]): + enf is_binary([s[0]]) = 0 + enf s[i]' = s[0] * s[i + 5] + (1 - s[0]) * s[i + 1] for i in 0..4 + enf s[i + 4]' = s[0] * s[i + 1] + (1 - s[0]) * s[i + 5] for i in 0..4 + enf s[i]' = s[i + 1] for i in 8..15 -ev mloadw(main: [s[16]], aux: [b[7], b_chip, clk]): +ev mloadw(main: [s[16]], aux: [clk, b_chip]): let v = sum([alpha[i + 5] * s[3 - i]' for i in 0..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 f_mloadw(b) * (b_chip' * u_mem - b_chip) = 0 - enf f_mloadw(b) * (s[i]' - s[i + 1]) = 0 for i in 4..15 + enf b_chip' * u_mem = b_chip + enf s[i]' = s[i + 1] for i in 4..15 -ev mstore(main: [s[16]], aux: [b[7], helper[3], clk, b_chip]): +ev mstore(main: [s[16]], aux: [helper[3], 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 - enf f_mstore(b) * (b_chip' * u_mem - b_chip) = 0 - enf f_mstore(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + enf b_chip' * u_mem = b_chip + enf s[i]' = s[i + 1] for i in 0..15 -ev mstorew(main: [s[16]], aux: [b[7]]): +ev mstorew(main: [s[16]], aux: [clk, b_chip]): let v = sum([alpha[i + 5] * s[3 - i]']) for i in 0..4 let op_mem_write = 4 let u_mem = alpha[0] + alpha[1] * op_mem_write + alpha[3] * s[0] + alpha[4] * clk + v - enf f_mstorew(b) * (b_chip' * u_mem - b_chip) = 0 - enf f_mstore(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 + enf b_chip' * u_mem = b_chip + enf s[i]' = s[i + 1] for i in 0..15 -ev fmpupdate(main: [s[16]], aux: [b[7], fmp]): - enf f_fmpupdate(b) * (fmp' - (fmp + s[0])) = 0 - enf f_fmpupdate(b) * (s[i]' - s[i + 1]) = 0 for i in 0..15 +ev fmpupdate(main: [s[16]], aux: [fmp]): + enf fmp' = fmp + s[0] + enf s[i]' = s[i + 1] for i in 0..15 # Right stack shift operations -ev pad(main: [s[16]], aux: [b[7]]): - enf f_pad(b) * s[0]' = 0 - enf f_pad(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev pad(main: [s[16]]): + enf s[0]' = 0 + enf s[i + 1]' = s[i] for i in 0..15 -ev dup(main: [s[16]], aux: [b[7]]): - enf f_dup(b) * (s[0]' - s[0]) = 0 - enf f_dup(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup(main: [s[16]]): + enf s[0]' = s[0] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup1(main: [s[16]], aux: [b[7]]): - enf f_dup1(b) * (s[0]' - s[1]) = 0 - enf f_dup1(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup1(main: [s[16]]): + enf s[0]' = s[1] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup2(main: [s[16]], aux: [b[7]]): - enf f_dup2(b) * (s[0]' - s[2]) = 0 - enf f_dup2(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup2(main: [s[16]]): + enf s[0]' = s[2] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup3(main: [s[16]], aux: [b[7]]): - enf f_dup3(b) * (s[0]' - s[3]) = 0 - enf f_dup3(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup3(main: [s[16]]): + enf s[0]' = s[3] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup4(main: [s[16]], aux: [b[7]]): - enf f_dup4(b) * (s[0]' - s[4]) = 0 - enf f_dup4(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup4(main: [s[16]]): + enf s[0]' = s[4] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup5(main: [s[16]], aux: [b[7]]): - enf f_dup5(b) * (s[0]' - s[5]) = 0 - enf f_dup5(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup5(main: [s[16]]): + enf s[0]' = s[5] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup6(main: [s[16]], aux: [b[7]]): - enf f_dup6(b) * (s[0]' - s[6]) = 0 - enf f_dup6(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup6(main: [s[16]]): + enf s[0]' = s[6] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup7(main: [s[16]], aux: [b[7]]): - enf f_dup7(b) * (s[0]' - s[7]) = 0 - enf f_dup7(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup7(main: [s[16]]): + enf s[0]' = s[7] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup9(main: [s[16]], aux: [b[7]]): - enf f_dup9(b) * (s[0]' - s[9]) = 0 - enf f_dup9(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup9(main: [s[16]]): + enf s[0]' = s[9] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup11(main: [s[16]], aux: [b[7]]): - enf f_dup11(b) * (s[0]' - s[11]) = 0 - enf f_dup11(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup11(main: [s[16]]): + enf s[0]' = s[11] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup13(main: [s[16]], aux: [b[7]]): - enf f_dup13(b) * (s[0]' - s[13]) = 0 - enf f_dup13(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup13(main: [s[16]]): + enf s[0]' = s[13] + enf s[i + 1]' = s[i] for i in 0..15 -ev dup15(main: [s[16]], aux: [b[7]]): - enf f_dup15(b) * (s[0]' - s[15]) = 0 - enf f_dup15(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev dup15(main: [s[16]]): + enf s[0]' = s[15] + enf s[i + 1]' = s[i] for i in 0..15 -ev advpop(main: [s[16]], aux: [b[7]]): - enf f_advpop(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev advpop(main: [s[16]]): + enf s[i + 1]' = s[i] for i in 0..15 -ev sdepth(main: [s[16], bookkeeping[2]], aux: [b[7]]): - enf f_sdepth(b) * (s[0]' - b[0]) = 0 - enf f_sdepth(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev sdepth(main: [s[16], bookkeeping[2]]): + enf s[0]' = bookkeeping[0] + enf s[i + 1]' = s[i] for i in 0..15 -ev clk(main: [s[16]], aux: [b[7], clk]): - enf f_clk(b) * (s[0]' - clk) = 0 - enf f_clk(b) * (s[i + 1]' - s[i]) = 0 for i in 0..15 +ev clk(main: [s[16]], aux: [clk]): + enf s[0]' = clk + enf s[i + 1]' = s[i] for i in 0..15 From 9e1178d8f1550d40c8a838e75da6eef9dd2ab41b Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Tue, 4 Apr 2023 05:18:00 +0300 Subject: [PATCH 05/12] feat: write u32 operations constraints --- constraints/miden-vm/stack.air | 297 ++++++++++++++++++++------------- 1 file changed, 183 insertions(+), 114 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index f982c6d06..5b8808aa2 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -2,10 +2,6 @@ mod StacktAir ### Helper functions ############################################################################## -fn delta(v: scalar) -> scalar: - return v' - v - - # Flags for the first bits (b[6], b[5], b[4]) fn f_000(b: vector[7]) -> scalar: @@ -498,157 +494,177 @@ ev is_binary(main: [a]): enf a^2 = a -ev range_check_16bit() +ev range_check_16bit(main: [helper[6]], aux: [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(main: [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, helper[6], clk, fmp], aux: [op_bits[7], extra, hasher5, 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] - neg([stack]) when op_flags[2] - inv([stack]) when op_flags[3] - incr([stack]) when op_flags[4] - not([stack]) when op_flags[5] - fmpadd([stack], [fmp]) when op_flags[6] - mload([stack], [helper, clk, b_chip]) when op_flags[7] - swap([stack]) when op_flags[8] + noop([stack]) when op_flags[0] + eqz([stack, h0]) when op_flags[1] + neg([stack]) when op_flags[2] + inv([stack]) when op_flags[3] + incr([stack]) when op_flags[4] + not([stack]) when op_flags[5] + fmpadd([stack, fmp]) when op_flags[6] + mload([stack, helper, clk], [b_chip]) when op_flags[7] + swap([stack]) when op_flags[8] # TODO: add match variant for caller caller() - movup2([stack]) when op_flags[10] - movdn2([stack]) when op_flags[11] - movup3([stack]) when op_flags[12] - movdn3([stack]) when op_flags[13] - advpopw([stack]) when op_flags[14] - expacc([stack], [h0]) when op_flags[15] - movup4([stack]) when op_flags[16] - movdn4([stack]) when op_flags[17] - movup5([stack]) when op_flags[18] - movdn5([stack]) when op_flags[19] - movup6([stack]) when op_flags[20] - movdn6([stack]) when op_flags[21] - movup7([stack]) when op_flags[22] - movdn7([stack]) when op_flags[23] - swapw([stack]) when op_flags[24] - ext2mul([stack]) when op_flags[25] - movup8([stack]) when op_flags[26] - movdn8([stack]) when op_flags[27] - swapw2([stack]) when op_flags[28] - swapw3([stack]) when op_flags[29] - swapdw([stack]) when op_flags[30] - - assert([stack]) when op_flags[32] - eq([stack], [h0]) when op_flags[33] - add([stack]) when op_flags[34] - mul([stack]) when op_flags[35] - and([stack]) when op_flags[36] - or([stack]) when op_flags[37] - u32and([stack], [b_chip]) when op_flags[38] - u32xor([stack], [b_chip]) when op_flags[39] + movup2([stack]) when op_flags[10] + movdn2([stack]) when op_flags[11] + movup3([stack]) when op_flags[12] + movdn3([stack]) when op_flags[13] + advpopw([stack]) when op_flags[14] + expacc([stack], [h0]) when op_flags[15] + movup4([stack]) when op_flags[16] + movdn4([stack]) when op_flags[17] + movup5([stack]) when op_flags[18] + movdn5([stack]) when op_flags[19] + movup6([stack]) when op_flags[20] + movdn6([stack]) when op_flags[21] + movup7([stack]) when op_flags[22] + movdn7([stack]) when op_flags[23] + swapw([stack]) when op_flags[24] + ext2mul([stack]) when op_flags[25] + movup8([stack]) when op_flags[26] + movdn8([stack]) when op_flags[27] + swapw2([stack]) when op_flags[28] + swapw3([stack]) when op_flags[29] + swapdw([stack]) when op_flags[30] + + assert([stack]) when op_flags[32] + eq([stack], [h0]) when op_flags[33] + add([stack]) when op_flags[34] + mul([stack]) when op_flags[35] + and([stack]) when op_flags[36] + or([stack]) when op_flags[37] + u32and([stack], [b_chip]) when op_flags[38] + u32xor([stack], [b_chip]) when op_flags[39] # TODO: add match variant for caller frie2f4() - drop([stack]) when op_flags[41] - 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] - mstorew([stack], [clk, b_chip]) when op_flags[46] - fmpupdate([stack], [fmp]) when op_flags[47] - - pad([stack]) when op_flags[48] - dup([stack]) when op_flags[49] - dup1([stack]) when op_flags[50] - dup2([stack]) when op_flags[51] - dup3([stack]) when op_flags[52] - dup4([stack]) when op_flags[53] - dup5([stack]) when op_flags[54] - dup6([stack]) when op_flags[55] - dup7([stack]) when op_flags[56] - dup9([stack]) when op_flags[57] - dup11([stack]) when op_flags[58] - dup13([stack]) when op_flags[59] - dup15([stack]) when op_flags[60] - advpop([stack]) when op_flags[61] - sdepth([stack, bookkeeping]) when op_flags[62] - clk([stack], [clk]) when op_flags[63] - + drop([stack]) when op_flags[41] + cswap([stack]) when op_flags[42] + cswapw([stack]) when op_flags[43] + mloadw([stack], [clk, b_chip]) when op_flags[44] + 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] + + pad([stack]) when op_flags[48] + dup([stack]) when op_flags[49] + dup1([stack]) when op_flags[50] + dup2([stack]) when op_flags[51] + dup3([stack]) when op_flags[52] + dup4([stack]) when op_flags[53] + dup5([stack]) when op_flags[54] + dup6([stack]) when op_flags[55] + dup7([stack]) when op_flags[56] + dup9([stack]) when op_flags[57] + dup11([stack]) when op_flags[58] + dup13([stack]) when op_flags[59] + dup15([stack]) when op_flags[60] + advpop([stack]) when op_flags[61] + sdepth([stack, bookkeeping]) when op_flags[62] + clk([stack], [clk]) when op_flags[63] + + u32add([stack, helper]) when op_flags[64] + u32sub([stack, helper]) when op_flags[65] + u32mul([stack, helper]) when op_flags[66] + u32div([stack, helper]) when op_flags[67] + u32split([stack, helper]) when op_flags[68] + u32assert2([stack, helper]) when op_flags[69] + u32add3([stack, helper]) when op_flags[70] + u32madd([stack, helper]) when op_flags[71] # No stack shift operations ev noop(main: [s[16]]): - enf delta(elem) = 0 for elem in s + enf elem' = elem for elem in s ev eqz(main: [s[16], h0]): enf s[0]' * s[0] = 0 enf s[0]' = 1 - s[0] * h0 - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 ev neg(main: [s[16]]): enf s[0]' + s[0] = 0 - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 ev inv(main: [s[16]]): enf s[0]' * s[0] = 1 - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 ev incr(main: [s[16]]): enf s[0]' = s[0] + 1 - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 ev not(main: [s[16]]): enf is_binary([s[0]]) enf s[0]' = !s[0] - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 -ev fmpadd(main: [s[16]], aux: [fmp]): +ev fmpadd(main: [s[16], fmp]): enf s[0]' = s[0] + fmp - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 # 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], helper[6], clk], aux: [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 + 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 - enf delta(s[i]) = 0 for i in 1..16 + enf s[i]' = s[i] for i in 1..16 ev swap(main: [s[16]]): enf s[0]' = s[1] enf s[1]' = s[0] - enf delta(s[i]) = 0 for i in 2..16 + enf s[i]' = s[i] for i in 2..16 # TODO: add constraints ev caller(main: [s[16]]): + ev movup2(main: [s[16]]): enf s[0]' = s[2] enf s[i + 1]' = s[i] for i in 0..2 - enf delta(s[i]) = 0 for i in 3..16 + enf s[i]' = s[i] for i in 3..16 ev movdn2(main: [s[16]]): enf s[2]' = s[0] enf s[i]' = s[i + 1] for i in 0..2 - enf delta(s[i]) = 0 for i in 3..16 + enf s[i]' = s[i] for i in 3..16 ev movup3(main: [s[16]]): enf s[0]' = s[3] enf s[i + 1]' = s[i] for i in 0..3 - enf delta(s[i]) = 0 for i in 4..16 + enf s[i]' = s[i] for i in 4..16 ev movdn3(main: [s[16]]): enf s[3]' = s[0] enf s[i]' = s[i + 1] for i in 0..3 - enf delta(s[i]) = 0 for i in 4..16 + enf s[i]' = s[i] for i in 4..16 ev advpopw(main: [s[16]]): - enf delta(s[i]) = 0 for i in 4..16 + enf s[i]' = s[i] for i in 4..16 ev expacc(main: [s[16]], aux: [h0]): enf is_binary([s[0]']) @@ -656,81 +672,81 @@ ev expacc(main: [s[16]], aux: [h0]): enf h0 = (s[1] - 1) * s[0]' + 1 enf s[2]' = s[2] * h0 enf s[3]' = s[3] * 2 + s[0]' - enf delta(s[i]) = 0 for i in 4..16 + enf s[i]' = s[i] for i in 4..16 ev movup4(main: [s[16]]): enf s[0]' = s[4] enf s[i + 1]' = s[i] for i in 0..4 - enf delta(s[i]) = 0 for i in 5..16 + enf s[i]' = s[i] for i in 5..16 ev movdn4(main: [s[16]]): enf s[4]' = s[0] = 0 enf s[i]' = s[i + 1] for i in 0..4 - enf delta(s[i]) = 0 for i in 5..16 + enf s[i]' = s[i] for i in 5..16 ev movup5(main: [s[16]]): enf s[0]' = s[5] enf s[i + 1]' = s[i] for i in 0..5 - enf delta(s[i]) = 0 for i in 6..16 + enf s[i]' = s[i] for i in 6..16 ev movdn5(main: [s[16]]): enf s[5]' = s[0] enf s[i]' = s[i + 1] for i in 0..5 - enf delta(s[i]) = 0 for i in 6..16 + enf s[i]' = s[i] for i in 6..16 ev movup6(main: [s[16]]): enf s[0]' = s[6] enf s[i + 1]' = s[i] for i in 0..6 - enf delta(s[i]) = 0 for i in 7..16 + enf s[i]' = s[i] for i in 7..16 ev movdn6(main: [s[16]]): enf s[6]' = s[0] enf s[i]' = s[i + 1] for i in 0..6 - enf delta(s[i]) = 0 for i in 7..16 + enf s[i]' = s[i] for i in 7..16 ev movup7(main: [s[16]]): enf s[0]' = s[7] = 0 enf s[i + 1]' = s[i] for i in 0..7 - enf delta(s[i]) = 0 for i in 8..16 + enf s[i]' = s[i] for i in 8..16 ev movdn7(main: [s[16]]): enf s[7]' = s[0] enf s[i]' = s[i + 1] for i in 0..7 - enf delta(s[i]) = 0 for i in 8..16 + enf s[i]' = s[i] for i in 8..16 ev swapw(main: [s[16]]): enf s[i]' = s[i + 4] for i in 0..4 enf s[i + 4]' = s[i] for i in 0..4 - enf delta(s[i]) = 0 for i in 8..16 + enf s[i]' = s[i] for i in 8..16 ev ext2mul(main: [s[16]]): enf s[0]' = s[0] enf s[1]' = s[1] enf s[2]' = (s[0] + s[1]) * (s[2] + s[3]) - s[0] * s[2] enf s[3]' = s[1] * s[3] - 2 * s[0] * s[2] - enf delta(s[i]) = 0 for i in 4..16 + enf s[i]' = s[i] for i in 4..16 ev movup8(main: [s[16]]): enf s[0]' = s[8] enf s[i + 1]' = s[i] for i in 0..8 - enf delta(s[i]) = 0 for i in 9..16 + enf s[i]' = s[i] for i in 9..16 ev movdn8(main: [s[16]]): enf s[8]' = s[0] enf s[i]' = s[i + 1] for i in 0..8 - enf delta(s[i]) = 0 for i in 9..16 + enf s[i]' = s[i] for i in 9..16 ev swapw2(main: [s[16]]): enf s[i]' = s[i + 8] for i in 0..4 enf s[i + 8]' = s[i] for i in 0..4 - enf delta(s[i]) = 0 for i in 4..8 - enf delta(s[i]) = 0 for i in 12..16 + enf s[i]' = s[i] for i in 4..8 + enf s[i]' = s[i] for i in 12..16 # Should we enforce that elements in position grater than 15 do not change? ev swapw3(main: [s[16]]): enf s[i]' = s[i + 12] for i in 0..4 enf s[i + 12]' = s[i] for i in 0..4 - enf delta(s[i]) = 0 for i in 4..12 + enf s[i]' = s[i] for i in 4..12 # Should we enforce that elements in position grater than 15 do not change? ev swapdw(main: [s[16]]): @@ -769,12 +785,12 @@ ev or(main: [s[16]]): ev u32and(main: [s[16]], aux: [b_chip]): let op_u32and = 2 - enf b_chip' * (alpha[0] + alpha[1] * op_u32and + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf b_chip' * ($alpha[0] + $alpha[1] * op_u32and + $alpha[2] * s[0] + $alpha[3] * s[1] + $alpha[4] * s[0]') = b_chip enf s[i]' = s[i + 1] for i in 1..15 ev u32xor(main: [s[16]], aux: [b_chip]): let op_u32xor = 6 - enf b_chip' * (alpha[0] + alpha[1] * op_u32xor + alpha[2] * s[0] + alpha[3] * s[1] + alpha[4] * s[0]') = b_chip + enf b_chip' * ($alpha[0] + $alpha[1] * op_u32xor + $alpha[2] * s[0] + $alpha[3] * s[1] + $alpha[4] * s[0]') = b_chip enf s[i]' = s[i + 1] for i in 1..15 # TODO: add constraints @@ -797,27 +813,27 @@ ev cswapw(main: [s[16]]): enf s[i]' = s[i + 1] for i in 8..15 ev mloadw(main: [s[16]], aux: [clk, b_chip]): - let v = sum([alpha[i + 5] * s[3 - i]' for i in 0..4]) + let v = sum([$alpha[i + 5] * s[3 - i]' for i in 0..4]) let op_mem_read = 12 - let u_mem = alpha[0] + alpha[1] * op_mem_read + alpha[3] * s[0] + alpha[4] * clk + v + 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 enf s[i]' = s[i + 1] for i in 4..15 -ev mstore(main: [s[16]], aux: [helper[3], clk, b_chip]): - let v = alpha[5] * s[0]' + sum([alpha[i + 5] * helper[3 - i]' for i in 1..4]) +ev mstore(main: [s[16], helper[6], clk], aux: [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 + let u_mem = $alpha[0] + $alpha[1] * op_mem_write + $alpha[3] * s[0] + $alpha[4] * clk + v enf b_chip' * u_mem = b_chip enf s[i]' = s[i + 1] for i in 0..15 ev mstorew(main: [s[16]], aux: [clk, b_chip]): - let v = sum([alpha[i + 5] * s[3 - i]']) for i in 0..4 + let v = sum([$alpha[i + 5] * s[3 - i]']) for i in 0..4 let op_mem_write = 4 - let u_mem = alpha[0] + alpha[1] * op_mem_write + alpha[3] * s[0] + alpha[4] * clk + v + let u_mem = $alpha[0] + $alpha[1] * op_mem_write + $alpha[3] * s[0] + $alpha[4] * clk + v enf b_chip' * u_mem = b_chip enf s[i]' = s[i + 1] for i in 0..15 -ev fmpupdate(main: [s[16]], aux: [fmp]): +ev fmpupdate(main: [s[16], fmp]): enf fmp' = fmp + s[0] enf s[i]' = s[i + 1] for i in 0..15 @@ -886,3 +902,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], 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 s[i]' = s[i] for i in 2..16 + +ev u32sub(main: [s[16], 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 s[i]' = s[i] for i in 2..16 + +ev u32mul(main: [s[16], 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 s[i]' = s[i] for i in 2..16 + +ev u32div(main: [s[16], 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 s[i]' = s[i] for i in 2..16 + +ev u32split(main: [s[16], 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], 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], 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], 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 \ No newline at end of file From 96804cd551d061bbda094fcb2077388b3ba09fec Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Wed, 5 Apr 2023 18:37:18 +0300 Subject: [PATCH 06/12] refactor: columns rename and bugs fix --- constraints/miden-vm/stack.air | 1010 +++++++++++++++++--------------- 1 file changed, 534 insertions(+), 476 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 5b8808aa2..efb9db937 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -2,174 +2,174 @@ mod StacktAir ### Helper functions ############################################################################## -# Flags for the first bits (b[6], b[5], b[4]) +# Flags for the first bits (op_bits[6], op_bits[5], op_bits[4]) -fn f_000(b: vector[7]) -> scalar: - return !b[6] & !b[5] & !b[4] +fn f_000(op_bits: vector[8]) -> scalar: + return !op_bits[6] & !op_bits[5] & !op_bits[4] -fn f_001(b: vector[7]) -> scalar: - return !b[6] & !b[5] & b[4] +fn f_001(op_bits: vector[8]) -> scalar: + return !op_bits[6] & !op_bits[5] & op_bits[4] -fn f_010(b: vector[7]) -> scalar: - return !b[6] & b[5] & !b[4] +fn f_010(op_bits: vector[8]) -> scalar: + return !op_bits[6] & op_bits[5] & !op_bits[4] -fn f_011(b: vector[7]) -> scalar: - return !b[6] & b[5] & b[4] +fn f_011(op_bits: vector[8]) -> scalar: + return !op_bits[6] & op_bits[5] & op_bits[4] # This flag is equal to f_100 -fn f_u32rc(b: vector[7]) -> scalar: - return b[6] & !b[5] & !b[4] +fn f_u32rc(op_bits: vector[8]) -> scalar: + return op_bits[6] & !op_bits[5] & !op_bits[4] -fn f_101(b: vector[7]) -> scalar: - return b[6] & !b[5] & b[4] +fn f_101(op_bits: vector[8]) -> scalar: + return op_bits[6] & !op_bits[5] & op_bits[4] -# Flags for the four last bits (b[3], b[2], b[1], b[0]) +# Flags for the four last bits (op_bits[3], op_bits[2], op_bits[1], op_bits[0]) -fn f_x0000(b: vector[7]) -> scalar: - return !b[3] & !b[2] & !b[1] & !b[0] +fn f_x0000(op_bits: vector[8]) -> scalar: + return !op_bits[3] & !op_bits[2] & !op_bits[1] & !op_bits[0] -fn f_x0001(b: vector[7]) -> scalar: - return !b[3] & !b[2] & !b[1] & b[0] +fn f_x0001(op_bits: vector[8]) -> scalar: + return !op_bits[3] & !op_bits[2] & !op_bits[1] & op_bits[0] -fn f_x0010(b: vector[7]) -> scalar: - return !b[3] & !b[2] & b[1] & !b[0] +fn f_x0010(op_bits: vector[8]) -> scalar: + return !op_bits[3] & !op_bits[2] & op_bits[1] & !op_bits[0] -fn f_x0011(b: vector[7]) -> scalar: - return !b[3] & !b[2] & b[1] & b[0] +fn f_x0011(op_bits: vector[8]) -> scalar: + return !op_bits[3] & !op_bits[2] & op_bits[1] & op_bits[0] -fn f_x0100(b: vector[7]) -> scalar: - return !b[3] & b[2] & !b[1] & !b[0] +fn f_x0100(op_bits: vector[8]) -> scalar: + return !op_bits[3] & op_bits[2] & !op_bits[1] & !op_bits[0] -fn f_x0101(b: vector[7]) -> scalar: - return !b[3] & b[2] & !b[1] & b[0] +fn f_x0101(op_bits: vector[8]) -> scalar: + return !op_bits[3] & op_bits[2] & !op_bits[1] & op_bits[0] -fn f_x0110(b: vector[7]) -> scalar: - return !b[3] & b[2] & b[1] & !b[0] +fn f_x0110(op_bits: vector[8]) -> scalar: + return !op_bits[3] & op_bits[2] & op_bits[1] & !op_bits[0] -fn f_x0111(b: vector[7]) -> scalar: - return !b[3] & b[2] & b[1] & b[0] +fn f_x0111(op_bits: vector[8]) -> scalar: + return !op_bits[3] & op_bits[2] & op_bits[1] & op_bits[0] -fn f_x1000(b: vector[7]) -> scalar: - return b[3] & !b[2] & !b[1] & !b[0] +fn f_x1000(op_bits: vector[8]) -> scalar: + return op_bits[3] & !op_bits[2] & !op_bits[1] & !op_bits[0] -fn f_x1001(b: vector[7]) -> scalar: - return b[3] & !b[2] & !b[1] & b[0] +fn f_x1001(op_bits: vector[8]) -> scalar: + return op_bits[3] & !op_bits[2] & !op_bits[1] & op_bits[0] -fn f_x1010(b: vector[7]) -> scalar: - return b[3] & !b[2] & b[1] & !b[0] +fn f_x1010(op_bits: vector[8]) -> scalar: + return op_bits[3] & !op_bits[2] & op_bits[1] & !op_bits[0] -fn f_x1011(b: vector[7]) -> scalar: - return b[3] & !b[2] & b[1] & b[0] +fn f_x1011(op_bits: vector[8]) -> scalar: + return op_bits[3] & !op_bits[2] & op_bits[1] & op_bits[0] -fn f_x1100(b: vector[7]) -> scalar: - return b[3] & b[2] & !b[1] & !b[0] +fn f_x1100(op_bits: vector[8]) -> scalar: + return op_bits[3] & op_bits[2] & !op_bits[1] & !op_bits[0] -fn f_x1101(b: vector[7]) -> scalar: - return b[3] & b[2] & !b[1] & b[0] +fn f_x1101(op_bits: vector[8]) -> scalar: + return op_bits[3] & op_bits[2] & !op_bits[1] & op_bits[0] -fn f_x1110(b: vector[7]) -> scalar: - return b[3] & b[2] & b[1] & !b[0] +fn f_x1110(op_bits: vector[8]) -> scalar: + return op_bits[3] & op_bits[2] & op_bits[1] & !op_bits[0] -fn f_x1111(b: vector[7]) -> scalar: - return b[3] & b[2] & b[1] & b[0] +fn f_x1111(op_bits: vector[8]) -> scalar: + return op_bits[3] & op_bits[2] & op_bits[1] & op_bits[0] # No stack shift operations -fn f_noop(b: vector[7]) -> scalar: - return f_000(b) & f_x0000(b) +fn f_noop(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0000(op_bits) -fn f_eqz(b: vector[7]) -> scalar: - return f_000(b) & f_x0001(b) +fn f_eqz(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0001(op_bits) -fn f_neg(b: vector[7]) -> scalar: - return f_000(b) & f_x0010(b) +fn f_neg(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0010(op_bits) -fn f_inv(b: vector[7]) -> scalar: - return f_000(b) & f_x0011(b) +fn f_inv(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0011(op_bits) -fn f_incr(b: vector[7]) -> scalar: - return f_000(b) & f_x0100(b) +fn f_incr(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0100(op_bits) -fn f_not(b: vector[7]) -> scalar: - return f_000(b) & f_x0101(b) +fn f_not(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0101(op_bits) -fn f_fmpadd(b: vector[7]) -> scalar: - return f_000(b) & f_x0110(b) +fn f_fmpadd(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0110(op_bits) -fn f_mload(b: vector[7]) -> scalar: - return f_000(b) & f_x0111(b) +fn f_mload(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x0111(op_bits) -fn f_swap(b: vector[7]) -> scalar: - return f_000(b) & f_x1000(b) +fn f_swap(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1000(op_bits) -fn f_caller(b: vector[7]) -> scalar: - return f_000(b) & f_x1001(b) +fn f_caller(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1001(op_bits) -fn f_movup2(b: vector[7]) -> scalar: - return f_000(b) & f_x1010(b) +fn f_movup2(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1010(op_bits) -fn f_movdn2(b: vector[7]) -> scalar: - return f_000(b) & f_x1011(b) +fn f_movdn2(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1011(op_bits) -fn f_movup3(b: vector[7]) -> scalar: - return f_000(b) & f_x1100(b) +fn f_movup3(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1100(op_bits) -fn f_movdn3(b: vector[7]) -> scalar: - return f_000(b) & f_x1101(b) +fn f_movdn3(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1101(op_bits) -fn f_advpopw(b: vector[7]) -> scalar: - return f_000(b) & f_x1110(b) +fn f_advpopw(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1110(op_bits) -fn f_expacc(b: vector[7]) -> scalar: - return f_000(b) & f_x1111(b) +fn f_expacc(op_bits: vector[8]) -> scalar: + return f_000(op_bits) & f_x1111(op_bits) -fn f_movup4(b: vector[7]) -> scalar: - return f_001(b) & f_x0000(b) +fn f_movup4(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0000(op_bits) -fn f_movdn4(b: vector[7]) -> scalar: - return f_001(b) & f_x0001(b) +fn f_movdn4(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0001(op_bits) -fn f_movup5(b: vector[7]) -> scalar: - return f_001(b) & f_x0010(b) +fn f_movup5(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0010(op_bits) -fn f_movdn5(b: vector[7]) -> scalar: - return f_001(b) & f_x0011(b) +fn f_movdn5(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0011(op_bits) -fn f_movup6(b: vector[7]) -> scalar: - return f_001(b) & f_x0100(b) +fn f_movup6(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0100(op_bits) -fn f_movdn6(b: vector[7]) -> scalar: - return f_001(b) & f_x0101(b) +fn f_movdn6(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0101(op_bits) -fn f_movup7(b: vector[7]) -> scalar: - return f_001(b) & f_x0110(b) +fn f_movup7(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0110(op_bits) -fn f_movdn7(b: vector[7]) -> scalar: - return f_001(b) & f_x0111(b) +fn f_movdn7(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x0111(op_bits) -fn f_swapw(b: vector[7]) -> scalar: - return f_001(b) & f_x1000(b) +fn f_swapw(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1000(op_bits) -fn f_ext2mul(b: vector[7]) -> scalar: - return f_001(b) & f_x1001(b) +fn f_ext2mul(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1001(op_bits) -fn f_movup8(b: vector[7]) -> scalar: - return f_001(b) & f_x1010(b) +fn f_movup8(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1010(op_bits) -fn f_movdn8(b: vector[7]) -> scalar: - return f_001(b) & f_x1011(b) +fn f_movdn8(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1011(op_bits) -fn f_swapw2(b: vector[7]) -> scalar: - return f_001(b) & f_x1100(b) +fn f_swapw2(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1100(op_bits) -fn f_swapw3(b: vector[7]) -> scalar: - return f_001(b) & f_x1101(b) +fn f_swapw3(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1101(op_bits) -fn f_swapdw(b: vector[7]) -> scalar: - return f_001(b) & f_x1110(b) +fn f_swapdw(op_bits: vector[8]) -> scalar: + return f_001(op_bits) & f_x1110(op_bits) fn f_001_1111() -> scalar: return 0 @@ -177,302 +177,303 @@ fn f_001_1111() -> scalar: # Left stack shift operations -fn f_assert(b: vector[7]) -> scalar: - return f_010(b) & f_x0000(b) +fn f_assert(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0000(op_bits) -fn f_eq(b: vector[7]) -> scalar: - return f_010(b) & f_x0001(b) +fn f_eq(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0001(op_bits) -fn f_add(b: vector[7]) -> scalar: - return f_010(b) & f_x0010(b) +fn f_add(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0010(op_bits) -fn f_mul(b: vector[7]) -> scalar: - return f_010(b) & f_x0011(b) +fn f_mul(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0011(op_bits) -fn f_and(b: vector[7]) -> scalar: - return f_010(b) & f_x0100(b) +fn f_and(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0100(op_bits) -fn f_or(b: vector[7]) -> scalar: - return f_010(b) & f_x0101(b) +fn f_or(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0101(op_bits) -fn f_u32and(b: vector[7]) -> scalar: - return f_010(b) & f_x0110(b) +fn f_u32and(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0110(op_bits) -fn f_u32xor(b: vector[7]) -> scalar: - return f_010(b) & f_x0111(b) +fn f_u32xor(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x0111(op_bits) -fn f_frie2f4(b: vector[7]) -> scalar: - return f_010(b) & f_x1000(b) +fn f_frie2f4(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1000(op_bits) -fn f_drop(b: vector[7]) -> scalar: - return f_010(b) & f_x1001(b) +fn f_drop(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1001(op_bits) -fn f_cswap(b: vector[7]) -> scalar: - return f_010(b) & f_x1010(b) +fn f_cswap(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1010(op_bits) -fn f_cswapw(b: vector[7]) -> scalar: - return f_010(b) & f_x1011(b) +fn f_cswapw(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1011(op_bits) -fn f_mloadw(b: vector[7]) -> scalar: - return f_010(b) & f_x1100(b) +fn f_mloadw(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1100(op_bits) -fn f_mstore(b: vector[7]) -> scalar: - return f_010(b) & f_x1101(b) +fn f_mstore(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1101(op_bits) -fn f_mstorew(b: vector[7]) -> scalar: - return f_010(b) & f_x1110(b) +fn f_mstorew(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1110(op_bits) -fn f_fmpupdate(b: vector[7]) -> scalar: - return f_010(b) & f_x1111(b) +fn f_fmpupdate(op_bits: vector[8]) -> scalar: + return f_010(op_bits) & f_x1111(op_bits) # Right stack shift operations -fn f_pad(b: vector[7]) -> scalar: - return f_011(b) & f_x0000(b) +fn f_pad(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0000(op_bits) -fn f_dup(b: vector[7]) -> scalar: - return f_011(b) & f_x0001(b) +fn f_dup(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0001(op_bits) -fn f_dup1(b: vector[7]) -> scalar: - return f_011(b) & f_x0010(b) +fn f_dup1(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0010(op_bits) -fn f_dup2(b: vector[7]) -> scalar: - return f_011(b) & f_x0011(b) +fn f_dup2(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0011(op_bits) -fn f_dup3(b: vector[7]) -> scalar: - return f_011(b) & f_x0100(b) +fn f_dup3(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0100(op_bits) -fn f_dup4(b: vector[7]) -> scalar: - return f_011(b) & f_x0101(b) +fn f_dup4(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0101(op_bits) -fn f_dup5(b: vector[7]) -> scalar: - return f_011(b) & f_x0110(b) +fn f_dup5(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0110(op_bits) -fn f_dup6(b: vector[7]) -> scalar: - return f_011(b) & f_x0111(b) +fn f_dup6(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x0111(op_bits) -fn f_dup7(b: vector[7]) -> scalar: - return f_011(b) & f_x1000(b) +fn f_dup7(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1000(op_bits) -fn f_dup9(b: vector[7]) -> scalar: - return f_011(b) & f_x1001(b) +fn f_dup9(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1001(op_bits) -fn f_dup11(b: vector[7]) -> scalar: - return f_011(b) & f_x1010(b) +fn f_dup11(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1010(op_bits) -fn f_dup13(b: vector[7]) -> scalar: - return f_011(b) & f_x1011(b) +fn f_dup13(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1011(op_bits) -fn f_dup15(b: vector[7]) -> scalar: - return f_011(b) & f_x1100(b) +fn f_dup15(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1100(op_bits) -fn f_advpop(b: vector[7]) -> scalar: - return f_011(b) & f_x1101(b) +fn f_advpop(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1101(op_bits) -fn f_sdepth(b: vector[7]) -> scalar: - return f_011(b) & f_x1110(b) +fn f_sdepth(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1110(op_bits) -fn f_clk(b: vector[7]) -> scalar: - return f_011(b) & f_x1111(b) +fn f_clk(op_bits: vector[8]) -> scalar: + return f_011(op_bits) & f_x1111(op_bits) # u32 operations -fn f_u32add(b: vector[7]) -> scalar: - return f_u32rc(b) & !b[3] & !b[2] & !b[1] +fn f_u32add(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1] -fn f_u32sub(b: vector[7]) -> scalar: - return f_u32rc(b) & !b[3] & !b[2] & b[1] +fn f_u32sub(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1] -fn f_u32mul(b: vector[7]) -> scalar: - return f_u32rc(b) & !b[3] & b[2] & !b[1] +fn f_u32mul(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1] -fn f_u32div(b: vector[7]) -> scalar: - return f_u32rc(b) & !b[3] & b[2] & b[1] +fn f_u32div(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1] -fn f_u32split(b: vector[7]) -> scalar: - return f_u32rc(b) & b[3] & !b[2] & !b[1] +fn f_u32split(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1] -fn f_u32assert2(b: vector[7]) -> scalar: - return f_u32rc(b) & b[3] & !b[2] & b[1] +fn f_u32assert2(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1] -fn f_u32add3(b: vector[7]) -> scalar: - return f_u32rc(b) & b[3] & b[2] & !b[1] +fn f_u32add3(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1] -fn f_madd(b: vector[7]) -> scalar: - return f_u32rc(b) & b[3] & b[2] & b[1] +fn f_madd(op_bits: vector[8]) -> scalar: + return f_u32rc(op_bits) & op_bits[3] & op_bits[2] & op_bits[1] # High-degree operations -fn f_hperm(b: vector[7]) -> scalar: - return f_101(b) & !b[3] & !b[2] & !b[1] +fn f_hperm(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1] -fn f_mpverify(b: vector[7]) -> scalar: - return f_101(b) & !b[3] & !b[2] & b[1] +fn f_mpverify(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1] -fn f_pipe(b: vector[7]) -> scalar: - return f_101(b) & !b[3] & b[2] & !b[1] +fn f_pipe(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1] -fn f_mstream(b: vector[7]) -> scalar: - return f_101(b) & !b[3] & b[2] & b[1] +fn f_mstream(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1] -fn f_span(b: vector[7]) -> scalar: - return f_101(b) & b[3] & !b[2] & !b[1] +fn f_span(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1] -fn f_join(b: vector[7]) -> scalar: - return f_101(b) & b[3] & !b[2] & b[1] +fn f_join(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1] -fn f_split(b: vector[7]) -> scalar: - return f_101(b) & b[3] & b[2] & !b[1] +fn f_split(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1] -fn f_loop(b: vector[7]) -> scalar: - return f_101(b) & b[3] & b[2] & b[1] +fn f_loop(op_bits: vector[8]) -> scalar: + return f_101(op_bits) & op_bits[3] & op_bits[2] & op_bits[1] # Very high-degree operations -fn f_mrupdate(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & !b[3] & !b[2] +fn f_mrupdate(op_bits: vector[8]) -> scalar: + return op_bits[7] & !op_bits[4] & !op_bits[3] & !op_bits[2] -fn f_push(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & !b[3] & b[2] +fn f_push(op_bits: vector[8]) -> scalar: + return op_bits[7] & !op_bits[4] & !op_bits[3] & op_bits[2] -fn f_syscall(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & b[3] & !b[2] +fn f_syscall(op_bits: vector[8]) -> scalar: + return op_bits[7] & !op_bits[4] & op_bits[3] & !op_bits[2] -fn f_call(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & b[3] & b[2] +fn f_call(op_bits: vector[8]) -> scalar: + return op_bits[7] & !op_bits[4] & op_bits[3] & op_bits[2] -fn f_end(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & !b[3] & !b[2] +fn f_end(op_bits: vector[8]) -> scalar: + return op_bits[7] & op_bits[4] & !op_bits[3] & !op_bits[2] -fn f_repeat(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & !b[3] & b[2] +fn f_repeat(op_bits: vector[8]) -> scalar: + return op_bits[7] & op_bits[4] & !op_bits[3] & op_bits[2] -fn f_respan(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & b[3] & !b[2] +fn f_respan(op_bits: vector[8]) -> scalar: + return op_bits[7] & op_bits[4] & op_bits[3] & !op_bits[2] -fn f_halt(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & b[3] & b[2] +fn f_halt(op_bits: vector[8]) -> scalar: + return op_bits[7] & op_bits[4] & op_bits[3] & op_bits[2] # Composite flags -fn f_shr(b: vector[7], extra: scalar) -> scalar: - return !b[6] & b[5] & b[4] + f_u32split(b) + f_push(b, extra) +fn f_shr(op_bits: vector[8]) -> scalar: + return !op_bits[6] & op_bits[5] & op_bits[4] + f_u32split(op_bits) + f_push(op_bits) -fn f_shl(b: vector[7], extra: scalar, h5: scalar) -> scalar: - let f_add3_mad = b[6] & !b[5] & !b[4] & b[3] & b[2] - let f_split_loop = b[6] & !b[5] & b[4] & b[3] & b[2] - return !b[6] & b[5] & !b[4] + f_add3_mad + f_split_loop + f_repeat(b, extra) + f_end(b, extra) * h5 +# hasher[5] = op_helpers[3], where hahser -- main columns from the decoder, helper -- aux columns from the stack +fn f_shl(op_bits: vector[8], op_helpers: vector[6]) -> scalar: + let f_add3_mad = op_bits[6] & !op_bits[5] & !op_bits[4] & op_bits[3] & op_bits[2] + let f_split_loop = op_bits[6] & !op_bits[5] & op_bits[4] & op_bits[3] & op_bits[2] + return !op_bits[6] & op_bits[5] & !op_bits[4] + f_add3_mad + f_split_loop + f_repeat(op_bits) + f_end(op_bits) * op_helpers[3] -fn f_ctrl(b: vector[7], extra: scalar) -> scalar: +fn f_ctrl(op_bits: vector[8]) -> scalar: # flag for SPAN, JOIN, SPLIT, LOOP - let f_sjsl = b[6] & !b[5] & b[4] & b[3] + let f_sjsl = op_bits[6] & !op_bits[5] & op_bits[4] & op_bits[3] # flag for END, REPEAT, RESPAN, HALT - let f_errh = b[6] & b[5] & b[4] + let f_errh = op_bits[6] & op_bits[5] & op_bits[4] - return f_sjsl + f_errh + f_call(b, extra) + f_syscall(b, extra) + return f_sjsl + f_errh + f_call(op_bits) + f_syscall(op_bits) -fn compute_op_flags(b: vector[7], extra: scalar) -> vector[88]: +fn compute_op_flags(op_bits: vector[8]) -> vector[88]: return [ - f_noop(b), - f_eqz(b), - f_neg(b), - f_inv(b), - f_incr(b), - f_not(b), - f_fmpadd(b), - f_mload(b), - f_swap(b), - f_caller(b), - f_movup2(b), - f_movdn2(b), - f_movup3(b), - f_movdn3(b), - f_advpopw(b), - f_expacc(b), - f_movup4(b), - f_movdn4(b), - f_movup5(b), - f_movdn5(b), - f_movup6(b), - f_movdn6(b), - f_movup7(b), - f_movdn7(b), - f_swapw(b), - f_ext2mul(b), - f_movup8(b), - f_movdn8(b), - f_swapw2(b), - f_swapw3(b), - f_swapdw(b), - f_001_1111(b), - - f_assert(b), - f_eq(b), - f_add(b), - f_mul(b), - f_and(b), - f_or(b), - f_u32and(b), - f_u32xor(b), - f_frie2f4(b), - f_drop(b), - f_cswap(b), - f_cswapw(b), - f_mloadw(b), - f_mstore(b), - f_mstorew(b), - f_fmpupdate(b), - - f_pad(b), - f_dup(b), - f_dup1(b), - f_dup2(b), - f_dup3(b), - f_dup4(b), - f_dup5(b), - f_dup6(b), - f_dup7(b), - f_dup9(b), - f_dup11(b), - f_dup13(b), - f_dup15(b), - f_advpop(b), - f_sdepth(b), - f_clk(b), - - f_u32add(b), - f_u32sub(b), - f_u32mul(b), - f_u32div(b), - f_u32split(b), - f_u32assert2(b), - f_u32add3(b), - f_madd(b), - - f_hperm(b), - f_mpverify(b), - f_pipe(b), - f_mstream(b), - f_span(b), - f_join(b), - f_split(b), - f_loop(b), - - f_mrupdate(b, extra), - f_push(b, extra), - f_syscall(b, extra), - f_call(b, extra), - f_end(b, extra), - f_repeat(b, extra), - f_respan(b, extra), - f_halt(b, extra) + f_noop(op_bits), + f_eqz(op_bits), + f_neg(op_bits), + f_inv(op_bits), + f_incr(op_bits), + f_not(op_bits), + f_fmpadd(op_bits), + f_mload(op_bits), + f_swap(op_bits), + f_caller(op_bits), + f_movup2(op_bits), + f_movdn2(op_bits), + f_movup3(op_bits), + f_movdn3(op_bits), + f_advpopw(op_bits), + f_expacc(op_bits), + f_movup4(op_bits), + f_movdn4(op_bits), + f_movup5(op_bits), + f_movdn5(op_bits), + f_movup6(op_bits), + f_movdn6(op_bits), + f_movup7(op_bits), + f_movdn7(op_bits), + f_swapw(op_bits), + f_ext2mul(op_bits), + f_movup8(op_bits), + f_movdn8(op_bits), + f_swapw2(op_bits), + f_swapw3(op_bits), + f_swapdw(op_bits), + f_001_1111(op_bits), + + f_assert(op_bits), + f_eq(op_bits), + f_add(op_bits), + f_mul(op_bits), + f_and(op_bits), + f_or(op_bits), + f_u32and(op_bits), + f_u32xor(op_bits), + f_frie2f4(op_bits), + f_drop(op_bits), + f_cswap(op_bits), + f_cswapw(op_bits), + f_mloadw(op_bits), + f_mstore(op_bits), + f_mstorew(op_bits), + f_fmpupdate(op_bits), + + f_pad(op_bits), + f_dup(op_bits), + f_dup1(op_bits), + f_dup2(op_bits), + f_dup3(op_bits), + f_dup4(op_bits), + f_dup5(op_bits), + f_dup6(op_bits), + f_dup7(op_bits), + f_dup9(op_bits), + f_dup11(op_bits), + f_dup13(op_bits), + f_dup15(op_bits), + f_advpop(op_bits), + f_sdepth(op_bits), + f_clk(op_bits), + + f_u32add(op_bits), + f_u32sub(op_bits), + f_u32mul(op_bits), + f_u32div(op_bits), + f_u32split(op_bits), + f_u32assert2(op_bits), + f_u32add3(op_bits), + f_madd(op_bits), + + f_hperm(op_bits), + f_mpverify(op_bits), + f_pipe(op_bits), + f_mstream(op_bits), + f_span(op_bits), + f_join(op_bits), + f_split(op_bits), + f_loop(op_bits), + + f_mrupdate(op_bits), + f_push(op_bits), + f_syscall(op_bits), + f_call(op_bits), + f_end(op_bits), + f_repeat(op_bits), + f_respan(op_bits), + f_halt(op_bits) ] @@ -494,109 +495,114 @@ ev is_binary(main: [a]): enf a^2 = a -ev range_check_16bit(main: [helper[6]], aux: [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(main: [op_helpers[6]]): + let m = op_helpers[4] + let v_hi = 2^16 * op_helpers[3] + op_helpers[2] + let v_lo = 2^16 * op_helpers[1] + op_helpers[0] + enf (1 - m * (2^32 - 1 - v_hi)) * v_lo = 0 -ev check_element_validity(main: [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 +ev b0_is_zero(main: [op_bits[8]]): + enf op_bits[6] & !op_bits[5] & op_bits[0] = 0 + + +ev b0_b1_is_zero(main: [op_bits[8]]): + enf op_bits[6] & op_bits[5] & op_bits[0] = 0 + enf op_bits[6] & op_bits[5] & op_bits[1] = 0 ### Stack Air Constraints ######################################################################### # Enforces the constraints on the stack. # TODO: add docs for columns -ev stack_constraints(main: [stack[16], bookkeeping[2], h0, helper[6], clk, fmp], aux: [op_bits[7], extra, hasher5, b_chip, b_range]): - let op_flags = compute_op_flags(op_bits, extra) - - enf range_check_16bit([helper], [b_range]) when f_u32rc([stack]) +# stack_helpers consists of [bookkeeping[0], bookkeeping[1], h0] +# op_bits consists of [op_bits[7], extra] +ev stack_constraints(main: [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp]): + let op_flags = compute_op_flags(op_bits) match enf: - noop([stack]) when op_flags[0] - eqz([stack, h0]) when op_flags[1] - neg([stack]) when op_flags[2] - inv([stack]) when op_flags[3] - incr([stack]) when op_flags[4] - not([stack]) when op_flags[5] - fmpadd([stack, fmp]) when op_flags[6] - mload([stack, helper, clk], [b_chip]) when op_flags[7] - swap([stack]) when op_flags[8] + noop([stack_top]) when op_flags[0] + eqz([stack_top, stack_helpers[2]]) when op_flags[1] + neg([stack_top]) when op_flags[2] + inv([stack_top]) when op_flags[3] + incr([stack_top]) when op_flags[4] + not([stack_top]) when op_flags[5] + fmpadd([stack_top, fmp]) when op_flags[6] + mload([stack_top, op_helpers, clk]) when op_flags[7] + swap([stack_top]) when op_flags[8] # TODO: add match variant for caller caller() - movup2([stack]) when op_flags[10] - movdn2([stack]) when op_flags[11] - movup3([stack]) when op_flags[12] - movdn3([stack]) when op_flags[13] - advpopw([stack]) when op_flags[14] - expacc([stack], [h0]) when op_flags[15] - movup4([stack]) when op_flags[16] - movdn4([stack]) when op_flags[17] - movup5([stack]) when op_flags[18] - movdn5([stack]) when op_flags[19] - movup6([stack]) when op_flags[20] - movdn6([stack]) when op_flags[21] - movup7([stack]) when op_flags[22] - movdn7([stack]) when op_flags[23] - swapw([stack]) when op_flags[24] - ext2mul([stack]) when op_flags[25] - movup8([stack]) when op_flags[26] - movdn8([stack]) when op_flags[27] - swapw2([stack]) when op_flags[28] - swapw3([stack]) when op_flags[29] - swapdw([stack]) when op_flags[30] - - assert([stack]) when op_flags[32] - eq([stack], [h0]) when op_flags[33] - add([stack]) when op_flags[34] - mul([stack]) when op_flags[35] - and([stack]) when op_flags[36] - or([stack]) when op_flags[37] - u32and([stack], [b_chip]) when op_flags[38] - u32xor([stack], [b_chip]) when op_flags[39] + movup2([stack_top]) when op_flags[10] + movdn2([stack_top]) when op_flags[11] + movup3([stack_top]) when op_flags[12] + movdn3([stack_top]) when op_flags[13] + advpopw([stack_top]) when op_flags[14] + expacc([stack_top, stack_helpers[2]]) when op_flags[15] + movup4([stack_top]) when op_flags[16] + movdn4([stack_top]) when op_flags[17] + movup5([stack_top]) when op_flags[18] + movdn5([stack_top]) when op_flags[19] + movup6([stack_top]) when op_flags[20] + movdn6([stack_top]) when op_flags[21] + movup7([stack_top]) when op_flags[22] + movdn7([stack_top]) when op_flags[23] + swapw([stack_top]) when op_flags[24] + ext2mul([stack_top]) when op_flags[25] + movup8([stack_top]) when op_flags[26] + movdn8([stack_top]) when op_flags[27] + swapw2([stack_top]) when op_flags[28] + swapw3([stack_top]) when op_flags[29] + swapdw([stack_top]) when op_flags[30] + + assert([stack_top]) when op_flags[32] + eq([stack_top, stack_helpers[2]]) when op_flags[33] + add([stack_top]) when op_flags[34] + mul([stack_top]) when op_flags[35] + and([stack_top]) when op_flags[36] + or([stack_top]) when op_flags[37] + u32and([stack_top]) when op_flags[38] + u32xor([stack_top]) when op_flags[39] # TODO: add match variant for caller frie2f4() - drop([stack]) when op_flags[41] - cswap([stack]) when op_flags[42] - cswapw([stack]) when op_flags[43] - mloadw([stack], [clk, b_chip]) when op_flags[44] - 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] - - pad([stack]) when op_flags[48] - dup([stack]) when op_flags[49] - dup1([stack]) when op_flags[50] - dup2([stack]) when op_flags[51] - dup3([stack]) when op_flags[52] - dup4([stack]) when op_flags[53] - dup5([stack]) when op_flags[54] - dup6([stack]) when op_flags[55] - dup7([stack]) when op_flags[56] - dup9([stack]) when op_flags[57] - dup11([stack]) when op_flags[58] - dup13([stack]) when op_flags[59] - dup15([stack]) when op_flags[60] - advpop([stack]) when op_flags[61] - sdepth([stack, bookkeeping]) when op_flags[62] - clk([stack], [clk]) when op_flags[63] - - u32add([stack, helper]) when op_flags[64] - u32sub([stack, helper]) when op_flags[65] - u32mul([stack, helper]) when op_flags[66] - u32div([stack, helper]) when op_flags[67] - u32split([stack, helper]) when op_flags[68] - u32assert2([stack, helper]) when op_flags[69] - u32add3([stack, helper]) when op_flags[70] - u32madd([stack, helper]) when op_flags[71] + drop([stack_top]) when op_flags[41] + cswap([stack_top]) when op_flags[42] + cswapw([stack_top]) when op_flags[43] + mloadw([stack_top, clk]) when op_flags[44] + mstore([stack_top, op_helpers, clk]) when op_flags[45] + mstorew([stack_top, clk]) when op_flags[46] + fmpupdate([stack_top, fmp]) when op_flags[47] + + pad([stack_top]) when op_flags[48] + dup([stack_top]) when op_flags[49] + dup1([stack_top]) when op_flags[50] + dup2([stack_top]) when op_flags[51] + dup3([stack_top]) when op_flags[52] + dup4([stack_top]) when op_flags[53] + dup5([stack_top]) when op_flags[54] + dup6([stack_top]) when op_flags[55] + dup7([stack_top]) when op_flags[56] + dup9([stack_top]) when op_flags[57] + dup11([stack_top]) when op_flags[58] + dup13([stack_top]) when op_flags[59] + dup15([stack_top]) when op_flags[60] + advpop([stack_top]) when op_flags[61] + sdepth([stack_top, stack_helpers[0]]) when op_flags[62] + clk([stack_top, clk]) when op_flags[63] + + u32add([stack_top, op_helpers]) when op_flags[64] + u32sub([stack_top, op_helpers]) when op_flags[65] + u32mul([stack_top, op_helpers]) when op_flags[66] + u32div([stack_top, op_helpers]) when op_flags[67] + u32split([stack_top, op_helpers]) when op_flags[68] + u32assert2([stack_top, op_helpers]) when op_flags[69] + u32add3([stack_top, op_helpers]) when op_flags[70] + u32madd([stack_top, op_helpers]) when op_flags[71] # No stack shift operations ev noop(main: [s[16]]): - enf elem' = elem for elem in s + enf s[i]' = s[i] for i in 0..16 ev eqz(main: [s[16], h0]): enf s[0]' * s[0] = 0 @@ -624,14 +630,8 @@ ev fmpadd(main: [s[16], fmp]): enf s[0]' = s[0] + fmp enf s[i]' = s[i] for i in 1..16 -# 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], helper[6], clk], aux: [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 +# Bus constraint is implemented in a separate file +ev mload(main: [s[16], clk]): enf s[i]' = s[i] for i in 1..16 ev swap(main: [s[16]]): @@ -666,7 +666,7 @@ ev movdn3(main: [s[16]]): ev advpopw(main: [s[16]]): enf s[i]' = s[i] for i in 4..16 -ev expacc(main: [s[16]], aux: [h0]): +ev expacc(main: [s[16], h0]): enf is_binary([s[0]']) enf s[1]' = s[1]^2 enf h0 = (s[1] - 1) * s[0]' + 1 @@ -760,7 +760,7 @@ ev assert(main: [s[16]]): enf s[0] = 1 enf s[i]' = s[i + 1] for i in 0..15 -ev eq(main: [s[16]], aux: [h0]): +ev eq(main: [s[16], h0]): enf s[0]' * (s[0] - s[1]) = 0 enf s[0]' = 1 - (s[0] - s[1]) * h0 enf s[i]' = s[i + 1] for i in 1..15 @@ -783,14 +783,12 @@ ev or(main: [s[16]]): enf s[0]' = s[1] + s[0] - s[1] * s[0] enf s[i]' = s[i + 1] for i in 1..15 -ev u32and(main: [s[16]], aux: [b_chip]): - let op_u32and = 2 - enf b_chip' * ($alpha[0] + $alpha[1] * op_u32and + $alpha[2] * s[0] + $alpha[3] * s[1] + $alpha[4] * s[0]') = b_chip +# Bus constraint is implemented in a separate file +ev u32and(main: [s[16]]): enf s[i]' = s[i + 1] for i in 1..15 -ev u32xor(main: [s[16]], aux: [b_chip]): - let op_u32xor = 6 - enf b_chip' * ($alpha[0] + $alpha[1] * op_u32xor + $alpha[2] * s[0] + $alpha[3] * s[1] + $alpha[4] * s[0]') = b_chip +# Bus constraint is implemented in a separate file +ev u32xor(main: [s[16]]): enf s[i]' = s[i + 1] for i in 1..15 # TODO: add constraints @@ -812,25 +810,16 @@ ev cswapw(main: [s[16]]): enf s[i + 4]' = s[0] * s[i + 1] + (1 - s[0]) * s[i + 5] for i in 0..4 enf s[i]' = s[i + 1] for i in 8..15 -ev mloadw(main: [s[16]], aux: [clk, b_chip]): - let v = sum([$alpha[i + 5] * s[3 - i]' for i in 0..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 +# Bus constraint is implemented in a separate file +ev mloadw(main: [s[16], clk]): enf s[i]' = s[i + 1] for i in 4..15 -ev mstore(main: [s[16], helper[6], clk], aux: [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 - enf b_chip' * u_mem = b_chip +# Bus constraint is implemented in a separate file +ev mstore(main: [s[16], clk]): enf s[i]' = s[i + 1] for i in 0..15 -ev mstorew(main: [s[16]], aux: [clk, b_chip]): - let v = sum([$alpha[i + 5] * s[3 - i]']) for i in 0..4 - let op_mem_write = 4 - let u_mem = $alpha[0] + $alpha[1] * op_mem_write + $alpha[3] * s[0] + $alpha[4] * clk + v - enf b_chip' * u_mem = b_chip +# Bus constraint is implemented in a separate file +ev mstorew(main: [s[16], clk]): enf s[i]' = s[i + 1] for i in 0..15 ev fmpupdate(main: [s[16], fmp]): @@ -895,63 +884,132 @@ ev dup15(main: [s[16]]): ev advpop(main: [s[16]]): enf s[i + 1]' = s[i] for i in 0..15 -ev sdepth(main: [s[16], bookkeeping[2]]): - enf s[0]' = bookkeeping[0] +ev sdepth(main: [s[16], bookkeeping]): + enf s[0]' = bookkeeping enf s[i + 1]' = s[i] for i in 0..15 -ev clk(main: [s[16]], aux: [clk]): +ev clk(main: [s[16], clk]): enf s[0]' = clk enf s[i + 1]' = s[i] for i in 0..15 # u32 operations -ev u32add(main: [s[16], 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] +ev u32add(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0] + s[1] = 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] + enf s[0]' = op_helpers[2] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i] for i in 2..16 + enf b0_is_zero([op_bits]) -ev u32sub(main: [s[16], helper[6]]): +ev u32sub(main: [s[16], op_bits[8], op_helpers[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 s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i] for i in 2..16 + enf b0_is_zero([op_bits]) -ev u32mul(main: [s[16], 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]) +ev u32mul(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0] * s[1] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] + enf check_element_validity([op_helpers]) enf s[i]' = s[i] for i in 2..16 + enf b0_is_zero([op_bits]) -ev u32div(main: [s[16], helper[6]]): +ev u32div(main: [s[16], op_bits[8], op_helpers[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 s[1] - s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[0] - s[0]' - 1 = 2^16 * op_helpers[2] + op_helpers[3] enf s[i]' = s[i] for i in 2..16 + enf b0_is_zero([op_bits]) -ev u32split(main: [s[16], 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]) +ev u32split(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] + enf check_element_validity([op_helpers]) enf s[i + 1]' = s[i] for i in 1..15 + enf b0_is_zero([op_bits]) + +ev u32assert2(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[i]' = s[i] for i in 0..16 + enf b0_is_zero([op_bits]) + +ev u32add3(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0] + s[1] + s[2] = 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] + enf s[0]' = op_helpers[2] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[i]' = s[i + 1] for i in 2..15 + enf b0_is_zero([op_bits]) -ev u32assert2(main: [s[16], 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], 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] +ev u32madd(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[0] * s[1] + s[2] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] + enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] + enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] + enf check_element_validity([op_helpers]) enf s[i]' = s[i + 1] for i in 2..15 + enf b0_is_zero([op_bits]) + + +# High-degree operations + +# Bus constraint is implemented in a separate file +ev hperm(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[i]' = s[i] for i in 12..16 + enf b0_is_zero([op_bits]) + +# Bus constraint is implemented in a separate file +ev mpverify(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[i]' = s[i] for i in 0..16 + enf b0_is_zero([op_bits]) + +# TODO: add constraints +ev pipe(main: [s[16], op_bits[8], op_helpers[6]]): + + +# TODO: add constraints +ev mstream(main: [s[16], op_bits[8], op_helpers[6]]): + + +ev span(main: [s[16], op_bits[8], op_helpers[6]]) + + +ev join() + + +ev split() + + +ev loop() + + +# Very high-degree operations + +# Bus constraint is implemented in a separate file +ev mrupdate(main: [s[16], op_bits[8], op_helpers[6]]): + enf s[i]' = s[i] for i in 4..16 + enf b0_b1_is_zero([op_bits]) + +ev push(main: [s[16]]): + enf s[i + 1]' = s[i] for i in 0..15 + +ev syscall(): + + +ev call(): + + +ev end(): + + +ev repeat(): + + +ev respan(): + + +ev halt(): -ev u32madd(main: [s[16], 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 \ No newline at end of file From e128a546d4ed4e15a1031d4182d9a29295609dc3 Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Fri, 7 Apr 2023 19:52:46 +0300 Subject: [PATCH 07/12] refactor: get rid of flag functions --- constraints/miden-vm/stack.air | 490 +++++++-------------------------- 1 file changed, 101 insertions(+), 389 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index efb9db937..0ecdde421 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -75,295 +75,12 @@ fn f_x1111(op_bits: vector[8]) -> scalar: return op_bits[3] & op_bits[2] & op_bits[1] & op_bits[0] -# No stack shift operations - -fn f_noop(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0000(op_bits) - -fn f_eqz(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0001(op_bits) - -fn f_neg(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0010(op_bits) - -fn f_inv(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0011(op_bits) - -fn f_incr(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0100(op_bits) - -fn f_not(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0101(op_bits) - -fn f_fmpadd(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0110(op_bits) - -fn f_mload(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x0111(op_bits) - -fn f_swap(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1000(op_bits) - -fn f_caller(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1001(op_bits) - -fn f_movup2(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1010(op_bits) - -fn f_movdn2(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1011(op_bits) - -fn f_movup3(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1100(op_bits) - -fn f_movdn3(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1101(op_bits) - -fn f_advpopw(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1110(op_bits) - -fn f_expacc(op_bits: vector[8]) -> scalar: - return f_000(op_bits) & f_x1111(op_bits) - - -fn f_movup4(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0000(op_bits) - -fn f_movdn4(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0001(op_bits) - -fn f_movup5(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0010(op_bits) - -fn f_movdn5(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0011(op_bits) - -fn f_movup6(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0100(op_bits) - -fn f_movdn6(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0101(op_bits) - -fn f_movup7(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0110(op_bits) - -fn f_movdn7(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x0111(op_bits) - -fn f_swapw(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1000(op_bits) - -fn f_ext2mul(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1001(op_bits) - -fn f_movup8(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1010(op_bits) - -fn f_movdn8(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1011(op_bits) - -fn f_swapw2(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1100(op_bits) - -fn f_swapw3(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1101(op_bits) - -fn f_swapdw(op_bits: vector[8]) -> scalar: - return f_001(op_bits) & f_x1110(op_bits) - -fn f_001_1111() -> scalar: - return 0 - - -# Left stack shift operations - -fn f_assert(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0000(op_bits) - -fn f_eq(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0001(op_bits) - -fn f_add(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0010(op_bits) - -fn f_mul(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0011(op_bits) - -fn f_and(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0100(op_bits) - -fn f_or(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0101(op_bits) - -fn f_u32and(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0110(op_bits) - -fn f_u32xor(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x0111(op_bits) - -fn f_frie2f4(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1000(op_bits) - -fn f_drop(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1001(op_bits) - -fn f_cswap(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1010(op_bits) - -fn f_cswapw(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1011(op_bits) - -fn f_mloadw(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1100(op_bits) - -fn f_mstore(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1101(op_bits) - -fn f_mstorew(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1110(op_bits) - -fn f_fmpupdate(op_bits: vector[8]) -> scalar: - return f_010(op_bits) & f_x1111(op_bits) - - -# Right stack shift operations - -fn f_pad(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0000(op_bits) - -fn f_dup(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0001(op_bits) - -fn f_dup1(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0010(op_bits) - -fn f_dup2(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0011(op_bits) - -fn f_dup3(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0100(op_bits) - -fn f_dup4(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0101(op_bits) - -fn f_dup5(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0110(op_bits) - -fn f_dup6(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x0111(op_bits) - -fn f_dup7(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1000(op_bits) - -fn f_dup9(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1001(op_bits) - -fn f_dup11(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1010(op_bits) - -fn f_dup13(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1011(op_bits) - -fn f_dup15(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1100(op_bits) - -fn f_advpop(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1101(op_bits) - -fn f_sdepth(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1110(op_bits) - -fn f_clk(op_bits: vector[8]) -> scalar: - return f_011(op_bits) & f_x1111(op_bits) - - -# u32 operations - -fn f_u32add(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1] - -fn f_u32sub(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1] - -fn f_u32mul(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1] - -fn f_u32div(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1] - -fn f_u32split(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1] - -fn f_u32assert2(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1] - -fn f_u32add3(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1] - -fn f_madd(op_bits: vector[8]) -> scalar: - return f_u32rc(op_bits) & op_bits[3] & op_bits[2] & op_bits[1] - - -# High-degree operations - -fn f_hperm(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1] - -fn f_mpverify(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1] - -fn f_pipe(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1] - -fn f_mstream(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1] - -fn f_span(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1] - -fn f_join(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1] - -fn f_split(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1] - -fn f_loop(op_bits: vector[8]) -> scalar: - return f_101(op_bits) & op_bits[3] & op_bits[2] & op_bits[1] - - -# Very high-degree operations - -fn f_mrupdate(op_bits: vector[8]) -> scalar: - return op_bits[7] & !op_bits[4] & !op_bits[3] & !op_bits[2] - -fn f_push(op_bits: vector[8]) -> scalar: - return op_bits[7] & !op_bits[4] & !op_bits[3] & op_bits[2] - -fn f_syscall(op_bits: vector[8]) -> scalar: - return op_bits[7] & !op_bits[4] & op_bits[3] & !op_bits[2] - -fn f_call(op_bits: vector[8]) -> scalar: - return op_bits[7] & !op_bits[4] & op_bits[3] & op_bits[2] - -fn f_end(op_bits: vector[8]) -> scalar: - return op_bits[7] & op_bits[4] & !op_bits[3] & !op_bits[2] - -fn f_repeat(op_bits: vector[8]) -> scalar: - return op_bits[7] & op_bits[4] & !op_bits[3] & op_bits[2] - -fn f_respan(op_bits: vector[8]) -> scalar: - return op_bits[7] & op_bits[4] & op_bits[3] & !op_bits[2] - -fn f_halt(op_bits: vector[8]) -> scalar: - return op_bits[7] & op_bits[4] & op_bits[3] & op_bits[2] - - # Composite flags fn f_shr(op_bits: vector[8]) -> scalar: return !op_bits[6] & op_bits[5] & op_bits[4] + f_u32split(op_bits) + f_push(op_bits) -# hasher[5] = op_helpers[3], where hahser -- main columns from the decoder, helper -- aux columns from the stack +# hasher[5] = op_helpers[3], where hahser[] are decoder columns, which are the same as helper[] -- columns from the stack fn f_shl(op_bits: vector[8], op_helpers: vector[6]) -> scalar: let f_add3_mad = op_bits[6] & !op_bits[5] & !op_bits[4] & op_bits[3] & op_bits[2] let f_split_loop = op_bits[6] & !op_bits[5] & op_bits[4] & op_bits[3] & op_bits[2] @@ -381,115 +98,110 @@ fn f_ctrl(op_bits: vector[8]) -> scalar: fn compute_op_flags(op_bits: vector[8]) -> vector[88]: return [ - f_noop(op_bits), - f_eqz(op_bits), - f_neg(op_bits), - f_inv(op_bits), - f_incr(op_bits), - f_not(op_bits), - f_fmpadd(op_bits), - f_mload(op_bits), - f_swap(op_bits), - f_caller(op_bits), - f_movup2(op_bits), - f_movdn2(op_bits), - f_movup3(op_bits), - f_movdn3(op_bits), - f_advpopw(op_bits), - f_expacc(op_bits), - f_movup4(op_bits), - f_movdn4(op_bits), - f_movup5(op_bits), - f_movdn5(op_bits), - f_movup6(op_bits), - f_movdn6(op_bits), - f_movup7(op_bits), - f_movdn7(op_bits), - f_swapw(op_bits), - f_ext2mul(op_bits), - f_movup8(op_bits), - f_movdn8(op_bits), - f_swapw2(op_bits), - f_swapw3(op_bits), - f_swapdw(op_bits), - f_001_1111(op_bits), - - f_assert(op_bits), - f_eq(op_bits), - f_add(op_bits), - f_mul(op_bits), - f_and(op_bits), - f_or(op_bits), - f_u32and(op_bits), - f_u32xor(op_bits), - f_frie2f4(op_bits), - f_drop(op_bits), - f_cswap(op_bits), - f_cswapw(op_bits), - f_mloadw(op_bits), - f_mstore(op_bits), - f_mstorew(op_bits), - f_fmpupdate(op_bits), - - f_pad(op_bits), - f_dup(op_bits), - f_dup1(op_bits), - f_dup2(op_bits), - f_dup3(op_bits), - f_dup4(op_bits), - f_dup5(op_bits), - f_dup6(op_bits), - f_dup7(op_bits), - f_dup9(op_bits), - f_dup11(op_bits), - f_dup13(op_bits), - f_dup15(op_bits), - f_advpop(op_bits), - f_sdepth(op_bits), - f_clk(op_bits), - - f_u32add(op_bits), - f_u32sub(op_bits), - f_u32mul(op_bits), - f_u32div(op_bits), - f_u32split(op_bits), - f_u32assert2(op_bits), - f_u32add3(op_bits), - f_madd(op_bits), - - f_hperm(op_bits), - f_mpverify(op_bits), - f_pipe(op_bits), - f_mstream(op_bits), - f_span(op_bits), - f_join(op_bits), - f_split(op_bits), - f_loop(op_bits), - - f_mrupdate(op_bits), - f_push(op_bits), - f_syscall(op_bits), - f_call(op_bits), - f_end(op_bits), - f_repeat(op_bits), - f_respan(op_bits), - f_halt(op_bits) + # No stack shift operations + f_000(op_bits) & f_x0000(op_bits), # noop + f_000(op_bits) & f_x0001(op_bits), # eqz + f_000(op_bits) & f_x0010(op_bits), # neg + f_000(op_bits) & f_x0011(op_bits), # inv + f_000(op_bits) & f_x0100(op_bits), # incr + f_000(op_bits) & f_x0101(op_bits), # not + f_000(op_bits) & f_x0110(op_bits), # fmpadd + f_000(op_bits) & f_x0111(op_bits), # mload + f_000(op_bits) & f_x1000(op_bits), # swap + f_000(op_bits) & f_x1001(op_bits), # caller + f_000(op_bits) & f_x1010(op_bits), # movup2 + f_000(op_bits) & f_x1011(op_bits), # movdn2 + f_000(op_bits) & f_x1100(op_bits), # movup3 + f_000(op_bits) & f_x1101(op_bits), # movdn3 + f_000(op_bits) & f_x1110(op_bits), # advpop + f_000(op_bits) & f_x1111(op_bits), # expacc + f_001(op_bits) & f_x0000(op_bits), # movup4 + f_001(op_bits) & f_x0001(op_bits), # movdn4 + f_001(op_bits) & f_x0010(op_bits), # movup5 + f_001(op_bits) & f_x0011(op_bits), # movdn5 + f_001(op_bits) & f_x0100(op_bits), # movup6 + f_001(op_bits) & f_x0101(op_bits), # movdn6 + f_001(op_bits) & f_x0110(op_bits), # movup7 + f_001(op_bits) & f_x0111(op_bits), # movdn7 + f_001(op_bits) & f_x1000(op_bits), # swapw + f_001(op_bits) & f_x1001(op_bits), # ext2mul + f_001(op_bits) & f_x1010(op_bits), # movup8 + f_001(op_bits) & f_x1011(op_bits), # movdn8 + f_001(op_bits) & f_x1100(op_bits), # swapw2 + f_001(op_bits) & f_x1101(op_bits), # swapw3 + f_001(op_bits) & f_x1110(op_bits), # swapdw + f_001_1111(op_bits), # + + # Left stack shift operations + f_010(op_bits) & f_x0000(op_bits), # assert + f_010(op_bits) & f_x0001(op_bits), # eq + f_010(op_bits) & f_x0010(op_bits), # add + f_010(op_bits) & f_x0011(op_bits), # mul + f_010(op_bits) & f_x0100(op_bits), # and + f_010(op_bits) & f_x0101(op_bits), # or + f_010(op_bits) & f_x0110(op_bits), # u32and + f_010(op_bits) & f_x0111(op_bits), # u32xor + f_010(op_bits) & f_x1000(op_bits), # frie2f4 + f_010(op_bits) & f_x1001(op_bits), # drop + f_010(op_bits) & f_x1010(op_bits), # cswap + f_010(op_bits) & f_x1011(op_bits), # cswapw + f_010(op_bits) & f_x1100(op_bits), # mloadw + f_010(op_bits) & f_x1101(op_bits), # mstore + f_010(op_bits) & f_x1110(op_bits), # mstorew + f_010(op_bits) & f_x1111(op_bits), # fmupdate + + # Right stack shift operations + f_011(op_bits) & f_x0000(op_bits), # pad + f_011(op_bits) & f_x0001(op_bits), # dup + f_011(op_bits) & f_x0010(op_bits), # dup1 + f_011(op_bits) & f_x0011(op_bits), # dup2 + f_011(op_bits) & f_x0100(op_bits), # dup3 + f_011(op_bits) & f_x0101(op_bits), # dup4 + f_011(op_bits) & f_x0110(op_bits), # dup5 + f_011(op_bits) & f_x0111(op_bits), # dup6 + f_011(op_bits) & f_x1000(op_bits), # dup7 + f_011(op_bits) & f_x1001(op_bits), # dup9 + f_011(op_bits) & f_x1010(op_bits), # dup11 + f_011(op_bits) & f_x1011(op_bits), # dup13 + f_011(op_bits) & f_x1100(op_bits), # dup15 + f_011(op_bits) & f_x1101(op_bits), # advpop + f_011(op_bits) & f_x1110(op_bits), # sdepth + f_011(op_bits) & f_x1111(op_bits), # clk + + # u32 operations + f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1], # u32add + f_u32rc(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1], # u32sub + f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1], # u32mul + f_u32rc(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1], # u32div + f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1], # u32split + f_u32rc(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1], # u32assert2 + f_u32rc(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1], # u32add3 + f_u32rc(op_bits) & op_bits[3] & op_bits[2] & op_bits[1], # u32madd + + # High-degree operations + f_101(op_bits) & !op_bits[3] & !op_bits[2] & !op_bits[1], # hperm + f_101(op_bits) & !op_bits[3] & !op_bits[2] & op_bits[1], # mpverify + f_101(op_bits) & !op_bits[3] & op_bits[2] & !op_bits[1], # pipe + f_101(op_bits) & !op_bits[3] & op_bits[2] & op_bits[1], # mstream + f_101(op_bits) & op_bits[3] & !op_bits[2] & !op_bits[1], # span + f_101(op_bits) & op_bits[3] & !op_bits[2] & op_bits[1], # join + f_101(op_bits) & op_bits[3] & op_bits[2] & !op_bits[1], # split + f_101(op_bits) & op_bits[3] & op_bits[2] & op_bits[1], # loop + + # Very high-degree operations + op_bits[7] & !op_bits[4] & !op_bits[3] & !op_bits[2], # mrupdate + op_bits[7] & !op_bits[4] & !op_bits[3] & op_bits[2], # push + op_bits[7] & !op_bits[4] & op_bits[3] & !op_bits[2], # syscall + op_bits[7] & !op_bits[4] & op_bits[3] & op_bits[2], # call + op_bits[7] & op_bits[4] & !op_bits[3] & !op_bits[2], # end + op_bits[7] & op_bits[4] & !op_bits[3] & op_bits[2], # repeat + op_bits[7] & op_bits[4] & op_bits[3] & !op_bits[2], # respan + op_bits[7] & op_bits[4] & op_bits[3] & op_bits[2], # halt ] ### Helper evaluators ############################################################################# -# Enforces that the provided columns must be zero. -ev is_zero(main: [values[4]]): - enf v = 0 for v in values - - -# Enforces that values in the columns in the current row must be equal to the values in the next -# row. -ev is_unchanged(main: [values[4]]): - enf v' = v for v in values - - # Enforces that the provided columns must be binary. ev is_binary(main: [a]): enf a^2 = a @@ -562,7 +274,7 @@ ev stack_constraints(main: [stack_top[16], stack_helpers[3], op_bits[8], op_help or([stack_top]) when op_flags[37] u32and([stack_top]) when op_flags[38] u32xor([stack_top]) when op_flags[39] - # TODO: add match variant for caller + # TODO: add match variant for frie2f4 frie2f4() drop([stack_top]) when op_flags[41] cswap([stack_top]) when op_flags[42] From 445393efc0f4121464367401555fffc4d6d13d34 Mon Sep 17 00:00:00 2001 From: Andrey Khmuro Date: Tue, 6 Jun 2023 16:21:02 +0300 Subject: [PATCH 08/12] refactor: remove segment names --- constraints/miden-vm/stack.air | 177 +++++++++++++++++---------------- 1 file changed, 93 insertions(+), 84 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 0ecdde421..35fbedec3 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -203,22 +203,22 @@ fn compute_op_flags(op_bits: vector[8]) -> vector[88]: ### Helper evaluators ############################################################################# # Enforces that the provided columns must be binary. -ev is_binary(main: [a]): +ev is_binary([a]): enf a^2 = a -ev check_element_validity(main: [op_helpers[6]]): +ev check_element_validity([op_helpers[6]]): let m = op_helpers[4] let v_hi = 2^16 * op_helpers[3] + op_helpers[2] let v_lo = 2^16 * op_helpers[1] + op_helpers[0] enf (1 - m * (2^32 - 1 - v_hi)) * v_lo = 0 -ev b0_is_zero(main: [op_bits[8]]): +ev b0_is_zero([op_bits[8]]): enf op_bits[6] & !op_bits[5] & op_bits[0] = 0 -ev b0_b1_is_zero(main: [op_bits[8]]): +ev b0_b1_is_zero([op_bits[8]]): enf op_bits[6] & op_bits[5] & op_bits[0] = 0 enf op_bits[6] & op_bits[5] & op_bits[1] = 0 @@ -229,7 +229,7 @@ ev b0_b1_is_zero(main: [op_bits[8]]): # TODO: add docs for columns # stack_helpers consists of [bookkeeping[0], bookkeeping[1], h0] # op_bits consists of [op_bits[7], extra] -ev stack_constraints(main: [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp]): +ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp]): let op_flags = compute_op_flags(op_bits) match enf: @@ -313,72 +313,72 @@ ev stack_constraints(main: [stack_top[16], stack_helpers[3], op_bits[8], op_help # No stack shift operations -ev noop(main: [s[16]]): +ev noop([s[16]]): enf s[i]' = s[i] for i in 0..16 -ev eqz(main: [s[16], h0]): +ev eqz([s[16], h0]): enf s[0]' * s[0] = 0 enf s[0]' = 1 - s[0] * h0 enf s[i]' = s[i] for i in 1..16 -ev neg(main: [s[16]]): +ev neg([s[16]]): enf s[0]' + s[0] = 0 enf s[i]' = s[i] for i in 1..16 -ev inv(main: [s[16]]): +ev inv([s[16]]): enf s[0]' * s[0] = 1 enf s[i]' = s[i] for i in 1..16 -ev incr(main: [s[16]]): +ev incr([s[16]]): enf s[0]' = s[0] + 1 enf s[i]' = s[i] for i in 1..16 -ev not(main: [s[16]]): +ev not([s[16]]): enf is_binary([s[0]]) enf s[0]' = !s[0] enf s[i]' = s[i] for i in 1..16 -ev fmpadd(main: [s[16], fmp]): +ev fmpadd([s[16], fmp]): enf s[0]' = s[0] + fmp enf s[i]' = s[i] for i in 1..16 # Bus constraint is implemented in a separate file -ev mload(main: [s[16], clk]): +ev mload([s[16], clk]): enf s[i]' = s[i] for i in 1..16 -ev swap(main: [s[16]]): +ev swap([s[16]]): enf s[0]' = s[1] enf s[1]' = s[0] enf s[i]' = s[i] for i in 2..16 # TODO: add constraints -ev caller(main: [s[16]]): +ev caller([s[16]]): -ev movup2(main: [s[16]]): +ev movup2([s[16]]): enf s[0]' = s[2] enf s[i + 1]' = s[i] for i in 0..2 enf s[i]' = s[i] for i in 3..16 -ev movdn2(main: [s[16]]): +ev movdn2([s[16]]): enf s[2]' = s[0] enf s[i]' = s[i + 1] for i in 0..2 enf s[i]' = s[i] for i in 3..16 -ev movup3(main: [s[16]]): +ev movup3([s[16]]): enf s[0]' = s[3] enf s[i + 1]' = s[i] for i in 0..3 enf s[i]' = s[i] for i in 4..16 -ev movdn3(main: [s[16]]): +ev movdn3([s[16]]): enf s[3]' = s[0] enf s[i]' = s[i + 1] for i in 0..3 enf s[i]' = s[i] for i in 4..16 -ev advpopw(main: [s[16]]): +ev advpopw([s[16]]): enf s[i]' = s[i] for i in 4..16 -ev expacc(main: [s[16], h0]): +ev expacc([s[16], h0]): enf is_binary([s[0]']) enf s[1]' = s[1]^2 enf h0 = (s[1] - 1) * s[0]' + 1 @@ -386,242 +386,242 @@ ev expacc(main: [s[16], h0]): enf s[3]' = s[3] * 2 + s[0]' enf s[i]' = s[i] for i in 4..16 -ev movup4(main: [s[16]]): +ev movup4([s[16]]): enf s[0]' = s[4] enf s[i + 1]' = s[i] for i in 0..4 enf s[i]' = s[i] for i in 5..16 -ev movdn4(main: [s[16]]): +ev movdn4([s[16]]): enf s[4]' = s[0] = 0 enf s[i]' = s[i + 1] for i in 0..4 enf s[i]' = s[i] for i in 5..16 -ev movup5(main: [s[16]]): +ev movup5([s[16]]): enf s[0]' = s[5] enf s[i + 1]' = s[i] for i in 0..5 enf s[i]' = s[i] for i in 6..16 -ev movdn5(main: [s[16]]): +ev movdn5([s[16]]): enf s[5]' = s[0] enf s[i]' = s[i + 1] for i in 0..5 enf s[i]' = s[i] for i in 6..16 -ev movup6(main: [s[16]]): +ev movup6([s[16]]): enf s[0]' = s[6] enf s[i + 1]' = s[i] for i in 0..6 enf s[i]' = s[i] for i in 7..16 -ev movdn6(main: [s[16]]): +ev movdn6([s[16]]): enf s[6]' = s[0] enf s[i]' = s[i + 1] for i in 0..6 enf s[i]' = s[i] for i in 7..16 -ev movup7(main: [s[16]]): +ev movup7([s[16]]): enf s[0]' = s[7] = 0 enf s[i + 1]' = s[i] for i in 0..7 enf s[i]' = s[i] for i in 8..16 -ev movdn7(main: [s[16]]): +ev movdn7([s[16]]): enf s[7]' = s[0] enf s[i]' = s[i + 1] for i in 0..7 enf s[i]' = s[i] for i in 8..16 -ev swapw(main: [s[16]]): +ev swapw([s[16]]): enf s[i]' = s[i + 4] for i in 0..4 enf s[i + 4]' = s[i] for i in 0..4 enf s[i]' = s[i] for i in 8..16 -ev ext2mul(main: [s[16]]): +ev ext2mul([s[16]]): enf s[0]' = s[0] enf s[1]' = s[1] enf s[2]' = (s[0] + s[1]) * (s[2] + s[3]) - s[0] * s[2] enf s[3]' = s[1] * s[3] - 2 * s[0] * s[2] enf s[i]' = s[i] for i in 4..16 -ev movup8(main: [s[16]]): +ev movup8([s[16]]): enf s[0]' = s[8] enf s[i + 1]' = s[i] for i in 0..8 enf s[i]' = s[i] for i in 9..16 -ev movdn8(main: [s[16]]): +ev movdn8([s[16]]): enf s[8]' = s[0] enf s[i]' = s[i + 1] for i in 0..8 enf s[i]' = s[i] for i in 9..16 -ev swapw2(main: [s[16]]): +ev swapw2([s[16]]): enf s[i]' = s[i + 8] for i in 0..4 enf s[i + 8]' = s[i] for i in 0..4 enf s[i]' = s[i] for i in 4..8 enf s[i]' = s[i] for i in 12..16 # Should we enforce that elements in position grater than 15 do not change? -ev swapw3(main: [s[16]]): +ev swapw3([s[16]]): enf s[i]' = s[i + 12] for i in 0..4 enf s[i + 12]' = s[i] for i in 0..4 enf s[i]' = s[i] for i in 4..12 # Should we enforce that elements in position grater than 15 do not change? -ev swapdw(main: [s[16]]): +ev swapdw([s[16]]): enf s[i]' = s[i + 8] for i in 0..8 enf s[i + 8]' = s[i] for i in 0..8 # Left stack shift operationds -ev assert(main: [s[16]]): +ev assert([s[16]]): enf s[0] = 1 enf s[i]' = s[i + 1] for i in 0..15 -ev eq(main: [s[16], h0]): +ev eq([s[16], h0]): enf s[0]' * (s[0] - s[1]) = 0 enf s[0]' = 1 - (s[0] - s[1]) * h0 enf s[i]' = s[i + 1] for i in 1..15 -ev add(main: [s[16]]): +ev add([s[16]]): enf s[0]' = s[0] + s[1] enf s[i]' = s[i + 1] for i in 1..15 -ev mul(main: [s[16]]): +ev mul([s[16]]): enf s[0]' = s[0] * s[1] enf s[i]' = s[i + 1] for i in 1..15 -ev and(main: [s[16]]): +ev and([s[16]]): enf is_binary([s[i]]) = 0 for i in 0..2 enf s[0]' = s[0] * s[1] enf s[i]' = s[i + 1] for i in 1..15 -ev or(main: [s[16]]): +ev or([s[16]]): enf is_binary([s[i]]) = 0 for i in 0..2 enf s[0]' = s[1] + s[0] - s[1] * s[0] enf s[i]' = s[i + 1] for i in 1..15 # Bus constraint is implemented in a separate file -ev u32and(main: [s[16]]): +ev u32and([s[16]]): enf s[i]' = s[i + 1] for i in 1..15 # Bus constraint is implemented in a separate file -ev u32xor(main: [s[16]]): +ev u32xor([s[16]]): enf s[i]' = s[i + 1] for i in 1..15 # TODO: add constraints -ev frie2f4(main: [s[16]]): +ev frie2f4([s[16]]): -ev drop(main: [s[16]]): +ev drop([s[16]]): enf s[i]' = s[i + 1] for i in 0..15 -ev cswap(main: [s[16]]): +ev cswap([s[16]]): enf is_binary([s[0]]) = 0 enf s[0]' = s[0] * s[2] + (1 - s[0]) * s[1] enf s[1]' = s[0] * s[1] + (1 - s[0]) * s[2] enf s[i]' = s[i + 1] for i in 2..15 -ev cswapw(main: [s[16]]): +ev cswapw([s[16]]): enf is_binary([s[0]]) = 0 enf s[i]' = s[0] * s[i + 5] + (1 - s[0]) * s[i + 1] for i in 0..4 enf s[i + 4]' = s[0] * s[i + 1] + (1 - s[0]) * s[i + 5] for i in 0..4 enf s[i]' = s[i + 1] for i in 8..15 # Bus constraint is implemented in a separate file -ev mloadw(main: [s[16], clk]): +ev mloadw([s[16], clk]): enf s[i]' = s[i + 1] for i in 4..15 # Bus constraint is implemented in a separate file -ev mstore(main: [s[16], clk]): +ev mstore([s[16], clk]): enf s[i]' = s[i + 1] for i in 0..15 # Bus constraint is implemented in a separate file -ev mstorew(main: [s[16], clk]): +ev mstorew([s[16], clk]): enf s[i]' = s[i + 1] for i in 0..15 -ev fmpupdate(main: [s[16], fmp]): +ev fmpupdate([s[16], fmp]): enf fmp' = fmp + s[0] enf s[i]' = s[i + 1] for i in 0..15 # Right stack shift operations -ev pad(main: [s[16]]): +ev pad([s[16]]): enf s[0]' = 0 enf s[i + 1]' = s[i] for i in 0..15 -ev dup(main: [s[16]]): +ev dup([s[16]]): enf s[0]' = s[0] enf s[i + 1]' = s[i] for i in 0..15 -ev dup1(main: [s[16]]): +ev dup1([s[16]]): enf s[0]' = s[1] enf s[i + 1]' = s[i] for i in 0..15 -ev dup2(main: [s[16]]): +ev dup2([s[16]]): enf s[0]' = s[2] enf s[i + 1]' = s[i] for i in 0..15 -ev dup3(main: [s[16]]): +ev dup3([s[16]]): enf s[0]' = s[3] enf s[i + 1]' = s[i] for i in 0..15 -ev dup4(main: [s[16]]): +ev dup4([s[16]]): enf s[0]' = s[4] enf s[i + 1]' = s[i] for i in 0..15 -ev dup5(main: [s[16]]): +ev dup5([s[16]]): enf s[0]' = s[5] enf s[i + 1]' = s[i] for i in 0..15 -ev dup6(main: [s[16]]): +ev dup6([s[16]]): enf s[0]' = s[6] enf s[i + 1]' = s[i] for i in 0..15 -ev dup7(main: [s[16]]): +ev dup7([s[16]]): enf s[0]' = s[7] enf s[i + 1]' = s[i] for i in 0..15 -ev dup9(main: [s[16]]): +ev dup9([s[16]]): enf s[0]' = s[9] enf s[i + 1]' = s[i] for i in 0..15 -ev dup11(main: [s[16]]): +ev dup11([s[16]]): enf s[0]' = s[11] enf s[i + 1]' = s[i] for i in 0..15 -ev dup13(main: [s[16]]): +ev dup13([s[16]]): enf s[0]' = s[13] enf s[i + 1]' = s[i] for i in 0..15 -ev dup15(main: [s[16]]): +ev dup15([s[16]]): enf s[0]' = s[15] enf s[i + 1]' = s[i] for i in 0..15 -ev advpop(main: [s[16]]): +ev advpop([s[16]]): enf s[i + 1]' = s[i] for i in 0..15 -ev sdepth(main: [s[16], bookkeeping]): +ev sdepth([s[16], bookkeeping]): enf s[0]' = bookkeeping enf s[i + 1]' = s[i] for i in 0..15 -ev clk(main: [s[16], clk]): +ev clk([s[16], clk]): enf s[0]' = clk enf s[i + 1]' = s[i] for i in 0..15 # u32 operations -ev u32add(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32add([s[16], op_bits[8], op_helpers[6]]): enf s[0] + s[1] = 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] enf s[0]' = op_helpers[2] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i] for i in 2..16 enf b0_is_zero([op_bits]) -ev u32sub(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32sub([s[16], op_bits[8], op_helpers[6]]): enf s[1] = s[0] + s[1]' + 2^32 * s[0]' enf (s[0]')^2 - s[0]' = 0 enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i] for i in 2..16 enf b0_is_zero([op_bits]) -ev u32mul(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32mul([s[16], op_bits[8], op_helpers[6]]): enf s[0] * s[1] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] @@ -629,14 +629,14 @@ ev u32mul(main: [s[16], op_bits[8], op_helpers[6]]): enf s[i]' = s[i] for i in 2..16 enf b0_is_zero([op_bits]) -ev u32div(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32div([s[16], op_bits[8], op_helpers[6]]): enf s[1] = s[0] * s[1]' + s[0]' enf s[1] - s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[0] - s[0]' - 1 = 2^16 * op_helpers[2] + op_helpers[3] enf s[i]' = s[i] for i in 2..16 enf b0_is_zero([op_bits]) -ev u32split(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32split([s[16], op_bits[8], op_helpers[6]]): enf s[0] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] @@ -644,20 +644,20 @@ ev u32split(main: [s[16], op_bits[8], op_helpers[6]]): enf s[i + 1]' = s[i] for i in 1..15 enf b0_is_zero([op_bits]) -ev u32assert2(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32assert2([s[16], op_bits[8], op_helpers[6]]): enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i] for i in 0..16 enf b0_is_zero([op_bits]) -ev u32add3(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32add3([s[16], op_bits[8], op_helpers[6]]): enf s[0] + s[1] + s[2] = 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] enf s[0]' = op_helpers[2] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[i]' = s[i + 1] for i in 2..15 enf b0_is_zero([op_bits]) -ev u32madd(main: [s[16], op_bits[8], op_helpers[6]]): +ev u32madd([s[16], op_bits[8], op_helpers[6]]): enf s[0] * s[1] + s[2] = 2^48 * op_helpers[3] + 2^32 * op_helpers[2] + 2^16 * op_helpers[1] + op_helpers[0] enf s[1]' = 2^16 * op_helpers[1] + op_helpers[0] enf s[0]' = 2^16 * op_helpers[3] + op_helpers[2] @@ -669,59 +669,68 @@ ev u32madd(main: [s[16], op_bits[8], op_helpers[6]]): # High-degree operations # Bus constraint is implemented in a separate file -ev hperm(main: [s[16], op_bits[8], op_helpers[6]]): +ev hperm([s[16], op_bits[8], op_helpers[6]]): enf s[i]' = s[i] for i in 12..16 enf b0_is_zero([op_bits]) # Bus constraint is implemented in a separate file -ev mpverify(main: [s[16], op_bits[8], op_helpers[6]]): +ev mpverify([s[16], op_bits[8], op_helpers[6]]): enf s[i]' = s[i] for i in 0..16 enf b0_is_zero([op_bits]) # TODO: add constraints -ev pipe(main: [s[16], op_bits[8], op_helpers[6]]): +ev pipe([s[16], op_bits[8], op_helpers[6]]): # TODO: add constraints -ev mstream(main: [s[16], op_bits[8], op_helpers[6]]): +ev mstream([s[16], op_bits[8], op_helpers[6]]): - -ev span(main: [s[16], op_bits[8], op_helpers[6]]) +# TODO: add constraints +ev span([s[16], op_bits[8], op_helpers[6]]) +# TODO: add constraints ev join() +# TODO: add constraints ev split() +# TODO: add constraints ev loop() # Very high-degree operations # Bus constraint is implemented in a separate file -ev mrupdate(main: [s[16], op_bits[8], op_helpers[6]]): +ev mrupdate([s[16], op_bits[8], op_helpers[6]]): enf s[i]' = s[i] for i in 4..16 enf b0_b1_is_zero([op_bits]) -ev push(main: [s[16]]): +ev push([s[16]]): enf s[i + 1]' = s[i] for i in 0..15 +# TODO: add constraints ev syscall(): +# TODO: add constraints ev call(): +# TODO: add constraints ev end(): +# TODO: add constraints ev repeat(): +# TODO: add constraints ev respan(): +# TODO: add constraints ev halt(): From d13b87586fa5fed6d4fefa19727ae1eb64b9308e Mon Sep 17 00:00:00 2001 From: hmuro andrej Date: Wed, 12 Apr 2023 16:12:37 +0300 Subject: [PATCH 09/12] feat: wtire stack overflow table constraints --- constraints/miden-vm/stack.air | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 35fbedec3..b3eecfb1f 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -311,6 +311,38 @@ ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6] u32madd([stack_top, op_helpers]) when op_flags[71] +ev overflow_table_constraints( + main: [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], + aux: [p1] +): + # Flag to indicate whether the overflow table contains values (overflow flag). + let f_ov = (stack_helpers[0] - 16) * stack_helpers[2] + + # Enforce that overflow flag is set correctly. + enf (1 - f_ov) * (stack_helpers[0] - 16) = 0 + + # Enforce that stack depth column stack_helpers[0] (bookkeeping[0]) is updated correctly. + enf stack_helpers[0]' - stack_helpers[0] + f_shl(op_bits, op_helpers) * f_ov - f_shr(op_bits) = 0 + + # Value of the row to be added to the table + let v = $alpha[0] + $alpha[1] * clk + $alpha[2] * stack_top[15] + $alpha[3] * stack_helpers[1] + + # Value of the row to be removed from the table + let u = $alpha[0] + $alpha[1] * stack_helpers[1] + $alpha[2] * stack_top[15]' + alpha[3] * stack_helpers[1]' + + # Enforce that right and left shifts update the overflow table correctly. + enf p1' * (u * f_shl(op_bits, op_helpers) * f_ov + 1 - f_shl(op_bits, op_helpers) * f_ov) = + p1 * (v * f_shr(op_bits) + 1 - f_shr) + + # Enforce that the next value of stack_helpers[1] (bookkeeping[1]) is set to the current value of clk. + enf f_shr(op_bits) * (stack_helpers[1]' - clk) = 0 + + # Enforce that when the overflow table is empty, 0 is "shifted in" from the right (i.e. stack_top[15] is set to 0). + enf f_shl(op_bits, op_helpers) * (1 - f_ov) * stack_top[15]' = 0 + + # TODO: enforce boundary constraints + + # No stack shift operations ev noop([s[16]]): From 26aba73b0d0e6cbc63e401776db0f9db47837ff5 Mon Sep 17 00:00:00 2001 From: Andrey Khmuro Date: Tue, 6 Jun 2023 17:25:10 +0300 Subject: [PATCH 10/12] feat: add overflow constraints usage --- constraints/miden-vm/stack.air | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index b3eecfb1f..684dfe757 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -229,7 +229,9 @@ ev b0_b1_is_zero([op_bits[8]]): # TODO: add docs for columns # stack_helpers consists of [bookkeeping[0], bookkeeping[1], h0] # op_bits consists of [op_bits[7], extra] -ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp]): +ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], [p1]): + enf overflow_table_constraints([stack_top, stack_helpers, op_bits, op_helpers, clk, fmp], [p1]) + let op_flags = compute_op_flags(op_bits) match enf: @@ -312,8 +314,8 @@ ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6] ev overflow_table_constraints( - main: [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], - aux: [p1] + [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], + [p1] ): # Flag to indicate whether the overflow table contains values (overflow flag). let f_ov = (stack_helpers[0] - 16) * stack_helpers[2] From 115fe4c94fd955f53451e385bbc30a185f8209e5 Mon Sep 17 00:00:00 2001 From: Andrey Khmuro Date: Tue, 25 Apr 2023 22:24:21 +0300 Subject: [PATCH 11/12] feat: write bitwise, memory, hash multiset constraints --- constraints/miden-vm/stack.air | 294 +++++++++++++++++++++++---------- 1 file changed, 207 insertions(+), 87 deletions(-) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 684dfe757..8689388bb 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -1,5 +1,20 @@ mod StacktAir +### Constants and periodic columns ################################################################ + +const BITWISE_AND = 2 +const BITWISE_XOR = 6 + +const MEMORY_READ = 12 +const MEMORY_WRITE = 4 + +const HASHER_LINEAR_HASH = 3 +const HASHER_MP_VERIFY = 11 +const HASHER_MR_UPDATE_OLD = 7 +const HASHER_MR_UPDATE_NEW = 15 +const HASHER_RETURN_HASH = 1 +const HASHER_RETURN_STATE = 9 + ### Helper functions ############################################################################## # Flags for the first bits (op_bits[6], op_bits[5], op_bits[4]) @@ -223,6 +238,109 @@ ev b0_b1_is_zero([op_bits[8]]): enf op_bits[6] & op_bits[5] & op_bits[1] = 0 +ev u32and_bus_constraint([stack_top[16]], [b_chip]): + # and_req_val represents bitwise operation request value. + let and_req_val = $alpha[0] + + $alpha[1] * BITWISE_AND + + $alpha[2] * stack_top[0] + + $alpha[3] * stack_top[1] + + $alpha[4] * stack_top[0]' + + # Enforce u32and bus constraint. + enf b_chip' * and_req_val = b_chip + + +ev u32xor_bus_constraint([stack_top[16]], [b_chip]): + # xor_req_val represents bitwise operation request value. + let xor_req_val = $alpha[0] + + $alpha[1] * BITWISE_XOR + + $alpha[2] * stack_top[0] + + $alpha[3] * stack_top[1] + + $alpha[4] * stack_top[0]' + + # Enforce u32and bus constraint. + enf b_chip' * xor_req_val = b_chip + + +ev mloadw_bus_constraint([s[16], clk], [b_chip]): + let v = sum([$alpha[i + 5] * s[3 - i]' for i in 0..4]) + let u_mem = $alpha[0] + $alpha[1] * MEMORY_READ + $alpha[3] * s[0] + $alpha[4] * clk + v + enf b_chip' * u_mem = b_chip + + +ev mload_bus_constraint([s[16], op_helpers[6], clk], [b_chip]): + let v = $alpha[5] * s[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) + let u_mem = $alpha[0] + $alpha[1] * MEMORY_READ + $alpha[3] * s[0] + $alpha[4] * clk + v + enf b_chip' * u_mem = b_chip + + +ev mstorew_bus_constraint([s[16], clk], [b_chip]): + let v = sum([$alpha[i + 5] * s[3 - i]']) for i in 0..4 + let u_mem = $alpha[0] + $alpha[1] * MEMORY_WRITE + $alpha[3] * s[0] + $alpha[4] * clk + v + enf b_chip' * u_mem = b_chip + + +ev mstore_bus_constraint([s[16], op_helpers[6], clk], [b_chip]): + let v = $alpha[5] * s[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) + let u_mem = $alpha[0] + $alpha[1] * MEMORY_WRITE + $alpha[3] * s[0] + $alpha[4] * clk + v + enf b_chip' * u_mem = b_chip + + +ev hperm_bus_constraint([s[16], op_helpers[6]], [b_chip]): + let v_input = $alpha[0] + + $alpha[1] * HASHER_LINEAR_HASH + + $alpha[2] * op_helpers[0] + + sum([$alpha[i + 4] * s[11 - i] for i in 0..12]) + + let v_output = $alpha[0] + + $alpha[1] * HASHER_RETURN_STATE + + $alpha[2] * (op_helpers[0] + 7) + + sum([$alpha[i + 4] * s[11 - i]' for i in 0..12]) + + enf b_chip' * v_input * v_output = b_chip + + +ev mpverify_bus_constraint([s[16], op_helpers[6]], [b_chip]): + let v_input = $alpha[0] + + $alpha[1] * HASHER_MP_VERIFY + + $alpha[2] * op_helpers[0] + + $alpha[3] * s[5] + + sum([$alpha[i + 8] * s[3 - i] for i in 0..4]) + + let v_output = $alpha[0] + + $alpha[1] * HASHER_RETURN_HASH + + $alpha[2] * (op_helpers[0] + 8 * s[4] - 1) + + sum([$alpha[i + 8] * s[9 - i] for i in 0..4]) + + enf b_chip' * v_input * v_output = b_chip + + +ev mrupdate_bus_constraint([s[16], op_helpers[6]], [b_chip]): + let v_input_old = $alpha[0] + + $alpha[1] * HASHER_MR_UPDATE_OLD + + $alpha[2] * op_helpers[0] + + $alpha[3] * s[5] + + sum([$alpha[i + 8] * s[3 - i] for i in 0..4]) + + let v_output_old = $alpha[0] + + $alpha[1] * HASHER_RETURN_HASH + + $alpha[2] * (op_helpers[0] + 8 * s[4] - 1) + + sum([$alpha[i + 8] * s[9 - i] for i in 0..4]) + + let v_input_new = $alpha[0] + + $alpha[1] * HASHER_MR_UPDATE_NEW + + $alpha[2] * (op_helpers[0] + 8 * s[4]) + + $alpha[3] * s[5] + + sum([$alpha[i + 8] * s[13 - i] for i in 0..4]) + + let v_output_new = $alpha[0] + + $alpha[1] * op_rethash + + $alpha[2] * (op_helpers[0] + 2 * 8 * s[4] - 1) + + sum([$alpha[i + 8] * s[3 - i]' for i in 0..4]) + + enf b_chip' * v_input_old * v_output_old * v_input_new * v_output_new = b_chip + + ### Stack Air Constraints ######################################################################### # Enforces the constraints on the stack. @@ -235,82 +353,82 @@ ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6] let op_flags = compute_op_flags(op_bits) match enf: - noop([stack_top]) when op_flags[0] - eqz([stack_top, stack_helpers[2]]) when op_flags[1] - neg([stack_top]) when op_flags[2] - inv([stack_top]) when op_flags[3] - incr([stack_top]) when op_flags[4] - not([stack_top]) when op_flags[5] - fmpadd([stack_top, fmp]) when op_flags[6] - mload([stack_top, op_helpers, clk]) when op_flags[7] - swap([stack_top]) when op_flags[8] + noop([stack_top]) when op_flags[0] + eqz([stack_top, stack_helpers[2]]) when op_flags[1] + neg([stack_top]) when op_flags[2] + inv([stack_top]) when op_flags[3] + incr([stack_top]) when op_flags[4] + not([stack_top]) when op_flags[5] + fmpadd([stack_top, fmp]) when op_flags[6] + mload([stack_top, op_helpers, clk], [b_chip]) when op_flags[7] + swap([stack_top]) when op_flags[8] # TODO: add match variant for caller caller() - movup2([stack_top]) when op_flags[10] - movdn2([stack_top]) when op_flags[11] - movup3([stack_top]) when op_flags[12] - movdn3([stack_top]) when op_flags[13] - advpopw([stack_top]) when op_flags[14] - expacc([stack_top, stack_helpers[2]]) when op_flags[15] - movup4([stack_top]) when op_flags[16] - movdn4([stack_top]) when op_flags[17] - movup5([stack_top]) when op_flags[18] - movdn5([stack_top]) when op_flags[19] - movup6([stack_top]) when op_flags[20] - movdn6([stack_top]) when op_flags[21] - movup7([stack_top]) when op_flags[22] - movdn7([stack_top]) when op_flags[23] - swapw([stack_top]) when op_flags[24] - ext2mul([stack_top]) when op_flags[25] - movup8([stack_top]) when op_flags[26] - movdn8([stack_top]) when op_flags[27] - swapw2([stack_top]) when op_flags[28] - swapw3([stack_top]) when op_flags[29] - swapdw([stack_top]) when op_flags[30] - - assert([stack_top]) when op_flags[32] - eq([stack_top, stack_helpers[2]]) when op_flags[33] - add([stack_top]) when op_flags[34] - mul([stack_top]) when op_flags[35] - and([stack_top]) when op_flags[36] - or([stack_top]) when op_flags[37] - u32and([stack_top]) when op_flags[38] - u32xor([stack_top]) when op_flags[39] + movup2([stack_top]) when op_flags[10] + movdn2([stack_top]) when op_flags[11] + movup3([stack_top]) when op_flags[12] + movdn3([stack_top]) when op_flags[13] + advpopw([stack_top]) when op_flags[14] + expacc([stack_top, stack_helpers[2]]) when op_flags[15] + movup4([stack_top]) when op_flags[16] + movdn4([stack_top]) when op_flags[17] + movup5([stack_top]) when op_flags[18] + movdn5([stack_top]) when op_flags[19] + movup6([stack_top]) when op_flags[20] + movdn6([stack_top]) when op_flags[21] + movup7([stack_top]) when op_flags[22] + movdn7([stack_top]) when op_flags[23] + swapw([stack_top]) when op_flags[24] + ext2mul([stack_top]) when op_flags[25] + movup8([stack_top]) when op_flags[26] + movdn8([stack_top]) when op_flags[27] + swapw2([stack_top]) when op_flags[28] + swapw3([stack_top]) when op_flags[29] + swapdw([stack_top]) when op_flags[30] + + assert([stack_top]) when op_flags[32] + eq([stack_top, stack_helpers[2]]) when op_flags[33] + add([stack_top]) when op_flags[34] + mul([stack_top]) when op_flags[35] + and([stack_top]) when op_flags[36] + or([stack_top]) when op_flags[37] + u32and([stack_top], [b_chip]) when op_flags[38] + u32xor([stack_top], [b_chip]) when op_flags[39] # TODO: add match variant for frie2f4 frie2f4() - drop([stack_top]) when op_flags[41] - cswap([stack_top]) when op_flags[42] - cswapw([stack_top]) when op_flags[43] - mloadw([stack_top, clk]) when op_flags[44] - mstore([stack_top, op_helpers, clk]) when op_flags[45] - mstorew([stack_top, clk]) when op_flags[46] - fmpupdate([stack_top, fmp]) when op_flags[47] - - pad([stack_top]) when op_flags[48] - dup([stack_top]) when op_flags[49] - dup1([stack_top]) when op_flags[50] - dup2([stack_top]) when op_flags[51] - dup3([stack_top]) when op_flags[52] - dup4([stack_top]) when op_flags[53] - dup5([stack_top]) when op_flags[54] - dup6([stack_top]) when op_flags[55] - dup7([stack_top]) when op_flags[56] - dup9([stack_top]) when op_flags[57] - dup11([stack_top]) when op_flags[58] - dup13([stack_top]) when op_flags[59] - dup15([stack_top]) when op_flags[60] - advpop([stack_top]) when op_flags[61] - sdepth([stack_top, stack_helpers[0]]) when op_flags[62] - clk([stack_top, clk]) when op_flags[63] - - u32add([stack_top, op_helpers]) when op_flags[64] - u32sub([stack_top, op_helpers]) when op_flags[65] - u32mul([stack_top, op_helpers]) when op_flags[66] - u32div([stack_top, op_helpers]) when op_flags[67] - u32split([stack_top, op_helpers]) when op_flags[68] - u32assert2([stack_top, op_helpers]) when op_flags[69] - u32add3([stack_top, op_helpers]) when op_flags[70] - u32madd([stack_top, op_helpers]) when op_flags[71] + drop([stack_top]) when op_flags[41] + cswap([stack_top]) when op_flags[42] + cswapw([stack_top]) when op_flags[43] + mloadw([stack_top, clk], [b_chip]) when op_flags[44] + mstore([stack_top, op_helpers, clk]) when op_flags[45] + mstorew([stack_top, clk], [b_chip]) when op_flags[46] + fmpupdate([stack_top, fmp]) when op_flags[47] + + pad([stack_top]) when op_flags[48] + dup([stack_top]) when op_flags[49] + dup1([stack_top]) when op_flags[50] + dup2([stack_top]) when op_flags[51] + dup3([stack_top]) when op_flags[52] + dup4([stack_top]) when op_flags[53] + dup5([stack_top]) when op_flags[54] + dup6([stack_top]) when op_flags[55] + dup7([stack_top]) when op_flags[56] + dup9([stack_top]) when op_flags[57] + dup11([stack_top]) when op_flags[58] + dup13([stack_top]) when op_flags[59] + dup15([stack_top]) when op_flags[60] + advpop([stack_top]) when op_flags[61] + sdepth([stack_top, stack_helpers[0]]) when op_flags[62] + clk([stack_top, clk]) when op_flags[63] + + u32add([stack_top, op_bits, op_helpers]) when op_flags[64] + u32sub([stack_top, op_bits, op_helpers]) when op_flags[65] + u32mul([stack_top, op_bits, op_helpers]) when op_flags[66] + u32div([stack_top, op_bits, op_helpers]) when op_flags[67] + u32split([stack_top, op_bits, op_helpers]) when op_flags[68] + u32assert2([stack_top, op_bits, op_helpers]) when op_flags[69] + u32add3([stack_top, op_bits, op_helpers]) when op_flags[70] + u32madd([stack_top, op_bits, op_helpers]) when op_flags[71] ev overflow_table_constraints( @@ -376,8 +494,8 @@ ev fmpadd([s[16], fmp]): enf s[0]' = s[0] + fmp enf s[i]' = s[i] for i in 1..16 -# Bus constraint is implemented in a separate file -ev mload([s[16], clk]): +ev mload([s[16], op_helpers, clk], [b_chip]): + enf mload_bus_constraint([s, op_helpers, clk], [b_chip]) enf s[i]' = s[i] for i in 1..16 ev swap([s[16]]): @@ -529,12 +647,12 @@ ev or([s[16]]): enf s[0]' = s[1] + s[0] - s[1] * s[0] enf s[i]' = s[i + 1] for i in 1..15 -# Bus constraint is implemented in a separate file -ev u32and([s[16]]): +ev u32and([s[16]], [b_chip]): + enf u32and_bus_constraint([s[16]], [b_chip]) enf s[i]' = s[i + 1] for i in 1..15 -# Bus constraint is implemented in a separate file -ev u32xor([s[16]]): +ev u32xor([s[16]], [b_chip]): + enf u32xor_bus_constraint([s[16]], [b_chip]) enf s[i]' = s[i + 1] for i in 1..15 # TODO: add constraints @@ -557,15 +675,17 @@ ev cswapw([s[16]]): enf s[i]' = s[i + 1] for i in 8..15 # Bus constraint is implemented in a separate file -ev mloadw([s[16], clk]): +ev mloadw([s[16], clk], [b_chip]): + enf mloadw_bus_constraint([s, clk], [b_chip]) enf s[i]' = s[i + 1] for i in 4..15 -# Bus constraint is implemented in a separate file -ev mstore([s[16], clk]): +ev mstore([s[16], op_helpers, clk]): + enf mstore_bus_constraint([s, op_helpers, clk], [b_chip]) enf s[i]' = s[i + 1] for i in 0..15 # Bus constraint is implemented in a separate file -ev mstorew([s[16], clk]): +ev mstorew([s[16], clk], [b_chip]): + enf mstorew_bus_constraint([s, clk], [b_chip]) enf s[i]' = s[i + 1] for i in 0..15 ev fmpupdate([s[16], fmp]): @@ -702,13 +822,13 @@ ev u32madd([s[16], op_bits[8], op_helpers[6]]): # High-degree operations -# Bus constraint is implemented in a separate file -ev hperm([s[16], op_bits[8], op_helpers[6]]): +ev hperm([s[16], op_bits[8], op_helpers[6]], [b_chip]): + enf hperm_bus_constraint([s, op_helpers], [b_chip]) enf s[i]' = s[i] for i in 12..16 enf b0_is_zero([op_bits]) -# Bus constraint is implemented in a separate file -ev mpverify([s[16], op_bits[8], op_helpers[6]]): +ev mpverify([s[16], op_bits[8], op_helpers[6]], [b_chip]): + enf mpverify_bus_constraint([s, op_helpers], [b_chip]) enf s[i]' = s[i] for i in 0..16 enf b0_is_zero([op_bits]) @@ -737,8 +857,8 @@ ev loop() # Very high-degree operations -# Bus constraint is implemented in a separate file ev mrupdate([s[16], op_bits[8], op_helpers[6]]): + enf mrupdate_bus_constraint([s, op_helpers], [b_chip]) enf s[i]' = s[i] for i in 4..16 enf b0_b1_is_zero([op_bits]) From 793e0a6b7c1773e6cba436fb07baa97756af13ec Mon Sep 17 00:00:00 2001 From: Andrey Khmuro Date: Tue, 6 Jun 2023 17:17:42 +0300 Subject: [PATCH 12/12] refactor: combine both sides of chiplet bus constraints --- constraints/miden-vm/buses/chiplet_bus.air | 506 +++++++++++++++++++++ constraints/miden-vm/decoder.air | 72 +-- constraints/miden-vm/stack.air | 137 ------ 3 files changed, 507 insertions(+), 208 deletions(-) create mode 100644 constraints/miden-vm/buses/chiplet_bus.air diff --git a/constraints/miden-vm/buses/chiplet_bus.air b/constraints/miden-vm/buses/chiplet_bus.air new file mode 100644 index 000000000..88185313b --- /dev/null +++ b/constraints/miden-vm/buses/chiplet_bus.air @@ -0,0 +1,506 @@ +mod ChipletBus + +### Constants and periodic columns ################################################################ + +const MEMORY_READ = 12 +const MEMORY_WRITE = 4 + +const HASHER_LINEAR_HASH = 3 +const HASHER_MP_VERIFY = 11 +const HASHER_MR_UPDATE_OLD = 7 +const HASHER_MR_UPDATE_NEW = 15 +const HASHER_RETURN_HASH = 1 +const HASHER_RETURN_STATE = 9 + +periodic_columns: + k0: [1, 0, 0, 0, 0, 0, 0, 0] + k1: [1, 1, 1, 1, 1, 1, 1, 0] + +### Helper functions ############################################################################## + +# Returns the f_join operation flag which is set when JOIN control operation is executed. +# +# Flag degree: 5 +fn get_f_join(op_bits: vector[9]) -> scalar: + return op_bits[7] & !op_bits[3] & op_bits[2] & op_bits[1] & op_bits[0] + + +# Returns the f_split operation flag which is set when SPLIT control operation is executed. +# +# Flag degree: 5 +fn get_f_split(op_bits: vector[9]) -> scalar: + return op_bits[7] & !op_bits[3] & op_bits[2] & !op_bits[1] & !op_bits[0] + + +# Returns the f_loop operation flag which is set when LOOP control operation is executed. +# +# Flag degree: 5 +fn get_f_loop(op_bits: vector[9]) -> scalar: + return op_bits[7] & !op_bits[3] & op_bits[2] & !op_bits[1] & op_bits[0] + + +# Returns the f_call operation flag which is set when CALL control operation is executed. +# +# Flag degree: 4 +fn get_f_call(op_bits: vector[9]) -> scalar: + return op_bits[8] & !op_bits[4] & op_bits[3] & op_bits[2] + + +# Returns the f_syscall operation flag which is set when SYSCALL control operation is executed. +# +# Flag degree: 4 +fn get_f_syscall(op_bits: vector[9]) -> scalar: + return op_bits[8] & !op_bits[4] & op_bits[3] & !op_bits[2] + + +# Returns the f_span operation flag which is set when SPAN operation is executed. +# +# Flag degree: 5 +fn get_f_span(op_bits: vector[9]) -> scalar: + return op_bits[7] & !op_bits[3] & op_bits[2] & op_bits[1] & !op_bits[0] + + +# Returns the f_respan operation flag which is set when RESPAN operation is executed. +# +# Flag degree: 4 +fn get_f_respan(op_bits: vector[9]) -> scalar: + return op_bits[8] & op_bits[4] & op_bits[3] & !op_bits[2] + + +# Returns the f_end operation flag which is set when END operation is executed. +# +# Flag degree: 4 +fn get_f_end(op_bits: vector[9]) -> scalar: + return op_bits[8] & op_bits[4] & !op_bits[3] & !op_bits[2] + + +# Returns f_ctrli flag which is set to 1 when a control flow operation that signifies the +# initialization of a control block (JOIN, SPLIT, LOOP, CALL, SYSCALL) is being executed on the VM. +# +# Flag degree: 5 +fn get_f_ctrli(op_bits: vector[9]) -> scalar: + return get_f_join(op_bits) + get_f_split(op_bits) + get_f_loop(op_bits) + get_f_call(op_bits) + get_f_syscall(op_bits) + + +# Returns transition label, composed of the operation label and the periodic columns that uniquely +# identify each transition function. +fn get_transition_label(op_label: scalar) -> scalar: + return op_label + 2^4 * cycle_row_7 + 2^5 * cycle_row_0 + + +# Set to 1 when selector flags are (1,0,0) on rows which are multiples of 8. This flag indicates +# that we are initiating computation of a single permutation, a 2-to-1 hash, or a linear hash of +# many elements. +fn get_f_bp(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & !s[1] & !s[2] + + +# Set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple of 8. This flag +# indicates that the result of the currently running computation is returned. +fn get_f_hout(s: vector[3]) -> scalar: + return cycle_row_7 & !s[0] & !s[1] & !s[2] + + +# Set to 1 when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This flag +# indicates that the entire hasher state is returned. +fn get_f_sout(s: vector[3]) -> scalar: + return cycle_row_7 & !s[0] & !s[1] & s[2] + + +# Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row. +fn get_f_out(s: vector[3]) -> scalar: + return cycle_row_7 & !s[0] & !s[1] + + +# Set to 1 when selector flags are (1,0,1) on rows which are multiples of 8. This is flag of the +# instruction that initiates Merkle path verification computation. +fn get_f_mp(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & !s[1] & s[2] + + +# Set to 1 when selector flags are (1,1,0) on rows which are multiples of 8. This is flag of the +# instruction that initiates Merkle path verification for the "old" node value during Merkle root +# update computation. +fn get_f_mv(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & s[1] & !s[2] + + +# Set to 1 when selector flags are (1,1,1) on rows which are multiples of 8. This is flag of the +# instruction that initiates Merkle path verification for the "new" node value during Merkle root +# update computation. +fn get_f_mu(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & s[1] & s[2] + + +# Set to 1 when selector flags are (1,0,0) on rows which are 1 less than a multiple of 8. This +# is flag of the instruction that absorbs a new set of elements into the hasher state when +# computing a linear hash of many elements. +fn get_f_abp(s: vector[3]) -> scalar: + return cycle_row_7 & s[0] & !s[1] & !s[2] + + +fn get_hash_response_value( + s: vector[3], + r: scalar, + hasher: vector[12], + hasher_next: vector[12], + i: scalar, + i_next: scalar +) -> scalar: + # Compute falgs required for the chiplet bus constraint. + let f_bp = get_f_bp(s) + let f_sout = get_f_sout(s) + let f_hout = get_f_hout(s) + let f_out = get_f_out(s) + let f_mp = get_f_mp(s) + let f_mv = get_f_mv(s) + let f_mu = get_f_mu(s) + let f_abp = get_f_abp(s) + + let op_label = 2^3 * s[2] + 2^2 * s[1] + 2^1 * s[0] + 1 + let transition_label = get_transition_label(op_label) + + # v_h is a common header. + let v_h = $alpha[0] + $alpha[1] * transition_label + $alpha[2] * r + $alpha[3] * i + + # v_a, v_b and v_c are the first, second, and third words of the hasher state. + let v_a = sum([$alpha[j + 4] * hasher[j] for j in 0..4]) + let v_b = sum([$alpha[j + 4] * hasher[j] for j in 4..8]) + let v_b_next = sum([$alpha[j + 4] * hasher_next[j] for j in 4..8]) + let v_c = sum([$alpha[j + 4] * hasher[j] for j in 8..12]) + let v_c_next = sum([$alpha[j + 4] * hasher_next[j] for j in 8..12]) + + # v_d is the third word of the hasher state but computed using the same alphas values as used + # for the second word. + let v_d = sum([$alpha[j] * hasher[j] for j in 8..12]) + + # v_all represents the entire hasher state. + let v_all = v_h + v_a + v_b + v_c + + # b is the value of the bit which is discarded during shift by one bit to the right. + let b = i - 2 * i_next + + # v_leaf represents the leaf of the path. + let v_leaf = v_h + (1 - b) * v_b + b * v_d + + # v_abp represents delta between the last 8 elements of the hasher state during absorption a + # new set of elements into the state while computing a linear hash. + let v_abp = v_h + v_b_next + v_c_next - (v_b + v_c) + + # v_res represents returning the hash result, taken from the second word of the hasher state. + let v_res = v_h + v_b + + let hash_response_value = ((f_bp + f_sout) * v_all + (f_mp + f_mv + f_mu) * v_leaf + f_abp * v_abp + + f_hout * v_res + 1 - (f_bp + f_mp + f_mv + f_mu + f_abp + f_out)) + + return hash_response_value + + +### Helper evaluators ############################################################################# + +# Enforces that register extra0 is set to 1 when high-degree operations are executed. +ev extra0([op_bits[9]]): + op_bits[7] = 1 when op_bits[6] & !op_bits[5] & op_bits[4] + +# Enforces that register extra1 is set to 1 when very high-degree operations are executed. +ev extra1([op_bits[9]]): + op_bits[8] = 1 when op_bits[6] & op_bits[5] + + +# - BITWISE --------------------------------------------------------------------------------------- + +# Enforces the constraint for the bitwise chiplet bus. +# +# Constraint degree: 4 +ev bitwise([stack[16], a, b, z], [b_chip]): + # Calculate the operation label for the bitwise operation. + let op_bitwise = s * 2^2 + 2 + + # req_val represents bitwise operation request value. + let req_val = $alpha[0] + + $alpha[1] * op_bitwise + + $alpha[2] * stack[0] + + $alpha[3] * stack[1] + + $alpha[4] * stack[0]' + + # u_i represents reduction of a, b abd z into a single value for row i. + let u_i = $alpha[0] + + $alpha[1] * op_bitwise + + $alpha[2] * a + + $alpha[3] * b + + $alpha[4] * z + + # m represents inversion of k1 periodic column. + let m = !k1 + + # v_i represents value that includes u_i into the product when k1 = 0. + let v_i = m * u_i + + # Enforce the constraints for the two sides of the bus communication. + # Constraint degree: 4 + enf b_chip' * req_val = b_chip * (v_i * m + 1 - m) + + +# - MEMORY ---------------------------------------------------------------------------------------- + +ev mloadw([stack[16], ctx, addr, clk, v[4]], [b_chip]): + let mem_state = sum([$alpha[i + 5] * stack[3 - i]' for i in 0..4]) + let u_mem = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * stack[0] + + $alpha[4] * clk + mem_state + + # v_mem represents a row in the memory table. + let v_mem = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * addr + + $alpha[4] * clk + + sum([$alpha[j + 5] * v[j] for j in 0..4]) + + # Enforce the constraint for the two sides of the bus communication. + enf b_chip' * u_mem = b_chip * v_mem + + +ev mload([stack[16], op_helpers[6], ctx, addr, clk, v[4]], [b_chip]): + let mem_state = $alpha[5] * stack[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) + let u_mem = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * stack[0] + + $alpha[4] * clk + mem_state + + # v_mem represents a row in the memory table. + let v_mem = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * addr + + $alpha[4] * clk + + sum([$alpha[j + 5] * v[j] for j in 0..4]) + + # Enforce the constraint for the two sides of the bus communication. + enf b_chip' * u_mem = b_chip * v_mem + + +ev mstorew([stack[16], ctx, addr, clk, v[4]], [b_chip]): + let mem_state = sum([$alpha[i + 5] * stack[3 - i]'] for i in 0..4) + let u_mem = $alpha[0] + + $alpha[1] * MEMORY_WRITE + + $alpha[2] * ctx + + $alpha[3] * stack[0] + + $alpha[4] * clk + mem_state + + # v_mem represents a row in the memory table. + let v_mem = $alpha[0] + + $alpha[1] * MEMORY_WRITE + + $alpha[2] * ctx + + $alpha[3] * addr + + $alpha[4] * clk + + sum([$alpha[j + 5] * v[j] for j in 0..4]) + + # Enforce the constraint for the two sides of the bus communication. + enf b_chip' * u_mem = b_chip * v_mem + + +ev mstore([stack[16], op_helpers[6], ctx, addr, clk, v[4]], [b_chip]): + let mem_state = $alpha[5] * stack[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) + let u_mem = $alpha[0] + + $alpha[1] * MEMORY_WRITE + + $alpha[2] * ctx + + $alpha[3] * stack[0] + + $alpha[4] * clk + mem_state + + # v_mem represents a row in the memory table. + let v_mem = $alpha[0] + + $alpha[1] * MEMORY_WRITE + + $alpha[2] * ctx + + $alpha[3] * addr + + $alpha[4] * clk + + sum([$alpha[j + 5] * v[j] for j in 0..4]) + + # Enforce the constraint for the two sides of the bus communication. + enf b_chip' * u_mem = b_chip * v_mem + + +ev mstream([stack[16], ctx, addr, clk, v[4]], [b_chip]): + let v1 = sum([$alpha[i + 5] * stack[7 - i]' for i in 0..4]) + let v2 = sum([$alpha[i + 5] * stack[3 - i]' for i in 0..4]) + let u_mem1 = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * stack[12] + + $alpha[4] * clk + v1 + + let u_mem2 = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * (stack[12] + 1) + + $alpha[4] * clk + v2 + + let u_mem = u_mem1 * u_mem2 + + # v_mem represents a row in the memory table. + let v_mem = $alpha[0] + + $alpha[1] * MEMORY_READ + + $alpha[2] * ctx + + $alpha[3] * addr + + $alpha[4] * clk + + sum([$alpha[j + 5] * v[j] for j in 0..4]) + + # Enforce the constraint for the two sides of the bus communication. + enf b_chip' * u_mem = b_chip * v_mem + + +# - HASH ------------------------------------------------------------------------------------------ + +ev hperm([stack[16], op_helpers[6], selector[3], row, hasher[12], index], [b_chip]): + let v_input = $alpha[0] + + $alpha[1] * HASHER_LINEAR_HASH + + $alpha[2] * op_helpers[0] + + sum([$alpha[i + 4] * stack[11 - i] for i in 0..12]) + + let v_output = $alpha[0] + + $alpha[1] * HASHER_RETURN_STATE + + $alpha[2] * (op_helpers[0] + 7) + + sum([$alpha[i + 4] * stack[11 - i]' for i in 0..12]) + + let response_value = get_hash_response_value(selector, row, hasher, hasher', index, index') + + enf b_chip' * v_input * v_output = b_chip * response_value + + +ev mpverify([stack[16], op_helpers[6], selector[3], row, hasher[12], index], [b_chip]): + let v_input = $alpha[0] + + $alpha[1] * HASHER_MP_VERIFY + + $alpha[2] * op_helpers[0] + + $alpha[3] * stack[5] + + sum([$alpha[i + 8] * stack[3 - i] for i in 0..4]) + + let v_output = $alpha[0] + + $alpha[1] * HASHER_RETURN_HASH + + $alpha[2] * (op_helpers[0] + 8 * stack[4] - 1) + + sum([$alpha[i + 8] * stack[9 - i] for i in 0..4]) + + let response_value = get_hash_response_value(selector, row, hasher, hasher', index, index') + + enf b_chip' * v_input * v_output = b_chip * response_value + + +ev mrupdate([stack[16], op_helpers[6], selector[3], row, hasher[12], index], [b_chip]): + let v_input_old = $alpha[0] + + $alpha[1] * HASHER_MR_UPDATE_OLD + + $alpha[2] * op_helpers[0] + + $alpha[3] * stack[5] + + sum([$alpha[i + 8] * stack[3 - i] for i in 0..4]) + + let v_output_old = $alpha[0] + + $alpha[1] * HASHER_RETURN_HASH + + $alpha[2] * (op_helpers[0] + 8 * stack[4] - 1) + + sum([$alpha[i + 8] * stack[9 - i] for i in 0..4]) + + let v_input_new = $alpha[0] + + $alpha[1] * HASHER_MR_UPDATE_NEW + + $alpha[2] * (op_helpers[0] + 8 * stack[4]) + + $alpha[3] * stack[5] + + sum([$alpha[i + 8] * stack[13 - i] for i in 0..4]) + + let v_output_new = $alpha[0] + + $alpha[1] * HASHER_RETURN_HASH + + $alpha[2] * (op_helpers[0] + 2 * 8 * stack[4] - 1) + + sum([$alpha[i + 8] * stack[3 - i]' for i in 0..4]) + + let response_value = get_hash_response_value(selector, row, hasher, hasher', index, index') + + enf b_chip' * v_input_old * v_output_old * v_input_new * v_output_new = b_chip * response_value + + +# Enforces the constraint for computing block hashes. +# +# Max constraint degree: 8 +ev block_hash_computation([addr, op_bits[9], extra, selector[3], row, hasher[12], index], [b_chip]): + enf extra0(op_bits) + enf extra1(op_bits) + + # Get flags required for the block hash computation constraint + let f_ctrli = get_f_ctrli(op_bits) + let f_span = get_f_span(op_bits) + let f_respan = get_f_respan(op_bits) + let f_end = get_f_end(op_bits) + + # Label specifying that we are starting a new hash computation. + let m_bp = get_transition_label(HASHER_LINEAR_HASH) + + # Label specifying that we are absorbing the next sequence of 8 elements into an ongoing hash + # computation. + let m_abp = get_transition_label(HASHER_LINEAR_HASH) + + # Label specifying that we are reading the result of a hash computation. + let m_hout = get_transition_label(HASHER_RETURN_HASH) + + # `alpha` is the global random values array. + let rate_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..8]) + let digest_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..4]) + + # Variable for initiating a hasher with address addr' and absorbing 8 elements from the hasher + # state (hasher[0], ..., hasher[7]) into it. + let h_init = $alpha[0] + $alpha[1] * m_bp + $alpha[2] * addr' + rate_sum + + # Variable for the absorption. + let h_abp = $alpha[0] + $alpha[1] * m_abp + $alpha[2] * addr' + rate_sum + + # Variable for the result. + let h_res = $alpha[0] + $alpha[1] * m_hout + $alpha[2] * (addr + 7) + digest_sum + + # Opcode value of the opcode being executed on the virtual machine. + let opcode_value = sum([op_bits[i] * 2^i for i in 0..7]) + + # When a control block initializer operation (JOIN, SPLIT, LOOP, CALL, SYSCALL) is executed, a + # new hasher is initialized and the contents of hasher[0], ..., hasher[7] are absorbed into the + # hasher. + # + # Value degree: 7 + let u_ctrli = f_ctrli * (h_init + $alpha[5] * opcode_value) + + # When SPAN operation is executed, a new hasher is initialized and contents of + # hasher[0], ..., hasher[7] are absorbed into the hasher. + # + # Value degree: 7 + let u_span = f_span * h_init + + # When RESPAN operation is executed, contents of hasher[0], ..., hasher[7] (which contain the + # new operation batch) are absorbed into the hasher. + # + # Value degree: 5 + let u_respan = f_respan * h_abp + + # When END operation is executed, the hash result is copied into registers + # hasher[0], ..., hasher[3]. + # + # Value degree: 5 + let u_end = f_end * h_res + + let response_value = get_hash_response_value(selector, row, hasher, hasher', index, index') + + # Enforce the block hash computation constraint. We need to add 1 and subtract the sum of the + # relevant operation flags in the left side of equation to ensure that when none of the flags + # is set to 1, the above constraint reduces to b_chip' = b_chip. + # Constraint degree: 8 + enf b_chip' * (u_ctrli + u_span + u_respan + u_end + 1 - (f_ctrli + f_span + f_respan + f_end)) = b_chip * response_value + + +### Chiplet Bus Air Constraints ################################################################### + +ev chiplet_bus([stack[16], op_helpers[6], ctx, addr, decoder_addr, clk, v[4], op_bits[9], extra, selector[3], row, hasher[12], index, a, b, z], [b_chip]): + enf block_hash_computation([decoder_addr, op_bits, extra, selector, row, hasher, index], [b_chip]) + + match enf: + bitwise([stack, a, b, z], [b_chip]) when !op_bits[6] & op_bits[5] & !op_bits[4] & !op_bits[3] & op_bits[2] & op_bits[1] + mloadw([stack, ctx, addr, clk, v], [b_chip]) when !op_bits[6] & op_bits[5] & !op_bits[4] & op_bits[3] & op_bits[2] & !op_bits[1] & !op_bits[0] + mload([stack, op_helpers, ctx, addr, clk, v], [b_chip]) when !op_bits[6] & !op_bits[5] & !op_bits[4] & !op_bits[3] & op_bits[2] & op_bits[1] & op_bits[0] + mstorew([stack, ctx, addr, clk, v], [b_chip]) when !op_bits[6] & op_bits[5] & !op_bits[4] & op_bits[3] & op_bits[2] & op_bits[1] & !op_bits[0] + mstore([stack, op_helpers, ctx, addr, clk, v], [b_chip]) when !op_bits[6] & op_bits[5] & !op_bits[4] & op_bits[3] & op_bits[2] & !op_bits[1] & op_bits[0] + mstream([stack, ctx, addr, clk, v], [b_chip]) when op_bits[7] & !op_bits[3] & !op_bits[2] & op_bits[1] & op_bits[0] + hperm([stack, op_helpers, selector, row, hasher, index], [b_chip]) when op_bits[7] & !op_bits[3] & !op_bits[2] & !op_bits[1] & !op_bits[0] + mpverify([stack, op_helpers, selector, row, hasher, index], [b_chip]) when op_bits[7] & !op_bits[3] & !op_bits[2] & !op_bits[1] & op_bits[0] + mrupdate([stack, op_helpers, selector, row, hasher, index], [b_chip]) when op_bits[8] & !op_bits[4] & !op_bits[3] & !op_bits[2] \ No newline at end of file diff --git a/constraints/miden-vm/decoder.air b/constraints/miden-vm/decoder.air index 46e3a603e..7a685749b 100644 --- a/constraints/miden-vm/decoder.air +++ b/constraints/miden-vm/decoder.air @@ -216,76 +216,6 @@ ev general([addr, op_bits[7], hasher[8], in_span, s0, extra]): enf 1 - in_span - get_f_ctrl(op_bits, extra) = 0 -# Enforces the constraint for computing block hashes. -# -# Max constraint degree: 8 -ev block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]): - # Get flags required for the block hash computation constraint - let f_ctrli = get_f_ctrli(op_bits, extra) - let f_span = get_f_span(op_bits) - let f_respan = get_f_respan(op_bits, extra) - let f_end = get_f_end(op_bits, extra) - - # Label specifying that we are starting a new hash computation. - let m_bp = get_transition_label(HASHER_LINEAR_HASH) - - # Label specifying that we are absorbing the next sequence of 8 elements into an ongoing hash - # computation. - let m_abp = get_transition_label(HASHER_LINEAR_HASH) - - # Label specifying that we are reading the result of a hash computation. - let m_hout = get_transition_label(HASHER_RETURN_HASH) - - # `alpha` is the global random values array. - let rate_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..8]) - let digest_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..4]) - - # Variable for initiating a hasher with address addr' and absorbing 8 elements from the hasher - # state (hasher[0], ..., hasher[7]) into it. - let h_init = $alpha[0] + $alpha[1] * m_bp + $alpha[2] * addr' + rate_sum - - # Variable for the absorption. - let h_abp = $alpha[0] + $alpha[1] * m_abp + $alpha[2] * addr' + rate_sum - - # Variable for the result. - let h_res = $alpha[0] + $alpha[1] * m_hout + $alpha[2] * (addr + 7) + digest_sum - - # Opcode value of the opcode being executed on the virtual machine. - let opcode_value = sum([op_bits[i] * 2^i for i in 0..7]) - - # When a control block initializer operation (JOIN, SPLIT, LOOP, CALL, SYSCALL) is executed, a - # new hasher is initialized and the contents of hasher[0], ..., hasher[7] are absorbed into the - # hasher. - # - # Value degree: 7 - let u_ctrli = f_ctrli * (h_init + $alpha[5] * opcode_value) - - # When SPAN operation is executed, a new hasher is initialized and contents of - # hasher[0], ..., hasher[7] are absorbed into the hasher. - # - # Value degree: 7 - let u_span = f_span * h_init - - # When RESPAN operation is executed, contents of hasher[0], ..., hasher[7] (which contain the - # new operation batch) are absorbed into the hasher. - # - # Value degree: 5 - let u_respan = f_respan * h_abp - - # When END operation is executed, the hash result is copied into registers - # hasher[0], ..., hasher[3]. - # - # Value degree: 5 - let u_end = f_end * h_res - - # Enforce the block hash computation constraint. We need to add 1 and subtract the sum of the - # relevant operation flags to ensure that when none of the flags is set to 1, the above - # constraint reduces to p[0]' = p[0]. - # Constraint degree: 8 - enf p[0]' * (u_ctrli + u_span + u_respan + u_end + 1 - - (f_ctrli + f_span + f_respan + f_end)) = p[0] - - # Enforces the constraint for updating the block stack table. # # Max constraint degree: 8 @@ -638,7 +568,7 @@ ev span_block([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_b ev decoder_constraints([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]): enf general([addr, op_bits[7], hasher[8], in_span, s0, extra]) - enf block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]) + # Block hash computation constraint (chiplet bus constraint) is implemented in the `chiplet_bus.air` file. enf block_stack_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) diff --git a/constraints/miden-vm/stack.air b/constraints/miden-vm/stack.air index 8689388bb..16cdc8dd0 100644 --- a/constraints/miden-vm/stack.air +++ b/constraints/miden-vm/stack.air @@ -238,109 +238,6 @@ ev b0_b1_is_zero([op_bits[8]]): enf op_bits[6] & op_bits[5] & op_bits[1] = 0 -ev u32and_bus_constraint([stack_top[16]], [b_chip]): - # and_req_val represents bitwise operation request value. - let and_req_val = $alpha[0] + - $alpha[1] * BITWISE_AND + - $alpha[2] * stack_top[0] + - $alpha[3] * stack_top[1] + - $alpha[4] * stack_top[0]' - - # Enforce u32and bus constraint. - enf b_chip' * and_req_val = b_chip - - -ev u32xor_bus_constraint([stack_top[16]], [b_chip]): - # xor_req_val represents bitwise operation request value. - let xor_req_val = $alpha[0] + - $alpha[1] * BITWISE_XOR + - $alpha[2] * stack_top[0] + - $alpha[3] * stack_top[1] + - $alpha[4] * stack_top[0]' - - # Enforce u32and bus constraint. - enf b_chip' * xor_req_val = b_chip - - -ev mloadw_bus_constraint([s[16], clk], [b_chip]): - let v = sum([$alpha[i + 5] * s[3 - i]' for i in 0..4]) - let u_mem = $alpha[0] + $alpha[1] * MEMORY_READ + $alpha[3] * s[0] + $alpha[4] * clk + v - enf b_chip' * u_mem = b_chip - - -ev mload_bus_constraint([s[16], op_helpers[6], clk], [b_chip]): - let v = $alpha[5] * s[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) - let u_mem = $alpha[0] + $alpha[1] * MEMORY_READ + $alpha[3] * s[0] + $alpha[4] * clk + v - enf b_chip' * u_mem = b_chip - - -ev mstorew_bus_constraint([s[16], clk], [b_chip]): - let v = sum([$alpha[i + 5] * s[3 - i]']) for i in 0..4 - let u_mem = $alpha[0] + $alpha[1] * MEMORY_WRITE + $alpha[3] * s[0] + $alpha[4] * clk + v - enf b_chip' * u_mem = b_chip - - -ev mstore_bus_constraint([s[16], op_helpers[6], clk], [b_chip]): - let v = $alpha[5] * s[0]' + sum([$alpha[i + 5] * op_helpers[3 - i]' for i in 1..4]) - let u_mem = $alpha[0] + $alpha[1] * MEMORY_WRITE + $alpha[3] * s[0] + $alpha[4] * clk + v - enf b_chip' * u_mem = b_chip - - -ev hperm_bus_constraint([s[16], op_helpers[6]], [b_chip]): - let v_input = $alpha[0] + - $alpha[1] * HASHER_LINEAR_HASH + - $alpha[2] * op_helpers[0] + - sum([$alpha[i + 4] * s[11 - i] for i in 0..12]) - - let v_output = $alpha[0] + - $alpha[1] * HASHER_RETURN_STATE + - $alpha[2] * (op_helpers[0] + 7) + - sum([$alpha[i + 4] * s[11 - i]' for i in 0..12]) - - enf b_chip' * v_input * v_output = b_chip - - -ev mpverify_bus_constraint([s[16], op_helpers[6]], [b_chip]): - let v_input = $alpha[0] + - $alpha[1] * HASHER_MP_VERIFY + - $alpha[2] * op_helpers[0] + - $alpha[3] * s[5] + - sum([$alpha[i + 8] * s[3 - i] for i in 0..4]) - - let v_output = $alpha[0] + - $alpha[1] * HASHER_RETURN_HASH + - $alpha[2] * (op_helpers[0] + 8 * s[4] - 1) + - sum([$alpha[i + 8] * s[9 - i] for i in 0..4]) - - enf b_chip' * v_input * v_output = b_chip - - -ev mrupdate_bus_constraint([s[16], op_helpers[6]], [b_chip]): - let v_input_old = $alpha[0] + - $alpha[1] * HASHER_MR_UPDATE_OLD + - $alpha[2] * op_helpers[0] + - $alpha[3] * s[5] + - sum([$alpha[i + 8] * s[3 - i] for i in 0..4]) - - let v_output_old = $alpha[0] + - $alpha[1] * HASHER_RETURN_HASH + - $alpha[2] * (op_helpers[0] + 8 * s[4] - 1) + - sum([$alpha[i + 8] * s[9 - i] for i in 0..4]) - - let v_input_new = $alpha[0] + - $alpha[1] * HASHER_MR_UPDATE_NEW + - $alpha[2] * (op_helpers[0] + 8 * s[4]) + - $alpha[3] * s[5] + - sum([$alpha[i + 8] * s[13 - i] for i in 0..4]) - - let v_output_new = $alpha[0] + - $alpha[1] * op_rethash + - $alpha[2] * (op_helpers[0] + 2 * 8 * s[4] - 1) + - sum([$alpha[i + 8] * s[3 - i]' for i in 0..4]) - - enf b_chip' * v_input_old * v_output_old * v_input_new * v_output_new = b_chip - - ### Stack Air Constraints ######################################################################### # Enforces the constraints on the stack. @@ -348,8 +245,6 @@ ev mrupdate_bus_constraint([s[16], op_helpers[6]], [b_chip]): # stack_helpers consists of [bookkeeping[0], bookkeeping[1], h0] # op_bits consists of [op_bits[7], extra] ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], [p1]): - enf overflow_table_constraints([stack_top, stack_helpers, op_bits, op_helpers, clk, fmp], [p1]) - let op_flags = compute_op_flags(op_bits) match enf: @@ -431,38 +326,6 @@ ev stack_constraints([stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6] u32madd([stack_top, op_bits, op_helpers]) when op_flags[71] -ev overflow_table_constraints( - [stack_top[16], stack_helpers[3], op_bits[8], op_helpers[6], clk, fmp], - [p1] -): - # Flag to indicate whether the overflow table contains values (overflow flag). - let f_ov = (stack_helpers[0] - 16) * stack_helpers[2] - - # Enforce that overflow flag is set correctly. - enf (1 - f_ov) * (stack_helpers[0] - 16) = 0 - - # Enforce that stack depth column stack_helpers[0] (bookkeeping[0]) is updated correctly. - enf stack_helpers[0]' - stack_helpers[0] + f_shl(op_bits, op_helpers) * f_ov - f_shr(op_bits) = 0 - - # Value of the row to be added to the table - let v = $alpha[0] + $alpha[1] * clk + $alpha[2] * stack_top[15] + $alpha[3] * stack_helpers[1] - - # Value of the row to be removed from the table - let u = $alpha[0] + $alpha[1] * stack_helpers[1] + $alpha[2] * stack_top[15]' + alpha[3] * stack_helpers[1]' - - # Enforce that right and left shifts update the overflow table correctly. - enf p1' * (u * f_shl(op_bits, op_helpers) * f_ov + 1 - f_shl(op_bits, op_helpers) * f_ov) = - p1 * (v * f_shr(op_bits) + 1 - f_shr) - - # Enforce that the next value of stack_helpers[1] (bookkeeping[1]) is set to the current value of clk. - enf f_shr(op_bits) * (stack_helpers[1]' - clk) = 0 - - # Enforce that when the overflow table is empty, 0 is "shifted in" from the right (i.e. stack_top[15] is set to 0). - enf f_shl(op_bits, op_helpers) * (1 - f_ov) * stack_top[15]' = 0 - - # TODO: enforce boundary constraints - - # No stack shift operations ev noop([s[16]]):