Attrs.td

Go to the documentation of this file.

//===-- Attrs.td -------------------------------------------*- tablegen -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2025 Veridise Inc.
// SPDX-License-Identifier: Apache-2.0
//
//===----------------------------------------------------------------------===//
 
#ifndef LLZK_FELT_ATTRS
#define LLZK_FELT_ATTRS
 
include "llzk/Dialect/Felt/IR/Dialect.td"
include "llzk/Dialect/LLZK/IR/AttributeHelper.td"
 
include "mlir/IR/AttrTypeBase.td"
include "mlir/IR/BuiltinAttributeInterfaces.td"
 
def LLZK_FeltConstAttr
    : AttrDef<FeltDialect, "FeltConst", [TypedAttrInterface]> {
  let mnemonic = "const";
  let summary = "finite field element";
  let description = [{
    A felt attribute stores an exact signed integer literal and its field type.
 
    For a specified field with prime modulus `p`, the attribute denotes
    `rawValue mod p`, regardless of its stored representation (i.e. the raw
    value). Use `getReducedValue()` to obtain the representative in `[0, p)`
    when the type specifies a field; gives `std::nullopt` otherwise.
 
    Builders accepting ArrayRef<uint64_t> decode 64-bit parts in
    least-significant-first order as a two's-complement signed integer. The
    most significant bit of the last part is the sign bit; an empty array is
    zero. Callers should append a zero part to represent a positive value whose
    highest data bit would otherwise be interpreted as the sign bit.
  }];
 
  let parameters =
      (ins DynamicAPIntParameter<"The unreduced felt constant value">:$rawValue,
          DefaultValuedParameter<"FeltType", "FeltType::get($_ctxt)">:$type);
 
  let hasCustomAssemblyFormat = 1;
 
  let builders =
      [AttrBuilder<
           (ins "const ::llvm::DynamicAPInt &":$rawValue, "FeltType":$ty),
           [{ return $_get(context, ::llzk::DynamicAPIntValue(rawValue), ty); }]>,
       AttrBuilder<
           (ins "const ::llvm::DynamicAPInt &":$rawValue),
           [{ return get(context, rawValue, FeltType::get(context)); }]>,
       AttrBuilder<
           (ins "const ::llvm::DynamicAPInt &":$rawValue,
               "::llvm::StringRef":$fieldName),
           [{ return get(context, rawValue, FeltType::get(context, fieldName)); }]>,
       AttrBuilder<
           (ins "::llvm::ArrayRef<uint64_t>":$parts, "FeltType":$ty),
           [{ return get(context, ::llzk::toSignedDynamicAPInt(parts), ty); }]>,
       AttrBuilder<
           (ins "::llvm::ArrayRef<uint64_t>":$parts),
           [{ return get(context, ::llzk::toSignedDynamicAPInt(parts)); }]>,
       AttrBuilder<
           (ins "::llvm::ArrayRef<uint64_t>":$parts,
               "::llvm::StringRef":$fieldName),
           [{ return get(context, ::llzk::toSignedDynamicAPInt(parts), fieldName); }]>];
 
  let extraClassDeclaration = [{
    /// Returns the field name from the stored FeltType, or a null StringAttr
    /// if no type is stored.
    ::mlir::StringAttr getFieldName() const;
 
    /// If the type specifies a field, returns the field representative in `[0, p)`
    /// for the signed raw value; gives `std::nullopt` otherwise.
    std::optional<::llvm::DynamicAPInt> getReducedValue() const;
 
    /// If the type specifies a field, returns `getReducedValue()`; otherwise `getRawValue()`.
    /// Use getReducedValue() when folding requires a known field representative.
    ::llvm::DynamicAPInt getReducedValueOrRaw() const;
  }];
}
 
def LLZK_FieldSpecAttr : AttrDef<FeltDialect, "FieldSpec"> {
  let mnemonic = "field";
  let summary = "prime field specification";
  let description = [{
    A specification of a prime field for use by felt types.
    Builders accepting ArrayRef<uint64_t> decode 64-bit parts in
    least-significant-first order as a two's-complement signed integer. The
    most significant bit of the last part is the sign bit; an empty array is
    zero. Callers should append a zero part to ensure the highest data bit
    (i.e. the sign bit) is zero since the modulus must be positive. A modulus
    below two is invalid: `getChecked()` emits a diagnostic and returns a null
    attribute, while `get()` requires a valid modulus.
 
    These specifications are provided in the `llzk.fields` attribute on the root
    module as either a single element or a flat array, for example:
 
        module attributes {llzk.lang, llzk.fields = field<foo, 7> { ... }
        module attributes {llzk.lang, llzk.fields = [field<>]} { ... }
 
    Specifications should not be provided for built-in fields, which include:
    - babybear
    - bn128/bn254
    - goldilocks
    - grumpkin
    - koalabear
    - mersenne31
  }];
 
  let parameters = (ins "::mlir::StringAttr":$fieldName,
      DynamicAPIntParameter<"The prime modulus">:$prime);
 
  // Format is [{ `<` $fieldName `,` $prime `>` }], but with custom parsing
  // to enable caching of the Field object definition.
  let hasCustomAssemblyFormat = 1;
 
  let builders =
      [AttrBuilder<
           (ins "::mlir::StringAttr":$fieldName,
               "const ::llvm::DynamicAPInt &":$prime),
           [{ return $_get(context, fieldName, ::llzk::DynamicAPIntValue(prime)); }]>,
       AttrBuilder<(ins "::mlir::StringAttr":$fieldName,
                       "::llvm::ArrayRef<uint64_t>":$parts),
                   [{ return $_get(context, fieldName,
                        ::llzk::DynamicAPIntValue(::llzk::toSignedDynamicAPInt(parts))); }]>,
       AttrBuilder<
           (ins "::llvm::StringRef":$fieldName,
               "::llvm::ArrayRef<uint64_t>":$parts),
           [{ return $_get(context, ::mlir::StringAttr::get(context, fieldName),
                        ::llzk::DynamicAPIntValue(::llzk::toSignedDynamicAPInt(parts))); }]>];
  let genVerifyDecl = 1;
}
 
#endif // LLZK_FELT_ATTRS