'array' Dialect
- Operations
- Types
  - ArrayType
    - Parameters:
'bool' Dialect
'cast' Dialect
'constrain' Dialect
- Operations
  - constrain.eq (llzk::constrain::EmitEqualityOp)
    - Operands:
  - constrain.in (llzk::constrain::EmitContainmentOp)
    - Operands:
'felt' Dialect
'function' Dialect
- Operations
'global' Dialect
- Operations
'include' Dialect
- Operations
  - include.from (llzk::include::IncludeOp)
    - Attributes:
'llzk' Dialect
- Operations
  - llzk.nondet (llzk::NonDetOp)
    - Results:
- Attributes
  - LoopBoundsAttr
    - Parameters:
  - PublicAttr
'pod' Dialect
'poly' Dialect
- Operations
- Types
  - TypeVarType
    - Parameters:
'string' Dialect
- Operations
  - string.new (llzk::string::LitStringOp)
    - Attributes:
    - Results:
- Types
  - StringType
'struct' Dialect
- Operations
- Types
  - StructType
    - Parameters:

'array' Dialect

LLZK array operations.

Operations

array.extract (::llzk::array::ExtractArrayOp)

Read subarray from a multi-dimensional array

Syntax:

operation ::= `array.extract` $arr_ref `[` $indices `]` `:` type($arr_ref) attr-dict

This operation takes an N-dimensional array and K indices and extracts the (N-K)-dimensional array by applying the given indices to the first K dimensions of the array. Error if K >= N. Use array.read instead if K == N.

Extracting a 1-D array from 3-D array by selecting the index of 2 dimensions:

%i = arith.constant 1 : index
%0 = array.new ... : !array.type<3,10,15 x !felt.type>
%1 = array.extract %0[%i,%i] : !array.type<3,10,15 x !felt.type>, !array.type<15 x !felt.type>

Extracting 1-D arrays for subcomponents:

scf.for %iv = %lb to %up step %step {
  %p = array.extract %in[%iv] : !array.type<@N,2 x !felt.type>
  %c = array.read %a[%iv] : !array.type<@N x !struct.type<@SubC>>, !struct.type<@SubC>
  function.call @SubC::@constrain(%c, %p) : (!struct.type<@SubC>, !array.type<2 x !felt.type>) -> ()
}

Traits: InferTypeOpAdaptor

Interfaces: ArrayAccessOpInterface, ArrayRefOpInterface, InferTypeOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
arr_ref	n-dimensional array
indices	variadic of index

Results:

Result	Description
result	n-dimensional array

array.insert (::llzk::array::InsertArrayOp)

Write subarray into a multi-dimensional array

Syntax:

operation ::= `array.insert` $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict

This operation takes an N-dimensional array, K indices, and an (N+K)-dimensional array and inserts the N-dimensional array into the (N+K)-dimensional array at the position specified by applying the given indices to the first K dimensions of the (N+K)-dimensional array. Use array.write instead if N == 0 (LLZK array type must have at least 1 dimension so a 0-dimensional array cannot exist anyway).

Inserting 1-D arrays into a 2-D array:

%c = array.new : !array.type<2,3 x index>
// Array %c is uninitialized [[?, ?, ?], [?, ?, ?]]
%0 = arith.constant 0 : index
%a = array.new %r, %s, %t : !array.type<3 x index>
array.insert %c[%0] = %a : !array.type<2,3 x index>, !array.type<3 x index>
// Array %c is now [[%r, %s, %t], [?, ?, ?]]
%1 = arith.constant 1 : index
%b = array.new %x, %y, %z : !array.type<3 x index>
array.insert %c[%1] = %b : !array.type<2,3 x index>, !array.type<3 x index>
// Array %c is now [[%r, %s, %t], [%x, %y, %z]]

Interfaces: ArrayAccessOpInterface, ArrayRefOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
arr_ref	n-dimensional array
indices	variadic of index
rvalue	n-dimensional array

array.len (::llzk::array::ArrayLengthOp)

Return the length of an array

Syntax:

operation ::= `array.len` $arr_ref `,` $dim `:` type($arr_ref) attr-dict

This operation returns the size of the specified dimension of an array.

Example:

%a = array.new : !array.type<2,3 x !felt.type>
%0 = arith.constant 0 : index
%x = array.len %a, %0 : !array.type<2,3 x !felt.type> // result is 2
%1 = arith.constant 1 : index
%y = array.len %a, %1 : !array.type<2,3 x !felt.type> // result is 3

Traits: AlwaysSpeculatableImplTrait

Interfaces: ArrayRefOpInterface, ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface), SymbolUserOpInterface

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
arr_ref	n-dimensional array
dim	index

Results:

Result	Description
length	index

array.new (::llzk::array::CreateArrayOp)

Create a new array

Syntax:

