# Constraint description sections

## Boundary constraints (boundary_constraints)

The boundary_constraints section consists of expressions describing the expected value of columns in the main or auxiliary traces at the specified boundary. Column boundaries can be selected using boundary accessors. Valid boundary accessors are .first, which selects the first cell of the column to which it is applied, and .last, which selects the last cell of the column column to which it is applied.

Boundary constraints are required. The boundary_constraints section must be defined and contain at least one boundary constraint.

Boundary constraints that are defined against auxiliary columns or that use random values from the built-in $rand array will be identified as auxiliary constraints. A boundary constraint definition must: 1. start with a block indentation and the enf keyword to indicate that the constraint must be enforced. 2. continue by specifying a column identifier with a boundary accessor, e.g. a.first or a.last. 3. continue with = 4. continue with a right-hand-side "value" expression that evaluates to the required value of the specified column at the specified boundary. The expression may include numbers, named constants, variables, public inputs, random values, and any of the available operations. 5. end with a newline. ### Simple example of boundary constraints The following is a simple example of a valid boundary_constraints source section: def BoundaryConstraintsExample trace_columns: main: [a] aux: [p] public_inputs: <omitted for brevity> boundary_constraints: # these are main constraints. enf a.first = 0 enf a.last = 10 # these are auxiliary constraints, since they are defined against auxiliary trace columns. enf p.first = 1 enf p.last = 1 integrity_constraints: <omitted for brevity>  ### Public inputs and random values Boundary constraints can access public input values and random values provided by the verifier in their value expressions. To use public inputs, the public input must be declared in the public_inputs source section. They can be accessed using array indexing syntax, as described by the accessor syntax rules. To use random values, they must be declared in the random_values source section. Random values are defined by an identifier which is bound to a fixed-length array (e.g. rand: [16]), but it is additionally possible to bind identifiers to specific random values or groups of values (e.g. rand: [a, b[14], c]). Random values can be accessed by using $ followed by the array identifier and the index of the value (e.g. $rand[10]) or by using the name of the bound random value or group along with the index of the value within the group (e.g. a or b[5]), as described by the accessor syntax rules. ### Example of boundary constraints with public inputs and random values The following is an example of a valid boundary_constraints source section that uses public inputs and random values: def BoundaryConstraintsExample trace_columns: main: [a, b] aux: [p0, p1] public_inputs: stack_inputs: [16] stack_outputs: [16] boundary_constraints: # these are main constraints that use public input values. enf a.first = stack_inputs[0] enf a.last = stack_outputs[0] # these are auxiliary constraints that use public input values. enf p0.first = stack_inputs[1] enf p0.last = stack_outputs[1] # these are auxiliary constraints that use random values from the verifier. enf b.first = a +$rand[0]
enf p1.first = (stack_inputs[2] + $rand[0]) * (stack_inputs[3] +$rand[1])

integrity_constraints:
<omitted for brevity>


### Intermediate variables

Boundary constraints can use intermediate variables to express more complex constraints. Intermediate variables are declared using the let keyword, as described in the variables section.

### Example of boundary constraints with intermediate variables

The following is an example of a valid boundary_constraints source section that uses intermediate variables:

def BoundaryConstraintsExample

trace_columns:
main: [a, b]
aux: [p0, p1]

public_inputs:
<omitted for brevity>

boundary_constraints:
# this is an auxiliary constraint that uses intermediate variables.
let x = $rand[0] let y =$rand[1]
enf p1.first = x * y

integrity_constraints:
<omitted for brevity>


## Integrity constraints (integrity_constraints)

The integrity_constraints section consists of expressions describing constraints that must be true at each row of the execution trace in order for the proof to be valid.

Integrity constraints are required. The integrity_constraints section must be defined and contain at least one integrity constraint.

### Example of integrity constraints with periodic columns and random values

The following is an example of a valid integrity_constraints source section that uses periodic columns and random values:

def IntegrityConstraintsExample

trace_columns:
main: [a, b]
aux: [p0, p1]

public_inputs:
<omitted for brevity>

periodic_columns:
k: [1, 1, 1, 0]

boundary_constraints:
<omitted for brevity>

integrity_constraints:
# this is a main constraint that uses a periodic column.
enf a' = k * a

# this is an auxiliary constraint that uses a periodic column.
enf p0' = k * p0

# these are auxiliary constraints that use random values from the verifier.
enf b = a + $rand[0] enf p1 = k * (a +$rand[0]) * (b + $rand[1])  ### Intermediate variables Integrity constraints can use intermediate variables to express more complex constraints. Intermediate variables are declared using the let keyword, as described in the variables section. ### Example of integrity constraints with intermediate variables The following is an example of a valid integrity_constraints source section that uses intermediate variables: def IntegrityConstraintsExample trace_columns: main: [a, b] aux: [p0, p1] public_inputs: <omitted for brevity> periodic_columns: k: [1, 1, 1, 0] boundary_constraints: <omitted for brevity> integrity_constraints: # this is an auxiliary constraint that uses intermediate variables. let x = a +$rand[0]
let y = b + \$rand[1]
enf p1 = k * x * y