lower the AIR degree to 4

Using substitution and the introduction of new variables, the degree of
the AIR as specified in the respective tables is lowered to 4.

The technique is straightforward and works as follows.
For example, with a target degree of 2 and a constraint of the form
`a = b²·c²·d`,
the degree lowering step could (as one among multiple possibilities)
- introduce new variables `e`, `f`, and `g`,
- introduce new constraints `e = b²`, `f = c²`, and `g = e·f`,
- replace the original constraint with `a = g·d`.

The degree lowering happens in the constraint evaluation generator.
It can be executed by running
`cargo run --bin constraint-evaluation-generator`.
Executing the constraint evaluator is a prerequisite for running both
the Stark prover and the Stark verifier.

The new variables introduced by the degree lowering step are called
“derived columns.” They are added to the `DegreeLoweringTable`, whose
sole purpose is to store the values of these derived columns.

Makefile

@@ -55,8 +55,8 @@ build-constraints:
 	cargo run --bin constraint-evaluation-generator
 
 clean-constraints:
-	git restore --staged triton-vm/src/table/constraints/
-	git restore triton-vm/src/table/constraints/
+	git restore --staged triton-vm/src/table/constraints.rs
+	git restore triton-vm/src/table/constraints.rs
 
 fmt-only:
 	cargo fmt $(FMT_ARGS)

constraint-evaluation-generator/Cargo.toml

@@ -26,3 +26,7 @@ default-features = false
 twenty-first = "0.25.1"
 triton-vm = { path = "../triton-vm" }
 itertools = "0.10"
+syn = "2.0"
+quote = "1.0"
+proc-macro2 = "1.0"
+prettyplease = "0.2"

triton-vm/Cargo.toml

@@ -45,6 +45,8 @@ serde = { version = "1.0", features = ["derive"] }
 strum = "0.24"
 strum_macros = "0.24"
 ndarray = { version = "0.15", features = ["rayon"] }
+quote = "1.0"
+proc-macro2 = "1.0"
 
 [[bench]]
 name = "prove_halt"

triton-vm/src/proof_stream.rs

