Kona Book

Documentation for the Kona project.

📖 kona is in active development, and is not yet ready for use in production. During development, this book will evolve quickly and may contain inaccuracies.

Please open an issue if you find any errors or have any suggestions for improvements, and also feel free to contribute to the project!

Introduction

Kona is a suite of libraries and build pipelines for developing verifiable Rust programs targeting Fault Proof VMs .

It is built and maintained by members of OP Labs as well as open source contributors, and is licensed under the MIT License.

Kona provides tooling and abstractions around low-level syscalls, memory management, and other common structures that authors of verifiable programs will need to interact with. It also provides build pipelines for compiling no_std Rust programs to a format that can be executed by supported Fault Proof VM targets.

Goals of Kona

1. Composability

Kona provides a common set of tools and abstractions for developing verifiable Rust programs on top of several supported Fault Proof VM targets. This is done to ensure that programs written for one supported FPVM can be easily ported to another supported FPVM, and that the ecosystem of programs built on top of these targets can be easily shared and reused.

2. Safety

Through standardization of these low-level system interfaces and build pipelines, Kona seeks to increase coverage over the low-level operations that are required to build on top of a FPVM.

3. Developer Experience

Building on top of custom Rust targets can be difficult, especially when the target is nascent and tooling is not yet mature. Kona seeks to improve this experience by standardizing and streamlining the process of developing and compiling verifiable Rust programs, targeted at supported FPVMs.

4. Performance

Kona is opinionated in that it favors no_std Rust programs for embedded FPVM development, for both performance and portability. In contrast with alternative approaches, such as the op-program using the Golang MIPS32 target, no_std Rust programs produce much smaller binaries, resulting in fewer instructions that need to be executed on the FPVM. In addition, this offers developers more low-level control over interactions with the FPVM kernel, which can be useful for optimizing performance-critical code.

Development Status

Kona is currently in active development, and is not yet ready for use in production.

Contributing

Contributors are welcome! Please see the contributing guide for more information.

Fault Proof Program Development

This chapter provides an overview of Fault Proof Program development on top of the custom FPVM targets supported by Kona.

At a high level, a Fault Proof Program is not much different from a regular no_std Rust program. A custom entrypoint is provided, and the program is compiled down to a custom target, which is then executed on the FPVM.

Fault Proof Programs are structured with 3 stages:

Prologue: The bootstrapping stage, where the program is loaded into memory and the initial state is set up. During this phase, the program's initial state is written to the FPVM's memory, and the program's entrypoint is set.
Execution: The main execution stage, where the program is executed on the FPVM. During this phase, the program's entrypoint is called, and the program is executed until it exits.
Epilogue: The finalization stage, where the program's final state is read from the FPVM's memory. During this phase, the program's final state is inspected and properties of the state transition are verified.

The following sections will provide a more in-depth overview of each of these stages, as well as the tools and abstractions provided by Kona for developing your own Fault Proof Programs.

Environment

Before kicking off the development of your own Fault Proof Program , it's important to understand the environment that your program will be running in.

The FPP runs on top of a custom FPVM target, which is typically a VM with a modified subset of an existing reduced instruction set architecture and a subset of Linux syscalls. The FPVM is designed to execute verifiable programs, and commonly modifies the instruction set it is derived from as well as the internal representation of memory to support verifiable memory access, client (program) communication with the host (the FPVM), and other implementation-specific features.

Host <-> Client Communication

While the program is running on top of the FPVM, it is considered to be in the client role, while the VM is in the host role. The only way for the client and host to communicate with one another is synchronously through the Preimage ABI (specification).

In order for the client to read from the host, the read and write syscalls are modified within the FPVM to allow the client to request preparation of and read foreign data.

Reading

When the client wants to read data from the host, it must first send a "hint" to the host through the hint file descriptor, which signals a request for the host to prepare the data for reading. The host will then prepare the data, and send a hint acknowledgement back to the client. The client can then read the data from the host through the designated file descriptor.

