Operations

Operations enable a constrained machine to expose behavior to the outside.

machine Arith(latch, operation_id) {
    operation add<0> a, b -> c;
    operation sub<1> a, b -> c;

    col witness operation_id;
    col fixed latch = [1]*;

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

    c = (1 - operation_id) * (a + b) + operation_id * (a - b);
}

They are defined by:

  • a value for the operation id. When calling this operation, the operation id of this machine is set to this value.
  • parameters in the form of columns defined in the current machine

The actual behavior of the operation is defined freely as constraints.