@@ -195,12 +195,12 @@ mod proof_stream_typed_tests {
     use twenty_first::shared_math::other::random_elements;
     use twenty_first::shared_math::tip5::Tip5;
     use twenty_first::shared_math::x_field_element::XFieldElement;
-    use twenty_first::util_types::merkle_tree::CpuParallel;
     use twenty_first::util_types::merkle_tree::MerkleTree;
     use twenty_first::util_types::merkle_tree_maker::MerkleTreeMaker;
 
     use crate::proof_item::FriResponse;
     use crate::proof_item::ProofItem;
+    use crate::stark::MTMaker;
 
     use super::*;
 
@@ -360,7 +360,7 @@ mod proof_stream_typed_tests {
         let num_leaves = 1 << tree_height;
         let leaf_values: Vec<XFieldElement> = random_elements(num_leaves);
         let leaf_digests = leaf_values.iter().map(|&xfe| xfe.into()).collect_vec();
-        let merkle_tree: MerkleTree<H> = CpuParallel::from_digests(&leaf_digests);
+        let merkle_tree: MerkleTree<H> = MTMaker::from_digests(&leaf_digests);
         let indices_to_check = vec![5, 173, 175, 167, 228, 140, 252, 149, 232, 182, 5, 5, 182];
         let authentication_structure = merkle_tree.get_authentication_structure(&indices_to_check);
         let fri_response_content = authentication_structure

triton-vm/src/table.rs

@@ -1,8 +1,11 @@
 pub mod cascade_table;
 pub mod challenges;
 pub mod constraint_circuit;
+#[rustfmt::skip]
 pub mod constraints;
 pub mod cross_table_argument;
+#[rustfmt::skip]
+pub mod degree_lowering_table;
 pub mod extension_table;
 pub mod hash_table;
 pub mod jump_stack_table;

triton-vm/src/table/cascade_table.rs

@@ -12,7 +12,6 @@ use twenty_first::shared_math::x_field_element::XFieldElement;
 use crate::table::challenges::ChallengeId;
 use crate::table::challenges::ChallengeId::*;
 use crate::table::challenges::Challenges;
-use crate::table::constraint_circuit::ConstraintCircuit;
 use crate::table::constraint_circuit::ConstraintCircuitBuilder;
 use crate::table::constraint_circuit::ConstraintCircuitMonad;
 use crate::table::constraint_circuit::DualRowIndicator;
@@ -135,9 +134,9 @@ impl CascadeTable {
 }
 
 impl ExtCascadeTable {
-    pub fn ext_initial_constraints_as_circuits() -> Vec<ConstraintCircuit<SingleRowIndicator>> {
-        let circuit_builder = ConstraintCircuitBuilder::new();
-
+    pub fn initial_constraints(
+        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
+    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
         let base_row = |col_id: CascadeBaseTableColumn| {
             circuit_builder.input(BaseRow(col_id.master_base_table_index()))
         };
@@ -200,17 +199,15 @@ impl ExtCascadeTable {
             * lookup_table_log_derivative_has_accumulated_first_row
             + is_padding * lookup_table_log_derivative_is_default_initial;
 
-        let mut constraints = [
+        vec![
             hash_table_log_derivative_is_initialized_correctly,
             lookup_table_log_derivative_is_initialized_correctly,
-        ];
-        ConstraintCircuitMonad::constant_folding(&mut constraints);
-        constraints.map(|circuit| circuit.consume()).to_vec()
+        ]
     }
 
-    pub fn ext_consistency_constraints_as_circuits() -> Vec<ConstraintCircuit<SingleRowIndicator>> {
-        let circuit_builder = ConstraintCircuitBuilder::new();
-
+    pub fn consistency_constraints(
+        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
+    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
         let base_row = |col_id: CascadeBaseTableColumn| {
             circuit_builder.input(BaseRow(col_id.master_base_table_index()))
         };
@@ -219,13 +216,12 @@ impl ExtCascadeTable {
         let is_padding = base_row(IsPadding);
         let is_padding_is_0_or_1 = is_padding.clone() * (one - is_padding);
 
-        let mut constraints = [is_padding_is_0_or_1];
-        ConstraintCircuitMonad::constant_folding(&mut constraints);
-        constraints.map(|circuit| circuit.consume()).to_vec()
+        vec![is_padding_is_0_or_1]
     }
 
-    pub fn ext_transition_constraints_as_circuits() -> Vec<ConstraintCircuit<DualRowIndicator>> {
-        let circuit_builder = ConstraintCircuitBuilder::new();
+    pub fn transition_constraints(
+        circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
+    ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
         let challenge = |c| circuit_builder.challenge(c);
         let constant = |c: u64| circuit_builder.b_constant(c.into());
 
@@ -304,16 +300,111 @@ impl ExtCascadeTable {
             * lookup_table_log_derivative_accumulates_next_row
             + is_padding_next * lookup_table_log_derivative_remains;
 
-        let mut constraints = [
+        vec![
             if_current_row_is_padding_row_then_next_row_is_padding_row,
             hash_table_log_derivative_updates_correctly,
             lookup_table_log_derivative_updates_correctly,
-        ];
-        ConstraintCircuitMonad::constant_folding(&mut constraints);
-        constraints.map(|circuit| circuit.consume()).to_vec()
+        ]
     }
 
-    pub fn ext_terminal_constraints_as_circuits() -> Vec<ConstraintCircuit<SingleRowIndicator>> {
+    pub fn terminal_constraints(
+        _circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
+    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
+        // no further constraints
         vec![]
     }
 }
+
+#[cfg(test)]
+pub mod tests {
+    use super::*;
+    use num_traits::Zero;
+
+    pub fn constraints_evaluate_to_zero(
+        master_base_trace_table: ArrayView2<BFieldElement>,
+        master_ext_trace_table: ArrayView2<XFieldElement>,
+        challenges: &Challenges,
+    ) -> bool {
+        let zero = XFieldElement::zero();
+        assert_eq!(
+            master_base_trace_table.nrows(),
+            master_ext_trace_table.nrows()
+        );
+
+        let circuit_builder = ConstraintCircuitBuilder::new();
+        for (constraint_idx, constraint) in ExtCascadeTable::initial_constraints(&circuit_builder)
+            .into_iter()
+            .map(|constraint_monad| constraint_monad.consume())
+            .enumerate()
+        {
+            let evaluated_constraint = constraint.evaluate(
+                master_base_trace_table.slice(s![..1, ..]),
+                master_ext_trace_table.slice(s![..1, ..]),
+                challenges,
+            );
+            assert_eq!(
+                zero, evaluated_constraint,
+                "Initial constraint {constraint_idx} failed."
+            );
+        }
+
+        let circuit_builder = ConstraintCircuitBuilder::new();
+        for (constraint_idx, constraint) in
+            ExtCascadeTable::consistency_constraints(&circuit_builder)
+                .into_iter()
+                .map(|constraint_monad| constraint_monad.consume())
+                .enumerate()
+        {
+            for row_idx in 0..master_base_trace_table.nrows() {
+                let evaluated_constraint = constraint.evaluate(
+                    master_base_trace_table.slice(s![row_idx..row_idx + 1, ..]),
+                    master_ext_trace_table.slice(s![row_idx..row_idx + 1, ..]),
+                    challenges,
+                );
+                assert_eq!(
+                    zero, evaluated_constraint,
+                    "Consistency constraint {constraint_idx} failed on row {row_idx}."
+                );
+            }
+        }
+
+        let circuit_builder = ConstraintCircuitBuilder::new();
+        for (constraint_idx, constraint) in
+            ExtCascadeTable::transition_constraints(&circuit_builder)
+                .into_iter()
+                .map(|constraint_monad| constraint_monad.consume())
+                .enumerate()
+        {
+            for row_idx in 0..master_base_trace_table.nrows() - 1 {
+                let evaluated_constraint = constraint.evaluate(
+                    master_base_trace_table.slice(s![row_idx..row_idx + 2, ..]),
+                    master_ext_trace_table.slice(s![row_idx..row_idx + 2, ..]),
+                    challenges,
+                );
+                assert_eq!(
+                    zero, evaluated_constraint,
+                    "Transition constraint {constraint_idx} failed on row {row_idx}."
+                );
+            }
+        }
+
+        let circuit_builder = ConstraintCircuitBuilder::new();
+        for (constraint_idx, constraint) in ExtCascadeTable::terminal_constraints(&circuit_builder)
+            .into_iter()
+            .map(|constraint_monad| constraint_monad.consume())
+            .enumerate()
+        {
+            let evaluated_constraint = constraint.evaluate(
+                master_base_trace_table.slice(s![-1.., ..]),
+                master_ext_trace_table.slice(s![-1.., ..]),
+                challenges,
+            );
+            assert_eq!(
+                zero, evaluated_constraint,
+                "Terminal constraint {constraint_idx} failed."
+            );
+        }
+
+        true
+    }
+}

triton-vm/src/table/challenges.rs

@@ -158,20 +158,6 @@ pub enum ChallengeId {
     U32CiWeight,
     U32ResultWeight,
 
-    ProcessorToProgramWeight,
-    InputToProcessorWeight,
-    ProcessorToOutputWeight,
-    ProcessorToOpStackWeight,
-    ProcessorToRamWeight,
-    ProcessorToJumpStackWeight,
-    HashInputWeight,
-    HashDigestWeight,
-    SpongeWeight,
-    HashToCascadeWeight,
-    CascadeToLookupWeight,
-    ProcessorToU32Weight,
-    ClockJumpDifferenceLookupWeight,
-
     /// The terminal for the Evaluation Argument with standard input.
     StandardInputTerminal,