feat: record opstack underflow read/write in AET

triton-vm/src/aet.rs

@@ -23,13 +23,13 @@ use crate::error::InstructionError::InstructionPointerOverflow;
 use crate::instruction::Instruction;
 use crate::program::Program;
 use crate::stark::StarkHasher;
-use crate::table::hash_table;
 use crate::table::hash_table::HashTable;
 use crate::table::hash_table::PermutationTrace;
-use crate::table::processor_table;
+use crate::table::op_stack_table::OpStackTableEntry;
 use crate::table::table_column::HashBaseTableColumn::CI;
 use crate::table::table_column::MasterBaseTableColumn;
 use crate::table::u32_table::U32TableEntry;
+use crate::table::*;
 use crate::vm::CoProcessorCall;
 use crate::vm::CoProcessorCall::*;
 use crate::vm::VMState;
@@ -53,6 +53,8 @@ pub struct AlgebraicExecutionTrace {
     /// Records the state of the processor after each instruction.
     pub processor_trace: Array2<BFieldElement>,
 
+    pub op_stack_underflow_trace: Array2<BFieldElement>,
+
     /// The trace of hashing the program whose execution generated this `AlgebraicExecutionTrace`.
     /// The resulting digest
     /// 1. ties a [`Proof`](crate::proof::Proof) to the program it was produced from, and
@@ -87,6 +89,7 @@ impl AlgebraicExecutionTrace {
             program,
             instruction_multiplicities: vec![0_u32; program_len],
             processor_trace: Array2::default([0, processor_table::BASE_WIDTH]),
+            op_stack_underflow_trace: Array2::default([0, op_stack_table::BASE_WIDTH]),
             program_hash_trace: Array2::default([0, hash_table::BASE_WIDTH]),
             hash_trace: Array2::default([0, hash_table::BASE_WIDTH]),
             sponge_trace: Array2::default([0, hash_table::BASE_WIDTH]),
@@ -177,6 +180,10 @@ impl AlgebraicExecutionTrace {
         self.processor_trace.nrows()
     }
 
+    pub fn op_stack_table_length(&self) -> usize {
+        self.op_stack_underflow_trace.nrows()
+    }
+
     pub fn hash_table_length(&self) -> usize {
         self.sponge_trace.nrows() + self.hash_trace.nrows() + self.program_hash_trace.nrows()
     }
@@ -223,7 +230,7 @@ impl AlgebraicExecutionTrace {
             SpongeStateReset => self.append_initial_sponge_state(),
             Tip5Trace(instruction, trace) => self.append_sponge_trace(instruction, *trace),
             U32Call(u32_entry) => self.record_u32_table_entry(u32_entry),
-            OpStackCall(_) => (), // todo
+            OpStackCall(op_stack_entry) => self.record_op_stack_entry(op_stack_entry),
         }
     }
 
@@ -307,6 +314,13 @@ impl AlgebraicExecutionTrace {
     fn record_u32_table_entry(&mut self, u32_entry: U32TableEntry) {
         self.u32_entries.entry(u32_entry).or_insert(0).add_assign(1)
     }
+
+    fn record_op_stack_entry(&mut self, op_stack_entry: OpStackTableEntry) {
+        let op_stack_table_row = op_stack_entry.to_base_table_row();
+        self.op_stack_underflow_trace
+            .push_row(op_stack_table_row.view())
+            .unwrap();
+    }
 }
 
 #[cfg(test)]

triton-vm/src/op_stack.rs

@@ -195,6 +195,13 @@ impl UnderflowIO {
             Self::Write(_) => true,
         }
     }
+
+    pub fn payload(self) -> BFieldElement {
+        match self {
+            Self::Read(payload) => payload,
+            Self::Write(payload) => payload,
+        }
+    }
 }
 
 /// Represents the [`OpStack`] registers directly accessible by Triton VM.

triton-vm/src/table/master_table.rs

@@ -146,6 +146,8 @@ pub const EXT_DEGREE_LOWERING_TABLE_START: usize = EXT_U32_TABLE_END;
 pub const EXT_DEGREE_LOWERING_TABLE_END: usize =
     EXT_DEGREE_LOWERING_TABLE_START + degree_lowering_table::EXT_WIDTH;
 
