refactor: limit input and output stack to 16 elements

air/src/constraints/stack/mod.rs

@@ -223,100 +223,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.stack().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

@@ -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);

core/src/stack/inputs.rs

@@ -1,7 +1,7 @@
 use alloc::vec::Vec;
 use core::slice;
 
-use super::{ByteWriter, Felt, InputError, Serializable, ToElements};
+use super::{super::ZERO, ByteWriter, Felt, InputError, Serializable, ToElements, STACK_DEPTH};
 use crate::utils::{ByteReader, Deserializable, DeserializationError};
 
 // STACK INPUTS
@@ -13,15 +13,10 @@ use crate::utils::{ByteReader, Deserializable, DeserializationError};
 /// reversed order on this struct.
 #[derive(Clone, Debug, Default)]
 pub struct StackInputs {
-    values: Vec<Felt>,
+    values: [Felt; STACK_DEPTH],
 }
 
 impl StackInputs {
-    // CONSTANTS
-    // --------------------------------------------------------------------------------------------
-
-    pub const MAX_LEN: usize = u16::MAX as usize;
-
     // CONSTRUCTORS
     // --------------------------------------------------------------------------------------------
 
@@ -30,12 +25,15 @@ impl StackInputs {
     /// # Errors
     /// Returns an error if the number of input values exceeds the allowed maximum.
     pub fn new(mut values: Vec<Felt>) -> Result<Self, InputError> {
-        if values.len() > Self::MAX_LEN {
-            return Err(InputError::InputLengthExceeded(Self::MAX_LEN, values.len()));
+        if values.len() > STACK_DEPTH {
+            return Err(InputError::InputLengthExceeded(STACK_DEPTH, values.len()));
         }
         values.reverse();
 
-        Ok(Self { values })
+        let mut values_arr = [ZERO; STACK_DEPTH];
+        values.iter().enumerate().for_each(|(i, v)| values_arr[i] = *v);
+
+        Ok(Self { values: values_arr })
     }
 
     /// Attempts to create stack inputs from an iterator of integers.
@@ -76,7 +74,7 @@ impl<'a> IntoIterator for &'a StackInputs {
 
 impl IntoIterator for StackInputs {
     type Item = Felt;
-    type IntoIter = alloc::vec::IntoIter<Felt>;
+    type IntoIter = core::array::IntoIter<Felt, 16>;
 
     fn into_iter(self) -> Self::IntoIter {
         self.values.into_iter()
@@ -94,27 +92,17 @@ impl ToElements<Felt> for StackInputs {
 
 impl Serializable for StackInputs {
     fn write_into<W: ByteWriter>(&self, target: &mut W) {
-        // TODO the length of the stack, by design, will not be greater than `u32::MAX`. however,
-        // we must define a common serialization format as we might diverge from the implementation
-        // here and the one provided by default from winterfell.
-
-        debug_assert!(self.values.len() <= Self::MAX_LEN);
-        target.write_usize(self.values.len());
-        target.write_many(&self.values);
+        debug_assert!(self.values.len() == STACK_DEPTH);
+        target.write_many(self.values);
     }
 }
 
 impl Deserializable for StackInputs {
     fn read_from<R: ByteReader>(source: &mut R) -> Result<Self, DeserializationError> {
-        let count = source.read_usize()?;
-        if count > Self::MAX_LEN {
-            return Err(DeserializationError::InvalidValue(format!(
-                "Number of values on the input stack can not be more than {}, but {} was found",
-                Self::MAX_LEN,
-                count
-            )));
-        }
-        let values = source.read_many::<Felt>(count)?;
+        let values = source
+            .read_many::<Felt>(STACK_DEPTH)?
+            .try_into()
+            .expect("Invalid input stack depth: expected 16");
         Ok(StackInputs { values })
     }
 }

core/src/stack/mod.rs

@@ -1,6 +1,6 @@
 use super::{
     errors::{InputError, OutputError},
-    Felt, StackTopState, ToElements,
+    Felt, ToElements,
 };
 use crate::utils::{ByteWriter, Serializable};
 
@@ -16,3 +16,6 @@ pub use outputs::StackOutputs;
 /// 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;
+
+/// Maximum number of elements allowed for the input and output stack.
+pub const STACK_DEPTH: usize = 16;