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