• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

TritonVM / triton-vm / 10825170249

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

push

github

jan-ferdinand
chore: Use “main” & “aux over “base” & “ext”

This completes the transition started in 07fdf159.

changelog: ignore

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

30 existing lines in 4 files now uncovered.

23038 of 23420 relevant lines covered (98.37%)

7954849.83 hits per line

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

87.9
/triton-constraint-builder/src/codegen.rs
1
//! The various tables' constraints are very inefficient to evaluate if they live in RAM.
2
//! Instead, the build script turns them into rust code, which is then optimized by rustc.
3

4
use std::collections::HashSet;
5

6
use constraint_circuit::BinOp;
7
use constraint_circuit::CircuitExpression;
8
use constraint_circuit::ConstraintCircuit;
9
use constraint_circuit::InputIndicator;
10
use isa::instruction::Instruction;
11
use isa::op_stack::NumberOfWords;
12
use itertools::Itertools;
13
use proc_macro2::TokenStream;
14
use quote::format_ident;
15
use quote::quote;
16
use quote::ToTokens;
17
use twenty_first::prelude::x_field_element::EXTENSION_DEGREE;
18
use twenty_first::prelude::*;
19

20
use crate::Constraints;
21

22
pub trait Codegen {
23
    fn constraint_evaluation_code(constraints: &Constraints) -> TokenStream;
24

25
    fn tokenize_bfe(bfe: BFieldElement) -> TokenStream {
415✔
26
        let raw_u64 = bfe.raw_u64();
415✔
27
        quote!(BFieldElement::from_raw_u64(#raw_u64))
415✔
28
    }
415✔
29

30
    fn tokenize_xfe(xfe: XFieldElement) -> TokenStream {
1✔
31
        let [c_0, c_1, c_2] = xfe.coefficients.map(Self::tokenize_bfe);
1✔
32
        quote!(XFieldElement::new([#c_0, #c_1, #c_2]))
1✔
33
    }
1✔
34
}
35

36
#[derive(Debug, Default, Clone, Eq, PartialEq)]
37
pub struct RustBackend {
38
    /// All [circuit] IDs known to be in scope.
39
    ///
40
    /// [circuit]: triton_vm::table::circuit::ConstraintCircuit
41
    scope: HashSet<usize>,
42
}
43

44
#[derive(Debug, Default, Clone, Eq, PartialEq)]
45
pub struct TasmBackend {
46
    /// All [circuit] IDs known to be processed and stored to memory.
47
    ///
48
    /// [circuit]: triton_vm::table::circuit::ConstraintCircuit
49
    scope: HashSet<usize>,
50

51
    /// The number of elements written to the output list.
52
    elements_written: usize,
53

54
    /// Whether the code that is to be generated can assume statically provided
55
    /// addresses for the various input arrays.
56
    input_location_is_static: bool,
57
}
58

59
impl Codegen for RustBackend {
60
    fn constraint_evaluation_code(constraints: &Constraints) -> TokenStream {
1✔
61
        let num_init_constraints = constraints.init.len();
1✔
62
        let num_cons_constraints = constraints.cons.len();
1✔
63
        let num_tran_constraints = constraints.tran.len();
1✔
64
        let num_term_constraints = constraints.term.len();
1✔
65

1✔
66
        let (init_constraint_degrees, init_constraints_bfe, init_constraints_xfe) =
1✔
67
            Self::tokenize_circuits(&constraints.init());
1✔
68
        let (cons_constraint_degrees, cons_constraints_bfe, cons_constraints_xfe) =
1✔
69
            Self::tokenize_circuits(&constraints.cons());
1✔
70
        let (tran_constraint_degrees, tran_constraints_bfe, tran_constraints_xfe) =
1✔
71
            Self::tokenize_circuits(&constraints.tran());
1✔
72
        let (term_constraint_degrees, term_constraints_bfe, term_constraints_xfe) =
1✔
73
            Self::tokenize_circuits(&constraints.term());
1✔
74

1✔
75
        let evaluable_over_base_field = Self::generate_evaluable_implementation_over_field(
1✔
76
            &init_constraints_bfe,
1✔
77
            &cons_constraints_bfe,
1✔
78
            &tran_constraints_bfe,
1✔
79
            &term_constraints_bfe,
1✔
80
            quote!(BFieldElement),
1✔
81
        );
1✔
82
        let evaluable_over_ext_field = Self::generate_evaluable_implementation_over_field(
1✔
83
            &init_constraints_xfe,
1✔
84
            &cons_constraints_xfe,
1✔
85
            &tran_constraints_xfe,
1✔
86
            &term_constraints_xfe,
1✔
87
            quote!(XFieldElement),
1✔
88
        );
1✔
89

1✔
90
        let quotient_trait_impl = quote!(
1✔
91
        impl MasterAuxTable {
1✔
92
            pub const NUM_INITIAL_CONSTRAINTS: usize = #num_init_constraints;
1✔
93
            pub const NUM_CONSISTENCY_CONSTRAINTS: usize = #num_cons_constraints;
1✔
94
            pub const NUM_TRANSITION_CONSTRAINTS: usize = #num_tran_constraints;
1✔
95
            pub const NUM_TERMINAL_CONSTRAINTS: usize = #num_term_constraints;
1✔
96
            pub const NUM_CONSTRAINTS: usize = Self::NUM_INITIAL_CONSTRAINTS
1✔
97
                + Self::NUM_CONSISTENCY_CONSTRAINTS
1✔
98
                + Self::NUM_TRANSITION_CONSTRAINTS
1✔
99
                + Self::NUM_TERMINAL_CONSTRAINTS;
1✔
100

1✔
101
            #[allow(unused_variables)]
1✔
102
            pub fn initial_quotient_degree_bounds(interpolant_degree: isize) -> Vec<isize> {
1✔
103
                let zerofier_degree = 1;
1✔
104
                [#init_constraint_degrees].to_vec()
1✔
105
            }
1✔
106

1✔
107
            #[allow(unused_variables)]
1✔
108
            pub fn consistency_quotient_degree_bounds(
1✔
109
                interpolant_degree: isize,
1✔
110
                padded_height: usize,
1✔
111
            ) -> Vec<isize> {
1✔
112
                let zerofier_degree = padded_height as isize;
1✔
113
                [#cons_constraint_degrees].to_vec()
1✔
114
            }
1✔
115

1✔
116
            #[allow(unused_variables)]
1✔
117
            pub fn transition_quotient_degree_bounds(
1✔
118
                interpolant_degree: isize,
1✔
119
                padded_height: usize,
1✔
120
            ) -> Vec<isize> {
1✔
121
                let zerofier_degree = padded_height as isize - 1;
1✔
122
                [#tran_constraint_degrees].to_vec()
1✔
123
            }
1✔
124

1✔
125
            #[allow(unused_variables)]
1✔
126
            pub fn terminal_quotient_degree_bounds(interpolant_degree: isize) -> Vec<isize> {
1✔
127
                let zerofier_degree = 1;
1✔
128
                [#term_constraint_degrees].to_vec()
1✔
129
            }
1✔
130
        }
1✔
131
        );
1✔
132

1✔
133
        quote!(
1✔
134
            #evaluable_over_base_field
1✔
135
            #evaluable_over_ext_field
1✔
136
            #quotient_trait_impl
1✔
137
        )
1✔
138
    }
1✔
139
}
140

141
impl RustBackend {
142
    fn generate_evaluable_implementation_over_field(
2✔
143
        init_constraints: &TokenStream,
2✔
144
        cons_constraints: &TokenStream,
2✔
145
        tran_constraints: &TokenStream,
2✔
146
        term_constraints: &TokenStream,
2✔
147
        field: TokenStream,
2✔
148
    ) -> TokenStream {
2✔
149
        quote!(
2✔
150
        impl Evaluable<#field> for MasterAuxTable {
2✔
151
            #[allow(unused_variables)]
2✔
152
            fn evaluate_initial_constraints(
2✔
153
                main_row: ArrayView1<#field>,
2✔
154
                aux_row: ArrayView1<XFieldElement>,
2✔
155
                challenges: &Challenges,
2✔
156
            ) -> Vec<XFieldElement> {
2✔
157
                #init_constraints
2✔
158
            }
2✔
159

2✔
160
            #[allow(unused_variables)]
2✔
161
            fn evaluate_consistency_constraints(
2✔
162
                main_row: ArrayView1<#field>,
2✔
163
                aux_row: ArrayView1<XFieldElement>,
2✔
164
                challenges: &Challenges,
2✔
165
            ) -> Vec<XFieldElement> {
2✔
166
                #cons_constraints
2✔
167
            }
2✔
168

2✔
169
            #[allow(unused_variables)]
2✔
170
            fn evaluate_transition_constraints(
2✔
171
                current_main_row: ArrayView1<#field>,
2✔
172
                current_aux_row: ArrayView1<XFieldElement>,
2✔
173
                next_main_row: ArrayView1<#field>,
2✔
174
                next_aux_row: ArrayView1<XFieldElement>,
2✔
175
                challenges: &Challenges,
2✔
176
            ) -> Vec<XFieldElement> {
2✔
177
                #tran_constraints
2✔
178
            }
2✔
179

2✔
180
            #[allow(unused_variables)]
2✔
181
            fn evaluate_terminal_constraints(
2✔
182
                main_row: ArrayView1<#field>,
2✔
183
                aux_row: ArrayView1<XFieldElement>,
2✔
184
                challenges: &Challenges,
2✔
185
            ) -> Vec<XFieldElement> {
2✔
186
                #term_constraints
2✔
187
            }
2✔
188
        }
2✔
189
        )
2✔
190
    }
2✔
191

192
    /// Return a tuple of [`TokenStream`]s corresponding to code evaluating these constraints as
193
    /// well as their degrees. In particular:
194
    /// 1. The first stream contains code that, when evaluated, produces the constraints' degrees,
195
    /// 1. the second stream contains code that, when evaluated, produces the constraints' values,
196
    ///    with the input type for the main row being `BFieldElement`, and
197
    /// 1. the third stream is like the second, except that the input type for the main row is
198
    ///    `XFieldElement`.
199
    fn tokenize_circuits<II: InputIndicator>(
4✔
200
        constraints: &[ConstraintCircuit<II>],
4✔
201
    ) -> (TokenStream, TokenStream, TokenStream) {
4✔
202
        if constraints.is_empty() {
4✔
203
            return (quote!(), quote!(vec![]), quote!(vec![]));
3✔
204
        }
1✔
205

1✔
206
        let mut backend = Self::default();
1✔
207
        let shared_declarations = backend.declare_shared_nodes(constraints);
1✔
208
        let (main_constraints, aux_constraints): (Vec<_>, Vec<_>) = constraints
1✔
209
            .iter()
1✔
210
            .partition(|constraint| constraint.evaluates_to_base_element());
1✔
211

1✔
212
        // The order of the constraints' degrees must match the order of the constraints.
1✔
213
        // Hence, listing the degrees is only possible after the partition into main and auxiliary
1✔
214
        // constraints is known.
1✔
215
        let tokenized_degree_bounds = main_constraints
1✔
216
            .iter()
1✔
217
            .chain(&aux_constraints)
1✔
218
            .map(|circuit| match circuit.degree() {
1✔
219
                d if d > 1 => quote!(interpolant_degree * #d - zerofier_degree),
1✔
220
                1 => quote!(interpolant_degree - zerofier_degree),
1✔
221
                _ => panic!("Constraint degree must be positive"),
×
222
            })
1✔
223
            .collect_vec();
1✔
224
        let tokenized_degree_bounds = quote!(#(#tokenized_degree_bounds),*);
1✔
225

226
        let tokenize_constraint_evaluation = |constraints: &[&ConstraintCircuit<II>]| {
2✔
227
            constraints
2✔
228
                .iter()
2✔
229
                .map(|constraint| backend.evaluate_single_node(constraint))
2✔
230
                .collect_vec()
2✔
231
        };
2✔
232
        let tokenized_main_constraints = tokenize_constraint_evaluation(&main_constraints);
1✔
233
        let tokenized_aux_constraints = tokenize_constraint_evaluation(&aux_constraints);
1✔
234

235
        // If there are no main constraints, the type needs to be explicitly declared.
236
        let tokenized_bfe_main_constraints = match main_constraints.is_empty() {
1✔
237
            true => quote!(let main_constraints: [BFieldElement; 0] = []),
1✔
238
            false => quote!(let main_constraints = [#(#tokenized_main_constraints),*]),
×
239
        };
240
        let tokenized_bfe_constraints = quote!(
1✔
241
            #(#shared_declarations)*
1✔
242
            #tokenized_bfe_main_constraints;
1✔
243
            let aux_constraints = [#(#tokenized_aux_constraints),*];
1✔
244
            main_constraints
1✔
245
                .into_iter()
1✔
246
                .map(|bfe| bfe.lift())
1✔
247
                .chain(aux_constraints)
1✔
248
                .collect()
1✔
249
        );
1✔
250

251
        let tokenized_xfe_constraints = quote!(
1✔
252
            #(#shared_declarations)*
1✔
253
            let main_constraints = [#(#tokenized_main_constraints),*];
1✔
254
            let aux_constraints = [#(#tokenized_aux_constraints),*];
1✔
255
            main_constraints
1✔
256
                .into_iter()
1✔
257
                .chain(aux_constraints)
1✔
258
                .collect()
1✔
259
        );
1✔
260

261
        (
1✔
262
            tokenized_degree_bounds,
1✔
263
            tokenized_bfe_constraints,
1✔
264
            tokenized_xfe_constraints,
1✔
265
        )
1✔
266
    }
4✔
267

268
    /// Declare all shared variables, i.e., those with a ref count greater than 1.
269
    /// These declarations must be made starting from the highest ref count.
270
    /// Otherwise, the resulting code will refer to bindings that have not yet been made.
271
    fn declare_shared_nodes<II: InputIndicator>(
1✔
272
        &mut self,
1✔
273
        constraints: &[ConstraintCircuit<II>],
1✔
274
    ) -> Vec<TokenStream> {
1✔
275
        let constraints_iter = constraints.iter();
1✔
276
        let all_ref_counts = constraints_iter.flat_map(ConstraintCircuit::all_ref_counters);
1✔
277
        let relevant_ref_counts = all_ref_counts.unique().filter(|&x| x > 1);
1✔
278
        let ordered_ref_counts = relevant_ref_counts.sorted().rev();
1✔
279

1✔
280
        ordered_ref_counts
1✔
281
            .map(|count| self.declare_nodes_with_ref_count(constraints, count))
1✔
282
            .collect()
1✔
283
    }
1✔
284

285
    /// Produce the code to evaluate code for all nodes that share a ref count.
286
    fn declare_nodes_with_ref_count<II: InputIndicator>(
×
287
        &mut self,
×
288
        circuits: &[ConstraintCircuit<II>],
×
289
        ref_count: usize,
×
290
    ) -> TokenStream {
×
291
        let all_nodes_in_circuit =
×
292
            |circuit| self.declare_single_node_with_ref_count(circuit, ref_count);
×
293
        let tokenized_circuits = circuits.iter().filter_map(all_nodes_in_circuit);
×
294
        quote!(#(#tokenized_circuits)*)
×
295
    }
×
296

297
    fn declare_single_node_with_ref_count<II: InputIndicator>(
×
298
        &mut self,
×
299
        circuit: &ConstraintCircuit<II>,
×
300
        ref_count: usize,
×
301
    ) -> Option<TokenStream> {
×
302
        if self.scope.contains(&circuit.id) {
×
303
            return None;
×
304
        }
×
305

306
        // constants can be declared trivially
307
        let CircuitExpression::BinOp(_, lhs, rhs) = &circuit.expression else {
×
308
            return None;
×
309
        };
310

311
        if circuit.ref_count < ref_count {
×
312
            let out_left = self.declare_single_node_with_ref_count(&lhs.borrow(), ref_count);
×
313
            let out_right = self.declare_single_node_with_ref_count(&rhs.borrow(), ref_count);
×
314
            return match (out_left, out_right) {
×
315
                (None, None) => None,
×
316
                (Some(l), None) => Some(l),
×
317
                (None, Some(r)) => Some(r),
×
318
                (Some(l), Some(r)) => Some(quote!(#l #r)),
×
319
            };
320
        }
×
321

×
322
        assert_eq!(circuit.ref_count, ref_count);
×
323
        let binding_name = Self::binding_name(circuit);
×
324
        let evaluation = self.evaluate_single_node(circuit);
×
325
        let new_binding = quote!(let #binding_name = #evaluation;);
×
326

×
327
        let is_new_insertion = self.scope.insert(circuit.id);
×
328
        assert!(is_new_insertion);
×
329

330
        Some(new_binding)
×
331
    }
×
332

333
    /// Recursively construct the code for evaluating a single node.
334
    pub fn evaluate_single_node<II: InputIndicator>(
2,882✔
335
        &self,
2,882✔
336
        circuit: &ConstraintCircuit<II>,
2,882✔
337
    ) -> TokenStream {
2,882✔
338
        if self.scope.contains(&circuit.id) {
2,882✔
339
            return Self::binding_name(circuit);
×
340
        }
2,882✔
341

342
        let CircuitExpression::BinOp(binop, lhs, rhs) = &circuit.expression else {
2,882✔
343
            return Self::binding_name(circuit);
1,574✔
344
        };
345

346
        let lhs = self.evaluate_single_node(&lhs.borrow());
1,308✔
347
        let rhs = self.evaluate_single_node(&rhs.borrow());
1,308✔
348
        quote!((#lhs) #binop (#rhs))
1,308✔
349
    }
2,882✔
350

351
    fn binding_name<II: InputIndicator>(circuit: &ConstraintCircuit<II>) -> TokenStream {
1,574✔
352
        match &circuit.expression {
1,574✔
353
            CircuitExpression::BConst(bfe) => Self::tokenize_bfe(*bfe),
411✔
354
            CircuitExpression::XConst(xfe) => Self::tokenize_xfe(*xfe),
×
355
            CircuitExpression::Input(idx) => quote!(#idx),
922✔
356
            CircuitExpression::Challenge(challenge) => quote!(challenges[#challenge]),
241✔
357
            CircuitExpression::BinOp(_, _, _) => {
358
                let node_ident = format_ident!("node_{}", circuit.id);
×
359
                quote!(#node_ident)
×
360
            }
361
        }
362
    }
1,574✔
363
}
364

365
/// The minimal required size of a memory page in [`BFieldElement`]s.
366
pub const MEM_PAGE_SIZE: usize = 1 << 32;
367

368
/// An offset from the [memory layout][layout]'s `free_mem_page_ptr`, in number of
369
/// [`XFieldElement`]s. Indicates the start of the to-be-returned array.
370
///
371
/// [layout]: memory_layout::IntegralMemoryLayout
372
const OUT_ARRAY_OFFSET: usize = {
373
    let max_num_words_for_evaluated_constraints = 1 << 16; // magic!
374
    let out_array_offset_in_words = MEM_PAGE_SIZE - max_num_words_for_evaluated_constraints;
375
    assert!(out_array_offset_in_words % EXTENSION_DEGREE == 0);
376
    out_array_offset_in_words / EXTENSION_DEGREE
377
};
378

379
/// Convenience macro to get raw opcodes of any [`Instruction`] variant, including its argument if
380
/// applicable.
381
///
382
/// [labelled]: triton_vm::instruction::LabelledInstruction::Instruction
383
macro_rules! instr {
384
    ($($instr:tt)*) => {{
385
        let instr = Instruction::$($instr)*;
386
        let opcode = u64::from(instr.opcode());
387
        match instr.arg().map(|arg| arg.value()) {
30✔
388
            Some(arg) => vec![quote!(#opcode), quote!(#arg)],
389
            None => vec![quote!(#opcode)],
390
        }
391
    }};
392
}
393

394
/// Convenience macro to get raw opcode of a [`Push`][push] instruction including its argument.
395
///
396
/// [push]: triton_vm::instruction::AnInstruction::Push
397
macro_rules! push {
398
    ($arg:ident) => {{
399
        let opcode = u64::from(Instruction::Push(BFieldElement::new(0)).opcode());
400
        let arg = u64::from($arg);
401
        vec![quote!(#opcode), quote!(#arg)]
402
    }};
403
    ($list:ident + $offset:expr) => {{
404
        let opcode = u64::from(Instruction::Push(BFieldElement::new(0)).opcode());
405
        let offset = u64::try_from($offset).unwrap();
406
        assert!(offset < u64::MAX - BFieldElement::P);
407
        // clippy will complain about the generated code if it contains `+ 0`
408
        if offset == 0 {
409
            vec![quote!(#opcode), quote!(#$list)]
410
        } else {
411
            vec![quote!(#opcode), quote!(#$list + #offset)]
412
        }
413
    }};
414
}
415

416
impl Codegen for TasmBackend {
417
    /// Emits a function that emits [Triton assembly][tasm] that evaluates Triton VM's AIR
418
    /// constraints over the [extension field][XFieldElement].
419
    ///
420
    /// [tasm]: isa::triton_asm
421
    fn constraint_evaluation_code(constraints: &Constraints) -> TokenStream {
1✔
422
        let doc_comment = Self::doc_comment_static_version();
1✔
423

1✔
424
        let mut backend = Self::statically_known_input_locations();
1✔
425
        let init_constraints = backend.tokenize_circuits(&constraints.init());
1✔
426
        let cons_constraints = backend.tokenize_circuits(&constraints.cons());
1✔
427
        let tran_constraints = backend.tokenize_circuits(&constraints.tran());
1✔
428
        let term_constraints = backend.tokenize_circuits(&constraints.term());
1✔
429
        let prepare_return_values = Self::prepare_return_values();
1✔
430
        let num_instructions = init_constraints.len()
1✔
431
            + cons_constraints.len()
1✔
432
            + tran_constraints.len()
1✔
433
            + term_constraints.len()
1✔
434
            + prepare_return_values.len();
1✔
435
        let num_instructions = u64::try_from(num_instructions).unwrap();
1✔
436

1✔
437
        let convert_and_decode_assembled_instructions = quote!(
1✔
438
            let raw_instructions = raw_instructions
1✔
439
                .into_iter()
1✔
440
                .map(BFieldElement::new)
1✔
441
                .collect::<Vec<_>>();
1✔
442
            let program = Program::decode(&raw_instructions).unwrap();
1✔
443

1✔
444
            let irrelevant_label = |_: &_| String::new();
1✔
445
            program
1✔
446
                .into_iter()
1✔
447
                .map(|instruction| instruction.map_call_address(irrelevant_label))
1✔
448
                .map(LabelledInstruction::Instruction)
1✔
449
                .collect()
1✔
450
        );
1✔
451

452
        let statically_known_input_locations = quote!(
1✔
453
            #[doc = #doc_comment]
1✔
454
            pub fn static_air_constraint_evaluation_tasm(
1✔
455
                mem_layout: StaticTasmConstraintEvaluationMemoryLayout,
1✔
456
            ) -> Vec<LabelledInstruction> {
1✔
457
                let free_mem_page_ptr = mem_layout.free_mem_page_ptr.value();
1✔
458
                let curr_main_row_ptr = mem_layout.curr_main_row_ptr.value();
1✔
459
                let curr_aux_row_ptr = mem_layout.curr_aux_row_ptr.value();
1✔
460
                let next_main_row_ptr = mem_layout.next_main_row_ptr.value();
1✔
461
                let next_aux_row_ptr = mem_layout.next_aux_row_ptr.value();
1✔
462
                let challenges_ptr = mem_layout.challenges_ptr.value();
1✔
463

1✔
464
                let raw_instructions = vec![
1✔
465
                    #num_instructions,
1✔
466
                    #(#init_constraints,)*
1✔
467
                    #(#cons_constraints,)*
1✔
468
                    #(#tran_constraints,)*
1✔
469
                    #(#term_constraints,)*
1✔
470
                    #(#prepare_return_values,)*
1✔
471
                ];
1✔
472
                #convert_and_decode_assembled_instructions
1✔
473
            }
1✔
474
        );
1✔
475

476
        let doc_comment = Self::doc_comment_dynamic_version();
1✔
477

1✔
478
        let mut backend = Self::dynamically_known_input_locations();
1✔
479
        let move_row_pointers = backend.write_row_pointers_to_ram();
1✔
480
        let init_constraints = backend.tokenize_circuits(&constraints.init());
1✔
481
        let cons_constraints = backend.tokenize_circuits(&constraints.cons());
1✔
482
        let tran_constraints = backend.tokenize_circuits(&constraints.tran());
1✔
483
        let term_constraints = backend.tokenize_circuits(&constraints.term());
1✔
484
        let prepare_return_values = Self::prepare_return_values();
1✔
485
        let num_instructions = move_row_pointers.len()
1✔
486
            + init_constraints.len()
1✔
487
            + cons_constraints.len()
1✔
488
            + tran_constraints.len()
1✔
489
            + term_constraints.len()
1✔
490
            + prepare_return_values.len();
1✔
491
        let num_instructions = u64::try_from(num_instructions).unwrap();
1✔
492

493
        let dynamically_known_input_locations = quote!(
1✔
494
            #[doc = #doc_comment]
1✔
495
            pub fn dynamic_air_constraint_evaluation_tasm(
1✔
496
                mem_layout: DynamicTasmConstraintEvaluationMemoryLayout,
1✔
497
            ) -> Vec<LabelledInstruction> {
1✔
498
                let num_pointer_pointers = 4;
1✔
499
                let free_mem_page_ptr = mem_layout.free_mem_page_ptr.value() + num_pointer_pointers;
1✔
500
                let curr_main_row_ptr = mem_layout.free_mem_page_ptr.value();
1✔
501
                let curr_aux_row_ptr = mem_layout.free_mem_page_ptr.value() + 1;
1✔
502
                let next_main_row_ptr = mem_layout.free_mem_page_ptr.value() + 2;
1✔
503
                let next_aux_row_ptr = mem_layout.free_mem_page_ptr.value() + 3;
1✔
504
                let challenges_ptr = mem_layout.challenges_ptr.value();
1✔
505

1✔
506
                let raw_instructions = vec![
1✔
507
                    #num_instructions,
1✔
508
                    #(#move_row_pointers,)*
1✔
509
                    #(#init_constraints,)*
1✔
510
                    #(#cons_constraints,)*
1✔
511
                    #(#tran_constraints,)*
1✔
512
                    #(#term_constraints,)*
1✔
513
                    #(#prepare_return_values,)*
1✔
514
                ];
1✔
515
                #convert_and_decode_assembled_instructions
1✔
516
            }
1✔
517
        );
1✔
518

519
        let uses = Self::uses();
1✔
520
        quote!(
1✔
521
            #uses
1✔
522
            #statically_known_input_locations
1✔
523
            #dynamically_known_input_locations
1✔
524
        )
1✔
525
    }
1✔
526
}
527

528
impl TasmBackend {
529
    fn statically_known_input_locations() -> Self {
2✔
530
        Self {
2✔
531
            scope: HashSet::new(),
2✔
532
            elements_written: 0,
2✔
533
            input_location_is_static: true,
2✔
534
        }
2✔
535
    }
2✔
536

537
    fn dynamically_known_input_locations() -> Self {
1✔
538
        Self {
1✔
539
            input_location_is_static: false,
1✔
540
            ..Self::statically_known_input_locations()
1✔
541
        }
1✔
542
    }
1✔
543

544
    fn uses() -> TokenStream {
1✔
545
        quote!(
1✔
546
            use twenty_first::prelude::BFieldCodec;
1✔
547
            use twenty_first::prelude::BFieldElement;
1✔
548
            use isa::instruction::LabelledInstruction;
1✔
549
            use isa::program::Program;
1✔
550
            use crate::memory_layout::StaticTasmConstraintEvaluationMemoryLayout;
1✔
551
            use crate::memory_layout::DynamicTasmConstraintEvaluationMemoryLayout;
1✔
552
        )
1✔
553
    }
1✔
554

555
    fn doc_comment_static_version() -> &'static str {
1✔
556
        "
1✔
557
         The emitted Triton assembly has the following signature:
1✔
558

1✔
559
         # Signature
1✔
560

1✔
561
         ```text
1✔
562
         BEFORE: _
1✔
563
         AFTER:  _ *evaluated_constraints
1✔
564
         ```
1✔
565
         # Requirements
1✔
566

1✔
567
         In order for this method to emit Triton assembly, various memory regions need to be
1✔
568
         declared. This is done through [`StaticTasmConstraintEvaluationMemoryLayout`]. The memory
1✔
569
         layout must be [integral].
1✔
570

1✔
571
         # Guarantees
1✔
572

1✔
573
         - The emitted code does not declare any labels.
1✔
574
         - The emitted code is “straight-line”, _i.e._, does not contain any of the instructions
1✔
575
           `call`, `return`, `recurse`, `recurse_or_return`, or `skiz`.
1✔
576
         - The emitted code does not contain instruction `halt`.
1✔
577
         - All memory write access of the emitted code is within the bounds of the memory region
1✔
578
           pointed to by `*free_memory_page`.
1✔
579
         - `*evaluated_constraints` points to an array of [`XFieldElement`][xfe]s of length
1✔
580
            [`NUM_CONSTRAINTS`][total]. Each element is the evaluation of one constraint. In
1✔
581
            particular, the disjoint sequence of slices containing
1✔
582
            [`NUM_INITIAL_CONSTRAINTS`][init], [`NUM_CONSISTENCY_CONSTRAINTS`][cons],
1✔
583
            [`NUM_TRANSITION_CONSTRAINTS`][tran], and [`NUM_TERMINAL_CONSTRAINTS`][term]
1✔
584
            (respectively and in this order) correspond to the evaluations of the initial,
1✔
585
            consistency, transition, and terminal constraints.
1✔
586

1✔
587
         [integral]: crate::memory_layout::IntegralMemoryLayout::is_integral
1✔
588
         [xfe]: twenty_first::prelude::XFieldElement
1✔
589
         [total]: crate::table::master_table::MasterAuxTable::NUM_CONSTRAINTS
1✔
590
         [init]: crate::table::master_table::MasterAuxTable::NUM_INITIAL_CONSTRAINTS
1✔
591
         [cons]: crate::table::master_table::MasterAuxTable::NUM_CONSISTENCY_CONSTRAINTS
1✔
592
         [tran]: crate::table::master_table::MasterAuxTable::NUM_TRANSITION_CONSTRAINTS
1✔
593
         [term]: crate::table::master_table::MasterAuxTable::NUM_TERMINAL_CONSTRAINTS
1✔
594
        "
1✔
595
    }
1✔
596

597
    fn doc_comment_dynamic_version() -> &'static str {
1✔
598
        "
1✔
599
         The emitted Triton assembly has the following signature:
1✔
600

1✔
601
         # Signature
1✔
602

1✔
603
         ```text
1✔
604
         BEFORE: _ *current_main_row *current_aux_row *next_main_row *next_aux_row
1✔
605
         AFTER:  _ *evaluated_constraints
1✔
606
         ```
1✔
607
         # Requirements
1✔
608

1✔
609
         In order for this method to emit Triton assembly, various memory regions need to be
1✔
610
         declared. This is done through [`DynamicTasmConstraintEvaluationMemoryLayout`]. The memory
1✔
611
         layout must be [integral].
1✔
612

1✔
613
         # Guarantees
1✔
614

1✔
615
         - The emitted code does not declare any labels.
1✔
616
         - The emitted code is “straight-line”, _i.e._, does not contain any of the instructions
1✔
617
           `call`, `return`, `recurse`, `recurse_or_return`, or `skiz`.
1✔
618
         - The emitted code does not contain instruction `halt`.
1✔
619
         - All memory write access of the emitted code is within the bounds of the memory region
1✔
620
           pointed to by `*free_memory_page`.
1✔
621
         - `*evaluated_constraints` points to an array of [`XFieldElement`][xfe]s of length
1✔
622
            [`NUM_CONSTRAINTS`][total]. Each element is the evaluation of one constraint. In
1✔
623
            particular, the disjoint sequence of slices containing
1✔
624
            [`NUM_INITIAL_CONSTRAINTS`][init], [`NUM_CONSISTENCY_CONSTRAINTS`][cons],
1✔
625
            [`NUM_TRANSITION_CONSTRAINTS`][tran], and [`NUM_TERMINAL_CONSTRAINTS`][term]
1✔
626
            (respectively and in this order) correspond to the evaluations of the initial,
1✔
627
            consistency, transition, and terminal constraints.
1✔
628

1✔
629
         [integral]: crate::memory_layout::IntegralMemoryLayout::is_integral
1✔
630
         [xfe]: twenty_first::prelude::XFieldElement
1✔
631
         [total]: crate::table::master_table::MasterAuxTable::NUM_CONSTRAINTS
1✔
632
         [init]: crate::table::master_table::MasterAuxTable::NUM_INITIAL_CONSTRAINTS
1✔
633
         [cons]: crate::table::master_table::MasterAuxTable::NUM_CONSISTENCY_CONSTRAINTS
1✔
634
         [tran]: crate::table::master_table::MasterAuxTable::NUM_TRANSITION_CONSTRAINTS
1✔
635
         [term]: crate::table::master_table::MasterAuxTable::NUM_TERMINAL_CONSTRAINTS
1✔
636
        "
1✔
637
    }
1✔
638

639
    /// Moves the dynamic arguments ({current, next} {main, aux} row pointers)
640
    /// to static addresses dedicated to them.
641
    fn write_row_pointers_to_ram(&self) -> Vec<TokenStream> {
1✔
642
        // BEFORE: _ *current_main_row *current_aux_row *next_main_row *next_aux_row
1✔
643
        // AFTER: _
1✔
644

1✔
645
        let write_pointer_to_ram = |list_id| {
4✔
646
            [
4✔
647
                push!(list_id + 0),
4✔
648
                instr!(WriteMem(NumberOfWords::N1)),
4✔
649
                instr!(Pop(NumberOfWords::N1)),
4✔
650
            ]
651
            .concat()
4✔
652
        };
4✔
653

654
        [
1✔
655
            IOList::NextAuxRow,
1✔
656
            IOList::NextMainRow,
1✔
657
            IOList::CurrAuxRow,
1✔
658
            IOList::CurrMainRow,
1✔
659
        ]
1✔
660
        .into_iter()
1✔
661
        .flat_map(write_pointer_to_ram)
1✔
662
        .collect()
1✔
663
    }
1✔
664

665
    fn tokenize_circuits<II: InputIndicator>(
8✔
666
        &mut self,
8✔
667
        constraints: &[ConstraintCircuit<II>],
8✔
668
    ) -> Vec<TokenStream> {
8✔
669
        self.scope = HashSet::new();
8✔
670
        let store_shared_nodes = self.store_all_shared_nodes(constraints);
8✔
671

8✔
672
        // to match the `RustBackend`, main constraints must be emitted first
8✔
673
        let (main_constraints, aux_constraints): (Vec<_>, Vec<_>) = constraints
8✔
674
            .iter()
8✔
675
            .partition(|constraint| constraint.evaluates_to_base_element());
8✔
676
        let sorted_constraints = main_constraints.into_iter().chain(aux_constraints);
8✔
677
        let write_to_output = sorted_constraints
8✔
678
            .map(|c| self.write_evaluated_constraint_into_output_list(c))
8✔
679
            .concat();
8✔
680

8✔
681
        [store_shared_nodes, write_to_output].concat()
8✔
682
    }
8✔
683

684
    fn store_all_shared_nodes<II: InputIndicator>(
8✔
685
        &mut self,
8✔
686
        constraints: &[ConstraintCircuit<II>],
8✔
687
    ) -> Vec<TokenStream> {
8✔
688
        let ref_counts = constraints.iter().flat_map(|c| c.all_ref_counters());
8✔
689
        let relevant_ref_counts = ref_counts.sorted().unique().filter(|&c| c > 1).rev();
8✔
690
        relevant_ref_counts
8✔
691
            .map(|count| self.store_all_shared_nodes_of_ref_count(constraints, count))
8✔
692
            .concat()
8✔
693
    }
8✔
694

695
    fn store_all_shared_nodes_of_ref_count<II: InputIndicator>(
×
696
        &mut self,
×
697
        constraints: &[ConstraintCircuit<II>],
×
698
        count: usize,
×
699
    ) -> Vec<TokenStream> {
×
700
        constraints
×
701
            .iter()
×
702
            .map(|c| self.store_single_shared_node_of_ref_count(c, count))
×
703
            .concat()
×
704
    }
×
705

706
    fn store_single_shared_node_of_ref_count<II: InputIndicator>(
×
707
        &mut self,
×
708
        constraint: &ConstraintCircuit<II>,
×
709
        ref_count: usize,
×
710
    ) -> Vec<TokenStream> {
×
711
        if self.scope.contains(&constraint.id) {
×
712
            return vec![];
×
713
        }
×
714

715
        let CircuitExpression::BinOp(_, lhs, rhs) = &constraint.expression else {
×
716
            return vec![];
×
717
        };
718

719
        if constraint.ref_count < ref_count {
×
720
            let out_left = self.store_single_shared_node_of_ref_count(&lhs.borrow(), ref_count);
×
721
            let out_right = self.store_single_shared_node_of_ref_count(&rhs.borrow(), ref_count);
×
722
            return [out_left, out_right].concat();
×
723
        }
×
724

×
725
        assert_eq!(constraint.ref_count, ref_count);
×
726
        let evaluate = self.evaluate_single_node(constraint);
×
727
        let store = Self::store_ext_field_element(constraint.id);
×
728
        let is_new_insertion = self.scope.insert(constraint.id);
×
729
        assert!(is_new_insertion);
×
730

731
        [evaluate, store].concat()
×
732
    }
×
733

734
    fn evaluate_single_node<II: InputIndicator>(
18✔
735
        &self,
18✔
736
        constraint: &ConstraintCircuit<II>,
18✔
737
    ) -> Vec<TokenStream> {
18✔
738
        if self.scope.contains(&constraint.id) {
18✔
739
            return self.load_node(constraint);
×
740
        }
18✔
741

742
        let CircuitExpression::BinOp(binop, lhs, rhs) = &constraint.expression else {
18✔
743
            return self.load_node(constraint);
10✔
744
        };
745

746
        let lhs = self.evaluate_single_node(&lhs.borrow());
8✔
747
        let rhs = self.evaluate_single_node(&rhs.borrow());
8✔
748
        let binop = match binop {
8✔
749
            BinOp::Add => instr!(XxAdd),
2✔
750
            BinOp::Mul => instr!(XxMul),
6✔
751
        };
752
        [lhs, rhs, binop].concat()
8✔
753
    }
18✔
754

755
    fn write_evaluated_constraint_into_output_list<II: InputIndicator>(
2✔
756
        &mut self,
2✔
757
        constraint: &ConstraintCircuit<II>,
2✔
758
    ) -> Vec<TokenStream> {
2✔
759
        let evaluated_constraint = self.evaluate_single_node(constraint);
2✔
760
        let element_index = OUT_ARRAY_OFFSET + self.elements_written;
2✔
761
        let store_element = Self::store_ext_field_element(element_index);
2✔
762
        self.elements_written += 1;
2✔
763
        [evaluated_constraint, store_element].concat()
2✔
764
    }
2✔
765

766
    fn load_node<II: InputIndicator>(&self, circuit: &ConstraintCircuit<II>) -> Vec<TokenStream> {
10✔
767
        match circuit.expression {
10✔
768
            CircuitExpression::BConst(bfe) => Self::load_ext_field_constant(bfe.into()),
4✔
769
            CircuitExpression::XConst(xfe) => Self::load_ext_field_constant(xfe),
×
770
            CircuitExpression::Input(input) => self.load_input(input),
4✔
771
            CircuitExpression::Challenge(challenge_idx) => Self::load_challenge(challenge_idx),
2✔
772
            CircuitExpression::BinOp(_, _, _) => Self::load_evaluated_bin_op(circuit.id),
×
773
        }
774
    }
10✔
775

776
    fn load_ext_field_constant(xfe: XFieldElement) -> Vec<TokenStream> {
4✔
777
        let [c0, c1, c2] = xfe.coefficients.map(|c| push!(c));
12✔
778
        [c2, c1, c0].concat()
4✔
779
    }
4✔
780

781
    fn load_input<II: InputIndicator>(&self, input: II) -> Vec<TokenStream> {
4✔
782
        let list = match (input.is_current_row(), input.is_main_table_column()) {
4✔
783
            (true, true) => IOList::CurrMainRow,
2✔
784
            (true, false) => IOList::CurrAuxRow,
2✔
NEW
785
            (false, true) => IOList::NextMainRow,
×
NEW
786
            (false, false) => IOList::NextAuxRow,
×
787
        };
788
        if self.input_location_is_static {
4✔
789
            Self::load_ext_field_element_from_list(list, input.column())
2✔
790
        } else {
791
            Self::load_ext_field_element_from_pointed_to_list(list, input.column())
2✔
792
        }
793
    }
4✔
794

795
    fn load_challenge(challenge_idx: usize) -> Vec<TokenStream> {
2✔
796
        Self::load_ext_field_element_from_list(IOList::Challenges, challenge_idx)
2✔
797
    }
2✔
798

799
    fn load_evaluated_bin_op(node_id: usize) -> Vec<TokenStream> {
×
800
        Self::load_ext_field_element_from_list(IOList::FreeMemPage, node_id)
×
801
    }
×
802

803
    fn load_ext_field_element_from_list(list: IOList, element_index: usize) -> Vec<TokenStream> {
4✔
804
        let word_index = Self::element_index_to_word_index_for_reading(element_index);
4✔
805

4✔
806
        [
4✔
807
            push!(list + word_index),
4✔
808
            instr!(ReadMem(NumberOfWords::N3)),
4✔
809
            instr!(Pop(NumberOfWords::N1)),
4✔
810
        ]
811
        .concat()
4✔
812
    }
4✔
813

814
    fn load_ext_field_element_from_pointed_to_list(
2✔
815
        list: IOList,
2✔
816
        element_index: usize,
2✔
817
    ) -> Vec<TokenStream> {
2✔
818
        let word_index = Self::element_index_to_word_index_for_reading(element_index);
2✔
819

2✔
820
        [
2✔
821
            push!(list + 0),
2✔
822
            instr!(ReadMem(NumberOfWords::N1)),
2✔
823
            instr!(Pop(NumberOfWords::N1)),
2✔
824
            instr!(AddI(word_index)),
2✔
825
            instr!(ReadMem(NumberOfWords::N3)),
2✔
826
            instr!(Pop(NumberOfWords::N1)),
2✔
827
        ]
828
        .concat()
2✔
829
    }
2✔
830

831
    fn element_index_to_word_index_for_reading(element_index: usize) -> BFieldElement {
6✔
832
        let word_offset = element_index * EXTENSION_DEGREE;
6✔
833
        let start_to_read_offset = EXTENSION_DEGREE - 1;
6✔
834
        let word_index = word_offset + start_to_read_offset;
6✔
835
        bfe!(u64::try_from(word_index).unwrap())
6✔
836
    }
6✔
837

838
    fn store_ext_field_element(element_index: usize) -> Vec<TokenStream> {
2✔
839
        let free_mem_page = IOList::FreeMemPage;
2✔
840

2✔
841
        let word_offset = element_index * EXTENSION_DEGREE;
2✔
842
        let word_index = u64::try_from(word_offset).unwrap();
2✔
843

844
        let push_address = push!(free_mem_page + word_index);
2✔
845
        let write_mem = instr!(WriteMem(NumberOfWords::N3));
2✔
846
        let pop = instr!(Pop(NumberOfWords::N1));
2✔
847

848
        [push_address, write_mem, pop].concat()
2✔
849
    }
2✔
850

851
    fn prepare_return_values() -> Vec<TokenStream> {
2✔
852
        let free_mem_page = IOList::FreeMemPage;
2✔
853
        let out_array_offset_in_num_bfes = OUT_ARRAY_OFFSET * EXTENSION_DEGREE;
2✔
854
        let out_array_offset = u64::try_from(out_array_offset_in_num_bfes).unwrap();
2✔
855
        push!(free_mem_page + out_array_offset)
2✔
856
    }
2✔
857
}
858

859
#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
860
enum IOList {
861
    FreeMemPage,
862
    CurrMainRow,
863
    CurrAuxRow,
864
    NextMainRow,
865
    NextAuxRow,
866
    Challenges,
867
}
868

869
impl ToTokens for IOList {
870
    fn to_tokens(&self, tokens: &mut TokenStream) {
14✔
871
        match self {
14✔
872
            IOList::FreeMemPage => tokens.extend(quote!(free_mem_page_ptr)),
4✔
873
            IOList::CurrMainRow => tokens.extend(quote!(curr_main_row_ptr)),
3✔
874
            IOList::CurrAuxRow => tokens.extend(quote!(curr_aux_row_ptr)),
3✔
875
            IOList::NextMainRow => tokens.extend(quote!(next_main_row_ptr)),
1✔
876
            IOList::NextAuxRow => tokens.extend(quote!(next_aux_row_ptr)),
1✔
877
            IOList::Challenges => tokens.extend(quote!(challenges_ptr)),
2✔
878
        }
879
    }
14✔
880
}
881

882
#[cfg(test)]
883
mod tests {
884
    use constraint_circuit::ConstraintCircuitBuilder;
885
    use constraint_circuit::SingleRowIndicator;
886
    use twenty_first::prelude::*;
887

888
    use super::*;
889

890
    pub(crate) fn mini_constraints() -> Constraints {
2✔
891
        let circuit_builder = ConstraintCircuitBuilder::new();
2✔
892
        let challenge = |c: usize| circuit_builder.challenge(c);
2✔
893
        let constant = |c: u32| circuit_builder.x_constant(c);
2✔
894
        let main_row = |i| circuit_builder.input(SingleRowIndicator::Main(i));
2✔
895
        let aux_row = |i| circuit_builder.input(SingleRowIndicator::Aux(i));
2✔
896

897
        let constraint = main_row(0) * challenge(3) - aux_row(1) * constant(42);
2✔
898

2✔
899
        Constraints {
2✔
900
            init: vec![constraint],
2✔
901
            cons: vec![],
2✔
902
            tran: vec![],
2✔
903
            term: vec![],
2✔
904
        }
2✔
905
    }
2✔
906

907
    pub fn print_constraints<B: Codegen>(constraints: &Constraints) {
2✔
908
        let code = B::constraint_evaluation_code(constraints);
2✔
909
        let syntax_tree = syn::parse2(code).unwrap();
2✔
910
        let code = prettyplease::unparse(&syntax_tree);
2✔
911
        println!("{code}");
2✔
912
    }
2✔
913

914
    #[test]
915
    fn tokenizing_base_field_elements_produces_expected_result() {
1✔
916
        let bfe = bfe!(42);
1✔
917
        let expected = "BFieldElement :: from_raw_u64 (180388626390u64)";
1✔
918
        assert_eq!(expected, RustBackend::tokenize_bfe(bfe).to_string());
1✔
919
    }
1✔
920

921
    #[test]
922
    fn tokenizing_extension_field_elements_produces_expected_result() {
1✔
923
        let xfe = xfe!([42, 43, 44]);
1✔
924
        let expected = "XFieldElement :: new ([\
1✔
925
            BFieldElement :: from_raw_u64 (180388626390u64) , \
1✔
926
            BFieldElement :: from_raw_u64 (184683593685u64) , \
1✔
927
            BFieldElement :: from_raw_u64 (188978560980u64)\
1✔
928
        ])";
1✔
929
        assert_eq!(expected, RustBackend::tokenize_xfe(xfe).to_string());
1✔
930
    }
1✔
931

932
    #[test]
933
    fn print_mini_constraints_rust() {
1✔
934
        print_constraints::<RustBackend>(&mini_constraints());
1✔
935
    }
1✔
936

937
    #[test]
938
    fn print_mini_constraints_tasm() {
1✔
939
        print_constraints::<TasmBackend>(&mini_constraints());
1✔
940
    }
1✔
941
}
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2025 Coveralls, Inc