Backend Dialects

Table of Contents

• 'r1cs' Dialect
  • Operations
    • r1cs.add (::r1cs::AddOp)
      • Operands:
      • Results:
    • r1cs.circuit (::r1cs::CircuitDefOp)
      • Attributes:
    • r1cs.const (::r1cs::ConstOp)
      • Attributes:
      • Results:
    • r1cs.constrain (::r1cs::ConstrainOp)
      • Operands:
    • r1cs.def (::r1cs::SignalDefOp)
      • Attributes:
      • Results:
    • r1cs.mul_const (::r1cs::MulConstOp)
      • Attributes:
      • Operands:
      • Results:
    • r1cs.neg (::r1cs::NegOp)
      • Operands:
      • Results:
    • r1cs.to_linear (::r1cs::ToLinearOp)
      • Operands:
      • Results:
  • Attributes
    • FeltAttr
      • Parameters:
    • PublicAttr
  • Types
    • LinearType
    • SignalType

'r1cs' Dialect

R1CS

Operations

r1cs.add (::r1cs::AddOp)

Add two linear expressions

Syntax:

operation ::= `r1cs.add` $lhs `,` $rhs attr-dict `:` type($sum)

Traits: AlwaysSpeculatableImplTrait, Commutative

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
lhs	R1CS linear expression type
rhs	R1CS linear expression type

Results:

Result	Description
sum	R1CS linear expression type

r1cs.circuit (::r1cs::CircuitDefOp)

Defines an R1CS circuit with labeled inputs and constraints

The r1cs.circuit operation defines a named circuit, with explicit inputs and internally declared signals and constraints.

Signals defined with r1cs.def and marked public are considered outputs.

Example:

r1cs.circuit @CmpConstraint inputs (%arg0: !r1cs.signal {#r1cs.pub}, %arg1: !r1cs.signal, %arg2: !r1cs.signal) {
    %0 = r1cs.def 0 : !r1cs.signal {pub = #r1cs.pub}
    %1 = r1cs.def 1 : !r1cs.signal
    %2 = r1cs.def 2 : !r1cs.signal
    %3 = r1cs.to_linear %arg1 : !r1cs.signal to !r1cs.linear
    %4 = r1cs.to_linear %arg2 : !r1cs.signal to !r1cs.linear
    %5 = r1cs.to_linear %1 : !r1cs.signal to !r1cs.linear
    %6 = r1cs.mul_const %5,  -1 : i64 : !r1cs.linear
    r1cs.constrain %3, %4, %6 : !r1cs.linear
}

Traits: IsolatedFromAbove, NoTerminator, SingleBlock

Interfaces: Symbol

Attributes:

Attribute	MLIR Type	Description
sym_name	::mlir::StringAttr	string attribute
arg_attrs	::mlir::DictionaryAttr	dictionary of named attribute values

r1cs.const (::r1cs::ConstOp)

Create a constant linear value

Syntax:

operation ::= `r1cs.const` $value attr-dict `:` type($out)

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

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

Results:

Result	Description
out	R1CS linear expression type

r1cs.constrain (::r1cs::ConstrainOp)

Enforce a * b - c = 0 R1CS constraint

Syntax:

operation ::= `r1cs.constrain` $a `,` $b `,` $c attr-dict `:` type($a)

Operands:

Operand	Description
a	R1CS linear expression type
b	R1CS linear expression type
c	R1CS linear expression type

r1cs.def (::r1cs::SignalDefOp)

Define a signal with label and optional public visibility

Syntax:

operation ::= `r1cs.def` $label `:` type($out) attr-dict

The def op creates a new signal associated with a numeric label.

If the optional public keyword is present, the signal is treated as a public output of the circuit. Otherwise, it is considered private/internal.

Example:

%0 = r1cs.def 0 : !r1cs.signal {pub = #r1cs.public} // public signal
%1 = r1cs.def 1 : !r1cs.signal // private

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
label	mlir::IntegerAttr	32-bit unsigned integer attribute
pub	::r1cs::PublicAttr	An attribute to mark a type as public

Results:

Result	Description
out	R1CS signal wire type

r1cs.mul_const (::r1cs::MulConstOp)

Scale a linear expression by a constant

Syntax:

operation ::= `r1cs.mul_const` $input `,` $constValue attr-dict `:` type($scaled)

Traits: AlwaysSpeculatableImplTrait, Commutative

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
constValue	::r1cs::FeltAttr	Field element represented as an arbitrary precision integer

Operands:

Operand	Description
input	R1CS linear expression type

Results:

Result	Description
scaled	R1CS linear expression type

r1cs.neg (::r1cs::NegOp)

Negate a linear expression

Syntax:

operation ::= `r1cs.neg` $input attr-dict `:` type($neg)

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
input	R1CS linear expression type

Results:

Result	Description
neg	R1CS linear expression type

r1cs.to_linear (::r1cs::ToLinearOp)

Casts a signal to a linear expression

Syntax:

operation ::= `r1cs.to_linear` $input `:` type($input) `to` type($output) attr-dict

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
input	R1CS signal wire type

Results:

Result	Description
output	R1CS linear expression type

Attributes

FeltAttr

Field element represented as an arbitrary precision integer

Syntax:

#r1cs.felt<
  ::mlir::IntegerAttr   # value
>

Parameters:

Parameter	C++ type	Description
value	mlir::IntegerAttr

PublicAttr

An attribute to mark a type as public

Syntax: #r1cs.pub

Examples:

%0 = r1cs.def 0 : !r1cs.signal {pub = #r1cs.pub}

Types

LinearType

R1CS linear expression type

Syntax: !r1cs.linear

SignalType

R1CS signal wire type

Syntax: !r1cs.signal