Operations

Operations enable a constrained machine to expose behavior to the outside. If a machine has a single operation, it can simply be declared with its name and parameters:

machine Add with
    latch: latch
{
    // operation name, with column names as inputs and outputs
    operation add a, b -> c;

    col fixed latch = [1]*;

    col witness a;
    col witness b;
    col witness c;

    // constraint "implementing" the operation
    c = a + b;
}

The parameters of the operation (inputs and outputs) must be columns declared in the machine.

If a machine exposes more than one operation, the machine itself needs an operation id column (op_id in the following). Then, each operation needs to be declared with its own unique operation id:

// machine declaration must include an operation id column name
machine AddSub with
    latch: latch,
    operation_id: op_id
{
    // each operation has its own unique operation id
    operation add<0> a, b -> c;
    operation sub<1> a, b -> c;

    col fixed latch = [1]*;
        // it also needs to be declared as a column
    col witness op_id;

    col witness a;
    col witness b;
    col witness c;

    // constraint "implementing" both operations, depending on `op_id`
    c = (1 - op_id) * (a + b) + op_id * (a - b);
}

The actual behavior of an operation is defined by the machine constraints on the columns used as inputs and outputs.