10825170249

Committed 12 Sep 2024 06:08AM UTC coverage: 98.369%. Remained the same

Build # 10825170249

Build Type

push

github

Committed by

jan-ferdinand

Commit Message

chore: Use “main” & “aux over “base” & “ext”

This completes the transition started in 07fdf159.

changelog: ignore

Run Details

546 of 558 new or added lines in 17 files covered. (97.85%)

30 existing lines in 4 files now uncovered.

23038 of 23420 relevant lines covered (98.37%)

7954849.83 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

83.26

/triton-vm/src/table.rs

use air::table::cascade::CascadeTable;
use air::table::hash::HashTable;
use air::table::jump_stack::JumpStackTable;
use air::AIR;
use ndarray::ArrayView2;
use ndarray::ArrayViewMut2;
use strum::Display;
use strum::EnumCount;
use strum::EnumIter;
use twenty_first::prelude::*;

use crate::aet::AlgebraicExecutionTrace;
use crate::challenges::Challenges;
pub use crate::stark::NUM_QUOTIENT_SEGMENTS;
use crate::table::master_table::MasterAuxTable;
use crate::table::master_table::MasterMainTable;
use crate::table::master_table::MasterTable;

pub mod auxiliary_table;
pub mod cascade;
pub mod degree_lowering;
pub mod hash;
pub mod jump_stack;
pub mod lookup;
pub mod master_table;
pub mod op_stack;
pub mod processor;
pub mod program;
pub mod ram;
pub mod u32;

trait TraceTable: AIR {
    // a nicer design is in order
    type FillParam;
    type FillReturnInfo;

    fn fill(
        main_table: ArrayViewMut2<BFieldElement>,
        aet: &AlgebraicExecutionTrace,
        _: Self::FillParam,
    ) -> Self::FillReturnInfo;

    fn pad(main_table: ArrayViewMut2<BFieldElement>, table_length: usize);

    fn extend(
        main_table: ArrayView2<BFieldElement>,
        aux_table: ArrayViewMut2<XFieldElement>,
        challenges: &Challenges,
    );
}

#[derive(
    Debug, Display, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, EnumCount, EnumIter,
)]
pub enum ConstraintType {
    /// Pertains only to the first row of the execution trace.
    Initial,

    /// Pertains to each row of the execution trace.
    Consistency,

    /// Pertains to each pair of consecutive rows of the execution trace.
    Transition,

    /// Pertains only to the last row of the execution trace.
    Terminal,
}

/// A single row of a [`MasterMainTable`].
///
/// Usually, the elements in the table are [`BFieldElement`]s. For out-of-domain rows, which is
/// relevant for “Domain Extension to Eliminate Pretenders” (DEEP), the elements are
/// [`XFieldElement`]s.
pub type MainRow<T> = [T; MasterMainTable::NUM_COLUMNS];

/// A single row of a [`MasterAuxTable`].
pub type AuxiliaryRow = [XFieldElement; MasterAuxTable::NUM_COLUMNS];

/// An element of the split-up quotient polynomial.
///
/// See also [`NUM_QUOTIENT_SEGMENTS`].
pub type QuotientSegments = [XFieldElement; NUM_QUOTIENT_SEGMENTS];

#[cfg(test)]
mod tests {
    use std::collections::HashMap;

    use air::table::hash::HashTable;
    use air::table::lookup::LookupTable;
    use air::table::op_stack::OpStackTable;
    use air::table::processor::ProcessorTable;
    use air::table::program::ProgramTable;
    use air::table::ram::RamTable;
    use air::table::u32::U32Table;
    use air::table::AUX_CASCADE_TABLE_END;
    use air::table::AUX_HASH_TABLE_END;
    use air::table::AUX_JUMP_STACK_TABLE_END;
    use air::table::AUX_LOOKUP_TABLE_END;
    use air::table::AUX_OP_STACK_TABLE_END;
    use air::table::AUX_PROCESSOR_TABLE_END;
    use air::table::AUX_PROGRAM_TABLE_END;
    use air::table::AUX_RAM_TABLE_END;
    use air::table::AUX_U32_TABLE_END;
    use air::table::CASCADE_TABLE_END;
    use air::table::HASH_TABLE_END;
    use air::table::JUMP_STACK_TABLE_END;
    use air::table::LOOKUP_TABLE_END;
    use air::table::OP_STACK_TABLE_END;
    use air::table::PROCESSOR_TABLE_END;
    use air::table::PROGRAM_TABLE_END;
    use air::table::RAM_TABLE_END;
    use air::table::U32_TABLE_END;
    use constraint_circuit::BinOp;
    use constraint_circuit::CircuitExpression;
    use constraint_circuit::ConstraintCircuit;
    use constraint_circuit::ConstraintCircuitBuilder;
    use constraint_circuit::ConstraintCircuitMonad;
    use constraint_circuit::DegreeLoweringInfo;
    use constraint_circuit::InputIndicator;
    use itertools::Itertools;
    use ndarray::Array2;
    use ndarray::ArrayView2;
    use rand::prelude::StdRng;
    use rand::random;
    use rand::Rng;
    use rand_core::SeedableRng;
    use twenty_first::prelude::BFieldElement;

    use crate::challenges::Challenges;
    use crate::prelude::Claim;
    use crate::table::degree_lowering::DegreeLoweringTable;

    use super::*;

