Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
717 lines (615 sloc) 37 KB

AirAssembly

AirAssembly is a low-level language for encoding Algebraic Intermediate Representation (AIR) of computations. The goal of the language is to provide a minimum number of constructs required to fully express AIR for an arbitrary computation.

AirAssembly is intended to be a compilation target for higher-level languages, and as such, expressivity and readability by humans are not explicit goals of the language. Instead, the language aims to:

  1. Be easy to parse. This is one of the reasons AirAssembly uses s-expression-based syntax.
  2. Provide a small number of primitives which can be combined together to form more complex constructs.
  3. Avoid redundancy and implicit behavior. Ideally, there should be one right way to do things, and all parameters should be specified explicitly.

AirAssembly module

A module in AirAssembly is a self-contained unit which fully describes a computation. Its purpose is to specify:

  1. Inputs required by the computation.
  2. Logic for generating execution trace for the computation.
  3. Logic for evaluating transition constraints for the computation.
  4. Metadata needed to compose the computation with other computations.

Module expression has the following form:

(module
    <field declaration>
    <constant declarations>
    <static registers>
    <transition function>
    <constraint evaluator>
    <export declarations>)

The code below illustrates AirAssembly module structure on an example of a MiMC computation:

(module
    (field prime 340282366920938463463374607393113505793)
    (const 3)
    (static
        (cycle 42 43 170 2209 16426 78087 279978 823517))
    (transition
        (span 1) (result vector 1)
        (add
            (exp (load.trace 0) (load.const 0))
            (load.static 0)))
    (evaluation
        (span 2) (result vector 1)
        (sub
            (load.trace 1)
            (add
                (exp (load.trace 0) (load.const 0))
                (load.static 0))))
    (export mimc128 (steps 256))
    (export mimc256 (steps 1024)))

The meaning of the components in the above example is as follows:

  • Field declaration specifies the finite field to be used for all arithmetic operations.
  • Constant declarations define a set of constants that can be used in transition function and constraint evaluator.
  • Static registers describe logic for building static registers, including logic for interpreting inputs.
  • Transition function describes state transition logic for the computation.
  • Constraint evaluator describes algebraic relation between steps of the computation.
  • Export declarations define endpoints which can be used to compose the computation with other computations.

Execution model

Executing an AirAssembly module against a set of inputs produces two outputs:

  1. Execution trace table
  2. Constraint evaluation table

Execution trace table is a two-dimensional matrix in which each column corresponds to a state register, and each row contains values for the registers at a given step of a computation. The columns in the execution trace table can be partitioned into 2 types:

  1. Static register traces - these are generated by transforming inputs according to static register specifications.
  2. Dynamic register traces - these are generated by iteratively applying a transition function for each step of the computation.

Constraint evaluation table is also a two-dimensional matrix. But in this case, each column corresponds to a transition constraint polynomial, and each row contains values of the constraint polynomials evaluated at a given point of the evaluation domain.

AirAssembly module execution process is illustrated in the picture below:

AirAssembly module execution

  1. First, the static segment of the execution trace table is built by evaluating static register specifications against provided inputs.
  2. Then, the dynamic segment of the execution trace table is built by evaluating the transition function for each step of the computation.
    • The dynamic segment is built after the static segment because transition function should be able to access static registers at every step.
  3. Finally, the constraint evaluation table is built by applying constraint evaluator to the extended execution trace.

(the funny shape of the Inputs drawing is not accidental; check out nested input register example to see why).

Module components

The sections below provide detailed explanation of AirAssembly module components.

Field declaration

Field declaration section specifies a finite field to be used in all arithmetic expressions. The declaration expression has the following form:

(field <type> <modulus>)

where:

  • type specifies the type of the field. Currently, only prime fields are supported.
  • modulus specifies prime field modulus.

For example:

(field prime 340282366920938463463374607393113505793)

The above example defines a prime field with modulus = 2128 - 9 * 232 + 1.

Constant declarations

Constant declaration section defines constants which can be used in transition functions and constraint evaluators. Constant declaration expression has the following form:

(const <value>)

where:

  • value can be either a scalar, a vector, or a matrix (see value types for more info).

For example:

