1include!(concat!(env!("OUT_DIR"), "/tasm_constraints.rs"));
2
3#[cfg(test)]
4#[cfg_attr(coverage_nightly, coverage(off))]
5mod tests {
6 use isa::instruction::AnInstruction;
7 use itertools::Itertools;
8 use ndarray::Array1;
9 use proptest::collection::vec;
10 use proptest::prelude::*;
11 use proptest_arbitrary_interop::arb;
12 use std::collections::HashMap;
13 use test_strategy::proptest;
14 use twenty_first::prelude::x_field_element::EXTENSION_DEGREE;
15 use twenty_first::prelude::*;
16
17 use crate::challenges::Challenges;
18 use crate::memory_layout;
19 use crate::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout;
20 use crate::memory_layout::IntegralMemoryLayout;
21 use crate::memory_layout::StaticTasmConstraintEvaluationMemoryLayout;
22 use crate::prelude::*;
23 use crate::table::auxiliary_table::Evaluable;
24 use crate::table::master_table::MasterAuxTable;
25 use crate::table::master_table::MasterMainTable;
26
27 use super::dynamic_air_constraint_evaluation_tasm;
28 use super::static_air_constraint_evaluation_tasm;
29
30 #[derive(Debug, Clone, test_strategy::Arbitrary)]
31 struct ConstraintEvaluationPoint {
32 #[strategy(vec(arb(), MasterMainTable::NUM_COLUMNS))]
33 #[map(Array1::from)]
34 curr_main_row: Array1<XFieldElement>,
35
36 #[strategy(vec(arb(), MasterAuxTable::NUM_COLUMNS))]
37 #[map(Array1::from)]
38 curr_aux_row: Array1<XFieldElement>,
39
40 #[strategy(vec(arb(), MasterMainTable::NUM_COLUMNS))]
41 #[map(Array1::from)]
42 next_main_row: Array1<XFieldElement>,
43
44 #[strategy(vec(arb(), MasterAuxTable::NUM_COLUMNS))]
45 #[map(Array1::from)]
46 next_aux_row: Array1<XFieldElement>,
47
48 #[strategy(arb())]
49 challenges: Challenges,
50
51 #[strategy(arb())]
52 #[filter(#static_memory_layout.is_integral())]
53 static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout,
54 }
55
56 impl ConstraintEvaluationPoint {
57 fn evaluate_all_constraints_rust(&self) -> Vec<XFieldElement> {
58 let init = MasterAuxTable::evaluate_initial_constraints(
59 self.curr_main_row.view(),
60 self.curr_aux_row.view(),
61 &self.challenges,
62 );
63 let cons = MasterAuxTable::evaluate_consistency_constraints(
64 self.curr_main_row.view(),
65 self.curr_aux_row.view(),
66 &self.challenges,
67 );
68 let tran = MasterAuxTable::evaluate_transition_constraints(
69 self.curr_main_row.view(),
70 self.curr_aux_row.view(),
71 self.next_main_row.view(),
72 self.next_aux_row.view(),
73 &self.challenges,
74 );
75 let term = MasterAuxTable::evaluate_terminal_constraints(
76 self.curr_main_row.view(),
77 self.curr_aux_row.view(),
78 &self.challenges,
79 );
80
81 [init, cons, tran, term].concat()
82 }
83
84 fn evaluate_all_constraints_tasm_static(&self) -> Vec<XFieldElement> {
85 let program = self.tasm_static_constraint_evaluation_code();
86 let mut vm_state =
87 self.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(program);
88 vm_state.run().unwrap();
89 Self::extract_constraint_evaluations(vm_state)
90 }
91
92 fn evaluate_all_constraints_tasm_dynamic(&self) -> Vec<XFieldElement> {
93 let program = self.tasm_dynamic_constraint_evaluation_code();
94 let mut vm_state =
95 self.set_up_triton_vm_to_evaluate_constraints_in_tasm_dynamic(program);
96 vm_state.run().unwrap();
97 Self::extract_constraint_evaluations(vm_state)
98 }
99
100 fn tasm_static_constraint_evaluation_code(&self) -> Program {
101 let mut source_code = static_air_constraint_evaluation_tasm(self.static_memory_layout);
102 source_code.push(triton_instr!(halt));
103 Program::new(&source_code)
104 }
105
106 fn tasm_dynamic_constraint_evaluation_code(&self) -> Program {
107 let dynamic_memory_layout = DynamicTasmConstraintEvaluationMemoryLayout {
108 free_mem_page_ptr: self.static_memory_layout.free_mem_page_ptr,
109 challenges_ptr: self.static_memory_layout.challenges_ptr,
110 };
111 let mut source_code = dynamic_air_constraint_evaluation_tasm(dynamic_memory_layout);
112 source_code.push(triton_instr!(halt));
113 Program::new(&source_code)
114 }
115
116 fn extract_constraint_evaluations(mut vm_state: VMState) -> Vec<XFieldElement> {
118 assert!(vm_state.halting);
119 let output_list_ptr = vm_state.op_stack.pop().unwrap().value();
120 let num_quotients = MasterAuxTable::NUM_CONSTRAINTS;
121 Self::read_xfe_list_at_address(vm_state.ram, output_list_ptr, num_quotients)
122 }
123
124 fn set_up_triton_vm_to_evaluate_constraints_in_tasm_static(
125 &self,
126 program: Program,
127 ) -> VMState {
128 let curr_main_row_ptr = self.static_memory_layout.curr_main_row_ptr;
129 let curr_aux_row_ptr = self.static_memory_layout.curr_aux_row_ptr;
130 let next_main_row_ptr = self.static_memory_layout.next_main_row_ptr;
131 let next_aux_row_ptr = self.static_memory_layout.next_aux_row_ptr;
132 let challenges_ptr = self.static_memory_layout.challenges_ptr;
133
134 let mut ram = HashMap::default();
135 Self::extend_ram_at_address(&mut ram, self.curr_main_row.to_vec(), curr_main_row_ptr);
136 Self::extend_ram_at_address(&mut ram, self.curr_aux_row.to_vec(), curr_aux_row_ptr);
137 Self::extend_ram_at_address(&mut ram, self.next_main_row.to_vec(), next_main_row_ptr);
138 Self::extend_ram_at_address(&mut ram, self.next_aux_row.to_vec(), next_aux_row_ptr);
139 Self::extend_ram_at_address(&mut ram, self.challenges.challenges, challenges_ptr);
140 let non_determinism = NonDeterminism::default().with_ram(ram);
141
142 VMState::new(program, PublicInput::default(), non_determinism)
143 }
144
145 fn set_up_triton_vm_to_evaluate_constraints_in_tasm_dynamic(
146 &self,
147 program: Program,
148 ) -> VMState {
149 let mut vm_state =
151 self.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(program);
152
153 let layout = self.static_memory_layout;
154 vm_state.op_stack.push(layout.curr_main_row_ptr);
155 vm_state.op_stack.push(layout.curr_aux_row_ptr);
156 vm_state.op_stack.push(layout.next_main_row_ptr);
157 vm_state.op_stack.push(layout.next_aux_row_ptr);
158 vm_state
159 }
160
161 fn extend_ram_at_address(
162 ram: &mut HashMap<BFieldElement, BFieldElement>,
163 list: impl IntoIterator<Item = impl Into<XFieldElement>>,
164 address: BFieldElement,
165 ) {
166 let list = list.into_iter().flat_map(|xfe| xfe.into().coefficients);
167 let indexed_list = list.enumerate();
168 let offset_address = |i| bfe!(i as u64) + address;
169 let ram_extension = indexed_list.map(|(i, bfe)| (offset_address(i), bfe));
170 ram.extend(ram_extension);
171 }
172
173 fn read_xfe_list_at_address(
174 ram: HashMap<BFieldElement, BFieldElement>,
175 address: u64,
176 len: usize,
177 ) -> Vec<XFieldElement> {
178 let mem_region_end = address + (len * EXTENSION_DEGREE) as u64;
179 (address..mem_region_end)
180 .map(BFieldElement::new)
181 .map(|i| ram[&i])
182 .chunks(EXTENSION_DEGREE)
183 .into_iter()
184 .map(|c| XFieldElement::try_from(c.collect_vec()).unwrap())
185 .collect()
186 }
187 }
188
189 #[proptest]
190 fn triton_constraints_and_assembly_constraints_agree(point: ConstraintEvaluationPoint) {
191 let all_constraints_rust = point.evaluate_all_constraints_rust();
192 let all_constraints_tasm_static = point.evaluate_all_constraints_tasm_static();
193 prop_assert_eq!(all_constraints_rust.clone(), all_constraints_tasm_static);
194
195 let all_constraints_tasm_dynamic = point.evaluate_all_constraints_tasm_dynamic();
196 prop_assert_eq!(all_constraints_rust, all_constraints_tasm_dynamic);
197 }
198
199 #[proptest]
200 fn triton_assembly_constraint_evaluators_do_not_write_outside_of_dedicated_memory_region(
201 point: ConstraintEvaluationPoint,
202 ) {
203 let program = point.tasm_static_constraint_evaluation_code();
204 let mut initial_state =
205 point.set_up_triton_vm_to_evaluate_constraints_in_tasm_static(program);
206 let mut terminal_state = initial_state.clone();
207 terminal_state.run().unwrap();
208
209 let free_mem_page_ptr = point.static_memory_layout.free_mem_page_ptr;
210 let mem_page_size = memory_layout::MEM_PAGE_SIZE;
211 let mem_page = memory_layout::MemoryRegion::new(free_mem_page_ptr, mem_page_size);
212 let not_in_mem_page = |addr: &_| !mem_page.contains_address(addr);
213
214 initial_state.ram.retain(|k, _| not_in_mem_page(k));
215 terminal_state.ram.retain(|k, _| not_in_mem_page(k));
216 prop_assert_eq!(initial_state.ram, terminal_state.ram);
217 }
218
219 #[proptest]
220 fn triton_assembly_constraint_evaluators_declare_no_labels(
221 #[strategy(arb())] static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout,
222 #[strategy(arb())] dynamic_memory_layout: DynamicTasmConstraintEvaluationMemoryLayout,
223 ) {
224 for instruction in static_air_constraint_evaluation_tasm(static_memory_layout)
225 .into_iter()
226 .chain(dynamic_air_constraint_evaluation_tasm(
227 dynamic_memory_layout,
228 ))
229 {
230 if let LabelledInstruction::Label(label) = instruction {
231 return Err(TestCaseError::Fail(format!("Found label: {label}").into()));
232 }
233 }
234 }
235
236 #[proptest]
237 fn triton_assembly_constraint_evaluators_are_straight_line_and_does_not_halt(
238 #[strategy(arb())] static_memory_layout: StaticTasmConstraintEvaluationMemoryLayout,
239 #[strategy(arb())] dynamic_memory_layout: DynamicTasmConstraintEvaluationMemoryLayout,
240 ) {
241 type I = AnInstruction<String>;
242 let is_legal = |instruction| {
243 !matches!(
244 instruction,
245 I::Call(_) | I::Return | I::Recurse | I::RecurseOrReturn | I::Skiz | I::Halt
246 )
247 };
248
249 for instruction in static_air_constraint_evaluation_tasm(static_memory_layout) {
250 if let LabelledInstruction::Instruction(instruction) = instruction {
251 prop_assert!(is_legal(instruction));
252 }
253 }
254
255 for instruction in dynamic_air_constraint_evaluation_tasm(dynamic_memory_layout) {
256 if let LabelledInstruction::Instruction(instruction) = instruction {
257 prop_assert!(is_legal(instruction));
258 }
259 }
260 }
261}