    /// Verify that all nodes evaluate to a unique value when given a randomized input.
    /// If this is not the case two nodes that are not equal evaluate to the same value.
    fn table_constraints_prop<II: InputIndicator>(
        constraints: &[ConstraintCircuit<II>],
        table_name: &str,
    ) {
        let seed = random();
        let mut rng = StdRng::seed_from_u64(seed);
        println!("seed: {seed}");

        let dummy_claim = Claim::default();
        let challenges: [XFieldElement; Challenges::SAMPLE_COUNT] = rng.gen();
        let challenges = challenges.to_vec();
        let challenges = Challenges::new(challenges, &dummy_claim);
        let challenges = &challenges.challenges;

        let num_rows = 2;
        let main_shape = [num_rows, MasterMainTable::NUM_COLUMNS];
        let aux_shape = [num_rows, MasterAuxTable::NUM_COLUMNS];
        let main_rows = Array2::from_shape_simple_fn(main_shape, || rng.gen::<BFieldElement>());
        let aux_rows = Array2::from_shape_simple_fn(aux_shape, || rng.gen::<XFieldElement>());
        let main_rows = main_rows.view();
        let aux_rows = aux_rows.view();

        let mut values = HashMap::new();
        for c in constraints {
            evaluate_assert_unique(c, challenges, main_rows, aux_rows, &mut values);
        }

        let circuit_degree = constraints.iter().map(|c| c.degree()).max().unwrap_or(-1);
        println!("Max degree constraint for {table_name} table: {circuit_degree}");
    }

    /// Recursively evaluates the given constraint circuit and its sub-circuits on the given
    /// main and auxiliary table, and returns the result of the evaluation.
    /// At each recursive step, updates the given HashMap with the result of the evaluation.
    /// If the HashMap already contains the result of the evaluation, panics.
    /// This function is used to assert that the evaluation of a constraint circuit
    /// and its sub-circuits is unique.
    /// It is used to identify redundant constraints or sub-circuits.
    /// The employed method is the Schwartz-Zippel lemma.
    fn evaluate_assert_unique<II: InputIndicator>(
        constraint: &ConstraintCircuit<II>,
        challenges: &[XFieldElement],
        main_rows: ArrayView2<BFieldElement>,
        aux_rows: ArrayView2<XFieldElement>,
        values: &mut HashMap<XFieldElement, (usize, ConstraintCircuit<II>)>,
    ) -> XFieldElement {
        let value = match &constraint.expression {
            CircuitExpression::BinOp(binop, lhs, rhs) => {
                let lhs = lhs.borrow();
                let rhs = rhs.borrow();
                let lhs = evaluate_assert_unique(&lhs, challenges, main_rows, aux_rows, values);
                let rhs = evaluate_assert_unique(&rhs, challenges, main_rows, aux_rows, values);
                binop.operation(lhs, rhs)
            }
            _ => constraint.evaluate(main_rows, aux_rows, challenges),
        };

        let own_id = constraint.id.to_owned();
        let maybe_entry = values.insert(value, (own_id, constraint.clone()));
        if let Some((other_id, other_circuit)) = maybe_entry {
            assert_eq!(
                own_id, other_id,
                "Circuit ID {other_id} and circuit ID {own_id} are not unique. \
                Collision on:\n\
                ID {other_id} – {other_circuit}\n\
                ID {own_id} – {constraint}\n\
                Both evaluate to {value}.",
            );
        }

        value
    }

    #[test]
    fn nodes_are_unique_for_all_constraints() {
        fn build_constraints<II: InputIndicator>(
            multicircuit_builder: &dyn Fn(
                &ConstraintCircuitBuilder<II>,
            ) -> Vec<ConstraintCircuitMonad<II>>,
        ) -> Vec<ConstraintCircuit<II>> {
            let circuit_builder = ConstraintCircuitBuilder::new();
            let multicircuit = multicircuit_builder(&circuit_builder);
            let mut constraints = multicircuit.into_iter().map(|c| c.consume()).collect_vec();
            ConstraintCircuit::assert_unique_ids(&mut constraints);
            constraints
        }

        macro_rules! assert_constraint_properties {
            ($table:ident) => {{
                let init = build_constraints(&$table::initial_constraints);
                let cons = build_constraints(&$table::consistency_constraints);
                let tran = build_constraints(&$table::transition_constraints);
                let term = build_constraints(&$table::terminal_constraints);
                table_constraints_prop(&init, concat!(stringify!($table), " init"));
                table_constraints_prop(&cons, concat!(stringify!($table), " cons"));
                table_constraints_prop(&tran, concat!(stringify!($table), " tran"));
                table_constraints_prop(&term, concat!(stringify!($table), " term"));
            }};
        }

        assert_constraint_properties!(ProcessorTable);
        assert_constraint_properties!(ProgramTable);
        assert_constraint_properties!(JumpStackTable);
        assert_constraint_properties!(OpStackTable);
        assert_constraint_properties!(RamTable);
        assert_constraint_properties!(HashTable);
        assert_constraint_properties!(U32Table);
        assert_constraint_properties!(CascadeTable);
        assert_constraint_properties!(LookupTable);
    }

