Declarations

Powdr-pil allows the same syntax to declare various kinds of symbols. This includes constants, fixed columns, witness columns and even higher-order functions. It deduces the symbol kind from the type of the symbol and the way the symbol is used.

Symbols can be declared using let <name>; and they can be declared and defined using let <name> = <value>;, where <value> is an expression. The type of the symbol can be explicitly specified using let <name>: <type>; and let <name>: <type> = <value>;. Symbols with a generic type can be defined using let<TV1, TV1, ..> <name>: <type> = <value>;, where the TV are newly created type variables that can be used in the type.

This syntax can be used for constants, fixed columns, witness columns and even (higher-order) functions that can transform expressions. The kind of symbol is deduced by its type and the way the symbol is used:

Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be col or col[k].
Symbols defined with a value and type col (or col[k]) are fixed columns (or arrays of fixed columns).
Symbols defined with a value and type expr (or expr[k]) are intermediate columns (or arrays of intermediate columns).
Everything else is a "generic symbol" that is not a column.

Examples:

    // This defines a integer constant. We can omit the type when it is used
    // somewhere that constrains its type. Since it is not used below,
    // we have to specify `: int` (another option would be `fe`, field element).
    let rows: int = 16;
    // This defines a fixed column that contains the row number in each row.
    // Only symbols whose type is "col" are considered fixed columns.
    let step: col = |i| i;
    // Here, we have a witness column, the do not need an explicit `: col`.
    let x;
    // This functions defines a fixed column where each cell contains the
    // square of its row number.
    let square: col = |x| x*x;
    // This is a generic function that computes the sum of an array
    // given its length.
    // It is not stored as a column.
    // If it is used in a constraint, it has to be evaulated, while
    // columns must be used symbolically.
    let<T: Add + FromLiteral> sum: T[], int -> T = |a, len| match len {
        0 => 0,
        _ => sum(a, len - 1) + a[len - 1],
    };
    // This is a constraint that uses the `sum` function:
    sum([x, step], 2) = 0;

Name lookup is performed as follows:

Lookup is performed starting from the current namespace, going up to the root component by component where the first match is used. If all lookups fail, a last attempt is done inside the std::prelude namespace.

powdr

Declarations