fill trace of Op Stack Table

triton-vm/src/table/op_stack_table.rs

@@ -1,25 +1,41 @@
+use std::cmp::Ordering;
+
 use itertools::Itertools;
+use ndarray::s;
+use ndarray::ArrayViewMut2;
 use num_traits::One;
 use strum::EnumCount;
-use strum_macros::{Display, EnumCount as EnumCountMacro, EnumIter};
+use strum_macros::Display;
+use strum_macros::EnumCount as EnumCountMacro;
+use strum_macros::EnumIter;
 use twenty_first::shared_math::b_field_element::BFieldElement;
 use twenty_first::shared_math::traits::Inverse;
 use twenty_first::shared_math::x_field_element::XFieldElement;
 
 use OpStackTableChallengeId::*;
 
-use crate::cross_table_arguments::{CrossTableArg, PermArg};
+use crate::cross_table_arguments::CrossTableArg;
+use crate::cross_table_arguments::PermArg;
+use crate::op_stack::OP_STACK_REG_COUNT;
+use crate::table::base_matrix::AlgebraicExecutionTrace;
 use crate::table::base_table::Extendable;
+use crate::table::base_table::InheritsFromTable;
+use crate::table::base_table::Table;
+use crate::table::base_table::TableLike;
+use crate::table::challenges::TableChallenges;
+use crate::table::constraint_circuit::ConstraintCircuit;
+use crate::table::constraint_circuit::ConstraintCircuitBuilder;
+use crate::table::constraint_circuit::DualRowIndicator;
+use crate::table::constraint_circuit::DualRowIndicator::*;
 use crate::table::constraint_circuit::SingleRowIndicator;
 use crate::table::constraint_circuit::SingleRowIndicator::Row;
-use crate::table::table_column::OpStackBaseTableColumn::{self, *};
-use crate::table::table_column::OpStackExtTableColumn::{self, *};
-
-use super::base_table::{InheritsFromTable, Table, TableLike};
-use super::challenges::TableChallenges;
-use super::constraint_circuit::DualRowIndicator::*;
-use super::constraint_circuit::{ConstraintCircuit, ConstraintCircuitBuilder, DualRowIndicator};
-use super::extension_table::{ExtensionTable, QuotientableExtensionTable};
+use crate::table::extension_table::ExtensionTable;
+use crate::table::extension_table::QuotientableExtensionTable;
+use crate::table::table_column::OpStackBaseTableColumn;
+use crate::table::table_column::OpStackBaseTableColumn::*;
+use crate::table::table_column::OpStackExtTableColumn;
+use crate::table::table_column::OpStackExtTableColumn::*;
+use crate::table::table_column::ProcessorBaseTableColumn;
 
 pub const OP_STACK_TABLE_NUM_PERMUTATION_ARGUMENTS: usize = 1;
 pub const OP_STACK_TABLE_NUM_EVALUATION_ARGUMENTS: usize = 0;
@@ -273,6 +289,55 @@ impl OpStackTable {
         Self { inherited_table }
     }
 
+    pub fn fill_trace(
+        op_stack_table: &mut ArrayViewMut2<BFieldElement>,
+        aet: &AlgebraicExecutionTrace,
+    ) {
+        // Store the registers relevant for the Op Stack Table, i.e., CLK, IB1, OSP, and OSV,
+        // with OSP as the key. Preserves, thus allows reusing, the order of the processor's
+        // rows, which are sorted by CLK.
+        let mut pre_processed_op_stack_table: Vec<Vec<_>> = vec![];
+        for processor_row in aet.processor_matrix.iter() {
+            let osp = processor_row[usize::from(ProcessorBaseTableColumn::OSP)];
+            let clk = processor_row[usize::from(ProcessorBaseTableColumn::CLK)];
+            let ib1 = processor_row[usize::from(ProcessorBaseTableColumn::IB1)];
+            let osv = processor_row[usize::from(ProcessorBaseTableColumn::OSV)];
+            // The (honest) prover can only grow the Op Stack's size by at most 1 per execution
+            // step. Hence, the following (a) works, and (b) sorts.
+            let osp_minus_16 = osp.value() as usize - OP_STACK_REG_COUNT;
+            match osp_minus_16.cmp(&pre_processed_op_stack_table.len()) {
+                Ordering::Less => pre_processed_op_stack_table[osp_minus_16].push((clk, ib1, osv)),
+                Ordering::Equal => pre_processed_op_stack_table.push(vec![(clk, ib1, osv)]),
+                Ordering::Greater => panic!("OSP must increase by at most 1 per execution step."),
+            }
+        }
+
+        // Move the rows into the Op Stack Table, sorted by OSP first, CLK second.
+        let mut op_stack_table_row = 0;
+        for (osp_minus_16, rows_with_this_osp) in
+            pre_processed_op_stack_table.into_iter().enumerate()
+        {
+            let osp = BFieldElement::new((osp_minus_16 + OP_STACK_REG_COUNT) as u64);
+            for (clk, ib1, osv) in rows_with_this_osp {
+                op_stack_table[(op_stack_table_row, usize::from(OSP))] = osp;
+                op_stack_table[(op_stack_table_row, usize::from(CLK))] = clk;
+                op_stack_table[(op_stack_table_row, usize::from(IB1ShrinkStack))] = ib1;
+                op_stack_table[(op_stack_table_row, usize::from(OSV))] = osv;
+                op_stack_table_row += 1;
+            }
+        }
+
+        // Set inverse of (clock difference - 1).
+        for op_stack_table_row in 0..op_stack_table.nrows() - 1 {
+            let (mut curr_row, next_row) = op_stack_table
+                .multi_slice_mut((s![op_stack_table_row, ..], s![op_stack_table_row + 1, ..]));
+            let clk_diff = next_row[usize::from(CLK)] - curr_row[usize::from(CLK)];
+            let clk_diff_minus_1 = clk_diff - BFieldElement::one();
+            let clk_diff_minus_1_inverse = clk_diff_minus_1.inverse_or_zero();
+            curr_row[usize::from(InverseOfClkDiffMinusOne)] = clk_diff_minus_1_inverse;
+        }
+    }
+
     pub fn extend(&self, challenges: &OpStackTableChallenges) -> ExtOpStackTable {
         let mut extension_matrix: Vec<Vec<XFieldElement>> = Vec::with_capacity(self.data().len());
         let mut running_product = PermArg::default_initial();

triton-vm/src/table/table_collection.rs

@@ -343,6 +343,8 @@ impl MasterBaseTable {
         ProgramTable::fill_trace(program_table, program);
         let instruction_table = &mut master_base_table.table_mut(TableId::InstructionTable);
         InstructionTable::fill_trace(instruction_table, &aet, program);
+        let op_stack_table = &mut master_base_table.table_mut(TableId::OpStackTable);
+        OpStackTable::fill_trace(op_stack_table, &aet);
 
         master_base_table
     }