Example AIR in AirScript

This is an example AIR definition in AirScript that includes all existing AirScript syntax. It is intended to be syntactically demonstrative rather than meaningful.

Complete Example

def ExampleAir

trace_columns {
    main: [s, a, b, c],
}

public_inputs {
    stack_inputs: [16],
    stack_outputs: [16],
}

periodic_columns {
    k0: [1, 1, 1, 1, 1, 1, 1, 0],
}

buses {
    logup q,
}

boundary_constraints {
    # define boundary constraints against the main trace at the first row of the trace.
    enf a.first = stack_inputs[0];
    enf b.first = stack_inputs[1];
    enf c.first = stack_inputs[2];

    # define boundary constraints against the main trace at the last row of the trace.
    enf a.last = stack_outputs[0];
    enf b.last = stack_outputs[1];
    enf c.last = stack_outputs[2];

    # set the bus q to be empty at the beginning and end
    enf q.first = null;
    enf q.last = null;
}

integrity_constraints {
    # the selector must be binary.
    enf s^2 = s;

    # selector should stay the same for all rows of an 8-row cycle.
    enf k0 * (s' - s) = 0;

    # c = a + b when s = 0.
    enf (1 - s) * (c - a - b) = 0;

    # c = a * b when s = 1.
    enf s * (c - a * b) = 0;

    # insert c to the q bus when s = 1
    q.insert(c) when s;
}

Additional Examples

For more practical examples, see the included examples in the docs/examples/ directory:

Simple Addition

def SimpleAddition

trace_columns {
    main: [a, b, c],
}

public_inputs {
    inputs: [2],
    outputs: [1],
}

periodic_columns {
    k0: [1, 1, 1, 1, 1, 1, 1, 0],
}

boundary_constraints {
    enf a.first = inputs[0];
    enf b.first = inputs[1];
    enf c.first = 0;

    enf a.last = outputs[0];
    enf b.last = outputs[0];
    enf c.last = 0;
}

integrity_constraints {
    enf k0 * (a' - a) = 0;
    enf k0 * (b' - b) = 0;
    
    enf c' = c + a + b;
}

Fibonacci Sequence

def Fibonacci

trace_columns {
    main: [a, b],
}

public_inputs {
    inputs: [32],
}

periodic_columns {
    k0: [1, 1, 1, 1, 1, 1, 1, 0],
}

boundary_constraints {
    enf a.first = 0;
    enf b.first = 1;
}

integrity_constraints {
    enf k0 * (a' - b) = 0;
    enf k0 * (b' - a - b) = 0;
}