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 /// Decompose a Var into base-|F| limbs. Should only be used when target is a circuit.
198 CircuitVarToFieldOrderLimbsF(Var<C::N>, Vec<Felt<C::F>>),
199
200 // Hashing.
201 /// Permutes an array of baby bear elements using Poseidon2 (output = p2_permute(array)).
202 Poseidon2PermuteBabyBear(Array<C, Felt<C::F>>, Array<C, Felt<C::F>>),
203 /// Compresses two baby bear element arrays using Poseidon2 (output = p2_compress(array1,
204 /// array2)).
205 Poseidon2CompressBabyBear(
206 Array<C, Felt<C::F>>,
207 Array<C, Felt<C::F>>,
208 Array<C, Felt<C::F>>,
209 ),
210 /// Permutes an array of Bn254 elements using Poseidon2 (output = p2_permute(array)). Should
211 /// only be used when target is a circuit.
212 CircuitPoseidon2Permute([Var<C::N>; 3]),
213
214 // Miscellaneous instructions.
215 /// Prints a variable.
216 PrintV(Var<C::N>),
217 /// Prints a field element.
218 PrintF(Felt<C::F>),
219 /// Prints an extension field element.
220 PrintE(Ext<C::F, C::EF>),
221 /// Throws an error.
222 Error(),
223
224 /// Prepare next input vector (preceded by its length) for hinting.
225 HintInputVec(),
226 /// Prepare next felt for hinting
227 HintFelt(),
228 /// Prepare bit decomposition for hinting.
229 HintBitsF(Felt<C::F>, u32),
230
231 StoreHintWord(Ptr<C::N>, MemIndex<C::N>),
232 /// Move data from input stream into hint space
233 HintLoad(),
234
235 /// Witness a variable. Should only be used when target is a circuit.
236 WitnessVar(Var<C::N>, u32),
237 /// Witness a field element. Should only be used when target is a circuit.
238 WitnessFelt(Felt<C::F>, u32),
239 /// Witness an extension field element. Should only be used when target is a circuit.
240 WitnessExt(Ext<C::F, C::EF>, u32),
241 /// Label a field element as the ith public input.
242 Publish(Felt<C::F>, Var<C::N>),
243 /// Operation to halt the program. Should be the last instruction in the program.
244 Halt,
245
246 // Public inputs for circuits.
247 /// Publish a field element as the ith public value. Should only be used when target is a
248 /// circuit.
249 CircuitPublish(Var<C::N>, usize),
250
251 // FRI specific instructions.
252 /// Select's a variable based on a condition. (select(cond, true_val, false_val) => output).
253 /// Should only be used when target is a circuit.
254 CircuitSelectV(Var<C::N>, Var<C::N>, Var<C::N>, Var<C::N>),
255 /// Select's a field element based on a condition. (select(cond, true_val, false_val) =>
256 /// output). Should only be used when target is a circuit.
257 CircuitSelectF(Var<C::N>, Felt<C::F>, Felt<C::F>, Felt<C::F>),
258 /// Select's an extension field element based on a condition. (select(cond, true_val,
259 /// false_val) => output). Should only be used when target is a circuit.
260 CircuitSelectE(
261 Var<C::N>,
262 Ext<C::F, C::EF>,
263 Ext<C::F, C::EF>,
264 Ext<C::F, C::EF>,
265 ),
266 /// Converts an ext to a slice of felts. Should only be used when target is a circuit.
267 CircuitExt2Felt([Felt<C::F>; 4], Ext<C::F, C::EF>),
268 /// Converts a slice of felts to an ext. Should only be used when target is a circuit.
269 CircuitFelts2Ext([Felt<C::F>; 4], Ext<C::F, C::EF>),
270 /// Halo2 only. Reduce a Felt so later computation becomes cheaper.
271 CircuitFeltReduce(Felt<C::F>),
272 /// Halo2 only. Reduce an Ext so later computation becomes cheaper.
273 CircuitExtReduce(Ext<C::F, C::EF>),
274 /// Halo2 only. Asserts that `a, b` both have <= `C::F::bits()` and then asserts `a < b`.
275 /// Assumes that `C::F::bits() < C::N::bits()`.
276 CircuitLessThan(Var<C::N>, Var<C::N>),
277 /// FriReducedOpening(alpha, hint_id, is_init, at_x_array, at_z_array, result)
278 FriReducedOpening(
279 Ext<C::F, C::EF>,
280 Var<C::N>,
281 Var<C::N>,
282 Array<C, Felt<C::F>>,
283 Array<C, Ext<C::F, C::EF>>,
284 Ext<C::F, C::EF>,
285 ),
286 /// VerifyBatch(dim, opened, proof_id, index, commit)
287 /// opened values are Felts
288 VerifyBatchFelt(
289 Array<C, Usize<C::F>>,
290 Array<C, Array<C, Felt<C::F>>>,
291 Var<C::N>,
292 Array<C, Var<C::N>>,
293 Array<C, Felt<C::F>>,
294 ),
295 /// VerifyBatch(dim, opened, proof_id, index, commit)
296 /// opened values are Exts
297 VerifyBatchExt(
298 Array<C, Usize<C::F>>,
299 Array<C, Array<C, Ext<C::F, C::EF>>>,
300 Var<C::N>,
301 Array<C, Var<C::N>>,
302 Array<C, Felt<C::F>>,
303 ),
304 /// RangeCheckV(v, bit)
305 /// Assert that v < 2^bit.
306 RangeCheckV(Var<C::N>, usize),
307
308 /// Start the cycle tracker used by a block of code annotated by the string input. Calling this
309 /// with the same string will end the open cycle tracker instance and start a new one with
310 /// an increasing numeric postfix.
311 CycleTrackerStart(String),
312 /// End the cycle tracker used by a block of code annotated by the string input.
313 CycleTrackerEnd(String),
314}
315
316impl<C: Config> Default for DslIr<C> {
317 fn default() -> Self {
318 Self::Halt
319 }
320}