(const 5)                       # declares scalar constant with value 5
(const (vector 1 2 3 4))        # declares vector constant with values [1, 2, 3, 4]
(const (matrix (1 2) (3 4)))    # declares matrix constant with rows [1, 2] and [3, 4]

Constants are un-named and can be referenced only by their indexes. For example, the following code block declares 3 constants with indexes 0, 1, and 2 (in the order of their declaration):

(const 5) (const (vector 1 2 3 4)) (const (matrix (1 2) (3 4)))

Once defined, values constants cannot be changed. To reference a constant in a transition function or a constraint evaluator load.const expression can be used (see load operations for more info).

Static registers

Static registers section defines logic for generating static register traces. These traces are computed before the execution of the transition function, and cannot be changed by the transition function or the constraint evaluator. Static section expression has the following form:

(static <registers>)

where:

  • registers is a list of register declarations consisting of input, embedded, and computed registers.

For example, the following code block declares 2 registers - one input register and one embedded cyclic register:

(static
    (input public vector (steps 8)))
    (cycle 1 2 3 4))

A detailed explanation of each type of static register is provided in the following sections.

Input registers

Input register declarations specify what inputs are required by the computation, and describes the logic needed to transform these inputs into register traces. Input register declaration expression has the following form:

(input <visibility> <binary?> <type> <filling> <steps?>)

where:

  • visibility can be either secret or public. Values for secret input registers are assumed to be known only to the prover and need to be provided only at the proof generation time. Values for public input registers must be known to both, the prover and the verifier, and must be provided at the time of proof generation, as well as, at the time of proof verification.
  • An optional binary attribute indicates whether the input register accepts only binary values (ones and zeros).
  • Input type can be scalar, vector, or a reference to a parent register. scalar input registers expect a single value; vector input registers expect a list of at least one value, and the length of the list must be a power of 2. References to parent registers have the form (parent <index>), where index is the index of the parent register. This allows forming of nested inputs (see examples for more info).
  • filling can be either sparse or a fill expression. sparse filling indicates that values at steps other than input alignment steps are unimportant. fill expression has the form (fill <value>), where value is a scalar value to be inserted into the register trace at all unaligned steps (see examples for more info).
  • steps expression has the form (steps <count>), where count specifies the number of steps by which a register trace should be expanded for each input value. The number of steps must be a power of 2. steps expression can be provided only for "leaf" input registers (see examples for more info).

Detailed examples of how different types of input registers are transformed into register traces are available here, but here are a few simple example of input register declarations:

(input public scalar sparse (steps 8))
(input secret vector (fill 0))
(input public binary (fill 0) (parent 0) (steps 8))

Embedded registers

Embedded register declarations contains the data needed to generate register traces without any additional inputs. Embedded register declaration expression has the following form:

(<type> <values>)

where:

  • type is the type of the embedded register. Currently, the only available type is cycle which will generate a trace with a cyclic pattern of values.
  • values is the list of scalars which form the basis of the register trace. The list must contain at least one value, and the length of the list must be a power of 2.

For example, the following code block declares two embedded cyclic registers:

(cycle 1 2 3 4)
(cycle 1 1 0 0 0 0 1 1)

If the trace length is equal to 16 steps, register traces for these registers will look like so:

register 0: [1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4]
register 1: [1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1]

Computed registers

Input and embedded registers can be combined using arithmetic and logical operators to form new static registers. Such registers are called computed registers and their declaration has the following form:

(<expression>)

where:

  • expression can be either an arithmetic expression or a logical expression involving one or more already declared registers.

For example, in the code block below, two static registers are declared: the first one is an embedded cyclic register, the second on is a computed register where every value for the register is equal to the corresponding value of the cyclic register multiplied by 2.

(cycle 1 2 3 4)
(mul (static 0) 2)

Note: computed registers cannot be based on secret input registers as a verifier also needs to generate register traces for these registers.

Logical expressions

Logical expressions can combine one or more public input registers into a computed register. Logical expressions have the following form:

(when <condition> <true value> <false value>)

where:

  • condition is a boolean predicate which evaluates to true when a referenced input register holds input value, and evaluates to false otherwise.
  • true value is a scalar which will be assigned to the register when the predicate is true.
  • false value is a scalar which will be assigned to the register when the predicate is false.