The preparation step ("hinting") is an optimization that allows the host to know ahead of time the intents of the client and the data it requires for execution. This can allow for lazy loading of data, and also prevent the need for unnecessary allocations within the host's memory. This step is a no-op on-chain, and is only ran locally when the host is the native implementation of the FPVM.

sequenceDiagram
    Client->>+Host: Hint preimage (no-op on-chain / read-only mode)
    Host-->>Host: Prepare Preimage
    Host-->>-Client: Hint acknowledgement
    Client-->>+Host: Preimage Request
    Host-->>-Client: Preimage Data

Full Example

Below, we have a full architecture diagram of the op-program (source: fault proof specs), the reference implementation for the OP Stack's Fault Proof Program, which has the objective of verifying claims about the state of an OP Stack layer two.

op-program-architecture

In this program, execution and derivation of the L2 chain is performed within it, and ultimately the claimed state of the L2 chain is verified in the prologue stage.

It communicates with the host for two reasons:

To request preparation of L1 and L2 state data preimages.
To read the L1 and L2 state data preimages that were prepared after the above requests.

The host is responsible for:

Preparing and maintaining a store of the L1 and L2 state data preimages, as well as localized bootstrap k/v pairs.
Providing the L1 and L2 state data preimages to the client for reading.

Other programs (clients) may have different requirements for communication with the host, but the above is a common pattern for programs built on top of a FPVMs. In general:

The client program is a state machine that is responsible for bootstrapping itself from the inputs, executing the progam logic, and verifying the outcome.
The host is responsible for providing the client with data it wasn't bootstrapped with, and for executing the program itself.

Supported Targets

Kona seeks to support all FPVM targets that LLVM and rustc can offer introductory support for. Below is a matrix of features that Kona offers for each FPVM target:

Target	Build Pipeline	IO	malloc	Program Stages
`cannon` & `cannon-rs`	✅	✅	✅	❌
`asterisc`	✅	✅	✅	❌

If there is a feature that you would like to see supported, please open an issue or consider contributing!

Cannon (MIPS32r2)

Cannon is based off of the mips32r2 target architecture, supporting 55 instructions:

Category	Instruction	Description
`Arithmetic`	`addi`	Add immediate (with sign-extension).
`Arithmetic`	`addiu`	Add immediate unsigned (no overflow).
`Arithmetic`	`addu`	Add unsigned (no overflow).
`Logical`	`and`	Bitwise AND.
`Logical`	`andi`	Bitwise AND immediate.
`Branch`	`b`	Unconditional branch.
`Conditional Branch`	`beq`	Branch on equal.
`Conditional Branch`	`beqz`	Branch if equal to zero.
`Conditional Branch`	`bgez`	Branch on greater than or equal to zero.
`Conditional Branch`	`bgtz`	Branch on greater than zero.
`Conditional Branch`	`blez`	Branch on less than or equal to zero.
`Conditional Branch`	`bltz`	Branch on less than zero.
`Conditional Branch`	`bne`	Branch on not equal.
`Conditional Branch`	`bnez`	Branch if not equal to zero.
`Logical`	`clz`	Count leading zeros.
`Arithmetic`	`divu`	Divide unsigned.
`Unconditional Jump`	`j`	Jump.
`Unconditional Jump`	`jal`	Jump and link.
`Unconditional Jump`	`jalr`	Jump and link register.
`Unconditional Jump`	`jr`	Jump register.
`Data Transfer`	`lb`	Load byte.
`Data Transfer`	`lbu`	Load byte unsigned.
`Data Transfer`	`lui`	Load upper immediate.
`Data Transfer`	`lw`	Load word.
`Data Transfer`	`lwr`	Load word right.
`Data Transfer`	`mfhi`	Move from HI register.
`Data Transfer`	`mflo`	Move from LO register.
`Data Transfer`	`move`	Move between registers.
`Data Transfer`	`movn`	Move conditional on not zero.
`Data Transfer`	`movz`	Move conditional on zero.
`Data Transfer`	`mtlo`	Move to LO register.
`Arithmetic`	`mul`	Multiply (to produce a word result).
`Arithmetic`	`multu`	Multiply unsigned.
`Arithmetic`	`negu`	Negate unsigned.
`No Op`	`nop`	No operation.
`Logical`	`not`	Bitwise NOT (pseudo-instruction in MIPS).
`Logical`	`or`	Bitwise OR.
`Logical`	`ori`	Bitwise OR immediate.
`Data Transfer`	`sb`	Store byte.
`Logical`	`sll`	Shift left logical.
`Logical`	`sllv`	Shift left logical variable.
`Comparison`	`slt`	Set on less than (signed).
`Comparison`	`slti`	Set on less than immediate.
`Comparison`	`sltiu`	Set on less than immediate unsigned.
`Comparison`	`sltu`	Set on less than unsigned.
`Logical`	`sra`	Shift right arithmetic.
`Logical`	`srl`	Shift right logical.
`Logical`	`srlv`	Shift right logical variable.
`Arithmetic`	`subu`	Subtract unsigned.
`Data Transfer`	`sw`	Store word.
`Data Transfer`	`swr`	Store word right.
`Serialization`	`sync`	Synchronize shared memory.
`System Calls`	`syscall`	System call.
`Logical`	`xor`	Bitwise XOR.
`Logical`	`xori`	Bitwise XOR immediate.

