Skip to content

Commit

Permalink
Merge pull request #1008 from 0xPolygonMiden/bobbin-fix-syscall-const…
Browse files Browse the repository at this point in the history
…raint

fix: stack depth constraint for syscall operation
  • Loading branch information
bobbinth authored Jul 18, 2023
2 parents 9155e63 + 18a1295 commit 602d185
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 16 deletions.
13 changes: 11 additions & 2 deletions air/src/constraints/stack/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -357,6 +357,10 @@ trait EvaluationFrameExt<E: FieldElement> {
/// 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<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
Expand Down Expand Up @@ -423,4 +427,9 @@ impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
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]
}
}
32 changes: 18 additions & 14 deletions air/src/constraints/stack/overflow/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,13 +43,13 @@ pub fn enforce_constraints<E: FieldElement>(
) -> 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
Expand All @@ -62,26 +62,30 @@ pub fn enforce_constraints<E: FieldElement>(
/// 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<E: FieldElement>(
frame: &EvaluationFrame<E>,
result: &mut [E],
op_flag: &OpFlags<E>,
) -> 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
Expand Down Expand Up @@ -116,11 +120,11 @@ pub fn enforce_overflow_index_constraints<E: FieldElement>(
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
Expand Down

0 comments on commit 602d185

Please sign in to comment.