This page specifies the basic syntax and types.
Delimiters and special characters
:is used as a delimiter when declaring source sections and types
.is used to access a boundary on a trace column, e.g.
]are used for defining arrays in type declarations and for indexing in constraint descriptions
,is used as a delimiter for defining arrays in type declarations
$is used to access random values or built-in variables by their identifier. For example, the column at index
iin the main execution trace can be accessed by
Valid identifiers are strings that start with a letter
A-Z followed by any combination of letters, digits
0-9 or an underscore
The only supported numbers are integers, and all integers are parsed as u64. Using a number larger than 2^64 - 1 will result in a
The following operations are supported in constraint descriptions with the specified syntax:
- Equality (
a = b)
- Addition (
a + b)
- Subtraction (
a - b)
- Multiplication (
a * b)
- Exponentiation by a constant integer x (
The following operations are not supported:
Parentheses and complex expressions
)) are supported and can be included in any expression except exponentiation, where complex expressions are not allowed.
The following is allowed:
a * (b + c)
The following is not allowed:
a^(2 + 3)
These accessors may only be used in the specified source section in which they are described below.
The following accessors may only be applied to trace columns when they are in boundary constraint definitions.
- First boundary (
.first): accesses the trace column's value in the first row. It is only supported in boundary constraint descriptions
- Last boundary (
.last): accesses the trace column's value in the last row. It is only supported in boundary constraint descriptions
The following accessor may only be applied to public inputs declared in
public_inputs when they are referenced in boundary constraint definitions.
- Indexing (
input_name[i]): public inputs may be accessed by using the indexing operator on the declared identifier name with an index value that is less than the declared size of its array.
Here is an example of usage of first and last boundaries and a public input within a boundary constraint:
trace_columns: main: [a] public_inputs: stack_inputs:  stack_outputs:  boundary_constraints: enf a.first = stack_inputs enf a.last = stack_outputs
The following accessor may only be applied to trace columns when they are referenced in integrity constraint definitions.
- Next Row (
'is a postfix operator that indicates the value of the specified trace column in the next row. It is only supported in integrity constraint descriptions.
Here is an example of usage of the Next Row operator within an integrity constraint:
trace_columns: main: [a] aux: [p] integrity_constraints: enf p' = p * a