Syscalls

$v0	system call	$a0	$a1	$a2	Effect
4090	mmap	uint32 addr	uint32 len	🚫	Allocates a page from the heap. See heap for details.
4045	brk	🚫	🚫	🚫	Returns a fixed address for the program break at `0x40000000`
4120	clone	🚫	🚫	🚫	Returns 1
4246	exit_group	uint8 exit_code	🚫	🚫	Sets the Exited and ExitCode states to `true` and `$a0` respectively.
4003	read	uint32 fd	char *buf	uint32 count	Similar behavior as Linux/MIPS with support for unaligned reads. See I/O for more details.
4004	write	uint32 fd	char *buf	uint32 count	Similar behavior as Linux/MIPS with support for unaligned writes. See I/O for more details.
4055	fcntl	uint32 fd	int32 cmd	🚫	Similar behavior as Linux/MIPS. Only the `F_GETFL` (3) cmd is supported. Sets errno to `0x16` for all other commands

For all of the above syscalls, an error is indicated by setting the return register ($v0) to 0xFFFFFFFF (-1) and errno ($a3) is set accordingly. The VM must not modify any register other than $v0 and $a3 during syscall handling. For unsupported syscalls, the VM must do nothing except to zero out the syscall return ($v0) and errno ($a3) registers.

Note that the above syscalls have identical syscall numbers and ABIs as Linux/MIPS.

Asterisc (RISC-V)

Asterisc is based off of the rv64gc target architecture, which defines the following extensions:

RV32I support - 32 bit base instruction set
- FENCE, ECALL, EBREAK are hardwired to implement a minimal subset of systemcalls of the linux kernel
  - Work in progress. All syscalls used by the Golang risc64 runtime.
RV64I support
RV64C: Compressed instructions
RV32M+RV64M: Multiplication support
RV32A+RV64A: Atomics support
RV{32,64}{D,F,Q}: no-op: No floating points support (since no IEEE754 determinism with rounding modes etc., nor worth the complexity)
Zifencei: FENCE.I no-op: No need for FENCE.I
Zicsr: no-op: some support for Control-and-status registers may come later though.
Ztso: no-op: no need for Total Store Ordering
other: revert with error code on unrecognized instructions

asterisc supports a plethora of syscalls, documented in the repository. kona offers an interface for programs to directly invoke a select few syscalls:

