Registers

Registers are central to a machine. powdr supports a few types of registers:

Program counter

Each machine can have at most one program counter. In the absence of a program counter, the machine is considered static, and no other register can be declared. The program counter is defined as follows:

reg pc[@pc]

At each step execution step, the program counter points to the function line to execute. The program counter behaves like a write register, with the exception that its value is incremented by default after each step.

Write registers

Write registers are the default type for registers. They are declared as follows:

reg A;

They hold a field element, are initialized as 0 at the beginning of a function and keep their value by default. They can be read from and written to.

// write to A
A <=X= 1;
// A is 1

// read from A
B <=X= A;
// A is still 1

Assignment registers

Assignment registers are transient to an execution step: their value is not persisted across steps. They are required in order to pass inputs and receive outputs from instructions, as well as in assignments. For example, if we want to assert that write register A is 0, we can use the following instruction:

reg pc[@pc];
reg A;

instr assert_A_is_zero {
    A = 0
}

function main {
    assert_A_is_zero;
    return;
}

However, if we want the instruction to accept any write register as input, we use an assignment register.

reg pc[@pc];
reg X[<=];
reg A;    

instr assert_zero X {
    X = 0
}

function main {
    assert_zero A;
    return;
}

Read-only registers

Read-only registers are used for function inputs. However, powdr creates them automatically based on functions arguments, so that they do not need to be declared explicitly.

Read-only registers are only mentioned for completeness here and are currently only used inside the compiler. We advise against using them.