Replace individual cross-table arguments by Grand Cross-Table Argument

Remove explicit terminal values, which fixes #52.

triton-vm/src/cross_table_arguments.rs

@@ -19,6 +19,7 @@ use crate::table::table_column::{
 pub const NUM_PRIVATE_PERM_ARGS: usize = PROCESSOR_TABLE_PERMUTATION_ARGUMENTS_COUNT;
 pub const NUM_PRIVATE_EVAL_ARGS: usize = 3;
 pub const NUM_CROSS_TABLE_ARGS: usize = NUM_PRIVATE_PERM_ARGS + NUM_PRIVATE_EVAL_ARGS;
+pub const NUM_PUBLIC_EVAL_ARGS: usize = 2;
 
 pub trait CrossTableArg {
     fn from(&self) -> (TableId, usize);
@@ -277,60 +278,277 @@ impl EvalArg {
     }
 }
 
-pub struct AllCrossTableArgs {
-    processor_instruction_perm_arg: PermArg,
-    processor_jump_stack_perm_arg: PermArg,
-    processor_op_stack_perm_arg: PermArg,
-    processor_ram_perm_arg: PermArg,
-    processor_u32_perm_arg: PermArg,
-    program_instruction_eval_arg: EvalArg,
-    processor_to_hash_eval_arg: EvalArg,
-    hash_to_processor_eval_arg: EvalArg,
-}
-
-impl Default for AllCrossTableArgs {
-    fn default() -> Self {
-        Self {
-            processor_instruction_perm_arg: PermArg::processor_instruction_perm_arg(),
-            processor_jump_stack_perm_arg: PermArg::processor_jump_stack_perm_arg(),
-            processor_op_stack_perm_arg: PermArg::processor_op_stack_perm_arg(),
-            processor_ram_perm_arg: PermArg::processor_ram_perm_arg(),
-            processor_u32_perm_arg: PermArg::processor_u32_perm_arg(),
-            program_instruction_eval_arg: EvalArg::program_instruction_eval_arg(),
-            processor_to_hash_eval_arg: EvalArg::processor_to_hash_eval_arg(),
-            hash_to_processor_eval_arg: EvalArg::hash_to_processor_eval_arg(),
-        }
-    }
+#[derive(Debug, Copy, Clone, Eq, PartialEq)]
+pub struct GrandCrossTableArg {
+    program_to_instruction: EvalArg,
+    processor_to_instruction: PermArg,
+    processor_to_op_stack: PermArg,
+    processor_to_ram: PermArg,
+    processor_to_jump_stack: PermArg,
+    processor_to_hash: EvalArg,
+    hash_to_processor: EvalArg,
+    processor_to_u32: PermArg,
+
+    program_to_instruction_weight: XFieldElement,
+    processor_to_instruction_weight: XFieldElement,
+    processor_to_op_stack_weight: XFieldElement,
+    processor_to_ram_weight: XFieldElement,
+    processor_to_jump_stack_weight: XFieldElement,
+    processor_to_hash_weight: XFieldElement,
+    hash_to_processor_weight: XFieldElement,
+    processor_to_u32_weight: XFieldElement,
+
+    input_terminal: XFieldElement,
+    input_to_processor: (TableId, usize),
+    input_to_processor_weight: XFieldElement,
+
+    output_terminal: XFieldElement,
+    processor_to_output: (TableId, usize),
+    processor_to_output_weight: XFieldElement,
 }
 
-impl<'a> IntoIterator for &'a AllCrossTableArgs {
-    type Item = &'a dyn CrossTableArg;
+impl<'a> IntoIterator for &'a GrandCrossTableArg {
+    type Item = (&'a dyn CrossTableArg, XFieldElement);
 
-    type IntoIter = std::array::IntoIter<&'a dyn CrossTableArg, NUM_CROSS_TABLE_ARGS>;
+    type IntoIter =
+        std::array::IntoIter<(&'a dyn CrossTableArg, XFieldElement), NUM_CROSS_TABLE_ARGS>;
 
     fn into_iter(self) -> Self::IntoIter {
         [
-            &self.processor_instruction_perm_arg as &'a dyn CrossTableArg,
-            &self.processor_jump_stack_perm_arg as &'a dyn CrossTableArg,
-            &self.processor_op_stack_perm_arg as &'a dyn CrossTableArg,
-            &self.processor_ram_perm_arg as &'a dyn CrossTableArg,
-            &self.processor_u32_perm_arg as &'a dyn CrossTableArg,
-            &self.program_instruction_eval_arg as &'a dyn CrossTableArg,
-            &self.processor_to_hash_eval_arg as &'a dyn CrossTableArg,
-            &self.hash_to_processor_eval_arg as &'a dyn CrossTableArg,
+            (
+                &self.program_to_instruction as &'a dyn CrossTableArg,
+                self.program_to_instruction_weight,
+            ),
+            (
+                &self.processor_to_instruction as &'a dyn CrossTableArg,
+                self.processor_to_instruction_weight,
+            ),
+            (
+                &self.processor_to_op_stack as &'a dyn CrossTableArg,
+                self.processor_to_op_stack_weight,
+            ),
+            (
+                &self.processor_to_ram as &'a dyn CrossTableArg,
+                self.processor_to_ram_weight,
+            ),
+            (
+                &self.processor_to_jump_stack as &'a dyn CrossTableArg,
+                self.processor_to_jump_stack_weight,
+            ),
+            (
+                &self.processor_to_hash as &'a dyn CrossTableArg,
+                self.processor_to_hash_weight,
+            ),
+            (
+                &self.hash_to_processor as &'a dyn CrossTableArg,
+                self.hash_to_processor_weight,
+            ),
+            (
+                &self.processor_to_u32 as &'a dyn CrossTableArg,
+                self.processor_to_u32_weight,
+            ),
         ]
         .into_iter()
     }
 }
 
+impl GrandCrossTableArg {
+    pub fn new(
+        weights: &[XFieldElement; NUM_CROSS_TABLE_ARGS + NUM_PUBLIC_EVAL_ARGS],
+        input_terminal: XFieldElement,
+        output_terminal: XFieldElement,
+    ) -> Self {
+        Self {
+            program_to_instruction: EvalArg::program_instruction_eval_arg(),
+            processor_to_instruction: PermArg::processor_instruction_perm_arg(),
+            processor_to_op_stack: PermArg::processor_op_stack_perm_arg(),
+            processor_to_ram: PermArg::processor_ram_perm_arg(),
+            processor_to_jump_stack: PermArg::processor_jump_stack_perm_arg(),
+            processor_to_hash: EvalArg::processor_to_hash_eval_arg(),
+            hash_to_processor: EvalArg::hash_to_processor_eval_arg(),
+            processor_to_u32: PermArg::processor_u32_perm_arg(),
+
+            program_to_instruction_weight: weights[0],
+            processor_to_instruction_weight: weights[1],
+            processor_to_op_stack_weight: weights[2],
+            processor_to_ram_weight: weights[3],
+            processor_to_jump_stack_weight: weights[4],
+            processor_to_hash_weight: weights[5],
+            hash_to_processor_weight: weights[6],
+            processor_to_u32_weight: weights[7],
+
+            input_terminal,
+            input_to_processor: (
+                TableId::ProcessorTable,
+                usize::from(ExtProcessorTableColumn::InputTableEvalArg),
+            ),
+            input_to_processor_weight: weights[8],
+
+            output_terminal,
+            processor_to_output: (
+                TableId::ProcessorTable,
+                usize::from(ExtProcessorTableColumn::OutputTableEvalArg),
+            ),
+            processor_to_output_weight: weights[9],
+        }
+    }
+
+    pub fn terminal_quotient_codeword(
+        &self,
+        ext_codeword_tables: &ExtTableCollection,
+        fri_domain: &FriDomain<XFieldElement>,
+        omicron: XFieldElement,
+    ) -> Vec<XFieldElement> {
+        let mut non_linear_sum_codeword = vec![XFieldElement::zero(); fri_domain.length];
+
+        // cross-table arguments
+        for (arg, weight) in self.into_iter() {
+            let (from_table, from_column) = arg.from();
+            let (to_table, to_column) = arg.to();
+            let from_codeword = &ext_codeword_tables.data(from_table)[from_column];
+            let to_codeword = &ext_codeword_tables.data(to_table)[to_column];
+            let non_linear_summand =
+                weighted_difference_codeword(from_codeword, to_codeword, weight);
+            non_linear_sum_codeword =
+                pointwise_addition(non_linear_sum_codeword, non_linear_summand);
+        }
+
+        // input
+        let input_terminal_codeword = vec![self.input_terminal; fri_domain.length];
+        let (to_table, to_column) = self.input_to_processor;
+        let to_codeword = &ext_codeword_tables.data(to_table)[to_column];
+        let weight = self.input_to_processor_weight;
+        let non_linear_summand =
+            weighted_difference_codeword(&input_terminal_codeword, to_codeword, weight);
+        non_linear_sum_codeword = pointwise_addition(non_linear_sum_codeword, non_linear_summand);
+
+        // output
+        let (from_table, from_column) = self.processor_to_output;
+        let from_codeword = &ext_codeword_tables.data(from_table)[from_column];
+        let output_terminal_codeword = vec![self.output_terminal; fri_domain.length];
+        let weight = self.processor_to_output_weight;
+        let non_linear_summand =
+            weighted_difference_codeword(from_codeword, &output_terminal_codeword, weight);
+        non_linear_sum_codeword = pointwise_addition(non_linear_sum_codeword, non_linear_summand);
+
+        let zerofier = fri_domain
+            .domain_values()
+            .into_iter()
+            .map(|x| x - omicron.inverse())
+            .collect();
+        let zerofier_inverse = XFieldElement::batch_inversion(zerofier);
+
+        zerofier_inverse
+            .into_iter()
+            .zip_eq(non_linear_sum_codeword.into_iter())
+            .map(|(z, nls)| nls * z)
+            .collect_vec()
+    }
+
+    pub fn quotient_degree_bound(
+        &self,
+        ext_codeword_tables: &ExtTableCollection,
+        num_trace_randomizers: usize,
+    ) -> Degree {
+        self.program_to_instruction
+            .quotient_degree_bound(ext_codeword_tables, num_trace_randomizers)
+    }
+
+    pub fn evaluate_non_linear_sum_of_differences(
+        &self,
+        cross_table_slice: &[Vec<XFieldElement>],
+    ) -> XFieldElement {
+        // cross-table arguments
+        let mut non_linear_sum = self
+            .into_iter()
+            .map(|(arg, weight)| weight * arg.evaluate_difference(cross_table_slice))
+            .sum();
+
+        // input
+        let (to_table, to_column) = self.input_to_processor;
+        let processor_in = cross_table_slice[to_table as usize][to_column];
+        non_linear_sum += self.input_to_processor_weight * (self.input_terminal - processor_in);
+
+        // output
+        let (from_table, from_colum) = self.processor_to_output;
+        let processor_out = cross_table_slice[from_table as usize][from_colum];
+        non_linear_sum += self.processor_to_output_weight * (processor_out - self.output_terminal);
+
+        non_linear_sum
+    }
+}
+
+fn pointwise_addition(left: Vec<XFieldElement>, right: Vec<XFieldElement>) -> Vec<XFieldElement> {
+    left.into_iter()
+        .zip_eq(right.into_iter())
+        .map(|(l, r)| l + r)
+        .collect_vec()
+}
+
+fn weighted_difference_codeword(
+    from_codeword: &[XFieldElement],
+    to_codeword: &[XFieldElement],
+    weight: XFieldElement,
+) -> Vec<XFieldElement> {
+    from_codeword
+        .iter()
+        .zip_eq(to_codeword.iter())
+        .map(|(&from, &to)| weight * (from - to))
+        .collect_vec()
+}
+
 #[cfg(test)]
 mod permutation_argument_tests {
     use super::*;
+    use crate::stark::triton_stark_tests::parse_simulate_pad_extend;
+    use crate::vm::triton_vm_tests::test_hash_nop_nop_lt;
 
     #[test]
     fn all_permutation_arguments_link_from_processor_table_test() {
         for perm_arg in PermArg::all_permutation_arguments() {
             assert_eq!(TableId::ProcessorTable, perm_arg.from_table);
         }
     }
+
+    #[test]
+    fn all_quotient_degree_bounds_of_grand_cross_table_argument_are_equal_test() {
+        let num_trace_randomizers = 10;
+        let code_with_input = test_hash_nop_nop_lt();
+        let code = code_with_input.source_code;
+        let input = code_with_input.input;
+        let secret_input = code_with_input.secret_input;
+        let (output, _, _, ext_codeword_tables, all_challenges, _) =
+            parse_simulate_pad_extend(&code, &input, &secret_input);
+
+        let input_terminal = EvalArg::compute_terminal(
+            &input,
+            EvalArg::default_initial(),
+            all_challenges
+                .processor_table_challenges
+                .input_table_eval_row_weight,
+        );
+
+        let output_terminal = EvalArg::compute_terminal(
+            &output.to_bword_vec(),
+            EvalArg::default_initial(),
+            all_challenges
+                .processor_table_challenges
+                .output_table_eval_row_weight,
+        );
+
+        let gxta = GrandCrossTableArg::new(
+            &[XFieldElement::one(); NUM_CROSS_TABLE_ARGS + 2],
+            input_terminal,
+            output_terminal,
+        );
+        let quotient_degree_bound = gxta
+            .program_to_instruction
+            .quotient_degree_bound(&ext_codeword_tables, num_trace_randomizers);
+        for (arg, _) in gxta.into_iter() {
+            assert_eq!(
+                quotient_degree_bound,
+                arg.quotient_degree_bound(&ext_codeword_tables, num_trace_randomizers)
+            );
+        }
+    }
 }

triton-vm/src/proof_item.rs

@@ -5,8 +5,6 @@ use twenty_first::util_types::merkle_tree::PartialAuthenticationPath;
 use twenty_first::util_types::proof_stream_typed::ProofStreamError;
 use twenty_first::util_types::simple_hasher::{Hashable, Hasher};
 
-use super::table::challenges_terminals::AllTerminals;
-
 type FriProof<Digest> = Vec<(PartialAuthenticationPath<Digest>, XFieldElement)>;
 type AuthenticationStructure<Digest> = Vec<PartialAuthenticationPath<Digest>>;
 
@@ -20,7 +18,6 @@ where
     TransposedBaseElementVectors(Vec<Vec<BFieldElement>>),
     TransposedExtensionElementVectors(Vec<Vec<XFieldElement>>),
     MerkleRoot(H::Digest),
-    Terminals(AllTerminals<H>),
     TransposedBaseElements(Vec<BFieldElement>),
     TransposedExtensionElements(Vec<XFieldElement>),
     AuthenticationPath(Vec<H::Digest>),
@@ -78,15 +75,6 @@ where
         }
     }
 
-    pub fn as_terminals(&self) -> Result<AllTerminals<H>, Box<dyn std::error::Error>> {
-        match self {
-            Self::Terminals(all_terminals) => Ok(all_terminals.to_owned()),
-            _ => Err(ProofStreamError::boxed(
-                "expected all terminals, but got something else",
-            )),
-        }
-    }
-
     pub fn as_transposed_base_elements(
         &self,
     ) -> Result<Vec<BFieldElement>, Box<dyn std::error::Error>> {
@@ -180,7 +168,6 @@ where
     fn into_iter(self) -> Self::IntoIter {
         match self {
             ProofItem::MerkleRoot(bs) => bs.to_sequence().into_iter(),
-            ProofItem::Terminals(all_terminals) => all_terminals.into_iter(),
             ProofItem::TransposedBaseElements(bs) => bs_to_ts::<H>(&bs).into_iter(),
             ProofItem::TransposedExtensionElements(xs) => bs_to_ts::<H>(&xs_to_bs(&xs)).into_iter(),
             ProofItem::AuthenticationPath(bss) => {