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 inline StructType getType(::std::optional<::mlir::ArrayAttr> constParams = {}) const {
93 return const_cast<StructDefOp*>(this)->getType(constParams);
94 }
95
96 /// Gets the FieldDefOp that defines the field in this
97 /// structure with the given name, if present.
98 FieldDefOp getFieldDef(::mlir::StringAttr fieldName);
99
100 /// Get all FieldDefOp in this structure.
101 ::std::vector<FieldDefOp> getFieldDefs();
102
103 /// Returns wether the struct defines fields marked as columns.
104 ::mlir::LogicalResult hasColumns() {
105 return ::mlir::success(::llvm::any_of(getFieldDefs(), [](FieldDefOp fdOp) {
106 return fdOp.getColumn();
107 }));
108 }
109
110 /// Gets the FuncDefOp that defines the compute function in this structure, if present.
111 ::llzk::function::FuncDefOp getComputeFuncOp();
112
113 /// Gets the FuncDefOp that defines the constrain function in this structure, if present.
114 ::llzk::function::FuncDefOp getConstrainFuncOp();
115
116 /// Generate header string, in the same format as the assemblyFormat
117 ::std::string getHeaderString();
118
119 /// Return `false` iff `getConstParamsAttr()` returns `nullptr`
120 bool hasConstParamsAttr() { return getProperties().const_params != nullptr; };
121
122 /// Return `true` iff this StructDefOp has a parameter with the given name
123 bool hasParamNamed(::mlir::StringAttr find);
124 inline bool hasParamNamed(::mlir::FlatSymbolRefAttr find) {
125 return hasParamNamed(find.getRootReference());
126 }
127
128 //===------------------------------------------------------------------===//
129 // Utility Methods
130 //===------------------------------------------------------------------===//
131
132 /// Return the full name for this struct from the root module, including
133 /// any surrounding module scopes.
134 ::mlir::SymbolRefAttr getFullyQualifiedName();
135
136 /// Return `true` iff this StructDefOp is named "Main".
137 bool isMainComponent();
138 }];
139
140 let hasRegionVerifier = 1;
141}
142
143def LLZK_FieldDefOp
144 : StructDialectOp<
145 "field", [HasParent<"::llzk::component::StructDefOp">,
146 DeclareOpInterfaceMethods<SymbolUserOpInterface>, Symbol]> {
147 let summary = "struct field definition";
148 let description = [{
149 This operation describes a field in a struct/component.
150
151 Example:
152
153 ```llzk
154 struct.field @f1 : !felt.type
155 struct.field @f2 : !felt.type {llzk.pub}
156 ```
157 }];
158
159 let arguments = (ins SymbolNameAttr:$sym_name, TypeAttrOf<AnyLLZKType>:$type,
160 UnitAttr:$column);
161
162 // Define builders manually to avoid the default ones that have extra
163 // TypeRange parameters that must always be empty.
164 let skipDefaultBuilders = 1;
165 let builders =
166 [OpBuilder<(ins "::mlir::StringAttr":$sym_name, "::mlir::TypeAttr":$type,
167 CArg<"bool", "false">:$isColumn)>,
168 OpBuilder<(ins "::llvm::StringRef":$sym_name, "::mlir::Type":$type,
169 CArg<"bool", "false">:$isColumn)>,
170 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
171 "::mlir::ValueRange":$operands,
172 "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
173 CArg<"bool", "false">:$isColumn)>,
174 // Simpler version since 'resultTypes' and 'operands' must be empty
175 OpBuilder<
176 (ins "::llvm::ArrayRef<::mlir::NamedAttribute>":$attributes,
177 CArg<"bool", "false">:$isColumn),
178 [{ build($_builder, $_state, {}, {}, attributes, isColumn); }]>];
179
180 let assemblyFormat = [{ $sym_name `:` $type attr-dict }];
181
182 let extraClassDeclaration = [{
183 inline bool hasPublicAttr() { return getOperation()->hasAttr(llzk::PublicAttr::name); }
184 void setPublicAttr(bool newValue = true);
185 }];
186}
187
188class FieldRefOpBase<string mnemonic, list<Trait> traits = []>
189 : StructDialectOp<
190 mnemonic, traits#[DeclareOpInterfaceMethods<FieldRefOpInterface>,
191 DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
192 bit isRead = ?; // read(1) vs write(0) ops
193 let extraClassDeclaration = [{
194 /// Gets the definition for the `field` referenced in this op.
195 inline ::mlir::FailureOr<SymbolLookupResult<FieldDefOp>> getFieldDefOp(::mlir::SymbolTableCollection &tables) {
196 return ::llvm::cast<FieldRefOpInterface>(getOperation()).getFieldDefOp(tables);
197 }
198 }];
199 let extraClassDefinition = [{
200 /// Return `true` if the op is a read, `false` if it's a write.
201 bool $cppClass::isRead() {
202 return }]#!if(isRead, "true", "false")#[{;
203 }
204 }];
205}
206
207def LLZK_FieldReadOp
208 : FieldRefOpBase<"readf", [VerifySizesForMultiAffineOps<1>]> {
209 let summary = "read value of a struct field";
210 let description = [{
211 This operation reads the value of a named field in a struct/component.
212
213 The value can be read from the signals table, in which case it can be
214 offset by a constant value. A negative value represents reading a value
215 backwards and a positive value represents reading a value forward.
216 Only fields marked as columns can be read in this manner.
217 }];
218 let isRead = 1;
219
220 let arguments = (ins LLZK_StructType:$component,
221 FlatSymbolRefAttr:$field_name,
222 OptionalAttr<AnyAttrOf<[SymbolRefAttr, IndexAttr,
223 AffineMapAttr]>>:$tableOffset,
224 VariadicOfVariadic<Index, "mapOpGroupSizes">:$mapOperands,
225 DefaultValuedAttr<DenseI32ArrayAttr, "{}">:$numDimsPerMap,
226 DenseI32ArrayAttr:$mapOpGroupSizes);
227 let results = (outs AnyLLZKType:$val);
228
229 // Define builders manually so inference of operand layout attributes is not
230 // circumvented.
231 let skipDefaultBuilders = 1;
232 let builders =
233 [OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
234 "::mlir::StringAttr":$field)>,
235 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
236 "::mlir::StringAttr":$field, "::mlir::Attribute":$dist,
237 "::mlir::ValueRange":$mapOperands,
238 "std::optional<int32_t>":$numDims)>,
239 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
240 "::mlir::StringAttr":$field,
241 "::mlir::SymbolRefAttr":$dist),
242 [{
243 build($_builder, $_state, resultType, component, field, dist, ::mlir::ValueRange(), std::nullopt);
244 }]>,
245 OpBuilder<(ins "::mlir::Type":$resultType, "::mlir::Value":$component,
246 "::mlir::StringAttr":$field, "::mlir::IntegerAttr":$dist),
247 [{
248 build($_builder, $_state, resultType, component, field, dist, ::mlir::ValueRange(), std::nullopt);
249 }]>,
250 OpBuilder<(ins "::mlir::TypeRange":$resultTypes,
251 "::mlir::ValueRange":$operands,
252 "::mlir::ArrayRef<::mlir::NamedAttribute>":$attrs)>];
253
254 let assemblyFormat = [{
255 $component `[` $field_name `]`
256 ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
257 `:` type($component) `,` type($val)
258 attr-dict
259 }];
260
261 let hasVerifier = 1;
262}
263
264def LLZK_FieldWriteOp : FieldRefOpBase<"writef", [WitnessGen]> {
265 let summary = "write value to a struct field";
266 let description = [{
267 This operation writes a value to a named field in a struct/component.
268 }];
269 let isRead = 0;
270
271 let arguments = (ins LLZK_StructType:$component,
272 FlatSymbolRefAttr:$field_name, AnyLLZKType:$val);
273
274 let assemblyFormat = [{
275 $component `[` $field_name `]` `=` $val `:` type($component) `,` type($val) attr-dict
276 }];
277}
278
279def LLZK_CreateStructOp
280 : StructDialectOp<"new", [DeclareOpInterfaceMethods<
281 OpAsmOpInterface, ["getAsmResultNames"]>,
282 DeclareOpInterfaceMethods<SymbolUserOpInterface>,
283 WitnessGen,
284]> {
285 let summary = "create a new struct";
286 let description = [{
287 This operation creates a new, uninitialized instance of a struct.
288
289 Example:
290
291 ```llzk
292 %self = struct.new : !struct.type<@Reg>
293 ```
294 }];
295
296 let results = (outs LLZK_StructType:$result);
297
298 let assemblyFormat = [{ `:` type($result) attr-dict }];
299}
300
301#endif // LLZK_STRUCT_OPS