🥷 Pretty-printing of Rust ZK constraints

Many zkVMs are implemented in Rust, using the Plonky3 library to describe their circuits. While Rust is efficient and expressive for describing complex circuits, it is a complex language when it comes to formal verification. We present here a way to pretty-print the list of constraints generated by a Plonky3 program. That way, we will be able to import the constraints in a formal verification system like Rocq to make sure they are safe and correct.

info

This work was funded by a grant from the Ethereum Foundation to whom we are thankful, as part of the zkEVM Formal Verification Project, to "accelerate the application of formal verification methods to zkEVMs".

🛠️ Plonky3

This is one of the most popular libraries in use to describe circuits for zkVMs, with something like half of the projects using it. The main API to describe circuits is the trait AirBuilder in air/src/air.rs, which we summarize and simplify here:

pub trait AirBuilder: Sized {
    /// Field element
    type F;
    /// Variable
    type Var;
    /// Polynomial expression
    type Expr;
    /// Matrix of the trace
    type M: Matrix<Self::Var>;

    /// Return the matrix representing the main (primary) trace registers.
    fn main(&self) -> Self::M;

    /// Expression evaluating to 1 on the first row, 0 elsewhere.
    fn is_first_row(&self) -> Self::Expr;

    /// Expression evaluating to 1 on the last row, 0 elsewhere.
    fn is_last_row(&self) -> Self::Expr;

    /// Expression evaluating to 1 on all transition rows (not last row), 0 on last row.
    fn is_transition(&self) -> Self::Expr

    /// Returns a sub-builder whose constraints are enforced only when `condition` is nonzero.
    fn when<I: Into<Self::Expr>>(&mut self, condition: I) -> FilteredAirBuilder<'_, Self>

    /// Assert that the given element is zero.
    ///
    /// Where possible, batching multiple assert_zero calls
    /// into a single assert_zeros call will improve performance.
    fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I);
}

From the assert_zero function, we can build all the other assertion operators, like assert_bool or assert_eq. These assertions, creating polynomial equations, will be applied to expressions built from the variables of the trace returned by the main function. Some special expressions is_first_row, is_last_row, and is_transition help state how to initialize the trace and transition between rows. Finally, the when function can be seen as a convenient helper with:

air_builder.when(condition).assert_zero(expr);

behaving like:

air_builder.assert_zero(condition * expr);

since:

$$\begin{align*} \text{condition} \cdot \text{expr} &= 0 \\ \Leftrightarrow \text{condition} \neq 0 \Rightarrow \text{expr} &= 0 \end{align*}$$

📚 Storing the constraints

Thanks to this modular architecture in Plonky3, we can provide a mock implementation of the AirBuilder trait, which will be used to pretty-print the constraints. We implement each primitive operation by saving the parameters in a list, so that at the end of the construction of a circuit, we obtain a list of constraints. For the representation of expressions, we use the existing SymbolicExpression implementation. Here is our current implementation of AirBuilder:

struct RocqAirBuilder {
    /// A matrix of variables, to be built with variables with an
    /// id numbering from 0 to width * height - 1
    main: RowMajorMatrix<SymbolicVariable<Goldilocks>>,
    /// A list of constraints, each one being a polynomial equation of
    /// an expression equal to zero
    constraints: Vec<Constraint<SymbolicExpression<Goldilocks>>>,
}

impl AirBuilder for RocqAirBuilder {
    type F = Goldilocks;

    type Expr = SymbolicExpression<Self::F>;

    type Var = SymbolicVariable<Self::F>;

    type M = RowMajorMatrix<Self::Var>;

    fn main(&self) -> <Self as AirBuilder>::M {
        self.main.clone()
    }

    fn is_first_row(&self) -> <Self as AirBuilder>::Expr {
        SymbolicExpression::IsFirstRow
    }

    fn is_last_row(&self) -> <Self as AirBuilder>::Expr {
        SymbolicExpression::IsLastRow
    }

    fn is_transition_window(&self, _: usize) -> <Self as AirBuilder>::Expr {
        SymbolicExpression::IsTransition
    }

    fn assert_zero<I>(&mut self, expr: I)
    where
        I: Into<Self::Expr>,
    {
        // We store the constraint in a list, to be printed at the end
        self.constraints.push(Constraint::AssertZero(expr.into()));
    }
}

As this is convenient when the list of constraints is long (in the tens of thousands for a typical precompile), we also add a logging function:

impl LoggingAirBuilder for RocqAirBuilder {
    fn log_in_constraints(&mut self, message: &str) {
        self.constraints
            .push(Constraint::Message(message.to_string()));
    }
}

to display a string marker at any point in the code.

🎨 Pretty-printing

We display the list of constraints on the standard output, so that they can be saved in a snapshot file. We take care of having an output that is regular and readable. The transformation we make is that we flatten the application of the associative binary operators + and * so that they get applied to a list of operands instead of two. This tends to flatten the output and increase the readability in our experience.

Here is a typical output:

Trace 🐾
  Message 🦜
    eval_row
  Message 🦜
    eval_row::flags
  AssertZero:
    Mul:
      Variable: 0
      Sub:
        Variable: 0
        Constant: 1
  AssertZero:
    Mul:
      Variable: 1
      Sub:
        Variable: 1
        Constant: 1
  AssertZero:
    Mul:
      Variable: 2
      Sub:
        Variable: 2
        Constant: 1
  AssertZero:
    Mul:
      Add:
        Variable: 0
        Variable: 2
      Sub:
        Add:
          Variable: 0
          Variable: 2
        Constant: 1

We annotate the user messages with a 🦜 to make them easier to find in the list of constraints. The variables are all identified by their id in the trace, which is a number from 0 to width * height - 1. We flatten the consecutive applications of binary operators, like in:

AssertZero:
  Mul:
    Variable: 459
    Constant: 18446462594437939201
    Sub:
      Add:
        Variable: 808
        Constant: 0
        Mul:
          Variable: 11
          Constant: 1
        Mul:
          Variable: 12
          Constant: 2
        Mul:
          Variable: 13
          Constant: 4
        Mul:
          Variable: 14
          Constant: 8
        Mul:
          Variable: 15
          Constant: 16
        Mul:
          Variable: 16
          Constant: 32
        Mul:
          Variable: 17
          Constant: 64
        Mul:
          Variable: 18
          Constant: 128
        Mul:
          Variable: 19
          Constant: 256
        Mul:
          Variable: 20
          Constant: 512
        Mul:
          Variable: 21
          Constant: 1024
        Mul:
          Variable: 22
          Constant: 2048
        Mul:
          Variable: 23
          Constant: 4096
        Mul:
          Variable: 24
          Constant: 8192
        Mul:
          Variable: 25
          Constant: 16384
        Mul:
          Variable: 26
          Constant: 32768
        Constant: 0
      Add:
        Constant: 0
        Mul:
          Variable: 782
          Constant: 1
        Mul:
          Variable: 783
          Constant: 256

Note that the large constant 18446462594437939201 is the inverse of 2 for the Goldilocks prime.

note

There are other kinds of constraints, like lookups, which we do not show here.

✒️ Conclusion

We have seen here how to output the definition of a Plonky3 circuit in a readable, and sometimes verbose, text format.

Next, we will see how to connect this representation to the Rocq formalization of a circuit, to make sure we are verifying the right implementation.

You want to secure your zkVM? Discuss to check what is possible! ⇨ contact@formal.land

For more

Follow us on X or LinkedIn for more, or comment on this post below! Feel free to DM us for any questions!