Machines

Machines are the first main concept in powdr-asm. They can currently be of two types: virtual or constrained.

Virtual machines

Dynamic machines are defined by:

An example of a simple dynamic machine is the following:

machine HelloWorld with degree: 8 {
    // this simple machine does not have submachines

    reg pc[@pc];
    reg X[<=];
    reg Y[<=];
    reg A;

    instr incr X -> Y {
        Y = X + 1
    }

    instr decr X -> Y {
        Y = X - 1
    }

    instr assert_zero X {
        X = 0
    }

    // the main function assigns the first prover input to A, increments it, decrements it, and loops forever
    function main {
        A <=X= ${ std::prelude::Query::Input(0, 1) };
        A <== incr(A);
        A <== decr(A);
        assert_zero A;
        return;
    }
}

Constrained machines

Constrained machines are a lower-level type of machine. They do not have registers, and instead rely on simple committed and fixed columns. They are used to implement hand-optimized computation.

They are defined by:

  • a degree range, indicating the number of execution steps
  • a set of operations
  • an operation_identifier column, used to make constraints conditional over which function is called. It can be omitted with _ if the machine has at most one operation.
  • a latch column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations.
  • a set of submachines
  • a set of links

An example of a simple constrained machine is the following:

machine SimpleStatic with
    degree: 8,
    latch: latch,
    operation_id: operation_id
{
    operation power_4<0> x -> y;

    col fixed operation_id = [0]*;
    col fixed latch = [0, 0, 0, 1]*;
    col witness x;
    col witness y;

    // initialise y to x at the beginning of each block
    latch * (y' - x') = 0;
    // x is unconstrained at the beginning of the block

    // x is constant within a block
    (1 - latch) * (x' - x) = 0;
    // y is multiplied by x at each row
    (1 - latch) * (y' - x * y) = 0;
}

For more details on the powdr-pil statements, check out the pil section of this book. Note that the parameters of the operation are columns defined in powdr-pil statements.

Submachines

Machines can have submachines which they access by defining external instructions or links. They are declared as follows:

machine MySubmachine {
    ...
}

machine MyMachine {
    MySubmachine my_submachine;
}

Machines can also receive submachines as construction parameters. A machine passed in as an argument can be accessed in the same way as locally declared submachines:

machine MachineWithParam(subm: MySubmachine) {
    // `subm` can be accessed as a submachine
    ...
}

machine MyMachine {
    MySubmachine my_submachine;
    // `my_submachine` is passed to `another_submachine` as a construction argument
    MachineWithParam another_submachine(my_submachine);
}