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>
49 &mustBeSafelyUsed) {
50 return ::llvm::cast<ArrayAccessOpInterface>(getOperation())
51 .canRewire(slot, usedIndices, mustBeSafelyUsed);
52 }
53
54 /// Required by DestructurableAllocationOpInterface / SROA pass
55 ::mlir::DeletionKind $cppClass::rewire(const
56 ::mlir::DestructurableMemorySlot &slot,
57 ::llvm::DenseMap<::mlir::Attribute, ::mlir::MemorySlot> &subslots,
58 ::mlir::RewriterBase &rewriter) {
59 return ::llvm::cast<ArrayAccessOpInterface>(getOperation())
60 .rewire(slot, subslots, rewriter);
61 }
62
63 /// Required by PromotableMemOpInterface / mem2reg pass
64 bool $cppClass::loadsFrom(const ::mlir::MemorySlot &slot) {
65 return }]#!if(isRead, "getArrRef() == slot.ptr", "false")#[{;
66 }
67
68 /// Required by PromotableMemOpInterface / mem2reg pass
69 bool $cppClass::storesTo(const ::mlir::MemorySlot &slot) {
70 return }]#!if(isRead, "false", "getArrRef() == slot.ptr")#[{;
71 }
72
73 /// Required by PromotableAllocationOpInterface / mem2reg pass
74 ::mlir::Value $cppClass::getStored(const ::mlir::MemorySlot &, ::mlir::RewriterBase &) {
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
118 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 from the given values using the specified shape
125 %1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
126
127 // Create an uninitialized array
128 %2 = array.new : !array.type<3,2 x !felt.type>
129 ```
130
131 The values used to construct the array must have type that exactly matches
132 the element type of the specified array type. This is true even if a `tvar`
133 type is used. In other words, cannot mix `tvar<@X>` with `tvar<@Y>` or any
134 concrete type. In such a scenario, first create an uninitialized array, as
135 shown in the examples above, and then use `array.write` to write each element
136 of the array.
137
138 Implementation note: This restriction exists due to a combination of:
139 (1) we have chosen to infer the type of `$elements` from the `$result`
140 ArrayType, via parseInferredArrayType(), rather than requiring the type of
141 every element be listed in the assembly format and,
142 (2) within the parser for an Op, there is no way to get the Value instances
143 for the operands aside from `OpAsmParser::resolveOperands()` which requires
144 the type of every operand to be known and ends up comparing the expected
145 to actual type via `operator==`. Thus, there is no way for this to be
146 successful apart from all elements having the exact type inferred in (1).
147
148 Also note that `std::equal_to` is used in the `VariadicTypesMatchWith`
149 trait on this Op so that the verifier function mirrors the aforementioned
150 restriction in the parser.
151
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 let arguments = (ins Variadic<ArrayElemType>:$elements,
176 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
177 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
178 DenseI32ArrayAttr:$mapOpGroupSizes);
179 let results = (outs LLZK_ArrayType:$result);
180
181 // Define builders manually so inference of operand layout attributes is not
182 // circumvented.
183 let skipDefaultBuilders = 1;
184 let builders = [OpBuilder<(ins "::llzk::array::ArrayType":$result,
185 CArg<"::mlir::ValueRange", "{}">:$elements)>,
186 OpBuilder<(ins "::llzk::array::ArrayType":$result,
187 "::llvm::ArrayRef<::mlir::ValueRange>":$mapOperands,
188 "::mlir::DenseI32ArrayAttr":$numDimsPerMap)>,
189 OpBuilder<
190 (ins "::llzk::array::ArrayType":$result,
191 "::llvm::ArrayRef<::mlir::ValueRange>":$mapOperands,
192 "::llvm::ArrayRef<int32_t>":$numDimsPerMap),
193 [{
194 build($_builder, $_state, result, mapOperands, odsBuilder.getDenseI32ArrayAttr(numDimsPerMap));
195 }]>];
196
197 // This uses the custom parseInferredArrayType function to compute the type
198 // of '$elements' to match the type of '$result', except when '$elements'
199 // is empty, then the type of '$elements' must also be empty (size == 0).
200 // The if-then-else has '$elements' second so that an empty '$elements' list
201 // can be parsed when neither of these is specified.
202 let assemblyFormat = [{
203 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` ) : ( $elements )?
204 `:` type($result)
205 `` custom<InferredArrayType>(type($elements), ref($elements), ref(type($result)))
206 custom<AttrDictWithWarnings>(attr-dict, prop-dict)
207 }];
208
209 let extraClassDeclaration = [{
210 static ::mlir::ParseResult parseInferredArrayType(::mlir::OpAsmParser &parser,
211 ::llvm::SmallVector<::mlir::Type,1> &elementsTypes,
212 ::mlir::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> elements,
213 ::mlir::Type resultType
214 );
215 static void printInferredArrayType(::mlir::OpAsmPrinter &printer, CreateArrayOp,
216 ::mlir::TypeRange, ::mlir::OperandRange, ::mlir::Type
217 );
218 private:
219 static ::llvm::SmallVector<::mlir::Type> resultTypeToElementsTypes(::mlir::Type resultType);
220 }];
221
222 let hasVerifier = 1;
223}
224
225def LLZK_ReadArrayOp
226 : ScalarArrayAccessOp<
227 "read", true, [ArrayTypeElemsUnifyWithResultCustomInfer<"arr_ref">]> {
228 let summary = "read scalar from an array";
229 let description = [{
230 This operation reads the value from an array at the specified position.
231
232 Example of 1-dimensional array:
233 ```llzk
234 %i = arith.constant 0 : index
235 %0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
236 // %1 is now equal to %a
237 %1 = array.read %0[%i] : !array.type<3 x !felt.type>, !felt.type
238 ```
239
240 Example of 3-dimensional array:
241 ```llzk
242 %i = arith.constant 0 : index
243 %j = arith.constant 1 : index
244 %k = arith.constant 4 : index
245 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
246 // %1 is now equal to %a
247 %1 = array.read %0[%i, %j, %k] : !array.type<3,10,15 x !felt.type>, !felt.type
248 ```
249 }];
250
251 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
252 let results = (outs ArrayElemType:$result);
253
254 let assemblyFormat = [{
255 $arr_ref `[` $indices `]` `:` type($arr_ref) `,` type($result) attr-dict
256 }];
257
258 let hasVerifier = 1;
259}
260
261def LLZK_WriteArrayOp
262 : ScalarArrayAccessOp<
263 "write", false, [ArrayElemTypeUnifyWith<"arr_ref", "rvalue">]> {
264 let summary = "write scalar to an array";
265 let description = [{
266 This operation writes a value into an array at the specified position.
267
268 Example of 1-dimensional array:
269 ```llzk
270 %i = arith.constant 0 : index
271 %0 = felt.const 42
272 %1 = array.new %a, %b, %c : !array.type<3 x !felt.type>
273 // The array now is [%0, %b, %c]
274 array.write %1[%i] = %0 : !array.type<3 x !felt.type>, !felt.type
275 ```
276
277 Example of 2-dimensional array:
278 ```llzk
279 %i = arith.constant 0 : index
280 %j = arith.constant 0 : index
281 %0 = felt.const 42
282 %1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
283 // The array now is [[%0, %b], [%c, %d]]
284 array.write %1[%i, %j] = %0 : !array.type<2,2 x !felt.type>, !felt.type
285 ```
286 }];
287
288 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
289 ArrayElemType:$rvalue);
290
291 let assemblyFormat = [{
292 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
293 }];
294
295 let hasVerifier = 1;
296}
297
298def LLZK_ExtractArrayOp
299 : RangedArrayAccessOp<"extract",
300 true, [InferTypeOpAdaptorWithIsCompatible]> {
301 let summary = "read subarray from a multi-dimensional array";
302 let description = [{
303 This operation takes an N-dimensional array and K indices and extracts the
304 (N-K)-dimensional array by applying the given indices to the first `K`
305 dimensions of the array. Error if `K >= N`. Use `array.read` instead if `K == N`.
306
307 Extracting a 1-D array from 3-D array by selecting the index of 2 dimensions:
308 ```llzk
309 %i = arith.constant 1 : index
310 %0 = array.new ... : !array.type<3,10,15 x !felt.type>
311 %1 = array.extract %0[%i,%i] : !array.type<3,10,15 x !felt.type>, !array.type<15 x !felt.type>
312 ```
313
314 Extracting 1-D arrays for subcomponents:
315 ```llzk
316 scf.for %iv = %lb to %up step %step {
317 %p = array.extract %in[%iv] : !array.type<@N,2 x !felt.type>
318 %c = array.read %a[%iv] : !array.type<@N x !struct.type<@SubC>>, !struct.type<@SubC>
319 function.call @SubC::@constrain(%c, %p) : (!struct.type<@SubC>, !array.type<2 x !felt.type>) -> ()
320 }
321 ```
322 }];
323
324 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices);
325 let results = (outs LLZK_ArrayType:$result);
326
327 let assemblyFormat = [{
328 $arr_ref `[` $indices `]` `:` type($arr_ref) attr-dict
329 }];
330}
331
332def LLZK_InsertArrayOp : RangedArrayAccessOp<"insert", false> {
333 let summary = "write subarray into a multi-dimensional array";
334 let description = [{
335 This operation takes an N-dimensional array, K indices, and an (N+K)-dimensional
336 array and inserts the N-dimensional array into the (N+K)-dimensional array at the
337 position specified by applying the given indices to the first `K` dimensions of
338 the (N+K)-dimensional array. Use `array.write` instead if `N == 0` (LLZK array type
339 must have at least 1 dimension so a 0-dimensional array cannot exist anyway).
340
341 Inserting 1-D arrays into a 2-D array:
342 ```llzk
343 %c = array.new : !array.type<2,3 x index>
344 // Array %c is uninitialized [[?, ?, ?], [?, ?, ?]]
345 %0 = arith.constant 0 : index
346 %a = array.new %r, %s, %t : !array.type<3 x index>
347 array.insert %c[%0] = %a : !array.type<2,3 x index>, !array.type<3 x index>
348 // Array %c is now [[%r, %s, %t], [?, ?, ?]]
349 %1 = arith.constant 1 : index
350 %b = array.new %x, %y, %z : !array.type<3 x index>
351 array.insert %c[%1] = %b : !array.type<2,3 x index>, !array.type<3 x index>
352 // Array %c is now [[%r, %s, %t], [%x, %y, %z]]
353 ```
354 }];
355
356 let arguments = (ins LLZK_ArrayType:$arr_ref, Variadic<Index>:$indices,
357 LLZK_ArrayType:$rvalue);
358
359 let assemblyFormat = [{
360 $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict
361 }];
362
363 let hasVerifier = 1;
364}
365
366def LLZK_ArrayLengthOp
367 : ArrayDialectOp<"len", [Pure,
368 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
369 DeclareOpInterfaceMethods<ArrayRefOpInterface>]> {
370 let summary = "return the length of an array";
371 let description = [{
372 This operation returns the size of the specified dimension of an array.
373
374 Example:
375 ```llzk
376 %a = array.new : !array.type<2,3 x !felt.type>
377 %0 = arith.constant 0 : index
378 %x = array.len %a, %0 : !array.type<2,3 x !felt.type> // result is 2
379 %1 = arith.constant 1 : index
380 %y = array.len %a, %1 : !array.type<2,3 x !felt.type> // result is 3
381 ```
382 }];
383
384 let arguments = (ins LLZK_ArrayType:$arr_ref, Index:$dim);
385 let results = (outs Index:$length);
386
387 let assemblyFormat = [{ $arr_ref `,` $dim `:` type($arr_ref) attr-dict }];
388
389 let extraClassDeclaration = [{
390 /// Gets the type of the referenced base array.
391 inline ::llzk::array::ArrayType getArrRefType() {
392 return ::llvm::cast<ArrayRefOpInterface>(getOperation()).getArrRefType();
393 }
394 }];
395}
396
397#endif // LLZK_ARRAY_OPS