Local Variables and Built-in Variables

This section describes the syntax for declaring local variables and built-in variables.

Variables

In AirScript, variables can be declared in boundary_constraints and integrity_constraints sections and can contain any expression that would be valid within that source section. Variables can be of type scalar, vector or matrix. In the example below, x is a variable of type scalar, y is a variable of type vector and z is a variable of type matrix.

def VariablesExample

const A = 1;
const B = 2;

trace_columns {
    main: [a, b, c, d],
    aux: [e, f],
}

public_inputs {
    stack_inputs: [16],
}

random_values {
    rand: [16],
}

boundary_constraints {
    let x = stack_inputs[0] + stack_inputs[1]   ;
    let y = [$rand[0], $rand[1]]  ;
    enf e.first = x + y[0] + y[1];
}

integrity_constraints {
    let z = [
        [a + b, c + d],
        [A * a, B * b]
    ];
    enf a' = z[0][0] + z[0][1] + z[1][0] + z[1][1];
}

Syntax restriction for local variables

Currently, it is not possible to:

1. Create matrices containing both arrays and references to arrays.

   Example:

   ...
   boundary_constraints {
       let a = [[1,2], [3,4]];  # <-- this is allowed
       let b = [1, 2];
       let c = [a[1], b];  # <-- this is allowed
       let d = [b, [3, 4]];  # <-- this is not allowed, because `d` consists of array `[3, 4]` and reference to array `b`
       enf ...
   ...
   }
   

2. Create variables with list comprehension for which the source array is a inlined vector, a matrix row, or a range in matrix row.

   Example:

   ...
   integrity_constraints {
       let a = [[1, 2], [3, 4]];
       let b = [5, 6];
       let c = 7;
       let d = [e for e in [8, 9, 10]];  # <-- source array is an inlined vector
       let f = [g for g in a[1]];  # <-- source is a matrix row
       let h = [i for i in a[0][0..2]];  # <-- source is a range in matrix row
       enf ...
   ...
   }
   

Built-in variables

Built-in variables are identified by the starting character $. There are two built-in variables:

$main

$main is used to access columns in the main execution trace.

These columns may be accessed by using the indexing operator on $main. For example, $main[i] provides the (i+1)th column in the main execution trace.

Columns using the $main built-in may only be accessed within source sections for integrity constraints, i.e. the integrity_constraints section.

$aux

$aux is used to access columns in the auxiliary execution trace.

These columns may be accessed by using the indexing operator on $aux. For example, $aux[i] provides the (i+1)th column in the auxiliary execution trace.

Columns using the $aux built-in may only be accessed within source sections for integrity constraints, i.e. the integrity_constraints section.