Skip to content

Commit

Permalink
specs: de-dup Cannon docs
Browse files Browse the repository at this point in the history
  • Loading branch information
Inphi committed Jul 20, 2023
1 parent 9ec0f1c commit 61b995b
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 41 deletions.
43 changes: 4 additions & 39 deletions cannon/docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,48 +44,17 @@ There are 3 types of witness data involved in onchain execution:

### Packed State

The following state is packed together, and provided in every executed onchain instruction:
```solidity
struct State {
bytes32 memRoot;
bytes32 preimageKey;
uint32 preimageOffset;
uint32 pc;
uint32 nextPC;
uint32 lo;
uint32 hi;
uint32 heap;
uint8 exitCode;
bool exited;
uint64 step;
uint32[32] registers;
}
```
The Packed State is provided in every executed onchain instruction.
See [Cannon VM Specs](../../specs/cannon-fault-proof-vm.md#state) for
details on the state structure.

The packed state is small! The `State` data can be packed in such a small amount of EVM words,
that it is more efficient to fully provide it, than to create a proof for each individual part involved in execution.

The memory is represented as a merkle-tree root, committing to a binary merkle tree of all memory data,
see [memory proofs](#memory-proofs).

The `State` covers all general purpose registers, as well as the `lo`, `hi` and `pc` values.

`nextPC` helps pre-schedule the program counter change, to emulate delay-slot behavior of MIPS
after branch and jump instructions.

The program stops changing the state when `exited` is set to true. The exit-code is remembered,
to determine if the program is successful, or panicked/exited in some unexpected way.
This outcome can be used to determine truthiness of claims that are verified as part of the program execution.

The `heap` value is a special value, used to emulate a growing heap, to map new memory upon `mmap` calls by the program.
No memory reads/writes are actually illegal however, mmap-ing is purely to satisfy program runtimes that
need the memory-pointer result of the syscall to locate free memory.

The `preimageKey` and `preimageOffset` are backing the in-flight communication of [pre-image data](#pre-image-data).

The VM `stateHash` is computed as `keccak256(encoded_packed_state)`,
where `encoded_packed_state` is the concatenation of all state-values (all `uint` values are big-endian).


### Memory proofs

Expand Down Expand Up @@ -133,11 +102,7 @@ Pre-image data is accessed through syscalls exclusively.
The OP-stack fault-proof [Pre-image Oracle specs](../../specs/fault-proof.md#pre-image-oracle)
define the ABI for communicating pre-images.

This ABI is implemented by the VM by intercepting the `read`/`write` syscalls to specific file descriptors:
- `hint client read = 3`: used by the client to send hint data to the host. Optional, implemented as blocking.
- `hint client write = 4`: used by the client to wait for the host. Always instant, since the above is implemented as blocking.
- `preimage client read = 5`: used by the client to read pre-image data, starting from the latest pre-image reading offset.
- `preimage client write = 6`: used by the client to change the pre-image key. The key may change a little bit at a time. The last 32 written bytes count as key for retrieval when reading the pre-image. Changing the key also resets the read offset to 0.
This ABI is implemented by the VM by intercepting the `read`/`write` syscalls to specific file descriptors. See [Cannon VM Specs](../../specs/cannon-fault-proof-vm.md#io) for more details.

The data is loaded into `PreimageOracle.sol` using the respective loading function based on the pre-image type.
And then retrieved during execution of the `read` syscall.
Expand Down
6 changes: 4 additions & 2 deletions specs/cannon-fault-proof-vm.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,9 @@ location as the entire address space is unprotected.
### Heap

FPVM state contains a `heap` that tracks the base address of the most recent memory allocation.
Heap pages are bump allocated at the page boundary, per `mmap` syscall. The page size is 4096.
Heap pages are bump allocated at the page boundary, per `mmap` syscall.
mmap-ing is purely to satisfy program runtimes that need the memory-pointer
result of the syscall to locate free memory. The page size is 4096.

The FPVM has a fixed program break at `0x40000000`. However, the FPVM is permitted to extend the
heap beyond this limit via mmap syscalls.
Expand Down Expand Up @@ -106,7 +108,7 @@ The following table list summarizes the supported syscalls and their behaviors.
| 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 change the value of registers other than `$v0` and `$a3` during syscall handling.
`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.

Expand Down

0 comments on commit 61b995b

Please sign in to comment.