1//===-- Ops.td ---------------------------------------------*- tablegen -*-===//
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
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
14//===----------------------------------------------------------------------===//
16#ifndef LLZK_STRUCT_OPS
17#define LLZK_STRUCT_OPS
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"
24include "llzk/Dialect/Verif/IR/OpInterfaces.td"
26include "mlir/IR/OpAsmInterface.td"
27include "mlir/IR/RegionKindInterface.td"
28include "mlir/IR/SymbolInterfaces.td"
29include "mlir/Interfaces/SideEffectInterfaces.td"
31class StructDialectOp<string mnemonic, list<Trait> traits = []>
32 : Op<StructDialect, mnemonic, traits>;
34/// Only valid/implemented for StructDefOp. Sets the proper `AllowWitnessAttr`
35/// and `AllowConstraintAttr` on the functions defined within the StructDefOp.
36def SetFuncAllowAttrs : NativeOpTrait<"SetFuncAllowAttrs">, StructuralOpTrait {
37 string cppNamespace = "::llzk::component";
40//===------------------------------------------------------------------===//
42//===------------------------------------------------------------------===//
45 : StructDialectOp<"def", [ParentOneOf<["::mlir::ModuleOp",
46 "::llzk::polymorphic::TemplateOp"]>,
47 Symbol, LLZKSymbolTable, IsolatedFromAbove,
48 SetFuncAllowAttrs, NoRegionArguments,
49 ContractTarget]#GraphRegionNoTerminator.traits> {
50 let summary = "circuit component definition";
52 This operation describes a component in a circuit. It can contain any number
53 of members that hold inputs, outputs, intermediate values, and subcomponents
54 of the defined component. It also contains a `compute()` function that holds
55 the witness generation code for the component and a `constrain()` function
56 that holds that constraint generation code for the component.
61 struct.def @ComponentA {
62 member @f1 : !array.type<5 x index>
63 member @f2 : !felt.type {llzk.pub}
65 function.def @compute(%p: !felt.type) -> !struct.type<@ComponentA> {
66 %self = struct.new : !struct.type<@ComponentA>
67 // initialize all members of `%self` here
68 return %self : !struct.type<@ComponentA>
71 function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
72 // emit constraints here
78 The optional `llzk.main = !struct.type<...>` attribute on the top-level module in an
79 LLZK IR program expresses the main entry point of the circuit as a concrete instantiation
80 of a specific struct. For example, `llzk.main = !struct.type<@Top<[52,12]>>` or
81 `llzk.main = !struct.type<@Main<[i1, !felt.type, 256]>>`.
82 This struct has additional restrictions:
83 1. The parameter types of its functions (besides the required "self" parameter) can
84 only be `!felt.type` or `!array.type<.. x !felt.type>`.
85 2. All inputs to the main struct are signals, even though they are not marked with
86 the `{signal}` attribute (as the `{signal}` attribute is not used on function arguments).
87 Input signals may be public (given the `{llzk.pub}` attribute) or private (by default).
88 3. All public members of the main struct are also signals (representing public output signals),
89 and can also only be `!felt.type` or `!array.type<.. x !felt.type>`.
91 Example of a `Main` component:
94 module attributes {llzk.main = !struct.type<@Main>, llzk.lang} {
96 member @out : !felt.type {llzk.pub, signal} // public output signal
97 member @out2 : !felt.type {llzk.pub} // also a public output signal, implicitly
98 member @intermediate : !struct.type<@OtherStruct> // an intermediate value, not a signal, can be any LLZK type
99 // %p is a private input signal
100 function.def @compute(%p: !felt.type) -> !struct.type<@Main> {
103 // %self is not a signal, but again, %p is a private input signal
104 function.def @constrain(%self: !struct.type<@Main>, %p: !felt.type) {
112 let arguments = (ins SymbolNameAttr:$sym_name);
114 let regions = (region SizedRegion<1>:$bodyRegion);
116 let assemblyFormat = [{ $sym_name $bodyRegion attr-dict }];
118 let useCustomPropertiesEncoding = 1;
120 let extraClassDeclaration = [{
121 /// Gets the StructType representing this struct. If the `constParams` to use in
122 /// the type are not given, the StructType will use `this->getParams()`.
123 StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {});
124 inline StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {}) const {
125 return const_cast<StructDefOp*>(this)->getType(constParams);
128 /// Gets the MemberDefOp that defines the member in this
129 /// structure with the given name, if present.
130 MemberDefOp getMemberDef(::mlir::StringAttr memberName);
132 /// Get all MemberDefOp in this structure.
133 ::std::vector<MemberDefOp> getMemberDefs();
135 /// Returns whether the struct defines members marked as columns.
136 ::mlir::LogicalResult hasColumns() {
137 return ::mlir::success(::llvm::any_of(getMemberDefs(), [](MemberDefOp memberOp) {
138 return memberOp.getColumn();
142 /// Returns whether the struct defines members marked as signals.
143 ::mlir::LogicalResult hasSignals() {
144 return ::mlir::success(::llvm::any_of(getMemberDefs(), [](MemberDefOp memberOp) {
145 return memberOp.getSignal();
149 /// Gets the FuncDefOp that defines the compute function in this structure, if present, or `nullptr` otherwise.
150 ::llzk::function::FuncDefOp getComputeFuncOp();
152 /// Gets the FuncDefOp that defines the constrain function in this structure, if present, or `nullptr` otherwise.
153 ::llzk::function::FuncDefOp getConstrainFuncOp();
155 /// Gets the FuncDefOp that defines the product function in this structure, if present, or `nullptr` otherwise
156 ::llzk::function::FuncDefOp getProductFuncOp();
158 /// Returns `true` iff this structure defines compute and constrain functions.
159 bool hasComputeConstrain() { return lookupSymbol(FUNC_NAME_COMPUTE) != nullptr && lookupSymbol(FUNC_NAME_CONSTRAIN) != nullptr; }
161 /// Generate header string, in the same format as the assemblyFormat.
162 ::std::string getHeaderString();
164 /// Return `true` iff the `struct.def` appears within a `poly.template` that defines
165 /// constant parameters and/or expressions.
166 bool hasTemplateSymbolBindings();
168 /// If this `struct.def` is within a `poly.template`, return names of all `poly.param`
169 /// within the `poly.template` in the order they are defined. Otherwise, return empty.
170 /// The names are returned as `FlatSymbolRefAttr` but the more general `Attribute` type
171 /// is used in the return type since that's usually what's needed.
172 ::llvm::SmallVector<::mlir::Attribute> getTemplateParamOpNames();
174 /// If this `struct.def` is within a `poly.template`, return names of all `poly.expr`
175 /// within the `poly.template` in the order they are defined. Otherwise, return empty.
176 /// The names are returned as `FlatSymbolRefAttr` but the more general `Attribute` type
177 /// is used in the return type since that's usually what's needed.
178 ::llvm::SmallVector<::mlir::Attribute> getTemplateExprOpNames();
180 /// Return the full name for this struct from the root module, including
181 /// any surrounding module scopes.
182 ::mlir::SymbolRefAttr getFullyQualifiedName();
184 /// Return `true` iff this `struct.def` is the main struct. See `llzk::MAIN_ATTR_NAME`.
185 bool isMainComponent();
188 let hasRegionVerifier = 1;
193 "member", [HasParent<"::llzk::component::StructDefOp">,
194 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
196 let summary = "struct member definition";
198 This operation describes a member in a struct/component.
203 struct.member @f1 : !felt.type
204 struct.member @f2 : !felt.type {llzk.pub}
205 struct.member @col1 : !felt.type {column}
206 struct.member @sig1 : !felt.type {signal}
207 struct.member @colsig1 : !felt.type {column, signal}
208 struct.member @pubcol : !felt.type {llzk.pub, column}
211 - Members marked with the `{llzk.pub}` attribute are considered public
212 and represent outputs of their defining struct/component.
213 - Members marked with the `{column}` attribute can be read/written with
214 table offsets using the `readm` and `writem` operations.
215 - Members marked with the `{signal}` attribute are constraint variables that
216 are stored in the witness; non-signal values are intermediate expressions.
218 Further restrictions on the `signal` attribute:
219 - It is only used on struct members, since they represent storage locations.
220 It is not used to mark struct inputs, as struct may be passed signal or non-signal
221 (i.e., intermediate expression) values.
222 - Only !felt.type or simple aggregates of !felt.type (i.e., !array.type and !pod.type)
223 may be marked as signals.
226 let arguments = (ins SymbolNameAttr:$sym_name, TypeAttrOf<AnyLLZKType>:$type,
227 UnitAttr:$column, UnitAttr:$signal);
229 // Define builders manually to avoid the default ones that have extra
230 // TypeRange parameters that must always be empty.
231 let skipDefaultBuilders = 1;
233 [OpBuilder<(ins "::mlir::StringAttr":$sym_name, "::mlir::TypeAttr":$type,
234 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
235 OpBuilder<(ins "::llvm::StringRef":$sym_name, "::mlir::Type":$type,
236 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
237 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
238 "::mlir::ValueRange":$operands,
239 "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
240 CArg<"bool", "false">:$isSignal, CArg<"bool", "false">:$isColumn)>,
241 // Simpler version since 'resultTypes' and 'operands' must be empty
243 (ins "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
244 CArg<"bool", "false">:$isSignal,
245 CArg<"bool", "false">:$isColumn),
246 [{ build($_builder, $_state, {}, {}, attributes, isSignal, isColumn); }]>];
248 let assemblyFormat = [{ $sym_name `:` $type attr-dict }];
250 let extraClassDeclaration = [{
251 /// Returns whether this member is a public output.
252 inline bool hasPublicAttr() { return getOperation()->hasAttr(llzk::PublicAttr::name); }
254 /// Adds or removes the unit `llzk.pub` attribute according to `newValue`.
255 void setPublicAttr(bool newValue = true);
261class MemberRefOpBase<string mnemonic, list<Trait> traits = []>
263 mnemonic, traits#[DeclareOpInterfaceMethods<MemberRefOpInterface>,
264 DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
265 bit isRead = ?; // read(1) vs write(0) ops
266 let extraClassDeclaration = [{
267 /// Gets the definition for the `member` referenced in this op.
268 inline ::mlir::FailureOr<SymbolLookupResult<MemberDefOp>> getMemberDefOp(::mlir::SymbolTableCollection &tables) {
269 return ::llvm::cast<MemberRefOpInterface>(getOperation()).getMemberDefOp(tables);
272 let extraClassDefinition = [{
273 /// Return `true` if the op is a read, `false` if it's a write.
274 bool $cppClass::isRead() {
275 return }]#!if(isRead, "true", "false")#[{;
281 : MemberRefOpBase<"readm", [VerifySizesForMultiAffineOps<1>,
282 MemoryEffects<[MemRead]>]> {
283 let summary = "read value of a struct member";
285 This operation copies the value of a named member in a struct/component.
286 The result is a value copy, not a pointer or alias to the member's storage.
287 When the member itself has `struct.type`, the copied value is an
288 identity-bearing handle to the same component instance.
290 A struct can read its own members regardless of whether they are marked as
291 public (i.e., with the `llzk.pub` attribute) or private (members without the
292 `llzk.pub` attribute). However, when reading members of other components, only
293 public members can be accessed. Free functions may also only read public members.
295 The value can be read from the signals table, in which case it can be
296 offset by a constant value. A negative value represents reading a value
297 backwards and a positive value represents reading a value forward.
298 Only members marked as columns can be read in this manner.
302 // See `VerifySizesForMultiAffineOps` for more explanation of these arguments.
303 let arguments = (ins LLZK_StructType:$component,
304 FlatSymbolRefAttr:$member_name,
305 OptionalAttr<AnyAttrOf<[SymbolRefAttr, IndexAttr,
306 AffineMapAttr]>>:$tableOffset,
307 // List of AffineMap operand groups where each group provides the
308 // arguments to instantiate the next (left-to-right) AffineMap used in
310 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
311 // Within each group in '$mapOperands', denotes the number of values that
312 // are AffineMap "dimensional" arguments with the remaining values being
313 // AffineMap "symbolic" arguments.
314 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
315 // Denotes the size of each variadic group in '$mapOperands'.
316 DenseI32ArrayAttr:$mapOpGroupSizes);
317 let results = (outs AnyLLZKType:$val);
319 // Define builders manually so inference of operand layout attributes is not
321 let skipDefaultBuilders = 1;
323 [OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
324 "::mlir::StringAttr":$member)>,
325 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
326 "::mlir::StringAttr":$member, "::mlir::Attribute":$dist,
327 "::mlir::ValueRange":$mapOperands,
328 "std::optional<int32_t>":$numDims)>,
329 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
330 "::mlir::StringAttr":$member,
331 "::mlir::SymbolRefAttr":$dist),
333 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
335 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
336 "::mlir::StringAttr":$member, "::mlir::IntegerAttr":$dist),
338 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
340 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
341 "::mlir::ValueRange":$operands,
342 "::mlir::ArrayRef<::mlir::NamedAttribute>":$attrs)>];
344 let assemblyFormat = [{
345 $component `[` $member_name `]`
346 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
347 `:` type($component) `,` type($val)
354def LLZK_MemberWriteOp
355 : MemberRefOpBase<"writem", [WitnessGen, MemoryEffects<[MemWrite]>]> {
356 let summary = "write value to a struct member";
358 This operation copies a value to a named member in a struct/component.
359 It does not create a pointer or alias between the source value and the member's
360 storage. When the value has `struct.type`, the copied value is an
361 identity-bearing handle to the same component instance.
363 A struct can write its own members. However, writing members of other components
368 let arguments = (ins LLZK_StructType:$component,
369 FlatSymbolRefAttr:$member_name, AnyLLZKType:$val);
371 let assemblyFormat = [{
372 $component `[` $member_name `]` `=` $val `:` type($component) `,` type($val) attr-dict
376def LLZK_CreateStructOp
377 : StructDialectOp<"new", [DeclareOpInterfaceMethods<
378 OpAsmOpInterface, ["getAsmResultNames"]>,
379 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
382 let summary = "create a new struct";
384 This operation creates a new, uninitialized instance of a struct.
389 %self = struct.new : !struct.type<@Reg>
393 let results = (outs LLZK_StructType:$result);
395 let assemblyFormat = [{ `:` type($result) attr-dict }];
398#endif // LLZK_STRUCT_OPS