Skip to content

Commit

Permalink
docs: Include cost of evaluating AIR in TASM
Browse files Browse the repository at this point in the history
  • Loading branch information
jan-ferdinand committed Jun 5, 2024
1 parent a61b042 commit 81e2a73
Show file tree
Hide file tree
Showing 3 changed files with 72 additions and 11 deletions.
12 changes: 12 additions & 0 deletions specification/src/arithmetization-overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -61,3 +61,15 @@ After automatically lowering degree to 4:
| [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 |
| **TOTAL** | **81** | **94** | **386** | **23** |
<!-- auto-gen info stop constraints_overview -->


## Triton Assembly Constraint Evaluation

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.

<!-- auto-gen info start tasm_air_evaluation_cost -->
| Processor | Op Stack | RAM |
|----------:|---------:|------:|
| 35689 | 66327 | 23592 |
<!-- auto-gen info stop tasm_air_evaluation_cost -->
28 changes: 17 additions & 11 deletions triton-vm/src/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -176,6 +176,22 @@ mod tests {

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,
Expand All @@ -200,17 +216,7 @@ mod tests {

#[test]
fn definitely_integral_memory_layout_is_detected_as_integral() {
let mem_page_size = TasmConstraintEvaluationMemoryLayout::MEM_PAGE_SIZE as u64;
let mem_page = |i| bfe!(i * mem_page_size);
let layout = 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),
};
assert!(layout.is_integral());
assert!(TasmConstraintEvaluationMemoryLayout::default().is_integral());
}

#[test]
Expand Down
43 changes: 43 additions & 0 deletions triton-vm/src/table/master_table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1339,6 +1339,7 @@ mod tests {
use twenty_first::prelude::x_field_element::EXTENSION_DEGREE;

use crate::arithmetic_domain::ArithmeticDomain;
use crate::instruction::Instruction;
use crate::shared_tests::ProgramAndInput;
use crate::stark::tests::*;
use crate::table::degree_lowering_table::DegreeLoweringBaseTableColumn;
Expand Down Expand Up @@ -1530,11 +1531,13 @@ mod tests {
fn update_arithmetization_overview() {
let table_overview = generate_table_overview();
let constraint_overview = generate_constraints_overview();
let tasm_air_overview = generate_tasm_air_evaluation_cost_overview();

// current directory is triton-vm/triton-vm/
let file_path = Path::new("../specification/src/arithmetization-overview.md");
update_spec_with(file_path, table_overview);
update_spec_with(file_path, constraint_overview);
update_spec_with(file_path, tasm_air_overview);
}

fn update_spec_with(spec_path: &Path, snippet: SpecSnippet) {
Expand Down Expand Up @@ -1811,6 +1814,46 @@ 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::<i32>();

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::<usize>();

let snippet = format!(
"\
| Processor | Op Stack | RAM |\n\
|----------:|---------:|------:|\n\
| {processor:>9} | {stack:>8} | {ram:>5} |\n\
"
);

SpecSnippet {
start_marker: "<!-- auto-gen info start tasm_air_evaluation_cost -->",
stop_marker: "<!-- auto-gen info stop tasm_air_evaluation_cost -->",
snippet,
}
}

/// intended use: `cargo t print_all_master_table_indices -- --nocapture`
#[test]
fn print_all_master_table_indices() {
Expand Down

0 comments on commit 81e2a73

Please sign in to comment.