Instructions

Instructions are declared as part of a powdr virtual machine. Once defined, they can be called by any function in this machine. An instruction is composed of:

• a name
• a set of inputs (assignment registers or labels)
• a set of outputs (assignment registers)
• a set of powdr-pil constraints to activate when the instruction is called
• a set of links calling into functions/operations in submachines

Local instructions

A local instruction is the simplest type of instruction. It is called local because its behavior is defined by a set of constraints over registers and columns of the machine it is defined in.

instr add X, Y -> Z {
    X + Y = Z
}

Instructions with links

Instructions may also delegate all or part of their implementation to functions/operations in submachines. Each link in an instruction defines the inputs and outputs of a call to a specific function/operation in a submachine.

Assume we have a submachine with a single operation add:

machine SubMachine with
    degree: 32,
    latch: latch,
    operation_id: operation_id
{
    col witness operation_id;
    col fixed latch = [1]*;

    operation add<0> x, y -> z;

    col witness x;
    col witness y;
    col witness z;
    z = y + x;
}

An instruction calling into this operation can be declared as follows:

    SubMachine submachine;

    instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call

In the previous example, only assignment registers (instruction inputs and outputs) were used to call the submachine. The following example shows more complex usage of link calls:

machine Main with degree: 32 {
    reg pc[@pc];
    reg X[<=];
    reg Y[<=];
    reg Z[<=];
    reg A;
    reg B;
    reg C;

    SubMachine submachine;

    instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
    instr add_to_A X, Y link => A' = submachine.add(X, Y);// - output to a regular register
    instr addAB -> X link => X = submachine.add(A, B);    // - inputs from regular registers
    instr addAB_to_C link => C' = submachine.add(A, B);   // - inputs and output from regular registers
    instr addAB_to_A link => A' = submachine.add(A, B);   // - reusing an input register as output
    instr sub X, Y -> Z link => X = submachine.add(Y, Z); // - swapping input/output
    // expressions can also be used as call parameters
    instr add5 X -> Z link => Z = submachine.add(X, 3+2); // - literal expression as argument
    col fixed STEP(i) { i };
    instr add_current_time_step X -> Z link => Z = submachine.add(X, STEP);// - machine columns can be referenced
    let arr = [1,2,3,4,5];                          // - functions can be used
    instr add_arr_sum X -> Z link => Z = submachine.add(X, std::array::sum(arr));

    instr assert_eq X, Y { X = Y }

    function main {
        A <== add(2, 3);
        assert_eq A, 5;
        add_to_A 6, 7;
        assert_eq A, 13;

        A <== sub(6, 5);
        assert_eq A, 1;
        B <=X= 20;
        C <== addAB();
        assert_eq C, 21;

        A <=X= 2;
        B <=X= 3;
        addAB_to_C;
        assert_eq C, 5;

        A <=X= 33;
        B <=X= 44;
        addAB_to_A;
        assert_eq A, 77;

        A <== add5(2);
        assert_eq A, 7;
        A <== add_arr_sum(3);
        assert_eq A, 18;

        // Note that the result of this operation depends on when it executed (STEP column)
        A <== add_current_time_step(42);
        B <== add_current_time_step(42);
        assert_eq B - A, 1;

        return;
    }
}

A single instruction can activate multiple links, and may also include a set of constraints. Furthermore, each link can be activated conditionally, based on a given boolean flag:

machine Main with degree: 16 {
    reg pc[@pc];
    reg X[<=];
    reg Y[<=];
    reg Z[<=];
    reg W[<=];
    reg A;
    col witness B;
    col witness C;

    SubMachine submachine;

    // multiple links can be activated by a single instruction,
    // witness columns can be used for temporary values,
    // and additional constraints can be used
    instr double_then_mul X, Y -> Z
        link => B = submachine.add(X, X)
        link => C = submachine.add(Y, Y)
    {
        Z = B * C
    }

    // links activated conditional on a boolean flag
    instr add_or_sub W, X, Y -> Z
        link if W => Z = submachine.add(X, Y)
        link if (1 - W) => Z = submachine.sub(X, Y);

    instr assert_eq X, Y { X = Y }

    function main {
        A <== double_then_mul(3, 2);
        assert_eq A, 24;

        A <== add_or_sub(1, 3, 2);
        assert_eq A, 5;
        A <== add_or_sub(0, 3, 2);
        assert_eq A, 1;

        return;
    }
}

Note that links cannot currently call functions from the same machine: they delegate computation to a submachine.