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"
25include "mlir/IR/OpAsmInterface.td"
26include "mlir/IR/RegionKindInterface.td"
27include "mlir/IR/SymbolInterfaces.td"
29class StructDialectOp<string mnemonic, list<Trait> traits = []>
30 : Op<StructDialect, mnemonic, traits>;
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";
38//===------------------------------------------------------------------===//
40//===------------------------------------------------------------------===//
44 "def", [ParentOneOf<["::mlir::ModuleOp",
45 "::llzk::polymorphic::TemplateOp"]>,
46 Symbol, LLZKSymbolTable, IsolatedFromAbove, SetFuncAllowAttrs,
47 NoRegionArguments]#GraphRegionNoTerminator.traits> {
48 let summary = "circuit component definition";
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.
59 struct.def @ComponentA {
60 member @f1 : !array.type<5 x index>
61 member @f2 : !felt.type {llzk.pub}
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>
69 function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
70 // emit constraints here
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>`.
89 Example of a `Main` component:
92 module attributes {llzk.main = !struct.type<@Main>, llzk.lang} {
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> {
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) {
110 let arguments = (ins SymbolNameAttr:$sym_name);
112 let regions = (region SizedRegion<1>:$bodyRegion);
114 let assemblyFormat = [{ $sym_name $bodyRegion attr-dict }];
116 let useCustomPropertiesEncoding = 1;
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);
126 /// Gets the MemberDefOp that defines the member in this
127 /// structure with the given name, if present.
128 MemberDefOp getMemberDef(::mlir::StringAttr memberName);
130 /// Get all MemberDefOp in this structure.
131 ::std::vector<MemberDefOp> getMemberDefs();
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();
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();
147 /// Gets the FuncDefOp that defines the compute function in this structure, if present, or `nullptr` otherwise.
148 ::llzk::function::FuncDefOp getComputeFuncOp();
150 /// Gets the FuncDefOp that defines the constrain function in this structure, if present, or `nullptr` otherwise.
151 ::llzk::function::FuncDefOp getConstrainFuncOp();
153 /// Gets the FuncDefOp that defines the product function in this structure, if present, or `nullptr` otherwise
154 ::llzk::function::FuncDefOp getProductFuncOp();
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; }
159 /// Generate header string, in the same format as the assemblyFormat.
160 ::std::string getHeaderString();
162 /// Return `true` iff the `struct.def` appears within a `poly.template` that defines
163 /// constant parameters and/or expressions.
164 bool hasTemplateSymbolBindings();
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();
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();
178 /// Return the full name for this struct from the root module, including
179 /// any surrounding module scopes.
180 ::mlir::SymbolRefAttr getFullyQualifiedName();
182 /// Return `true` iff this `struct.def` is the main struct. See `llzk::MAIN_ATTR_NAME`.
183 bool isMainComponent();
186 let hasRegionVerifier = 1;
191 "member", [HasParent<"::llzk::component::StructDefOp">,
192 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
194 let summary = "struct member definition";
196 This operation describes a member in a struct/component.
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}
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.
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.
224 let arguments = (ins SymbolNameAttr:$sym_name, TypeAttrOf<AnyLLZKType>:$type,
225 UnitAttr:$column, UnitAttr:$signal);
227 // Define builders manually to avoid the default ones that have extra
228 // TypeRange parameters that must always be empty.
229 let skipDefaultBuilders = 1;
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
241 (ins "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
242 CArg<"bool", "false">:$isSignal,
243 CArg<"bool", "false">:$isColumn),
244 [{ build($_builder, $_state, {}, {}, attributes, isSignal, isColumn); }]>];
246 let assemblyFormat = [{ $sym_name `:` $type attr-dict }];
248 let extraClassDeclaration = [{
249 inline bool hasPublicAttr() { return getOperation()->hasAttr(llzk::PublicAttr::name); }
250 void setPublicAttr(bool newValue = true);
256class MemberRefOpBase<string mnemonic, list<Trait> traits = []>
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);
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")#[{;
276 : MemberRefOpBase<"readm", [VerifySizesForMultiAffineOps<1>]> {
277 let summary = "read value of a struct member";
279 This operation reads the value of a named member in a struct/component.
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.
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.
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
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);
310 // Define builders manually so inference of operand layout attributes is not
312 let skipDefaultBuilders = 1;
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),
324 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
326 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
327 "::mlir::StringAttr":$member, "::mlir::IntegerAttr":$dist),
329 build($_builder, $_state, resultType, component, member, dist, ::mlir::ValueRange(), std::nullopt);
331 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
332 "::mlir::ValueRange":$operands,
333 "::mlir::ArrayRef<::mlir::NamedAttribute>":$attrs)>];
335 let assemblyFormat = [{
336 $component `[` $member_name `]`
337 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
338 `:` type($component) `,` type($val)
345def LLZK_MemberWriteOp : MemberRefOpBase<"writem", [WitnessGen]> {
346 let summary = "write value to a struct member";
348 This operation writes a value to a named member in a struct/component.
350 A struct can write its own members. However, writing members of other components
355 let arguments = (ins LLZK_StructType:$component,
356 FlatSymbolRefAttr:$member_name, AnyLLZKType:$val);
358 let assemblyFormat = [{
359 $component `[` $member_name `]` `=` $val `:` type($component) `,` type($val) attr-dict
363def LLZK_CreateStructOp
364 : StructDialectOp<"new", [DeclareOpInterfaceMethods<
365 OpAsmOpInterface, ["getAsmResultNames"]>,
366 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
369 let summary = "create a new struct";
371 This operation creates a new, uninitialized instance of a struct.
376 %self = struct.new : !struct.type<@Reg>
380 let results = (outs LLZK_StructType:$result);
382 let assemblyFormat = [{ `:` type($result) attr-dict }];
385#endif // LLZK_STRUCT_OPS