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.