    /// Like [`ConstraintCircuitMonad::lower_to_degree`] with additional assertion of expected
    /// properties. Also prints:
    /// - the given multicircuit prior to degree lowering
    /// - the multicircuit after degree lowering
    /// - the new base constraints
    /// - the new auxiliary constraints
    /// - the numbers of original and new constraints
    fn lower_degree_and_assert_properties<II: InputIndicator>(
        multicircuit: &mut [ConstraintCircuitMonad<II>],
        info: DegreeLoweringInfo,
    ) -> (
        Vec<ConstraintCircuitMonad<II>>,
        Vec<ConstraintCircuitMonad<II>>,
    ) {
        let seed = random();
        let mut rng = StdRng::seed_from_u64(seed);
        println!("seed: {seed}");

        let num_constraints = multicircuit.len();
        println!("original multicircuit:");
        for circuit in multicircuit.iter() {
            println!("  {circuit}");
        }

        let (new_main_constraints, new_aux_constraints) =
            ConstraintCircuitMonad::lower_to_degree(multicircuit, info);

        assert_eq!(num_constraints, multicircuit.len());

        let target_deg = info.target_degree;
        assert!(ConstraintCircuitMonad::multicircuit_degree(multicircuit) <= target_deg);
        assert!(ConstraintCircuitMonad::multicircuit_degree(&new_main_constraints) <= target_deg);
        assert!(ConstraintCircuitMonad::multicircuit_degree(&new_aux_constraints) <= target_deg);

        // Check that the new constraints are simple substitutions.
        let mut substitution_rules = vec![];
        for (constraint_type, constraints) in [
            ("main", &new_main_constraints),
            ("aux", &new_aux_constraints),
        ] {
            for (i, constraint) in constraints.iter().enumerate() {
                let expression = constraint.circuit.borrow().expression.clone();
                let CircuitExpression::BinOp(BinOp::Add, lhs, rhs) = expression else {
                    panic!("New {constraint_type} constraint {i} must be a subtraction.");
                };
                let CircuitExpression::Input(input_indicator) = lhs.borrow().expression.clone()
                else {
                    panic!("New {constraint_type} constraint {i} must be a simple substitution.");
                };
                let substitution_rule = rhs.borrow().clone();
                assert_substitution_rule_uses_legal_variables(input_indicator, &substitution_rule);
                substitution_rules.push(substitution_rule);
            }
        }

        // Use the Schwartz-Zippel lemma to check no two substitution rules are equal.
        let dummy_claim = Claim::default();
        let challenges: [XFieldElement; Challenges::SAMPLE_COUNT] = rng.gen();
        let challenges = challenges.to_vec();
        let challenges = Challenges::new(challenges, &dummy_claim);
        let challenges = &challenges.challenges;

        let num_rows = 2;
        let main_shape = [num_rows, MasterMainTable::NUM_COLUMNS];
        let aux_shape = [num_rows, MasterAuxTable::NUM_COLUMNS];
        let main_rows = Array2::from_shape_simple_fn(main_shape, || rng.gen::<BFieldElement>());
        let aux_rows = Array2::from_shape_simple_fn(aux_shape, || rng.gen::<XFieldElement>());
        let main_rows = main_rows.view();
        let aux_rows = aux_rows.view();

        let evaluated_substitution_rules = substitution_rules
            .iter()
            .map(|c| c.evaluate(main_rows, aux_rows, challenges));

        let mut values_to_index = HashMap::new();
        for (idx, value) in evaluated_substitution_rules.enumerate() {
            if let Some(index) = values_to_index.get(&value) {
                panic!("Substitution {idx} must be distinct from substitution {index}.");
            } else {
                values_to_index.insert(value, idx);
            }
        }

        // Print the multicircuit and new constraints after degree lowering.
        println!("new multicircuit:");
        for circuit in multicircuit.iter() {
            println!("  {circuit}");
        }
        println!("new main constraints:");
        for constraint in &new_main_constraints {
            println!("  {constraint}");
        }
        println!("new aux constraints:");
        for constraint in &new_aux_constraints {
            println!("  {constraint}");
        }

        let num_new_main_constraints = new_main_constraints.len();
        let num_new_aux_constraints = new_aux_constraints.len();
        println!(
            "Started with {num_constraints} constraints. \
            Derived {num_new_main_constraints} new main, \
            {num_new_aux_constraints} new auxiliary constraints."
        );

        (new_main_constraints, new_aux_constraints)
    }

    /// Panics if the given substitution rule uses variables with an index greater than (or equal)
    /// to the given index. In practice, this given index corresponds to a newly introduced
    /// variable.
    fn assert_substitution_rule_uses_legal_variables<II: InputIndicator>(
        new_var: II,
        substitution_rule: &ConstraintCircuit<II>,
    ) {
        match substitution_rule.expression.clone() {
            CircuitExpression::BinOp(_, lhs, rhs) => {
                let lhs = lhs.borrow();
                let rhs = rhs.borrow();
                assert_substitution_rule_uses_legal_variables(new_var, &lhs);
                assert_substitution_rule_uses_legal_variables(new_var, &rhs);
            }
            CircuitExpression::Input(old_var) => {
                let new_var_is_main = new_var.is_main_table_column();
                let old_var_is_main = old_var.is_main_table_column();
                let legal_substitute = match (new_var_is_main, old_var_is_main) {
                    (true, false) => false,
                    (false, true) => true,
                    _ => old_var.column() < new_var.column(),
                };
                assert!(legal_substitute, "Cannot replace {old_var} with {new_var}.");
            }
            _ => (),
        };
    }