For example:

(input public vector sparse (steps 4))
(when (static 0) 1 0)

Assuming inputs for register 0 are [3, 4], register traces for the above example will look like so:

register 0: [3, ?, ?, ?, 4, ?, ?, ?]
register 1: [1, 0, 0, 0, 1, 0, 0, 0]

Essentially, the computed register will hold value 1 when there is an input in static register 0, and 0 otherwise.

Predicates can be also combined using standard boolean operators and, or and, not. For example:

(input public vector sparse)
(input public (parent 0) (fill 0) (steps 4))
(when (and (not (static 0)) (static 1)) 1 0)

Assuming inputs for register 0 are [3, 4], and inputs for register 1 are [[4, 5], [6, 7]], register traces for the above example will look like so:

register 0: [3, ?, ?, ?, ?, ?, ?, ?, 4, ?, ?, ?, ?, ?, ?, ?]
register 1: [4, 0, 0, 0, 5, 0, 0, 0, 6, 0, 0, 0, 7, 0, 0, 0]
register 2: [0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]
Arithmetic expressions

Arithmetic expressions can combine static registers into a new computed register using standard arithmetic operators add, sub, mul, div, exp, neg, and inv. Valid operands for these operators are:

  • Embedded, computed, and public input registers.
  • Logical expressions
  • Arithmetic expressions (i.e. arithmetic expressions can be nested).

For example:

(input public vector (fill 0) (steps 8))
(cycle 1 2 3 4)
(mul
    2
    (add 
        (when (static 0) 1 0) 
        (static 1)))

Assuming inputs for register 0 are [3, 4], register traces for the above example will look like so:

register 0: [3, 0, 0, 0, 4, 0, 0, 0]
register 1: [1, 2, 3, 4, 1, 2, 3, 4]
register 2: [4, 4, 6, 8, 4, 4, 6, 8]

Transition function

Transition function describes state transition logic needed to generate dynamic register traces. Transition function expression has the following form:

(transition <signature> <locals> <body>)

Transition function components (signature, locals, body) are described in the following sections. The code block below shows a simple example of a transition function:

(transition
    (span 1) (result vector 2)      # function signature
    (local scalar)                  # local variable declaration
    (store 0                        # function body starts here
        (add                        
            (get (load.trace 0) 0)) 
            (get (load.trace 0) 1))
    (vector
        (load.local 0)
        (add
            (load.local 0)
            (get (load.trace 0) 1))))

The above transition function produces a trace table with 2 dynamic registers per row. The transition logic is as follows:

  • At each step, the values of the first and second registers are summed.
  • Then this sum becomes the value of the first register for the next row,
  • And the value of the second register for the next row is set to the sum plus the value of the second register.

(this is actually a somewhat convoluted way to describe a transition function for the Fibonacci sequence).

Transition function signature

Transition function signature contains metadata for the transition function and has the following form:

(span <length>) (result <type>)

where:

  • Span length is the number of consecutive trace table rows which can be accessed from within the transition function body. Currently, the only supported span length is 1. To access the the dynamic segment of a trace table row load.trace expression can be used (see load operations for more info).
  • Result type is the type of the value to which the transition function resolves. This must always be a vector, and the length of the vector defines the width of dynamic segment of the execution trace table.

For example:

(span 1) (result vector 2)

The above signature specifies that:

  • The transition function can access only a single row of the trace table (the row at the current step).
  • Each row of the trace table contains 2 dynamic registers (the width of the dynamic segment of the trace table is 2).

Transition function locals

Locals section of a transition function declares variables which can be used in the function body. Variable declaration expression has the following form:

(local <type>)

where:

  • Variable type can be either a scalar, a vector, or a matrix (see value types for more info). For non-scalar types, additional info must be supplied to specify the dimensions of the variable.

For example:

(local scalar)      # declares a scalar variable
(local vector 4)    # declares a vector variable with length 4
(local matrix 2 4)  # declares a matrix variable with 2 rows and 4 columns

Local variables are un-named and can be referenced only by their indexes. For example, the following code block declares 3 variables with indexes 0, 1, and 2 (in the order of their declaration):

