sp1_recursion_compiler/constraints/
mod.rs

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

sp1_recursion_compiler/constraints/
mod.rs
