diff --git a/constraint-evaluation-generator/src/codegen.rs b/constraint-evaluation-generator/src/codegen.rs index 36dd79bd..cea9343b 100644 --- a/constraint-evaluation-generator/src/codegen.rs +++ b/constraint-evaluation-generator/src/codegen.rs @@ -40,7 +40,21 @@ pub(crate) struct TasmBackend { scope: HashSet, /// The number of elements written to the output list. - /// - /// See [`TasmBackend::doc_comment`] for details. elements_written: usize, + + /// Whether the code that is to be generated can assume statically provided + /// addresses for the various input arrays. + input_location_is_static: bool, +} + +#[cfg(test)] +pub mod tests { + use super::*; + + pub fn print_constraints(constraints: &Constraints) { + let code = B::constraint_evaluation_code(constraints); + let syntax_tree = syn::parse2(code).unwrap(); + let code = prettyplease::unparse(&syntax_tree); + println!("{code}"); + } } diff --git a/constraint-evaluation-generator/src/codegen/rust.rs b/constraint-evaluation-generator/src/codegen/rust.rs index 6b4b6198..d2480ebe 100644 --- a/constraint-evaluation-generator/src/codegen/rust.rs +++ b/constraint-evaluation-generator/src/codegen/rust.rs @@ -332,6 +332,8 @@ impl RustBackend { mod tests { use twenty_first::prelude::*; + use crate::codegen::tests::print_constraints; + use super::*; #[test] @@ -352,20 +354,13 @@ mod tests { assert_eq!(expected, RustBackend::tokenize_xfe(xfe).to_string()); } - fn print_constraints_as_rust(constraints: &Constraints) { - let rust = RustBackend::constraint_evaluation_code(constraints); - let syntax_tree = syn::parse2(rust).unwrap(); - let code = prettyplease::unparse(&syntax_tree); - println!("{code}"); - } - #[test] - fn print_mini_constraints_as_rust() { - print_constraints_as_rust(&Constraints::mini_constraints()); + fn print_mini_constraints() { + print_constraints::(&Constraints::mini_constraints()); } #[test] - fn print_test_constraints_as_rust() { - print_constraints_as_rust(&Constraints::test_constraints()); + fn print_test_constraints() { + print_constraints::(&Constraints::test_constraints()); } } diff --git a/constraint-evaluation-generator/src/codegen/tasm.rs b/constraint-evaluation-generator/src/codegen/tasm.rs index 48bc09c2..e6c5e51d 100644 --- a/constraint-evaluation-generator/src/codegen/tasm.rs +++ b/constraint-evaluation-generator/src/codegen/tasm.rs @@ -4,17 +4,18 @@ use itertools::Itertools; use proc_macro2::TokenStream; use quote::quote; use quote::ToTokens; +use twenty_first::prelude::bfe; use twenty_first::prelude::x_field_element::EXTENSION_DEGREE; use twenty_first::prelude::BFieldElement; use twenty_first::prelude::XFieldElement; +use triton_vm::air::memory_layout; use triton_vm::instruction::Instruction; use triton_vm::op_stack::NumberOfWords; use triton_vm::table::constraint_circuit::BinOp; use triton_vm::table::constraint_circuit::CircuitExpression; use triton_vm::table::constraint_circuit::ConstraintCircuit; use triton_vm::table::constraint_circuit::InputIndicator; -use triton_vm::table::TasmConstraintEvaluationMemoryLayout; use crate::codegen::Codegen; use crate::codegen::TasmBackend; @@ -23,17 +24,15 @@ use crate::constraints::Constraints; /// An offset from the [memory layout][layout]'s `free_mem_page_ptr`, in number of /// [`XFieldElement`]s. Indicates the start of the to-be-returned array. /// -/// [layout]: TasmConstraintEvaluationMemoryLayout +/// [layout]: memory_layout::IntegralMemoryLayout const OUT_ARRAY_OFFSET: usize = { - let mem_page_size = TasmConstraintEvaluationMemoryLayout::MEM_PAGE_SIZE; + let mem_page_size = memory_layout::MEM_PAGE_SIZE; let max_num_words_for_evaluated_constraints = 1 << 16; // magic! let out_array_offset_in_words = mem_page_size - max_num_words_for_evaluated_constraints; assert!(out_array_offset_in_words % EXTENSION_DEGREE == 0); out_array_offset_in_words / EXTENSION_DEGREE }; -const OPCODE_PUSH: u64 = Instruction::Push(BFieldElement::new(0)).opcode() as u64; - /// Convenience macro to get raw opcodes of any [`Instruction`] variant, including its argument if /// applicable. /// @@ -54,13 +53,20 @@ macro_rules! instr { /// [push]: triton_vm::instruction::AnInstruction::Push macro_rules! push { ($arg:ident) => {{ + let opcode = u64::from(Instruction::Push(BFieldElement::new(0)).opcode()); let arg = u64::from($arg); - vec![quote!(#OPCODE_PUSH), quote!(#arg)] + vec![quote!(#opcode), quote!(#arg)] }}; - ($list:ident + $offset:ident) => {{ + ($list:ident + $offset:expr) => {{ + let opcode = u64::from(Instruction::Push(BFieldElement::new(0)).opcode()); let offset = u64::try_from($offset).unwrap(); assert!(offset < u64::MAX - BFieldElement::P); - vec![quote!(#OPCODE_PUSH), quote!(#$list + #$offset)] + // clippy will complain about the generated code if it contains `+ 0` + if offset == 0 { + vec![quote!(#opcode), quote!(#$list)] + } else { + vec![quote!(#opcode), quote!(#$list + #offset)] + } }}; } @@ -70,10 +76,9 @@ impl Codegen for TasmBackend { /// /// [tasm]: triton_vm::prelude::triton_asm fn constraint_evaluation_code(constraints: &Constraints) -> TokenStream { - let uses = Self::uses(); - let doc_comment = Self::doc_comment(); + let doc_comment = Self::doc_comment_static_version(); - let mut backend = Self::new(); + let mut backend = Self::statically_known_input_locations(); let init_constraints = backend.tokenize_circuits(&constraints.init()); let cons_constraints = backend.tokenize_circuits(&constraints.cons()); let tran_constraints = backend.tokenize_circuits(&constraints.tran()); @@ -86,11 +91,25 @@ impl Codegen for TasmBackend { + prepare_return_values.len(); let num_instructions = u64::try_from(num_instructions).unwrap(); - quote!( - #uses + let convert_and_decode_assembled_instructions = quote!( + let raw_instructions = raw_instructions + .into_iter() + .map(BFieldElement::new) + .collect::>(); + let program = Program::decode(&raw_instructions).unwrap(); + + let irrelevant_label = |_: &_| String::new(); + program + .into_iter() + .map(|instruction| instruction.map_call_address(irrelevant_label)) + .map(LabelledInstruction::Instruction) + .collect() + ); + + let statically_known_input_locations = quote!( #[doc = #doc_comment] - pub fn air_constraint_evaluation_tasm( - mem_layout: TasmConstraintEvaluationMemoryLayout, + pub fn static_air_constraint_evaluation_tasm( + mem_layout: StaticTasmConstraintEvaluationMemoryLayout, ) -> Vec { let free_mem_page_ptr = mem_layout.free_mem_page_ptr.value(); let curr_base_row_ptr = mem_layout.curr_base_row_ptr.value(); @@ -107,29 +126,75 @@ impl Codegen for TasmBackend { #(#term_constraints,)* #(#prepare_return_values,)* ]; + #convert_and_decode_assembled_instructions + } + ); + + let doc_comment = Self::doc_comment_dynamic_version(); + + let mut backend = Self::dynamically_known_input_locations(); + let move_row_pointers = backend.write_row_pointers_to_ram(); + let init_constraints = backend.tokenize_circuits(&constraints.init()); + let cons_constraints = backend.tokenize_circuits(&constraints.cons()); + let tran_constraints = backend.tokenize_circuits(&constraints.tran()); + let term_constraints = backend.tokenize_circuits(&constraints.term()); + let prepare_return_values = Self::prepare_return_values(); + let num_instructions = move_row_pointers.len() + + init_constraints.len() + + cons_constraints.len() + + tran_constraints.len() + + term_constraints.len() + + prepare_return_values.len(); + let num_instructions = u64::try_from(num_instructions).unwrap(); - let raw_instructions = raw_instructions - .into_iter() - .map(BFieldElement::new) - .collect::>(); - let program = Program::decode(&raw_instructions).unwrap(); - - let irrelevant_label = |_: &_| String::new(); - program - .into_iter() - .map(|instruction| instruction.map_call_address(irrelevant_label)) - .map(LabelledInstruction::Instruction) - .collect() + let dynamically_known_input_locations = quote!( + #[doc = #doc_comment] + pub fn dynamic_air_constraint_evaluation_tasm( + mem_layout: DynamicTasmConstraintEvaluationMemoryLayout, + ) -> Vec { + let num_pointer_pointers = 4; + let free_mem_page_ptr = mem_layout.free_mem_page_ptr.value() + num_pointer_pointers; + let curr_base_row_ptr = mem_layout.free_mem_page_ptr.value(); + let curr_ext_row_ptr = mem_layout.free_mem_page_ptr.value() + 1; + let next_base_row_ptr = mem_layout.free_mem_page_ptr.value() + 2; + let next_ext_row_ptr = mem_layout.free_mem_page_ptr.value() + 3; + let challenges_ptr = mem_layout.challenges_ptr.value(); + + let raw_instructions = vec![ + #num_instructions, + #(#move_row_pointers,)* + #(#init_constraints,)* + #(#cons_constraints,)* + #(#tran_constraints,)* + #(#term_constraints,)* + #(#prepare_return_values,)* + ]; + #convert_and_decode_assembled_instructions } + ); + + let uses = Self::uses(); + quote!( + #uses + #statically_known_input_locations + #dynamically_known_input_locations ) } } impl TasmBackend { - fn new() -> Self { + fn statically_known_input_locations() -> Self { Self { scope: HashSet::new(), elements_written: 0, + input_location_is_static: true, + } + } + + fn dynamically_known_input_locations() -> Self { + Self { + input_location_is_static: false, + ..Self::statically_known_input_locations() } } @@ -139,14 +204,15 @@ impl TasmBackend { use twenty_first::prelude::BFieldElement; use crate::instruction::LabelledInstruction; use crate::Program; - use crate::table::TasmConstraintEvaluationMemoryLayout; + use crate::air::memory_layout::StaticTasmConstraintEvaluationMemoryLayout; + use crate::air::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout; // for rustdoc – https://github.com/rust-lang/rust/issues/74563 #[allow(unused_imports)] use crate::table::extension_table::Quotientable; ) } - fn doc_comment() -> &'static str { + fn doc_comment_static_version() -> &'static str { " The emitted Triton assembly has the following signature: @@ -159,14 +225,56 @@ impl TasmBackend { # Requirements In order for this method to emit Triton assembly, various memory regions need to be - declared. This is done through [`TasmConstraintEvaluationMemoryLayout`]. The memory + declared. This is done through [`StaticTasmConstraintEvaluationMemoryLayout`]. The memory + layout must be [integral]. + + # Guarantees + + - The emitted code does not declare any labels. + - The emitted code is “straight-line”, _i.e._, does not contain any of the instructions + `call`, `return`, `recurse`, `recurse_or_return`, or `skiz`. + - The emitted code does not contain instruction `halt`. + - All memory write access of the emitted code is within the bounds of the memory region + pointed to by `*free_memory_page`. + - `*evaluated_constraints` points to an array of [`XFieldElement`][xfe]s of length + [`NUM_CONSTRAINTS`][total]. Each element is the evaluation of one constraint. In + particular, the disjoint sequence of slices containing + [`NUM_INITIAL_CONSTRAINTS`][init], [`NUM_CONSISTENCY_CONSTRAINTS`][cons], + [`NUM_TRANSITION_CONSTRAINTS`][tran], and [`NUM_TERMINAL_CONSTRAINTS`][term] + (respectively and in this order) correspond to the evaluations of the initial, + consistency, transition, and terminal constraints. + + [integral]: crate::air::memory_layout::IntegralMemoryLayout::is_integral + [xfe]: twenty_first::prelude::XFieldElement + [total]: crate::table::master_table::MasterExtTable::NUM_CONSTRAINTS + [init]: crate::table::master_table::MasterExtTable::NUM_INITIAL_CONSTRAINTS + [cons]: crate::table::master_table::MasterExtTable::NUM_CONSISTENCY_CONSTRAINTS + [tran]: crate::table::master_table::MasterExtTable::NUM_TRANSITION_CONSTRAINTS + [term]: crate::table::master_table::MasterExtTable::NUM_TERMINAL_CONSTRAINTS + " + } + + fn doc_comment_dynamic_version() -> &'static str { + " + The emitted Triton assembly has the following signature: + + # Signature + + ```text + BEFORE: _ *current_main_row *current_aux_row *next_main_row *next_aux_row + AFTER: _ *evaluated_constraints + ``` + # Requirements + + In order for this method to emit Triton assembly, various memory regions need to be + declared. This is done through [`DynamicTasmConstraintEvaluationMemoryLayout`]. The memory layout must be [integral]. # Guarantees - The emitted code does not declare any labels. - The emitted code is “straight-line”, _i.e._, does not contain any of the instructions - `call`, `return`, `recurse`, or `skiz`. + `call`, `return`, `recurse`, `recurse_or_return`, or `skiz`. - The emitted code does not contain instruction `halt`. - All memory write access of the emitted code is within the bounds of the memory region pointed to by `*free_memory_page`. @@ -175,10 +283,10 @@ impl TasmBackend { particular, the disjoint sequence of slices containing [`NUM_INITIAL_CONSTRAINTS`][init], [`NUM_CONSISTENCY_CONSTRAINTS`][cons], [`NUM_TRANSITION_CONSTRAINTS`][tran], and [`NUM_TERMINAL_CONSTRAINTS`][term] - (respectively and in this order) correspond to the evaluations of the initial, consistency, - transition, and terminal constraints. + (respectively and in this order) correspond to the evaluations of the initial, + consistency, transition, and terminal constraints. - [integral]: TasmConstraintEvaluationMemoryLayout::is_integral + [integral]: crate::air::memory_layout::IntegralMemoryLayout::is_integral [xfe]: twenty_first::prelude::XFieldElement [total]: crate::table::master_table::MasterExtTable::NUM_CONSTRAINTS [init]: crate::table::master_table::MasterExtTable::NUM_INITIAL_CONSTRAINTS @@ -188,11 +296,37 @@ impl TasmBackend { " } + /// Moves the dynamic arguments ({current, next} {main, aux} row pointers) + /// to static addresses dedicated to them. + fn write_row_pointers_to_ram(&self) -> Vec { + // BEFORE: _ *current_main_row *current_aux_row *next_main_row *next_aux_row + // AFTER: _ + + let write_pointer_to_ram = |list_id| { + [ + push!(list_id + 0), + instr!(WriteMem(NumberOfWords::N1)), + instr!(Pop(NumberOfWords::N1)), + ] + .concat() + }; + + [ + IOList::NextExtRow, + IOList::NextBaseRow, + IOList::CurrExtRow, + IOList::CurrBaseRow, + ] + .into_iter() + .flat_map(write_pointer_to_ram) + .collect() + } + fn tokenize_circuits( &mut self, constraints: &[ConstraintCircuit], ) -> Vec { - self.reset_scope(); + self.scope = HashSet::new(); let store_shared_nodes = self.store_all_shared_nodes(constraints); // to match the `RustBackend`, base constraints must be emitted first @@ -207,10 +341,6 @@ impl TasmBackend { [store_shared_nodes, write_to_output].concat() } - fn reset_scope(&mut self) { - self.scope = HashSet::new(); - } - fn store_all_shared_nodes( &mut self, constraints: &[ConstraintCircuit], @@ -266,16 +396,19 @@ impl TasmBackend { constraint: &ConstraintCircuit, ) -> Vec { if self.scope.contains(&constraint.id) { - return Self::load_node(constraint); + return self.load_node(constraint); } let CircuitExpression::BinaryOperation(binop, lhs, rhs) = &constraint.expression else { - return Self::load_node(constraint); + return self.load_node(constraint); }; let lhs = self.evaluate_single_node(&lhs.borrow()); let rhs = self.evaluate_single_node(&rhs.borrow()); - let binop = Self::tokenize_bin_op(*binop); + let binop = match binop { + BinOp::Add => instr!(XxAdd), + BinOp::Mul => instr!(XxMul), + }; [lhs, rhs, binop].concat() } @@ -290,11 +423,11 @@ impl TasmBackend { [evaluated_constraint, store_element].concat() } - fn load_node(circuit: &ConstraintCircuit) -> Vec { + fn load_node(&self, circuit: &ConstraintCircuit) -> Vec { match circuit.expression { CircuitExpression::BConstant(bfe) => Self::load_ext_field_constant(bfe.into()), CircuitExpression::XConstant(xfe) => Self::load_ext_field_constant(xfe), - CircuitExpression::Input(input) => Self::load_input(input), + CircuitExpression::Input(input) => self.load_input(input), CircuitExpression::Challenge(challenge_idx) => Self::load_challenge(challenge_idx), CircuitExpression::BinaryOperation(_, _, _) => Self::load_evaluated_bin_op(circuit.id), } @@ -305,14 +438,18 @@ impl TasmBackend { [c2, c1, c0].concat() } - fn load_input(input: II) -> Vec { + fn load_input(&self, input: II) -> Vec { let list = match (input.is_current_row(), input.is_base_table_column()) { (true, true) => IOList::CurrBaseRow, (true, false) => IOList::CurrExtRow, (false, true) => IOList::NextBaseRow, (false, false) => IOList::NextExtRow, }; - Self::load_ext_field_element_from_list(list, input.column()) + if self.input_location_is_static { + Self::load_ext_field_element_from_list(list, input.column()) + } else { + Self::load_ext_field_element_from_pointed_to_list(list, input.column()) + } } fn load_challenge(challenge_idx: usize) -> Vec { @@ -324,16 +461,38 @@ impl TasmBackend { } fn load_ext_field_element_from_list(list: IOList, element_index: usize) -> Vec { + let word_index = Self::element_index_to_word_index_for_reading(element_index); + + [ + push!(list + word_index), + instr!(ReadMem(NumberOfWords::N3)), + instr!(Pop(NumberOfWords::N1)), + ] + .concat() + } + + fn load_ext_field_element_from_pointed_to_list( + list: IOList, + element_index: usize, + ) -> Vec { + let word_index = Self::element_index_to_word_index_for_reading(element_index); + + [ + push!(list + 0), + instr!(ReadMem(NumberOfWords::N1)), + instr!(Pop(NumberOfWords::N1)), + instr!(AddI(word_index)), + instr!(ReadMem(NumberOfWords::N3)), + instr!(Pop(NumberOfWords::N1)), + ] + .concat() + } + + fn element_index_to_word_index_for_reading(element_index: usize) -> BFieldElement { let word_offset = element_index * EXTENSION_DEGREE; let start_to_read_offset = EXTENSION_DEGREE - 1; let word_index = word_offset + start_to_read_offset; - let word_index = u64::try_from(word_index).unwrap(); - - let push_address = push!(list + word_index); - let read_mem = instr!(ReadMem(NumberOfWords::N3)); - let pop = instr!(Pop(NumberOfWords::N1)); - - [push_address, read_mem, pop].concat() + bfe!(u64::try_from(word_index).unwrap()) } fn store_ext_field_element(element_index: usize) -> Vec { @@ -349,13 +508,6 @@ impl TasmBackend { [push_address, write_mem, pop].concat() } - fn tokenize_bin_op(binop: BinOp) -> Vec { - match binop { - BinOp::Add => instr!(XxAdd), - BinOp::Mul => instr!(XxMul), - } - } - fn prepare_return_values() -> Vec { let free_mem_page = IOList::FreeMemPage; let out_array_offset_in_num_bfes = OUT_ARRAY_OFFSET * EXTENSION_DEGREE; @@ -389,22 +541,17 @@ impl ToTokens for IOList { #[cfg(test)] mod tests { - use super::*; + use crate::codegen::tests::print_constraints; - fn print_constraints_as_tasm(constraints: &Constraints) { - let tasm = TasmBackend::constraint_evaluation_code(constraints); - let syntax_tree = syn::parse2(tasm).unwrap(); - let code = prettyplease::unparse(&syntax_tree); - println!("{code}"); - } + use super::*; #[test] - fn print_mini_constraints_as_tasm() { - print_constraints_as_tasm(&Constraints::mini_constraints()); + fn print_mini_constraints() { + print_constraints::(&Constraints::mini_constraints()); } #[test] - fn print_test_constraints_as_tasm() { - print_constraints_as_tasm(&Constraints::test_constraints()); + fn print_test_constraints() { + print_constraints::(&Constraints::test_constraints()); } } diff --git a/constraint-evaluation-generator/src/main.rs b/constraint-evaluation-generator/src/main.rs index 24f80652..44b74a2f 100644 --- a/constraint-evaluation-generator/src/main.rs +++ b/constraint-evaluation-generator/src/main.rs @@ -17,9 +17,8 @@ #![warn(missing_debug_implementations)] #![warn(missing_docs)] -use std::fs::write; - use proc_macro2::TokenStream; +use std::fs::write; use crate::codegen::Codegen; use crate::codegen::RustBackend; @@ -39,16 +38,18 @@ fn main() { let rust = RustBackend::constraint_evaluation_code(&constraints); let tasm = TasmBackend::constraint_evaluation_code(&constraints); - write_code_to_file(degree_lowering_table_code, "degree_lowering_table"); - write_code_to_file(rust, "constraints"); - write_code_to_file(tasm, "tasm_air_constraints"); + write_code_to_file( + degree_lowering_table_code, + "triton-vm/src/table/degree_lowering_table.rs", + ); + write_code_to_file(rust, "triton-vm/src/table/constraints.rs"); + write_code_to_file(tasm, "triton-vm/src/air/tasm_air_constraints.rs"); } fn write_code_to_file(code: TokenStream, file_name: &str) { let syntax_tree = syn::parse2(code).unwrap(); let code = prettyplease::unparse(&syntax_tree); - let path = format!("triton-vm/src/table/{file_name}.rs"); - write(path, code).unwrap(); + write(file_name, code).unwrap(); } #[cfg(test)] diff --git a/specification/src/arithmetization-overview.md b/specification/src/arithmetization-overview.md index 18fa8537..86be89cd 100644 --- a/specification/src/arithmetization-overview.md +++ b/specification/src/arithmetization-overview.md @@ -4,20 +4,20 @@ -| table name | #main cols | #aux cols | total width | -|:-------------------------------------------|-----------:|----------:|------------:| -| [ProgramTable](program-table.md) | 7 | 3 | 16 | -| [ProcessorTable](processor-table.md) | 39 | 11 | 72 | -| [OpStackTable](operational-stack-table.md) | 4 | 2 | 10 | -| [RamTable](random-access-memory-table.md) | 7 | 6 | 25 | -| [JumpStackTable](jump-stack-table.md) | 5 | 2 | 11 | -| [HashTable](hash-table.md) | 67 | 20 | 127 | -| [CascadeTable](cascade-table.md) | 6 | 2 | 12 | -| [LookupTable](lookup-table.md) | 4 | 2 | 10 | -| [U32Table](u32-table.md) | 10 | 1 | 13 | -| DegreeLowering | 203 | 36 | 311 | -| Randomizers | 0 | 1 | 3 | -| **TOTAL** | **352** | **86** | **610** | +| table name | #main cols | #aux cols | total width | +|:-------------------------------------------|----------------:|-----------------:|----------------:| +| [ProgramTable](program-table.md) | 7 | 3 | 16 | +| [ProcessorTable](processor-table.md) | 39 | 11 | 72 | +| [OpStackTable](operational-stack-table.md) | 4 | 2 | 10 | +| [RamTable](random-access-memory-table.md) | 7 | 6 | 25 | +| [JumpStackTable](jump-stack-table.md) | 5 | 2 | 11 | +| [HashTable](hash-table.md) | 67 | 20 | 127 | +| [CascadeTable](cascade-table.md) | 6 | 2 | 12 | +| [LookupTable](lookup-table.md) | 4 | 2 | 10 | +| [U32Table](u32-table.md) | 10 | 1 | 13 | +| DegreeLowering (-/8/4) | 0/111/203 | 0/14/36 | 0/153/311 | +| Randomizers | 0 | 1 | 3 | +| **TOTAL** | **149/260/352** | **50/64/86** | **299/452/610** | ## Constraints @@ -44,8 +44,26 @@ Before automatic degree lowering: | [U32Table](u32-table.md) | 1 | 15 | 22 | 2 | 12 | | [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | 1 | | **TOTAL** | **79** | **76** | **150** | **23** | **19** | +| (# nodes) | (534) | (624) | (6077) | (213) | | -After automatically lowering degree to 4: +After lowering degree to 8: + +| table name | #initial | #consistency | #transition | #terminal | +|:-----------------------------------------------|---------:|-------------:|------------:|----------:| +| [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 | +| [ProcessorTable](processor-table.md) | 29 | 10 | 158 | 1 | +| [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 | +| [RamTable](random-access-memory-table.md) | 7 | 0 | 12 | 1 | +| [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 | +| [HashTable](hash-table.md) | 22 | 46 | 49 | 2 | +| [CascadeTable](cascade-table.md) | 2 | 1 | 3 | 0 | +| [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 | +| [U32Table](u32-table.md) | 1 | 18 | 24 | 2 | +| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | +| **TOTAL** | **79** | **80** | **271** | **23** | +| (# nodes) | (534) | (635) | (6335) | (213) | + +After lowering degree to 4: | table name | #initial | #consistency | #transition | #terminal | |:-----------------------------------------------|---------:|-------------:|------------:|----------:| @@ -60,6 +78,7 @@ After automatically lowering degree to 4: | [U32Table](u32-table.md) | 1 | 26 | 34 | 2 | | [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | | **TOTAL** | **81** | **94** | **369** | **23** | +| (# nodes) | (538) | (676) | (6557) | (213) | @@ -69,9 +88,10 @@ Triton VM's recursive verifier needs to evaluate Triton VM's AIR constraints. In order to gauge the runtime cost for this step, the following table provides estimates for that step's contribution to various tables. -| Processor | Op Stack | RAM | -|----------:|---------:|------:| -| 34609 | 64237 | 22716 | +| Type | Processor | Op Stack | RAM | +|:-------------|----------:|---------:|------:| +| static | 34609 | 64237 | 22716 | +| dynamic | 45793 | 71697 | 26444 | ## Opcode Pressure diff --git a/triton-vm/src/air.rs b/triton-vm/src/air.rs new file mode 100644 index 00000000..2ea2033a --- /dev/null +++ b/triton-vm/src/air.rs @@ -0,0 +1,270 @@ +pub mod memory_layout; +#[rustfmt::skip] +pub mod tasm_air_constraints; + +#[cfg(test)] +mod test { + use itertools::Itertools; + use ndarray::Array1; + use proptest::collection::vec; + use proptest::prelude::*; + use proptest_arbitrary_interop::arb; + use std::collections::HashMap; + use test_strategy::proptest; + use twenty_first::prelude::x_field_element::EXTENSION_DEGREE; + use twenty_first::prelude::*; + + use crate::air::tasm_air_constraints::dynamic_air_constraint_evaluation_tasm; + use crate::air::tasm_air_constraints::static_air_constraint_evaluation_tasm; + use crate::instruction::AnInstruction; + use crate::prelude::*; + use crate::table::challenges::Challenges; + use crate::table::extension_table::Evaluable; + use crate::table::extension_table::Quotientable; + use crate::table::master_table::MasterExtTable; + use crate::table::NUM_BASE_COLUMNS; + use crate::table::NUM_EXT_COLUMNS; + + use super::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout; + use super::memory_layout::IntegralMemoryLayout; + use super::memory_layout::StaticTasmConstraintEvaluationMemoryLayout; + use super::*; + + #[derive(Debug, Clone, test_strategy::Arbitrary)] + struct ConstraintEvaluationPoint { + #[strategy(vec(arb(), NUM_BASE_COLUMNS))] + #[map(Array1::from)] + curr_base_row: Array1, + + #[strategy(vec(arb(), NUM_EXT_COLUMNS))] + #[map(Array1::from)] + curr_ext_row: Array1, + + #[strategy(vec(arb(), NUM_BASE_COLUMNS))] + #[map(Array1::from)] + next_base_row: Array1, + + #[strategy(vec(arb(), NUM_EXT_COLUMNS))] + #[map(Array1::from)] + next_ext_row: Array1, + + #[strategy(arb())] + challenges: Challenges, + + #[strategy(arb())] + #[filter(#static_memory_layout.is_integral())] + static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout, + } + + impl ConstraintEvaluationPoint { + fn evaluate_all_constraints_rust(&self) -> Vec { + let init = MasterExtTable::evaluate_initial_constraints( + self.curr_base_row.view(), + self.curr_ext_row.view(), + &self.challenges, + ); + let cons = MasterExtTable::evaluate_consistency_constraints( + self.curr_base_row.view(), + self.curr_ext_row.view(), + &self.challenges, + ); + let tran = MasterExtTable::evaluate_transition_constraints( + self.curr_base_row.view(), + self.curr_ext_row.view(), + self.next_base_row.view(), + self.next_ext_row.view(), + &self.challenges, + ); + let term = MasterExtTable::evaluate_terminal_constraints( + self.curr_base_row.view(), + self.curr_ext_row.view(), + &self.challenges, + ); + + [init, cons, tran, term].concat() + } + + fn evaluate_all_constraints_tasm_static(&self) -> Vec { + let program = self.tasm_static_constraint_evaluation_code(); + let mut vm_state = + self.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(&program); + + vm_state.run().unwrap(); + + let output_list_ptr = vm_state.op_stack.pop().unwrap().value(); + let num_quotients = MasterExtTable::NUM_CONSTRAINTS; + Self::read_xfe_list_at_address(vm_state.ram, output_list_ptr, num_quotients) + } + + fn evaluate_all_constraints_tasm_dynamic(&self) -> Vec { + let program = self.tasm_dynamic_constraint_evaluation_code(); + let mut vm_state = + self.set_up_triton_vm_to_evaluate_constraints_in_tasm_dynamic(&program); + + vm_state.run().unwrap(); + + let output_list_ptr = vm_state.op_stack.pop().unwrap().value(); + let num_quotients = MasterExtTable::NUM_CONSTRAINTS; + Self::read_xfe_list_at_address(vm_state.ram, output_list_ptr, num_quotients) + } + + fn tasm_static_constraint_evaluation_code(&self) -> Program { + let mut source_code = static_air_constraint_evaluation_tasm(self.static_memory_layout); + source_code.push(triton_instr!(halt)); + Program::new(&source_code) + } + + fn tasm_dynamic_constraint_evaluation_code(&self) -> Program { + let dynamic_memory_layout = DynamicTasmConstraintEvaluationMemoryLayout { + free_mem_page_ptr: self.static_memory_layout.free_mem_page_ptr, + challenges_ptr: self.static_memory_layout.challenges_ptr, + }; + let mut source_code = dynamic_air_constraint_evaluation_tasm(dynamic_memory_layout); + source_code.push(triton_instr!(halt)); + Program::new(&source_code) + } + + fn set_up_triton_vm_to_evaluate_constraints_in_tasm_static( + &self, + program: &Program, + ) -> VMState { + let curr_base_row_ptr = self.static_memory_layout.curr_base_row_ptr; + let curr_ext_row_ptr = self.static_memory_layout.curr_ext_row_ptr; + let next_base_row_ptr = self.static_memory_layout.next_base_row_ptr; + let next_ext_row_ptr = self.static_memory_layout.next_ext_row_ptr; + let challenges_ptr = self.static_memory_layout.challenges_ptr; + + let mut ram = HashMap::default(); + Self::extend_ram_at_address(&mut ram, self.curr_base_row.to_vec(), curr_base_row_ptr); + Self::extend_ram_at_address(&mut ram, self.curr_ext_row.to_vec(), curr_ext_row_ptr); + Self::extend_ram_at_address(&mut ram, self.next_base_row.to_vec(), next_base_row_ptr); + Self::extend_ram_at_address(&mut ram, self.next_ext_row.to_vec(), next_ext_row_ptr); + Self::extend_ram_at_address(&mut ram, self.challenges.challenges, challenges_ptr); + let non_determinism = NonDeterminism::default().with_ram(ram); + + VMState::new(program, PublicInput::default(), non_determinism) + } + + fn set_up_triton_vm_to_evaluate_constraints_in_tasm_dynamic( + &self, + program: &Program, + ) -> VMState { + // for convenience, reuse the (integral) static memory layout + let mut vm_state = + self.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(program); + vm_state + .op_stack + .push(self.static_memory_layout.curr_base_row_ptr); + vm_state + .op_stack + .push(self.static_memory_layout.curr_ext_row_ptr); + vm_state + .op_stack + .push(self.static_memory_layout.next_base_row_ptr); + vm_state + .op_stack + .push(self.static_memory_layout.next_ext_row_ptr); + vm_state + } + + fn extend_ram_at_address( + ram: &mut HashMap, + list: impl IntoIterator>, + address: BFieldElement, + ) { + let list = list.into_iter().flat_map(|xfe| xfe.into().coefficients); + let indexed_list = list.enumerate(); + let offset_address = |i| bfe!(i as u64) + address; + let ram_extension = indexed_list.map(|(i, bfe)| (offset_address(i), bfe)); + ram.extend(ram_extension); + } + + fn read_xfe_list_at_address( + ram: HashMap, + address: u64, + len: usize, + ) -> Vec { + let mem_region_end = address + (len * EXTENSION_DEGREE) as u64; + (address..mem_region_end) + .map(BFieldElement::new) + .map(|i| ram[&i]) + .chunks(EXTENSION_DEGREE) + .into_iter() + .map(|c| XFieldElement::try_from(c.collect_vec()).unwrap()) + .collect() + } + } + + #[proptest] + fn triton_constraints_and_assembly_constraints_agree(point: ConstraintEvaluationPoint) { + let all_constraints_rust = point.evaluate_all_constraints_rust(); + let all_constraints_tasm_static = point.evaluate_all_constraints_tasm_static(); + prop_assert_eq!(all_constraints_rust.clone(), all_constraints_tasm_static); + + let all_constraints_tasm_dynamic = point.evaluate_all_constraints_tasm_dynamic(); + prop_assert_eq!(all_constraints_rust, all_constraints_tasm_dynamic); + } + + #[proptest] + fn triton_assembly_constraint_evaluators_do_not_write_outside_of_dedicated_memory_region( + point: ConstraintEvaluationPoint, + ) { + let program = point.tasm_static_constraint_evaluation_code(); + let mut initial_state = + point.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(&program); + let mut terminal_state = initial_state.clone(); + terminal_state.run().unwrap(); + + let free_mem_page_ptr = point.static_memory_layout.free_mem_page_ptr; + let mem_page_size = memory_layout::MEM_PAGE_SIZE; + let mem_page = memory_layout::MemoryRegion::new(free_mem_page_ptr, mem_page_size); + let not_in_mem_page = |addr: &_| !mem_page.contains_address(addr); + + initial_state.ram.retain(|k, _| not_in_mem_page(k)); + terminal_state.ram.retain(|k, _| not_in_mem_page(k)); + prop_assert_eq!(initial_state.ram, terminal_state.ram); + } + + #[proptest] + fn triton_assembly_constraint_evaluators_declare_no_labels( + #[strategy(arb())] static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout, + #[strategy(arb())] dynamic_memory_layout: DynamicTasmConstraintEvaluationMemoryLayout, + ) { + for instruction in static_air_constraint_evaluation_tasm(static_memory_layout) + .into_iter() + .chain(dynamic_air_constraint_evaluation_tasm( + dynamic_memory_layout, + )) + { + if let LabelledInstruction::Label(label) = instruction { + return Err(TestCaseError::Fail(format!("Found label: {label}").into())); + } + } + } + + #[proptest] + fn triton_assembly_constraint_evaluators_are_straight_line_and_does_not_halt( + #[strategy(arb())] static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout, + #[strategy(arb())] dynamic_memory_layout: DynamicTasmConstraintEvaluationMemoryLayout, + ) { + type I = AnInstruction; + let is_legal = |instruction| { + !matches!( + instruction, + I::Call(_) | I::Return | I::Recurse | I::RecurseOrReturn | I::Skiz | I::Halt + ) + }; + + for instruction in static_air_constraint_evaluation_tasm(static_memory_layout) { + if let LabelledInstruction::Instruction(instruction) = instruction { + prop_assert!(is_legal(instruction)); + } + } + + for instruction in dynamic_air_constraint_evaluation_tasm(dynamic_memory_layout) { + if let LabelledInstruction::Instruction(instruction) = instruction { + prop_assert!(is_legal(instruction)); + } + } + } +} diff --git a/triton-vm/src/air/memory_layout.rs b/triton-vm/src/air/memory_layout.rs new file mode 100644 index 00000000..c5d929bf --- /dev/null +++ b/triton-vm/src/air/memory_layout.rs @@ -0,0 +1,210 @@ +use arbitrary::Arbitrary; +use itertools::Itertools; +use twenty_first::prelude::*; + +use crate::table::challenges::Challenges; +use crate::table::NUM_BASE_COLUMNS; +use crate::table::NUM_EXT_COLUMNS; + +/// The minimal required size of a memory page in [`BFieldElement`]s. +pub const MEM_PAGE_SIZE: usize = 1 << 32; + +/// Memory layout guarantees for the [Triton assembly AIR constraint evaluator][tasm_air] +/// with input lists at dynamically known memory locations. +/// +/// [tasm_air]: crate::air::tasm_air_constraints::dynamic_air_constraint_evaluation_tasm +#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Arbitrary)] +pub struct DynamicTasmConstraintEvaluationMemoryLayout { + /// Pointer to a region of memory that is reserved for (a) pointers to {current, + /// next} {main, aux} rows, and (b) intermediate values in the course of + /// constraint evaluation. The size of the region must be at least + /// [`MEM_PAGE_SIZE`] [`BFieldElement`]s. + pub free_mem_page_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_CHALLENGES`][num_challenges]. + /// + /// [num_challenges]: Challenges::COUNT + pub challenges_ptr: BFieldElement, +} + +/// Memory layout guarantees for the [Triton assembly AIR constraint evaluator][tasm_air] +/// with input lists at statically known memory locations. +/// +/// [tasm_air]: crate::air::tasm_air_constraints::static_air_constraint_evaluation_tasm +#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Arbitrary)] +pub struct StaticTasmConstraintEvaluationMemoryLayout { + /// Pointer to a region of memory that is reserved for constraint evaluation. + /// The size of the region must be at least [`MEM_PAGE_SIZE`] [`BFieldElement`]s. + pub free_mem_page_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_BASE_COLUMNS`]. + pub curr_base_row_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_EXT_COLUMNS`]. + pub curr_ext_row_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_BASE_COLUMNS`]. + pub next_base_row_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_EXT_COLUMNS`]. + pub next_ext_row_ptr: BFieldElement, + + /// Pointer to an array of [`XFieldElement`]s of length [`NUM_CHALLENGES`][num_challenges]. + /// + /// [num_challenges]: Challenges::COUNT + pub challenges_ptr: BFieldElement, +} + +pub trait IntegralMemoryLayout { + /// Determine if the memory layout's constraints are met, _i.e._, whether the + /// various pointers point to large enough regions of memory. + fn is_integral(&self) -> bool { + let memory_regions = self.memory_regions(); + if memory_regions.iter().unique().count() != memory_regions.len() { + return false; + } + + let disjoint_from_all_others = |region| { + let mut all_other_regions = memory_regions.iter().filter(|&r| r != region); + all_other_regions.all(|r| r.disjoint_from(region)) + }; + memory_regions.iter().all(disjoint_from_all_others) + } + + fn memory_regions(&self) -> Box<[MemoryRegion]>; +} + +impl IntegralMemoryLayout for StaticTasmConstraintEvaluationMemoryLayout { + fn memory_regions(&self) -> Box<[MemoryRegion]> { + let all_regions = [ + MemoryRegion::new(self.free_mem_page_ptr, MEM_PAGE_SIZE), + MemoryRegion::new(self.curr_base_row_ptr, NUM_BASE_COLUMNS), + MemoryRegion::new(self.curr_ext_row_ptr, NUM_EXT_COLUMNS), + MemoryRegion::new(self.next_base_row_ptr, NUM_BASE_COLUMNS), + MemoryRegion::new(self.next_ext_row_ptr, NUM_EXT_COLUMNS), + MemoryRegion::new(self.challenges_ptr, Challenges::COUNT), + ]; + Box::new(all_regions) + } +} + +impl IntegralMemoryLayout for DynamicTasmConstraintEvaluationMemoryLayout { + fn memory_regions(&self) -> Box<[MemoryRegion]> { + let all_regions = [ + MemoryRegion::new(self.free_mem_page_ptr, MEM_PAGE_SIZE), + MemoryRegion::new(self.challenges_ptr, Challenges::COUNT), + ]; + Box::new(all_regions) + } +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)] +pub struct MemoryRegion { + start: u64, + size: u64, +} + +impl MemoryRegion { + pub fn new>(address: A, size: usize) -> Self { + let start = address.into(); + let size = u64::try_from(size).unwrap(); + Self { start, size } + } + + pub fn disjoint_from(self, other: &Self) -> bool { + !self.overlaps(other) + } + + pub fn overlaps(self, other: &Self) -> bool { + self.contains_address(other.start) || other.contains_address(self.start) + } + + pub fn contains_address>(self, addr: A) -> bool { + (self.start..self.start + self.size).contains(&addr.into()) + } +} + +#[cfg(test)] +mod tests { + use proptest::prelude::*; + use proptest_arbitrary_interop::arb; + use test_strategy::proptest; + use twenty_first::bfe; + + use super::*; + + impl Default for StaticTasmConstraintEvaluationMemoryLayout { + /// For testing purposes only. + fn default() -> Self { + let mem_page_size = MEM_PAGE_SIZE as u64; + let mem_page = |i| bfe!(i * mem_page_size); + StaticTasmConstraintEvaluationMemoryLayout { + free_mem_page_ptr: mem_page(0), + curr_base_row_ptr: mem_page(1), + curr_ext_row_ptr: mem_page(2), + next_base_row_ptr: mem_page(3), + next_ext_row_ptr: mem_page(4), + challenges_ptr: mem_page(5), + } + } + } + + impl Default for DynamicTasmConstraintEvaluationMemoryLayout { + /// For testing purposes only. + fn default() -> Self { + let mem_page_size = MEM_PAGE_SIZE as u64; + let mem_page = |i| bfe!(i * mem_page_size); + DynamicTasmConstraintEvaluationMemoryLayout { + free_mem_page_ptr: mem_page(0), + challenges_ptr: mem_page(1), + } + } + } + + #[proptest] + fn size_0_memory_region_contains_no_addresses( + #[strategy(arb())] region_start: BFieldElement, + #[strategy(arb())] address: BFieldElement, + ) { + let region = MemoryRegion::new(region_start, 0); + prop_assert!(!region.contains_address(region_start)); + prop_assert!(!region.contains_address(address)); + } + + #[proptest] + fn size_1_memory_region_contains_only_start_address( + #[strategy(arb())] region_start: BFieldElement, + #[strategy(arb())] + #[filter(#region_start != #address)] + address: BFieldElement, + ) { + let region = MemoryRegion::new(region_start, 1); + prop_assert!(region.contains_address(region_start)); + prop_assert!(!region.contains_address(address)); + } + + #[test] + fn definitely_integral_memory_layout_is_detected_as_integral() { + assert!(StaticTasmConstraintEvaluationMemoryLayout::default().is_integral()); + assert!(DynamicTasmConstraintEvaluationMemoryLayout::default().is_integral()); + } + + #[test] + fn definitely_non_integral_memory_layout_is_detected_as_non_integral() { + let layout = StaticTasmConstraintEvaluationMemoryLayout { + free_mem_page_ptr: bfe!(0), + curr_base_row_ptr: bfe!(1), + curr_ext_row_ptr: bfe!(2), + next_base_row_ptr: bfe!(3), + next_ext_row_ptr: bfe!(4), + challenges_ptr: bfe!(5), + }; + assert!(!layout.is_integral()); + + let layout = DynamicTasmConstraintEvaluationMemoryLayout { + free_mem_page_ptr: bfe!(0), + challenges_ptr: bfe!(5), + }; + assert!(!layout.is_integral()); + } +} diff --git a/triton-vm/src/air/tasm_air_constraints.rs b/triton-vm/src/air/tasm_air_constraints.rs new file mode 100644 index 00000000..4c9c0b1a --- /dev/null +++ b/triton-vm/src/air/tasm_air_constraints.rs @@ -0,0 +1,20 @@ +//! This file is a placeholder for auto-generated code +//! Run `cargo run --bin constraint-evaluation-generator` +//! to fill in this file with optimized constraints. + +use crate::air::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout; +use crate::air::memory_layout::StaticTasmConstraintEvaluationMemoryLayout; +use crate::instruction::LabelledInstruction; +use crate::table::constraints::ERROR_MESSAGE_GENERATE_CONSTRAINTS; + +pub fn static_air_constraint_evaluation_tasm( + _: StaticTasmConstraintEvaluationMemoryLayout, +) -> Vec { + panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}"); +} + +pub fn dynamic_air_constraint_evaluation_tasm( + _: DynamicTasmConstraintEvaluationMemoryLayout, +) -> Vec { + panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}"); +} diff --git a/triton-vm/src/lib.rs b/triton-vm/src/lib.rs index 3e1ffa55..538cad66 100644 --- a/triton-vm/src/lib.rs +++ b/triton-vm/src/lib.rs @@ -167,6 +167,7 @@ use crate::error::ProvingError; use crate::prelude::*; pub mod aet; +pub mod air; pub mod arithmetic_domain; pub mod config; pub mod error; @@ -695,7 +696,8 @@ mod tests { implements_auto_traits::(); implements_auto_traits::(); implements_auto_traits::(); - implements_auto_traits::(); + implements_auto_traits::(); + implements_auto_traits::(); // other implements_auto_traits::(); diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index f75a98c3..34cabe92 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -1327,15 +1327,11 @@ pub(crate) mod tests { use strum::IntoEnumIterator; use test_strategy::proptest; use twenty_first::math::other::random_elements; - use twenty_first::prelude::x_field_element::EXTENSION_DEGREE; use crate::error::InstructionError; use crate::example_programs::*; - use crate::instruction::AnInstruction; use crate::instruction::Instruction; - use crate::instruction::LabelledInstruction; use crate::op_stack::OpStackElement; - use crate::prelude::Program; use crate::program::NonDeterminism; use crate::shared_tests::*; use crate::table::cascade_table::ExtCascadeTable; @@ -1365,14 +1361,9 @@ pub(crate) mod tests { use crate::table::table_column::ProcessorExtTableColumn::InputTableEvalArg; use crate::table::table_column::ProcessorExtTableColumn::OutputTableEvalArg; use crate::table::table_column::RamBaseTableColumn; - use crate::table::tasm_air_constraints::air_constraint_evaluation_tasm; use crate::table::u32_table::ExtU32Table; - use crate::table::MemoryRegion; - use crate::table::TasmConstraintEvaluationMemoryLayout; - use crate::triton_instr; use crate::triton_program; use crate::vm::tests::*; - use crate::vm::VMState; use crate::PublicInput; use super::*; @@ -2554,7 +2545,7 @@ pub(crate) mod tests { } #[proptest] - fn polynomial_segments_are_coherent_with_the_polynomial_they_originate_from( + fn polynomial_segments_cohere_with_originating_polynomial( #[strategy(2_usize..8)] log_trace_length: usize, #[strategy(1_usize..#log_trace_length.min(3))] log_num_segments: usize, #[strategy(1_usize..6)] log_expansion_factor: usize, @@ -2608,174 +2599,6 @@ pub(crate) mod tests { prop_assert_eq!(segments_codewords, actual_segment_codewords); } - #[derive(Debug, Clone, test_strategy::Arbitrary)] - struct ConstraintEvaluationPoint { - #[strategy(vec(arb(), NUM_BASE_COLUMNS))] - #[map(Array1::from)] - curr_base_row: Array1, - - #[strategy(vec(arb(), NUM_EXT_COLUMNS))] - #[map(Array1::from)] - curr_ext_row: Array1, - - #[strategy(vec(arb(), NUM_BASE_COLUMNS))] - #[map(Array1::from)] - next_base_row: Array1, - - #[strategy(vec(arb(), NUM_EXT_COLUMNS))] - #[map(Array1::from)] - next_ext_row: Array1, - - #[strategy(arb())] - challenges: Challenges, - - #[strategy(arb())] - #[filter(#memory_layout.is_integral())] - memory_layout: TasmConstraintEvaluationMemoryLayout, - } - - impl ConstraintEvaluationPoint { - fn evaluate_all_constraints_rust(&self) -> Vec { - let init = MasterExtTable::evaluate_initial_constraints( - self.curr_base_row.view(), - self.curr_ext_row.view(), - &self.challenges, - ); - let cons = MasterExtTable::evaluate_consistency_constraints( - self.curr_base_row.view(), - self.curr_ext_row.view(), - &self.challenges, - ); - let tran = MasterExtTable::evaluate_transition_constraints( - self.curr_base_row.view(), - self.curr_ext_row.view(), - self.next_base_row.view(), - self.next_ext_row.view(), - &self.challenges, - ); - let term = MasterExtTable::evaluate_terminal_constraints( - self.curr_base_row.view(), - self.curr_ext_row.view(), - &self.challenges, - ); - - [init, cons, tran, term].concat() - } - - fn evaluate_all_constraints_tasm(&self) -> Vec { - let program = self.tasm_constraint_evaluation_code(); - let mut vm_state = self.set_up_triton_vm_to_evaluate_constraints_in_tasm(&program); - - vm_state.run().unwrap(); - - let output_list_ptr = vm_state.op_stack.pop().unwrap().value(); - let num_quotients = MasterExtTable::NUM_CONSTRAINTS; - Self::read_xfe_list_at_address(vm_state.ram, output_list_ptr, num_quotients) - } - - fn tasm_constraint_evaluation_code(&self) -> Program { - let mut source_code = air_constraint_evaluation_tasm(self.memory_layout); - source_code.push(triton_instr!(halt)); - Program::new(&source_code) - } - - fn set_up_triton_vm_to_evaluate_constraints_in_tasm(&self, program: &Program) -> VMState { - let curr_base_row_ptr = self.memory_layout.curr_base_row_ptr; - let curr_ext_row_ptr = self.memory_layout.curr_ext_row_ptr; - let next_base_row_ptr = self.memory_layout.next_base_row_ptr; - let next_ext_row_ptr = self.memory_layout.next_ext_row_ptr; - let challenges_ptr = self.memory_layout.challenges_ptr; - - let mut ram = HashMap::default(); - Self::extend_ram_at_address(&mut ram, self.curr_base_row.to_vec(), curr_base_row_ptr); - Self::extend_ram_at_address(&mut ram, self.curr_ext_row.to_vec(), curr_ext_row_ptr); - Self::extend_ram_at_address(&mut ram, self.next_base_row.to_vec(), next_base_row_ptr); - Self::extend_ram_at_address(&mut ram, self.next_ext_row.to_vec(), next_ext_row_ptr); - Self::extend_ram_at_address(&mut ram, self.challenges.challenges, challenges_ptr); - let non_determinism = NonDeterminism::default().with_ram(ram); - - VMState::new(program, PublicInput::default(), non_determinism) - } - - fn extend_ram_at_address( - ram: &mut HashMap, - list: impl IntoIterator>, - address: BFieldElement, - ) { - let list = list.into_iter().flat_map(|xfe| xfe.into().coefficients); - let indexed_list = list.enumerate(); - let offset_address = |i| bfe!(i as u64) + address; - let ram_extension = indexed_list.map(|(i, bfe)| (offset_address(i), bfe)); - ram.extend(ram_extension); - } - - fn read_xfe_list_at_address( - ram: HashMap, - address: u64, - len: usize, - ) -> Vec { - let mem_region_end = address + (len * EXTENSION_DEGREE) as u64; - (address..mem_region_end) - .map(BFieldElement::new) - .map(|i| ram[&i]) - .chunks(EXTENSION_DEGREE) - .into_iter() - .map(|c| XFieldElement::try_from(c.collect_vec()).unwrap()) - .collect() - } - } - - #[proptest] - fn triton_constraints_and_assembly_constraints_agree(point: ConstraintEvaluationPoint) { - let all_constraints_rust = point.evaluate_all_constraints_rust(); - let all_constraints_tasm = point.evaluate_all_constraints_tasm(); - prop_assert_eq!(all_constraints_rust, all_constraints_tasm); - } - - #[proptest] - fn triton_assembly_constraint_evaluator_does_not_write_outside_of_dedicated_memory_region( - point: ConstraintEvaluationPoint, - ) { - let program = point.tasm_constraint_evaluation_code(); - let mut initial_state = point.set_up_triton_vm_to_evaluate_constraints_in_tasm(&program); - let mut terminal_state = initial_state.clone(); - terminal_state.run().unwrap(); - - let free_mem_page_ptr = point.memory_layout.free_mem_page_ptr; - let mem_page_size = TasmConstraintEvaluationMemoryLayout::MEM_PAGE_SIZE; - let mem_page = MemoryRegion::new(free_mem_page_ptr, mem_page_size); - let not_in_mem_page = |addr: &_| !mem_page.contains_address(addr); - - initial_state.ram.retain(|k, _| not_in_mem_page(k)); - terminal_state.ram.retain(|k, _| not_in_mem_page(k)); - prop_assert_eq!(initial_state.ram, terminal_state.ram); - } - - #[proptest] - fn triton_assembly_constraint_evaluator_declares_no_labels( - #[strategy(arb())] memory_layout: TasmConstraintEvaluationMemoryLayout, - ) { - for instruction in air_constraint_evaluation_tasm(memory_layout) { - if let LabelledInstruction::Label(label) = instruction { - return Err(TestCaseError::Fail(format!("Found label: {label}").into())); - } - } - } - - #[proptest] - fn triton_assembly_constraint_evaluator_is_straight_line_and_does_not_halt( - #[strategy(arb())] memory_layout: TasmConstraintEvaluationMemoryLayout, - ) { - type I = AnInstruction; - let is_legal = |i| !matches!(i, I::Call(_) | I::Return | I::Recurse | I::Skiz | I::Halt); - - for instruction in air_constraint_evaluation_tasm(memory_layout) { - if let LabelledInstruction::Instruction(instruction) = instruction { - prop_assert!(is_legal(instruction)); - } - } - } - #[proptest] fn linear_combination_weights_samples_correct_number_of_elements( #[strategy(arb())] mut proof_stream: ProofStream, diff --git a/triton-vm/src/table.rs b/triton-vm/src/table.rs index d4c4942d..8c84eea0 100644 --- a/triton-vm/src/table.rs +++ b/triton-vm/src/table.rs @@ -3,10 +3,8 @@ use std::fmt::Formatter; use std::fmt::Result as FmtResult; use arbitrary::Arbitrary; -use itertools::Itertools; use strum::EnumCount; use strum::EnumIter; -use twenty_first::prelude::BFieldElement; use twenty_first::prelude::XFieldElement; pub use crate::stark::NUM_QUOTIENT_SEGMENTS; @@ -31,8 +29,6 @@ pub mod processor_table; pub mod program_table; pub mod ram_table; pub mod table_column; -#[rustfmt::skip] -pub mod tasm_air_constraints; pub mod u32_table; #[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, EnumCount, EnumIter)] @@ -63,11 +59,12 @@ impl Display for ConstraintType { /// A single row of a [`MasterBaseTable`][table]. /// -/// Usually, the elements in the table are [`BFieldElement`]s. For out-of-domain rows, which is +/// Usually, the elements in the table are [`BFieldElement`][bfe]s. For out-of-domain rows, which is /// relevant for “Domain Extension to Eliminate Pretenders” (DEEP), the elements are /// [`XFieldElement`]s. /// /// [table]: master_table::MasterBaseTable +/// [bfe]: crate::prelude::BFieldElement pub type BaseRow = [T; NUM_BASE_COLUMNS]; /// A single row of a [`MasterExtensionTable`][table]. @@ -79,156 +76,3 @@ pub type ExtensionRow = [XFieldElement; NUM_EXT_COLUMNS]; /// /// See also [`NUM_QUOTIENT_SEGMENTS`]. pub type QuotientSegments = [XFieldElement; NUM_QUOTIENT_SEGMENTS]; - -/// Memory layout guarantees for the [Triton assembly AIR constraint evaluator][tasm_air]. -/// -/// [tasm_air]: tasm_air_constraints::air_constraint_evaluation_tasm -#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Arbitrary)] -pub struct TasmConstraintEvaluationMemoryLayout { - /// Pointer to a region of memory that is reserved for constraint evaluation. The size of the - /// region must be at least [`MEM_PAGE_SIZE`][mem_page_size] [`BFieldElement`]s. - /// - /// [mem_page_size]: TasmConstraintEvaluationMemoryLayout::MEM_PAGE_SIZE - pub free_mem_page_ptr: BFieldElement, - - /// Pointer to an array of [`XFieldElement`]s of length [`NUM_BASE_COLUMNS`]. - pub curr_base_row_ptr: BFieldElement, - - /// Pointer to an array of [`XFieldElement`]s of length [`NUM_EXT_COLUMNS`]. - pub curr_ext_row_ptr: BFieldElement, - - /// Pointer to an array of [`XFieldElement`]s of length [`NUM_BASE_COLUMNS`]. - pub next_base_row_ptr: BFieldElement, - - /// Pointer to an array of [`XFieldElement`]s of length [`NUM_EXT_COLUMNS`]. - pub next_ext_row_ptr: BFieldElement, - - /// Pointer to an array of [`XFieldElement`]s of length [`NUM_CHALLENGES`][num_challenges]. - /// - /// [num_challenges]: challenges::Challenges::COUNT - pub challenges_ptr: BFieldElement, -} - -impl TasmConstraintEvaluationMemoryLayout { - /// The minimal required size of a memory page in [`BFieldElement`]s. - pub const MEM_PAGE_SIZE: usize = 1 << 32; - - /// Determine if the memory layout's constraints are met, _i.e._, whether the various pointers - /// point to large enough regions of memory. - pub fn is_integral(self) -> bool { - let memory_regions = self.into_memory_regions(); - if memory_regions.iter().unique().count() != memory_regions.len() { - return false; - } - - let disjoint_from_all_others = |region| { - let mut all_other_regions = memory_regions.iter().filter(|&r| r != region); - all_other_regions.all(|r| r.disjoint_from(region)) - }; - memory_regions.iter().all(disjoint_from_all_others) - } - - fn into_memory_regions(self) -> Box<[MemoryRegion]> { - let all_regions = [ - MemoryRegion::new(self.free_mem_page_ptr, Self::MEM_PAGE_SIZE), - MemoryRegion::new(self.curr_base_row_ptr, NUM_BASE_COLUMNS), - MemoryRegion::new(self.curr_ext_row_ptr, NUM_EXT_COLUMNS), - MemoryRegion::new(self.next_base_row_ptr, NUM_BASE_COLUMNS), - MemoryRegion::new(self.next_ext_row_ptr, NUM_EXT_COLUMNS), - MemoryRegion::new(self.challenges_ptr, challenges::Challenges::COUNT), - ]; - Box::new(all_regions) - } -} - -#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)] -pub(crate) struct MemoryRegion { - start: u64, - size: u64, -} - -impl MemoryRegion { - pub fn new>(address: A, size: usize) -> Self { - let start = address.into(); - let size = u64::try_from(size).unwrap(); - Self { start, size } - } - - pub fn disjoint_from(self, other: &Self) -> bool { - !self.overlaps(other) - } - - pub fn overlaps(self, other: &Self) -> bool { - self.contains_address(other.start) || other.contains_address(self.start) - } - - pub fn contains_address>(self, addr: A) -> bool { - (self.start..self.start + self.size).contains(&addr.into()) - } -} - -#[cfg(test)] -mod tests { - use proptest::prelude::*; - use proptest_arbitrary_interop::arb; - use test_strategy::proptest; - use twenty_first::bfe; - - use super::*; - - impl Default for TasmConstraintEvaluationMemoryLayout { - /// For testing purposes only. - fn default() -> Self { - let mem_page_size = TasmConstraintEvaluationMemoryLayout::MEM_PAGE_SIZE as u64; - let mem_page = |i| bfe!(i * mem_page_size); - TasmConstraintEvaluationMemoryLayout { - free_mem_page_ptr: mem_page(0), - curr_base_row_ptr: mem_page(1), - curr_ext_row_ptr: mem_page(2), - next_base_row_ptr: mem_page(3), - next_ext_row_ptr: mem_page(4), - challenges_ptr: mem_page(5), - } - } - } - - #[proptest] - fn size_0_memory_region_contains_no_addresses( - #[strategy(arb())] region_start: BFieldElement, - #[strategy(arb())] address: BFieldElement, - ) { - let region = MemoryRegion::new(region_start, 0); - prop_assert!(!region.contains_address(region_start)); - prop_assert!(!region.contains_address(address)); - } - - #[proptest] - fn size_1_memory_region_contains_only_start_address( - #[strategy(arb())] region_start: BFieldElement, - #[strategy(arb())] - #[filter(#region_start != #address)] - address: BFieldElement, - ) { - let region = MemoryRegion::new(region_start, 1); - prop_assert!(region.contains_address(region_start)); - prop_assert!(!region.contains_address(address)); - } - - #[test] - fn definitely_integral_memory_layout_is_detected_as_integral() { - assert!(TasmConstraintEvaluationMemoryLayout::default().is_integral()); - } - - #[test] - fn definitely_non_integral_memory_layout_is_detected_as_non_integral() { - let layout = TasmConstraintEvaluationMemoryLayout { - free_mem_page_ptr: bfe!(0), - curr_base_row_ptr: bfe!(1), - curr_ext_row_ptr: bfe!(2), - next_base_row_ptr: bfe!(3), - next_ext_row_ptr: bfe!(4), - challenges_ptr: bfe!(5), - }; - assert!(!layout.is_integral()); - } -} diff --git a/triton-vm/src/table/constraint_circuit.rs b/triton-vm/src/table/constraint_circuit.rs index 30ed4e0b..44ba52bc 100644 --- a/triton-vm/src/table/constraint_circuit.rs +++ b/triton-vm/src/table/constraint_circuit.rs @@ -920,6 +920,16 @@ impl ConstraintCircuitMonad { all_nodes } + /// Counts the number of nodes in this multicircuit. Only counts nodes that + /// are used; not nodes that have been forgotten. + pub fn num_nodes(constraints: &[Self]) -> usize { + constraints + .iter() + .flat_map(|ccm| Self::all_nodes_in_circuit(&ccm.circuit.borrow())) + .unique() + .count() + } + /// Returns the maximum degree of all circuits in the multicircuit. pub(crate) fn multicircuit_degree(multicircuit: &[ConstraintCircuitMonad]) -> isize { multicircuit diff --git a/triton-vm/src/table/master_table.rs b/triton-vm/src/table/master_table.rs index a89a7308..692ff9c3 100644 --- a/triton-vm/src/table/master_table.rs +++ b/triton-vm/src/table/master_table.rs @@ -1287,6 +1287,10 @@ mod tests { use twenty_first::math::traits::FiniteField; use twenty_first::prelude::x_field_element::EXTENSION_DEGREE; + use crate::air::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout; + use crate::air::memory_layout::StaticTasmConstraintEvaluationMemoryLayout; + use crate::air::tasm_air_constraints::dynamic_air_constraint_evaluation_tasm; + use crate::air::tasm_air_constraints::static_air_constraint_evaluation_tasm; use crate::arithmetic_domain::ArithmeticDomain; use crate::instruction::tests::InstructionBucket; use crate::instruction::Instruction; @@ -1472,6 +1476,25 @@ mod tests { .is_zero()); } + macro_rules! constraints_without_degree_lowering { + ($constraint_type: ident) => {{ + let circuit_builder = ConstraintCircuitBuilder::new(); + vec![ + ExtProgramTable::$constraint_type(&circuit_builder), + ExtProcessorTable::$constraint_type(&circuit_builder), + ExtOpStackTable::$constraint_type(&circuit_builder), + ExtRamTable::$constraint_type(&circuit_builder), + ExtJumpStackTable::$constraint_type(&circuit_builder), + ExtHashTable::$constraint_type(&circuit_builder), + ExtCascadeTable::$constraint_type(&circuit_builder), + ExtLookupTable::$constraint_type(&circuit_builder), + ExtU32Table::$constraint_type(&circuit_builder), + GrandCrossTableArg::$constraint_type(&circuit_builder), + ] + .concat() + }}; + } + struct SpecSnippet { pub start_marker: &'static str, pub stop_marker: &'static str, @@ -1511,12 +1534,23 @@ mod tests { } fn generate_table_overview() -> SpecSnippet { + const NUM_DEGREE_LOWERING_TARGETS: usize = 3; + const DEGREE_LOWERING_TARGETS: [Option; NUM_DEGREE_LOWERING_TARGETS] = + [None, Some(8), Some(4)]; + assert!(DEGREE_LOWERING_TARGETS.contains(&Some(AIR_TARGET_DEGREE))); + macro_rules! table_info { ($($module:ident: $name:literal at $location:literal),* $(,)?) => {{ let mut info = vec![]; $( let name = format!("[{}]({})", $name, $location); - info.push((name, $module::BASE_WIDTH, $module::EXT_WIDTH)); + info.push( + ( + name, + [$module::BASE_WIDTH; NUM_DEGREE_LOWERING_TARGETS], + [$module::EXT_WIDTH; NUM_DEGREE_LOWERING_TARGETS] + ) + ); )* info }}; @@ -1534,37 +1568,107 @@ mod tests { u32_table: "U32Table" at "u32-table.md", ]; - let deg_low_base = degree_lowering_table::BASE_WIDTH; - let deg_low_ext = degree_lowering_table::EXT_WIDTH; - all_table_info.push(("DegreeLowering".to_string(), deg_low_base, deg_low_ext)); - all_table_info.push(("Randomizers".to_string(), 0, NUM_RANDOMIZER_POLYNOMIALS)); + let mut deg_low_main = vec![]; + let mut deg_low_aux = vec![]; + for maybe_target_degree in DEGREE_LOWERING_TARGETS { + let Some(target_degree) = maybe_target_degree else { + deg_low_main.push(0); + deg_low_aux.push(0); + continue; + }; + + let initial_constraints = constraints_without_degree_lowering!(initial_constraints); + let consistency_constraints = + constraints_without_degree_lowering!(consistency_constraints); + let transition_constraints = + constraints_without_degree_lowering!(transition_constraints); + let terminal_constraints = constraints_without_degree_lowering!(terminal_constraints); + + // generic closures are not possible; define two variants :( + let lower_to_target_degree_single_row = |mut constraints: Vec<_>| { + ConstraintCircuitMonad::lower_to_degree(&mut constraints, target_degree, 0, 0) + }; + let lower_to_target_degree_double_row = |mut constraints: Vec<_>| { + ConstraintCircuitMonad::lower_to_degree(&mut constraints, target_degree, 0, 0) + }; + + let (init_main, init_aux) = lower_to_target_degree_single_row(initial_constraints); + let (cons_main, cons_aux) = lower_to_target_degree_single_row(consistency_constraints); + let (tran_main, tran_aux) = lower_to_target_degree_double_row(transition_constraints); + let (term_main, term_aux) = lower_to_target_degree_single_row(terminal_constraints); + + deg_low_main + .push(init_main.len() + cons_main.len() + tran_main.len() + term_main.len()); + deg_low_aux.push(init_aux.len() + cons_aux.len() + tran_aux.len() + term_aux.len()); + } + let target_degrees = DEGREE_LOWERING_TARGETS + .into_iter() + .map(|target| target.map_or_else(|| "-".to_string(), |t| t.to_string())) + .join("/"); + all_table_info.push(( + format!("DegreeLowering ({target_degrees})"), + deg_low_main.try_into().unwrap(), + deg_low_aux.try_into().unwrap(), + )); + all_table_info.push(( + "Randomizers".to_string(), + [0; NUM_DEGREE_LOWERING_TARGETS], + [NUM_RANDOMIZER_POLYNOMIALS; NUM_DEGREE_LOWERING_TARGETS], + )); let all_table_info = all_table_info; // produce table code let mut ft = format!("| {:<42} ", "table name"); - ft = format!("{ft}| {:<10} ", "#main cols"); - ft = format!("{ft}| {:<9} ", "#aux cols"); - ft = format!("{ft}| {:<11} |\n", "total width"); + ft = format!("{ft}| {:>15} ", "#main cols"); + ft = format!("{ft}| {:>16} ", "#aux cols"); + ft = format!("{ft}| {:>15} |\n", "total width"); ft = format!("{ft}|:{:-<42}-", "-"); - ft = format!("{ft}|-{:-<10}:", "-"); - ft = format!("{ft}|-{:-<9}:", "-"); - ft = format!("{ft}|-{:-<11}:|\n", "-"); - - let mut total_main = 0; - let mut total_aux = 0; + ft = format!("{ft}|-{:-<15}:", "-"); + ft = format!("{ft}|-{:-<16}:", "-"); + ft = format!("{ft}|-{:-<15}:|\n", "-"); + + let format_slice_and_collapse_if_all_entries_equal = |slice: &[usize]| { + if slice.iter().all(|&n| n == slice[0]) { + format!("{}", slice[0]) + } else { + slice.iter().join("/").to_string() + } + }; + let mut total_main = [0; NUM_DEGREE_LOWERING_TARGETS]; + let mut total_aux = [0; NUM_DEGREE_LOWERING_TARGETS]; for (name, num_main, num_aux) in all_table_info { - let num_total = num_main + EXTENSION_DEGREE * num_aux; - ft = format!("{ft}| {name:<42} | {num_main:>10} | {num_aux:9} | {num_total:>11} |\n"); - total_main += num_main; - total_aux += num_aux; + let num_total = num_main + .into_iter() + .zip(num_aux) + .map(|(m, a)| m + EXTENSION_DEGREE * a) + .collect_vec(); + ft = format!( + "{ft}| {name:<42} | {:>15} | {:>16} | {:>15} |\n", + format_slice_and_collapse_if_all_entries_equal(&num_main), + format_slice_and_collapse_if_all_entries_equal(&num_aux), + format_slice_and_collapse_if_all_entries_equal(&num_total), + ); + for (t, n) in total_main.iter_mut().zip(num_main) { + *t += n; + } + for (t, n) in total_aux.iter_mut().zip(num_aux) { + *t += n; + } } ft = format!( - "{ft}| {:<42} | {:>10} | {:>9} | {:>11} |\n", + "{ft}| {:<42} | {:>15} | {:>16} | {:>15} |\n", "**TOTAL**", - format!("**{total_main}**"), - format!("**{total_aux}**"), - format!("**{}**", total_main + EXTENSION_DEGREE * total_aux) + format!("**{}**", total_main.iter().join("/")), + format!("**{}**", total_aux.iter().join("/")), + format!( + "**{}**", + total_main + .into_iter() + .zip(total_aux) + .map(|(m, a)| m + EXTENSION_DEGREE * a) + .join("/") + ) ); let how_to_update = ""; @@ -1613,154 +1717,182 @@ mod tests { // an `expr` cannot be followed up with `and`. Instead, declare this `const` to // have an `ident`, which _can_ be followed up with `and`. const ZERO: usize = 0; - let mut tables = constraint_overview_rows!( - ExtProgramTable ends at PROGRAM_TABLE_END and EXT_PROGRAM_TABLE_END. - Spec: ["ProgramTable"]("program-table.md"), - ExtProcessorTable ends at PROCESSOR_TABLE_END and EXT_PROCESSOR_TABLE_END. - Spec: ["ProcessorTable"]("processor-table.md"), - ExtOpStackTable ends at OP_STACK_TABLE_END and EXT_OP_STACK_TABLE_END. - Spec: ["OpStackTable"]("operational-stack-table.md"), - ExtRamTable ends at RAM_TABLE_END and EXT_RAM_TABLE_END. - Spec: ["RamTable"]("random-access-memory-table.md"), - ExtJumpStackTable ends at JUMP_STACK_TABLE_END and EXT_JUMP_STACK_TABLE_END. - Spec: ["JumpStackTable"]("jump-stack-table.md"), - ExtHashTable ends at HASH_TABLE_END and EXT_HASH_TABLE_END. - Spec: ["HashTable"]("hash-table.md"), - ExtCascadeTable ends at CASCADE_TABLE_END and EXT_CASCADE_TABLE_END. - Spec: ["CascadeTable"]("cascade-table.md"), - ExtLookupTable ends at LOOKUP_TABLE_END and EXT_LOOKUP_TABLE_END. - Spec: ["LookupTable"]("lookup-table.md"), - ExtU32Table ends at U32_TABLE_END and EXT_U32_TABLE_END. - Spec: ["U32Table"]("u32-table.md"), - GrandCrossTableArg ends at ZERO and ZERO. - Spec: ["Grand Cross-Table Argument"]("table-linking.md"), - ); - let mut ft = String::new(); - ft = format!("{ft}\nBefore automatic degree lowering:\n\n"); - ft = format!("{ft}| {:<46} ", "table name"); - ft = format!("{ft}| #initial "); - ft = format!("{ft}| #consistency "); - ft = format!("{ft}| #transition "); - ft = format!("{ft}| #terminal "); - ft = format!("{ft}| max degree |\n"); - - ft = format!("{ft}|:{:-<46}-", "-"); - ft = format!("{ft}|-{:-<8}:", "-"); - ft = format!("{ft}|-{:-<12}:", "-"); - ft = format!("{ft}|-{:-<11}:", "-"); - ft = format!("{ft}|-{:-<9}:", "-"); - ft = format!("{ft}|-{:-<10}:|\n", "-"); - - let mut total_initial = 0; - let mut total_consistency = 0; - let mut total_transition = 0; - let mut total_terminal = 0; - let mut total_max_degree = 0; - for table in &tables { - let table_max_degree = [ - ConstraintCircuitMonad::multicircuit_degree(&table.initial_constraints), - ConstraintCircuitMonad::multicircuit_degree(&table.consistency_constraints), - ConstraintCircuitMonad::multicircuit_degree(&table.transition_constraints), - ConstraintCircuitMonad::multicircuit_degree(&table.terminal_constraints), - ] - .into_iter() - .max() - .unwrap_or(-1); + let degree_lowering_targets = [None, Some(8), Some(4)]; + assert!(degree_lowering_targets.contains(&Some(AIR_TARGET_DEGREE))); - let num_init = table.initial_constraints.len(); - let num_cons = table.consistency_constraints.len(); - let num_tran = table.transition_constraints.len(); - let num_term = table.terminal_constraints.len(); - ft = format!( - "{ft}| {:<46} | {:>8} | {:12} | {:>11} | {:>9} | {:>10} |\n", - table.name, num_init, num_cons, num_tran, num_term, table_max_degree, - ); - total_initial += num_init; - total_consistency += num_cons; - total_transition += num_tran; - total_terminal += num_term; - total_max_degree = total_max_degree.max(table_max_degree); - } - ft = format!( - "{ft}| {:<46} | {:>8} | {:>12} | {:>11} | {:>9} | {:>10} |\n", - "**TOTAL**", - format!("**{total_initial}**"), - format!("**{total_consistency}**"), - format!("**{total_transition}**"), - format!("**{total_terminal}**"), - format!("**{}**", total_max_degree) - ); - ft = format!("{ft}\nAfter automatically lowering degree to {AIR_TARGET_DEGREE}:\n\n"); - ft = format!("{ft}| {:<46} ", "table name"); - ft = format!("{ft}| #initial "); - ft = format!("{ft}| #consistency "); - ft = format!("{ft}| #transition "); - ft = format!("{ft}| #terminal |\n"); - - ft = format!("{ft}|:{:-<46}-", "-"); - ft = format!("{ft}|-{:-<8}:", "-"); - ft = format!("{ft}|-{:-<12}:", "-"); - ft = format!("{ft}|-{:-<11}:", "-"); - ft = format!("{ft}|-{:-<9}:|\n", "-"); - - let mut total_initial = 0; - let mut total_consistency = 0; - let mut total_transition = 0; - let mut total_terminal = 0; - for table in &mut tables { - let (new_base_initial, new_ext_initial) = ConstraintCircuitMonad::lower_to_degree( - &mut table.initial_constraints, - AIR_TARGET_DEGREE, - table.last_base_column_index, - table.last_ext_column_index, + let mut ft = String::new(); + for target_degree in degree_lowering_targets { + let mut total_initial = 0; + let mut total_consistency = 0; + let mut total_transition = 0; + let mut total_terminal = 0; + ft = match target_degree { + None => format!("{ft}\nBefore automatic degree lowering:\n\n"), + Some(target) => format!("{ft}\nAfter lowering degree to {target}:\n\n"), + }; + ft = format!("{ft}| {:<46} ", "table name"); + ft = format!("{ft}| #initial "); + ft = format!("{ft}| #consistency "); + ft = format!("{ft}| #transition "); + ft = format!("{ft}| #terminal "); + if target_degree.is_none() { + ft = format!("{ft}| max degree "); + } + ft = format!("{ft}|\n"); + + ft = format!("{ft}|:{:-<46}-", "-"); + ft = format!("{ft}|-{:-<8}:", "-"); + ft = format!("{ft}|-{:-<12}:", "-"); + ft = format!("{ft}|-{:-<11}:", "-"); + ft = format!("{ft}|-{:-<9}:", "-"); + if target_degree.is_none() { + ft = format!("{ft}|-{:-<10}:", "-"); + } + ft = format!("{ft}|\n"); + + let mut total_max_degree = 0; + let mut tables = constraint_overview_rows!( + ExtProgramTable ends at PROGRAM_TABLE_END and EXT_PROGRAM_TABLE_END. + Spec: ["ProgramTable"]("program-table.md"), + ExtProcessorTable ends at PROCESSOR_TABLE_END and EXT_PROCESSOR_TABLE_END. + Spec: ["ProcessorTable"]("processor-table.md"), + ExtOpStackTable ends at OP_STACK_TABLE_END and EXT_OP_STACK_TABLE_END. + Spec: ["OpStackTable"]("operational-stack-table.md"), + ExtRamTable ends at RAM_TABLE_END and EXT_RAM_TABLE_END. + Spec: ["RamTable"]("random-access-memory-table.md"), + ExtJumpStackTable ends at JUMP_STACK_TABLE_END and EXT_JUMP_STACK_TABLE_END. + Spec: ["JumpStackTable"]("jump-stack-table.md"), + ExtHashTable ends at HASH_TABLE_END and EXT_HASH_TABLE_END. + Spec: ["HashTable"]("hash-table.md"), + ExtCascadeTable ends at CASCADE_TABLE_END and EXT_CASCADE_TABLE_END. + Spec: ["CascadeTable"]("cascade-table.md"), + ExtLookupTable ends at LOOKUP_TABLE_END and EXT_LOOKUP_TABLE_END. + Spec: ["LookupTable"]("lookup-table.md"), + ExtU32Table ends at U32_TABLE_END and EXT_U32_TABLE_END. + Spec: ["U32Table"]("u32-table.md"), + GrandCrossTableArg ends at ZERO and ZERO. + Spec: ["Grand Cross-Table Argument"]("table-linking.md"), ); - let (new_base_consistency, new_ext_consistency) = - ConstraintCircuitMonad::lower_to_degree( - &mut table.consistency_constraints, - AIR_TARGET_DEGREE, - table.last_base_column_index, - table.last_ext_column_index, + let mut all_initial_constraints = vec![]; + let mut all_consistency_constraints = vec![]; + let mut all_transition_constraints = vec![]; + let mut all_terminal_constraints = vec![]; + for table in &mut tables { + let mut initial_constraints = table.initial_constraints.clone(); + let mut consistency_constraints = table.consistency_constraints.clone(); + let mut transition_constraints = table.transition_constraints.clone(); + let mut terminal_constraints = table.terminal_constraints.clone(); + + if let Some(target) = target_degree { + let (new_base_initial, new_ext_initial) = + ConstraintCircuitMonad::lower_to_degree( + &mut table.initial_constraints, + target, + table.last_base_column_index, + table.last_ext_column_index, + ); + let (new_base_consistency, new_ext_consistency) = + ConstraintCircuitMonad::lower_to_degree( + &mut table.consistency_constraints, + target, + table.last_base_column_index, + table.last_ext_column_index, + ); + let (new_base_transition, new_ext_transition) = + ConstraintCircuitMonad::lower_to_degree( + &mut table.transition_constraints, + target, + table.last_base_column_index, + table.last_ext_column_index, + ); + let (new_base_terminal, new_ext_terminal) = + ConstraintCircuitMonad::lower_to_degree( + &mut table.terminal_constraints, + target, + table.last_base_column_index, + table.last_ext_column_index, + ); + + initial_constraints.extend(new_base_initial); + consistency_constraints.extend(new_base_consistency); + transition_constraints.extend(new_base_transition); + terminal_constraints.extend(new_base_terminal); + + initial_constraints.extend(new_ext_initial); + consistency_constraints.extend(new_ext_consistency); + transition_constraints.extend(new_ext_transition); + terminal_constraints.extend(new_ext_terminal); + } + + let table_max_degree = [ + ConstraintCircuitMonad::multicircuit_degree(&initial_constraints), + ConstraintCircuitMonad::multicircuit_degree(&consistency_constraints), + ConstraintCircuitMonad::multicircuit_degree(&transition_constraints), + ConstraintCircuitMonad::multicircuit_degree(&terminal_constraints), + ] + .into_iter() + .max() + .unwrap_or(-1); + + let num_init = initial_constraints.len(); + let num_cons = consistency_constraints.len(); + let num_tran = transition_constraints.len(); + let num_term = terminal_constraints.len(); + + all_initial_constraints.extend(initial_constraints); + all_consistency_constraints.extend(consistency_constraints); + all_transition_constraints.extend(transition_constraints); + all_terminal_constraints.extend(terminal_constraints); + + ft = format!( + "{ft}| {:<46} | {:>8} | {:12} | {:>11} | {:>9} |", + table.name, num_init, num_cons, num_tran, num_term, ); - let (new_base_transition, new_ext_transition) = ConstraintCircuitMonad::lower_to_degree( - &mut table.transition_constraints, - AIR_TARGET_DEGREE, - table.last_base_column_index, - table.last_ext_column_index, - ); - let (new_base_terminal, new_ext_terminal) = ConstraintCircuitMonad::lower_to_degree( - &mut table.terminal_constraints, - AIR_TARGET_DEGREE, - table.last_base_column_index, - table.last_ext_column_index, + if target_degree.is_none() { + ft = format!("{ft} {table_max_degree:>10} |"); + } + ft = format!("{ft}\n"); + total_initial += num_init; + total_consistency += num_cons; + total_transition += num_tran; + total_terminal += num_term; + total_max_degree = total_max_degree.max(table_max_degree); + } + ft = format!( + "{ft}| {:<46} | {:>8} | {:>12} | {:>11} | {:>9} |", + "**TOTAL**", + format!("**{total_initial}**"), + format!("**{total_consistency}**"), + format!("**{total_transition}**"), + format!("**{total_terminal}**"), ); - let num_init = - table.initial_constraints.len() + new_base_initial.len() + new_ext_initial.len(); - let num_cons = table.consistency_constraints.len() - + new_base_consistency.len() - + new_ext_consistency.len(); - let num_tran = table.transition_constraints.len() - + new_base_transition.len() - + new_ext_transition.len(); - let num_term = - table.terminal_constraints.len() + new_base_terminal.len() + new_ext_terminal.len(); + if target_degree.is_none() { + ft = format!("{ft} {:>10} |", format!("**{}**", total_max_degree)); + } + ft = format!("{ft}\n"); + + let num_nodes_in_all_initial_constraints = + ConstraintCircuitMonad::num_nodes(&all_initial_constraints); + let num_nodes_in_all_consistency_constraints = + ConstraintCircuitMonad::num_nodes(&all_consistency_constraints); + let num_nodes_in_all_transition_constraints = + ConstraintCircuitMonad::num_nodes(&all_transition_constraints); + let num_nodes_in_all_terminal_constraints = + ConstraintCircuitMonad::num_nodes(&all_terminal_constraints); ft = format!( - "{ft}| {:<46} | {num_init:>8} | {num_cons:12} | {num_tran:>11} | {num_term:>9} |\n", - table.name, + "{ft}| {:<46} | {:>8} | {:>12} | {:>11} | {:>9} |", + "(# nodes)", + format!("({num_nodes_in_all_initial_constraints})"), + format!("({num_nodes_in_all_consistency_constraints})"), + format!("({num_nodes_in_all_transition_constraints})"), + format!("({num_nodes_in_all_terminal_constraints})"), ); - total_initial += num_init; - total_consistency += num_cons; - total_transition += num_tran; - total_terminal += num_term; + if target_degree.is_none() { + ft = format!("{ft} {:>10} |", ""); + } + ft = format!("{ft}\n"); } - ft = format!( - "{ft}| {:<46} | {:>8} | {:>12} | {:>11} | {:>9} |\n", - "**TOTAL**", - format!("**{total_initial}**"), - format!("**{total_consistency}**"), - format!("**{total_transition}**"), - format!("**{total_terminal}**"), - ); let how_to_update = ""; SpecSnippet { @@ -1771,37 +1903,45 @@ mod tests { } fn generate_tasm_air_evaluation_cost_overview() -> SpecSnippet { - let layout = TasmConstraintEvaluationMemoryLayout::default(); - let tasm = tasm_air_constraints::air_constraint_evaluation_tasm(layout); - let program = triton_program!({ &tasm }); - - let processor = program.clone().into_iter().count(); - let stack = program - .clone() - .into_iter() - .map(|instruction| instruction.op_stack_size_influence().abs()) - .sum::(); - - let ram_table_influence = |instruction| match instruction { - Instruction::ReadMem(st) | Instruction::WriteMem(st) => st.num_words(), - Instruction::SpongeAbsorbMem => tip5::RATE, - Instruction::XbDotStep => 4, - Instruction::XxDotStep => 6, - _ => 0, - }; - let ram = program - .clone() - .into_iter() - .map(ram_table_influence) - .sum::(); - - let snippet = format!( - "\ - | Processor | Op Stack | RAM |\n\ - |----------:|---------:|------:|\n\ - | {processor:>9} | {stack:>8} | {ram:>5} |\n\ + let static_layout = StaticTasmConstraintEvaluationMemoryLayout::default(); + let static_tasm = static_air_constraint_evaluation_tasm(static_layout); + let dynamic_layout = DynamicTasmConstraintEvaluationMemoryLayout::default(); + let dynamic_tasm = dynamic_air_constraint_evaluation_tasm(dynamic_layout); + + let mut snippet = "\ + | Type | Processor | Op Stack | RAM |\n\ + |:-------------|----------:|---------:|------:|\n" + .to_string(); + + for (label, tasm) in [("static", static_tasm), ("dynamic", dynamic_tasm)] { + let program = triton_program!({ &tasm }); + + let processor = program.clone().into_iter().count(); + let stack = program + .clone() + .into_iter() + .map(|instruction| instruction.op_stack_size_influence().abs()) + .sum::(); + + let ram_table_influence = |instruction| match instruction { + Instruction::ReadMem(st) | Instruction::WriteMem(st) => st.num_words(), + Instruction::SpongeAbsorbMem => tip5::RATE, + Instruction::XbDotStep => 4, + Instruction::XxDotStep => 6, + _ => 0, + }; + let ram = program + .clone() + .into_iter() + .map(ram_table_influence) + .sum::(); + + snippet = format!( + "{snippet}\ + | {label:<12} | {processor:>9} | {stack:>8} | {ram:>5} |\n\ " - ); + ); + } SpecSnippet { start_marker: "", diff --git a/triton-vm/src/table/tasm_air_constraints.rs b/triton-vm/src/table/tasm_air_constraints.rs deleted file mode 100644 index 96d653cf..00000000 --- a/triton-vm/src/table/tasm_air_constraints.rs +++ /dev/null @@ -1,13 +0,0 @@ -//! This file is a placeholder for auto-generated code -//! Run `cargo run --bin constraint-evaluation-generator` -//! to fill in this file with optimized constraints. - -use crate::instruction::LabelledInstruction; -use crate::table::constraints::ERROR_MESSAGE_GENERATE_CONSTRAINTS; -use crate::table::TasmConstraintEvaluationMemoryLayout; - -pub fn air_constraint_evaluation_tasm( - _: TasmConstraintEvaluationMemoryLayout, -) -> Vec { - panic!("{ERROR_MESSAGE_GENERATE_CONSTRAINTS}"); -}