operation ::= `array.new` ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` ) : ( $elements )?
              `:` type($result)
              `` custom<InferredArrayType>(type($elements), ref($elements), ref(type($result)))
              custom<AttrDictWithWarnings>(attr-dict, prop-dict)

This operation creates a fresh mutable array with the given elements. Even when two array.new operations have identical operands and result types, they are distinct allocations; writes through one result must not affect reads through the other.

The arguments are passed as a flat array but get arranged in row-major order according the shape declared in the type.

Examples:

%0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
 
// Create an array of the specified shape, initialized with the given
// values assigned in row-major order: [[%a, %b], [%c, %d]]
%1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
 
// Create an uninitialized array: [[?, ?], [?, ?], [?, ?]]
%2 = array.new : !array.type<3,2 x !felt.type>

The values used to construct the array must have type that exactly matches the element type of the specified array type. This is true even if a tvar type is used. In other words, cannot mix tvar<@X> with tvar<@Y> or any concrete type. In such a scenario, first create an uninitialized array, as shown in the examples above, and then use array.write to write each element of the array.

Implementation note: This restriction exists due to a combination of: (1) we have chosen to infer the type of $elements from the $result ArrayType, via parseInferredArrayType(), rather than requiring the type of every element be listed in the assembly format and, (2) within the parser for an Op, there is no way to get the Value instances for the operands aside from OpAsmParser::resolveOperands() which requires the type of every operand to be known and ends up comparing the expected to actual type via operator==. Thus, there is no way for this to be successful apart from all elements having the exact type inferred in (1).

Also note that std::equal_to is used in the VariadicTypesMatchWith trait on this Op so that the verifier function mirrors the aforementioned restriction in the parser.

In some cases, the length of an uninitialized array depends on the value of the loop induction variable (i.e., each iteration creates an array with a different size/shape). In that case, an AffineMapAttr can be used to specify the dimension size in the ArrayType and the optional instantiation parameter list of this operation must be used to instatiate all AffineMap used in the array dimensions.

Examples:

// Create an uninitialized array with dimension size defined by AffineMap
#IdxToLen = affine_map<(i) -> (5*i+1)>
%3 = array.new {(%i)} : !array.type<#IdxToLen x index>
 
// Create an uninitialized array with multiple dimensions defined by
//  AffineMap. The list of instantiation parameters are assigned to
//  the AffineMap dimensions left-to-right.
#M1 = affine_map<(i)[c] -> (c+i)>
#M3 = affine_map<(m,n) -> (5*m+n)>
%4 = array.new{(%i)[%c], (%m,%n)} : !array.type<#M1,2,#M3 x i1>

Traits: AttrSizedOperandSegments, VerifySizesForMultiAffineOps<1>

Interfaces: DestructurableAllocationOpInterface, MemoryEffectOpInterface (MemoryEffectOpInterface), OpAsmOpInterface, PromotableAllocationOpInterface, SymbolUserOpInterface

Effects: MemoryEffects::Effect{MemoryEffects::Allocate on llzk::DiscardableAllocationResource}

Attributes:

Attribute	MLIR Type	Description
`numDimsPerMap`	::mlir::DenseI32ArrayAttr	i32 dense array attribute
`mapOpGroupSizes`	::mlir::DenseI32ArrayAttr	i32 dense array attribute

Operands:

Operand	Description
elements	variadic of a valid array element type
mapOperands	variadic of index

Results:

Result	Description
result	n-dimensional array

array.read (::llzk::array::ReadArrayOp)

Read scalar from an array

Syntax:

operation ::= `array.read` $arr_ref `[` $indices `]` `:` type($arr_ref) `,` type($result) attr-dict

This operation copies the value from an array at the specified position. The result is a value copy, not a pointer or alias to the array element's storage.

Example of 1-dimensional array:

%i = arith.constant 0 : index
%0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
// %1 is now equal to %a
%1 = array.read %0[%i] : !array.type<3 x !felt.type>, !felt.type

Example of 3-dimensional array:

%i = arith.constant 0 : index
%j = arith.constant 1 : index
%k = arith.constant 4 : index
%0 = array.new ... : !array.type<3,10,15 x !felt.type>
// %1 is now equal to %a
%1 = array.read %0[%i, %j, %k] : !array.type<3,10,15 x !felt.type>, !felt.type

Traits: InferTypeOpAdaptor

Interfaces: ArrayAccessOpInterface, ArrayRefOpInterface, DestructurableAccessorOpInterface, DiscardableAllocationAccessorOpInterface, InferTypeOpInterface, PromotableMemOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
arr_ref	n-dimensional array
indices	variadic of index

Results:

Result	Description
result	a valid array element type

array.write (::llzk::array::WriteArrayOp)

Write scalar to an array

Syntax:

operation ::= `array.write` $arr_ref `[` $indices `]` `=` $rvalue `:` type($arr_ref) `,` type($rvalue) attr-dict

This operation copies a value into an array at the specified position. It does not create a pointer or alias between the source value and the array element's storage.

Example of 1-dimensional array:

%i = arith.constant 0 : index
%0 = felt.const 42
%1 = array.new %a, %b, %c : !array.type<3 x !felt.type>
// The array now is [%0, %b, %c]
array.write %1[%i] = %0 : !array.type<3 x !felt.type>, !felt.type

Example of 2-dimensional array:

%i = arith.constant 0 : index
%j = arith.constant 0 : index
%0 = felt.const 42
%1 = array.new %a, %b, %c, %d : !array.type<2,2 x !felt.type>
// The array now is [[%0, %b], [%c, %d]]
array.write %1[%i, %j] = %0 : !array.type<2,2 x !felt.type>, !felt.type

Interfaces: ArrayAccessOpInterface, ArrayRefOpInterface, DestructurableAccessorOpInterface, DiscardableAllocationAccessorOpInterface, PromotableMemOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
arr_ref	n-dimensional array
indices	variadic of index
rvalue	a valid array element type

Types

ArrayType

N-dimensional array

Syntax:

!array.type<
  ::mlir::Type,   # elementType
  ::llvm::ArrayRef<::mlir::Attribute>,   # dimensionSizes
  ::llvm::ArrayRef<int64_t>   # shape
>

Array type with a ranked shape and homogeneous element type. It can only be instantiated with the following element types:

Any LLZK type other than an ArrayType (i.e., arrays cannot be nested)
IndexType
NoneType for shape-only arrays with no element payload
Unsigned integers of 1 bit (aka booleans)

The dimensions of the array are specified using a list of attributes, one per dimension. Each attribute must be one of the following:

IntegerAttr (with IndexType), specifying a fixed dimension size
SymbolRefAttr, specifying a dimension size defined by a struct parameter or global constant
AffineMapAttr, specifying a dimension size computed from surrounding loop induction variables

// Example array of 5 by 2 elements of `Felt` type.
!array.type<5,2 x !felt.type>
 
// Example array using a struct parameter for one dimension.
!array.type<5,@A x index>

Parameters:

Parameter	C++ type	Description
elementType	::mlir::Type	Type of all elements within the array.
dimensionSizes	::llvm::ArrayRef<::mlir::Attribute>	List of array dimension size specifiers.
shape	::llvm::ArrayRef<int64_t>	Array shape, for ShapedTypeInterface, computed from $dimensionSizes.

'bool' Dialect

LLZK boolean operations.

Operations

bool.and (::llzk::boolean::AndBoolOp)

Logical AND operator

Syntax:

operation ::= `bool.and` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

This operation computes the logical AND (i.e., conjunction) of two i1 (i.e., boolean) values as an i1 value. The result is 1 if the operation is true and 0 otherwise.

If used in a constraint expression, this operation can be converted to a*b on felt operands.

Traits: AlwaysSpeculatableImplTrait, Commutative, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	1-bit signless integer or type variable
rhs	1-bit signless integer or type variable

Results:

Result	Description
result	1-bit signless integer

bool.assert (::llzk::boolean::AssertOp)

Assertion operation

Syntax:

operation ::= `bool.assert` $condition (`,` $msg^)? attr-dict

This operation asserts that a given boolean value is true. Assertions are checked statically when possible. If the condition evaluates to true, the assertion is removed. If false, an error is reported. Otherwise, the assertion is preserved. All assertions that appear in constrain() functions must evaluate statically (i.e., they cannot depend on inputs to the circuit) else an error is reported.

Assertion without message:

%1 = bool.cmp lt(%a, %b)

bool.assert %1

Assertion with a message:

%1 = bool.cmp eq(%a, %b)

bool.assert %1, "expected equal values"

Interfaces: MemoryEffectOpInterface

Attributes:

Attribute	MLIR Type	Description
`msg`	::mlir::StringAttr	string attribute

Operands:

Operand	Description
condition	1-bit signless integer

bool.cmp (::llzk::boolean::CmpOp)

Compare field element values

Syntax:

operation ::= `bool.cmp` $predicate `(` $lhs `,` $rhs `)`
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false") attr-dict

This operation takes two field element values and compares them according to the comparison predicate and returns an i1. The following comparisons are supported:

eq: equal
ne: not equal
lt: less than
le: less than or equal
gt: greater than
ge: greater than or equal

The result is 1 if the comparison is true and 0 otherwise.

The inequality operators (lt, gt, le, ge) for the finite field elements are defined by treating the field elements as integer values: f1 op f2 iff int(f1) op int(f2)

Example:

// Less than comparison.
%0 = bool.cmp lt(%a, %b)
 
// Greater than or equal comparison.
%1 = bool.cmp ge(%a, %b)
 
// Not equal comparison.
%2 = bool.cmp ne(%a, %b)
 
// Not equal comparison for felts in a specified field
%3 = bool.cmp ne(%c, %d) : !felt.type<"babybear">, !felt.type<"babybear">

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`predicate`	::llzk::boolean::FeltCmpPredicateAttr	Field element comparison predicate

Operands:

Operand	Description
lhs	finite field element
rhs	finite field element

Results:

Result	Description
result	1-bit signless integer

bool.exists (::llzk::boolean::ExistsOp)

Exists quantifier operation

This operation applies a predicate to each element of the given sort. Returns true iff the predicate is true for at least one element of the sort.

Only LLZK arrays are supported as the sort type at the moment.

Example:

%c10 = felt.const  10
%0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
%1 = bool.exists %e in %0 !array.type<3 x !felt.type> {
  %2 = bool.cmp lt(%e, %c10)
  bool.yield %2
}

Traits: AlwaysSpeculatableImplTrait, NotFieldNative, SingleBlock

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
sort	n-dimensional array

Results:

Result	Description
result	1-bit signless integer

bool.forall (::llzk::boolean::ForAllOp)

Forall quantifier operation

This operation applies a predicate to each element of the given sort. Returns true iff the predicate is true for all elements of the sort.

Only LLZK arrays are supported as the sort type at the moment.

Example:

%c10 = felt.const  10
%0 = array.new %a, %b, %c : !array.type<3 x !felt.type>
%1 = bool.forall %e in %0 !array.type<3 x !felt.type> {
  %2 = bool.cmp lt(%e, %c10)
  bool.yield %2
}

Traits: AlwaysSpeculatableImplTrait, NotFieldNative, SingleBlock

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
sort	n-dimensional array

Results:

Result	Description
result	1-bit signless integer

bool.not (::llzk::boolean::NotBoolOp)

Logical NOT operator

Syntax:

operation ::= `bool.not` $operand
              `` custom<InferredOrParsedType>(type($operand), "true")
              attr-dict

This operation computes the logical NOT (i.e., negation) of an i1 (i.e., boolean) value as an i1 value. The result is 1 if the operation is true and 0 otherwise.

If used in a constraint expression, this operation can be converted to 1+a - 2*a on felt operands.

Traits: AlwaysSpeculatableImplTrait, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	1-bit signless integer or type variable

Results:

Result	Description
result	1-bit signless integer

bool.or (::llzk::boolean::OrBoolOp)

Logical OR operator

Syntax:

operation ::= `bool.or` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

This operation computes the logical OR (i.e., disjunction) of two i1 (i.e., boolean) values as an i1 value. The result is 1 if the operation is true and 0 otherwise.

If used in a constraint expression, this operation can be converted to a+b - a*b on felt operands.

Traits: AlwaysSpeculatableImplTrait, Commutative, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	1-bit signless integer or type variable
rhs	1-bit signless integer or type variable

Results:

Result	Description
result	1-bit signless integer

bool.xor (::llzk::boolean::XorBoolOp)

Logical XOR operator

Syntax:

operation ::= `bool.xor` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

This operation computes the logical XOR (i.e., exclusive disjunction) of two i1 (i.e., boolean) values as an i1 value. The result is 1 if the operation is true and 0 otherwise.

If used in a constraint expression, this operation can be converted to a+b - 2*a*b on felt operands.

Traits: AlwaysSpeculatableImplTrait, Commutative, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	1-bit signless integer or type variable
rhs	1-bit signless integer or type variable

Results:

Result	Description
result	1-bit signless integer

bool.yield (::llzk::boolean::YieldOp)

Boolean yield operation

Syntax:

operation ::= `bool.yield` $value attr-dict

This terminator operation yields the boolean value of the predicate inside the body of bool.forall and bool.exists operations.

Traits: HasParent<ForAllOp, ExistsOp>, NotFieldNative, ReturnLike, Terminator

Interfaces: RegionBranchTerminatorOpInterface

Operands:

Operand	Description
value	1-bit signless integer

Attributes

FeltCmpPredicateAttr

Field element comparison predicate

Syntax:

#bool.cmp<
  `eq` | `ne` | `lt` | `le` | `gt` | `ge`   # value
>

Parameters:

Parameter	C++ type	Description
value	llzk::boolean::FeltCmpPredicate	an enum of type FeltCmpPredicate

Enums

FeltCmpPredicate

Field element comparison predicate

Cases:

Symbol	Value	String
EQ	0	eq
NE	1	ne
LT	2	lt
LE	3	le
GT	4	gt
GE	5	ge

'cast' Dialect

LLZK type conversion operations.

Operations

cast.tofelt (::llzk::cast::IntToFeltOp)

Convert an integer into a field element

Syntax:

operation ::= `cast.tofelt` `` custom<OptionalOverflowSemantics>($overflow) $value
              `:` type($value)
              `` custom<InferredOrParsedType>(type($result), "false") attr-dict

This operation converts a supported integer type value into a field element value. Boolean (i1) values map to zero or one, while index values are interpreted as signed integers. The overflow mode determines how values outside the target field's safe range are handled. For index inputs, the default assert mode fails on such values, even when the result is unused, and cannot be speculated. Boolean inputs always fit in every field, so their casts are side-effect-free and speculatable in every mode, even when the result field is unspecified. The sat, wrap, and trunc modes are side-effect-free and speculatable.

The trunc mode keeps the low k = bitwidth(p) bits, then reduces modulo the target field's prime p: (value mod 2^k) mod p, with nonnegative remainders. The result is always in [0, p). This differs from wrap, which reduces the original integer directly modulo p. For example, with p = 7, truncating -1 keeps the bits 111 and reduces 7 to 0, while wrapping -1 yields 6.

Constant folding defers casts whose result field is unspecified, whose operand is unknown, or whose assert range check fails.

Example:

%0 = bool.cmp lt(%a, %b)

%1 = cast.tofelt %0 : i1

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, MemoryEffectOpInterface

Attributes:

Attribute	MLIR Type	Description
`overflow`	::llzk::cast::OverflowSemanticsAttr	Specifies how a cast handles a source value outside the target's safe range. For a felt target with prime p, the safe range is [0, p-1]. For an index target with bitwidth N, it is [0, 2^(N-1)-1].

Operands:

Operand	Description
value	1-bit signless integer or index

Results:

Result	Description
result	finite field element

cast.toindex (::llzk::cast::FeltToIndexOp)

Convert a field element into an index

Syntax:

operation ::= `cast.toindex` `` custom<OptionalOverflowSemantics>($overflow) $value

`` custom<InferredOrParsedType>(type($value), "true") attr-dict

This operation converts a field element value into an index value to allow use as an array index or loop bound.

The default assert overflow mode fails when the value is outside the index safe range, even when the result is unused, and cannot be speculated. If the source has a declared field whose maximum canonical value p-1 fits in the index safe range, the assertion cannot fail, so the cast is side-effect-free and speculatable. Unspecified fields remain conservative. The sat, wrap, and trunc modes are side-effect-free and speculatable.

Constant folding reduces the operand in its field before applying the overflow mode and returns an index constant. Folding defers when the field is unspecified or the assert range check fails.

Example:

%0 = cast.toindex %a

%1 = array.read %b[%0]

Traits: NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, MemoryEffectOpInterface

Attributes:

Attribute	MLIR Type	Description
`overflow`	::llzk::cast::OverflowSemanticsAttr	Specifies how a cast handles a source value outside the target's safe range. For a felt target with prime p, the safe range is [0, p-1]. For an index target with bitwidth N, it is [0, 2^(N-1)-1].

Operands:

Operand	Description
value	finite field element

Results:

Result	Description
result	index

Attributes

OverflowSemanticsAttr

Specifies how a cast handles a source value outside the target's safe range. For a felt target with prime p, the safe range is [0, p-1]. For an index target with bitwidth N, it is [0, 2^(N-1)-1].

Syntax:

#cast.overflow<
  `assert` | `sat` | `wrap` | `trunc`   # value
>

Parameters:

Parameter	C++ type	Description
value	llzk::cast::OverflowSemantics	an enum of type OverflowSemantics

Enums

OverflowSemantics

Specifies how a cast handles a source value outside the target's safe range. For a felt target with prime p, the safe range is [0, p-1]. For an index target with bitwidth N, it is [0, 2^(N-1)-1].

Cases:

Symbol	Value	String
ASSERT	0	assert
SATURATE	1	sat
WRAP	2	wrap
TRUNCATE	3	trunc

'constrain' Dialect

LLZK constraint emission operations.

Operations

constrain.eq (::llzk::constrain::EmitEqualityOp)

Emit an equality constraint

Syntax:

operation ::= `constrain.eq` $lhs `,` $rhs `:` type($lhs)
              `` custom<InferredOrParsedType>(type($rhs), ref(type($lhs)))
              attr-dict

Emits an equality constraint between lhs and rhs.

Traits: Commutative, ConstraintGen, Elementwise, Scalarizable, Tensorizable, Vectorizable

Interfaces: ConstraintOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
lhs	any LLZK type, excluding struct and string types
rhs	any LLZK type, excluding struct and string types

constrain.in (::llzk::constrain::EmitContainmentOp)

Emit a containment constraint

Syntax:

operation ::= `constrain.in` $lhs `,` $rhs `:` type($lhs) `,` type($rhs) attr-dict

Emits a containment constraint between lhs and rhs (rhs must be contained within lhs). If lhs is an N-dimensional array (N >= 1), rhs must be an M-dimensional array, where N >= M (M=0 means that rhs is a scalar element of type accepted by the constrain.eq operation).

Traits: ConstraintGen

Interfaces: ConstraintOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
lhs	n-dimensional array
rhs	a valid LLZK type

'felt' Dialect

LLZK felt (Field ELemenT) type and operations.

Operations

felt.add (::llzk::felt::AddFeltOp)

Addition operator for field elements

Syntax:

operation ::= `felt.add` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.bit_and (::llzk::felt::AndFeltOp)

Bitwise AND operator for field elements

Syntax:

operation ::= `felt.bit_and` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.bit_not (::llzk::felt::NotFeltOp)

Integer complement (bitwise-not) operator for field elements

Syntax:

operation ::= `felt.bit_not` $operand
              `` custom<InferredOrParsedType>(type($operand), "true")
              attr-dict

Treats the operand as an integer with a bitwidth equal to the bitwidth of the prime field's modulus and compute the one's complement of the integer. The result is converted back to a field element by applying the prime modulus.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.bit_or (::llzk::felt::OrFeltOp)

Bitwise OR operator for field elements

Syntax:

operation ::= `felt.bit_or` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.bit_xor (::llzk::felt::XorFeltOp)

Bitwise XOR operator for field elements

Syntax:

operation ::= `felt.bit_xor` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.const (::llzk::felt::FeltConstantOp)

Field element constant

Syntax:

operation ::= `felt.const` $value attr-dict

This operation produces a constant finite field element. felt.const N : !felt.type<F> denotes N mod p, where p is the prime modulus of field F. This meaning does not depend on whether the operation has been canonicalized: raw values congruent modulo p denote the same field element.

The stored integer need not be in [0, p). Canonicalization replaces it with the unique representative in that range without changing its meaning. When the field is unspecified, reduction is deferred until the field is known, and canonicalization leaves the stored integer unchanged.

Some analyses or transformations may supply an explicit prime modulus q for their arithmetic, such as interval analysis with its field option. The constant retains its declared-field meaning: its value is first interpreted as N mod p, then reduced modulo q, yielding (N mod p) mod q. For example, a literal 8 declared in a field of modulus 7 contributes 1 when analyzed with modulus 5, both before and after canonicalization. If the constant's field is unspecified, it is reduced directly as N mod q.

Example:

%0 = felt.const 42

%0 = felt.const 99 <"bn254">

Traits: AlwaysSpeculatableImplTrait, ConstantLike, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface), OpAsmOpInterface

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`value`	::llzk::felt::FeltConstAttr	finite field element

Results:

Result	Description
result	a valid LLZK type

felt.div (::llzk::felt::DivFeltOp)

Field-division operator for field elements

Syntax:

operation ::= `felt.div` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Performs finite-field division by multiplying the dividend by the multiplicative inverse of the divisor. For a non-zero divisor b, felt.div a, b computes a * inv(b) modulo the field prime of the result prime field.

The divisor must be non-zero.

This is not integer division. Use felt.uintdiv or felt.sintdiv when the operands should be interpreted as integers.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.inv (::llzk::felt::InvFeltOp)

Inverse operator for field elements

Syntax:

operation ::= `felt.inv` $operand
              `` custom<InferredOrParsedType>(type($operand), "true")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.mul (::llzk::felt::MulFeltOp)

Multiplication operator for field elements

Syntax:

operation ::= `felt.mul` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.neg (::llzk::felt::NegFeltOp)

Negation operator for field elements

Syntax:

operation ::= `felt.neg` $operand
              `` custom<InferredOrParsedType>(type($operand), "true")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.pow (::llzk::felt::PowFeltOp)

Exponentiation operator for field elements

Syntax:

operation ::= `felt.pow` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Raises a field element to the power of an exponent.

%result = felt.pow %base, %exponent

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.shl (::llzk::felt::ShlFeltOp)

Left shift operator for field elements

Syntax:

operation ::= `felt.shl` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Treats both operands as unsigned integer representatives of field elements. felt.shl a, b computes a * 2^b, then converts the result back to a field element by reducing modulo the field prime.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.shr (::llzk::felt::ShrFeltOp)

Right shift operator for field elements

Syntax:

operation ::= `felt.shr` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Treats both operands as unsigned integer representatives of field elements. felt.shr a, b computes a / 2^b using unsigned integer division rounding towards zero, then converts the result back to a field element.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.sintdiv (::llzk::felt::SignedIntDivFeltOp)

Signed integer division operator for field elements

Syntax:

operation ::= `felt.sintdiv` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Treats the operands as if they were signed integers with bitwidth equal to that of the prime modulus (no additional sign bit is added) and performs division rounding towards zero.

The signed integer representation of felt f in prime field with modulus p follows the following formula:

signed_int(f) = f    if 0 <= f < p/2 + 1
    "p/2" here is unsigned integer division rounding towards 0
signed_int(f) = f-p  if p/2 + 1 <= f < p

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.smod (::llzk::felt::SignedModFeltOp)

Signed integer modulus/remainder operator for field elements

Syntax:

operation ::= `felt.smod` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Computes the remainder that would result from the division operation performed by felt.sintdiv.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.sub (::llzk::felt::SubFeltOp)

Subtraction operator for field elements

Syntax:

operation ::= `felt.sub` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.uintdiv (::llzk::felt::UnsignedIntDivFeltOp)

Unsigned integer division operator for field elements

Syntax:

operation ::= `felt.uintdiv` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Treats the operands as if they were unsigned integers with bitwidth equal to that of the prime modulus and performs division rounding towards zero.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

felt.umod (::llzk::felt::UnsignedModFeltOp)

Unsigned integer modulus/remainder operator for field elements

Syntax:

operation ::= `felt.umod` $lhs `,` $rhs
              `` custom<InferredOrParsedType>(type($lhs), "true")
              `` custom<InferredOrParsedType>(type($rhs), "false")
              attr-dict

Computes the remainder that would result from the division operation performed by felt.uintdiv.

Traits: AlwaysSpeculatableImplTrait, InferTypeOpAdaptor, NotFieldNative

Interfaces: ConditionallySpeculatable, FeltBinaryOpInterface, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	finite field element or type variable
rhs	finite field element or type variable

Results:

Result	Description
result	a valid LLZK type

Attributes

FeltConstAttr

Finite field element

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.

Parameters:

Parameter	C++ type	Description
rawValue	llzk::DynamicAPIntValue	The unreduced felt constant value
type	FeltType

FieldSpecAttr

Prime field specification

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

Parameters:

Parameter	C++ type	Description
fieldName	::mlir::StringAttr
prime	llzk::DynamicAPIntValue	The prime modulus

Types

FeltType

Finite field element

Syntax:

!felt.type<
  ::mlir::StringAttr   # fieldName
>

An element of a finite field. The field can be specified (e.g., !felt.type<"bn254">) or left unspecified (!felt.type), to be filled in by the backend consumer of LLZK IR. Leaving the field unspecified may reduce the power of certain transformation passes.

For a field with prime modulus p, a felt denotes a residue modulo p, with its canonical representative in [0, p). An unreduced integer representation does not denote a distinct value outside this range.

Backends are responsible for performing conversions between felts of different fields. If a circuit needs to encode translations between fields, the circuit may define a function prototype, e.g.:

function.def @convert(%a : !felt.type<"bn254">) -> !felt.type<"goldilocks">;

and perform the lowering of calls to this conversion function in a backend-specific manner.

The field name can be chosen from one of the built-in fields or specified using felt.field specification attributes on the root module.

Parameters:

Parameter	C++ type	Description
fieldName	::mlir::StringAttr

'function' Dialect

LLZK function operations.

Operations

function.call (::llzk::function::CallOp)

Call operation

Syntax:

operation ::= `function.call` $callee
              ( `<` custom<TemplateParams>($templateParams)^ `>` )?
              `` `(` $argOperands `)`
              ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
              `:` functional-type($argOperands, results)
              custom<AttrDictWithWarnings>(attr-dict, prop-dict)

The function.call operation represents a call to another function. The operands and result types of the call must match the specified function type. The callee is encoded as a symbol reference attribute named "callee" which must be the full path to the target function from the root module (i.e., the module containing the [llzk::LANG_ATTR_NAME] attribute).

Example:

// Call a global function defined in the root module.
function.call @do_stuff(%0) : (!struct.type<@Bob>) -> ()
%1, %2 = function.call @split(%x) : (index) -> (index, index)
 
// Call a function within a component
%2 = function.call @OtherStruct::@compute(%3, %4) : (index, index) -> !struct.type<@OtherStruct>
function.call @OtherStruct::@constrain(%5, %6) : (!struct.type<@OtherStruct>, !felt.type) -> ()

When the return StructType of a compute() function uses AffineMapAttr to express struct parameter(s) that depend on a loop variable, the optional instantiation parameter list of this operation must be used to instatiate all AffineMap used as parameters to the StructType.

Examples:

#M = affine_map<(i)[] -> (5*i+1)>

%r = function.call @A::@compute(%x){(%i)} : (!felt.type) -> !struct.type<@A<[#M]>>

When the call targets a free function within a poly.template region, the optional template parameter list can be used to instantiate all poly.param symbols within the template. If all poly.param symbols are used within the function signature, this can be elided. Otherwise, it is required to instantiate the function. The ? wildcard can be used for any poly.param with a poly.tvar type restriction, even those that cannot be inferred from the function signature. The wildcard allows for inference of the type within the function body itself during the flattening pass but may fail if the type cannot be inferred from the function body.

Traits: AttrSizedOperandSegments, MemRefsNormalizable, VerifySizesForMultiAffineOps<1>

Interfaces: ArgAndResultAttrsOpInterface, CallOpInterface, LLZKCallLikeOpInterface, SymbolUserOpInterface

Attributes:

Attribute	MLIR Type	Description
`callee`	::mlir::SymbolRefAttr	symbol reference attribute
`templateParams`	::mlir::ArrayAttr	array attribute
`numDimsPerMap`	::mlir::DenseI32ArrayAttr	i32 dense array attribute
`mapOpGroupSizes`	::mlir::DenseI32ArrayAttr	i32 dense array attribute
`arg_attrs`	::mlir::ArrayAttr	Array of dictionary attributes
`res_attrs`	::mlir::ArrayAttr	Array of dictionary attributes

Operands:

Operand	Description
argOperands	variadic of a valid LLZK type
mapOperands	variadic of index

Results:

Result	Description
«unnamed»	variadic of a valid LLZK type

function.def (::llzk::function::FuncDefOp)

An operation with a name containing a single SSACFG region

Operations within the function cannot implicitly capture values defined outside of the function, i.e., functions are IsolatedFromAbove. All external references must use function arguments (which are passed by value) or reference external members or globals by symbol name.

Functions appearing within a struct.def have specific semantics and must be named compute, constrain, or product. Functions appearing at the module level (i.e. not within a struct.def) have no name restrictions and their body may be elided to denote an external function declaration.

Modules and struct.def ops are not allowed to be nested within functions.

Function arguments may carry an optional function.arg_name attribute to preserve the source-level argument name independently from the printed SSA block argument name. The value must be a non-empty, untyped StringAttr, and all attached function.arg_name values must be unique within the function. Typed string attributes such as "x" : i1 are rejected. The attribute is only valid on function arguments. Argument-splitting transforms preserve this metadata by deriving unique names for generated arguments, such as input[0] for array elements or self.member for struct members.

Function results may similarly carry an optional function.res_name attribute. The value must be a non-empty, untyped StringAttr, all attached result names must be unique within the function, and the attribute is only valid on function results.

Example:

// External function definitions.
function.def private @abort()
function.def private @scribble(
  !array.type<5 x !felt.type> {function.arg_name = "input"},
  !struct.type<@Hello> {function.arg_name = "state"}) -> i1
 
// A function that returns its argument twice:
function.def @count(%x: !felt.type {function.arg_name = "x"})
    -> (!felt.type {function.res_name = "first"},
        !felt.type {function.res_name = "second"}) {
  function.return %x, %x: !felt.type, !felt.type
}
 
// Function definition within a component
struct.def @NonZero {
  function.def @compute(%a: !felt.type {function.arg_name = "a"}) { function.return }
  function.def @constrain(%a: !felt.type {function.arg_name = "a"}) { function.return }
}

Traits: AffineScope, AutomaticAllocationScope, HasParent<::mlir::ModuleOp, llzk::component::StructDefOp, llzk::polymorphic::TemplateOp>, IsolatedFromAbove

Interfaces: ArgAndResultAttrsOpInterface, CallableOpInterface, ContractTarget, FunctionOpInterface, SymbolUserOpInterface, Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute
`function_type`	::mlir::TypeAttr	type attribute of function type
`arg_attrs`	::mlir::ArrayAttr	Array of dictionary attributes
`res_attrs`	::mlir::ArrayAttr	Array of dictionary attributes

function.return (::llzk::function::ReturnOp)

Function return operation

Syntax:

operation ::= `function.return` attr-dict ($operands^ `:` type($operands))?

The function.return operation represents a return operation within a function. The operation takes variable number of operands and produces no results. The operand number and types must match the signature of the function that contains the operation.

Example:

function.def @foo() : (!felt.type, index) {
  ...
  return %0, %1 : !felt.type, index
}

Traits: AlwaysSpeculatableImplTrait, HasParent<::llzk::function::FuncDefOp>, MemRefsNormalizable, ReturnLike, Terminator

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface), RegionBranchTerminatorOpInterface

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operands	variadic of a valid LLZK type

'global' Dialect

LLZK support for global values, defined outside of structs.

Operations

global.def (::llzk::global::GlobalDefOp)

Global value

Examples:

// Global constant (denoted by "const" modifier) string.
global.def const @s : !string.type = "Hello World!"
 
// Global variable (i.e., no "const" modifier) with initial value.
global.def @b : i1 = false
 
// Uninitialized global variable.
global.def @a : !array.type<2,2 x i1>

An initializer's typed attributes must exactly match the declared global type. When parsing a felt initializer, an explicitly selected field refines an unspecified declared felt type; conversely, an unspecified felt initializer adopts an explicitly declared field. Thus, an initialized global always stores matching declared and initializer felt types.

Traits: HasParent<mlir::ModuleOp>

Interfaces: SymbolUserOpInterface, Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute
`constant`	::mlir::UnitAttr	unit attribute
`type`	::mlir::TypeAttr	type attribute of any LLZK type except non-constant types
`initial_value`	::mlir::Attribute	any attribute

global.read (::llzk::global::GlobalReadOp)

Read value of a global

Syntax:

operation ::= `global.read` (`const` $constant^)? $name_ref `:` type($val) attr-dict

This operation copies the value of a named global. The result is a value copy, not a pointer or alias to the global's storage. Reads marked const must target a global declared with the const modifier and thus have no memory effects.

Interfaces: GlobalRefOpInterface, MemoryEffectOpInterface, SymbolUserOpInterface

Attributes:

Attribute	MLIR Type	Description
`constant`	::mlir::UnitAttr	unit attribute
`name_ref`	::mlir::SymbolRefAttr	symbol reference attribute

Results:

Result	Description
val	any LLZK type except non-constant types

global.write (::llzk::global::GlobalWriteOp)

Write value to a global

Syntax:

operation ::= `global.write` $name_ref `=` $val `:` type($val) attr-dict

This operation copies a value to a named global. It does not create a pointer or alias between the source value and the global's storage. Not allowed for globals declared with the "const" modifier.

Traits: WitnessGen

Interfaces: GlobalRefOpInterface, MemoryEffectOpInterface (MemoryEffectOpInterface), SymbolUserOpInterface

Effects: MemoryEffects::Effect{MemoryEffects::Write on llzk::global::GlobalMemoryResource}

Attributes:

Attribute	MLIR Type	Description
`name_ref`	::mlir::SymbolRefAttr	symbol reference attribute

Operands:

Operand	Description
val	any LLZK type except non-constant types

'include' Dialect

LLZK include operations.

Operations

include.from (::llzk::include::IncludeOp)

Include operation

Syntax:

operation ::= `include.from` $path `as` $sym_name attr-dict

This operation imports the contents of another source file in place of itself.

Example:

include.from "lib.llzk" as @aliasName

Traits: HasParent<::mlir::ModuleOp>

Interfaces: Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute
`path`	::mlir::StringAttr	string attribute

'llzk' Dialect

Common LLZK attributes.

Operations

llzk.nondet (::llzk::NonDetOp)

Uninitialized variable

Syntax:

operation ::= `llzk.nondet` `:` type($res) attr-dict

This operation produces an SSA variable of the specified type but with nondeterministic value.

This op can be used in @constrain() functions in place of expressions that cannot be included in constraints. It may also be generated for a frontend language that supports uninitialized variables and can also be introduced by the llzk-array-to-scalar pass if there is a read from an array index that was not dominated by an earlier write to that same index.

Example:

%0 = llzk.nondet : !felt.type

Note that llzk.nondet does not have the ConstantLike or NoMemoryEffect traits because different SSA variables initialized with llzk.nondet may be constrained in different ways so they cannot be treated as identical values. However, it does have the AlwaysSpeculatable trait to denote that it is free to move, hoist, and sick without changing the semantics.

Example:

%0 = llzk.nondet : !felt.type
%1 = llzk.nondet : !felt.type
%c1 = felt.const 1
constrain.eq %0, %c1 : !felt.type
 
%m = struct.readm %self[@m] : !struct.type<@S>, !felt.type
constrain.eq %m, %1 : !felt.type

In the above example, m is effectively unconstrained, as it is only constrained to the nondet value %1. However, if %0 and %1 were treated as pure constants, %0 and %1 could be combined, resulting in:

%0 = llzk.nondet : !felt.type
%c1 = felt.const 1
constrain.eq %0, %c1 : !felt.type
 
%m = struct.readm %self[@m] : !struct.type<@S>, !felt.type
constrain.eq %m, %0 : !felt.type

This transformation would constrain m to be exactly equal to 1, thus changing the semantics of the circuit.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, OpAsmOpInterface

Results:

Result	Description
res	a valid LLZK type

Attributes

LoopBoundsAttr

Trusted annotation with the bounds of a loop

Syntax:

#llzk.loopbounds<
  ::llzk::DynamicAPIntValue,   # lower
  ::llzk::DynamicAPIntValue,   # upper
  ::llzk::DynamicAPIntValue   # step
>

This attribute indicates the loop variable's lower bound (inclusive), upper bound (exclusive), and step size.

These attributes are trusted unconditionally, so the producer must ensure these values agree with the loop's behavior. Passes are not required to produce an error diagnostic if the values specified by the attribute contradict the IR itself; incorrect annotations can change program behavior.

Example:

scf.while ... {
  ...
} do {
  ...
} attributes { llzk.loopbounds = #llzk.loopbounds<0 to 10 step 1> }

Parameters:

Parameter	C++ type	Description
lower	llzk::DynamicAPIntValue	Loop variable lower bound (inclusive)
upper	llzk::DynamicAPIntValue	Loop variable upper bound (exclusive)
step	llzk::DynamicAPIntValue	Loop variable step/increment

PublicAttr

A unit attribute to mark an input/output as public

Syntax: #llzk.pub

This attribute is used on parameters of compute() and constrain() functions within a struct.def to denote the public inputs of the circuit and on struct.member ops to denote public output of the circuit.

Examples:

struct.member @member_name : !felt.type {llzk.pub}
 
function.def @compute(%0: !felt.type {llzk.pub})

'pod' Dialect

Dialect for working with plain-old-data structs.

Operations

pod.new (::llzk::pod::NewPodOp)

Create a new plain-old-data struct

Creates a new, uninitialized, pod instance. Optionally, the user can pass a list of record names and values that initialize the records of the pod. Partial initialization is allowed. All records without an explicit initialization are initialized with nondeterministic values.

If the types of the pod records have affine map parameters the user can pass values for them similar to how array.new does it.

This operation returns one value of type PODType and, if present, the records passed for initialization must form a subset of the records in the type.

Examples:

// Empty pod instance
%0 = pod.new : !pod.type<[]>
 
// Uninitialized/nondeterministic pod instance
%0 = pod.new : !pod.type<[@n: !felt.type]>
 
// Initialized pod instance
%0 = felt.const 1
%1 = pod.new { @n = %0 } : !pod.type<[@n: !felt.type]>
 
// Another one, but with 2 fields
%0 = felt.const 1
%1 = felt.inv %0
%2 = pod.new { @n = %0, @inv = %1 } :   !pod.type<[@n: !felt.type, @inv: !felt.type]>
 
// Partial init
%0 = felt.const 1
%1 = pod.new { @n = %0 } : !pod.type<[@n: !felt.type, @inv: !felt.type]>
 
// Affine map args on uninitialized pod instance
%0 = arith.constant 1 : index
%c = arith.constant 2 : index
%1 = pod.new(%0)[%c] : !pod.type<[@a: !array.type<#map, !felt.type>]>
 
// Affine map with initialized records
%0 = arith.constant 1 : index
%c = arith.constant 2 : index
%1 = felt.const 5
%2 = pod.new { @f = %1 }(%0)[%c] : !pod.type<[@f: !felt.type, @a: !array.type<#map, !felt.type>]>

Traits: AttrSizedOperandSegments, VerifySizesForMultiAffineOps<1>

Interfaces: DestructurableAllocationOpInterface, MemoryEffectOpInterface (MemoryEffectOpInterface), OpAsmOpInterface, PromotableAllocationOpInterface

Effects: MemoryEffects::Effect{MemoryEffects::Allocate on llzk::DiscardableAllocationResource}

Attributes:

Attribute	MLIR Type	Description
`initializedRecords`	::mlir::ArrayAttr	string array attribute
`numDimsPerMap`	::mlir::DenseI32ArrayAttr	i32 dense array attribute
`mapOpGroupSizes`	::mlir::DenseI32ArrayAttr	i32 dense array attribute

Operands:

Operand	Description
initialValues	variadic of a valid LLZK type
mapOperands	variadic of index

Results:

Result	Description
result	plain-old-data struct

pod.read (::llzk::pod::ReadPodOp)

Reads the contents of a plain-old-data struct record

Syntax:

operation ::= `pod.read` $pod_ref `[` custom<RecordName>($record_name) `]` `:` type($pod_ref) `,` type($result) attr-dict

Copies the current value of a named record from a pod instance. The result is a value copy, not a pointer or alias to the record's storage. Returns one value of the type of the record. For an identity-bearing struct.type record, the copied value is a handle to the same component instance; it does not duplicate the component's members, signals, or tables. Immutable scalars and shape-only arrays may likewise reuse their SSA representation because they have no independently mutable payload. Lowering must reject a mutable aggregate when it cannot materialize independent storage for the copy.

The name of the record must be a valid record name for the pod type and the result type must match the type of the record.

Example:

%1 = pod.read %0[@sym] : !pod.type<[@sym: !type, ...]>, !type

Interfaces: DestructurableAccessorOpInterface, DiscardableAllocationAccessorOpInterface, PodAccessOpInterface, PodRefOpInterface, PromotableMemOpInterface

Attributes:

Attribute	MLIR Type	Description
`record_name`	::mlir::StringAttr	string attribute

Operands:

Operand	Description
pod_ref	plain-old-data struct

Results:

Result	Description
result	a valid LLZK type

pod.write (::llzk::pod::WritePodOp)

Writes content into a plain-old-data struct record

Syntax:

operation ::= `pod.write` $pod_ref `[` custom<RecordName>($record_name) `]` `=` $value `:` type($pod_ref) `,` type($value) attr-dict

Copies a value into a named record of a pod instance. It does not create a pointer or alias between the source value and the record's storage. For an identity-bearing struct.type source, the stored value is a handle to the same component instance; it does not duplicate the component's members, signals, or tables. This operation has no result values. Immutable scalars and shape-only arrays may reuse their SSA representation because they have no independently mutable payload. Lowering must reject a mutable aggregate when it cannot materialize independent storage for the copy.

The name of the record must be a valid record name for the pod type and the source value type must match the type of the record.

Writing a record that was written or initialized earlier overwrites the previous value.

Example:

pod.write %0[@sym] = %1 : !pod.type<[@sym: !type, ...]>, !type

Interfaces: DestructurableAccessorOpInterface, DiscardableAllocationAccessorOpInterface, PodAccessOpInterface, PodRefOpInterface, PromotableMemOpInterface

Attributes:

Attribute	MLIR Type	Description
`record_name`	::mlir::StringAttr	string attribute

Operands:

Operand	Description
pod_ref	plain-old-data struct
value	a valid LLZK type

Attributes

RecordAttr

A named entry in a plain-old-data struct

Syntax:

#pod.record<
  ::mlir::StringAttr,   # name
  ::mlir::Type   # type
>

Parameters:

Parameter	C++ type	Description
name	::mlir::StringAttr	Name of the record entry.
type	::mlir::Type	Type of the record entry.

Types

PodType

Plain-old-data struct

Syntax:

!pod.type<
  ::llvm::ArrayRef<::llzk::pod::RecordAttr>   # records
>

Contains a list of RecordAttr defining structure of a pod. The order of records in the pod matters and each record must have a unique name. It is possible to have a pod with no records.

Two PODType types unify if they have the same record names, defined in the same order, and if the types of corresponding records unify.

This type can be used in the struct.member op, and it can be declared as a column, in which case that annotation is also implied on the inner records (except those that cannot be column such as string.type records).

// Type with no records.
!pod.type
 
// Type with two records of felt type.
!pod.type<[@a: !felt.type, @b: !felt.type]>

Parameters:

Parameter	C++ type	Description
records	::llvm::ArrayRef<::llzk::pod::RecordAttr>	List of records in the pod

'poly' Dialect

LLZK types and operations to support templated/parameterized structs.

Operations

poly.applymap (::llzk::polymorphic::ApplyMapOp)

Apply an AffineMap

Syntax:

operation ::= `poly.applymap` custom<DimAndSymbolList>($mapOperands, $numDims) $map attr-dict

This operation applies an AffineMap to a list of SSA values, yielding a single SSA value. The number of dimension and symbol arguments must be equal to the respective number of dimensional and symbolic inputs to the AffineMap; the AffineMap has to be one-dimensional, and so this operation always returns one value. The input operands and result all have index type.

Named map example:

#map10 = affine_map<(d0, d1) -> (d0 floordiv 8 + d1 floordiv 128)>
...
%1 = poly.applymap(%s, %t) #map10

Inline example:

%2 = poly.applymap(%42)[%n] affine_map<(i)[s0] -> (i+s0)>

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`map`	::mlir::AffineMapAttr	AffineMap attribute
`numDims`	::mlir::IntegerAttr	index attribute

Operands:

Operand	Description
mapOperands	variadic of index

Results:

Result	Description
«unnamed»	index

poly.expr (::llzk::polymorphic::TemplateExprOp)

Declares a named expression in a polymorphic template

Syntax:

operation ::= `poly.expr` $sym_name $initializerRegion attr-dict

Declares an expression over parameters of a poly.template that can be used just like a parameter within the function and/or struct definitions within the template.

The body of a poly.expr cannot contain any symbols defined via poly.expr to prevent cyclic initialization. The body must also have no side effects to ensure it can be safely duplicated if needed. This means operations such as read/write to globals or function calls are not allowed in the body of a poly.expr.

Example:

poly.template @TemplateName {
  poly.expr @ExprName {
    %0 = some_op %param1, %param2 : (!felt.type, !felt.type) -> !felt.type
    poly.yield %0 : !felt.type
  }
}

Traits: HasParent<::llzk::polymorphic::TemplateOp>, IsolatedFromAbove, NoRegionArguments, SingleBlock

Interfaces: SymbolUserOpInterface, Symbol, TemplateSymbolBindingOpInterface

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute

poly.param (::llzk::polymorphic::TemplateParamOp)

Declares a parameter of a polymorphic template

Syntax:

operation ::= `poly.param` $sym_name (`:` $type_opt^)? attr-dict

Declares a parameter of a poly.template that can be used by the function and/or struct definitions within the template. Each parameter can have an optional type restriction.

Example:

poly.template @TemplateName {
  poly.param @N
  poly.param @F : !felt.type
  // To restrict a parameter to accept only a type, use `!poly.tvar` with the parameter's own name.
  poly.param @T : !poly.tvar<@T>
}

Traits: HasParent<::llzk::polymorphic::TemplateOp>

Interfaces: SymbolUserOpInterface, Symbol, TemplateSymbolBindingOpInterface

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute
`type_opt`	::mlir::TypeAttr	type attribute of integral, felt, or typevar type

poly.read_const (::llzk::polymorphic::ConstReadOp)

Read value of a template parameter

Syntax:

operation ::= `poly.read_const` $const_name `:` type($val) attr-dict

This operation reads the value from the named constant parameter of the template in which this op appears. The op itself puts a type restriction on the value, but leaves it to a later type-checking pass to ensure the template parameters are instantiated with types matching the uses of the parameter within the template.

Examples:

// Read a `!felt.type` value from struct parameter "@A"
%0 = poly.read_const @A : !felt.type
// Read a value from struct parameter "@B" where its type is
// specified by struct parameter "@T"
%1 = poly.read_const @B : !poly.tvar<@T>

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface), SymbolUserOpInterface

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`const_name`	::mlir::FlatSymbolRefAttr	flat symbol reference attribute

Results:

Result	Description
val	integral, felt, or typevar type

poly.template (::llzk::polymorphic::TemplateOp)

Defines polymorphic functions or structs

Syntax:

operation ::= `poly.template` $sym_name $bodyRegion attr-dict

The poly.template allows defining polymorphic templated functions and structs. The body contains the definitions of the template's parameters along with the function and/or struct definitions that utilize those parameters in their bodies.

Example:

poly.template @TemplateName {
  poly.param @N
  poly.param @T
 
  function.def @f(%inp: !array.type<8,5,@N x !felt.type>) -> !array.type<@N x !felt.type> {
    // function header and body can use parameters @N and @T
  }
 
  struct.def @StructName {
    function.def @compute() -> !struct.type<@TemplateName::@StructName> {
      ...
    }
    function.def @constrain(%self: !struct.type<@TemplateName::@StructName>) {
      ...
    }
  }
}

The order of poly.param definitions in the template body determines the order that template parameters must be listed in the parameter list of a struct.type referring to a struct nested within the template. In the example above, the type of @StructName is !struct.type<@TemplateName::@StructName<[@N, @T]>>.

Transform passes may attach the discardable generic attribute poly.name_pattern to a partial template with P current poly.param operations. Its value is an ArrayAttr of P + 1 literal StringAttr chunks; gap i, between chunks i and i + 1, corresponds to current parameter i. The chunks are carried as structured metadata and are never recovered by interpreting sym_name; without the attribute, every byte of the current sym_name is opaque source or legacy text. When a transform closes the final gap, it removes the attribute rather than retaining a terminal one-chunk state.

Traits: HasParent<::mlir::ModuleOp>, IsolatedFromAbove, LLZKSymbolTableImplTrait, NoRegionArguments, NoTerminator, SingleBlock, SymbolTable

Interfaces: Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute

poly.unifiable_cast (::llzk::polymorphic::UnifiableCastOp)

Cast between two unifiable types

Syntax:

operation ::= `poly.unifiable_cast` $input `:` functional-type($input, results) attr-dict

This operation reinterprets a value as a different type with the restriction that the input and output types of the cast are unifiable.

Most ops that accept LLZK types accept unifiable types as input and thus there is no need for casting between types. This op is meant to be used in situations where is not possible to modify the given or the target type and they are different but unifiable. For example, inside a conversion pattern the driver may introduce unrealized_conversion_cast operations if the types are not equal. This will happen regardless of whether the two types unify. This cast can be introduced instead of the default cast operation to satisfy MLIR's assumptions on type equality.

Example:

%0 = some_other_op : !array.type<@N x !felt.type>

%1 = unifiable_cast %0 : (!array.type<@N x @felt.type>) -> !array.type<affine_map<()[s0, s1] -> (s0 + s1)> x !felt.type>

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
input	a valid LLZK type

Results:

Result	Description
result	a valid LLZK type

poly.yield (::llzk::polymorphic::YieldOp)

Expr initialization yield and termination operation

Syntax:

operation ::= `poly.yield` $val `:` type($val) attr-dict

This operation yields an SSA value from a poly.expr initialization region and terminates the region.

Traits: HasParent<::llzk::polymorphic::TemplateExprOp>, ReturnLike, Terminator

Interfaces: RegionBranchTerminatorOpInterface

Operands:

Operand	Description
val	integral, felt, or typevar type

Types

TypeVarType

Type variable

Syntax:

!poly.tvar<
  ::mlir::FlatSymbolRefAttr   # nameRef
>

This type serves as a placeholder for a type that is instantiated via a parameter of the struct.

For example, we can define a struct that holds a size-2 array where the type of the elements in the array is specified by a parameter of the struct and instantiated with a specific type at the uses of the struct.

poly.template @TA {
  poly.param @Ty
  struct.def @A {
    member @x : !array.type<2 x !poly.tvar<@Ty>>
    ...
  }
}

Parameters:

Parameter	C++ type	Description
nameRef	::mlir::FlatSymbolRefAttr	reference to the struct parameter

'string' Dialect

LLZK string type and operations.

Operations

string.new (::llzk::string::LitStringOp)

Literal string

Syntax:

operation ::= `string.new` $value attr-dict

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`value`	::mlir::StringAttr	string attribute

Results:

Result	Description
result	string type

Types

StringType

String type

Syntax: !string.type

'struct' Dialect

LLZK component/struct operations.

Operations

struct.def (::llzk::component::StructDefOp)

Circuit component definition

Syntax:

operation ::= `struct.def` $sym_name $bodyRegion attr-dict

This operation describes a component in a circuit. It can contain any number of members that hold inputs, outputs, intermediate values, and subcomponents of the defined component. It also contains a compute() function that holds the witness generation code for the component and a constrain() function that holds that constraint generation code for the component.

Example:

struct.def @ComponentA {
  member @f1 : !array.type<5 x index>
  member @f2 : !felt.type {llzk.pub}
 
  function.def @compute(%p: !felt.type) -> !struct.type<@ComponentA> {
    %self = struct.new : !struct.type<@ComponentA>
    // initialize all members of `%self` here
    return %self : !struct.type<@ComponentA>
  }
 
  function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
    // emit constraints here
    return
  }
}

The optional llzk.main = !struct.type<...> attribute on the top-level module in an LLZK IR program expresses the main entry point of the circuit as a concrete instantiation of a specific struct. For example, llzk.main = !struct.type<@Top<[52,12]>> or llzk.main = !struct.type<@Main<[i1, !felt.type, 256]>>. This struct has additional restrictions:

The parameter types of its functions (besides the required "self" parameter) can only be !felt.type or !array.type<.. x !felt.type>.
All inputs to the main struct are signals, even though they are not marked with the {signal} attribute (as the {signal} attribute is not used on function arguments). Input signals may be public (given the {llzk.pub} attribute) or private (by default).
All public members of the main struct are also signals (representing public output signals), and can also only be !felt.type or !array.type<.. x !felt.type>.

Example of a Main component:

module attributes {llzk.main = !struct.type<@Main>, llzk.lang} {
  struct.def @Main {
    member @out : !felt.type {llzk.pub, signal} // public output signal
    member @out2 : !felt.type {llzk.pub} // also a public output signal, implicitly
    member @intermediate : !struct.type<@OtherStruct> // an intermediate value, not a signal, can be any LLZK type
    // %p is a private input signal
    function.def @compute(%p: !felt.type) -> !struct.type<@Main> {
      // ...
    }
    // %self is not a signal, but again, %p is a private input signal
    function.def @constrain(%self: !struct.type<@Main>, %p: !felt.type) {
      // ...
    }
  }
}

Traits: HasOnlyGraphRegion, HasParent<::mlir::ModuleOp, llzk::polymorphic::TemplateOp>, IsolatedFromAbove, LLZKSymbolTableImplTrait, NoRegionArguments, NoTerminator, SetFuncAllowAttrs, SingleBlock, SymbolTable

Interfaces: ContractTarget, RegionKindInterface, Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute

struct.member (::llzk::component::MemberDefOp)

Struct member definition

Syntax:

operation ::= `struct.member` $sym_name `:` $type attr-dict

This operation describes a member in a struct/component.

Example:

struct.member @f1 : !felt.type
struct.member @f2 : !felt.type {llzk.pub}
struct.member @col1 : !felt.type {column}
struct.member @sig1 : !felt.type {signal}
struct.member @colsig1 : !felt.type {column, signal}
struct.member @pubcol : !felt.type {llzk.pub, column}

Members marked with the {llzk.pub} attribute are considered public and represent outputs of their defining struct/component.
Members marked with the {column} attribute can be read/written with table offsets using the readm and writem operations.
Members marked with the {signal} attribute are constraint variables that are stored in the witness; non-signal values are intermediate expressions.

Further restrictions on the signal attribute:

It is only used on struct members, since they represent storage locations. It is not used to mark struct inputs, as struct may be passed signal or non-signal (i.e., intermediate expression) values.
Only !felt.type or simple aggregates of !felt.type (i.e., !array.type and !pod.type) may be marked as signals.

Traits: HasParent<::llzk::component::StructDefOp>

Interfaces: SymbolUserOpInterface, Symbol

Attributes:

Attribute	MLIR Type	Description
`sym_name`	::mlir::StringAttr	string attribute
`type`	::mlir::TypeAttr	type attribute of a valid LLZK type
`column`	::mlir::UnitAttr	unit attribute
`signal`	::mlir::UnitAttr	unit attribute

struct.new (::llzk::component::CreateStructOp)

Create a new struct

Syntax:

operation ::= `struct.new` `:` type($result) attr-dict

This operation creates a new, uninitialized instance of a struct.

Example:

%self = struct.new : !struct.type<@Reg>

Traits: WitnessGen

Interfaces: OpAsmOpInterface, SymbolUserOpInterface

Results:

Result	Description
result	circuit component

struct.readm (::llzk::component::MemberReadOp)

Read value of a struct member

Syntax:

operation ::= `struct.readm` $component `[` $member_name `]`
              ( `{` custom<MultiDimAndSymbolList>($mapOperands, $numDimsPerMap)^ `}` )?
              `:` type($component) `,` type($val)
              attr-dict

This operation copies the value of a named member in a struct/component. The result is a value copy, not a pointer or alias to the member's storage. When the member itself has struct.type, the copied value is an identity-bearing handle to the same component instance.

A struct can read its own members regardless of whether they are marked as public (i.e., with the llzk.pub attribute) or private (members without the llzk.pub attribute). However, when reading members of other components, only public members can be accessed. Free functions may also only read public members.

The value can be read from the signals table, in which case it can be offset by a constant value. A negative value represents reading a value backwards and a positive value represents reading a value forward. Only members marked as columns can be read in this manner.

Traits: VerifySizesForMultiAffineOps<1>

Interfaces: MemberRefOpInterface, MemoryEffectOpInterface (MemoryEffectOpInterface), SymbolUserOpInterface

Effects: MemoryEffects::Effect{MemoryEffects::Read on ::mlir::SideEffects::DefaultResource}

Attributes:

Attribute	MLIR Type	Description
`member_name`	::mlir::FlatSymbolRefAttr	flat symbol reference attribute
`tableOffset`	::mlir::Attribute	symbol reference attribute or index attribute or AffineMap attribute
`numDimsPerMap`	::mlir::DenseI32ArrayAttr	i32 dense array attribute
`mapOpGroupSizes`	::mlir::DenseI32ArrayAttr	i32 dense array attribute

Operands:

Operand	Description
component	circuit component
mapOperands	variadic of index

Results:

Result	Description
val	a valid LLZK type

struct.writem (::llzk::component::MemberWriteOp)

Write value to a struct member

Syntax:

operation ::= `struct.writem` $component `[` $member_name `]` `=` $val `:` type($component) `,` type($val) attr-dict

This operation copies a value to a named member in a struct/component. It does not create a pointer or alias between the source value and the member's storage. When the value has struct.type, the copied value is an identity-bearing handle to the same component instance.

A struct can write its own members. However, writing members of other components is not allowed.

Traits: WitnessGen

Interfaces: MemberRefOpInterface, MemoryEffectOpInterface (MemoryEffectOpInterface), SymbolUserOpInterface

Effects: MemoryEffects::Effect{MemoryEffects::Write on ::mlir::SideEffects::DefaultResource}

Attributes:

Attribute	MLIR Type	Description
`member_name`	::mlir::FlatSymbolRefAttr	flat symbol reference attribute

Operands:

Operand	Description
component	circuit component
val	a valid LLZK type

Types

StructType

Circuit component

Syntax:

!struct.type<
  ::mlir::SymbolRefAttr,   # nameRef
  ::mlir::ArrayAttr   # params
>

Type of a struct op instance. Struct values are identity-bearing, pointer-like handles to mutable component instances rather than bags of member values. Copying a struct value copies the handle and preserves the identity of the referenced component; it does not duplicate the component's members, signals, or tables.

For structs that contain template parameters, the type must contain a list of attributes that instantiate the template parameters, one per parameter. Each attribute must be one of the following:

IntegerAttr (with IndexType), specifying a fixed parameter value; the wildcard (?) is not allowed
SymbolRefAttr, specifying a parameter value defined by a struct parameter or global constant
AffineMapAttr, for an array of struct elements whose template parameters vary based on some fixed pattern.
TypeAttr, for specifying a type parameter.

// Type for struct `A` with no parameters.
!struct.type<@A>
 
// Type for struct `B` with IntegerAttr and SymbolRefAttr parameters.
!struct.type<@B<[5, @C]>>
 
// Type for struct `C` with TypeAttr and IntegerAttr parameters.
!struct.type<@C<[!felt.type, 24]>>

Parameters:

Parameter	C++ type	Description
nameRef	::mlir::SymbolRefAttr	Fully-qualified name of the struct definition.
params	::mlir::ArrayAttr	Struct parameters

Table of Contents

'array' Dialect

Operations

array.extract (::llzk::array::ExtractArrayOp)

Operands:

Results:

array.insert (::llzk::array::InsertArrayOp)

Operands:

array.len (::llzk::array::ArrayLengthOp)

Operands:

Results:

array.new (::llzk::array::CreateArrayOp)

Attributes:

Operands:

Results:

array.read (::llzk::array::ReadArrayOp)

Operands:

Results:

array.write (::llzk::array::WriteArrayOp)

Operands:

Types

ArrayType

Parameters:

'bool' Dialect

Operations

bool.and (::llzk::boolean::AndBoolOp)

Operands:

Results:

bool.assert (::llzk::boolean::AssertOp)

Attributes:

Operands:

bool.cmp (::llzk::boolean::CmpOp)

Attributes:

Operands:

Results:

bool.exists (::llzk::boolean::ExistsOp)

Operands:

Results:

bool.forall (::llzk::boolean::ForAllOp)

Operands:

Results:

bool.not (::llzk::boolean::NotBoolOp)

Operands:

Results:

bool.or (::llzk::boolean::OrBoolOp)

Operands:

Results:

bool.xor (::llzk::boolean::XorBoolOp)

Operands:

Results:

bool.yield (::llzk::boolean::YieldOp)

Operands:

Attributes

FeltCmpPredicateAttr

Parameters:

Enums

FeltCmpPredicate

Cases:

'cast' Dialect

Operations

cast.tofelt (::llzk::cast::IntToFeltOp)

Attributes:

Operands:

Results:

cast.toindex (::llzk::cast::FeltToIndexOp)

Attributes:

Operands:

Results:

Attributes

OverflowSemanticsAttr

Parameters:

Enums

OverflowSemantics

Cases:

'constrain' Dialect

Operations

constrain.eq (::llzk::constrain::EmitEqualityOp)

Operands:

constrain.in (::llzk::constrain::EmitContainmentOp)

Operands: