ZKLean Backend

Table of Contents

• 'ZKExpr' Dialect
  • Operations
    • ZKExpr.Add (::llzk::zkexpr::AddOp)
      • Operands:
      • Results:
    • ZKExpr.Literal (::llzk::zkexpr::LiteralOp)
      • Operands:
      • Results:
    • ZKExpr.Mul (::llzk::zkexpr::MulOp)
      • Operands:
      • Results:
    • ZKExpr.Neg (::llzk::zkexpr::NegOp)
      • Operands:
      • Results:
    • ZKExpr.Sub (::llzk::zkexpr::SubOp)
      • Operands:
      • Results:
  • Types
    • ComposedLookupTableType
      • Parameters:
    • WitnessIDType
    • ZKExprType
• 'ZKBuilder' Dialect
  • Operations
    • ZKBuilder.AllocWitness (::llzk::zkbuilder::AllocWitnessOp)
      • Results:
    • ZKBuilder.ConstrainEq (::llzk::zkbuilder::ConstrainEqOp)
      • Operands:
      • Results:
    • ZKBuilder.ConstrainR1CS (::llzk::zkbuilder::ConstrainR1CSOp)
      • Operands:
      • Results:
  • Types
    • ZKBuilderStateType
• 'ZKLeanLean' Dialect
  • Operations
    • ZKLeanLean.accessor (::llzk::zkleanlean::AccessorOp)
      • Attributes:
      • Operands:
      • Results:
    • ZKLeanLean.call (::llzk::zkleanlean::CallOp)
      • Attributes:
      • Operands:
      • Results:
    • ZKLeanLean.member (::llzk::zkleanlean::MemberDefOp)
      • Attributes:
    • ZKLeanLean.structure (::llzk::zkleanlean::StructDefOp)
      • Attributes:
  • Types
    • StructType
      • Parameters:

'ZKExpr' Dialect

A dialect for zkexpr

The ZKExpr dialect defines types and operations for ZK Expressions from the ZK Lean project.

Operations

ZKExpr.Add (::llzk::zkexpr::AddOp)

Addition operation between ZK Expressions.

Syntax:

operation ::= `ZKExpr.Add` $lhs $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Elementwise, SameOperandsAndResultType, Scalarizable, Tensorizable, Vectorizable

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	ZK Expressions
rhs	ZK Expressions

Results:

Result	Description
output	ZK Expressions

ZKExpr.Literal (::llzk::zkexpr::LiteralOp)

Introduce ZK literal

Syntax:

operation ::= `ZKExpr.Literal` $literal attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
literal	finite field element

Results:

Result	Description
output	ZK Expressions

ZKExpr.Mul (::llzk::zkexpr::MulOp)

Multiplication operation between ZK Expressions.

Syntax:

operation ::= `ZKExpr.Mul` $lhs $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Elementwise, SameOperandsAndResultType, Scalarizable, Tensorizable, Vectorizable

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	ZK Expressions
rhs	ZK Expressions

Results:

Result	Description
output	ZK Expressions

ZKExpr.Neg (::llzk::zkexpr::NegOp)

Negate a ZK Expression

Syntax:

operation ::= `ZKExpr.Neg` $value attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	ZK Expressions

Results:

Result	Description
output	ZK Expressions

ZKExpr.Sub (::llzk::zkexpr::SubOp)

Subtraction operation between ZK Expressions.

Syntax:

operation ::= `ZKExpr.Sub` $lhs $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Elementwise, SameOperandsAndResultType, Scalarizable, Tensorizable, Vectorizable

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	ZK Expressions
rhs	ZK Expressions

Results:

Result	Description
output	ZK Expressions

Types

ComposedLookupTableType

Lookup table parameterized by table dimensions

Syntax:

!ZKExpr.composedlookuptable<
  int,   # cols
  int   # rows
>

Parameters:

Parameter	C++ type	Description
cols	int
rows	int

WitnessIDType

WitnessID

Syntax: !ZKExpr.Witnessid

ZKExprType

ZK Expressions

Syntax: !ZKExpr.zkexpr

'ZKBuilder' Dialect

Dialect for ZKBuilder

The ZKBuilder dialect defines types and operations for ZK Builders from the ZK Lean project.

Operations

ZKBuilder.AllocWitness (::llzk::zkbuilder::AllocWitnessOp)

Allocate a witness value

Syntax:

operation ::= `ZKBuilder.AllocWitness` attr-dict

Traits: ConstantLike

Interfaces: InferTypeOpInterface

Results:

Result	Description
output	ZK Expressions

ZKBuilder.ConstrainEq (::llzk::zkbuilder::ConstrainEqOp)

Constrain two ZK Expressions to be equal

Syntax:

operation ::= `ZKBuilder.ConstrainEq` $lhs $rhs attr-dict

Interfaces: InferTypeOpInterface

Operands:

Operand	Description
lhs	ZK Expressions
rhs	ZK Expressions

Results:

Result	Description
output	State of the ZKBuilder

ZKBuilder.ConstrainR1CS (::llzk::zkbuilder::ConstrainR1CSOp)

Constrain R1CS in the Builder State

Syntax:

operation ::= `ZKBuilder.ConstrainR1CS` $a $b $c attr-dict

Interfaces: InferTypeOpInterface

Operands:

Operand	Description
a	ZK Expressions
b	ZK Expressions
c	ZK Expressions

Results:

Result	Description
output	State of the ZKBuilder

Types

ZKBuilderStateType

State of the ZKBuilder

Syntax: !ZKBuilder.zkbuilderstate

'ZKLeanLean' Dialect

A dialect for ZKLean Lean primitives

The ZKLeanLean dialect defines types and operations for Lean-facing primitives, including struct definitions, field access, and function calls.

Operations

ZKLeanLean.accessor (::llzk::zkleanlean::AccessorOp)

Access member of a struct

Syntax:

operation ::= `ZKLeanLean.accessor` $component `[` $member_name `]` `:` type($component) `,` type($value) attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

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

Operands:

Operand	Description
component	ZKLean struct value type

Results:

Result	Description
value	ZK Expressions

ZKLeanLean.call (::llzk::zkleanlean::CallOp)

Call a Lean function

Syntax:

operation ::= `ZKLeanLean.call` $callee `(` $args `)` `:` functional-type($args, results) attr-dict

Represents a call to a Lean function by name with explicit argument and result types.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
callee	::mlir::SymbolRefAttr	symbol reference attribute

Operands:

Operand	Description
args	variadic of any type

Results:

Result	Description
results	variadic of any type

ZKLeanLean.member (::llzk::zkleanlean::MemberDefOp)

ZKLean struct member definition

Syntax:

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

Traits: HasParent<::llzk::zkleanlean::StructDefOp>

Interfaces: Symbol

Attributes:

Attribute	MLIR Type	Description
sym_name	::mlir::StringAttr	string attribute
type	::mlir::TypeAttr	type attribute of ZK Expressions

ZKLeanLean.structure (::llzk::zkleanlean::StructDefOp)

ZKLean struct definition

Syntax:

operation ::= `ZKLeanLean.structure` $sym_name $bodyRegion attr-dict

Defines a ZKLean struct with named members. Only member definitions are allowed in the body region.

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

Interfaces: RegionKindInterface, Symbol

Attributes:

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

Types

StructType

ZKLean struct value type

Syntax:

!ZKLeanLean.type<
  ::mlir::SymbolRefAttr   # nameRef
>

Type of a ZKLean struct instance. The referenced struct definition is identified by a symbol reference.

Parameters:

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