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// Adapted from mlir/include/mlir/Dialect/Func/IR/FuncOps.td
9// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
10// See https://llvm.org/LICENSE.txt for license information.
11// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
12//
13//===----------------------------------------------------------------------===//
14
15#ifndef LLZK_STRUCT_OPS
16#define LLZK_STRUCT_OPS
17
18include "llzk/Dialect/Function/IR/OpTraits.td"
19include "llzk/Dialect/Struct/IR/Dialect.td"
20include "llzk/Dialect/Struct/IR/OpInterfaces.td"
21include "llzk/Dialect/Struct/IR/Types.td"
22include "llzk/Dialect/Shared/OpTraits.td"
23
24include "mlir/IR/OpAsmInterface.td"
25include "mlir/IR/RegionKindInterface.td"
26include "mlir/IR/SymbolInterfaces.td"
27
28class StructDialectOp<string mnemonic, list<Trait> traits = []>
29 : Op<StructDialect, mnemonic, traits>;
30
31/// Only valid/implemented for StructDefOp. Sets the proper
32/// `AllowConstraintAttr` and `AllowWitnessAttr` on the functions defined within
33/// 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", [HasParent<"::mlir::ModuleOp">, Symbol, SymbolTable,
45 IsolatedFromAbove, GraphRegionNoTerminator, SetFuncAllowAttrs,
46 DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
47 let summary = "circuit component definition";
48 let description = [{
49 This operation describes a component in a circuit. It can contain any number
50 of fields that hold inputs, outputs, intermediate values, and subcomponents
51 of the defined component. It also contains a `compute()` function that holds
52 the witness generation code for the component and a `constrain()` function
53 that holds that constraint generation code for the component.
54
55 Example:
56
57 ```llzk
58 struct.def @ComponentA {
59 field @f1 : !array.type<5 x index>
60 field @f2 : !felt.type {llzk.pub}
61
62 function.def @compute(%p: !felt.type) -> !struct.type<@ComponentA> {
63 %self = struct.new : !struct.type<@ComponentA>
64 // initialize all fields of `%self` here
65 return %self : !struct.type<@ComponentA>
66 }
67
68 function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
69 // emit constraints here
70 return
71 }
72 }
73 ```
74 }];
75
76 // Note: `$const_params` contains symbol definitions that do not use the
77 // standard SymbolTable mechanism. Instead hasParamNamed() can be used to
78 // check if a certain FlatSymbolRefAttr is a parameter in the function.
79 let arguments = (ins SymbolNameAttr:$sym_name,
80 OptionalAttr<FlatSymbolRefArrayAttr>:$const_params);
81
82 let regions = (region SizedRegion<1>:$body);
83
84 let assemblyFormat = [{
85 $sym_name (`<` $const_params^ `>`)? $body attr-dict
86 }];
87
88 let extraClassDeclaration = [{
89 /// Gets the StructType representing this struct. If the `constParams` to use in
90 /// the type are not given, the StructType will use `this->getConstParamsAttr()`.
91 StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {});
92
93 /// Gets the FieldDefOp that defines the field in this
94 /// structure with the given name, if present.
95 FieldDefOp getFieldDef(::mlir::StringAttr fieldName);
96
97 /// Get all FieldDefOp in this structure.
98 ::std::vector<FieldDefOp> getFieldDefs();
99
100 /// Returns wether the struct defines fields marked as columns.
101 ::mlir::LogicalResult hasColumns() {
102 return ::mlir::success(::llvm::any_of(getFieldDefs(), [](FieldDefOp fdOp) {
103 return fdOp.getColumn();
104 }));
105 }
106
107 /// Gets the FuncDefOp that defines the compute function in this structure, if present.
108 ::llzk::function::FuncDefOp getComputeFuncOp();
109
110 /// Gets the FuncDefOp that defines the constrain function in this structure, if present.
111 ::llzk::function::FuncDefOp getConstrainFuncOp();
112
113 /// Generate header string, in the same format as the assemblyFormat
114 ::std::string getHeaderString();
115
116 /// Return `true` iff this StructDefOp has a parameter with the given name
117 bool hasParamNamed(::mlir::StringAttr find);
118 inline bool hasParamNamed(::mlir::FlatSymbolRefAttr find) {
119 return hasParamNamed(find.getRootReference());
120 }
121
122 //===------------------------------------------------------------------===//
123 // Utility Methods
124 //===------------------------------------------------------------------===//
125
126 /// Return the full name for this struct from the root module, including
127 /// any surrounding module scopes.
128 ::mlir::SymbolRefAttr getFullyQualifiedName();
129
130 /// Return `true` iff this StructDefOp is named "Main".
131 bool isMainComponent();
132 }];
133
134 let hasRegionVerifier = 1;
135}
136
137def LLZK_FieldDefOp
138 : StructDialectOp<
139 "field", [HasParent<"::llzk::component::StructDefOp">,
140 DeclareOpInterfaceMethods<SymbolUserOpInterface>, Symbol]> {
141 let summary = "struct field definition";
142 let description = [{
143 This operation describes a field in a struct/component.
144
145 Example:
146
147 ```llzk
148 struct.field @f1 : !felt.type
149 struct.field @f2 : !felt.type {llzk.pub}
150 ```
151 }];
152
153 let arguments = (ins SymbolNameAttr:$sym_name, TypeAttrOf<AnyLLZKType>:$type,
154 UnitAttr:$column);
155
156 // Define builders manually to avoid the default ones that have extra
157 // TypeRange parameters that must always be empty.
158 let skipDefaultBuilders = 1;
159 let builders =
160 [OpBuilder<(ins "::mlir::StringAttr":$sym_name, "::mlir::TypeAttr":$type,
161 CArg<"bool", "false">:$isColumn)>,
162 OpBuilder<(ins "::llvm::StringRef":$sym_name, "::mlir::Type":$type,
163 CArg<"bool", "false">:$isColumn)>,
164 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
165 "::mlir::ValueRange":$operands,
166 "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
167 CArg<"bool", "false">:$isColumn)>,
168 // Simpler version since 'resultTypes' and 'operands' must be empty
169 OpBuilder<
170 (ins "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
171 CArg<"bool", "false">:$isColumn),
172 [{ build($_builder, $_state, {}, {}, attributes, isColumn); }]>];
173
174 let assemblyFormat = [{ $sym_name `:` $type attr-dict }];
175
176 let extraClassDeclaration = [{
177 inline bool hasPublicAttr() { return getOperation()->hasAttr(llzk::PublicAttr::name); }
178 void setPublicAttr(bool newValue = true);
179 }];
180}
181
182class FieldRefOpBase<string mnemonic, list<Trait> traits = []>
183 : StructDialectOp<
184 mnemonic, traits#[DeclareOpInterfaceMethods<FieldRefOpInterface>,
185 DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
186 bit isRead = ?; // read(1) vs write(0) ops
187 let extraClassDeclaration = [{
188 /// Gets the definition for the `field` referenced in this op.
189 inline ::mlir::FailureOr<SymbolLookupResult<FieldDefOp>> getFieldDefOp(::mlir::SymbolTableCollection &tables) {
190 return ::llvm::cast<FieldRefOpInterface>(getOperation()).getFieldDefOp(tables);
191 }
192 }];
193 let extraClassDefinition = [{
194 /// Return `true` if the op is a read, `false` if it's a write.
195 bool $cppClass::isRead() {
196 return }]#!if(isRead, "true", "false")#[{;
197 }
198 }];
199}
200
201def LLZK_FieldReadOp
202 : FieldRefOpBase<"readf", [VerifySizesForMultiAffineOps<1>]> {
203 let summary = "read value of a struct field";
204 let description = [{
205 This operation reads the value of a named field in a struct/component.
206
207 The value can be read from the signals table, in which case it can be
208 offset by a constant value. A negative value represents reading a value
209 backwards and a positive value represents reading a value forward.
210 Only fields marked as columns can be read in this manner.
211 }];
212 let isRead = 1;
213
214 let arguments = (ins LLZK_StructType:$component,
215 FlatSymbolRefAttr:$field_name,
216 OptionalAttr<AnyAttrOf<[SymbolRefAttr, IndexAttr,
217 AffineMapAttr]>>:$tableOffset,
218 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
219 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
220 DenseI32ArrayAttr:$mapOpGroupSizes);
221 let results = (outs AnyLLZKType:$val);
222
223 // Define builders manually so inference of operand layout attributes is not
224 // circumvented.
225 let skipDefaultBuilders = 1;
226 let builders =
227 [OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
228 "::mlir::StringAttr":$field)>,
229 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
230 "::mlir::StringAttr":$field, "::mlir::Attribute":$dist,
231 "::mlir::ValueRange":$mapOperands,
232 "std::optional<int32_t>":$numDims)>,
233 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
234 "::mlir::StringAttr":$field,
235 "::mlir::SymbolRefAttr":$dist),
236 [{
237 build($_builder, $_state, resultType, component, field, dist, ::mlir::ValueRange(), std::nullopt);
238 }]>,
239 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
240 "::mlir::StringAttr":$field, "::mlir::IntegerAttr":$dist),
241 [{
242 build($_builder, $_state, resultType, component, field, dist, ::mlir::ValueRange(), std::nullopt);
243 }]>,
244 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
245 "::mlir::ValueRange":$operands,
246 "::mlir::ArrayRef<::mlir::NamedAttribute>":$attrs)>];
247
248 let assemblyFormat = [{
249 $component `[` $field_name `]`
250 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
251 `:` type($component) `,` type($val)
252 attr-dict
253 }];
254
255 let hasVerifier = 1;
256}
257
258def LLZK_FieldWriteOp : FieldRefOpBase<"writef", [WitnessGen]> {
259 let summary = "write value to a struct field";
260 let description = [{
261 This operation writes a value to a named field in a struct/component.
262 }];
263 let isRead = 1;
264
265 let arguments = (ins LLZK_StructType:$component,
266 FlatSymbolRefAttr:$field_name, AnyLLZKType:$val);
267
268 let assemblyFormat = [{
269 $component `[` $field_name `]` `=` $val `:` type($component) `,` type($val) attr-dict
270 }];
271}
272
273def LLZK_CreateStructOp
274 : StructDialectOp<"new", [DeclareOpInterfaceMethods<
275 OpAsmOpInterface, ["getAsmResultNames"]>,
276 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
277 WitnessGen,
278]> {
279 let summary = "create a new struct";
280 let description = [{
281 This operation creates a new, uninitialized instance of a struct.
282
283 Example:
284
285 ```llzk
286 %self = struct.new : !struct.type<@Reg>
287 ```
288 }];
289
290 let results = (outs LLZK_StructType:$result);
291
292 let assemblyFormat = [{ `:` type($result) attr-dict }];
293}
294
295#endif // LLZK_STRUCT_OPS