refactor: restrict the number of stack inputs and outputs to 16 (#1456)

CHANGELOG.md

@@ -74,6 +74,7 @@
 
 - [BREAKING] Replaced `SourceManager` parameter with `Assembler` in `Library::from_dir` (#1445).
 - [BREAKING] Moved `Library` and `KernelLibrary` exports to the root of the `miden-assembly` crate. (#1445).
+- [BREAKING] Depth of the input and output stack was restricted to 16 (#1456).
 
 ## 0.10.2 (2024-08-10)
 

air/src/constraints/stack/mod.rs

@@ -1,6 +1,6 @@
 use alloc::vec::Vec;
 
-use vm_core::{stack::STACK_TOP_SIZE, StackOutputs};
+use vm_core::{stack::MIN_STACK_DEPTH, StackOutputs};
 
 use super::super::{
     Assertion, EvaluationFrame, Felt, FieldElement, TransitionConstraintDegree, CLK_COL_IDX,
@@ -22,15 +22,15 @@ pub mod u32_ops;
 // CONSTANTS
 // ================================================================================================
 
-const B0_COL_IDX: usize = STACK_TRACE_OFFSET + STACK_TOP_SIZE;
+const B0_COL_IDX: usize = STACK_TRACE_OFFSET + MIN_STACK_DEPTH;
 const B1_COL_IDX: usize = B0_COL_IDX + 1;
 const H0_COL_IDX: usize = B1_COL_IDX + 1;
 
 // --- Main constraints ---------------------------------------------------------------------------
 
 /// The number of boundary constraints required by the Stack, which is all stack positions for
 /// inputs and outputs as well as the initial values of the bookkeeping columns.
-pub const NUM_ASSERTIONS: usize = 2 * STACK_TOP_SIZE + 2;
+pub const NUM_ASSERTIONS: usize = 2 * MIN_STACK_DEPTH + 2;
 
 /// The number of general constraints in the stack operations.
 pub const NUM_GENERAL_CONSTRAINTS: usize = 17;
@@ -193,19 +193,19 @@ pub fn enforce_general_constraints<E: FieldElement>(
 /// Returns the stack's boundary assertions for the main trace at the first step.
 pub fn get_assertions_first_step(result: &mut Vec<Assertion<Felt>>, stack_inputs: &[Felt]) {
     // stack columns at the first step should be set to stack inputs, excluding overflow inputs.
-    for (i, &value) in stack_inputs.iter().take(STACK_TOP_SIZE).enumerate() {
+    for (i, &value) in stack_inputs.iter().take(MIN_STACK_DEPTH).enumerate() {
         result.push(Assertion::single(STACK_TRACE_OFFSET + i, 0, value));
     }
 
     // if there are remaining slots on top of the stack without specified values, set them to ZERO.
-    for i in stack_inputs.len()..STACK_TOP_SIZE {
+    for i in stack_inputs.len()..MIN_STACK_DEPTH {
         result.push(Assertion::single(STACK_TRACE_OFFSET + i, 0, ZERO));
     }
 
     // get the initial values for the bookkeeping columns.
-    let mut depth = STACK_TOP_SIZE;
+    let mut depth = MIN_STACK_DEPTH;
     let mut overflow_addr = ZERO;
-    if stack_inputs.len() > STACK_TOP_SIZE {
+    if stack_inputs.len() > MIN_STACK_DEPTH {
         depth = stack_inputs.len();
         overflow_addr = -ONE;
     }
@@ -225,100 +225,27 @@ pub fn get_assertions_last_step(
     stack_outputs: &StackOutputs,
 ) {
     // stack columns at the last step should be set to stack outputs, excluding overflow outputs
-    for (i, value) in stack_outputs.stack_top().iter().enumerate() {
+    for (i, value) in stack_outputs.iter().enumerate() {
         result.push(Assertion::single(STACK_TRACE_OFFSET + i, step, *value));
     }
 }
 
 // --- AUXILIARY COLUMNS --------------------------------------------------------------------------
 
 /// Returns the stack's boundary assertions for auxiliary columns at the first step.
-pub fn get_aux_assertions_first_step<E>(
-    result: &mut Vec<Assertion<E>>,
-    alphas: &[E],
-    stack_inputs: &[Felt],
-) where
-    E: FieldElement<BaseField = Felt>,
-{
-    let step = 0;
-    let value = if stack_inputs.len() > STACK_TOP_SIZE {
-        get_overflow_table_init(alphas, &stack_inputs[STACK_TOP_SIZE..])
-    } else {
-        E::ONE
-    };
-
-    result.push(Assertion::single(STACK_AUX_TRACE_OFFSET, step, value));
-}
-
-/// Returns the stack's boundary assertions for auxiliary columns at the last step.
-pub fn get_aux_assertions_last_step<E>(
-    result: &mut Vec<Assertion<E>>,
-    alphas: &[E],
-    stack_outputs: &StackOutputs,
-    step: usize,
-) where
-    E: FieldElement<BaseField = Felt>,
-{
-    let value = if stack_outputs.has_overflow() {
-        get_overflow_table_final(alphas, stack_outputs)
-    } else {
-        E::ONE
-    };
-
-    result.push(Assertion::single(STACK_AUX_TRACE_OFFSET, step, value));
-}
-
-// BOUNDARY CONSTRAINT HELPERS
-// ================================================================================================
-
-// --- AUX TRACE ----------------------------------------------------------------------------------
-
-/// Gets the initial value of the overflow table auxiliary column from the provided sets of initial
-/// values and random elements.
-fn get_overflow_table_init<E>(alphas: &[E], init_values: &[Felt]) -> E
+pub fn get_aux_assertions_first_step<E>(result: &mut Vec<Assertion<E>>)
 where
     E: FieldElement<BaseField = Felt>,
 {
-    let mut value = E::ONE;
-    let mut prev_clk = ZERO;
-    let mut clk = -Felt::from(init_values.len() as u32);
-
-    // the values are in the overflow table in reverse order, since the deepest stack
-    // value is added to the overflow table first.
-    for &input in init_values.iter().rev() {
-        value *= alphas[0]
-            + alphas[1].mul_base(clk)
-            + alphas[2].mul_base(input)
-            + alphas[3].mul_base(prev_clk);
-        prev_clk = clk;
-        clk += ONE;
-    }
-
-    value
+    result.push(Assertion::single(STACK_AUX_TRACE_OFFSET, 0, E::ONE));
 }
 
-/// Gets the final value of the overflow table auxiliary column from the provided program outputs
-/// and random elements.
-fn get_overflow_table_final<E>(alphas: &[E], stack_outputs: &StackOutputs) -> E
+/// Returns the stack's boundary assertions for auxiliary columns at the last step.
+pub fn get_aux_assertions_last_step<E>(result: &mut Vec<Assertion<E>>, step: usize)
 where
     E: FieldElement<BaseField = Felt>,
 {
-    let mut value = E::ONE;
-
-    // When the overflow table is non-empty, we expect at least 2 addresses (the `prev` value of
-    // the first row and the address value(s) of the row(s)) and more than STACK_TOP_SIZE
-    // elements in the stack.
-    let mut prev = stack_outputs.overflow_prev();
-    for (clk, val) in stack_outputs.stack_overflow() {
-        value *= alphas[0]
-            + alphas[1].mul_base(clk)
-            + alphas[2].mul_base(val)
-            + alphas[3].mul_base(prev);
-
-        prev = clk;
-    }
-
-    value
+    result.push(Assertion::single(STACK_AUX_TRACE_OFFSET, step, E::ONE));
 }
 
 // STACK OPERATION EXTENSION TRAIT

air/src/lib.rs

@@ -146,7 +146,7 @@ impl Air for ProcessorAir {
         result.push(Assertion::single(FMP_COL_IDX, 0, Felt::new(2u64.pow(30))));
 
         // add initial assertions for the stack.
-        stack::get_assertions_first_step(&mut result, self.stack_inputs.values());
+        stack::get_assertions_first_step(&mut result, &*self.stack_inputs);
 
         // Add initial assertions for the range checker.
         range::get_assertions_first_step(&mut result);
@@ -165,18 +165,14 @@ impl Air for ProcessorAir {
 
     fn get_aux_assertions<E: FieldElement<BaseField = Self::BaseField>>(
         &self,
-        aux_rand_elements: &[E],
+        _aux_rand_elements: &[E],
     ) -> Vec<Assertion<E>> {
         let mut result: Vec<Assertion<E>> = Vec::new();
 
         // --- set assertions for the first step --------------------------------------------------
 
         // add initial assertions for the stack's auxiliary columns.
-        stack::get_aux_assertions_first_step(
-            &mut result,
-            aux_rand_elements,
-            self.stack_inputs.values(),
-        );
+        stack::get_aux_assertions_first_step(&mut result);
 
         // Add initial assertions for the range checker's auxiliary columns.
         range::get_aux_assertions_first_step::<E>(&mut result);
@@ -185,12 +181,7 @@ impl Air for ProcessorAir {
         let last_step = self.last_step();
 
         // add the stack's auxiliary column assertions for the last step.
-        stack::get_aux_assertions_last_step(
-            &mut result,
-            aux_rand_elements,
-            &self.stack_outputs,
-            last_step,
-        );
+        stack::get_aux_assertions_last_step(&mut result, last_step);
 
         // Add the range checker's auxiliary column assertions for the last step.
         range::get_aux_assertions_last_step::<E>(&mut result, last_step);
@@ -281,8 +272,8 @@ impl PublicInputs {
 impl vm_core::ToElements<Felt> for PublicInputs {
     fn to_elements(&self) -> Vec<Felt> {
         let mut result = self.program_info.to_elements();
-        result.append(&mut self.stack_inputs.to_elements());
-        result.append(&mut self.stack_outputs.to_elements());
+        result.append(&mut self.stack_inputs.to_vec());
+        result.append(&mut self.stack_outputs.to_vec());
         result
     }
 }

air/src/trace/stack/mod.rs

@@ -1,19 +1,15 @@
 use core::ops::Range;
 
-use vm_core::utils::range;
+use vm_core::{stack::MIN_STACK_DEPTH, utils::range};
 
 // CONSTANTS
 // ================================================================================================
 
 /// Index at which stack item columns start in the stack trace.
 pub const STACK_TOP_OFFSET: usize = 0;
 
-/// The number of stack registers which can be accessed by the VM directly. This is also the
-/// minimum stack depth enforced by the VM.
-pub const STACK_TOP_SIZE: usize = 16;
-
 /// Location of stack top items in the stack trace.
-pub const STACK_TOP_RANGE: Range<usize> = range(STACK_TOP_OFFSET, STACK_TOP_SIZE);
+pub const STACK_TOP_RANGE: Range<usize> = range(STACK_TOP_OFFSET, MIN_STACK_DEPTH);
 
 /// Number of bookkeeping and helper columns in the stack trace.
 pub const NUM_STACK_HELPER_COLS: usize = 3;

core/src/lib.rs

@@ -124,8 +124,3 @@ pub mod stack;
 pub use stack::{StackInputs, StackOutputs};
 
 pub mod utils;
-
-// TYPE ALIASES
-// ================================================================================================
-
-pub type StackTopState = [Felt; stack::STACK_TOP_SIZE];