EXIT - Terminate the process with the provided exit code.
WRITE - Write the passed buffer to the passed file descriptor.
READ - Read the specified number of bytes from the passed file descriptor.

Prologue

The prologue stage of the program is commonly responsible for bootstrapping the program with inputs from an external source, pulled in through the Host <-> Client communication implementation.

As a rule of thumb, the prologue implementation should be kept minimal, and should not do much more than establish the inputs for the execution phase.

Example

As an example, the prologue stage of the kona-client program runs through several steps:

Pull in the boot information over the Preimage Oracle ABI, containing:
- The L1 head hash containing all data required to reproduce the L2 safe chain at the claimed block height.
- The latest finalized L2 output root.
- The L2 output root claim.
- The block number of the L2 output root claim.
- The L2 chain ID.
Pull in the RollupConfig and L2ChainConfig corresponding to the passed L2 chain ID.
Validate these values.
Pass the boot information to the execution phase.

Execution

The execution phase of the program is commonly the heaviest portion of the fault proof program, where the computation that is being verified is performed.

This phase consumes the outputs of the prologue phase, and performs the bulk of the verifiable computation. After execution has concluded, the outputs are passed along to the epilogue phase for final verification.

Example

At a high-level, in the kona-client program, the execution phase:

Derives the inputs to the L2 derivation pipeline by unrolling the L1 head hash fetched in the epilogue.
Passes the inputs to the L2 derivation pipeline, producing the L2 execution payloads required to reproduce the L2 safe chain at the claimed height.
Executes the payloads produced by the L2 derivation pipeline, producing the L2 output root at the L2 claim height.

Epilogue

The epilogue stage of the program is intended to perform the final validation on the outputs from the execution phase. In most programs, this entails comparing the outputs of the execution phase to portions of the bootstrap data made available during the prologue phase.

Generally, this phase should consist almost entirely of validation steps.

Example

In the kona-client program, the prologue phase only contains two directives:

Validate that the L2 safe chain could be produced at the claimed L2 block height.
The constructed output root is equivalent to the claimed L2 output root.

Glossary

This document contains definitions for terms used throughout the Kona book.

Fault Proof VM

A Fault Proof VM is a virtual machine, commonly supporting a subset of the Linux kernel's syscalls and a modified subset of an existing reduced instruction set architecture, that is designed to execute verifiable programs.

Full specification for the cannon & cannon-rs FPVMs, as an example, is available in the Optimism Monorepo.

Fault Proof Program

A Fault Proof Program is a program, commonly written in a general purpose language such as Golang, C, or Rust, that may be compiled down to a compatible Fault Proof VM target and provably executed on that target VM.

Examples of Fault Proof Programs include the OP Program, which runs on top of cannon, cannon-rs, and asterisc to verify a claim about the state of an OP Stack layer two.

Preimage ABI

The Preimage ABI is a specification for a synchronous communication protocol between a client and a host that is used to request and read data from the host's datastore. Full specifications for the Preimage ABI are available in the Optimism Monorepo.

Contributing

Thank you for wanting to contribute! Before contributing to this repository, please read through this document and discuss the change you wish to make via issue or in the development telegram.

Dependencies

Before working with this repository locally, you'll need to install several dependencies:

Docker for cross-compilation.
just for our command-runner scripts.
The Rust toolchain
The Golang toolchain

Optional

mdbook to contribute to the book
- mdbook-template
- mdbook-mermaid

Pull Request Process

Before anything, create an issue to discuss the change you're wanting to make, if it is significant or changes functionality. Feel free to skip this step for trivial changes.
Once your change is implemented, ensure that all checks are passing before creating a PR. The full CI pipeline can be ran locally via the justfiles in the repository.
Make sure to update any documentation that has gone stale as a result of the change, in the README files, the [book][book], and in rustdoc comments.
Once you have sign-off from a maintainer, you may merge your pull request yourself if you have permissions to do so. If not, the maintainer who approves your pull request will add it to the merge queue.

The Kona Book