sp1_recursion_compiler/constraints/
mod.rs

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

sp1_recursion_compiler/constraints/
mod.rs
