Machines
Machines are the first main concept in powdr-asm. They can currently be of two types: virtual or constrained.
Virtual machines
Dynamic machines are defined by:
- a degree range, indicating the number of execution steps
- a set of registers, including a program counter
- an instruction set
- a set of powdr-pil statements
- a set of functions
- a set of submachines
An example of a simple dynamic machine is the following:
machine HelloWorld with degree: 8 {
// this simple machine does not have submachines
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg A;
instr incr X -> Y {
Y = X + 1
}
instr decr X -> Y {
Y = X - 1
}
instr assert_zero X {
X = 0
}
// the main function assigns the first prover input to A, increments it, decrements it, and loops forever
function main {
A <=X= ${ std::prelude::Query::Input(0, 1) };
A <== incr(A);
A <== decr(A);
assert_zero A;
return;
}
}
Constrained machines
Constrained machines are a lower-level type of machine. They do not have registers, and instead rely on simple committed and fixed columns. They are used to implement hand-optimized computation.
They are defined by:
- a degree range, indicating the number of execution steps
- a set of operations
- an
operation_identifier
column, used to make constraints conditional over which function is called. It can be omitted with_
if the machine has at most one operation. - a
latch
column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations. - a set of submachines
- a set of links
An example of a simple constrained machine is the following:
machine SimpleStatic with
degree: 8,
latch: latch,
operation_id: operation_id
{
operation power_4<0> x -> y;
col fixed operation_id = [0]*;
col fixed latch = [0, 0, 0, 1]*;
col witness x;
col witness y;
// initialise y to x at the beginning of each block
latch * (y' - x') = 0;
// x is unconstrained at the beginning of the block
// x is constant within a block
(1 - latch) * (x' - x) = 0;
// y is multiplied by x at each row
(1 - latch) * (y' - x * y) = 0;
}
For more details on the powdr-pil statements, check out the pil section of this book. Note that the parameters of the operation are columns defined in powdr-pil statements.
Submachines
Machines can have submachines which they access by defining external instructions or links. They are declared as follows:
machine MySubmachine {
...
}
machine MyMachine {
MySubmachine my_submachine;
}
Machines can also receive submachines as construction parameters. A machine passed in as an argument can be accessed in the same way as locally declared submachines:
machine MachineWithParam(subm: MySubmachine) {
// `subm` can be accessed as a submachine
...
}
machine MyMachine {
MySubmachine my_submachine;
// `my_submachine` is passed to `another_submachine` as a construction argument
MachineWithParam another_submachine(my_submachine);
}