R1CS Backend

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
  • Arbitrary-precision coefficients
  • Cast range checks

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

The optional r1cs.input_labels array supplies one explicit wire ID for each input, in block-argument order. When present, all wire IDs must be consecutive after constant one, ordered as public outputs, public inputs, private inputs, then internal signals. Circuits may omit this attribute when the binary exporter will assign input labels.

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 : !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 allocates a distinct signal associated with a numeric label. Unused signals remain part of the circuit interface and wire layout, so their declarations must survive common subexpression elimination.

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

Interfaces: MemoryEffectOpInterface (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{MemoryEffects::Allocate on ::mlir::SideEffects::DefaultResource}

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<
  ::llzk::DynamicAPIntValue   # value
>

An exact signed mathematical coefficient, independent of storage width. Binary export reduces coefficients modulo the selected field prime.

Parameters:

Parameter	C++ type	Description
value	llzk::DynamicAPIntValue	signed coefficient

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

Arbitrary-precision coefficients

R1CS constants and multipliers use exact signed mathematical integers. Their assembly has no integer-width annotation: for example, r1cs.mul_const x, -1 : !r1cs.linear. Binary export reduces each coefficient modulo the selected prime. The --r1cs-prime decimal option does not require a bit width; the exporter derives the fixed byte width required by the R1CS format.

Cast range checks

R1CS lowering rejects live cast.tofelt and cast.toindex operations and potentially failing assertions in constrain functions. An assert cast that can fail must be preserved even when its result is unused (current lowering does not encode its range check). Valid constant assertions can be folded by canonicalization before lowering (the full R1CS pipeline includes this). Unused infallible casts, including boolean-to-felt casts and cast.toindex assertions from fields whose entire canonical range fits in the index safe range, such as BabyBear, are accepted even without prior cleanup.