Powdr-Asm is used to define instruction sets and write programs that depend on control flow, with the aim of generating ZKPs about them. Powdr-Asm follows the execution trace table model shared by many proof systems. In fact, Powdr-Asm extends Polygon Hermez' PIL and zkASM. In such a model, the execution is represented by a two-dimensional fixed-size table, where columns represent the state (for example, registers or memory) and each row represents a step in time for a given execution. Constraints specify how the state evolves from any step to the next.
As an example, let's apply that model to a program that computes the factorial of a number. Our state consists of two registers:
- CNT - a counter
- ACC - the answer accumulator
The first row represents the initial state of our program, that is, PC = 0, CNT = <input>, ACC = 1.
From then on, we compute the subsequent rows with the following pseudocode:
START:
Is CNT = 0?
If yes go to END
ACC := ACC * CNT
CNT := CNT - 1
Go to START
END:
ACC equals factorial(input)
We can compute the following execution trace with 5 as input:
| CNT | ACC |
|---|---|
| 5 | 1 |
| 4 | 5 |
| 3 | 20 |
| 2 | 60 |
| 1 | 120 |
| 0 | 120 |
Note that the height of the table limits the length of the trace.
There are three constructs that can be used to define an instruction set:
- Registers
- Macros
- Instructions
Registers are basic state components that can store a single number. There are three types of registers:
- Program Counter (PC). Used for control flow.
- Assignment registers. Used by parametric instructions and for assignments.
- General registers. Used by program logic.
The registers are declared in the following way:
reg pc[@pc];
reg X[<=];
reg A;In the snippet above, the @pc annotation means that pc is implicitly
incremented by one for instructions that do not explicitly assign it. The <= annotation
means X is an assignment register and can be used by parametric instructions
and for assignments.
Finally, A is a general purpose register and can be used by program logic.
Instructions are predicates that define constraints that are enforced only when the
instruction is invoked. The constraints may refer to registers on the execution
trace line that it is invoked and/or the next line.
If the next line version of a register is used, for example X', it must be in
the LHS of the expression, where the RHS contains no next registers.
If an instruction has formal parameters, they must be either literals or
assignment registers.
instr ADD X, Y -> Z { X + Y = Z }The above instruction can be read as "If Z is the same as X + Y, then ADD X Y returns Z".
As an analogy, this is similar to Prolog predicates.
Macros can be used to build expressions which are inlined at the call site.
macro if_then_else(condition, true_value, false_value) {
condition * true_value + (1 - condition) * false_value
};The macro above can be used to simplify if-then-else arithmetic expressions.
We now have enough constructs to create a simple ISA and implement our Factorial program.
pil {
col witness XInv;
col witness XIsZero;
XIsZero * (1 - XIsZero) = 0;
XIsZero = 1 - X * XInv;
XIsZero * X = 0;
}
macro if_then_else(condition, true_value, false_value) {
condition * true_value + (1 - condition) * false_value
};
macro jump_to(target) { pc' = target; };
macro jump_to_if(condition, target) {
jump_to(if_then_else(condition, target, pc + 1));
};
reg pc[@pc];
reg X[<=];
reg CNT;
reg ACC;
instr jmpz X, l: label { jump_to_if(XIsZero, l) }
instr jmp l: label { jump_to(l) }
instr dec_CNT { CNT' = CNT - 1 }
instr assert_zero X { XIsZero = 1 }
CNT <=X= ${ ("input", 0) };
start::
jmpz CNT, end;
ACC <=X= ACC + ${ ("input", CNT) };
dec_CNT;
jmp start;
end::The beginning of the snippet above is a necessary gadget that computes whether
X is 0 at a certain point.
The macros, registers and instructions define our ISA, and can be used to write any programs that only need these features.
Finally we have the program itself, which can be either manually written or automatically compiled from some higher level language.