    #[test]
    fn degree_lowering_works_correctly_for_all_tables() {
        macro_rules! assert_degree_lowering {
            ($table:ident ($main_end:ident, $aux_end:ident)) => {{
                let degree_lowering_info = DegreeLoweringInfo {
                    target_degree: air::TARGET_DEGREE,
                    num_main_cols: $main_end,
                    num_aux_cols: $aux_end,
                };
                let circuit_builder = ConstraintCircuitBuilder::new();
                let mut init = $table::initial_constraints(&circuit_builder);
                lower_degree_and_assert_properties(&mut init, degree_lowering_info);

                let circuit_builder = ConstraintCircuitBuilder::new();
                let mut cons = $table::consistency_constraints(&circuit_builder);
                lower_degree_and_assert_properties(&mut cons, degree_lowering_info);

                let circuit_builder = ConstraintCircuitBuilder::new();
                let mut tran = $table::transition_constraints(&circuit_builder);
                lower_degree_and_assert_properties(&mut tran, degree_lowering_info);

                let circuit_builder = ConstraintCircuitBuilder::new();
                let mut term = $table::terminal_constraints(&circuit_builder);
                lower_degree_and_assert_properties(&mut term, degree_lowering_info);
            }};
        }

        assert_degree_lowering!(ProgramTable(PROGRAM_TABLE_END, AUX_PROGRAM_TABLE_END));
        assert_degree_lowering!(ProcessorTable(PROCESSOR_TABLE_END, AUX_PROCESSOR_TABLE_END));
        assert_degree_lowering!(OpStackTable(OP_STACK_TABLE_END, AUX_OP_STACK_TABLE_END));
        assert_degree_lowering!(RamTable(RAM_TABLE_END, AUX_RAM_TABLE_END));
        assert_degree_lowering!(JumpStackTable(
            JUMP_STACK_TABLE_END,
            AUX_JUMP_STACK_TABLE_END
        ));
        assert_degree_lowering!(HashTable(HASH_TABLE_END, AUX_HASH_TABLE_END));
        assert_degree_lowering!(CascadeTable(CASCADE_TABLE_END, AUX_CASCADE_TABLE_END));
        assert_degree_lowering!(LookupTable(LOOKUP_TABLE_END, AUX_LOOKUP_TABLE_END));
        assert_degree_lowering!(U32Table(U32_TABLE_END, AUX_U32_TABLE_END));
    }

    /// Fills the derived columns of the degree-lowering table using randomly generated rows and
    /// checks the resulting values for uniqueness. The described method corresponds to an
    /// application of the Schwartz-Zippel lemma to check uniqueness of the substitution rules
    /// generated during degree lowering.
    #[test]
    #[ignore = "(probably) requires normalization of circuit expressions"]
    fn substitution_rules_are_unique() {
        let challenges = Challenges::default();
        let mut main_table_rows =
            Array2::from_shape_fn((2, MasterMainTable::NUM_COLUMNS), |_| random());
        let mut aux_table_rows =
            Array2::from_shape_fn((2, MasterAuxTable::NUM_COLUMNS), |_| random());

        DegreeLoweringTable::fill_derived_main_columns(main_table_rows.view_mut());
        DegreeLoweringTable::fill_derived_aux_columns(
            main_table_rows.view(),
            aux_table_rows.view_mut(),
            &challenges,
        );

        let mut encountered_values = HashMap::new();
        for col_idx in 0..MasterMainTable::NUM_COLUMNS {
            let val = main_table_rows[(0, col_idx)].lift();
            let other_entry = encountered_values.insert(val, col_idx);
            if let Some(other_idx) = other_entry {
                panic!("Duplicate value {val} in derived main column {other_idx} and {col_idx}.");
            }
        }
        println!("Now comparing auxiliary columns…");
        for col_idx in 0..MasterAuxTable::NUM_COLUMNS {
            let val = aux_table_rows[(0, col_idx)];
            let other_entry = encountered_values.insert(val, col_idx);
            if let Some(other_idx) = other_entry {
                panic!("Duplicate value {val} in derived aux column {other_idx} and {col_idx}.");
            }
        }
    }
}

