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// SPDX-License-Identifier: Apache-2.0
8//===----------------------------------------------------------------------===//
13include "llzk/Dialect/Felt/IR/Dialect.td"
14include "llzk/Dialect/Felt/IR/Types.td"
15include "llzk/Dialect/Felt/IR/Attrs.td"
16include "llzk/Dialect/Function/IR/OpTraits.td"
17include "llzk/Dialect/Shared/OpsBase.td"
18include "llzk/Dialect/Felt/IR/OpInterfaces.td"
20include "mlir/IR/OpAsmInterface.td"
21include "mlir/IR/OpBase.td"
22include "mlir/IR/SymbolInterfaces.td"
23include "mlir/Interfaces/SideEffectInterfaces.td"
25//===------------------------------------------------------------------===//
27//===------------------------------------------------------------------===//
29class FeltDialectOp<string mnemonic, list<Trait> traits = []>
30 : Op<FeltDialect, mnemonic, traits>;
32class FeltDialectBinaryOp<string mnemonic, list<Trait> traits = []>
33 : BinaryOpBase<FeltDialect, mnemonic, LLZK_FeltType,
34 traits#[TypesUnify<"lhs", "rhs">,
35 DeclareOpInterfaceMethods<FeltBinaryOpInterface>,
36 InferTypeOpAdaptorWithIsCompatible]> {
37 // Allow any type to avoid building default felt for the result type, we
38 // employ our own inference below.
39 let results = (outs AnyLLZKType:$result);
42 let extraClassDefinition = [{
43 ::llvm::LogicalResult $cppClass::inferReturnTypes(
44 mlir::MLIRContext *context, std::optional<mlir::Location> loc, Adaptor adaptor,
45 llvm::SmallVectorImpl<mlir::Type> &inferred
48 auto value = adaptor.getLhs();
49 inferred[0] = value ? value.getType() : FeltType::get(context, mlir::StringAttr());
50 return mlir::success();
53 bool $cppClass::isCompatibleReturnTypes(mlir::TypeRange l, mlir::TypeRange r) {
59class FeltDialectUnaryOp<string mnemonic, list<Trait> traits = []>
60 : UnaryOpBase<FeltDialect, mnemonic, LLZK_FeltType,
61 traits#[InferTypeOpAdaptorWithIsCompatible]> {
62 // Allow any type to avoid building default felt for the result type, we
63 // employ our own inference below.
64 let results = (outs AnyLLZKType:$result);
67 let extraClassDefinition = [{
68 ::llvm::LogicalResult $cppClass::inferReturnTypes(
69 mlir::MLIRContext *context, std::optional<mlir::Location> loc, Adaptor adaptor,
70 llvm::SmallVectorImpl<mlir::Type> &inferred
73 auto value = adaptor.getOperand();
74 inferred[0] = value ? value.getType() : FeltType::get(context, mlir::StringAttr());
75 return mlir::success();
78 bool $cppClass::isCompatibleReturnTypes(mlir::TypeRange l, mlir::TypeRange r) {
84//===------------------------------------------------------------------===//
86//===------------------------------------------------------------------===//
88def LLZK_FeltConstantOp
89 : FeltDialectOp<"const", [ConstantLike, Pure,
90 DeclareOpInterfaceMethods<
91 OpAsmOpInterface, ["getAsmResultNames"]>,
92 TypeUnifyWithResult<"value">,
93 InferTypeOpAdaptorWithIsCompatible]> {
94 let summary = "field element constant";
96 This operation produces a felt-typed SSA value holding an integer constant.
102 %0 = felt.const 99 <"bn254">
106 let arguments = (ins LLZK_FeltConstAttr:$value);
107 let results = (outs AnyLLZKType:$result);
108 let assemblyFormat = [{ $value attr-dict }];
110 let extraClassDeclaration = [{
111 auto getValueAPInt() -> ::llvm::APInt { return getValue().getValue(); }
113 auto tryGetZExtValue() -> std::optional<uint64_t> { return getValueAPInt().tryZExtValue(); }
117//===------------------------------------------------------------------===//
119//===------------------------------------------------------------------===//
121def LLZK_AddFeltOp : FeltDialectBinaryOp<"add", [Commutative]> {
122 let summary = "addition operator for field elements";
123 let description = [{}];
126def LLZK_SubFeltOp : FeltDialectBinaryOp<"sub"> {
127 let summary = "subtraction operator for field elements";
128 let description = [{}];
131def LLZK_MulFeltOp : FeltDialectBinaryOp<"mul", [Commutative]> {
132 let summary = "multiplication operator for field elements";
133 let description = [{}];
136def LLZK_PowFeltOp : FeltDialectBinaryOp<"pow", [NotFieldNative]> {
137 let summary = "exponentiation operator for field elements";
140 Raises a field element to the power of an exponent.
143 %result = felt.pow %base, %exponent
149def LLZK_DivFeltOp : FeltDialectBinaryOp<"div"> {
150 let summary = "field-division operator for field elements";
152 Performs finite-field division by multiplying the dividend by the
153 multiplicative inverse of the divisor. For a non-zero divisor `b`,
154 `felt.div %a, %b` computes `%a * inv(%b)` modulo the field prime of the result
157 The divisor must be non-zero.
159 This is not integer division. Use `felt.uintdiv` or `felt.sintdiv` when the
160 operands should be interpreted as integers.
164def LLZK_UnsignedIntDivFeltOp
165 : FeltDialectBinaryOp<"uintdiv", [NotFieldNative]> {
166 let summary = "unsigned integer division operator for field elements";
168 Treats the operands as if they were unsigned integers with bitwidth
169 equal to that of the prime modulus and performs division rounding towards zero.
173def LLZK_SignedIntDivFeltOp : FeltDialectBinaryOp<"sintdiv", [NotFieldNative]> {
174 let summary = "signed integer division operator for field elements";
176 Treats the operands as if they were signed integers with bitwidth
177 equal to that of the prime modulus (no additional sign bit is added)
178 and performs division rounding towards zero.
180 The signed integer representation of felt `f` in prime field with modulus
181 `p` follows the following formula:
183 signed_int(f) = f if 0 <= f < p/2 + 1
184 "p/2" here is unsigned integer division rounding towards 0
185 signed_int(f) = f-p if p/2 + 1 <= f < p
189def LLZK_UnsignedModFeltOp : FeltDialectBinaryOp<"umod", [NotFieldNative]> {
191 "unsigned integer modulus/remainder operator for field elements";
193 Computes the remainder that would result from the division operation performed
198def LLZK_SignedModFeltOp : FeltDialectBinaryOp<"smod", [NotFieldNative]> {
199 let summary = "signed integer modulus/remainder operator for field elements";
201 Computes the remainder that would result from the division operation performed
206def LLZK_NegFeltOp : FeltDialectUnaryOp<"neg"> {
207 let summary = "negation operator for field elements";
208 let description = [{}];
211def LLZK_InvFeltOp : FeltDialectUnaryOp<"inv", [NotFieldNative]> {
212 let summary = "inverse operator for field elements";
213 let description = [{}];
217 : FeltDialectBinaryOp<"bit_and", [NotFieldNative, Commutative]> {
218 let summary = "bitwise AND operator for field elements";
219 let description = [{}];
223 : FeltDialectBinaryOp<"bit_or", [NotFieldNative, Commutative]> {
224 let summary = "bitwise OR operator for field elements";
225 let description = [{}];
229 : FeltDialectBinaryOp<"bit_xor", [NotFieldNative, Commutative]> {
230 let summary = "bitwise XOR operator for field elements";
231 let description = [{}];
234def LLZK_NotFeltOp : FeltDialectUnaryOp<"bit_not", [NotFieldNative]> {
235 let summary = "integer complement (bitwise-not) operator for field elements";
237 Treats the operand as an integer with a bitwidth equal to the bitwidth
238 of the prime field's modulus and compute the one's complement of the integer.
239 The result is converted back to a field element by applying the prime modulus.
243def LLZK_ShlFeltOp : FeltDialectBinaryOp<"shl", [NotFieldNative]> {
244 let summary = "left shift operator for field elements";
246 Treats both operands as unsigned integer representatives of field elements.
247 `felt.shl %a, %b` computes `%a * 2^%b`, then converts the result back to a
248 field element by reducing modulo the field prime.
252def LLZK_ShrFeltOp : FeltDialectBinaryOp<"shr", [NotFieldNative]> {
253 let summary = "right shift operator for field elements";
255 Treats both operands as unsigned integer representatives of field elements.
256 `felt.shr %a, %b` computes `%a / 2^%b` using unsigned integer division
257 rounding towards zero, then converts the result back to a field element.
261#endif // LLZK_FELT_OPS