sp1_recursion_compiler/ir/
instructions.rs

1use std::{
2    borrow::Cow,
3    ops::{Deref, Range},
4};
5
6use backtrace::Backtrace;
7use sp1_hypercube::septic_curve::SepticCurve;
8use sp1_primitives::{SP1ExtensionField, SP1Field};
9use sp1_recursion_executor::RecursionPublicValues;
10
11use super::{Config, Ext, Felt, Var};
12
13/// An intermeddiate instruction set for implementing programs.
14///
15/// Programs written in the DSL can compile both to the recursive zkVM and the R1CS or Plonk-ish
16/// circuits.
17#[derive(Debug, Clone)]
18pub enum DslIr<C: Config> {
19    // Immediates.
20    /// Assigns an immediate to a variable (var = imm).
21    ImmV(Var<C::N>, C::N),
22    /// Assigns a field immediate to a field element (felt = field imm).
23    ImmF(Felt<SP1Field>, SP1Field),
24    /// Assigns an ext field immediate to an extension field element (ext = ext field imm).
25    ImmE(Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
26
27    // Additions.
28    /// Add two variables (var = var + var).
29    AddV(Var<C::N>, Var<C::N>, Var<C::N>),
30    /// Add a variable and an immediate (var = var + imm).
31    AddVI(Var<C::N>, Var<C::N>, C::N),
32    /// Add two field elements (felt = felt + felt).
33    AddF(Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
34    /// Add a field element and a field immediate (felt = felt + field imm).
35    AddFI(Felt<SP1Field>, Felt<SP1Field>, SP1Field),
36    /// Add two extension field elements (ext = ext + ext).
37    AddE(
38        Ext<SP1Field, SP1ExtensionField>,
39        Ext<SP1Field, SP1ExtensionField>,
40        Ext<SP1Field, SP1ExtensionField>,
41    ),
42    /// Add an extension field element and an ext field immediate (ext = ext + ext field imm).
43    AddEI(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
44    /// Add an extension field element and a field element (ext = ext + felt).
45    AddEF(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>),
46    /// Add a field element and an ext field immediate (ext = felt + ext field imm).
47    AddEFFI(Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>, SP1ExtensionField),
48
49    // Subtractions.
50    /// Subtracts two variables (var = var - var).
51    SubV(Var<C::N>, Var<C::N>, Var<C::N>),
52    /// Subtracts a variable and an immediate (var = var - imm).
53    SubVI(Var<C::N>, Var<C::N>, C::N),
54    /// Subtracts an immediate and a variable (var = imm - var).
55    SubVIN(Var<C::N>, C::N, Var<C::N>),
56    /// Subtracts two field elements (felt = felt - felt).
57    SubF(Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
58    /// Subtracts a field element and a field immediate (felt = felt - field imm).
59    SubFI(Felt<SP1Field>, Felt<SP1Field>, SP1Field),
60    /// Subtracts a field immediate and a field element (felt = field imm - felt).
61    SubFIN(Felt<SP1Field>, SP1Field, Felt<SP1Field>),
62    /// Subtracts two extension field elements (ext = ext - ext).
63    SubE(
64        Ext<SP1Field, SP1ExtensionField>,
65        Ext<SP1Field, SP1ExtensionField>,
66        Ext<SP1Field, SP1ExtensionField>,
67    ),
68    /// Subtrancts an extension field element and an extension field immediate (ext = ext - ext
69    /// field imm).
70    SubEI(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
71    /// Subtracts an extension field immediate and an extension field element (ext = ext field imm
72    /// - ext).
73    SubEIN(Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField, Ext<SP1Field, SP1ExtensionField>),
74    /// Subtracts an extension field element and a field element (ext = ext - felt).
75    SubEF(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>),
76
77    // Multiplications.
78    /// Multiplies two variables (var = var * var).
79    MulV(Var<C::N>, Var<C::N>, Var<C::N>),
80    /// Multiplies a variable and an immediate (var = var * imm).
81    MulVI(Var<C::N>, Var<C::N>, C::N),
82    /// Multiplies two field elements (felt = felt * felt).
83    MulF(Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
84    /// Multiplies a field element and a field immediate (felt = felt * field imm).
85    MulFI(Felt<SP1Field>, Felt<SP1Field>, SP1Field),
86    /// Multiplies two extension field elements (ext = ext * ext).
87    MulE(
88        Ext<SP1Field, SP1ExtensionField>,
89        Ext<SP1Field, SP1ExtensionField>,
90        Ext<SP1Field, SP1ExtensionField>,
91    ),
92    /// Multiplies an extension field element and an extension field immediate (ext = ext * ext
93    /// field imm).
94    MulEI(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
95    /// Multiplies an extension field element and a field element (ext = ext * felt).
96    MulEF(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>),
97
98    // Divisions.
99    /// Divides two variables (var = var / var).
100    DivF(Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
101    /// Divides a field element and a field immediate (felt = felt / field imm).
102    DivFI(Felt<SP1Field>, Felt<SP1Field>, SP1Field),
103    /// Divides a field immediate and a field element (felt = field imm / felt).
104    DivFIN(Felt<SP1Field>, SP1Field, Felt<SP1Field>),
105    /// Divides two extension field elements (ext = ext / ext).
106    DivE(
107        Ext<SP1Field, SP1ExtensionField>,
108        Ext<SP1Field, SP1ExtensionField>,
109        Ext<SP1Field, SP1ExtensionField>,
110    ),
111    /// Divides an extension field element and an extension field immediate (ext = ext / ext field
112    /// imm).
113    DivEI(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
114    /// Divides and extension field immediate and an extension field element (ext = ext field imm /
115    /// ext).
116    DivEIN(Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField, Ext<SP1Field, SP1ExtensionField>),
117    /// Divides an extension field element and a field element (ext = ext / felt).
118    DivEF(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>, Felt<SP1Field>),
119
120    // Negations.
121    /// Negates a variable (var = -var).
122    NegV(Var<C::N>, Var<C::N>),
123    /// Negates a field element (felt = -felt).
124    NegF(Felt<SP1Field>, Felt<SP1Field>),
125    /// Negates an extension field element (ext = -ext).
126    NegE(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
127    /// Inverts a variable (var = 1 / var).
128    InvV(Var<C::N>, Var<C::N>),
129    /// Inverts a field element (felt = 1 / felt).
130    InvF(Felt<SP1Field>, Felt<SP1Field>),
131    /// Inverts an extension field element (ext = 1 / ext).
132    InvE(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
133
134    /// Selects order of felts based on a bit (should_swap, first result, second result, first
135    /// input, second input)
136    Select(Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
137
138    // Assertions.
139    /// Assert that two variables are equal (var == var).
140    AssertEqV(Var<C::N>, Var<C::N>),
141    /// Assert that two variables are not equal (var != var).
142    AssertNeV(Var<C::N>, Var<C::N>),
143    /// Assert that two field elements are equal (felt == felt).
144    AssertEqF(Felt<SP1Field>, Felt<SP1Field>),
145    /// Assert that two field elements are not equal (felt != felt).
146    AssertNeF(Felt<SP1Field>, Felt<SP1Field>),
147    /// Assert that two extension field elements are equal (ext == ext).
148    AssertEqE(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
149    /// Assert that two extension field elements are not equal (ext != ext).
150    AssertNeE(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
151    /// Assert that a variable is equal to an immediate (var == imm).
152    AssertEqVI(Var<C::N>, C::N),
153    /// Assert that a variable is not equal to an immediate (var != imm).
154    AssertNeVI(Var<C::N>, C::N),
155    /// Assert that a field element is equal to a field immediate (felt == field imm).
156    AssertEqFI(Felt<SP1Field>, SP1Field),
157    /// Assert that a field element is not equal to a field immediate (felt != field imm).
158    AssertNeFI(Felt<SP1Field>, SP1Field),
159    /// Assert that an extension field element is equal to an extension field immediate (ext == ext
160    /// field imm).
161    AssertEqEI(Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
162    /// Assert that an extension field element is not equal to an extension field immediate (ext !=
163    /// ext field imm).
164    AssertNeEI(Ext<SP1Field, SP1ExtensionField>, SP1ExtensionField),
165
166    /// Force reduction of field elements in circuit.
167    ReduceE(Ext<SP1Field, SP1ExtensionField>),
168
169    // Bits.
170    /// Decompose a variable into size bits (bits = num2bits(var, size)). Should only be used when
171    /// target is a gnark circuit.
172    CircuitNum2BitsV(Var<C::N>, usize, Vec<Var<C::N>>),
173    /// Decompose a field element into bits (bits = num2bits(felt)). Should only be used when
174    /// target is a gnark circuit.
175    CircuitNum2BitsF(Felt<SP1Field>, Vec<Var<C::N>>),
176    /// Convert a Felt to a Var in a circuit. Avoids decomposing to bits and then reconstructing.
177    CircuitFelt2Var(Felt<SP1Field>, Var<C::N>),
178
179    // Hashing.
180    /// Performs the external linear layer of Poseidon2.
181    Poseidon2ExternalLinearLayer(
182        Box<([Ext<SP1Field, SP1ExtensionField>; 4], [Ext<SP1Field, SP1ExtensionField>; 4])>,
183    ),
184    /// Performs the internal linear layer of Poseidon2.
185    Poseidon2InternalLinearLayer(
186        Box<([Ext<SP1Field, SP1ExtensionField>; 4], [Ext<SP1Field, SP1ExtensionField>; 4])>,
187    ),
188    /// Performs the external SBOX mapping for Poseidon2 in a batch.
189    Poseidon2ExternalSBOX(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
190    /// Performs the internal SBOX mapping for Poseidon2 in a batch.
191    Poseidon2InternalSBOX(Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
192
193    /// Permutes an array of Bn254 elements using Poseidon2 (output = p2_permute(array)). Should
194    /// only be used when target is a gnark circuit.
195    CircuitPoseidon2Permute([Var<C::N>; 3]),
196    /// Permutates an array of SP1Field elements in the circuit.
197    CircuitPoseidon2PermuteKoalaBear(Box<[Felt<SP1Field>; 16]>),
198    /// Permutates an array of SP1Field elements in the circuit using the skinny precompile.
199    CircuitV2Poseidon2PermuteKoalaBear(Box<([Felt<SP1Field>; 16], [Felt<SP1Field>; 16])>),
200    /// Commits the public values.
201    CircuitV2CommitPublicValues(Box<RecursionPublicValues<Felt<SP1Field>>>),
202
203    /// Decompose hint operation of a field element into an array. (output = num2bits(felt)).
204    CircuitV2HintBitsF(Vec<Felt<SP1Field>>, Felt<SP1Field>),
205    /// Prints a variable.
206    PrintV(Var<C::N>),
207    /// Prints a field element.
208    PrintF(Felt<SP1Field>),
209    /// Prints an extension field element.
210    PrintE(Ext<SP1Field, SP1ExtensionField>),
211    /// Throws an error.
212    Error(),
213
214    /// Hint an array of field elements.
215    CircuitV2HintFelts(Felt<SP1Field>, usize),
216    /// Hint an array of extension field elements.
217    CircuitV2HintExts(Ext<SP1Field, SP1ExtensionField>, usize),
218    /// Witness a variable. Should only be used when target is a gnark circuit.
219    WitnessVar(Var<C::N>, u32),
220    /// Witness a field element. Should only be used when target is a gnark circuit.
221    WitnessFelt(Felt<SP1Field>, u32),
222    /// Witness an extension field element. Should only be used when target is a gnark circuit.
223    WitnessExt(Ext<SP1Field, SP1ExtensionField>, u32),
224    /// Label a field element as the ith public input.
225    Commit(Felt<SP1Field>, Var<C::N>),
226
227    // Public inputs for circuits.
228    /// Asserts that the inputted var is equal the circuit's vkey hash public input. Should only be
229    /// used when target is a gnark circuit.
230    CircuitCommitVkeyHash(Var<C::N>),
231    /// Asserts that the inputted var is equal the circuit's committed values digest public input.
232    /// Should only be used when target is a gnark circuit.
233    CircuitCommitCommittedValuesDigest(Var<C::N>),
234    /// Asserts that the inputted var is equal the circuit's exit code public input. Should only be
235    /// used when target is a gnark circuit.
236    CircuitCommitExitCode(Var<C::N>),
237    /// Asserts that the inputted var is equal the circuit's vk root public input. Should only be
238    /// used when target is a gnark circuit.
239    CircuitCommitVkRoot(Var<C::N>),
240    /// Asserts that the inputted var is equal the circuit's proof nonce public input. Should only
241    /// be used when target is a gnark circuit.
242    CircuitCommitProofNonce(Var<C::N>),
243    /// Adds two elliptic curve points. (sum, point_1, point_2).
244    CircuitV2HintAddCurve(
245        Box<(
246            SepticCurve<Felt<SP1Field>>,
247            SepticCurve<Felt<SP1Field>>,
248            SepticCurve<Felt<SP1Field>>,
249        )>,
250    ),
251
252    /// Executes full lagrange eval as well as computes field element that corresponds to input bit
253    /// representation.
254    CircuitV2PrefixSumChecks(
255        Box<(
256            Felt<SP1Field>,
257            Ext<SP1Field, SP1ExtensionField>,
258            Vec<Ext<SP1Field, SP1ExtensionField>>,
259            Vec<Felt<SP1Field>>,
260            Vec<Felt<SP1Field>>,
261            Vec<Ext<SP1Field, SP1ExtensionField>>,
262        )>,
263    ),
264    /// Select's a variable based on a condition. (select(cond, true_val, false_val) => output).
265    /// Should only be used when target is a gnark circuit.
266    CircuitSelectV(Var<C::N>, Var<C::N>, Var<C::N>, Var<C::N>),
267    /// Select's a field element based on a condition. (select(cond, true_val, false_val) =>
268    /// output). Should only be used when target is a gnark circuit.
269    CircuitSelectF(Var<C::N>, Felt<SP1Field>, Felt<SP1Field>, Felt<SP1Field>),
270    /// Select's an extension field element based on a condition. (select(cond, true_val,
271    /// false_val) => output). Should only be used when target is a gnark circuit.
272    CircuitSelectE(
273        Var<C::N>,
274        Ext<SP1Field, SP1ExtensionField>,
275        Ext<SP1Field, SP1ExtensionField>,
276        Ext<SP1Field, SP1ExtensionField>,
277    ),
278    /// Converts an ext to a slice of felts. Should only be used when target is a gnark circuit.
279    CircuitExt2Felt([Felt<SP1Field>; 4], Ext<SP1Field, SP1ExtensionField>),
280    /// Converts a slice of felts to an ext. Should only be used when target is a gnark circuit.
281    CircuitFelts2Ext([Felt<SP1Field>; 4], Ext<SP1Field, SP1ExtensionField>),
282    /// Evaluates a single `eq` computation, while verifying that the first element is a bit.
283    /// Should only be used when target is a gnark circuit.
284    EqEval(Felt<SP1Field>, Ext<SP1Field, SP1ExtensionField>, Ext<SP1Field, SP1ExtensionField>),
285    /// Converts a slice of felts to an ext, using a chip. Should be used for wrap.
286    CircuitChipExt2Felt([Felt<SP1Field>; 4], Ext<SP1Field, SP1ExtensionField>),
287    /// Converts an ext to a slice of felts, using a chip. Should be used for wrap.
288    CircuitChipFelt2Ext(Ext<SP1Field, SP1ExtensionField>, [Felt<SP1Field>; 4]),
289
290    // Debugging instructions.
291    /// Tracks the number of cycles used by a block of code annotated by the string input.
292    CycleTrackerV2Enter(Cow<'static, str>),
293    /// Tracks the number of cycles used by a block of code annotated by the string input.
294    CycleTrackerV2Exit,
295
296    // Structuring IR constructors.
297    /// Blocks that may be executed in parallel.
298    Parallel(Vec<DslIrBlock<C>>),
299
300    /// Pass a backtrace for debugging.
301    DebugBacktrace(Backtrace),
302}
303
304/// A block of instructions.
305#[derive(Clone, Default, Debug)]
306pub struct DslIrBlock<C: Config> {
307    pub ops: Vec<DslIr<C>>,
308    pub addrs_written: Range<u32>,
309}
310
311#[derive(Clone, Debug)]
312pub struct DslIrProgram<C: Config>(DslIrBlock<C>);
313
314impl<C: Config> DslIrProgram<C> {
315    /// # Safety
316    /// The given block must represent a well formed program. This is defined as the following:
317    /// - reads are performed after writes, according to a "happens-before" relation; and
318    /// - an address is written to at most once.
319    ///
320    /// The "happens-before" relation is defined as follows:
321    /// - It is a strict partial order, meaning it is transitive, irreflexive, and asymmetric.
322    /// - Contiguous sequences of instructions that are not [`DslIr::Parallel`] in a [`DslIrBlock`]
323    ///   are linearly ordered. Call these sequences "sequential blocks."
324    /// - For each `DslIrBlock` in the `DslIr::Parallel` variant:
325    ///   - The block's first instruction comes after the last instruction in the parent's previous
326    ///     sequential block. if it exists.
327    ///   - The block's last instruction comes before the first instruction in the parent's next
328    ///     sequential block, if it exists.
329    ///   - If the sequential blocks mentioned in eiither of the previous two rules do not exist,
330    ///     then the situation is that of two consecutive [`DslIr::Parallel`] instructions `x` and
331    ///     `y`. Then each last instruction of `x` comes before each first instruction of `y`.
332    pub unsafe fn new_unchecked(block: DslIrBlock<C>) -> Self {
333        Self(block)
334    }
335
336    pub fn into_inner(self) -> DslIrBlock<C> {
337        self.0
338    }
339}
340
341impl<C: Config> Default for DslIrProgram<C> {
342    fn default() -> Self {
343        // SAFETY: An empty block is always well formed.
344        unsafe { Self::new_unchecked(DslIrBlock::default()) }
345    }
346}
347
348impl<C: Config> Deref for DslIrProgram<C> {
349    type Target = DslIrBlock<C>;
350
351    fn deref(&self) -> &Self::Target {
352        &self.0
353    }
354}
sp1_recursion_compiler/ir/instructions.rs

sp1_recursion_compiler/ir/
instructions.rs
