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

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::APIntValue   # value
>

Parameters:

Parameter	C++ type	Description
value	llzk::APIntValue	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::APIntValue   # value
>

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

Parameters:

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

Types

BoolType

Boolean in {0,1}

Syntax: !pcl.bool

FeltType

Finite field element

Syntax: !pcl.felt