PCL Backend

Table of Contents

• 'pcl' Dialect
  • Operations
    • pcl.add (::pcl::AddOp)
      • Operands:
      • Results:
    • pcl.and (::pcl::AndOp)
      • Operands:
      • Results:
    • pcl.asfelt (::pcl::AsFeltOp)
      • Operands:
      • Results:
    • pcl.assert (::pcl::AssertOp)
      • Operands:
    • pcl.assume.deterministic (::pcl::AssumeDeterministicOp)
      • Operands:
    • pcl.const (::pcl::ConstOp)
      • Attributes:
      • Results:
    • pcl.det (::pcl::DetOp)
      • Operands:
      • Results:
    • pcl.eq (::pcl::CmpEqOp)
      • Operands:
      • Results:
    • pcl.false (::pcl::FalseOp)
      • Results:
    • pcl.ge (::pcl::CmpGeOp)
      • Operands:
      • Results:
    • pcl.gt (::pcl::CmpGtOp)
      • Operands:
      • Results:
    • pcl.iff (::pcl::IffOp)
      • Operands:
      • Results:
    • pcl.implies (::pcl::ImpliesOp)
      • Operands:
      • Results:
    • pcl.le (::pcl::CmpLeOp)
      • Operands:
      • Results:
    • pcl.lt (::pcl::CmpLtOp)
      • Operands:
      • Results:
    • pcl.mul (::pcl::MulOp)
      • Operands:
      • Results:
    • pcl.neg (::pcl::NegOp)
      • Operands:
      • Results:
    • pcl.not (::pcl::NotOp)
      • Operands:
      • Results:
    • pcl.or (::pcl::OrOp)
      • Operands:
      • Results:
    • pcl.post_cond (::pcl::PostOp)
      • Operands:
    • pcl.sub (::pcl::SubOp)
      • Operands:
      • Results:
    • pcl.true (::pcl::TrueOp)
      • Results:
    • pcl.var (::pcl::VarOp)
      • Attributes:
      • Results:
  • Attributes
    • FeltAttr
      • Parameters:
    • BoolAttr
      • Parameters:
    • PrimeAttr
      • Parameters:
  • Types
    • BoolType
    • FeltType
  • Lowering pipeline
  • Integer values

Allows LLZK to be lowered to PCL (Picus Constraint Language) for use with the Picus verifier

'pcl' Dialect

PCL

Operations

pcl.add (::pcl::AddOp)

Field addition

Syntax:

operation ::= `pcl.add` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Finite field element

pcl.and (::pcl::AndOp)

Boolean conjunction (lhs && rhs)

Syntax:

operation ::= `pcl.and` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Boolean in {0,1}
rhs	Boolean in {0,1}

Results:

Result	Description
result	Boolean in {0,1}

pcl.asfelt (::pcl::AsFeltOp)

Bool to felt conversion

Syntax:

operation ::= `pcl.asfelt` $value attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	Boolean in {0,1}

Results:

Result	Description
result	Finite field element

pcl.assert (::pcl::AssertOp)

Assert that a boolean holds

Syntax:

operation ::= `pcl.assert` $cond attr-dict

Operands:

Operand	Description
cond	Boolean in {0,1}

pcl.assume.deterministic (::pcl::AssumeDeterministicOp)

Assume the given value is deterministic

Syntax:

operation ::= `pcl.assume.deterministic` $v attr-dict

Operands:

Operand	Description
v	Finite field element

pcl.const (::pcl::ConstOp)

Constant felt

Syntax:

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

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
value	::pcl::FeltAttr	Field element represented as an arbitrary precision integer

Results:

Result	Description
res	Finite field element

pcl.det (::pcl::DetOp)

Returns true iff $expr deterministic

Syntax:

operation ::= `pcl.det` $value attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.eq (::pcl::CmpEqOp)

Lhs == rhs (field equality)

Syntax:

operation ::= `pcl.eq` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.false (::pcl::FalseOp)

Constant false value

Syntax:

operation ::= `pcl.false` attr-dict

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Results:

Result	Description
res	Boolean in {0,1}

pcl.ge (::pcl::CmpGeOp)

Lhs >= rhs

Syntax:

operation ::= `pcl.ge` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.gt (::pcl::CmpGtOp)

Lhs > rhs

Syntax:

operation ::= `pcl.gt` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.iff (::pcl::IffOp)

Boolean equivalence (lhs <=> rhs)

Syntax:

operation ::= `pcl.iff` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Boolean in {0,1}
rhs	Boolean in {0,1}

Results:

Result	Description
result	Boolean in {0,1}

pcl.implies (::pcl::ImpliesOp)

Boolean implication (lhs => rhs)

Syntax:

operation ::= `pcl.implies` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Boolean in {0,1}
rhs	Boolean in {0,1}

Results:

Result	Description
result	Boolean in {0,1}

pcl.le (::pcl::CmpLeOp)

Lhs <= rhs

Syntax:

operation ::= `pcl.le` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.lt (::pcl::CmpLtOp)

Lhs < rhs

Syntax:

operation ::= `pcl.lt` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Boolean in {0,1}

pcl.mul (::pcl::MulOp)

Field multiplication

Syntax:

operation ::= `pcl.mul` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Finite field element

pcl.neg (::pcl::NegOp)

Field negation

Syntax:

operation ::= `pcl.neg` $value attr-dict

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	Finite field element

Results:

Result	Description
result	Finite field element

pcl.not (::pcl::NotOp)

Boolean negation (!cond)

Syntax:

operation ::= `pcl.not` $value attr-dict

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	Boolean in {0,1}

Results:

Result	Description
result	Boolean in {0,1}

pcl.or (::pcl::OrOp)

Boolean disjunction (lhs || rhs)

Syntax:

operation ::= `pcl.or` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, Commutative, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Boolean in {0,1}
rhs	Boolean in {0,1}

Results:

Result	Description
result	Boolean in {0,1}

pcl.post_cond (::pcl::PostOp)

Post-condition on function outputs

Syntax:

operation ::= `pcl.post_cond` $cond attr-dict

Operands:

Operand	Description
cond	Boolean in {0,1}

pcl.sub (::pcl::SubOp)

Field subtraction

Syntax:

operation ::= `pcl.sub` $lhs `,` $rhs attr-dict

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	Finite field element
rhs	Finite field element

Results:

Result	Description
result	Finite field element

pcl.true (::pcl::TrueOp)

Constant true value

Syntax:

operation ::= `pcl.true` attr-dict

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Results:

Result	Description
res	Boolean in {0,1}

pcl.var (::pcl::VarOp)

Declare a felt variable.

Syntax:

operation ::= `pcl.var` $name $is_output attr-dict

The var op creates a new variable associated with a name. It additionally takes a parameter is_output which indicates an output variable if true and an intermediate otherwise.

Example:

%0 = pcl.def "foo" true // output
%1 = pcl.def "bar" false // intermediate

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
name	::mlir::StringAttr	string attribute
is_output	::mlir::BoolAttr	bool attribute

Results:

Result	Description
res	Finite field element

Attributes

FeltAttr

Field element represented as an arbitrary precision integer

Syntax:

#pcl.felt<
  ::llzk::DynamicAPIntValue   # value
>

Parameters:

Parameter	C++ type	Description
value	llzk::DynamicAPIntValue	felt constant value

BoolAttr

Boolean value

Syntax:

#pcl.bool<
  bool   # value
>

Parameters:

Parameter	C++ type	Description
value	bool

PrimeAttr

Prime field modulus for this module

Syntax:

#pcl.prime<
  ::llzk::DynamicAPIntValue   # value
>

Attach this as a named attribute (e.g. pcl.prime) on builtin.module. Use a signed arbitrary-precision literal so very large primes are supported.

Parameters:

Parameter	C++ type	Description
value	llzk::DynamicAPIntValue	field prime modulus

Types

BoolType

Boolean in {0,1}

Syntax: !pcl.bool

FeltType

Finite field element

Syntax: !pcl.felt

Lowering pipeline

Run llzk-opt input.llzk --llzk-full-pcl-lowering to normalize while loops, canonicalize loop bounds, flatten templates and unroll loops rooted at llzk.main, then scalarize PODs and arrays before converting to PCL. Canonicalization also runs after flattening and scalarization. Common subexpression elimination runs before and after POD/array scalarization, followed by redundant read/write elimination before PCL conversion.

This pipeline preserves component boundaries; it does not inline structs or free functions. Existing PCL restrictions still apply, including the requirement that each struct has a public output. In particular, assertion-only components and a main component with no public outputs still require separate handling.

Use --llzk-to-pcl directly when the input has already been prepared.

When PCL is enabled, C clients can append the pipeline to a module pass manager with llzkBuildFullPCLLoweringPipeline. Alternatively, call llzkRegisterPCLConversionPassPipelines and parse builtin.module(llzk-full-pcl-lowering) with mlirParsePassPipeline.

Integer values

PCL felt constants and prime moduli use signed arbitrary-precision integers. Arithmetic intermediates grow as needed and are reduced modulo the module's prime. Literal storage widths have no semantic meaning. During LLZK-to-PCL conversion, the prime modulus is inferred from the felt types used across the circuit and stored in the top-level module's pcl.prime attribute. Conversion requires a single field for the entire circuit. Its value must be at least two; the PCL verifier does not check primality.