'array' Dialect
- Operations
- Types
  - ArrayType
    - Parameters:
'bool' Dialect
'cast' Dialect
- Operations
  - cast.tofelt (llzk::cast::IntToFeltOp)
    - Operands:
    - Results:
  - cast.toindex (llzk::cast::FeltToIndexOp)
    - Operands:
    - Results:
'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 new array with the given elements. 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: AlwaysSpeculatableImplTrait, AttrSizedOperandSegments, VerifySizesForMultiAffineOps<1>

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

Effects: MemoryEffects::Effect{}

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 reads the value from an array at the specified position.

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, 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 writes a value into an array at the specified position.

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, 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
IndexType
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.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

Attributes

FeltCmpPredicateAttr

Field element comparison predicate

Syntax:

#bool.cmp<
  ::llzk::boolean::FeltCmpPredicate   # value
>

Enum cases:

eq (EQ)
ne (NE)
lt (LT)
le (LE)
gt (GT)
ge (GE)

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` $value `:` type($value) `` custom<InferredOrParsedType>(type($result), "false") attr-dict

This operation converts a supported integer type value into a field element value.

Example:

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

%1 = cast.tofelt %0 : i1

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

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` $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.

Example:

%0 = cast.toindex %a

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

Traits: AlwaysSpeculatableImplTrait, NotFieldNative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	finite field element

Results:

Result	Description
result	index

'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 felt-typed SSA value holding an integer constant.

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

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

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 represents a finite field element.

Parameters:

Parameter	C++ type	Description
value	::llvm::APInt	The felt constant value
type	FeltType

FieldSpecAttr

prime field specification

A specification of a prime field for use by felt types.

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
koalabear
mersenne31

Parameters:

Parameter	C++ type	Description
fieldName	::mlir::StringAttr
prime	::llvm::APInt	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.

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]>>

Traits: AttrSizedOperandSegments, MemRefsNormalizable, VerifySizesForMultiAffineOps<1>

Interfaces: CallOpInterface, 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

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.

Example:

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

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

Interfaces: CallableOpInterface, 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

Syntax:

operation ::= `global.def` (`const` $constant^)?
              $sym_name `:` $type
              `` custom<GlobalInitialValue>($initial_value, ref($type))
              attr-dict

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>

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` $name_ref `:` type($val) attr-dict

This operation reads the value of a named global.

Interfaces: GlobalRefOpInterface, SymbolUserOpInterface

Attributes:

Attribute	MLIR Type	Description
`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 writes a value to a named global. Not allowed for globals declared with the "const" modifier.

Traits: WitnessGen

Interfaces: GlobalRefOpInterface, SymbolUserOpInterface

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

Annotation with the bounds of a loop

Syntax:

#llzk.loopbounds<
  ::llvm::APInt,   # lower
  ::llvm::APInt,   # upper
  ::llvm::APInt   # step
>

This attribute holds information useful for the analysis of loops. Holds the bounds of the loop and the step size.

Example:

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

Parameters:

Parameter	C++ type	Description
lower	::llvm::APInt	Loop variable lower bound (inclusive)
upper	::llvm::APInt	Loop variable upper bound (exclusive)
step	::llvm::APInt	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_felt 1 
%1 = pod.new { @n = %0 } : !pod.type<[@n: !felt.type]>
 
// Another one, but with 2 fields
%0 = felt.const_felt 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_felt 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_felt 5 
%2 = pod.new { @f = %1 }(%0)[%c] : !pod.type<[@f: !felt.type, @a: !array.type<#map, !felt.type>]>

Traits: AlwaysSpeculatableImplTrait, AttrSizedOperandSegments, VerifySizesForMultiAffineOps<1>

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface), OpAsmOpInterface

Effects: MemoryEffects::Effect{}

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

Reads the current value of a named record from a pod instance. Returns one value of the type of the record.

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

Attributes:

Attribute	MLIR Type	Description
`record_name`	::mlir::FlatSymbolRefAttr	flat symbol reference 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

Writes a value into a named record of a pod instance. This operation has no result values.

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

Attributes:

Attribute	MLIR Type	Description
`record_name`	::mlir::FlatSymbolRefAttr	flat symbol reference 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 struct parameter

Syntax:

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

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

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 refering to a struct nested within the template. In the example above, the type of @StructName is !struct.type<@TemplateName::@StructName<[@N, @T]>>.

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: 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 reads the value of a named member in a struct/component.

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, SymbolUserOpInterface

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 writes a value to a named member in a struct/component.

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

Traits: WitnessGen

Interfaces: MemberRefOpInterface, SymbolUserOpInterface

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. 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
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.not (::llzk::boolean::NotBoolOp)

Operands:

Results:

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

Operands:

Results:

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

Operands:

Results:

Attributes

FeltCmpPredicateAttr

Parameters:

Enums

FeltCmpPredicate

Cases:

'cast' Dialect

Operations

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

Operands:

Results:

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

Operands:

Results:

'constrain' Dialect

Operations

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

Operands:

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

Operands:

'felt' Dialect

Operations

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

Operands:

Results:

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

Operands:

Results:

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

Operands:

Results:

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

Operands:

Results:

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

Operands: