Instructions

Instructions are declared as part of a powdr virtual machine. Their inputs and outputs are assignment registers as well as labels. Once defined, they can be called by any function in this machine.

Local instructions

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

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

Instructions feature:

  • a name
  • some inputs
  • some outputs
  • a set of powdr-pil constraints to activate when the instruction is called

External instructions

An external instruction delegates its implementation to a function/operation from a submachine. When called, the inputs and outputs of the declared instruction are mapped into a call to the submachine function.

Assume we have a submachine with a single operation add:

machine SubMachine(latch, 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 external instruction calling into this operation can be declared as follows:

    SubMachine submachine;

    instr add X, Y -> Z = submachine.add; // - trivial usage, equivalent to:
                                          //   instr add X, Y -> Z = submachine.add X, Y -> Z;

The left-hand side of the definition declares the local instruction and which assignment registers are used in its inputs and outputs. It describes how the instruction is used. The right-hand side of the definition specifies the call to the external operation, with its inputs and outputs. All assignment registers on the left-hand side must be used in the call to the external operation.

In the previous example, parameters of the instruction match exactly with how the target operation should be called, and the right-hand parameters can thus be omitted. The following example shows more complex usages of external instructions:

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

    SubMachine submachine;

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

    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
        A <== add_current_time_step(42);
        B <== add_current_time_step(42);
        assert_eq B - A, 1;

        return;
    }
}

Note that external instructions cannot currently link to functions of the same machine: they delegate computation to a submachine.