(local scalar) (local vector 4) (local matrix 2 4)

To access these local variables load.local and store.local expressions can be used (see load operations and store operations for more info).

Transition function body

Transition function body consists of a list of arithmetic expressions such that:

  1. All expressions in the list, except the last one, must be store operations which save the result of some arithmetic expression into a local variable.
  2. The last expression in the list must evaluate to a vector. The length of the vector must be equal to the length of the result vector specified in the transition function signature.

For example, the body of the function below consists of a single expression:

(vector (add 1 2))                      # resolves to vector [3]

Another example, where a local variable is used to store value of a common sub-expression:

(store 0 (add 1 2))                     # stores value 3 into local variable 0
(vector (load.local 0) (load.local 0))  # resolves to vector [3, 3]

Constraint evaluator

Constraint evaluator section describes transition constraint evaluation logic needed to generate a constraint evaluation table for the computation. Constraint evaluation expression has the following form:

(evaluation <signature> <locals> <body>)

Constraint evaluator components (signature, locals, body) are similar to their equivalents in transition function, except for the following differences:

  1. Constraint evaluator can access multiple rows of the execution trace table. To do this, set the span of the evaluator to a value greater than 1 (though, currently, 2 is the maximum allowed span value). Info about how to access future execution trace table rows can be found in load operations section.
  2. The length of the result vector defines the number of transition constraints (the width of the constraint evaluation table).

The code block below shows a simple example of a constraint evaluator which complements the example of a transition function described previously.

(evaluation
    (span 2) (result vector 2)         # evaluator signature
    (local scalar)                     # local variable declaration
    (store 0                           # evaluator body starts here
        (add                        
            (get (load.trace 0) 0)) 
            (get (load.trace 0) 1))
    (sub
        (load.trace 1)                 # loads the next row the dynamic trace registers
        (vector
            (load.local 0)
            (add
                (load.local 0)
                (get (load.trace 0) 1)))))

The evaluator above loads the next row of the dynamic segment of the execution trace table, and subtracts the result of applying the transition function to the current row from it.

Export declarations

Export declarations specify how the module can be executed either as a stand-alone computation or as a part of a composed computation. There can be many export declarations per module and each declaration expression has the following form:

(export <name> <initializer?> <trace cycle>)

where:

  • Export name defines a unique name for the exported endpoint. The name must start with a letter and can contain any combination of letters, numbers, and underscores. The name main has special meaning as described in the main export section below.
  • Trace initializer defines initialization logic for the first row of dynamic register traces. This item is relevant only for the main export. All other exports do not have control over initialization of the first trace row. The initialization expression is described in detail in the main export section below.
  • trace cycle defines the length of a single execution trace cycle required by the computation. Trace cycle expression has the following form (steps <count>), where count specifies the number of required steps. The count parameter must be a power of 2 and also must be a multiple of the number of steps required to consume the smallest possible set of inputs. For example, if according to input register declarations, the smallest possible execution trace can be 64 steps, then the count parameter can be set to 64, 128, 256 etc.

Main export

When the name of an export is set to main, the export defines rules for how the computation can be run as a stand-alone module. This also requires that export expression includes an initializer which has the following form:

(init <initialization vector>)

where:

  • initialization vector is an expression that resolves to a vector of the same length as the length of the vector returned by the transition function (i.e. the number of dynamic trace registers).

For example, if the execution trace has 4 dynamic trace registers, the main export expression may look like so:

(export main 
    (init (vector 0 0 0 0)) (steps 64))

This will initialize the first row of dynamic register traces to all 0's.

Trace initializer also has access to a special seed vector. Values for the seed vector are provided at the time of proof generation. The initializer can resolve to the seed vector directly like so:

(export main (init seed) (steps 64))

The initializer can also perform basic vector and arithmetic operations with the seed vector. For example, the initializer in the code block below resolves to a vector of 4 values where the first two values are taken from the seed vector, and the remaining two values are set to 0:

(export main 
    (init (vector (get seed 0) (get seed 1) 0 0))
    (steps 64))

Interface exports

When the name of an export is set to anything other than main, the export defines rules for how the module can be composed with other computations. In this case, only the cycle length expression is required to specify minimum possible trace cycle length.

For example, the code block below declares two exports, with mimc128 export requiring 256 steps to execute, and mimc256 requiring 1024 steps to execute.

(export mimc128 (steps 256))
(export mimc256 (steps 1024))

Arithmetic expressions

Arithmetic expressions are the basic building blocks for the bodies of transition functions and transition constraint evaluators. These expressions usually perform some operation with one or more values, and resolve to a new value which is the result of the operation.

Value types

Values in AirAssembly can be of one of the following types:

  1. Scalar - which is a single field element.
  2. Vector - which is a one-dimensional arrays of field elements.
  3. Matrix - which is a two-dimensional arrays of field elements.

Vector operations

To create a vector, the following expression can be used:

(vector <elements>)

where:

  • elements is a list of expressions which resolve to scalars or vectors.

For example:

(vector 1 2 3 4)
(vector 1 (vector 2 3) (add 2 2))

Both of the above expressions resolve to a vector with elements [1, 2, 3, 4].

Extracting vector element

To extract a single element from a vector, the following expression can be used:

(get <vector> <index>)

where:

  • vector is the vector from which the element is to be extracted,
  • index is the zero-based index of the element to extract.

For example:

(get (vector 1 2 3 4) 1)    # resolves to scalar value 2

Slicing vectors

To extract a slice of elements from a vector, the following expression can be used:

(slice <vector> <start index> <end index>)

where:

  • vector is the vector from which the elements are to be extracted,
  • start index is the zero-based, inclusive index of the element at which to start extraction,
  • end index is the zero-based, inclusive index of the element at which to end extraction.

For example:

(slice (vector 1 2 3 4) 1 2)    # resolves to vector [2, 3]
(slice (vector 1 2 3 4) 1 1)    # resolves to vector [2]

Matrix operations

To create a matrix, the following expression can be used:

(matrix <rows>)

where:

  • rows is a list of expressions which resolve to a list of field elements or to a vector. All rows in the matrix must have the same number of columns (elements).

For example:

(matrix (1 2 3 4) (5 6 7 8))
(matrix (vector 1 2 3 4) (vector 5 6 7 8))

Both of the above expressions resolve to a matrix with 2 rows and 4 columns containing values [[1, 2, 3, 4], [5, 6, 7, 8]].

Binary arithmetic operations

AirAssembly supports basic arithmetic operations. To perform such operations the following expression can be used:

(<operation> <operand 1> <operand 2>)

where:

  • operation is one of the following operations:
    • add - modular addition.
    • sub - modular subtraction.
    • mul - modular multiplication.
    • div - modular division computed as modular multiplication of the first operand with the multiplicative inverse of the second operand.
    • exp - modular exponentiation, where the second operand (the exponent) must be a static scalar value.
    • prod - matrix or vector product as described here.
  • operand 1 is an expression resolving to the first operand.
  • operand 2 is an expression resolving to the second operand.

For example:

(add 1 2)   # resolves to 3
(sub 3 1)   # resolves to 2
(mul 3 3)   # resolves to 9
(div 4 2)   # resolves to 2
(exp 2 8)   # resolves to 256

The above operations can also take vectors and matrixes as operands. In such cases, the operations are treated as element-wise operations and it is required that both operands have the same lengths/dimensions. For example:

(add (vector 1 2) (vector 3 4))     # resolves to [4, 6]
(add (vector 1 2) (vector 3 4 5))   # results in an error

The second operand can also be replaced with a scalar value. For example:

(exp (vector 3 4) 2)                # resolves to [9, 16]

prod operation

prod operation can be applied only to vectors and matrixes, and types of operands define the operation performed like so:

  • (prod <matrix> <matrix>) - performs a standard matrix multiplication of two matrixes. If the matrixes have dimensions [n,p] and [p,m] respectively, the resulting matrix will have dimensions [n,m].
  • (prod <matrix> <vector>)- also performs matrix multiplication, but the result is a vector. If the input matrix dimensions are [n,m], and the length of the input vector is m, the resulting vector will have length n.
  • (prod <vector> <vector>) - performs a linear combination of two vectors. Vectors must have the same length, and the output is a scalar.

Unary arithmetic operations

AirAssembly also supports two unary arithmetic operations. These operations are applied to a single operand like so:

(<operation> <operand>)

where:

  • operation is one of the following operations:
    • neg - modular additive inverse.
    • inv - modular multiplicative inverse.
  • operand is an expression resolving a scalar, a vector, or a matrix.

For example (assuming field modulus is 23):

(neg 21)    # resolves to 2
(inv 15)    # resolves to 20

If the operand is a vector or a matrix, the operation is performed element-wise. For example:

(neg (vector 1 2 3 4))      # resolves to [22, 21, 20 19]

Load operations

To retrieve values from various sections of a program's memory, the following expression can be used:

(load.<source> <index>)

where:

  • source specifies the memory segment; can be one of the following values:
    • const - array of global constants.
    • static - static segment of the execution trace table.
    • trace - dynamic segment of the execution trace table.
    • local - array of local variables.
  • index specifies which value to retrieve from the specified source. The meaning of this parameter depends on the source parameter as follows:
    • const - index of a global constant.
    • static - row offset into the execution trace table, with 0 being the row at the current step, 1 being the row at the next step etc.
    • trace - row offset into the execution trace table, with 0 being the row at the current step, 1 being the row at the next step etc.
    • local - index of a local variable.

For example:

(load.const 0)   # resolves to the value of the global constant at index 0
(load.static 0)  # resolves to the static register row at the current step
(load.trace 0)   # resolves to the dynamic register row at the current step
(load.trace 1)   # resolves to the dynamic register row at the next step
(load.local 0)   # resolves to the value of local variable at index 0

For static and trace sources, the result of a load operation is always a vector with each element of the vector corresponding to a single register. For const and local sources, the result could be a scalar, a vector, or a matrix - depending on the declared type of a global constant or a local variable.

Note: trying to load a value from a local variable that hasn't been initialized yet, will result in an error.

Store operations

To update a value of a local variable, the following expression can be used:

(store.local <index> <value>)
  • index is a zero-based position of the variable in the local variables array;
  • value is an expression which resolves to a value to be assigned to the local variable. Type of the value must match the declared type of the local variable, otherwise an error will be thrown.

For example:

(store.local 0 1)                   # stores a scalar into local variable 0
(store.local 1 (vector 1 2 3 4))    # stores a vector into local variable 1
(store.local 1 5)                   # results in an error

Value of a given local variable can be updated an unlimited number of times. Also, the value expression can contain references to the variable being updated. For example, the following is perfectly valid:

(store.local 0 1)                       # stores 1 into local variable 0
(store.local 0 (add 2 (load.local 0)))  # stores 3 into local variable 0

Note: unlike other expressions, store expressions do not resolve to a value, and therefore, cannot be used as sub-expressions in other expressions.

Input register trace generation

Input register traces require two pieces of data to generate:

  1. Input register declarations which belong to the static section of AirAssembly module (described here),
  2. Input values which are provided at the time of proof generation and proof verification. The inputs are expected to be provided as arrays, which can also be nested (i.g. arrays of arrays multiple layers deep).

Single input register

The examples below illustrate how various inputs for a single register are transformed into register traces. Since we work with a single register, our traces will have only 1 column.

Let's start with a simple example of an input register that expects a scalar value and resolves to a trace of 4 steps long.

(input public scalar sparse (steps 4))

If the input value for this register was 3, the resulting trace column would be [3, ?, ?, ?]. The sparse attribute indicates that values at steps other than 0 are not important, and therefore, can be anything. Thus, when interpolating a polynomial for this column, the only thing we need to ensure is that the value at step 0 is 3.

If we want to make sure trace values at all steps are well-defined, we can replace sparse attribute with fill expression like so:

(input public scalar (fill 0) (steps 4))

Now, with the same input 3, the resulting trace column would be [3, 0, 0, 0].

We can also change trace length by changing the number of steps. For example:

(input public scalar (fill 0) (steps 8))

Given input 3, this will evaluate to a column with values [3, 0, 0, 0, 0, 0, 0, 0, 0].

If we want the register to accept a list of values (rather than just one value), we can change its type from scalar to vector like so:

