LLZK 2.0.0
An open-source IR for Zero Knowledge (ZK) circuits
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// Copyright 2026 Project LLZK
7// SPDX-License-Identifier: Apache-2.0
8//
9// Adapted from mlir/include/mlir/Dialect/Func/IR/FuncOps.td
10// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
11// See https://llvm.org/LICENSE.txt for license information.
12// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
13//
14//===----------------------------------------------------------------------===//
15
16#ifndef LLZK_STRUCT_OPS
17#define LLZK_STRUCT_OPS
18
19include "llzk/Dialect/Function/IR/OpTraits.td"
20include "llzk/Dialect/Struct/IR/Dialect.td"
21include "llzk/Dialect/Struct/IR/OpInterfaces.td"
22include "llzk/Dialect/Struct/IR/Types.td"
23include "llzk/Dialect/Shared/OpTraits.td"
24
25include "mlir/IR/OpAsmInterface.td"
26include "mlir/IR/RegionKindInterface.td"
27include "mlir/IR/SymbolInterfaces.td"
28
29class StructDialectOp<string mnemonic, list<Trait> traits = []>
30 : Op<StructDialect, mnemonic, traits>;
31
32/// Only valid/implemented for StructDefOp. Sets the proper `AllowWitnessAttr`
33/// and `AllowConstraintAttr` on the functions defined within the StructDefOp.
34def SetFuncAllowAttrs : NativeOpTrait<"SetFuncAllowAttrs">, StructuralOpTrait {
35 string cppNamespace = "::llzk::component";
36}
37
38//===------------------------------------------------------------------===//
39// Struct Operations
40//===------------------------------------------------------------------===//
41
42def LLZK_StructDefOp
43 : StructDialectOp<
44 "def", [ParentOneOf<["::mlir::ModuleOp",
45 "::llzk::polymorphic::TemplateOp"]>,
46 Symbol, LLZKSymbolTable, IsolatedFromAbove, SetFuncAllowAttrs,
47 NoRegionArguments]#GraphRegionNoTerminator.traits> {
48 let summary = "circuit component definition";
49 let description = [{
50 This operation describes a component in a circuit. It can contain any number
51 of members that hold inputs, outputs, intermediate values, and subcomponents
52 of the defined component. It also contains a `compute()` function that holds
53 the witness generation code for the component and a `constrain()` function
54 that holds that constraint generation code for the component.
55
56 Example:
57
58 ```llzk
59 struct.def @ComponentA {
60 member @f1 : !array.type<5 x index>
61 member @f2 : !felt.type {llzk.pub}
62
63 function.def @compute(%p: !felt.type) -> !struct.type<@ComponentA> {
64 %self = struct.new : !struct.type<@ComponentA>
65 // initialize all members of `%self` here
66 return %self : !struct.type<@ComponentA>
67 }
68
69 function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
70 // emit constraints here
71 return
72 }
73 }
74 ```
75
76 The optional `llzk.main = !struct.type<...>` attribute on the top-level module in an
77 LLZK IR program expresses the main entry point of the circuit as a concrete instantiation
78 of a specific struct. For example, `llzk.main = !struct.type<@Top<[52,12]>>` or
79 `llzk.main = !struct.type<@Main<[i1, !felt.type, 256]>>`.
80 This struct has additional restrictions:
81 1. The parameter types of its functions (besides the required "self" parameter) can
82 only be `!felt.type` or `!array.type<.. x !felt.type>`.
83 2. All inputs to the main struct are signals, even though they are not marked with
84 the `{signal}` attribute (as the `{signal}` attribute is not used on function arguments).
85 Input signals may be public (given the `{llzk.pub}` attribute) or private (by default).
86 3. All public members of the main struct are also signals (representing public output signals),
87 and can also only be `!felt.type` or `!array.type<.. x !felt.type>`.
88
89 Example of a `Main` component:
90
91 ```llzk
92 module attributes {llzk.main = !struct.type<@Main>, llzk.lang} {
93 struct.def @Main {
94 member @out : !felt.type {llzk.pub, signal} // public output signal
95 member @out2 : !felt.type {llzk.pub} // also a public output signal, implicitly
96 member @intermediate : !struct.type<@OtherStruct> // an intermediate value, not a signal, can be any LLZK type
97 // %p is a private input signal
98 function.def @compute(%p: !felt.type) -> !struct.type<@Main> {
99 // ...
100 }
101 // %self is not a signal, but again, %p is a private input signal
102 function.def @constrain(%self: !struct.type<@Main>, %p: !felt.type) {
103 // ...
104 }
105 }
106 }
107 ```
108 }];
109
110 let arguments = (ins SymbolNameAttr:$sym_name);
111
112 let regions = (region SizedRegion<1>:$bodyRegion);
113
114 let assemblyFormat = [{ $sym_name $bodyRegion attr-dict }];
115
116 let useCustomPropertiesEncoding = 1;
117
118 let extraClassDeclaration = [{
119 /// Gets the StructType representing this struct. If the `constParams` to use in
120 /// the type are not given, the StructType will use `this->getParams()`.
121 StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {});
122 inline StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {}) const {
123 return const_cast<StructDefOp*>(this)->getType(constParams);
124 }
125
126 /// Gets the MemberDefOp that defines the member in this
127 /// structure with the given name, if present.
128 MemberDefOp getMemberDef(::mlir::StringAttr memberName);
129
130 /// Get all MemberDefOp in this structure.
131 ::std::vector<MemberDefOp> getMemberDefs();
132
133 /// Returns whether the struct defines members marked as columns.
134 ::mlir::LogicalResult hasColumns() {
135 return ::mlir::success(::llvm::any_of(getMemberDefs(), [](MemberDefOp memberOp) {
136 return memberOp.getColumn();
137 }));
138 }
139
140 /// Returns whether the struct defines members marked as signals.
141 ::mlir::LogicalResult hasSignals() {
142 return ::mlir::success(::llvm::any_of(getMemberDefs(), [](MemberDefOp memberOp) {
143 return memberOp.getSignal();
144 }));
145 }
146
147 /// Gets the FuncDefOp that defines the compute function in this structure, if present, or `nullptr` otherwise.
148 ::llzk::function::FuncDefOp getComputeFuncOp();
149
150 /// Gets the FuncDefOp that defines the constrain function in this structure, if present, or `nullptr` otherwise.
151 ::llzk::function::FuncDefOp getConstrainFuncOp();
152
153 /// Gets the FuncDefOp that defines the product function in this structure, if present, or `nullptr` otherwise
154 ::llzk::function::FuncDefOp getProductFuncOp();
155
156 /// Returns `true` iff this structure defines compute and constrain functions.
157 bool hasComputeConstrain() { return lookupSymbol(FUNC_NAME_COMPUTE) != nullptr && lookupSymbol(FUNC_NAME_CONSTRAIN) != nullptr; }
158
159 /// Generate header string, in the same format as the assemblyFormat.
160 ::std::string getHeaderString();
161
162 /// Return `true` iff the `struct.def` appears within a `poly.template` that defines
163 /// constant parameters and/or expressions.
164 bool hasTemplateSymbolBindings();
165
166 /// If this `struct.def` is within a `poly.template`, return names of all `poly.param`
167 /// within the `poly.template` in the order they are defined. Otherwise, return empty.
168 /// The names are returned as `FlatSymbolRefAttr` but the more general `Attribute` type
169 /// is used in the return type since that's usually what's needed.
170 ::llvm::SmallVector<::mlir::Attribute> getTemplateParamOpNames();
171
172 /// If this `struct.def` is within a `poly.template`, return names of all `poly.expr`
173 /// within the `poly.template` in the order they are defined. Otherwise, return empty.
174 /// The names are returned as `FlatSymbolRefAttr` but the more general `Attribute` type
175 /// is used in the return type since that's usually what's needed.
176 ::llvm::SmallVector<::mlir::Attribute> getTemplateExprOpNames();
177
178 /// Return the full name for this struct from the root module, including
179 /// any surrounding module scopes.
180 ::mlir::SymbolRefAttr getFullyQualifiedName();
181
182 /// Return `true` iff this `struct.def` is the main struct. See `llzk::MAIN_ATTR_NAME`.
183 bool isMainComponent();
184 }];
185
186 let hasRegionVerifier = 1;
187}
188
189def LLZK_MemberDefOp
190 : StructDialectOp<
191 "member", [HasParent<"::llzk::component::StructDefOp">,
192 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
193 Symbol]> {
194 let summary = "struct member definition";
195 let description = [{
196 This operation describes a member in a struct/component.
197
198 Example:
199
200 ```llzk
201 struct.member @f1 : !felt.type
202 struct.member @f2 : !felt.type {llzk.pub}
203 struct.member @col1 : !felt.type {column}
204 struct.member @sig1 : !felt.type {signal}
205 struct.member @colsig1 : !felt.type {column, signal}
206 struct.member @pubcol : !felt.type {llzk.pub, column}
207 ```
208
209 - Members marked with the `{llzk.pub}` attribute are considered public
210 and represent outputs of their defining struct/component.
211 - Members marked with the `{column}` attribute can be read/written with
212 table offsets using the `readm` and `writem` operations.
213 - Members marked with the `{signal}` attribute are constraint variables that
214 are stored in the witness; non-signal values are intermediate expressions.
215
216 Further restrictions on the `signal` attribute:
217 - It is only used on struct members, since they represent storage locations.
218 It is not used to mark struct inputs, as struct may be passed signal or non-signal
219 (i.e., intermediate expression) values.
220 - Only !felt.type or simple aggregates of !felt.type (i.e., !array.type and !pod.type)
221 may be marked as signals.
222 }];
223
224 let arguments = (ins SymbolNameAttr:$sym_name, TypeAttrOf<AnyLLZKType>:$type,
225 UnitAttr:$column, UnitAttr:$signal);
226
227 // Define builders manually to avoid the default ones that have extra
228 // TypeRange parameters that must always be empty.
229 let skipDefaultBuilders = 1;
230 let builders =
231 [OpBuilder<(ins "::mlir::StringAttr":$sym_name, "::mlir::TypeAttr":$type,
232 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
233 OpBuilder<(ins "::llvm::StringRef":$sym_name, "::mlir::Type":$type,
234 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
235 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
236 "::mlir::ValueRange":$operands,
237 "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
238 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
239 // Simpler version since 'resultTypes' and 'operands' must be empty
240 OpBuilder<
241 (ins "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
242 CArg<"bool", "false">:$isSignal,
243 CArg<"bool", "false">:$isColumn),
244 [{ build($_builder, $_state, {}, {}, attributes, isSignal, isColumn); }]>];
245
246 let assemblyFormat = [{ $sym_name `:` $type attr-dict }];
247
248 let extraClassDeclaration = [{
249 inline bool hasPublicAttr() { return getOperation()->hasAttr(llzk::PublicAttr::name); }
250 void setPublicAttr(bool newValue = true);
251 }];
252
253 let hasVerifier = 1;
254}
255
256class MemberRefOpBase<string mnemonic, list<Trait> traits = []>
257 : StructDialectOp<
258 mnemonic, traits#[DeclareOpInterfaceMethods<MemberRefOpInterface>,
259 DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
260 bit isRead = ?; // read(1) vs write(0) ops
261 let extraClassDeclaration = [{
262 /// Gets the definition for the `member` referenced in this op.
263 inline ::mlir::FailureOr<SymbolLookupResult<MemberDefOp>> getMemberDefOp(::mlir::SymbolTableCollection &tables) {
264 return ::llvm::cast<MemberRefOpInterface>(getOperation()).getMemberDefOp(tables);
265 }
266 }];
267 let extraClassDefinition = [{
268 /// Return `true` if the op is a read, `false` if it's a write.
269 bool $cppClass::isRead() {
270 return }]#!if(isRead, "true", "false")#[{;
271 }
272 }];
273}
274
275def LLZK_MemberReadOp
276 : MemberRefOpBase<"readm", [VerifySizesForMultiAffineOps<1>]> {
277 let summary = "read value of a struct member";
278 let description = [{
279 This operation reads the value of a named member in a struct/component.
280
281 A struct can read its own members regardless of whether they are marked as
282 public (i.e., with the `llzk.pub` attribute) or private (members without the
283 `llzk.pub` attribute). However, when reading members of other components, only
284 public members can be accessed. Free functions may also only read public members.
285
286 The value can be read from the signals table, in which case it can be
287 offset by a constant value. A negative value represents reading a value
288 backwards and a positive value represents reading a value forward.
289 Only members marked as columns can be read in this manner.
290 }];
291 let isRead = 1;
292
293 // See `VerifySizesForMultiAffineOps` for more explanation of these arguments.
294 let arguments = (ins LLZK_StructType:$component,
295 FlatSymbolRefAttr:$member_name,
296 OptionalAttr<AnyAttrOf<[SymbolRefAttr, IndexAttr,
297 AffineMapAttr]>>:$tableOffset,
298 // List of AffineMap operand groups where each group provides the
299 // arguments to instantiate the next (left-to-right) AffineMap used in
300 // `tableOffset`.
301 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
302 // Within each group in '$mapOperands', denotes the number of values that
303 // are AffineMap "dimensional" arguments with the remaining values being
304 // AffineMap "symbolic" arguments.
305 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
306 // Denotes the size of each variadic group in '$mapOperands'.
307 DenseI32ArrayAttr:$mapOpGroupSizes);
308 let results = (outs AnyLLZKType:$val);
309
310 // Define builders manually so inference of operand layout attributes is not
311 // circumvented.
312 let skipDefaultBuilders = 1;
313 let builders =
314 [OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
315 "::mlir::StringAttr":$member)>,
316 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
317 "::mlir::StringAttr":$member, "::mlir::Attribute":$dist,
318 "::mlir::ValueRange":$mapOperands,
319 "std::optional<int32_t>":$numDims)>,
320 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
321 "::mlir::StringAttr":$member,
322 "::mlir::SymbolRefAttr":$dist),
323 [{
324 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
325 }]>,
326 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
327 "::mlir::StringAttr":$member, "::mlir::IntegerAttr":$dist),
328 [{
329 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
330 }]>,
331 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
332 "::mlir::ValueRange":$operands,
333 "::mlir::ArrayRef<::mlir::NamedAttribute>":$attrs)>];
334
335 let assemblyFormat = [{
336 $component `[` $member_name `]`
337 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
338 `:` type($component) `,` type($val)
339 attr-dict
340 }];
341
342 let hasVerifier = 1;
343}
344
345def LLZK_MemberWriteOp : MemberRefOpBase<"writem", [WitnessGen]> {
346 let summary = "write value to a struct member";
347 let description = [{
348 This operation writes a value to a named member in a struct/component.
349
350 A struct can write its own members. However, writing members of other components
351 is not allowed.
352 }];
353 let isRead = 0;
354
355 let arguments = (ins LLZK_StructType:$component,
356 FlatSymbolRefAttr:$member_name, AnyLLZKType:$val);
357
358 let assemblyFormat = [{
359 $component `[` $member_name `]` `=` $val `:` type($component) `,` type($val) attr-dict
360 }];
361}
362
363def LLZK_CreateStructOp
364 : StructDialectOp<"new", [DeclareOpInterfaceMethods<
365 OpAsmOpInterface, ["getAsmResultNames"]>,
366 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
367 WitnessGen,
368]> {
369 let summary = "create a new struct";
370 let description = [{
371 This operation creates a new, uninitialized instance of a struct.
372
373 Example:
374
375 ```llzk
376 %self = struct.new : !struct.type<@Reg>
377 ```
378 }];
379
380 let results = (outs LLZK_StructType:$result);
381
382 let assemblyFormat = [{ `:` type($result) attr-dict }];
383}
384
385#endif // LLZK_STRUCT_OPS