From 18a1295fcca36e28280ac4b73abefc9bf97eefbc Mon Sep 17 00:00:00 2001 From: Bobbin Threadbare Date: Mon, 17 Jul 2023 13:40:25 -0700 Subject: [PATCH] fix: stack depth constraint for syscall operation --- air/src/constraints/stack/mod.rs | 13 +++++++-- air/src/constraints/stack/overflow/mod.rs | 32 +++++++++++++---------- 2 files changed, 29 insertions(+), 16 deletions(-) diff --git a/air/src/constraints/stack/mod.rs b/air/src/constraints/stack/mod.rs index add95e0da3..41ddbbcfec 100644 --- a/air/src/constraints/stack/mod.rs +++ b/air/src/constraints/stack/mod.rs @@ -3,7 +3,7 @@ use super::super::{ TransitionConstraintDegree, CLK_COL_IDX, DECODER_TRACE_OFFSET, FMP_COL_IDX, ONE, STACK_AUX_TRACE_OFFSET, STACK_TRACE_OFFSET, ZERO, }; -use crate::decoder::{IS_CALL_FLAG_COL_IDX, USER_OP_HELPERS_OFFSET}; +use crate::decoder::{IS_CALL_FLAG_COL_IDX, IS_SYSCALL_FLAG_COL_IDX, USER_OP_HELPERS_OFFSET}; use crate::utils::{are_equal, is_binary}; use vm_core::{stack::STACK_TOP_SIZE, utils::collections::Vec, StackOutputs, StarkField}; @@ -33,7 +33,7 @@ pub const NUM_GENERAL_CONSTRAINTS: usize = 17; /// The degrees of constraints in the general stack operations. Each operation being executed /// either shifts the stack to the left, right or doesn't effect it at all. Therefore, majority -/// of the general transtitions of a stack item would be common across the operations and composite +/// of the general transitions of a stack item would be common across the operations and composite /// flags were introduced to compute the individual stack item transition. A particular item lets say /// at depth ith in the next stack frame can be transitioned into from ith depth (no shift op) or /// (i+1)th depth(left shift) or (i-1)th depth(right shift) in the current frame. Therefore, the VM @@ -357,6 +357,10 @@ trait EvaluationFrameExt { /// Returns the value if the `h6` helper register in the decoder which is set to ONE if the /// ending block is a `CALL` block. fn is_call_end(&self) -> E; + + /// Returns the value if the `h7` helper register in the decoder which is set to ONE if the + /// ending block is a `SYSCALL` block. + fn is_syscall_end(&self) -> E; } impl EvaluationFrameExt for &EvaluationFrame { @@ -423,4 +427,9 @@ impl EvaluationFrameExt for &EvaluationFrame { fn is_call_end(&self) -> E { self.current()[DECODER_TRACE_OFFSET + IS_CALL_FLAG_COL_IDX] } + + #[inline] + fn is_syscall_end(&self) -> E { + self.current()[DECODER_TRACE_OFFSET + IS_SYSCALL_FLAG_COL_IDX] + } } diff --git a/air/src/constraints/stack/overflow/mod.rs b/air/src/constraints/stack/overflow/mod.rs index d9b203144c..0761a93846 100644 --- a/air/src/constraints/stack/overflow/mod.rs +++ b/air/src/constraints/stack/overflow/mod.rs @@ -43,13 +43,13 @@ pub fn enforce_constraints( ) -> usize { let mut index = 0; - // Enforce constaints of the stack depth transition. + // Enforce constraints of the stack depth transition. index += enforce_stack_depth_constraints(frame, result, op_flag); - // Enforce constaints of the overflow flag constraints. + // Enforce constraints of the overflow flag constraints. index += enforce_overflow_flag_constraints(frame, &mut result[index..], op_flag); - // Enforce constaints of the stack bookeeping b1 item. + // Enforce constraints of the stack bookkeeping b1 item. index += enforce_overflow_index_constraints(frame, &mut result[index..], op_flag); index @@ -62,12 +62,13 @@ pub fn enforce_constraints( /// following constraints are enforced: /// - If the operation is a no shift op, then, depth wouldn't change. /// - If the operation is a right shift op, then, depth should increment by 1. -/// - If the operation is a left shift op, then, depth should be decresed by 1 provided the existing -/// depth of the stack is not 16. In the case of depth being 16, depth will not be updated. -/// - If the current op being executed is `CALL`, then, the depth should be reseted to 16. +/// - If the operation is a left shift op, then, depth should be decreased by 1 provided the +/// existing depth of the stack is not 16. In the case of depth being 16, depth will not be +/// updated. +/// - If the current op being executed is `CALL` or `SYSCALL`, then the depth should be reset to 16. /// -/// TODO- This skips the operation when `END` is exiting a `CALL` block. It should be handled later in -/// multiset constraints. +/// TODO: This skips the operation when `END` is exiting for a `CALL` or a `SYSCALL` block. It +/// should be handled later in multiset constraints. pub fn enforce_stack_depth_constraints( frame: &EvaluationFrame, result: &mut [E], @@ -75,13 +76,16 @@ pub fn enforce_stack_depth_constraints( ) -> usize { let depth = frame.stack_depth(); let depth_next = frame.stack_depth_next(); - let no_shift_part = - (depth_next - depth) * (E::ONE - op_flag.call() - (op_flag.end() * frame.is_call_end())); + + let call_or_syscall = op_flag.call() + op_flag.syscall(); + let call_or_syscall_end = op_flag.end() * (frame.is_call_end() + frame.is_syscall_end()); + + let no_shift_part = (depth_next - depth) * (E::ONE - call_or_syscall - call_or_syscall_end); let left_shift_part = op_flag.left_shift() * op_flag.overflow(); let right_shift_part = op_flag.right_shift(); - let call_part = op_flag.call() * (depth_next - E::from(16u32)); + let call_part = call_or_syscall * (depth_next - E::from(16u32)); - // Enforces constraints of the transtition of depth of the stack. + // Enforces constraints of the transition of depth of the stack. result[0] = no_shift_part + left_shift_part - right_shift_part + call_part; 1 @@ -116,11 +120,11 @@ pub fn enforce_overflow_index_constraints( let overflow_next = frame.stack_overflow_addr_next(); let last_stack_item_next = frame.stack_item_next(15); - // enforces that the bookeeping index b1 is set to the current clk value. + // enforces that the bookkeeping index b1 is set to the current clk value. result[0] = (overflow_next - frame.clk()) * op_flag.right_shift(); // enforces that the last stack item in the next frame has been updated with z ZERO when the - // depth of the stack is 16 and the current operatio being executed is a left shift op. + // depth of the stack is 16 and the current operation being executed is a left shift op. result[1] = (E::ONE - op_flag.overflow()) * op_flag.left_shift() * last_stack_item_next; 1