(input public vector (fill 0) (steps 4))

Now, we can provide a list of values, and the trace columns will look like so:

  • Input [3] => [3, 0, 0, 0]
  • input [3, 4] => [3, 0, 0, 0, 4, 0, 0, 0]
  • Input [3, 4, 5, 6] => [3, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 6, 0, 0, 0]

Notice, how for each input value, trace length extends by 4 steps.

Multiple independent input registers

We can define multiple input registers, and in such cases the number of trace columns will equal to the number of declared registers. For example, the following code block defines two input registers, each expecting a list of values. The first register expands by 4 steps for each input value, while the second register expand by 8 steps for each input value.

(input public vector (fill 0) (steps 4))
(input public vector (fill 0) (steps 8))

If we provide [3, 4, 5, 6] as inputs for the first register, and [7, 8] as inputs for the second register, the resulting column traces will look like so:

register 0: [3, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 6, 0, 0, 0]
register 1: [7, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0]

Notice that both registers resolve to traces of the same length. This is required. Providing inputs that evaluate to trace columns of different lengths will result in an error.

Nested input registers

We can also specify relationships between input registers like so:

(input public vector (fill 0))
(input public (parent 0) (fill 0) (steps 2))

The above example declares 2 input registers such that:

  1. The first register expects a list of values,
  2. The second register expects one or more values for each value provided for the first register. This is accomplished by replacing register type with parent expression in which (parent 0) means that the parent of the register is register with index 0.

For example, if we provide [3, 4] as inputs for the first register, we need to provide one or more values for each value in this list. For example, it could be [[5, 6], [7, 8]]. For this set of inputs, trace columns will look like so:

register 0: [3, 0, 0, 0, 4, 0, 0, 0]
register 1: [5, 0, 6, 0, 7, 0, 8, 0]

If, on the other hand, we keep the inputs for the first register as [3, 4], but provide [[5, 6, 7, 8], [9, 10, 11, 12]] as inputs for the second register, trace columns would look like so:

register 0: [3, 0, 0, 0, 0, 0, 0, 0, 4, 0,  0, 0,  0, 0,  0, 0]
register 1: [5, 0, 6, 0, 7, 0, 8, 0, 9, 0, 10, 0, 11, 0, 12, 0]

We can also nest register relations as deep as needed. For example, the code block below has two levels of nesting and also two parallel nesting structures:

(input public vector (fill 0))
(input public (parent 0) (fill 0))
(input public (parent 1) (fill 0) (steps 2))
(input public (parent 0) (fill 0))
(input public (parent 3) (fill 0) (steps 4))

This results in a tree-like structure where:

  • Register 0 is the parent of both registers 1 and 3
  • Register 1 is the parent of register 2
  • Register 3 is the parent of register 4
  • Registers 2 and 4 are the "leaves" of the dependency tree.

Notice also that we didn't specify the number of steps for non-leaf registers. In general, number of steps must be specified only for the leaf registers. Specifying number of steps for non-leaf registers will result in an error.

To illustrate how inputs for such register structure are transformed into register traces, suppose we provide the following inputs for each register:

Register 0: [3]
Register 1: [[5, 6, 7, 8]]
Register 2: [[[9, 10], [11, 12], [13, 14], [15, 16]]]
Register 3: [[17, 18]]
Register 4: [[[19, 20], [21, 22]]]

The register traces generated for this set of inputs would look like so:

step # reg 0 reg 1 reg 2 reg 3 reg 4
0 3 5 9 17 19
1 0 0 0 0 0
2 0 0 10 0 0
3 0 0 0 0 0
4 0 6 11 0 20
5 0 0 0 0 0
6 0 0 12 0 0
7 0 0 0 0 0
8 0 7 13 18 21
9 0 0 0 0 0
10 0 0 14 0 0
11 0 0 0 0 0
12 0 8 15 0 22
13 0 0 0 0 0
14 0 0 16 0 0
15 0 0 0 0 0

Current limitations

  • No binary fields - current specifications support only prime field.
  • No sparse constraints - transition constraints in current specifications are limited to constraints that apply to two consecutive execution trace rows.
You can’t perform that action at this time.