1	use air::table::cascade::CascadeTable;
2	use air::table::hash::HashTable;
3	use air::table::jump_stack::JumpStackTable;
4	use air::AIR;
5	use ndarray::ArrayView2;
6	use ndarray::ArrayViewMut2;
7	use strum::Display;
8	use strum::EnumCount;
9	use strum::EnumIter;
10	use twenty_first::prelude::*;
11
12	use crate::aet::AlgebraicExecutionTrace;
13	use crate::challenges::Challenges;
14	pub use crate::stark::NUM_QUOTIENT_SEGMENTS;
15	use crate::table::master_table::MasterAuxTable;
16	use crate::table::master_table::MasterMainTable;
17	use crate::table::master_table::MasterTable;
18
19	pub mod auxiliary_table;
20	pub mod cascade;
21	pub mod degree_lowering;
22	pub mod hash;
23	pub mod jump_stack;
24	pub mod lookup;
25	pub mod master_table;
26	pub mod op_stack;
27	pub mod processor;
28	pub mod program;
29	pub mod ram;
30	pub mod u32;
31
32	trait TraceTable: AIR {
33	// a nicer design is in order
34	type FillParam;
35	type FillReturnInfo;
36
37	fn fill(
38	main_table: ArrayViewMut2<BFieldElement>,
39	aet: &AlgebraicExecutionTrace,
40	_: Self::FillParam,
41	) -> Self::FillReturnInfo;
42
43	fn pad(main_table: ArrayViewMut2<BFieldElement>, table_length: usize);
44
45	fn extend(
46	main_table: ArrayView2<BFieldElement>,
47	aux_table: ArrayViewMut2<XFieldElement>,
48	challenges: &Challenges,
49	);
50	}
51
52	#[derive(
53	Debug, Display, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, EnumCount, EnumIter,	592✔
54	)]
55	pub enum ConstraintType {
56	/// Pertains only to the first row of the execution trace.
57	Initial,
58
59	/// Pertains to each row of the execution trace.
60	Consistency,
61
62	/// Pertains to each pair of consecutive rows of the execution trace.
63	Transition,
64
65	/// Pertains only to the last row of the execution trace.
66	Terminal,
67	}
68
69	/// A single row of a [`MasterMainTable`].
70	///
71	/// Usually, the elements in the table are [`BFieldElement`]s. For out-of-domain rows, which is
72	/// relevant for “Domain Extension to Eliminate Pretenders” (DEEP), the elements are
73	/// [`XFieldElement`]s.
74	pub type MainRow<T> = [T; MasterMainTable::NUM_COLUMNS];
75
76	/// A single row of a [`MasterAuxTable`].
77	pub type AuxiliaryRow = [XFieldElement; MasterAuxTable::NUM_COLUMNS];
78
79	/// An element of the split-up quotient polynomial.
80	///
81	/// See also [`NUM_QUOTIENT_SEGMENTS`].
82	pub type QuotientSegments = [XFieldElement; NUM_QUOTIENT_SEGMENTS];
83
84	#[cfg(test)]
85	mod tests {
86	use std::collections::HashMap;
87
88	use air::table::hash::HashTable;
89	use air::table::lookup::LookupTable;
90	use air::table::op_stack::OpStackTable;
91	use air::table::processor::ProcessorTable;
92	use air::table::program::ProgramTable;
93	use air::table::ram::RamTable;
94	use air::table::u32::U32Table;
95	use air::table::AUX_CASCADE_TABLE_END;
96	use air::table::AUX_HASH_TABLE_END;
97	use air::table::AUX_JUMP_STACK_TABLE_END;
98	use air::table::AUX_LOOKUP_TABLE_END;
99	use air::table::AUX_OP_STACK_TABLE_END;
100	use air::table::AUX_PROCESSOR_TABLE_END;
101	use air::table::AUX_PROGRAM_TABLE_END;
102	use air::table::AUX_RAM_TABLE_END;
103	use air::table::AUX_U32_TABLE_END;
104	use air::table::CASCADE_TABLE_END;
105	use air::table::HASH_TABLE_END;
106	use air::table::JUMP_STACK_TABLE_END;
107	use air::table::LOOKUP_TABLE_END;
108	use air::table::OP_STACK_TABLE_END;
109	use air::table::PROCESSOR_TABLE_END;
110	use air::table::PROGRAM_TABLE_END;
111	use air::table::RAM_TABLE_END;
112	use air::table::U32_TABLE_END;
113	use constraint_circuit::BinOp;
114	use constraint_circuit::CircuitExpression;
115	use constraint_circuit::ConstraintCircuit;
116	use constraint_circuit::ConstraintCircuitBuilder;
117	use constraint_circuit::ConstraintCircuitMonad;
118	use constraint_circuit::DegreeLoweringInfo;
119	use constraint_circuit::InputIndicator;
120	use itertools::Itertools;
121	use ndarray::Array2;
122	use ndarray::ArrayView2;
123	use rand::prelude::StdRng;
124	use rand::random;
125	use rand::Rng;
126	use rand_core::SeedableRng;
127	use twenty_first::prelude::BFieldElement;
128
129	use crate::challenges::Challenges;
130	use crate::prelude::Claim;
131	use crate::table::degree_lowering::DegreeLoweringTable;
132
133	use super::*;
134
135	/// Verify that all nodes evaluate to a unique value when given a randomized input.
136	/// If this is not the case two nodes that are not equal evaluate to the same value.
137	fn table_constraints_prop<II: InputIndicator>(	36✔
138	constraints: &[ConstraintCircuit<II>],	36✔
139	table_name: &str,	36✔
140	) {	36✔
141	let seed = random();	36✔
142	let mut rng = StdRng::seed_from_u64(seed);	36✔
143	println!("seed: {seed}");	36✔
144		36✔
145	let dummy_claim = Claim::default();	36✔
146	let challenges: [XFieldElement; Challenges::SAMPLE_COUNT] = rng.gen();	36✔
147	let challenges = challenges.to_vec();	36✔
148	let challenges = Challenges::new(challenges, &dummy_claim);	36✔
149	let challenges = &challenges.challenges;	36✔
150		36✔
151	let num_rows = 2;	36✔
152	let main_shape = [num_rows, MasterMainTable::NUM_COLUMNS];	36✔
153	let aux_shape = [num_rows, MasterAuxTable::NUM_COLUMNS];	36✔
154	let main_rows = Array2::from_shape_simple_fn(main_shape, \|\| rng.gen::<BFieldElement>());	27,000✔
155	let aux_rows = Array2::from_shape_simple_fn(aux_shape, \|\| rng.gen::<XFieldElement>());	6,336✔
156	let main_rows = main_rows.view();	36✔
157	let aux_rows = aux_rows.view();	36✔
158		36✔
159	let mut values = HashMap::new();	36✔
160	for c in constraints {	350✔
161	evaluate_assert_unique(c, challenges, main_rows, aux_rows, &mut values);	314✔
162	}	314✔
163
164	let circuit_degree = constraints.iter().map(\|c\| c.degree()).max().unwrap_or(-1);	314✔
165	println!("Max degree constraint for {table_name} table: {circuit_degree}");	36✔
166	}	36✔
167
168	/// Recursively evaluates the given constraint circuit and its sub-circuits on the given
169	/// main and auxiliary table, and returns the result of the evaluation.
170	/// At each recursive step, updates the given HashMap with the result of the evaluation.
171	/// If the HashMap already contains the result of the evaluation, panics.
172	/// This function is used to assert that the evaluation of a constraint circuit
173	/// and its sub-circuits is unique.
174	/// It is used to identify redundant constraints or sub-circuits.
175	/// The employed method is the Schwartz-Zippel lemma.
176	fn evaluate_assert_unique<II: InputIndicator>(	54,086✔
177	constraint: &ConstraintCircuit<II>,	54,086✔
178	challenges: &[XFieldElement],	54,086✔
179	main_rows: ArrayView2<BFieldElement>,	54,086✔
180	aux_rows: ArrayView2<XFieldElement>,	54,086✔
181	values: &mut HashMap<XFieldElement, (usize, ConstraintCircuit<II>)>,	54,086✔
182	) -> XFieldElement {	54,086✔
183	let value = match &constraint.expression {	54,086✔
184	CircuitExpression::BinOp(binop, lhs, rhs) => {	26,886✔
185	let lhs = lhs.borrow();	26,886✔
186	let rhs = rhs.borrow();	26,886✔
187	let lhs = evaluate_assert_unique(&lhs, challenges, main_rows, aux_rows, values);	26,886✔
188	let rhs = evaluate_assert_unique(&rhs, challenges, main_rows, aux_rows, values);	26,886✔
189	binop.operation(lhs, rhs)	26,886✔
190	}
191	_ => constraint.evaluate(main_rows, aux_rows, challenges),	27,200✔
192	};
193
194	let own_id = constraint.id.to_owned();	54,086✔
195	let maybe_entry = values.insert(value, (own_id, constraint.clone()));	54,086✔
196	if let Some((other_id, other_circuit)) = maybe_entry {	54,086✔
197	assert_eq!(	46,530✔
198	own_id, other_id,
199	"Circuit ID {other_id} and circuit ID {own_id} are not unique. \	×
200	Collision on:\n\	×
201	ID {other_id} – {other_circuit}\n\	×
202	ID {own_id} – {constraint}\n\	×
203	Both evaluate to {value}.",	×
204	);
205	}	7,556✔
206
207	value	54,086✔
208	}	54,086✔
209
210	#[test]
211	fn nodes_are_unique_for_all_constraints() {	1✔
212	fn build_constraints<II: InputIndicator>(	36✔
213	multicircuit_builder: &dyn Fn(	36✔
214	&ConstraintCircuitBuilder<II>,	36✔
215	) -> Vec<ConstraintCircuitMonad<II>>,	36✔
216	) -> Vec<ConstraintCircuit<II>> {	36✔
217	let circuit_builder = ConstraintCircuitBuilder::new();	36✔
218	let multicircuit = multicircuit_builder(&circuit_builder);	36✔
219	let mut constraints = multicircuit.into_iter().map(\|c\| c.consume()).collect_vec();	314✔
220	ConstraintCircuit::assert_unique_ids(&mut constraints);	36✔
221	constraints	36✔
222	}	36✔
223
224	macro_rules! assert_constraint_properties {
225	($table:ident) => {{
226	let init = build_constraints(&$table::initial_constraints);
227	let cons = build_constraints(&$table::consistency_constraints);
228	let tran = build_constraints(&$table::transition_constraints);
229	let term = build_constraints(&$table::terminal_constraints);
230	table_constraints_prop(&init, concat!(stringify!($table), " init"));
231	table_constraints_prop(&cons, concat!(stringify!($table), " cons"));
232	table_constraints_prop(&tran, concat!(stringify!($table), " tran"));
233	table_constraints_prop(&term, concat!(stringify!($table), " term"));
234	}};
235	}
236
237	assert_constraint_properties!(ProcessorTable);	1✔
238	assert_constraint_properties!(ProgramTable);	1✔
239	assert_constraint_properties!(JumpStackTable);	1✔
240	assert_constraint_properties!(OpStackTable);	1✔
241	assert_constraint_properties!(RamTable);	1✔
242	assert_constraint_properties!(HashTable);	1✔
243	assert_constraint_properties!(U32Table);	1✔
244	assert_constraint_properties!(CascadeTable);	1✔
245	assert_constraint_properties!(LookupTable);	1✔
246	}	1✔
247
248	/// Like [`ConstraintCircuitMonad::lower_to_degree`] with additional assertion of expected
249	/// properties. Also prints:
250	/// - the given multicircuit prior to degree lowering
251	/// - the multicircuit after degree lowering
252	/// - the new base constraints
253	/// - the new auxiliary constraints
254	/// - the numbers of original and new constraints
255	fn lower_degree_and_assert_properties<II: InputIndicator>(	36✔
256	multicircuit: &mut [ConstraintCircuitMonad<II>],	36✔
257	info: DegreeLoweringInfo,	36✔
258	) -> (	36✔
259	Vec<ConstraintCircuitMonad<II>>,	36✔
260	Vec<ConstraintCircuitMonad<II>>,	36✔
261	) {	36✔
262	let seed = random();	36✔
263	let mut rng = StdRng::seed_from_u64(seed);	36✔
264	println!("seed: {seed}");	36✔
265		36✔
266	let num_constraints = multicircuit.len();	36✔
267	println!("original multicircuit:");	36✔
268	for circuit in multicircuit.iter() {	314✔
269	println!(" {circuit}");	314✔
270	}	314✔
271
272	let (new_main_constraints, new_aux_constraints) =	36✔
273	ConstraintCircuitMonad::lower_to_degree(multicircuit, info);	36✔
274		36✔
275	assert_eq!(num_constraints, multicircuit.len());	36✔
276
277	let target_deg = info.target_degree;	36✔
278	assert!(ConstraintCircuitMonad::multicircuit_degree(multicircuit) <= target_deg);	36✔
279	assert!(ConstraintCircuitMonad::multicircuit_degree(&new_main_constraints) <= target_deg);	36✔
280	assert!(ConstraintCircuitMonad::multicircuit_degree(&new_aux_constraints) <= target_deg);	36✔
281
282	// Check that the new constraints are simple substitutions.
283	let mut substitution_rules = vec![];	36✔
284	for (constraint_type, constraints) in [	72✔
285	("main", &new_main_constraints),	36✔
286	("aux", &new_aux_constraints),	36✔
287	] {
288	for (i, constraint) in constraints.iter().enumerate() {	264✔
289	let expression = constraint.circuit.borrow().expression.clone();	264✔
290	let CircuitExpression::BinOp(BinOp::Add, lhs, rhs) = expression else {	264✔
291	panic!("New {constraint_type} constraint {i} must be a subtraction.");	×
292	};
293	let CircuitExpression::Input(input_indicator) = lhs.borrow().expression.clone()	264✔
294	else {
295	panic!("New {constraint_type} constraint {i} must be a simple substitution.");	×
296	};
297	let substitution_rule = rhs.borrow().clone();	264✔
298	assert_substitution_rule_uses_legal_variables(input_indicator, &substitution_rule);	264✔
299	substitution_rules.push(substitution_rule);	264✔
300	}
301	}
302
303	// Use the Schwartz-Zippel lemma to check no two substitution rules are equal.
304	let dummy_claim = Claim::default();	36✔
305	let challenges: [XFieldElement; Challenges::SAMPLE_COUNT] = rng.gen();	36✔
306	let challenges = challenges.to_vec();	36✔
307	let challenges = Challenges::new(challenges, &dummy_claim);	36✔
308	let challenges = &challenges.challenges;	36✔
309		36✔
310	let num_rows = 2;	36✔
311	let main_shape = [num_rows, MasterMainTable::NUM_COLUMNS];	36✔
312	let aux_shape = [num_rows, MasterAuxTable::NUM_COLUMNS];	36✔
313	let main_rows = Array2::from_shape_simple_fn(main_shape, \|\| rng.gen::<BFieldElement>());	27,000✔
314	let aux_rows = Array2::from_shape_simple_fn(aux_shape, \|\| rng.gen::<XFieldElement>());	6,336✔
315	let main_rows = main_rows.view();	36✔
316	let aux_rows = aux_rows.view();	36✔
317		36✔
318	let evaluated_substitution_rules = substitution_rules	36✔
319	.iter()	36✔
320	.map(\|c\| c.evaluate(main_rows, aux_rows, challenges));	264✔
321		36✔
322	let mut values_to_index = HashMap::new();	36✔
323	for (idx, value) in evaluated_substitution_rules.enumerate() {	264✔
324	if let Some(index) = values_to_index.get(&value) {	264✔
325	panic!("Substitution {idx} must be distinct from substitution {index}.");	×
326	} else {	264✔
327	values_to_index.insert(value, idx);	264✔
328	}	264✔
329	}
330
331	// Print the multicircuit and new constraints after degree lowering.
332	println!("new multicircuit:");	36✔
333	for circuit in multicircuit.iter() {	314✔
334	println!(" {circuit}");	314✔
335	}	314✔
336	println!("new main constraints:");	36✔
337	for constraint in &new_main_constraints {	262✔
338	println!(" {constraint}");	226✔
339	}	226✔
340	println!("new aux constraints:");	36✔
341	for constraint in &new_aux_constraints {	74✔
342	println!(" {constraint}");	38✔
343	}	38✔
344
345	let num_new_main_constraints = new_main_constraints.len();	36✔
346	let num_new_aux_constraints = new_aux_constraints.len();	36✔
347	println!(	36✔
348	"Started with {num_constraints} constraints. \	36✔
349	Derived {num_new_main_constraints} new main, \	36✔
350	{num_new_aux_constraints} new auxiliary constraints."	36✔
351	);	36✔
352		36✔
353	(new_main_constraints, new_aux_constraints)	36✔
354	}	36✔
355
356	/// Panics if the given substitution rule uses variables with an index greater than (or equal)
357	/// to the given index. In practice, this given index corresponds to a newly introduced
358	/// variable.
359	fn assert_substitution_rule_uses_legal_variables<II: InputIndicator>(	3,394✔
360	new_var: II,	3,394✔
361	substitution_rule: &ConstraintCircuit<II>,	3,394✔
362	) {	3,394✔
363	match substitution_rule.expression.clone() {	3,394✔
364	CircuitExpression::BinOp(_, lhs, rhs) => {	1,565✔
365	let lhs = lhs.borrow();	1,565✔
366	let rhs = rhs.borrow();	1,565✔
367	assert_substitution_rule_uses_legal_variables(new_var, &lhs);	1,565✔
368	assert_substitution_rule_uses_legal_variables(new_var, &rhs);	1,565✔
369	}	1,565✔
370	CircuitExpression::Input(old_var) => {	916✔
371	let new_var_is_main = new_var.is_main_table_column();	916✔
372	let old_var_is_main = old_var.is_main_table_column();	916✔
373	let legal_substitute = match (new_var_is_main, old_var_is_main) {	916✔
UNCOV 374	(true, false) => false,	×
375	(false, true) => true,	196✔
376	_ => old_var.column() < new_var.column(),	720✔
377	};
378	assert!(legal_substitute, "Cannot replace {old_var} with {new_var}.");	916✔
379	}
380	_ => (),	913✔
381	};
382	}	3,394✔
383
384	#[test]
385	fn degree_lowering_works_correctly_for_all_tables() {	1✔
386	macro_rules! assert_degree_lowering {
387	($table:ident ($main_end:ident, $aux_end:ident)) => {{
388	let degree_lowering_info = DegreeLoweringInfo {
389	target_degree: air::TARGET_DEGREE,
390	num_main_cols: $main_end,
391	num_aux_cols: $aux_end,
392	};
393	let circuit_builder = ConstraintCircuitBuilder::new();
394	let mut init = $table::initial_constraints(&circuit_builder);
395	lower_degree_and_assert_properties(&mut init, degree_lowering_info);
396
397	let circuit_builder = ConstraintCircuitBuilder::new();
398	let mut cons = $table::consistency_constraints(&circuit_builder);
399	lower_degree_and_assert_properties(&mut cons, degree_lowering_info);
400
401	let circuit_builder = ConstraintCircuitBuilder::new();
402	let mut tran = $table::transition_constraints(&circuit_builder);
403	lower_degree_and_assert_properties(&mut tran, degree_lowering_info);
404
405	let circuit_builder = ConstraintCircuitBuilder::new();
406	let mut term = $table::terminal_constraints(&circuit_builder);
407	lower_degree_and_assert_properties(&mut term, degree_lowering_info);
408	}};
409	}
410
411	assert_degree_lowering!(ProgramTable(PROGRAM_TABLE_END, AUX_PROGRAM_TABLE_END));	1✔
412	assert_degree_lowering!(ProcessorTable(PROCESSOR_TABLE_END, AUX_PROCESSOR_TABLE_END));	1✔
413	assert_degree_lowering!(OpStackTable(OP_STACK_TABLE_END, AUX_OP_STACK_TABLE_END));	1✔
414	assert_degree_lowering!(RamTable(RAM_TABLE_END, AUX_RAM_TABLE_END));	1✔
415	assert_degree_lowering!(JumpStackTable(	1✔
416	JUMP_STACK_TABLE_END,	1✔
417	AUX_JUMP_STACK_TABLE_END	1✔
418	));	1✔
419	assert_degree_lowering!(HashTable(HASH_TABLE_END, AUX_HASH_TABLE_END));	1✔
420	assert_degree_lowering!(CascadeTable(CASCADE_TABLE_END, AUX_CASCADE_TABLE_END));	1✔
421	assert_degree_lowering!(LookupTable(LOOKUP_TABLE_END, AUX_LOOKUP_TABLE_END));	1✔
422	assert_degree_lowering!(U32Table(U32_TABLE_END, AUX_U32_TABLE_END));	1✔
423	}	1✔
424
425	/// Fills the derived columns of the degree-lowering table using randomly generated rows and
426	/// checks the resulting values for uniqueness. The described method corresponds to an
427	/// application of the Schwartz-Zippel lemma to check uniqueness of the substitution rules
428	/// generated during degree lowering.
429	#[test]
430	#[ignore = "(probably) requires normalization of circuit expressions"]
431	fn substitution_rules_are_unique() {	×
432	let challenges = Challenges::default();	×
NEW 433	let mut main_table_rows =	×
434	Array2::from_shape_fn((2, MasterMainTable::NUM_COLUMNS), \|_\| random());	×
NEW 435	let mut aux_table_rows =	×
436	Array2::from_shape_fn((2, MasterAuxTable::NUM_COLUMNS), \|_\| random());	×
437		×
NEW 438	DegreeLoweringTable::fill_derived_main_columns(main_table_rows.view_mut());	×
439	DegreeLoweringTable::fill_derived_aux_columns(	×
NEW 440	main_table_rows.view(),	×
NEW 441	aux_table_rows.view_mut(),	×
442	&challenges,	×
443	);	×
444		×
445	let mut encountered_values = HashMap::new();	×
446	for col_idx in 0..MasterMainTable::NUM_COLUMNS {	×
NEW 447	let val = main_table_rows[(0, col_idx)].lift();	×
448	let other_entry = encountered_values.insert(val, col_idx);	×
449	if let Some(other_idx) = other_entry {	×
450	panic!("Duplicate value {val} in derived main column {other_idx} and {col_idx}.");	×
451	}	×
452	}
NEW 453	println!("Now comparing auxiliary columns…");	×
454	for col_idx in 0..MasterAuxTable::NUM_COLUMNS {	×
NEW 455	let val = aux_table_rows[(0, col_idx)];	×
456	let other_entry = encountered_values.insert(val, col_idx);	×
457	if let Some(other_idx) = other_entry {	×
458	panic!("Duplicate value {val} in derived aux column {other_idx} and {col_idx}.");	×
459	}	×
460	}
461	}	×
462	}

TritonVM / triton-vm / 10825170249

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous