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>;.

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[].
  • Symbols evaluating to a number or with type fe are constants.
  • Symbols without type but with a value that is a function with a single parameter are fixed columns.
  • Symbols defined with a value and type col (or col[]) are fixed columns (or arrays of fixed columns).
  • Everything else is a "generic symbol" that is not a column or constant.

Note that the type col is the same as int -> fe, so let w: int -> fe also declares a witness column.

Examples:

#![allow(unused)]
fn main() {
    // This defines a constant
    let rows = 2**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.
    let x;
    // This functions defines a fixed column where each cell contains the
    // square of its row number.
    let square: col = |x| x*x;
    // The same function as `square` above, but now its type is given as
    // `int -> int` and thus it is *not* classified as a column. Instead,
    // it is stored as a utility function. If utility functions are
    // referenced in constraints, they have to be evaluated, meaning that
    // the constraint `w = square_non_column;` is invalid but both
    // `w = square_non_column(7);` and `w = square;` are valid constraints.
    let square_non_column: int -> int = |x| x*x;
    // A recursive function, taking a function and an integer as parameter
    let sum = |f, i| match i {
        0 => f(0),
        _ => f(i) + sum(f, i - 1)
    };
}