openvm_native_compiler/ir/
instructions.rs

1use serde::{Deserialize, Serialize};
2
3use super::{Array, Config, Ext, Felt, MemIndex, Ptr, RVar, TracedVec, Usize, Var};
4
5/// An intermediate instruction set for implementing programs.
6///
7/// Programs written in the DSL can compile both to the recursive zkVM and the R1CS or Plonk-ish
8/// circuits.
9#[derive(Debug, Clone, strum_macros::Display, Serialize, Deserialize)]
10pub enum DslIr<C: Config> {
11    // Immediates.
12    /// Assigns an immediate to a variable (var = imm).
13    ImmV(Var<C::N>, C::N),
14    /// Assigns a field immediate to a field element (felt = field imm).
15    ImmF(Felt<C::F>, C::F),
16    /// Assigns an ext field immediate to an extension field element (ext = ext field imm).
17    ImmE(Ext<C::F, C::EF>, C::EF),
18
19    // Additions.
20    /// Add two variables (var = var + var).
21    AddV(Var<C::N>, Var<C::N>, Var<C::N>),
22    /// Add a variable and an immediate (var = var + imm).
23    AddVI(Var<C::N>, Var<C::N>, C::N),
24    /// Add two field elements (felt = felt + felt).
25    AddF(Felt<C::F>, Felt<C::F>, Felt<C::F>),
26    /// Add a field element and a field immediate (felt = felt + field imm).
27    AddFI(Felt<C::F>, Felt<C::F>, C::F),
28    /// Add two extension field elements (ext = ext + ext).
29    AddE(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Ext<C::F, C::EF>),
30    /// Add an extension field element and an ext field immediate (ext = ext + ext field imm).
31    AddEI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::EF),
32    /// Add an extension field element and a field element (ext = ext + felt).
33    AddEF(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Felt<C::F>),
34    /// Add an extension field element and a field immediate (ext = ext + field imm).
35    AddEFI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::F),
36    /// Add a field element and an ext field immediate (ext = felt + ext field imm).
37    AddEFFI(Ext<C::F, C::EF>, Felt<C::F>, C::EF),
38
39    // Subtractions.
40    /// Subtracts two variables (var = var - var).
41    SubV(Var<C::N>, Var<C::N>, Var<C::N>),
42    /// Subtracts a variable and an immediate (var = var - imm).
43    SubVI(Var<C::N>, Var<C::N>, C::N),
44    /// Subtracts an immediate and a variable (var = imm - var).
45    SubVIN(Var<C::N>, C::N, Var<C::N>),
46    /// Subtracts two field elements (felt = felt - felt).
47    SubF(Felt<C::F>, Felt<C::F>, Felt<C::F>),
48    /// Subtracts a field element and a field immediate (felt = felt - field imm).
49    SubFI(Felt<C::F>, Felt<C::F>, C::F),
50    /// Subtracts a field immediate and a field element (felt = field imm - felt).
51    SubFIN(Felt<C::F>, C::F, Felt<C::F>),
52    /// Subtracts two extension field elements (ext = ext - ext).
53    SubE(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Ext<C::F, C::EF>),
54    /// Subtracts an extension field element and an extension field immediate (ext = ext - ext
55    /// field imm).
56    SubEI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::EF),
57    /// Subtracts an extension field immediate and an extension field element (ext = ext field imm
58    /// - ext).
59    SubEIN(Ext<C::F, C::EF>, C::EF, Ext<C::F, C::EF>),
60    /// Subtracts an extension field element and a field immediate (ext = ext - field imm).
61    SubEFI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::F),
62    /// Subtracts an extension field element and a field element (ext = ext - felt).
63    SubEF(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Felt<C::F>),
64
65    // Multiplications.
66    /// Multiplies two variables (var = var * var).
67    MulV(Var<C::N>, Var<C::N>, Var<C::N>),
68    /// Multiplies a variable and an immediate (var = var * imm).
69    MulVI(Var<C::N>, Var<C::N>, C::N),
70    /// Multiplies two field elements (felt = felt * felt).
71    MulF(Felt<C::F>, Felt<C::F>, Felt<C::F>),
72    /// Multiplies a field element and a field immediate (felt = felt * field imm).
73    MulFI(Felt<C::F>, Felt<C::F>, C::F),
74    /// Multiplies two extension field elements (ext = ext * ext).
75    MulE(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Ext<C::F, C::EF>),
76    /// Multiplies an extension field element and an extension field immediate (ext = ext * ext
77    /// field imm).
78    MulEI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::EF),
79    /// Multiplies an extension field element and a field immediate (ext = ext * field imm).
80    MulEFI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::F),
81    /// Multiplies an extension field element and a field element (ext = ext * felt).
82    MulEF(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Felt<C::F>),
83
84    // Divisions.
85    /// Divides two variables (var = var / var).
86    DivF(Felt<C::F>, Felt<C::F>, Felt<C::F>),
87    /// Divides a field element and a field immediate (felt = felt / field imm).
88    DivFI(Felt<C::F>, Felt<C::F>, C::F),
89    /// Divides a field immediate and a field element (felt = field imm / felt).
90    DivFIN(Felt<C::F>, C::F, Felt<C::F>),
91    /// Divides two extension field elements (ext = ext / ext).
92    DivE(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Ext<C::F, C::EF>),
93    /// Divides an extension field element and an extension field immediate (ext = ext / ext field
94    /// imm).
95    DivEI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::EF),
96    /// Divides and extension field immediate and an extension field element (ext = ext field imm /
97    /// ext).
98    DivEIN(Ext<C::F, C::EF>, C::EF, Ext<C::F, C::EF>),
99    /// Divides an extension field element and a field immediate (ext = ext / field imm).
100    DivEFI(Ext<C::F, C::EF>, Ext<C::F, C::EF>, C::F),
101    /// Divides an extension field element and a field element (ext = ext / felt).
102    DivEF(Ext<C::F, C::EF>, Ext<C::F, C::EF>, Felt<C::F>),
103
104    // Negations.
105    /// Negates a variable (var = -var).
106    NegV(Var<C::N>, Var<C::N>),
107    /// Negates a field element (felt = -felt).
108    NegF(Felt<C::F>, Felt<C::F>),
109    /// Negates an extension field element (ext = -ext).
110    NegE(Ext<C::F, C::EF>, Ext<C::F, C::EF>),
111
112    /// Cast a Felt to a Var.
113    CastFV(Var<C::N>, Felt<C::F>),
114    /// Cast a Var to a Felt. This is unsafe because of possible overflow. Dynamic mode only.
115    UnsafeCastVF(Felt<C::F>, Var<C::N>),
116
117    // =======
118
119    // Control flow.
120    /// Executes a zipped iterator for loop over pointers with the parameters
121    /// (start step values, end step value of first pointer, step sizes, step variables, body).
122    ZipFor(
123        Vec<RVar<C::N>>,
124        RVar<C::N>,
125        Vec<C::N>,
126        Vec<Var<C::N>>,
127        TracedVec<DslIr<C>>,
128    ),
129
130    /// Executes an equal conditional branch with the parameters (lhs var, rhs var, then body, else
131    /// body).
132    IfEq(
133        Var<C::N>,
134        Var<C::N>,
135        TracedVec<DslIr<C>>,
136        TracedVec<DslIr<C>>,
137    ),
138    /// Executes a not equal conditional branch with the parameters (lhs var, rhs var, then body,
139    /// else body).
140    IfNe(
141        Var<C::N>,
142        Var<C::N>,
143        TracedVec<DslIr<C>>,
144        TracedVec<DslIr<C>>,
145    ),
146    /// Executes an equal conditional branch with the parameters (lhs var, rhs imm, then body, else
147    /// body).
148    IfEqI(Var<C::N>, C::N, TracedVec<DslIr<C>>, TracedVec<DslIr<C>>),
149    /// Executes a not equal conditional branch with the parameters (lhs var, rhs imm, then body,
150    /// else body).
151    IfNeI(Var<C::N>, C::N, TracedVec<DslIr<C>>, TracedVec<DslIr<C>>),
152
153    // Assertions.
154    /// Assert that two variables are equal (var == var).
155    AssertEqV(Var<C::N>, Var<C::N>),
156    /// Assert that two field elements are equal (felt == felt).
157    AssertEqF(Felt<C::F>, Felt<C::F>),
158    /// Assert that two extension field elements are equal (ext == ext).
159    AssertEqE(Ext<C::F, C::EF>, Ext<C::F, C::EF>),
160    /// Assert that a variable is equal to an immediate (var == imm).
161    AssertEqVI(Var<C::N>, C::N),
162    /// Assert that a field element is equal to a field immediate (felt == field imm).
163    AssertEqFI(Felt<C::F>, C::F),
164    /// Assert that an extension field element is equal to an extension field immediate (ext == ext
165    /// field imm).
166    AssertEqEI(Ext<C::F, C::EF>, C::EF),
167
168    /// Assert that a usize is not zero (usize != 0).
169    AssertNonZero(Usize<C::N>),
170
171    // Memory instructions.
172    /// Allocate (ptr, len, size) a memory slice of length len
173    Alloc(Ptr<C::N>, RVar<C::N>, usize),
174    /// Load variable (var, ptr, index)
175    LoadV(Var<C::N>, Ptr<C::N>, MemIndex<C::N>),
176    /// Load field element (var, ptr, index)
177    LoadF(Felt<C::F>, Ptr<C::N>, MemIndex<C::N>),
178    /// Load extension field
179    LoadE(Ext<C::F, C::EF>, Ptr<C::N>, MemIndex<C::N>),
180    /// Load heap pointer into a stack variable. ASM only.
181    LoadHeapPtr(Ptr<C::N>),
182    /// Store variable at address
183    StoreV(Var<C::N>, Ptr<C::N>, MemIndex<C::N>),
184    /// Store field element at address
185    StoreF(Felt<C::F>, Ptr<C::N>, MemIndex<C::N>),
186    /// Store extension field at address
187    StoreE(Ext<C::F, C::EF>, Ptr<C::N>, MemIndex<C::N>),
188    /// Store heap pointer. ASM only.
189    StoreHeapPtr(Ptr<C::N>),
190
191    // Bits.
192    /// Decompose a field element into bits (bits = num2bits(felt)). Should only be used when
193    /// target is a circuit.
194    CircuitNum2BitsF(Felt<C::F>, Vec<Var<C::N>>),
195    /// Decompose a Var into 16-bit limbs.
196    CircuitVarTo64BitsF(Var<C::N>, [Felt<C::F>; 4]),
197
198    // Hashing.
199    /// Permutes an array of baby bear elements using Poseidon2 (output = p2_permute(array)).
200    Poseidon2PermuteBabyBear(Array<C, Felt<C::F>>, Array<C, Felt<C::F>>),
201    /// Compresses two baby bear element arrays using Poseidon2 (output = p2_compress(array1,
202    /// array2)).
203    Poseidon2CompressBabyBear(
204        Array<C, Felt<C::F>>,
205        Array<C, Felt<C::F>>,
206        Array<C, Felt<C::F>>,
207    ),
208    /// Permutes an array of Bn254 elements using Poseidon2 (output = p2_permute(array)). Should
209    /// only be used when target is a circuit.
210    CircuitPoseidon2Permute([Var<C::N>; 3]),
211
212    // Miscellaneous instructions.
213    /// Prints a variable.
214    PrintV(Var<C::N>),
215    /// Prints a field element.
216    PrintF(Felt<C::F>),
217    /// Prints an extension field element.
218    PrintE(Ext<C::F, C::EF>),
219    /// Throws an error.
220    Error(),
221
222    /// Prepare next input vector (preceded by its length) for hinting.
223    HintInputVec(),
224    /// Prepare next felt for hinting
225    HintFelt(),
226    /// Prepare bit decomposition for hinting.
227    HintBitsF(Felt<C::F>, u32),
228
229    StoreHintWord(Ptr<C::N>, MemIndex<C::N>),
230    /// Move data from input stream into hint space
231    HintLoad(),
232
233    /// Witness a variable. Should only be used when target is a circuit.
234    WitnessVar(Var<C::N>, u32),
235    /// Witness a field element. Should only be used when target is a circuit.
236    WitnessFelt(Felt<C::F>, u32),
237    /// Witness an extension field element. Should only be used when target is a circuit.
238    WitnessExt(Ext<C::F, C::EF>, u32),
239    /// Label a field element as the ith public input.
240    Publish(Felt<C::F>, Var<C::N>),
241    /// Operation to halt the program. Should be the last instruction in the program.
242    Halt,
243
244    // Public inputs for circuits.
245    /// Publish a field element as the ith public value. Should only be used when target is a
246    /// circuit.
247    CircuitPublish(Var<C::N>, usize),
248
249    // FRI specific instructions.
250    /// Select's a variable based on a condition. (select(cond, true_val, false_val) => output).
251    /// Should only be used when target is a circuit.
252    CircuitSelectV(Var<C::N>, Var<C::N>, Var<C::N>, Var<C::N>),
253    /// Select's a field element based on a condition. (select(cond, true_val, false_val) =>
254    /// output). Should only be used when target is a circuit.
255    CircuitSelectF(Var<C::N>, Felt<C::F>, Felt<C::F>, Felt<C::F>),
256    /// Select's an extension field element based on a condition. (select(cond, true_val,
257    /// false_val) => output). Should only be used when target is a circuit.
258    CircuitSelectE(
259        Var<C::N>,
260        Ext<C::F, C::EF>,
261        Ext<C::F, C::EF>,
262        Ext<C::F, C::EF>,
263    ),
264    /// Converts an ext to a slice of felts. Should only be used when target is a circuit.
265    CircuitExt2Felt([Felt<C::F>; 4], Ext<C::F, C::EF>),
266    /// Converts a slice of felts to an ext. Should only be used when target is a circuit.
267    CircuitFelts2Ext([Felt<C::F>; 4], Ext<C::F, C::EF>),
268    /// Halo2 only. Reduce a Felt so later computation becomes cheaper.
269    CircuitFeltReduce(Felt<C::F>),
270    /// Halo2 only. Reduce an Ext so later computation becomes cheaper.
271    CircuitExtReduce(Ext<C::F, C::EF>),
272    /// Halo2 only. Asserts that `a, b` both have <= `C::F::bits()` and then asserts `a < b`.
273    /// Assumes that `C::F::bits() < C::N::bits()`.
274    CircuitLessThan(Var<C::N>, Var<C::N>),
275    /// FriReducedOpening(alpha, hint_id, is_init, at_x_array, at_z_array, result)
276    FriReducedOpening(
277        Ext<C::F, C::EF>,
278        Var<C::N>,
279        Var<C::N>,
280        Array<C, Felt<C::F>>,
281        Array<C, Ext<C::F, C::EF>>,
282        Ext<C::F, C::EF>,
283    ),
284    /// VerifyBatch(dim, opened, proof_id, index, commit)
285    /// opened values are Felts
286    VerifyBatchFelt(
287        Array<C, Usize<C::F>>,
288        Array<C, Array<C, Felt<C::F>>>,
289        Var<C::N>,
290        Array<C, Var<C::N>>,
291        Array<C, Felt<C::F>>,
292    ),
293    /// VerifyBatch(dim, opened, proof_id, index, commit)
294    /// opened values are Exts
295    VerifyBatchExt(
296        Array<C, Usize<C::F>>,
297        Array<C, Array<C, Ext<C::F, C::EF>>>,
298        Var<C::N>,
299        Array<C, Var<C::N>>,
300        Array<C, Felt<C::F>>,
301    ),
302    /// RangeCheckV(v, bit)
303    /// Assert that v < 2^bit.
304    RangeCheckV(Var<C::N>, usize),
305
306    /// Start the cycle tracker used by a block of code annotated by the string input. Calling this
307    /// with the same string will end the open cycle tracker instance and start a new one with
308    /// an increasing numeric postfix.
309    CycleTrackerStart(String),
310    /// End the cycle tracker used by a block of code annotated by the string input.
311    CycleTrackerEnd(String),
312}
313
314impl<C: Config> Default for DslIr<C> {
315    fn default() -> Self {
316        Self::Halt
317    }
318}
openvm_native_compiler/ir/instructions.rs

openvm_native_compiler/ir/
instructions.rs