+const NUM_TABLES_WITHOUT_DEGREE_LOWERING: usize = TableId::COUNT - 1;
+
 /// A `TableId` uniquely determines one of Triton VM's tables.
 #[derive(Debug, Copy, Clone, Display, EnumCount, EnumIter, PartialEq, Eq, Hash)]
 pub enum TableId {
@@ -327,6 +329,7 @@ pub struct MasterBaseTable {
 
     program_table_len: usize,
     main_execution_len: usize,
+    op_stack_table_len: usize,
     hash_coprocessor_execution_len: usize,
     cascade_table_len: usize,
     u32_coprocesor_execution_len: usize,
@@ -587,6 +590,7 @@ impl MasterBaseTable {
             num_trace_randomizers,
             program_table_len: aet.program_table_length(),
             main_execution_len: aet.processor_table_length(),
+            op_stack_table_len: aet.op_stack_table_length(),
             hash_coprocessor_execution_len: aet.hash_table_length(),
             cascade_table_len: aet.cascade_table_length(),
             u32_coprocesor_execution_len: aet.u32_table_length(),
@@ -705,7 +709,7 @@ impl MasterBaseTable {
         DegreeLoweringTable::fill_derived_base_columns(self.trace_table_mut());
     }
 
-    fn all_pad_functions() -> [PadFunction; TableId::COUNT - 1] {
+    fn all_pad_functions() -> [PadFunction; NUM_TABLES_WITHOUT_DEGREE_LOWERING] {
         [
             ProgramTable::pad_trace,
             ProcessorTable::pad_trace,
@@ -719,13 +723,17 @@ impl MasterBaseTable {
         ]
     }
 
-    fn all_table_lengths(&self) -> [usize; TableId::COUNT - 1] {
+    fn all_table_lengths(&self) -> [usize; NUM_TABLES_WITHOUT_DEGREE_LOWERING] {
+        let processor_table_len = self.main_execution_len;
+        let ram_table_len = self.main_execution_len;
+        let jump_stack_table_len = self.main_execution_len;
+
         [
             self.program_table_len,
+            processor_table_len,
             self.main_execution_len,
-            self.main_execution_len,
-            self.main_execution_len,
-            self.main_execution_len,
+            ram_table_len,
+            jump_stack_table_len,
             self.hash_coprocessor_execution_len,
             self.cascade_table_len,
             1 << 8,
@@ -830,7 +838,7 @@ impl MasterBaseTable {
         master_ext_table
     }
 
-    fn all_extend_functions() -> [ExtendFunction; TableId::COUNT - 1] {
+    fn all_extend_functions() -> [ExtendFunction; NUM_TABLES_WITHOUT_DEGREE_LOWERING] {
         [
             ProgramTable::extend,
             ProcessorTable::extend,
@@ -844,7 +852,9 @@ impl MasterBaseTable {
         ]
     }
 
-    fn base_tables_for_extending(&self) -> [ArrayView2<BFieldElement>; TableId::COUNT - 1] {
+    fn base_tables_for_extending(
+        &self,
+    ) -> [ArrayView2<BFieldElement>; NUM_TABLES_WITHOUT_DEGREE_LOWERING] {
         [
             self.table(TableId::ProgramTable),
             self.table(TableId::ProcessorTable),

triton-vm/src/table/op_stack_table.rs

@@ -8,6 +8,8 @@ use ndarray::ArrayView1;
 use ndarray::ArrayView2;
 use ndarray::ArrayViewMut2;
 use ndarray::Axis;
+use num_traits::One;
+use num_traits::Zero;
 use strum::EnumCount;
 use twenty_first::shared_math::b_field_element::BFieldElement;
 use twenty_first::shared_math::traits::Inverse;
@@ -79,6 +81,20 @@ impl OpStackTableEntry {
         }
         op_stack_table_entries
     }
+
+    pub fn to_base_table_row(self) -> Array1<BFieldElement> {
+        let shrink_stack_indicator = match self.shrinks_stack() {
+            true => BFieldElement::one(),
+            false => BFieldElement::zero(),
+        };
+
+        let mut row = Array1::zeros(BASE_WIDTH);
+        row[CLK.base_table_index()] = self.clk.into();
+        row[IB1ShrinkStack.base_table_index()] = shrink_stack_indicator;
+        row[OSP.base_table_index()] = self.op_stack_pointer;
+        row[OSV.base_table_index()] = self.underflow_io.payload();
+        row
+    }
 }
 
 impl ExtOpStackTable {