LLZK 0.1.0
Veridise's ZK Language IR
Loading...
Searching...
No Matches
Ops.td
Go to the documentation of this file.
1//===-- Ops.td ---------------------------------------------*- tablegen -*-===//
2//
3// Part of the LLZK Project, under the Apache License v2.0.
4// See LICENSE.txt for license information.
5// Copyright 2025 Veridise Inc.
6// SPDX-License-Identifier: Apache-2.0
7//
8//===----------------------------------------------------------------------===//
9
10#ifndef LLZK_ARRAY_OPS
11#define LLZK_ARRAY_OPS
12
13include "llzk/Dialect/Array/IR/Dialect.td"
14include "llzk/Dialect/Array/IR/OpInterfaces.td"
15include "llzk/Dialect/Array/IR/Types.td"
16include "llzk/Dialect/Shared/OpTraits.td"
17
18include "mlir/IR/OpAsmInterface.td"
19include "mlir/IR/OpBase.td"
20include "mlir/IR/SymbolInterfaces.td"
21
22class ArrayDialectOp<string mnemonic, list<Trait> traits = []>
23 : Op<ArrayDialect, mnemonic, traits>;
24
25class ArrayAccessOpBase<string mnemonic, list<Trait> traits = []>
26 : ArrayDialectOp<
27 mnemonic,
28 traits#[DeclareOpInterfaceMethods<SymbolUserOpInterface>,
29 DeclareOpInterfaceMethods<ArrayAccessOpInterface>]> {
30 let extraClassDeclaration = [{
31 /// Gets the type of the referenced base array.
32 inline ::llzk::array::ArrayType getArrRefType() {
33 return ::llvm::cast<ArrayAccessOpInterface>(getOperation()).getArrRefType();
34 }
35 }];
36}
37
38// isRead: read(1) vs write(0) ops
39class ScalarArrayAccessOp<string mnemonic, bit isRead, list<Trait> traits = []>
40 : ArrayAccessOpBase<
41 mnemonic,
42 traits#[DeclareOpInterfaceMethods<DestructurableAccessorOpInterface>,
43 DeclareOpInterfaceMethods<PromotableMemOpInterface>]> {
44 let extraClassDefinition = [{
45 /// Required by DestructurableAllocationOpInterface / SROA pass
46 bool $cppClass::canRewire(const ::mlir::DestructurableMemorySlot &slot,
47 ::llvm::SmallPtrSetImpl<::mlir::Attribute> &usedIndices,
48 ::mlir::SmallVectorImpl<::mlir::MemorySlot> &mustBeSafelyUsed,
49 const ::mlir::DataLayout &dataLayout) {
50 return ::llvm::cast<ArrayAccessOpInterface>(getOperation())
51 .canRewire(slot, usedIndices, mustBeSafelyUsed, dataLayout);
52 }
53
54 /// Required by DestructurableAllocationOpInterface / SROA pass
55 ::mlir::DeletionKind $cppClass::rewire(const ::mlir::DestructurableMemorySlot &slot,
56 ::llvm::DenseMap<::mlir::Attribute, ::mlir::MemorySlot> &subslots,
57 ::mlir::OpBuilder &builder, const ::mlir::DataLayout &dataLayout) {
58 return ::llvm::cast<ArrayAccessOpInterface>(getOperation())
59 .rewire(slot, subslots, builder, dataLayout);
60 }
61
62 /// Required by PromotableMemOpInterface / mem2reg pass
63 bool $cppClass::loadsFrom(const ::mlir::MemorySlot &slot) {
64 return }]#!if(isRead, "getArrRef() == slot.ptr", "false")#[{;
65 }
66
67 /// Required by PromotableMemOpInterface / mem2reg pass
68 bool $cppClass::storesTo(const ::mlir::MemorySlot &slot) {
69 return }]#!if(isRead, "false", "getArrRef() == slot.ptr")#[{;
70 }
71
72 /// Required by PromotableAllocationOpInterface / mem2reg pass
73 ::mlir::Value $cppClass::getStored(const ::mlir::MemorySlot &, ::mlir::OpBuilder &,
74 ::mlir::Value, const ::mlir::DataLayout &) {
75 }]#!if(isRead,
76 "llvm_unreachable(\"getStored() should not be called on "
77 "$cppClass\")",
78 "return getRvalue()")#[{;
79 }
80
81 /// Return `true` if the op is a read, `false` if it's a write.
82 bool $cppClass::isRead() {
83 return }]#!if(isRead, "true", "false")#[{;
84 }
85 }];
86}
87
88// isRead: read(1) vs write(0) ops
89class RangedArrayAccessOp<string mnemonic, bit isRead, list<Trait> traits = []>
90 : ArrayAccessOpBase<mnemonic, traits> {
91 let extraClassDefinition = [{
92 /// Return `true` if the op is a read, `false` if it's a write.
93 bool $cppClass::isRead() {
94 return }]#!if(isRead, "true", "false")#[{;
95 }
96 }];
97}
98
99//===------------------------------------------------------------------===//
100// Array operations
101//===------------------------------------------------------------------===//
102
103def LLZK_CreateArrayOp
104 : ArrayDialectOp<
105 "new",
106 [Pure, AttrSizedOperandSegments, VerifySizesForMultiAffineOps<1>,
107 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
108 DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>,
109 DeclareOpInterfaceMethods<PromotableAllocationOpInterface>,
110 DeclareOpInterfaceMethods<DestructurableAllocationOpInterface>,
111 VariadicTypesMatchWith<
112 "operand types match result type", "result", "elements",
113 "resultTypeToElementsTypes($_self)", "std::equal_to<>()">]> {
114 let summary = "create a new array";
115 let description = [{
116 This operation creates a new array with the given elements.
117 The arguments are passed as a flat array but get arranged in
118 row-major order according the shape declared in the type.
119
120 Examples:
121 ```llzk
122 %0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
123
124 // Create an array of the specified shape, initialized with the given
125 // values assigned in row-major order: [[%a, %b], [%c, %d]]
126 %1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
127
128 // Create an uninitialized array: [[?, ?], [?, ?], [?, ?]]
129 %2 = array.new : !array.type<3,2 x !felt.type>
130 ```
131
132 The values used to construct the array must have type that exactly matches
133 the element type of the specified array type. This is true even if a `tvar`
134 type is used. In other words, cannot mix `tvar<@X>` with `tvar<@Y>` or any
135 concrete type. In such a scenario, first create an uninitialized array, as
136 shown in the examples above, and then use `array.write` to write each element
137 of the array.
138
139 Implementation note: This restriction exists due to a combination of:
140 (1) we have chosen to infer the type of `$elements` from the `$result`
141 ArrayType, via parseInferredArrayType(), rather than requiring the type of
142 every element be listed in the assembly format and,
143 (2) within the parser for an Op, there is no way to get the Value instances
144 for the operands aside from `OpAsmParser::resolveOperands()` which requires
145 the type of every operand to be known and ends up comparing the expected
146 to actual type via `operator==`. Thus, there is no way for this to be
147 successful apart from all elements having the exact type inferred in (1).
148
149 Also note that `std::equal_to` is used in the `VariadicTypesMatchWith`
150 trait on this Op so that the verifier function mirrors the aforementioned
151 restriction in the parser.
152
153 In some cases, the length of an uninitialized array depends on the value
154 of the loop induction variable (i.e., each iteration creates an array with
155 a different size/shape). In that case, an AffineMapAttr can be used to
156 specify the dimension size in the ArrayType and the optional instantiation
157 parameter list of this operation must be used to instatiate all AffineMap
158 used in the array dimensions.
159
160 Examples:
161 ```llzk
162 // Create an uninitialized array with dimension size defined by AffineMap
163 #IdxToLen = affine_map<(i) -> (5*i+1)>
164 %3 = array.new {(%i)} : !array.type<#IdxToLen x index>
165
166 // Create an uninitialized array with multiple dimensions defined by
167 // AffineMap. The list of instantiation parameters are assigned to
168 // the AffineMap dimensions left-to-right.
169 #M1 = affine_map<(i)[c] -> (c+i)>
170 #M3 = affine_map<(m,n) -> (5*m+n)>
171 %4 = array.new{(%i)[%c], (%m,%n)} : !array.type<#M1,2,#M3 x i1>
172 ```
173 }];
174
175 // See `VerifySizesForMultiAffineOps` for more explanation of these arguments.
176 let arguments = (ins
177 // Elements to initialize the array. Length is either zero or equal to
178 // the length of the flattened/linearized result ArrayType.
179 Variadic<ArrayElemType>:$elements,
180 // List of AffineMap operand groups where each group provides the
181 // arguments to instantiate the next (left-to-right) AffineMap used as an
182 // array dimension in the result ArrayType.
183 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
184 // Within each group in '$mapOperands', denotes the number of values that
185 // are AffineMap "dimensional" arguments with the remaining values being
186 // AffineMap "symbolic" arguments.
187 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
188 // Denotes the size of each variadic group in '$mapOperands'.
189 DenseI32ArrayAttr:$mapOpGroupSizes);
190 let results = (outs LLZK_ArrayType:$result);
191
192 // Define builders manually so inference of operand layout attributes is not
193 // circumvented.
194 let skipDefaultBuilders = 1;
195 let builders = [OpBuilder<(ins "::llzk::array::ArrayType":$result,
196 CArg<"::mlir::ValueRange", "{}">:$elements)>,
197 OpBuilder<(ins "::llzk::array::ArrayType":$result,
198 "::llvm::ArrayRef<::mlir::ValueRange>":$mapOperands,
199 "::mlir::DenseI32ArrayAttr":$numDimsPerMap)>,
200 OpBuilder<
201 (ins "::llzk::array::ArrayType":$result,
202 "::llvm::ArrayRef<::mlir::ValueRange>":$mapOperands,
203 "::llvm::ArrayRef<int32_t>":$numDimsPerMap),
204 [{
205 build($_builder, $_state, result, mapOperands, odsBuilder.getDenseI32ArrayAttr(numDimsPerMap));
206 }]>];
207
208 // This uses the custom parseInferredArrayType function to compute the type
209 // of '$elements' to match the type of '$result', except when '$elements'
210 // is empty, then the type of '$elements' must also be empty (size == 0).
211 // The if-then-else has '$elements' second so that an empty '$elements' list
212 // can be parsed when neither of these is specified.
213 let assemblyFormat = [{
214 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` ) : ( $elements )?
215 `:` type($result)
216 `` custom<InferredArrayType>(type($elements), ref($elements), ref(type($result)))
217 custom<AttrDictWithWarnings>(attr-dict, prop-dict)
218 }];
219
220 let extraClassDeclaration = [{
221 static ::mlir::ParseResult parseInferredArrayType(::mlir::OpAsmParser &parser,
222 ::llvm::SmallVector<::mlir::Type,1> &elementsTypes,
223 ::mlir::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> elements,
224 ::mlir::Type resultType
225 );
226 static void printInferredArrayType(::mlir::OpAsmPrinter &printer, CreateArrayOp,
227 ::mlir::TypeRange, ::mlir::OperandRange, ::mlir::Type
228 );
229 private:
230 static ::llvm::SmallVector<::mlir::Type> resultTypeToElementsTypes(::mlir::Type resultType);
231 }];
232
233 let hasVerifier = 1;
234}
235
236def LLZK_ReadArrayOp
237 : ScalarArrayAccessOp<
238 "read", true, [ArrayTypeElemsUnifyWithResultCustomInfer<"arr_ref">]> {
239 let summary = "read scalar from an array";
240 let description = [{
241 This operation reads the value from an array at the specified position.
242
243 Example of 1-dimensional array:
244 ```llzk
245 %i = arith.constant 0 : index
246 %0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
247 // %1 is now equal to %a
248 %1 = array.read %0[%i] : !array.type<3 x !felt.type>, !felt.type
249 ```
250
251 Example of 3-dimensional array:
252 ```llzk
253 %i = arith.constant 0 : index
254 %j = arith.constant 1 : index
255 %k = arith.constant 4 : index
256 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
257 // %1 is now equal to %a
258 %1 = array.read %0[%i, %j, %k] : !array.type<3,10,15 x !felt.type>, !felt.type
259 ```
260 }];
261
262 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
263 let results = (outs ArrayElemType:$result);
264
265 let assemblyFormat = [{
266 $arr_ref `[` $indices `]` `:` type($arr_ref) `,` type($result) attr-dict
267 }];
268
269 let hasVerifier = 1;
270}
271
272def LLZK_WriteArrayOp
273 : ScalarArrayAccessOp<
274 "write", false, [ArrayElemTypeUnifyWith<"arr_ref", "rvalue">]> {
275 let summary = "write scalar to an array";
276 let description = [{
277 This operation writes a value into an array at the specified position.
278
279 Example of 1-dimensional array:
280 ```llzk
281 %i = arith.constant 0 : index
282 %0 = felt.const 42
283 %1 = array.new %a, %b, %c : !array.type<3 x !felt.type>
284 // The array now is [%0, %b, %c]
285 array.write %1[%i] = %0 : !array.type<3 x !felt.type>, !felt.type
286 ```
287
288 Example of 2-dimensional array:
289 ```llzk
290 %i = arith.constant 0 : index
291 %j = arith.constant 0 : index
292 %0 = felt.const 42
293 %1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
294 // The array now is [[%0, %b], [%c, %d]]
295 array.write %1[%i, %j] = %0 : !array.type<2,2 x !felt.type>, !felt.type
296 ```
297 }];
298
299 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
300 ArrayElemType:$rvalue);
301
302 let assemblyFormat = [{
303 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
304 }];
305
306 let hasVerifier = 1;
307}
308
309def LLZK_ExtractArrayOp
310 : RangedArrayAccessOp<"extract",
311 true, [InferTypeOpAdaptorWithIsCompatible]> {
312 let summary = "read subarray from a multi-dimensional array";
313 let description = [{
314 This operation takes an N-dimensional array and K indices and extracts the
315 (N-K)-dimensional array by applying the given indices to the first `K`
316 dimensions of the array. Error if `K >= N`. Use `array.read` instead if `K == N`.
317
318 Extracting a 1-D array from 3-D array by selecting the index of 2 dimensions:
319 ```llzk
320 %i = arith.constant 1 : index
321 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
322 %1 = array.extract %0[%i,%i] : !array.type<3,10,15 x !felt.type>, !array.type<15 x !felt.type>
323 ```
324
325 Extracting 1-D arrays for subcomponents:
326 ```llzk
327 scf.for %iv = %lb to %up step %step {
328 %p = array.extract %in[%iv] : !array.type<@N,2 x !felt.type>
329 %c = array.read %a[%iv] : !array.type<@N x !struct.type<@SubC>>, !struct.type<@SubC>
330 function.call @SubC::@constrain(%c, %p) : (!struct.type<@SubC>, !array.type<2 x !felt.type>) -> ()
331 }
332 ```
333 }];
334
335 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
336 let results = (outs LLZK_ArrayType:$result);
337
338 let assemblyFormat = [{
339 $arr_ref `[` $indices `]` `:` type($arr_ref) attr-dict
340 }];
341}
342
343def LLZK_InsertArrayOp : RangedArrayAccessOp<"insert", false> {
344 let summary = "write subarray into a multi-dimensional array";
345 let description = [{
346 This operation takes an N-dimensional array, K indices, and an (N+K)-dimensional
347 array and inserts the N-dimensional array into the (N+K)-dimensional array at the
348 position specified by applying the given indices to the first `K` dimensions of
349 the (N+K)-dimensional array. Use `array.write` instead if `N == 0` (LLZK array type
350 must have at least 1 dimension so a 0-dimensional array cannot exist anyway).
351
352 Inserting 1-D arrays into a 2-D array:
353 ```llzk
354 %c = array.new : !array.type<2,3 x index>
355 // Array %c is uninitialized [[?, ?, ?], [?, ?, ?]]
356 %0 = arith.constant 0 : index
357 %a = array.new %r, %s, %t : !array.type<3 x index>
358 array.insert %c[%0] = %a : !array.type<2,3 x index>, !array.type<3 x index>
359 // Array %c is now [[%r, %s, %t], [?, ?, ?]]
360 %1 = arith.constant 1 : index
361 %b = array.new %x, %y, %z : !array.type<3 x index>
362 array.insert %c[%1] = %b : !array.type<2,3 x index>, !array.type<3 x index>
363 // Array %c is now [[%r, %s, %t], [%x, %y, %z]]
364 ```
365 }];
366
367 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
368 LLZK_ArrayType:$rvalue);
369
370 let assemblyFormat = [{
371 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
372 }];
373
374 let hasVerifier = 1;
375}
376
377def LLZK_ArrayLengthOp
378 : ArrayDialectOp<"len", [Pure,
379 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
380 DeclareOpInterfaceMethods<ArrayRefOpInterface>]> {
381 let summary = "return the length of an array";
382 let description = [{
383 This operation returns the size of the specified dimension of an array.
384
385 Example:
386 ```llzk
387 %a = array.new : !array.type<2,3 x !felt.type>
388 %0 = arith.constant 0 : index
389 %x = array.len %a, %0 : !array.type<2,3 x !felt.type> // result is 2
390 %1 = arith.constant 1 : index
391 %y = array.len %a, %1 : !array.type<2,3 x !felt.type> // result is 3
392 ```
393 }];
394
395 let arguments = (ins LLZK_ArrayType:$arr_ref, Index:$dim);
396 let results = (outs Index:$length);
397
398 let assemblyFormat = [{ $arr_ref `,` $dim `:` type($arr_ref) attr-dict }];
399
400 let extraClassDeclaration = [{
401 /// Gets the type of the referenced base array.
402 inline ::llzk::array::ArrayType getArrRefType() {
403 return ::llvm::cast<ArrayRefOpInterface>(getOperation()).getArrRefType();
404 }
405 }];
406}
407
408#endif // LLZK_ARRAY_OPS