Appendix: Constraint System#

Symbolic Expression DAG#

Constraints are represented as a directed acyclic graph (DAG) of symbolic expressions (SymbolicExpressionDag). Each node has:

kind: One of VARIABLE, CONSTANT, IS_FIRST_ROW, IS_LAST_ROW, IS_TRANSITION, ADD, SUB, MUL, NEG.
operands: Indices into the DAG node array (for binary/unary operations).
degree_multiple: The constraint degree for variable nodes.

The DAG is stored in topological order: every node’s operands have smaller indices than the node itself.

Node Types#

Kind	Arity	Description
`VARIABLE`	0	Reference to a trace column at a specific offset
`CONSTANT`	0	Literal field element
`IS_FIRST_ROW`	0	Lagrange selector \(L_0(\zeta)\)
`IS_LAST_ROW`	0	Lagrange selector \(L_{N-1}(\zeta)\)
`IS_TRANSITION`	0	\(\zeta/s - \omega^{-1}\) (nonzero on non-last rows)
`ADD`	2	\(a + b\)
`SUB`	2	\(a - b\)
`MUL`	2	\(a \cdot b\)
`NEG`	1	\(-a\)

Variables#

A SymbolicVariable (SymbolicVariable) references a specific trace column:

entry_type: PREPROCESSED, MAIN, PERMUTATION, PUBLIC, CHALLENGE, EXPOSED_AFTER_CHALLENGE.
column_index: Column within the partition.
offset: Row offset (0 = current row, 1 = next row).

DAG Evaluation#

At a Point (Verifier)#

The verifier evaluates the DAG at the OOD point \(\zeta\) using the opened polynomial values (eval_symbolic_dag):

Walk nodes in topological order.
For each node, dispatch on kind:
- VARIABLE: look up the opened value from the appropriate trace partition.
- CONSTANT: wrap as FF4.
- Selector nodes: fetch from precomputed DomainSelectors.
- Arithmetic nodes: compute from previously evaluated operands.
Extract the constraint output indices: dag.constraint_idx.

Over the Full Trace (Prover)#

The prover evaluates the DAG at every point of the quotient domain (eval_symbolic_expression_dag_full). The same DAG walk applies, but each node result is a column (array) rather than a scalar.

Constraint Folding#

Given \(k\) constraint evaluations \(C_0, C_1, \ldots, C_{k-1}\) and the challenge \(\alpha\), the folded constraint value is computed by Horner’s method (fold_constraints):

\[ \text{folded} = C_0 \cdot \alpha^{k-1} + C_1 \cdot \alpha^{k-2} + \cdots + C_{k-1} \]

Equivalently, accumulate right-to-left:

accumulator = 0
for i in range(k):
    accumulator = accumulator * alpha + C_i

Quotient Relationship#

The quotient polynomial \(Q(X)\) encodes the constraint satisfaction:

\[ Q(X) = \frac{\sum_i \alpha^i \cdot C_i(X)}{Z_H(X)} \]

where \(Z_H(X) = (X/s)^N - 1\) is the vanishing polynomial of the trace domain.

The verifier checks this at \(\zeta\):

\[ \text{folded} \cdot Z_H(\zeta)^{-1} = Q(\zeta) \]

where \(Q(\zeta)\) is reconstructed from the quotient chunk openings (reconstruct_quotient).

Domain Selectors#

The selectors at a point \(\zeta\) outside the trace domain \(H = \{s \cdot \omega^i\}\) are ():

Let \(u = \zeta / s\) (the “unshifted” point).

\[\begin{split} \begin{aligned} Z_H(\zeta) &= u^N - 1 \\ \text{is\_first\_row} &= \frac{Z_H(\zeta)}{u - 1} \\ \text{is\_last\_row} &= \frac{Z_H(\zeta)}{u - \omega^{-1}} \\ \text{is\_transition} &= u - \omega^{-1} \\ \text{inv\_zeroifier} &= Z_H(\zeta)^{-1} \end{aligned} \end{split}\]

These are unnormalized selectors (as in Plonky3). The normalization factor cancels in the quotient relationship.

Appendix: Constraint System

Contents