Working ISA Spec
maxgillett opened this issue · 6 comments
Note that the spec below may be subject to change, and includes contributions made by @clvv and @dlubarov.
Last updated: 6/21/2023
Architecture
A Valida zkVM consists of a CPU and several coprocessors, which are connected with communication buses. A basic example of a machine layout, omitting some standard chips for simplicity, would be
graph TD;
CpuChip --- MemoryChip;
CpuChip --- MemoryChip;
CpuChip --- MemoryChip;
MemoryChip --- PagerChip;
CpuChip --- MonolithChip;
PagerChip --- MonolithChip;
CpuChip --- LogicChip;
CpuChip --- Add32Chip;
CpuChip --- Mul32Chip;
CpuChip --- OutputChip;
Communication buses are implemented using the logarithmic derivative lookup argument, and are multiplexed for efficiency (i.e. CPU interactions with multiple chips may share the same bus).
There are multiple VM configurations. The "Core" configuration is always present, and provides instructions for basic control flow and memory access. Additional configurations, such as "Field Arithmetic" or "Additional Jump" build upon the core configuration and offer additional instructions.
Instruction format
Instructions are encoded in groups of 6 field elements. The first element in the group contains the opcode, followed by three elements representing the operands and two immediate value flags:
Program ROM
Our VM operates under the Harvard architecture, where program code is stored separately from main memory. Code is addressed by any field element, starting from pc
stores the location (a field element) of the instruction that is being executed.
Memory
Memory is comprised of word-addressable cells. A given cell contains 4 field elements, each of which are typically used to store a single byte (arbitrary field elements can also be stored). All core and ALU-related instructions operate on cells (i.e. any operand address is word aligned -- a multiple of 4). In the VM compiler, the address of newly added local variables in the stack is word aligned.
For example, a U32 is represented in memory by its byte decomposition (4 elements). To initialize a U32 from an immediate value, we use the SETL16
instruction (see the complete instruction list below), which sets the first two bytes in memory. To initialize a U32 value greater than 16 bits, we can also call the SETH16
instruction to set the upper two bytes.
Immediate Values
Our VM cannot represent operand values that are greater than the prime
Registers
Our zkVM does not operate on general purpose registers. Instead, instructions refer to variables local to the call frame, i.e. relative to the current frame pointer fp
.
Notation
The following notation is used throughout this document:
Operand values: opa
, opb
, opc
denote the value encoded in the operand a, b, or c of the current instruction.
CPU registers: fp
, pc
denote the value of the current frame pointer and program counter, respectively.
Relative addressing: [a]
denote the cell value at address a
offset from fp
, i.e. fp + a
. Variables local to the call frame are denoted in this form. Note that we are omitting fp
in the expression here, but that the first dereference of an operand is always relative to the frame pointer.
Absolute addressing: [[a]]
denotes the cell value at absolute address [a]
. Heap-allocated values are denoted in this form.
To refer to relative or absolute element values, we use the notation $[a]\text{elem}$ or $[[a]]\text{elem}$ respectively.
Instruction list
Each instruction contains 5 field element operands,
Listed below are the instructions offered in each configuration.
Core
Mnemonic | Operands (asm) |
Description |
---|---|---|
LW / LOAD32 | a(fp), c(fp) |
Follow the pointer stored at offset |
SW / STORE32 | b(fp), c(fp) |
Write the 4 byte values beginning at the address stroed at offset |
JAL | a(fp), b, c |
Jump to address and link: Store the |
JALV | a(fp), b(fp), c(fp) |
Jump to variable and link: Store the |
BEQ | a, b(fp), c(fp) |
If |
BEQI | a, b(fp), c |
If |
BNE | a, b(fp), c(fp) |
If |
BNEI | a, b(fp), c |
If |
IMM32 | a, b, c, d, e |
Write the immediate values |
Field arithmetic
Mnemonic | Operands (asm) |
Description |
---|---|---|
FEADD | a(fp), b(fp), c(fp) |
|
FEMUL | a(fp), b(fp), c(fp) |
|
TO_FE | a(fp), b(fp) |
Convert an U32, represented by 4 field elements starting at offset b, to a field element stored to the first field element at offset |
FROM_FE | a(fp), b(fp) |
Convert a field element |
Note that field arithmetic instructions only operate on the first element in a cell, which represents a field element instead of a single byte.
U32 Arithmetic
Mnemonic | Operands (asm) |
Description |
---|---|---|
ADD | a(fp), b(fp), c(fp) |
Compute the unchecked addition of the U32 values at cell offsets |
ADDI | a(fp), b(fp), c |
Compute the unchecked addition of the U32 variable at cell offsets |
SUB | a(fp), b(fp), c(fp) |
Unchecked subtraction |
SUBI | a(fp), b(fp), c |
Unchecked subtraction |
MUL | a(fp), b(fp), c(fp) |
Unchecked multiplication |
MULI | a(fp), b(fp), c |
Unchecked subtraction |
DIV | a(fp), b(fp), c(fp) |
Division |
SH{L,R} | a(fp), b(fp), c(fp) |
Shift [b] left/right by [c] and write to offset |
SH{L,R}I | a(fp), b(fp), c |
Shift [b] left/right by c and write to offset |
ISH{L,R} | a(fp), b, c(fp) |
Shift b left/right by [c] and write to offset |
LT | a(fp), b(fp), c(fp) |
Set local variable |
LTI | a(fp), b(fp), c |
Set local variable |
Bitwise
Mnemonic | Operands (asm) | Description |
---|---|---|
AND | a(fp), b(fp), c(fp) |
Set |
OR | a(fp), b(fp), c(fp) |
Set |
XOR | a(fp), b(fp), c(fp) |
Set |
Byte Manipulation
Note: These will not be supported in the initial version.
Instruction | Operands (asm) |
|
---|---|---|
LOAD8 | a(fp), b(fp) |
Load a byte at the address specified by local variable at offset |
STORE8 | b(fp), c(fp) |
Store a byte encoded at offset |
STORE8I | b(fp), c |
Store a byte encoded in the field element |
Heap allocation
Notes:
- Fixed configurable stack size (e.g. 8MB), growing in opposite direction of the heap.
- Allocate-only malloc (no de-allocation using
free
)
Assembly
Instructions
We will closely follow RISC-V assembly, making modifications as necessary. The most important difference between our zkVM assembly and RV32IM is that instead of registers x0-31
, we only have two special-purpose registers fp
and pc
. However, we have (up to fp
.
Calling convention / stack frame
Stack (grows downwards, i.e. address decreases from top row to bottom row) |
---|
Arg 2 |
Arg 1 |
Return FP |
Return value |
Return address (<- Current fp) |
Local 1 |
Local 2 |
... |
Local N |
We follow the RISC-V convention and grow the stack downwards. For a function call, the arguments are pushed onto the stack in reverse order. We only allow statically sized allocation on the stack, unlike traditional architectures where alloca
can be used to allocate dynamically. All dynamic allocation will be compiled to heap allocations. Instead of using a frame pointer that points at the begining of the frame, we use a stack pointer which points at the first free stack cell.
Note that:
- Functions arguments are stored at fp + 12, fp + 16, ...
- Return FP (the value of FP before the call) is stored at fp+8
- Return value is stored at fp + 4
- Return address is stored at fp
- Local variables are stored at fp - 4, fp - 8, ...
Pseudo instructions
Pseudo Instruction | Instruction |
---|---|
call label |
imm32 (-b+8)(fp), 0, 0, 0, -b(fp) ; jal -b(fp), label, -b(fp) , where b is the size of the current stack frame plus the call frame size for instantiating a call to label |
ret |
jalv -4(fp), 0(fp), 8(fp) |
Implementing MEMCPY/SET/MOVE
Memcpy will require roughly 2 cycles per word. We can follow this memcpy implementation on RISC-V.
Example program
; fib.s
...
fib: ; @fib
; %bb.0:
sw -4(fp), 12(fp)
imm32 -8(fp), 0, 0, 0, 0
imm32 -12(fp), 0, 0, 0, 1
imm32 -16(fp), 0, 0, 0, 0
beq .LBB0_1, 0(fp), 0(fp)
.LBB0_1:
bne .LBB0_2, -16(fp), -4(fp)
beq .LBB0_4, 0(fp), 0(fp)
; %bb.2:
add -20(fp), -8(fp), -12(fp)
sw -8(fp), -12(fp)
sw -12(fp), -20(fp)
beq .LBB0_3, 0(fp), 0(fp)
; %bb.3:
addi -16(fp), -16(fp), 1
beq .LBB0_1, 0(fp), 0(fp)
.LBB0_4:
sw 4(fp), -8(fp)
jalv -4(fp), 0(fp), 8(fp)
...
main: ; @main
; %bb.0:
imm32 -4(fp), 0, 0, 0, 0
imm32 -8(fp), 0, 0, 0, 10
sw -16(fp), -8(fp)
imm32 -20(fp), 0, 0, 0, 28
jal -28(fp), fib, -28
sw -12(fp), -24(fp)
sw 4(fp), -12(fp)
jalv -4(fp), 0(fp), 8(fp)
...
The (partial) stack at the time of executing the first instruction (sw
) inside fib
after the call from main
(line 6 above) looks like:
Stack | Description |
---|---|
10 | Argument 1 |
28 | Return frame pointer |
... | Return value |
main:6 | Return address |
... | Local variable 1 (unset) |
... | Local variable 2 (unset) |
Trace
Main CPU
Columns | Configuration | Description |
---|---|---|
Core | Clock cycle | |
Core | Program counter | |
Core | Frame pointer | |
Core | Instruction opcode | |
Core | Operand |
|
Core | Operand |
|
Core | Operand |
|
Core | Operand |
|
Core | Operand |
|
Core |
|
|
Core |
|
|
Core |
Columns
Trace cells are also allocated to hold buffered read memory values for
We read and write 4 elements from memory at a time to the main trace. These elements are only constrained when the immediate value flags are not set (see the "Instruction Decoding" section below):
Cell | Configuration | Description |
---|---|---|
Core | $[\text{addr}a]\text{elem}$ | |
Core | $[\text{addr}a+1]\text{elem}$ | |
Core | $[\text{addr}a+2]\text{elem}$ | |
Core | $[\text{addr}a+3]\text{elem}$ | |
Core | $[\text{addr}b]\text{elem}$ | |
Core | $[\text{addr}b+1]\text{elem}$ | |
Core | $[\text{addr}b+2]\text{elem}$ | |
Core | $[\text{addr}b+3]\text{elem}$ | |
Core | Value written to |
|
Core | Value written to |
|
Core | Value written to |
|
Core | Value written to |
Memory
Cell | Description |
---|---|
Address | |
Clock cycle | |
Value 0 | |
Value 1 | |
Value 2 | |
Value 3 | |
Lower 16 bits of |
|
Upper 16 bits of |
|
Nondeterministic inverse of |
The memory table is sorted by (
Instruction decoding
Trace cells are also allocated for each selector. In each cycle, main CPU opcodes are decoded into binary selector flags, or to a single is_bus_opcode
flag in the case that the opcode is processed by a different chip.
Instruction Trace
Each instruction is encoded as 6 field elements
Core
Mnemonic | Operands (asm) | Encoded |
---|---|---|
LW / LOAD32 | a(fp), c(fp) |
|
SW / STORE32 | b(fp), c(fp) |
|
JAL | a(fp), b, c |
|
JALV | a(fp), b(fp), c |
|
BEQ | a, b(fp), c(fp) |
|
BEQ | a, b(fp), c |
|
BNE | a, b(fp), c(fp) |
|
BNEI | a, b(fp), c |
|
IMM32 | a, b, c, d, e |
|
Field arithmetic
Mnemonic | Operands (asm) | Encoded |
---|---|---|
FEADD | a(fp), b(fp), c(fp) |
|
FEMUL | a(fp), b(fp), c(fp) |
|
TO_FE | a(fp), b(fp) |
|
FROM_FE | a(fp), b(fp) |
U32 Arithmetic
Mnemonic | Operands (asm) | Encoded |
---|---|---|
ADD | a(fp), b(fp), c(fp) |
|
ADDI | a(fp), b(fp), c |
|
SUB | a(fp), b(fp), c(fp) |
|
SUBI | a(fp), b(fp), c |
|
MUL | a(fp), b(fp), c(fp) |
|
MULI | a(fp), b(fp), c |
|
DIV | a(fp), b(fp), c(fp) |
|
SH{L,R} | a(fp), b(fp), c(fp) |
|
SH{L,R}I | a(fp), b(fp), c |
|
ISH{L,R} | a(fp), b, c(fp) |
|
SLT | a(fp), b(fp), c(fp) |
|
SLT | a(fp), b(fp), c |
|
Bitwise
Mnemonic | Operands (asm) | Encoded |
---|---|---|
AND | a(fp), b(fp), c(fp) |
|
OR | a(fp), b(fp), c(fp) |
|
XOR | a(fp), b(fp), c(fp) |
|
Design notes
Frontend target
We are writing a compiler from LLVM IR to our ISA
ZK stack
This is a STARK-based zkVM. We are using Plonky3 to implement the polynomial IOP and PCS.
Field choice
We plan to use the 32-bit field defined by p = 2^31 - 1
, which should give very good performance on GPUs or with most vector instruction sets.
Registers
Our VM has no general purpose registers, since memory is cheap.
Memory
We will use a conventional R/W memory.
Tables
The CPU can do up to three memory operations per cycle, to support binary operations involving two reads and one write.
If we used a single-trace model, we could support this by adding columns for 6 memory operations in each row of our trace: 3 for the chronological memory log and 3 for the (address, timestamp)
ordered memory log.
Instead, we make the memory a separate table (i.e. a separate STARK which gets connected with a permutation argument). We also use multi-table support to implement other coprocessors that are wasteful to include in the main CPU, as their operations may not be used during most cycles (e.g. Keccak).
Continuations
TODO: Explain the permutation-based continuation implementation.
Lookups
Initially, we will support lookups only against prover-supplied tables. The main use case is range checks. To perform a 16-bit range check, for example, we would have the prover send a table containing [0 .. 2^16 - 1]
in order. (If the trace was not already 2^16, we would pad it. If it was longer than 2^16, the prover would include some duplicates.) We would then use constraints to enforce that this table starts at 0, ends at 2^16 - 1, and increments by 0 or 1.
Preprocessed tables can also be useful, particularly for bitwise operations like xor. However, we will not support them initially because they require non-succinct preprocessing.
Floating point arithmetic
Fast floating point arithmetic doesn't seem important for our anticipated use cases, so we will convert float operations to integer ones during compilation.
Should we define both STOREI16
(low) and STOREh16
(high) to be able to write to any byte of a word?
I guess we can start by sorting the calling convention and the related code in TargetLowering
.
That is to say, successfully compiling this snippet may be one of the item in the first milestone:
define i16 @main(i32 %a, i16 %b, i8 %c) {
ret i16 %b
}
I think this LLVM backend can be done in similar to WebAssmebly , something like https://github.com/llvm/llvm-project/blob/main/llvm/lib/Target/WebAssembly/WebAssemblyReplacePhysRegs.cpp
I guess we can start by sorting the calling convention and the related code in
TargetLowering
.That is to say, successfully compiling this snippet may be one of the item in the first milestone:
define i16 @main(i32 %a, i16 %b, i8 %c) { ret i16 %b }
Yes, I think that's a good plan. I started working towards this goal by implementing call lowering in GlobalISel. I still need to implement CallLowering::OutgoingValueHandler
. IR translation is working for lowering formal arguments into the stack, but legalization and instruction selection is not complete (see issues #3 and #4).
I think this LLVM backend can be done in similar to WebAssmebly , something like https://github.com/llvm/llvm-project/blob/main/llvm/lib/Target/WebAssembly/WebAssemblyReplacePhysRegs.cpp
Yes, I think there are similarities. I think the problem simplifies if using GlobalISel (which WebAssembly does not use), because we can match instructions directly to virtual registers in that framework, and never have to allocate physical registers (edit: I might be wrong about this. It seems you do need to assign virtual registers to a physical register bank first, but like you pointed out, this can probably still be replaced with a virtual register.)
The implemented READ_ADVICE
and WRITE_ADVICE
instructions are missing from the spec.