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 private:
222 static ::mlir::ParseResult parseInferredArrayType(::mlir::OpAsmParser &parser,
223 ::llvm::SmallVector<::mlir::Type,1> &elementsTypes,
224 ::mlir::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> elements,
225 ::mlir::Type resultType
226 );
227
228 static void printInferredArrayType(::mlir::OpAsmPrinter &printer, CreateArrayOp,
229 ::mlir::TypeRange, ::mlir::OperandRange, ::mlir::Type
230 );
231
232 static ::llvm::SmallVector<::mlir::Type> resultTypeToElementsTypes(::mlir::Type resultType);
233 }];
234
235 let hasVerifier = 1;
236}
237
238def LLZK_ReadArrayOp
239 : ScalarArrayAccessOp<
240 "read", true, [ArrayTypeElemsUnifyWithResultCustomInfer<"arr_ref">]> {
241 let summary = "read scalar from an array";
242 let description = [{
243 This operation reads the value from an array at the specified position.
244
245 Example of 1-dimensional array:
246 ```llzk
247 %i = arith.constant 0 : index
248 %0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
249 // %1 is now equal to %a
250 %1 = array.read %0[%i] : !array.type<3 x !felt.type>, !felt.type
251 ```
252
253 Example of 3-dimensional array:
254 ```llzk
255 %i = arith.constant 0 : index
256 %j = arith.constant 1 : index
257 %k = arith.constant 4 : index
258 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
259 // %1 is now equal to %a
260 %1 = array.read %0[%i, %j, %k] : !array.type<3,10,15 x !felt.type>, !felt.type
261 ```
262 }];
263
264 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
265 let results = (outs ArrayElemType:$result);
266
267 let assemblyFormat = [{
268 $arr_ref `[` $indices `]` `:` type($arr_ref) `,` type($result) attr-dict
269 }];
270
271 let hasVerifier = 1;
272}
273
274def LLZK_WriteArrayOp
275 : ScalarArrayAccessOp<
276 "write", false, [ArrayElemTypeUnifyWith<"arr_ref", "rvalue">]> {
277 let summary = "write scalar to an array";
278 let description = [{
279 This operation writes a value into an array at the specified position.
280
281 Example of 1-dimensional array:
282 ```llzk
283 %i = arith.constant 0 : index
284 %0 = felt.const 42
285 %1 = array.new %a, %b, %c : !array.type<3 x !felt.type>
286 // The array now is [%0, %b, %c]
287 array.write %1[%i] = %0 : !array.type<3 x !felt.type>, !felt.type
288 ```
289
290 Example of 2-dimensional array:
291 ```llzk
292 %i = arith.constant 0 : index
293 %j = arith.constant 0 : index
294 %0 = felt.const 42
295 %1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
296 // The array now is [[%0, %b], [%c, %d]]
297 array.write %1[%i, %j] = %0 : !array.type<2,2 x !felt.type>, !felt.type
298 ```
299 }];
300
301 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
302 ArrayElemType:$rvalue);
303
304 let assemblyFormat = [{
305 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
306 }];
307
308 let hasVerifier = 1;
309}
310
311def LLZK_ExtractArrayOp
312 : RangedArrayAccessOp<"extract",
313 true, [InferTypeOpAdaptorWithIsCompatible]> {
314 let summary = "read subarray from a multi-dimensional array";
315 let description = [{
316 This operation takes an N-dimensional array and K indices and extracts the
317 (N-K)-dimensional array by applying the given indices to the first `K`
318 dimensions of the array. Error if `K >= N`. Use `array.read` instead if `K == N`.
319
320 Extracting a 1-D array from 3-D array by selecting the index of 2 dimensions:
321 ```llzk
322 %i = arith.constant 1 : index
323 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
324 %1 = array.extract %0[%i,%i] : !array.type<3,10,15 x !felt.type>, !array.type<15 x !felt.type>
325 ```
326
327 Extracting 1-D arrays for subcomponents:
328 ```llzk
329 scf.for %iv = %lb to %up step %step {
330 %p = array.extract %in[%iv] : !array.type<@N,2 x !felt.type>
331 %c = array.read %a[%iv] : !array.type<@N x !struct.type<@SubC>>, !struct.type<@SubC>
332 function.call @SubC::@constrain(%c, %p) : (!struct.type<@SubC>, !array.type<2 x !felt.type>) -> ()
333 }
334 ```
335 }];
336
337 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
338 let results = (outs LLZK_ArrayType:$result);
339
340 let assemblyFormat = [{
341 $arr_ref `[` $indices `]` `:` type($arr_ref) attr-dict
342 }];
343}
344
345def LLZK_InsertArrayOp : RangedArrayAccessOp<"insert", false> {
346 let summary = "write subarray into a multi-dimensional array";
347 let description = [{
348 This operation takes an N-dimensional array, K indices, and an (N+K)-dimensional
349 array and inserts the N-dimensional array into the (N+K)-dimensional array at the
350 position specified by applying the given indices to the first `K` dimensions of
351 the (N+K)-dimensional array. Use `array.write` instead if `N == 0` (LLZK array type
352 must have at least 1 dimension so a 0-dimensional array cannot exist anyway).
353
354 Inserting 1-D arrays into a 2-D array:
355 ```llzk
356 %c = array.new : !array.type<2,3 x index>
357 // Array %c is uninitialized [[?, ?, ?], [?, ?, ?]]
358 %0 = arith.constant 0 : index
359 %a = array.new %r, %s, %t : !array.type<3 x index>
360 array.insert %c[%0] = %a : !array.type<2,3 x index>, !array.type<3 x index>
361 // Array %c is now [[%r, %s, %t], [?, ?, ?]]
362 %1 = arith.constant 1 : index
363 %b = array.new %x, %y, %z : !array.type<3 x index>
364 array.insert %c[%1] = %b : !array.type<2,3 x index>, !array.type<3 x index>
365 // Array %c is now [[%r, %s, %t], [%x, %y, %z]]
366 ```
367 }];
368
369 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
370 LLZK_ArrayType:$rvalue);
371
372 let assemblyFormat = [{
373 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
374 }];
375
376 let hasVerifier = 1;
377}
378
379def LLZK_ArrayLengthOp
380 : ArrayDialectOp<"len", [Pure,
381 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
382 DeclareOpInterfaceMethods<ArrayRefOpInterface>]> {
383 let summary = "return the length of an array";
384 let description = [{
385 This operation returns the size of the specified dimension of an array.
386
387 Example:
388 ```llzk
389 %a = array.new : !array.type<2,3 x !felt.type>
390 %0 = arith.constant 0 : index
391 %x = array.len %a, %0 : !array.type<2,3 x !felt.type> // result is 2
392 %1 = arith.constant 1 : index
393 %y = array.len %a, %1 : !array.type<2,3 x !felt.type> // result is 3
394 ```
395 }];
396
397 let arguments = (ins LLZK_ArrayType:$arr_ref, Index:$dim);
398 let results = (outs Index:$length);
399
400 let assemblyFormat = [{ $arr_ref `,` $dim `:` type($arr_ref) attr-dict }];
401
402 let extraClassDeclaration = [{
403 /// Gets the type of the referenced base array.
404 inline ::llzk::array::ArrayType getArrRefType() {
405 return ::llvm::cast<ArrayRefOpInterface>(getOperation()).getArrRefType();
406 }
407 }];
408}
409
410#endif // LLZK_ARRAY_OPS