LLZK Dialects

Table of Contents

• 'array' Dialect
  • Types
• 'bool' Dialect
  • Operations
  • Attributes
• 'cast' Dialect
  • Operations
• 'constrain' Dialect
  • Operations
• 'felt' Dialect
  • Operations
  • Attributes
  • Types
• 'function' Dialect
  • Operations
• 'global' Dialect
  • Operations
• 'include' Dialect
  • Operations
• 'llzk' Dialect
  • Attributes
• 'poly' Dialect
  • Operations
  • Types
• 'string' Dialect
  • Operations
  • Types
• 'struct' Dialect
  • Operations
  • Types
• 'undef' Dialect
  • Operations

'array' Dialect

LLZK array operations.

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 types:

• Any LLZK type
• IndexType
• Unsigned integers of 1 bit (aka booleans)

// 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.

Traits: AlwaysSpeculatableImplTrait, Commutative, WitnessGen

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 `)` 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)

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.

Traits: AlwaysSpeculatableImplTrait, WitnessGen

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.

Traits: AlwaysSpeculatableImplTrait, Commutative, WitnessGen

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.

Traits: AlwaysSpeculatableImplTrait, Commutative, WitnessGen

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

'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) 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, 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 attr-dict

This operation converts a field element value into an index value to allow use as an array index or loop bound. In struct @constrain functions, the argument to this op is not allowed to be derived from a Signal struct.

Example:

%0 = cast.toindex %a
%1 = array.read %b[%0]

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, 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. For the built-in Signal struct, the constraint is performed on the Signal's inner @reg felt field.

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

Interfaces: ConstraintOpInterface, SymbolUserOpInterface

Operands:

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

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

Emit a containment constraint

Syntax:

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

Traits: ConstraintGen

Interfaces: ConstraintOpInterface, SymbolUserOpInterface

Operands:

Operand	Description
lhs	n-dimensional array
rhs	a valid array element 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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Bit flip operator for field elements

Syntax:

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

Traits: AlwaysSpeculatableImplTrait, WitnessGen

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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 = llzk.const 42

Traits: AlwaysSpeculatableImplTrait, ConstantLike

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	finite field element

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

Division operator for field elements

Syntax:

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

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Inverse operator for field elements

Syntax:

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

Traits: AlwaysSpeculatableImplTrait, WitnessGen

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	finite field element

felt.mod (::llzk::felt::ModFeltOp)

Modulus/remainder operator for field elements

Syntax:

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

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Negation operator for field elements

Syntax:

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

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
operand	finite field element or type variable

Results:

Result	Description
result	finite field element

felt.nondet (::llzk::felt::FeltNonDetOp)

Uninitialized field element

Syntax:

operation ::= `felt.nondet` attr-dict

This operation produces a felt-typed SSA value without a specified value. This can be used in constrain() functions in place of expressions that cannot be included in constraints.

Example:

%0 = llzk.nondet

Traits: AlwaysSpeculatableImplTrait, ConstantLike

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

Effects: MemoryEffects::Effect{}

Results:

Result	Description
result	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

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

Interfaces: ConditionallySpeculatable, 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	finite field element

Attributes

FeltConstAttr

finite field element

Syntax:

#felt.felt.const<
  ::llvm::APInt   # value
>

A felt attribute represents a finite field element.

Parameters:

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

Types

FeltType

finite field element

Syntax: !felt.type

'function' Dialect

LLZK function operations.

Operations

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

Call operation

Syntax:

operation ::= `function.call` $callee `(` $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
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 or attributes that establish a symbolic connection (e.g. symbols referenced by name via a string attribute like SymbolRefAttr). An external function declaration (used when referring to a function declared in some other module) has no body. While the MLIR textual form provides a nice inline syntax for function arguments, they are internally represented as “block arguments” to the first block in the region.

Only dialect attribute names may be specified in the attribute dictionaries for function arguments, results, or the function itself.

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

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 a type as public

Syntax: #llzk.pub

Examples:

struct.field @field_name : !felt.type {llzk.pub}
 
function.def @func_name(%0: !felt.type {llzk.pub})

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

Interfaces: SymbolUserOpInterface

Attributes:

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

Results:

Result	Description
val	integral, felt, or typevar type

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

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.

struct.def @A<[@Ty]> {
  field @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 (`<` $const_params^ `>`)? $body attr-dict

This operation describes a component in a circuit. It can contain any number of fields 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 {
  field @f1 : !array.type<5 x index>
  field @f2 : !felt.type {llzk.pub}
 
  function.def @compute(%p: !felt.type) -> !struct.type<@ComponentA> {
    %self = struct.new : !struct.type<@ComponentA>
    // initialize all fields of `%self` here
    return %self : !struct.type<@ComponentA>
  }
 
  function.def @constrain(%self: !struct.type<@ComponentA>, %p: !felt.type) {
    // emit constraints here
    return
  }
}

Traits: HasOnlyGraphRegion, HasParent<::mlir::ModuleOp>, IsolatedFromAbove, NoTerminator, SetFuncAllowAttrs, SingleBlock, SymbolTable

Interfaces: RegionKindInterface, SymbolUserOpInterface, Symbol

Attributes:

Attribute	MLIR Type	Description
sym_name	::mlir::StringAttr	string attribute
const_params	::mlir::ArrayAttr	flat symbol ref array attribute

struct.field (::llzk::component::FieldDefOp)

Struct field definition

Syntax:

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

This operation describes a field in a struct/component.

Example:

struct.field @f1 : !felt.type
struct.field @f2 : !felt.type {llzk.pub}

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

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.readf (::llzk::component::FieldReadOp)

Read value of a struct field

Syntax:

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

This operation reads the value of a named field in a struct/component.

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 fields marked as columns can be read in this manner.

Traits: VerifySizesForMultiAffineOps<1>

Interfaces: FieldRefOpInterface, SymbolUserOpInterface

Attributes:

Attribute	MLIR Type	Description
field_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.writef (::llzk::component::FieldWriteOp)

Write value to a struct field

Syntax:

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

This operation writes a value to a named field in a struct/component.

Traits: WitnessGen

Interfaces: FieldRefOpInterface, SymbolUserOpInterface

Attributes:

Attribute	MLIR Type	Description
field_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
>

Parameters:

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

'undef' Dialect

LLZK undefined value support operations.

Operations

undef.undef (::llzk::undef::UndefOp)

Creates an undefined value of the specified type.

Syntax:

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

This operation has no operands or attributes. It represents an undefined value of the specified LLZK IR dialect type. This op can 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 = undef.undef : !felt.type

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Results:

Result	Description
res	a valid LLZK type