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, Type resultType,
33 list<Trait> traits = []>
34 : BinaryOpBase<FeltDialect, mnemonic, resultType,
35 traits#[DeclareOpInterfaceMethods<FeltBinaryOpInterface>]>;
37class FeltDialectUnaryOp<string mnemonic, Type resultType,
38 list<Trait> traits = []>
39 : UnaryOpBase<FeltDialect, mnemonic, resultType, traits>;
41//===------------------------------------------------------------------===//
43//===------------------------------------------------------------------===//
45def LLZK_FeltConstantOp
46 : FeltDialectOp<"const", [ConstantLike, Pure,
47 DeclareOpInterfaceMethods<
48 OpAsmOpInterface, ["getAsmResultNames"]>]> {
49 let summary = "field element constant";
51 This operation produces a felt-typed SSA value holding an integer constant.
60 let arguments = (ins LLZK_FeltConstAttr:$value);
61 let results = (outs LLZK_FeltType:$result);
62 let assemblyFormat = [{ $value attr-dict }];
66//===------------------------------------------------------------------===//
68//===------------------------------------------------------------------===//
70def LLZK_AddFeltOp : FeltDialectBinaryOp<"add", LLZK_FeltType, [Commutative]> {
71 let summary = "addition operator for field elements";
72 let description = [{}];
75def LLZK_SubFeltOp : FeltDialectBinaryOp<"sub", LLZK_FeltType> {
76 let summary = "subtraction operator for field elements";
77 let description = [{}];
80def LLZK_MulFeltOp : FeltDialectBinaryOp<"mul", LLZK_FeltType, [Commutative]> {
81 let summary = "multiplication operator for field elements";
82 let description = [{}];
86 : FeltDialectBinaryOp<"pow", LLZK_FeltType, [NotFieldNative]> {
87 let summary = "exponentiation operator for field elements";
90 Raises a field element to the power of an exponent.
93 %result = felt.pow %base, %exponent
99def LLZK_DivFeltOp : FeltDialectBinaryOp<"div", LLZK_FeltType> {
100 let summary = "division operator for field elements";
101 let description = [{}];
104def LLZK_UnsignedIntDivFeltOp
105 : FeltDialectBinaryOp<"uintdiv", LLZK_FeltType, [NotFieldNative]> {
106 let summary = "unsigned integer division operator for field elements";
108 Treats the operands as if they were unsigned integers with bitwidth
109 equal to that of the prime modulus and performs division rounding towards zero.
113def LLZK_SignedIntDivFeltOp
114 : FeltDialectBinaryOp<"sintdiv", LLZK_FeltType, [NotFieldNative]> {
115 let summary = "signed integer division operator for field elements";
117 Treats the operands as if they were signed integers with bitwidth
118 equal to that of the prime modulus (no additional sign bit is added)
119 and performs division rounding towards zero.
121 The signed integer representation of felt `f` in prime field with modulus
122 `p` follows the following formula:
124 signed_int(f) = f if 0 <= f < p/2 + 1
125 "p/2" here is unsigned integer division rounding towards 0
126 signed_int(f) = f-p if p/2 + 1 <= f < p
130def LLZK_UnsignedModFeltOp
131 : FeltDialectBinaryOp<"umod", LLZK_FeltType, [NotFieldNative]> {
133 "unsigned integer modulus/remainder operator for field elements";
135 Computes the remainder that would result from the division operation performed
140def LLZK_SignedModFeltOp
141 : FeltDialectBinaryOp<"smod", LLZK_FeltType, [NotFieldNative]> {
142 let summary = "signed integer modulus/remainder operator for field elements";
144 Computes the remainder that would result from the division operation performed
149def LLZK_NegFeltOp : FeltDialectUnaryOp<"neg", LLZK_FeltType> {
150 let summary = "negation operator for field elements";
151 let description = [{}];
155 : FeltDialectUnaryOp<"inv", LLZK_FeltType, [NotFieldNative]> {
156 let summary = "inverse operator for field elements";
157 let description = [{}];
161 : FeltDialectBinaryOp<"bit_and",
162 LLZK_FeltType, [NotFieldNative, Commutative]> {
163 let summary = "bitwise AND operator for field elements";
164 let description = [{}];
168 : FeltDialectBinaryOp<"bit_or",
169 LLZK_FeltType, [NotFieldNative, Commutative]> {
170 let summary = "bitwise OR operator for field elements";
171 let description = [{}];
175 : FeltDialectBinaryOp<"bit_xor",
176 LLZK_FeltType, [NotFieldNative, Commutative]> {
177 let summary = "bitwise XOR operator for field elements";
178 let description = [{}];
182 : FeltDialectUnaryOp<"bit_not", LLZK_FeltType, [NotFieldNative]> {
183 let summary = "integer complement (bitwise-not) operator for field elements";
185 Treats the operand as an integer with a bitwidth equal to the bitwidth
186 of the prime field's modulus and compute the one's complement of the integer.
187 The result is converted back to a field element by applying the prime modulus.
192 : FeltDialectBinaryOp<"shl", LLZK_FeltType, [NotFieldNative]> {
193 let summary = "left shift operator for field elements";
194 let description = [{}];
198 : FeltDialectBinaryOp<"shr", LLZK_FeltType, [NotFieldNative]> {
199 let summary = "right shift operator for field elements";
200 let description = [{}];
203#endif // LLZK_FELT_OPS