openvm_native_compiler/constraints/
mod.rs

Help
1use core::fmt::Debug;
2use std::marker::PhantomData;
3
4use openvm_stark_backend::p3_field::{Field, FieldExtensionAlgebra, PrimeField};
5use serde::{Deserialize, Serialize};
6
7use self::opcodes::ConstraintOpcode;
8use crate::{
9    ir::{Config, DslIr},
10    prelude::TracedVec,
11};
12
13#[cfg(feature = "halo2-compiler")]
14pub mod halo2;
15
16pub mod opcodes;
17
18/// A constraint is an operation and a list of nested arguments.
19#[derive(Debug, Clone, Serialize, Deserialize)]
20pub struct Constraint {
21    pub opcode: ConstraintOpcode,
22    pub args: Vec<Vec<String>>,
23}
24
25/// The backend for the constraint compiler.
26#[derive(Debug, Clone, Default)]
27pub struct ConstraintCompiler<C: Config> {
28    pub allocator: usize,
29    pub phantom: PhantomData<C>,
30}
31
32impl<C: Config + Debug> ConstraintCompiler<C> {
33    /// Allocate a new variable name in the constraint system.
34    pub fn alloc_id(&mut self) -> String {
35        let id = self.allocator;
36        self.allocator += 1;
37        format!("backend{}", id)
38    }
39
40    /// Allocates a variable in the constraint system.
41    pub fn alloc_v(&mut self, constraints: &mut Vec<Constraint>, value: C::N) -> String {
42        let tmp_id = self.alloc_id();
43        constraints.push(Constraint {
44            opcode: ConstraintOpcode::ImmV,
45            args: vec![
46                vec![tmp_id.clone()],
47                vec![value.as_canonical_biguint().to_string()],
48            ],
49        });
50        tmp_id
51    }
52
53    /// Allocate a felt in the constraint system.
54    pub fn alloc_f(&mut self, constraints: &mut Vec<Constraint>, value: C::F) -> String {
55        let tmp_id = self.alloc_id();
56        constraints.push(Constraint {
57            opcode: ConstraintOpcode::ImmF,
58            args: vec![
59                vec![tmp_id.clone()],
60                vec![value.as_canonical_biguint().to_string()],
61            ],
62        });
63        tmp_id
64    }
65
66    /// Allocate an extension element in the constraint system.
67    pub fn alloc_e(&mut self, constraints: &mut Vec<Constraint>, value: C::EF) -> String {
68        let tmp_id = self.alloc_id();
69        constraints.push(Constraint {
70            opcode: ConstraintOpcode::ImmE,
71            args: vec![
72                vec![tmp_id.clone()],
73                value
74                    .as_base_slice()
75                    .iter()
76                    .map(|x| x.as_canonical_biguint().to_string())
77                    .collect(),
78            ],
79        });
80        tmp_id
81    }
82
83    /// Emit the constraints from a list of operations in the DSL.
84    pub fn emit(&mut self, operations: TracedVec<DslIr<C>>) -> Vec<Constraint> {
85        let mut constraints: Vec<Constraint> = Vec::new();
86        for (instruction, _) in operations {
87            match instruction {
88                DslIr::ImmV(a, b) => constraints.push(Constraint {
89                    opcode: ConstraintOpcode::ImmV,
90                    args: vec![vec![a.id()], vec![b.as_canonical_biguint().to_string()]],
91                }),
92                DslIr::ImmF(a, b) => constraints.push(Constraint {
93                    opcode: ConstraintOpcode::ImmF,
94                    args: vec![vec![a.id()], vec![b.as_canonical_biguint().to_string()]],
95                }),
96                DslIr::ImmE(a, b) => constraints.push(Constraint {
97                    opcode: ConstraintOpcode::ImmE,
98                    args: vec![
99                        vec![a.id()],
100                        b.as_base_slice()
101                            .iter()
102                            .map(|x| x.as_canonical_biguint().to_string())
103                            .collect(),
104                    ],
105                }),
106                DslIr::AddV(a, b, c) => constraints.push(Constraint {
107                    opcode: ConstraintOpcode::AddV,
108                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
109                }),
110                DslIr::AddVI(a, b, c) => {
111                    let tmp = self.alloc_v(&mut constraints, c);
112                    constraints.push(Constraint {
113                        opcode: ConstraintOpcode::AddV,
114                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
115                    });
116                }
117                DslIr::AddF(a, b, c) => constraints.push(Constraint {
118                    opcode: ConstraintOpcode::AddF,
119                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
120                }),
121                DslIr::AddFI(a, b, c) => {
122                    let tmp = self.alloc_f(&mut constraints, c);
123                    constraints.push(Constraint {
124                        opcode: ConstraintOpcode::AddF,
125                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
126                    });
127                }
128                DslIr::AddE(a, b, c) => constraints.push(Constraint {
129                    opcode: ConstraintOpcode::AddE,
130                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
131                }),
132                DslIr::AddEF(a, b, c) => constraints.push(Constraint {
133                    opcode: ConstraintOpcode::AddEF,
134                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
135                }),
136                DslIr::AddEFI(a, b, c) => {
137                    let tmp = self.alloc_f(&mut constraints, c);
138                    constraints.push(Constraint {
139                        opcode: ConstraintOpcode::AddEF,
140                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
141                    });
142                }
143                DslIr::AddEI(a, b, c) => {
144                    let tmp = self.alloc_e(&mut constraints, c);
145                    constraints.push(Constraint {
146                        opcode: ConstraintOpcode::AddE,
147                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
148                    });
149                }
150                DslIr::AddEFFI(a, b, c) => {
151                    let tmp = self.alloc_e(&mut constraints, c);
152                    constraints.push(Constraint {
153                        opcode: ConstraintOpcode::AddEF,
154                        args: vec![vec![a.id()], vec![tmp], vec![b.id()]],
155                    });
156                }
157                DslIr::SubV(a, b, c) => constraints.push(Constraint {
158                    opcode: ConstraintOpcode::SubV,
159                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
160                }),
161                DslIr::SubF(a, b, c) => constraints.push(Constraint {
162                    opcode: ConstraintOpcode::SubF,
163                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
164                }),
165                DslIr::SubE(a, b, c) => constraints.push(Constraint {
166                    opcode: ConstraintOpcode::SubE,
167                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
168                }),
169                DslIr::SubEF(a, b, c) => constraints.push(Constraint {
170                    opcode: ConstraintOpcode::SubEF,
171                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
172                }),
173                DslIr::SubEI(a, b, c) => {
174                    let tmp = self.alloc_e(&mut constraints, c);
175                    constraints.push(Constraint {
176                        opcode: ConstraintOpcode::SubE,
177                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
178                    });
179                }
180                DslIr::SubEIN(a, b, c) => {
181                    let tmp = self.alloc_e(&mut constraints, b);
182                    constraints.push(Constraint {
183                        opcode: ConstraintOpcode::SubE,
184                        args: vec![vec![a.id()], vec![tmp], vec![c.id()]],
185                    });
186                }
187                DslIr::MulV(a, b, c) => constraints.push(Constraint {
188                    opcode: ConstraintOpcode::MulV,
189                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
190                }),
191                DslIr::MulVI(a, b, c) => {
192                    let tmp = self.alloc_v(&mut constraints, c);
193                    constraints.push(Constraint {
194                        opcode: ConstraintOpcode::MulV,
195                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
196                    });
197                }
198                DslIr::MulF(a, b, c) => constraints.push(Constraint {
199                    opcode: ConstraintOpcode::MulF,
200                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
201                }),
202                DslIr::MulE(a, b, c) => constraints.push(Constraint {
203                    opcode: ConstraintOpcode::MulE,
204                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
205                }),
206                DslIr::MulEI(a, b, c) => {
207                    let tmp = self.alloc_e(&mut constraints, c);
208                    constraints.push(Constraint {
209                        opcode: ConstraintOpcode::MulE,
210                        args: vec![vec![a.id()], vec![b.id()], vec![tmp]],
211                    });
212                }
213                DslIr::MulEF(a, b, c) => constraints.push(Constraint {
214                    opcode: ConstraintOpcode::MulEF,
215                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
216                }),
217                DslIr::DivFIN(a, b, c) => {
218                    let tmp = self.alloc_f(&mut constraints, b.inverse());
219                    constraints.push(Constraint {
220                        opcode: ConstraintOpcode::MulF,
221                        args: vec![vec![a.id()], vec![tmp], vec![c.id()]],
222                    });
223                }
224                DslIr::DivE(a, b, c) => constraints.push(Constraint {
225                    opcode: ConstraintOpcode::DivE,
226                    args: vec![vec![a.id()], vec![b.id()], vec![c.id()]],
227                }),
228                DslIr::DivEIN(a, b, c) => {
229                    let tmp = self.alloc_e(&mut constraints, b);
230                    constraints.push(Constraint {
231                        opcode: ConstraintOpcode::DivE,
232                        args: vec![vec![a.id()], vec![tmp], vec![c.id()]],
233                    });
234                }
235                DslIr::NegE(a, b) => constraints.push(Constraint {
236                    opcode: ConstraintOpcode::NegE,
237                    args: vec![vec![a.id()], vec![b.id()]],
238                }),
239                DslIr::CircuitNum2BitsF(value, output) => constraints.push(Constraint {
240                    opcode: ConstraintOpcode::Num2BitsF,
241                    args: vec![output.iter().map(|x| x.id()).collect(), vec![value.id()]],
242                }),
243                DslIr::CircuitPoseidon2Permute(state) => constraints.push(Constraint {
244                    opcode: ConstraintOpcode::Permute,
245                    args: state.iter().map(|x| vec![x.id()]).collect(),
246                }),
247                DslIr::CircuitSelectV(cond, a, b, out) => {
248                    constraints.push(Constraint {
249                        opcode: ConstraintOpcode::SelectV,
250                        args: vec![vec![out.id()], vec![cond.id()], vec![a.id()], vec![b.id()]],
251                    });
252                }
253                DslIr::CircuitSelectF(cond, a, b, out) => {
254                    constraints.push(Constraint {
255                        opcode: ConstraintOpcode::SelectF,
256                        args: vec![vec![out.id()], vec![cond.id()], vec![a.id()], vec![b.id()]],
257                    });
258                }
259                DslIr::CircuitSelectE(cond, a, b, out) => {
260                    constraints.push(Constraint {
261                        opcode: ConstraintOpcode::SelectE,
262                        args: vec![vec![out.id()], vec![cond.id()], vec![a.id()], vec![b.id()]],
263                    });
264                }
265                DslIr::CircuitExt2Felt(a, b) => {
266                    constraints.push(Constraint {
267                        opcode: ConstraintOpcode::Ext2Felt,
268                        args: vec![
269                            vec![a[0].id()],
270                            vec![a[1].id()],
271                            vec![a[2].id()],
272                            vec![a[3].id()],
273                            vec![b.id()],
274                        ],
275                    });
276                }
277                DslIr::AssertEqV(a, b) => constraints.push(Constraint {
278                    opcode: ConstraintOpcode::AssertEqV,
279                    args: vec![vec![a.id()], vec![b.id()]],
280                }),
281                DslIr::AssertEqVI(a, b) => {
282                    let tmp = self.alloc_v(&mut constraints, b);
283                    constraints.push(Constraint {
284                        opcode: ConstraintOpcode::AssertEqV,
285                        args: vec![vec![a.id()], vec![tmp]],
286                    });
287                }
288                DslIr::AssertEqF(a, b) => constraints.push(Constraint {
289                    opcode: ConstraintOpcode::AssertEqF,
290                    args: vec![vec![a.id()], vec![b.id()]],
291                }),
292                DslIr::AssertEqFI(a, b) => {
293                    let tmp = self.alloc_f(&mut constraints, b);
294                    constraints.push(Constraint {
295                        opcode: ConstraintOpcode::AssertEqF,
296                        args: vec![vec![a.id()], vec![tmp]],
297                    });
298                }
299                DslIr::AssertEqE(a, b) => constraints.push(Constraint {
300                    opcode: ConstraintOpcode::AssertEqE,
301                    args: vec![vec![a.id()], vec![b.id()]],
302                }),
303                DslIr::AssertEqEI(a, b) => {
304                    let tmp = self.alloc_e(&mut constraints, b);
305                    constraints.push(Constraint {
306                        opcode: ConstraintOpcode::AssertEqE,
307                        args: vec![vec![a.id()], vec![tmp]],
308                    });
309                }
310                DslIr::PrintV(a) => constraints.push(Constraint {
311                    opcode: ConstraintOpcode::PrintV,
312                    args: vec![vec![a.id()]],
313                }),
314                DslIr::PrintF(a) => constraints.push(Constraint {
315                    opcode: ConstraintOpcode::PrintF,
316                    args: vec![vec![a.id()]],
317                }),
318                DslIr::PrintE(a) => constraints.push(Constraint {
319                    opcode: ConstraintOpcode::PrintE,
320                    args: vec![vec![a.id()]],
321                }),
322                DslIr::WitnessVar(a, b) => constraints.push(Constraint {
323                    opcode: ConstraintOpcode::WitnessV,
324                    args: vec![vec![a.id()], vec![b.to_string()]],
325                }),
326                DslIr::WitnessFelt(a, b) => constraints.push(Constraint {
327                    opcode: ConstraintOpcode::WitnessF,
328                    args: vec![vec![a.id()], vec![b.to_string()]],
329                }),
330                DslIr::WitnessExt(a, b) => constraints.push(Constraint {
331                    opcode: ConstraintOpcode::WitnessE,
332                    args: vec![vec![a.id()], vec![b.to_string()]],
333                }),
334                DslIr::CircuitFelts2Ext(a, b) => constraints.push(Constraint {
335                    opcode: ConstraintOpcode::CircuitFelts2Ext,
336                    args: vec![
337                        vec![b.id()],
338                        vec![a[0].id()],
339                        vec![a[1].id()],
340                        vec![a[2].id()],
341                        vec![a[3].id()],
342                    ],
343                }),
344                _ => panic!("unsupported {:?}", instruction),
345            };
346        }
347        constraints
348    }
349}
openvm_native_compiler/constraints/mod.rs

openvm_native_compiler/constraints/
mod.rs
