o1vm/interpreters/mips/
constraints.rs

1use crate::{
2    interpreters::mips::{
3        column::{
4            ColumnAlias as MIPSColumn, MIPS_BYTE_COUNTER_OFF, MIPS_CHUNK_BYTES_LEN,
5            MIPS_END_OF_PREIMAGE_OFF, MIPS_HASH_COUNTER_OFF, MIPS_HAS_N_BYTES_OFF,
6            MIPS_LENGTH_BYTES_OFF, MIPS_NUM_BYTES_READ_OFF, MIPS_PREIMAGE_BYTES_OFF,
7            MIPS_PREIMAGE_CHUNK_OFF, MIPS_PREIMAGE_KEY, N_MIPS_REL_COLS,
8        },
9        interpreter::{interpret_instruction, InterpreterEnv},
10        Instruction,
11    },
12    lookups::{Lookup, LookupTableIDs},
13    E,
14};
15use ark_ff::{Field, One};
16use kimchi::circuits::{
17    expr::{ConstantTerm::Literal, Expr, ExprInner, Operations, Variable},
18    gate::CurrOrNext,
19};
20use kimchi_msm::columns::ColumnIndexer as _;
21use std::array;
22use strum::IntoEnumIterator;
23
24use super::column::N_MIPS_SEL_COLS;
25
26/// The environment keeping the constraints between the different polynomials
27pub struct Env<Fp> {
28    scratch_state_idx: usize,
29    scratch_state_idx_inverse: usize,
30    /// A list of constraints, which are multi-variate polynomials over a field,
31    /// represented using the expression framework of `kimchi`.
32    constraints: Vec<E<Fp>>,
33    lookups: Vec<Lookup<E<Fp>>>,
34    /// Selector (as expression) for the constraints of the environment.
35    selector: Option<E<Fp>>,
36}
37
38impl<Fp: Field> Default for Env<Fp> {
39    fn default() -> Self {
40        Self {
41            scratch_state_idx: 0,
42            scratch_state_idx_inverse: 0,
43            constraints: Vec::new(),
44            lookups: Vec::new(),
45            selector: None,
46        }
47    }
48}
49
50impl<Fp: Field> InterpreterEnv for Env<Fp> {
51    /// In the concrete implementation for the constraints, the interpreter will
52    /// work over columns. The position in this case can be seen as a new
53    /// variable/input of our circuit.
54    type Position = MIPSColumn;
55
56    // Use one of the available columns. It won't create a new column every time
57    // this function is called. The number of columns is defined upfront by
58    // crate::interpreters::mips::column::SCRATCH_SIZE.
59    fn alloc_scratch(&mut self) -> Self::Position {
60        // All columns are implemented using a simple index, and a name is given
61        // to the index. See crate::interpreters::mips::column::SCRATCH_SIZE for the maximum number of
62        // columns the circuit can use.
63        let scratch_idx = self.scratch_state_idx;
64        self.scratch_state_idx += 1;
65        MIPSColumn::ScratchState(scratch_idx)
66    }
67
68    fn alloc_scratch_inverse(&mut self) -> Self::Position {
69        let scratch_idx = self.scratch_state_idx_inverse;
70        self.scratch_state_idx_inverse += 1;
71        MIPSColumn::ScratchStateInverse(scratch_idx)
72    }
73
74    type Variable = E<Fp>;
75
76    fn variable(&self, column: Self::Position) -> Self::Variable {
77        Expr::Atom(ExprInner::Cell(Variable {
78            col: column.to_column(),
79            row: CurrOrNext::Curr,
80        }))
81    }
82
83    fn activate_selector(&mut self, selector: Instruction) {
84        // Sanity check: we only want to activate once per instruction
85        assert!(self.selector.is_none(), "A selector has been already activated. You might need to reset the environment if you want to start a new instruction.");
86        let n = usize::from(selector) - N_MIPS_REL_COLS;
87        self.selector = Some(self.variable(MIPSColumn::Selector(n)))
88    }
89
90    fn add_constraint(&mut self, assert_equals_zero: Self::Variable) {
91        self.constraints.push(assert_equals_zero)
92    }
93
94    fn check_is_zero(_assert_equals_zero: &Self::Variable) {
95        // No-op, witness only
96    }
97
98    fn check_equal(_x: &Self::Variable, _y: &Self::Variable) {
99        // No-op, witness only
100    }
101
102    fn check_boolean(_x: &Self::Variable) {
103        // No-op, witness only
104    }
105
106    fn add_lookup(&mut self, lookup: Lookup<Self::Variable>) {
107        self.lookups.push(lookup);
108    }
109
110    fn instruction_counter(&self) -> Self::Variable {
111        self.variable(MIPSColumn::InstructionCounter)
112    }
113
114    fn increase_instruction_counter(&mut self) {
115        // No-op, witness only
116    }
117
118    unsafe fn fetch_register(
119        &mut self,
120        _idx: &Self::Variable,
121        output: Self::Position,
122    ) -> Self::Variable {
123        self.variable(output)
124    }
125
126    unsafe fn push_register_if(
127        &mut self,
128        _idx: &Self::Variable,
129        _value: Self::Variable,
130        _if_is_true: &Self::Variable,
131    ) {
132        // No-op, witness only
133    }
134
135    unsafe fn fetch_register_access(
136        &mut self,
137        _idx: &Self::Variable,
138        output: Self::Position,
139    ) -> Self::Variable {
140        self.variable(output)
141    }
142
143    unsafe fn push_register_access_if(
144        &mut self,
145        _idx: &Self::Variable,
146        _value: Self::Variable,
147        _if_is_true: &Self::Variable,
148    ) {
149        // No-op, witness only
150    }
151
152    unsafe fn fetch_memory(
153        &mut self,
154        _addr: &Self::Variable,
155        output: Self::Position,
156    ) -> Self::Variable {
157        self.variable(output)
158    }
159
160    unsafe fn push_memory(&mut self, _addr: &Self::Variable, _value: Self::Variable) {
161        // No-op, witness only
162    }
163
164    unsafe fn fetch_memory_access(
165        &mut self,
166        _addr: &Self::Variable,
167        output: Self::Position,
168    ) -> Self::Variable {
169        self.variable(output)
170    }
171
172    unsafe fn push_memory_access(&mut self, _addr: &Self::Variable, _value: Self::Variable) {
173        // No-op, witness only
174    }
175
176    fn constant(x: u32) -> Self::Variable {
177        Self::Variable::constant(Operations::from(Literal(Fp::from(x))))
178    }
179
180    unsafe fn bitmask(
181        &mut self,
182        _x: &Self::Variable,
183        _highest_bit: u32,
184        _lowest_bit: u32,
185        position: Self::Position,
186    ) -> Self::Variable {
187        self.variable(position)
188    }
189
190    unsafe fn shift_left(
191        &mut self,
192        _x: &Self::Variable,
193        _by: &Self::Variable,
194        position: Self::Position,
195    ) -> Self::Variable {
196        self.variable(position)
197    }
198
199    unsafe fn shift_right(
200        &mut self,
201        _x: &Self::Variable,
202        _by: &Self::Variable,
203        position: Self::Position,
204    ) -> Self::Variable {
205        self.variable(position)
206    }
207
208    unsafe fn shift_right_arithmetic(
209        &mut self,
210        _x: &Self::Variable,
211        _by: &Self::Variable,
212        position: Self::Position,
213    ) -> Self::Variable {
214        self.variable(position)
215    }
216
217    unsafe fn test_zero(
218        &mut self,
219        _x: &Self::Variable,
220        position: Self::Position,
221    ) -> Self::Variable {
222        self.variable(position)
223    }
224
225    fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable {
226        let res = {
227            let pos = self.alloc_scratch();
228            unsafe { self.test_zero(x, pos) }
229        };
230        let x_inv_or_zero = {
231            let pos = self.alloc_scratch_inverse();
232            self.variable(pos)
233        };
234        // If x = 0, then res = 1 and x_inv_or_zero = 0
235        // If x <> 0, then res = 0 and x_inv_or_zero = x^(-1)
236        self.add_constraint(x.clone() * x_inv_or_zero.clone() + res.clone() - Self::constant(1));
237        self.add_constraint(x.clone() * res.clone());
238        res
239    }
240
241    fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable {
242        self.is_zero(&(x.clone() - y.clone()))
243    }
244
245    unsafe fn test_less_than(
246        &mut self,
247        _x: &Self::Variable,
248        _y: &Self::Variable,
249        position: Self::Position,
250    ) -> Self::Variable {
251        self.variable(position)
252    }
253
254    unsafe fn test_less_than_signed(
255        &mut self,
256        _x: &Self::Variable,
257        _y: &Self::Variable,
258        position: Self::Position,
259    ) -> Self::Variable {
260        self.variable(position)
261    }
262
263    unsafe fn and_witness(
264        &mut self,
265        _x: &Self::Variable,
266        _y: &Self::Variable,
267        position: Self::Position,
268    ) -> Self::Variable {
269        self.variable(position)
270    }
271
272    unsafe fn nor_witness(
273        &mut self,
274        _x: &Self::Variable,
275        _y: &Self::Variable,
276        position: Self::Position,
277    ) -> Self::Variable {
278        self.variable(position)
279    }
280
281    unsafe fn or_witness(
282        &mut self,
283        _x: &Self::Variable,
284        _y: &Self::Variable,
285        position: Self::Position,
286    ) -> Self::Variable {
287        self.variable(position)
288    }
289
290    unsafe fn xor_witness(
291        &mut self,
292        _x: &Self::Variable,
293        _y: &Self::Variable,
294        position: Self::Position,
295    ) -> Self::Variable {
296        self.variable(position)
297    }
298
299    unsafe fn add_witness(
300        &mut self,
301        _y: &Self::Variable,
302        _x: &Self::Variable,
303        out_position: Self::Position,
304        overflow_position: Self::Position,
305    ) -> (Self::Variable, Self::Variable) {
306        (
307            self.variable(out_position),
308            self.variable(overflow_position),
309        )
310    }
311
312    unsafe fn sub_witness(
313        &mut self,
314        _y: &Self::Variable,
315        _x: &Self::Variable,
316        out_position: Self::Position,
317        underflow_position: Self::Position,
318    ) -> (Self::Variable, Self::Variable) {
319        (
320            self.variable(out_position),
321            self.variable(underflow_position),
322        )
323    }
324
325    unsafe fn mul_signed_witness(
326        &mut self,
327        _x: &Self::Variable,
328        _y: &Self::Variable,
329        position: Self::Position,
330    ) -> Self::Variable {
331        self.variable(position)
332    }
333
334    unsafe fn mul_hi_lo_signed(
335        &mut self,
336        _x: &Self::Variable,
337        _y: &Self::Variable,
338        position_hi: Self::Position,
339        position_lo: Self::Position,
340    ) -> (Self::Variable, Self::Variable) {
341        (self.variable(position_hi), self.variable(position_lo))
342    }
343
344    unsafe fn mul_hi_lo(
345        &mut self,
346        _x: &Self::Variable,
347        _y: &Self::Variable,
348        position_hi: Self::Position,
349        position_lo: Self::Position,
350    ) -> (Self::Variable, Self::Variable) {
351        (self.variable(position_hi), self.variable(position_lo))
352    }
353
354    unsafe fn divmod_signed(
355        &mut self,
356        _x: &Self::Variable,
357        _y: &Self::Variable,
358        position_quotient: Self::Position,
359        position_remainder: Self::Position,
360    ) -> (Self::Variable, Self::Variable) {
361        (
362            self.variable(position_quotient),
363            self.variable(position_remainder),
364        )
365    }
366
367    unsafe fn divmod(
368        &mut self,
369        _x: &Self::Variable,
370        _y: &Self::Variable,
371        position_quotient: Self::Position,
372        position_remainder: Self::Position,
373    ) -> (Self::Variable, Self::Variable) {
374        (
375            self.variable(position_quotient),
376            self.variable(position_remainder),
377        )
378    }
379
380    unsafe fn count_leading_zeros(
381        &mut self,
382        _x: &Self::Variable,
383        position: Self::Position,
384    ) -> Self::Variable {
385        self.variable(position)
386    }
387
388    unsafe fn count_leading_ones(
389        &mut self,
390        _x: &Self::Variable,
391        position: Self::Position,
392    ) -> Self::Variable {
393        self.variable(position)
394    }
395
396    fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable {
397        let res = self.variable(position);
398        self.constraints.push(x.clone() - res.clone());
399        res
400    }
401
402    fn set_halted(&mut self, _flag: Self::Variable) {
403        // TODO
404    }
405
406    fn report_exit(&mut self, _exit_code: &Self::Variable) {}
407
408    /// This function checks that the preimage is read correctly.
409    /// It adds 13 constraints, and 5 lookups for the communication channel.
410    /// In particular, at every step it writes the bytes of the preimage into
411    /// the channel (excluding the length bytes) and it reads the hash digest
412    /// from the channel when the preimage is fully read.
413    /// The output is the actual number of bytes that have been read.
414    fn request_preimage_write(
415        &mut self,
416        _addr: &Self::Variable,
417        len: &Self::Variable,
418        pos: Self::Position,
419    ) -> Self::Variable {
420        // How many hashes have been performed so far in the circuit
421        let hash_counter = self.variable(Self::Position::ScratchState(MIPS_HASH_COUNTER_OFF));
422
423        // How many bytes have been read from the preimage so far
424        let byte_counter = self.variable(Self::Position::ScratchState(MIPS_BYTE_COUNTER_OFF));
425
426        // Whether this is the last step of the preimage or not (boolean)
427        let end_of_preimage = self.variable(Self::Position::ScratchState(MIPS_END_OF_PREIMAGE_OFF));
428
429        // How many preimage bytes are being processed in this instruction
430        // FIXME: need to connect this to REGISTER_PREIMAGE_OFFSET or pos?
431        let num_preimage_bytes_read =
432            self.variable(Self::Position::ScratchState(MIPS_NUM_BYTES_READ_OFF));
433
434        // The chunk of at most 4 bytes that is being processed from the
435        // preimage in this instruction
436        let this_chunk = self.variable(Self::Position::ScratchState(MIPS_PREIMAGE_CHUNK_OFF));
437
438        // The preimage key composed of 248 bits
439        let preimage_key = self.variable(Self::Position::ScratchState(MIPS_PREIMAGE_KEY));
440
441        // The (at most) 4 bytes that are being processed from the preimage
442        let bytes: [_; MIPS_CHUNK_BYTES_LEN] = array::from_fn(|i| {
443            self.variable(Self::Position::ScratchState(MIPS_PREIMAGE_BYTES_OFF + i))
444        });
445
446        // The (at most) 4 bytes that are being read from the bytelength
447        let length_bytes: [_; MIPS_CHUNK_BYTES_LEN] = array::from_fn(|i| {
448            self.variable(Self::Position::ScratchState(MIPS_LENGTH_BYTES_OFF + i))
449        });
450
451        // Whether the preimage chunk read has at least n bytes (1, 2, 3, or 4).
452        // It will be all zero when the syscall reads the bytelength prefix.
453        let has_n_bytes: [_; MIPS_CHUNK_BYTES_LEN] = array::from_fn(|i| {
454            self.variable(Self::Position::ScratchState(MIPS_HAS_N_BYTES_OFF + i))
455        });
456
457        // The actual number of bytes read in this instruction, will be 0 <= x <= len <= 4
458        let actual_read_bytes = self.variable(pos);
459
460        // EXTRA 13 CONSTRAINTS
461
462        // 5 Booleanity constraints
463        {
464            for var in has_n_bytes.iter() {
465                self.assert_boolean(var.clone());
466            }
467            self.assert_boolean(end_of_preimage.clone());
468        }
469
470        // + 4 constraints
471        {
472            // Expressions that are nonzero when the exact corresponding number
473            // of preimage bytes are read (case 0 bytes used when bytelength is read)
474            // TODO: embed any more complex logic to know how many bytes are read
475            //       depending on the address and length as in the witness?
476            // FIXME: use the lines below when the issue with `equal` is solved
477            //        that will bring the number of constraints from 23 to 31
478            //        (meaning the unit test needs to be manually adapted)
479            // let preimage_1 = self.equal(&num_preimage_bytes_read, &Expr::from(1));
480            // let preimage_2 = self.equal(&num_preimage_bytes_read, &Expr::from(2));
481            // let preimage_3 = self.equal(&num_preimage_bytes_read, &Expr::from(3));
482            // let preimage_4 = self.equal(&num_preimage_bytes_read, &Expr::from(4));
483
484            let preimage_1 = (num_preimage_bytes_read.clone())
485                * (num_preimage_bytes_read.clone() - Expr::from(2))
486                * (num_preimage_bytes_read.clone() - Expr::from(3))
487                * (num_preimage_bytes_read.clone() - Expr::from(4));
488            let preimage_2 = (num_preimage_bytes_read.clone())
489                * (num_preimage_bytes_read.clone() - Expr::from(1))
490                * (num_preimage_bytes_read.clone() - Expr::from(3))
491                * (num_preimage_bytes_read.clone() - Expr::from(4));
492            let preimage_3 = (num_preimage_bytes_read.clone())
493                * (num_preimage_bytes_read.clone() - Expr::from(1))
494                * (num_preimage_bytes_read.clone() - Expr::from(2))
495                * (num_preimage_bytes_read.clone() - Expr::from(4));
496            let preimage_4 = (num_preimage_bytes_read.clone())
497                * (num_preimage_bytes_read.clone() - Expr::from(1))
498                * (num_preimage_bytes_read.clone() - Expr::from(2))
499                * (num_preimage_bytes_read.clone() - Expr::from(3));
500
501            // Constrain the byte decomposition of the preimage chunk
502            // NOTE: these constraints also hold when 0 preimage bytes are read
503            {
504                // When only 1 preimage byte is read, the chunk equals byte[0]
505                self.add_constraint(preimage_1 * (this_chunk.clone() - bytes[0].clone()));
506                // When 2 bytes are read, the chunk is equal to the
507                // byte[0] * 2^8 + byte[1]
508                self.add_constraint(
509                    preimage_2
510                        * (this_chunk.clone()
511                            - (bytes[0].clone() * Expr::from(2u64.pow(8)) + bytes[1].clone())),
512                );
513                // When 3 bytes are read, the chunk is equal to
514                // byte[0] * 2^16 + byte[1] * 2^8 + byte[2]
515                self.add_constraint(
516                    preimage_3
517                        * (this_chunk.clone()
518                            - (bytes[0].clone() * Expr::from(2u64.pow(16))
519                                + bytes[1].clone() * Expr::from(2u64.pow(8))
520                                + bytes[2].clone())),
521                );
522                // When all 4 bytes are read, the chunk is equal to
523                // byte[0] * 2^24 + byte[1] * 2^16 + byte[2] * 2^8 + byte[3]
524                self.add_constraint(
525                    preimage_4
526                        * (this_chunk.clone()
527                            - (bytes[0].clone() * Expr::from(2u64.pow(24))
528                                + bytes[1].clone() * Expr::from(2u64.pow(16))
529                                + bytes[2].clone() * Expr::from(2u64.pow(8))
530                                + bytes[3].clone())),
531                );
532            }
533
534            // +4 constraints
535            // Constrain the bytes flags depending on the number of preimage
536            // bytes read in this row
537            {
538                // When at least has_1_byte, then any number of bytes can be
539                // read <=> Check that you can only read 1, 2, 3 or 4 bytes
540                self.add_constraint(
541                    has_n_bytes[0].clone()
542                        * (num_preimage_bytes_read.clone() - Expr::from(1))
543                        * (num_preimage_bytes_read.clone() - Expr::from(2))
544                        * (num_preimage_bytes_read.clone() - Expr::from(3))
545                        * (num_preimage_bytes_read.clone() - Expr::from(4)),
546                );
547
548                // When at least has_2_byte, then any number of bytes can be
549                // read from the preimage except 1
550                self.add_constraint(
551                    has_n_bytes[1].clone()
552                        * (num_preimage_bytes_read.clone() - Expr::from(2))
553                        * (num_preimage_bytes_read.clone() - Expr::from(3))
554                        * (num_preimage_bytes_read.clone() - Expr::from(4)),
555                );
556                // When at least has_3_byte, then any number of bytes can be
557                // read from the preimage except 1 nor 2
558                self.add_constraint(
559                    has_n_bytes[2].clone()
560                        * (num_preimage_bytes_read.clone() - Expr::from(3))
561                        * (num_preimage_bytes_read.clone() - Expr::from(4)),
562                );
563
564                // When has_4_byte, then only can read 4 preimage bytes
565                self.add_constraint(
566                    has_n_bytes[3].clone() * (num_preimage_bytes_read.clone() - Expr::from(4)),
567                );
568            }
569        }
570
571        // FIXED LOOKUPS
572
573        // Byte checks with lookups: both preimage and length bytes are checked
574        // TODO: think of a way to merge these together to perform 4 lookups
575        // instead of 8 per row
576        // FIXME: understand if length bytes can ever be read together with
577        // preimage bytes. If not, then we can merge the lookups and just run
578        // 4 lookups per row for the byte checks. AKA: does the oracle always
579        // read the length bytes first and then the preimage bytes, with no
580        // overlapping?
581        for byte in bytes.iter() {
582            self.add_lookup(Lookup::read_one(
583                LookupTableIDs::ByteLookup,
584                vec![byte.clone()],
585            ));
586        }
587        for b in length_bytes.iter() {
588            self.add_lookup(Lookup::read_one(
589                LookupTableIDs::ByteLookup,
590                vec![b.clone()],
591            ));
592        }
593
594        // Check that 0 <= preimage read <= actual read <= len <= 4
595        self.lookup_2bits(len);
596        self.lookup_2bits(&actual_read_bytes);
597        self.lookup_2bits(&num_preimage_bytes_read);
598        self.lookup_2bits(&(len.clone() - actual_read_bytes.clone()));
599        self.lookup_2bits(&(actual_read_bytes.clone() - num_preimage_bytes_read.clone()));
600
601        // COMMUNICATION CHANNEL: Write preimage chunk (1, 2, 3, or 4 bytes)
602        for i in 0..MIPS_CHUNK_BYTES_LEN {
603            self.add_lookup(Lookup::write_if(
604                has_n_bytes[i].clone(),
605                LookupTableIDs::SyscallLookup,
606                vec![
607                    hash_counter.clone(),
608                    byte_counter.clone() + Expr::from(i as u64),
609                    bytes[i].clone(),
610                ],
611            ));
612        }
613
614        // COMMUNICATION CHANNEL: Read hash output
615        // If no more bytes left to be read, then the end of the preimage is
616        // true.
617        // TODO: keep track of counter to diminish the number of bytes at
618        // each step and check it is zero at the end?
619        self.add_lookup(Lookup::read_if(
620            end_of_preimage,
621            LookupTableIDs::SyscallLookup,
622            vec![hash_counter.clone(), preimage_key],
623        ));
624
625        // Return actual length read as variable, stored in `pos`
626        actual_read_bytes
627    }
628
629    fn request_hint_write(&mut self, _addr: &Self::Variable, _len: &Self::Variable) {
630        // No-op, witness only
631    }
632
633    fn reset(&mut self) {
634        self.scratch_state_idx = 0;
635        self.scratch_state_idx_inverse = 0;
636        self.constraints.clear();
637        self.lookups.clear();
638        self.selector = None;
639    }
640}
641
642impl<Fp: Field> Env<Fp> {
643    /// Return the constraints for the selector.
644    /// Each selector must be a boolean.
645    pub fn get_selector_constraints(&self) -> Vec<E<Fp>> {
646        let one = <Self as InterpreterEnv>::Variable::one();
647        let mut enforce_bool: Vec<E<Fp>> = (0..N_MIPS_SEL_COLS)
648            .map(|i| {
649                let var = self.variable(MIPSColumn::Selector(i));
650                (var.clone() - one.clone()) * var.clone()
651            })
652            .collect();
653        let enforce_one_activation = (0..N_MIPS_SEL_COLS).fold(E::<Fp>::one(), |res, i| {
654            let var = self.variable(MIPSColumn::Selector(i));
655            res - var.clone()
656        });
657
658        enforce_bool.push(enforce_one_activation);
659        enforce_bool
660    }
661
662    pub fn get_selector(&self) -> E<Fp> {
663        self.selector
664            .clone()
665            .unwrap_or_else(|| panic!("Selector is not set"))
666    }
667
668    /// Return the constraints for the current instruction, without the selector
669    pub fn get_constraints(&self) -> Vec<E<Fp>> {
670        self.constraints.clone()
671    }
672
673    pub fn get_lookups(&self) -> Vec<Lookup<E<Fp>>> {
674        self.lookups.clone()
675    }
676}
677
678pub fn get_all_constraints<Fp: Field>() -> Vec<E<Fp>> {
679    let mut mips_con_env = Env::<Fp>::default();
680    let mut constraints = Instruction::iter()
681        .flat_map(|instr_typ| instr_typ.into_iter())
682        .fold(vec![], |mut acc, instr| {
683            interpret_instruction(&mut mips_con_env, instr);
684            let selector = mips_con_env.get_selector();
685            let constraints_with_selector: Vec<E<Fp>> = mips_con_env
686                .get_constraints()
687                .into_iter()
688                .map(|c| selector.clone() * c)
689                .collect();
690            acc.extend(constraints_with_selector);
691            mips_con_env.reset();
692            acc
693        });
694    constraints.extend(mips_con_env.get_selector_constraints());
695    constraints
696}
o1vm/interpreters/mips/constraints.rs

o1vm/interpreters/mips/
constraints.rs
