This is the original whitepaper for the Cartesi project published in 2018.
While much of the technological underpinning and software architecture describedin the whitepaper still holds true for the project to this day, the Cartesi technology
in its current state is the product of years of research, development, andcontributions by a growing and decentralized community of independent teams,
companies, and individuals.
For regular updates on the Cartesi ecosystem, visit the Cartesi Blog.

Version 1.01

The Core of Cartesi
Augusto Teixeira

Diego Nehab

Abstractof critical importance to all parties and therefore require global consensus. Otherwise, for most interactions mediated by the blockchain,
it is perfectly safe to limit access and verification responsibility to
the few parties that can potentially be affected. The blockchain canthen be used to provide finality and to guarantee local consensus in
the rare occasions where a dispute arises between these parties. In
other words, global consensus is a precious resource that should be
used with parsimony. In recognition of this fact, layer-2 scalability
solutions such as plasma, side chains, TrueBit, or state channels
move as much data and computation as possible off-chain. Layer-1
and 2 scalability solutions are discussed at some depth in section 2.

Cartesi is a layer-2 platform for the development and deployment of
scalable decentralized applications. Cartesi DApps are composed ofboth blockchain and off-chain components. Off-chain components
run inside Cartesi Nodes that represent the interests of each DApp
user. Cartesi Nodes provide DApp developers with reproducible
Cartesi Machines, where large scale verifiable computations canbe run. These verifiable computations are easily integrated into
smart contracts by powerful primitives that provide strong conflictresolution guarantees. More precisely, any dispute arising over the
result of computations run inside Cartesi Machines can be fairly
adjudicated at negligible cost on the blockchain. Cartesi Nodes also
allow DApp developers to run native code. Native computations canleverage the node’s full processing power, including any available
GPUs. Whether performed natively by the node or inside Cartesi
Machines, off-chain components run under a complete Linux operating system that provides the full ecosystem required by complex
computations. Cartesi enables DApp developers to use all the programming languages, tools, libraries, software, and services they
are already familiar with. By moving most of the complex logic of
their DApps to portable off-chain components, developers are freed
from the limitations and idiosyncrasies imposed by blockchains. In
this way, Cartesi empowers developers to select the best run-timeenvironment in which to host each part of their DApps.

1

Every computation that can influencea transaction, whether performed on-chain or off-chain, must be reproducible by all parties playing a validating role. Reproducible
computational models must be self-contained and deterministic. In
other words, the complete state for the computation and the entire
sequence of modifications to this state must be fully specified andagreed upon. Sadly, real computing architectures were not designedwith these constraints in mind, and therefore are not reproducible.
Blockchain platforms solve this problem by employing custom virtual machines (VMs) when processing smart contracts. These VMs
are reproducible, but also domain specific. On the one hand, they
offer native support for features useful to smart contracts (e.g., accounting, rollback, associative memory, authentication, cryptography etc). On the other hand, they lack valuable features found ingeneral-purpose architectures (e.g., floating-point arithmetic, virtual
memory, interrupts etc).
Computation environment

Introduction

Public blockchains are mechanisms through which networks canmaintain decentralized consensus over a shared state. Typically, thisstate holds, among other data, a payment system. The stake held byparticipants in the resulting economy works as their incentive formaking the state widely available to others and for rejecting invalidtransactions. In this virtuous cycle, the payment system is built on
top of the decentralized consensus, which only functions due toincentives created by the payment system itself. Both the payment
system and the consensus can then be used for other purposes.

The revolution in software capability the world experienced overthe last few decades can be attributed to two key factors. The firstis an exponential increase in the speed at which modern hardware
platforms can process vast amounts of data. The second, and equallyimportant, is the ever-increasing expressive power of software development environments. Indeed, general-purpose computations do nothappen in isolation. Rather, they are assembled from inter-dependentbuilding-blocks created by a worldwide collaboration of softwaredevelopers. These components and services rely on standard-libraryfacilities hosted by an underlying operating system (memory management, process management, file systems, networking, etc). It is
the operating system that ties everything together. Such facilities
are not available from the free-standing programming languages andcompilers that typical blockchains offer to smart contract developers.

As new applications for blockchain technology are envisioned, thedemands on the underlying infrastructure are constantly increasing.
At the moment, the two major obstacles to widespread adoption ofblockchain technology are its poor scalability and lack of a solid
development environment. The main contribution of Cartesi to theblockchain ecosystem is overcoming both these issues.

Reproducibility and scalability concerns have made on-chain computation environments very restrictive. To boost productivity andwiden the scope of blockchain development, we need a reproducible
computation model that supports modern operating systems.

Currently deployed consensus mechanisms are basedon full redundancy [Nakamoto 2009; Wood 2018]. They require
every transaction to be stored permanently and to be validated byevery participant. This inefficiency is the key limiting factor to thegrowth of the transaction rate, the amount of data involved, and theintensity of computations within transactions. High transaction costs
and increased latency have become a barrier to many innovative
applications that would otherwise benefit from the flexibility thatsmart contracts bring to the blockchain.
Scalability

CartesiThis paper describes Cartesi, a layer-2 platform for the development and deployment of scalable decentralized applications. Cartesi
DApps are hybrid, i.e., they include both blockchain and off-chain
components.

Attempts to improve blockchain scalability can be divided intolayer 1 and layer 2 solutions. Layer 1 scalability solutions change
the underlying blockchain infrastructure itself. Examples include
the optimization of block sizes, sharding, and Delegated Proof of
Stake (DPoS). Because they operate at the infrastructure level, thesesolutions are burdened by the requirement of preserving global consensus. Certain aspects of the state, such as the payment system, are

The off-chain component runs in a network of Cartesi Nodes (section 6), each representing the interests of a DApp user. The off-chain
component is further divided into two modalities. Native computations run directly in the host hardware. Although native computations have access to the node’s full processing power (includingGPUs), the computations are not reproducible, at least not a pri-1Version 1.01
ori. Reproducible computations run instead inside Cartesi Machinesthat are controlled by the Cartesi Node. These are general, fully
self-contained Linux systems, that run on a deterministic RISC-V
architecture (section 3). Nodes interact with Cartesi Machines bymeans of a well-defined host interface (section 4).

applications access to the tools, libraries, services, and software they
are already familiar with, Cartesi chose to support Linux. A realistic
ISA, such as RISC-V, is much better suited for this purpose.
One of the differences of greatest consequence is in how Cartesialigns the interest in off-chain computations with the responsibility
for their execution. In TrueBit, there is no such alignment. A smart
contract posts the computation to a pool of untrusted parties andwaits for one of them to perform it off-chain and post the result
back. In this sense, TrueBit can be seen as a means for increasing
the computational power of individual smart contracts. Cheating isprevented with a complex incentive layer that rewards pool members
for successively disputing incorrect results. To keep the members
engaged, computations with incorrect results must be artificiallyinjected by the incentive layer. This inefficiency is a fundamental
part of the design of TrueBit. Conversely, Cartesi can be seen as away for off-chain computations to be endorsed by a smart contract.
All parties that could be affected by this endorsement are responsible
for performing the computation off-chain and, if needed, startinga dispute. Although the ensuing verification can be outsourced toa dispute resolution market (see section 6.2), there is no built-in
inefficiency and no need for an incentive layer.

Within the blockchain, a Cartesi DApp can specify reproducible offchain computations to be performed over large amounts of off-chain
data (section 5). Cartesi Nodes can automatically follow these specifications to perform the computations off-chain. DApp developers
can instruct the nodes to submit results or verify and dispute results
submitted by others. From the blockchain’s perspective, undisputed
computations take negligible resources. Even in case of disputes, thesettlement cost is only the logarithm of the storage and time required
during the computation. Off-chain, Cartesi Nodes never experience
more than twice the space and time required by the computation. In
this way, Cartesi virtually eliminates the gap in storage and computation power between smart contracts and traditional computer
programs.
Moving computations off-chain brings several advantages beyond
scalability. Cartesi Machines enable DApp developers to use all the
programming languages, tools, libraries, software, and services they
are already familiar with. Moreover, the way in which computations
are formulated is agnostic to the underlying blockchain. By isolating
all the complex smart-contract logic into reproducible off-chain computations, developers can make their DApps more portable acrossdifferent blockchains.

The large storage requirements of real-world computations pose asignificant challenge that TrueBit does not address. Explicit representations of code and data do not fit within the blockchain. Instead,a Cartesi Machine, together with its code and data, are represented
on-chain by a hash of its state. This arrangement allows for complex
transactions built from several rounds of off-chain computations to
be fully specified. The states themselves are only ever known explicitly off-chain, by interested parties. Some applications can facedata availability issues to which Cartesi offers a range of original
solutions [Teixeira and Nehab 2019a].

The focus of this document is the core of Cartesi. It includes thefull specification for the Cartesi Machine, the host interface for controlling it, the blockchain interface for specifying complex off-chain
computations, and the Cartesi Node interface for performing andverifying these computations. Higher-level tools, interfaces, and avariety of use cases built on top of this core functionality will be described in a future document [Teixeira and Nehab 2019a]. Detailed
documentation on all interfaces, as well as the development environment for Cartesi Nodes and Cartesi Machines will be available fromthe Cartesi SDK [Teixeira and Nehab 2019b].

2

Finally, Cartesi is committed to making off-chain computations
portable across different blockchain platforms.

2.1

Other related technologies

New blockchain technologies emerge at such a high rate that any
attempt at a comprehensive survey is doomed to become obsolete
before it is even published. Nevertheless, some general trends merit
discussion. Specific examples cited in the discussion should be seen
as representatives of entire categories, rather than exhaustive lists.

Related work

The work most closely related to Cartesi is TrueBit [Teutsch andReitwießner 2017]. The connection between Cartesi and Truebit
comes from the fact that both technologies move intensive computations off-chain and then, within the blockchain, use a verification
game [Feige and Kilian 1997] to efficiently settle disputes regarding
the results of these computations. Despite this similarity, many otherdesign decisions set these two technologies apart.

The scalability trilemma put forth
by Buterin [2018a] poses that no simple workaround can improvetransaction throughput without reducing the decentralization or security of a blockchain. On the one hand, requiring higher throughput
from nodes raises their operating cost, which centralizes power inthe hands of the few players that can afford them. On the other,fragmenting consensus into independent chains makes each of themmore vulnerable to 51% attacks.
Layer-1 scalability solutions

TrueBit is based on WebAssembly [2018], a VM ISA designed by
a W3C Community Group to support efficient web applications.1
In contrast, Cartesi is based on RISC-V [Waterman and Asanović
2017a,b], an open ISA designed in UC Berkley for implementation
by native hardware. The WebAssembly and RISC-V ISAs are ofsimilar complexity. The key difference is their position in relation toapplications and the operating system. WebAssembly was designed
to sit between applications and the underlying operating system.
RISC-V is instead meant to sit under the operating system and theapplications it supports. TrueBit’s choice is consistent with a focus
on extending the computational power of smart contracts, which
tend to operate under severely restricted environments. Real-world
applications, however, cannot exist in isolation. They depend onrich, complex run-time environments that are invariably built on topof a modern operating system. To give developers of decentralized

The two leading proposals for breaking the trillema are refinementsof these two ideas. Delegated Proof of Stake (e.g., Larimer [2017])
requires a small number of powerful nodes to validate every single
transaction. However, these nodes are democratically elected by allparties that hold a stake in the blockchain. The alternative proposal
is to split the state and history into multiple shards that are verified
independently [Buterin 2018b]. These shards are then connected toa main chain in a way that reduces the odds of successful attacks.
Both ideas are expected to significantly improve the throughput oftransactions processed by the blockchain. They must neverthelessachieve universal consensus among nodes on each transaction. This
imposes a super-linear global cost as computation sizes grow.

1 It was originally based on the LLVM back-end for an obscure Myricom

NIC embedded processor design used internally at Google.

2

Version 1.01
Cartesi, on the other hand, is designed to achieve local (instead of
universal) consensus over its computations. More precisely, only
affected parties are required to perform the computation, while
any possible dispute among them can be resolved in logarithmic
time. This design allows for intensive computations to be performed
off-chain only by the impacted participants, who still enjoy strong
conflict resolution guarantees.

very different from Cartesi’s. Future applications may wish to combine both technologies by running part of their native computations
inside hardware enclaves within Cartesi Nodes, or by running anentire Cartesi Node inside a hardware enclave.
Another approach to enable private andscalable computations on the blockchain is to use general purposezero-knowledge proof systems such as zk-SNARKS [Blum et al.
1988; Bitansky et al. 2012] or zk-STARKS [Ben-Sasson et al. 2018].
These systems achieve verifications in a fast, non-interactive andprivate manner. However, the computations that can be specified
within these models are very restrictive as they are derived fromarithmetic circuits without control flow. Therefore, they are notTuring complete and cannot run arbitrary code.
Zero knowledge proofs

In this way, DPoS and sharding are orthogonal to Cartesi. Cartesi
benefits from the faster and cheaper transactions provided by theunderlying infrastructure. Conversely, the blockchain benefits from
Cartesi’s ability to specify and adjudicate large-scale realistic computations.
Various solutions have been proposed on the second layer to increase blockchain scalability in termsof transaction throughput, such as Plasma or State Channels. Thesedevelopments have particularities of their own, but are generally
designed to register large amounts of transactions off-chain, which
are only committed on-chain in order to reach finality or in the caseof a dispute. A common requirement of these solutions is that theblockchain should be able to resolve any dispute that may arise (after
a Plasma exit, or when a channel is closed). These exit mechanisms
impose strong limitation on the maximum transaction size that either
Plasma or State Channels can handle. So for example, if two parties
disagree on an off-chain transaction that requires a large computation to be completed, they would be unable to settle who is correct
on the main chain.
Layer-2 scalability solutions

In off-chain environments, this technology is reaching maturity
through projects such as Pinocchio [Parno et al. 2013] and libsnark [Ben-Sasson et al. 2013]. Meanwhile, zero-knowledge proofs
have first appeared in blockchain technology with privacy coins,where shielded addresses protect the identities of parties involvedin a transaction [Miers et al. 2013; van Saberhangen 2013]. In the
Metropolis (Byzantium) fork, Ethereum introduced zk-SNARKS
primitives into its virtual machine and some libraries have alreadystarted to be developed [Schaeffer 2018]. In this context, Cartesi
can accelerate this development by bringing more mature off-chain
implementations of zk-SNARKS, such as Pinocchio or libsnark,
directly into the blockchain.

Cartesi can greatly improve these technologies, as it allows both a
Plasma chain or a State Channel to specify full Cartesi computations
within its transactions. And in case a dispute lifts the computation
to the main chain, the settlement can still be efficiently and safely
resolved.

Besides the scalability solutions mentioned above, several projects try to provide different
languages for developers to write smart contracts in, such as Vyper,
LLL, Bamboo, etc. Although these projects provide a welcome setof languages and tools for the development of smart contracts, they
do not fully alleviate the most fundamental restrictions that currently
hamper blockchain development. The main reason being that allthese languages run on a free standing environment and therefore
they do not offer the advantages that come with Cartesi’s underlying
operating system, as described in section 3 below.
Compilers and Virtual Machines

Several projects intend to bring large scale
and flexible computations to the blockchain by relying on a systemof redundancy, reputation, and verification (e.g., SONM [2018],
Golem [2016], and iExec [2017]). Although all these systems havedifferent designs, the main idea is that computations are sent to apool of off-chain providers, who submit their results independently.
If someone challenges the presented results, a randomly assigned
verifier decides on the correct outcome.
Reputation solutions

3

Cartesi Machine specification

The Cartesi Machine is a self-contained and deterministic computational model that can host modern operating systems. Real-world
computations happen inside operating systems for good reasons.
Developers are trained to use toolchains that operate at the highest
possible abstraction level for any given job. These toolchains isolatethem from irrelevant hardware details and even from the particulars
of a given operating system. Inventing an ad-hoc new architecture
would then require the porting of a toolchain and operating system. Instead, Cartesi Machines are based on a proven architecture
for which a standard toolchain and operating system are alreadyavailable.

Although these systems have a built-in reputation mechanism todiscourage misbehavior, it is not yet clear whether they are resistant
to collusions or bribing in case the outcome of a computation canhave financial consequences. Cartesi gives instead mathematicalguarantees on its dispute resolutions.
Several projects are integrating
enclaves (e.g., Intel’s SGX, ARM’s TrustZone, or AMD’s SEV) withthe blockchain [TEEX 2018; Song et al. 2018; Enigma 2018; Chenget al. 2018]. In a nutshell, enclaves are hardware-supported featuresthat allow user-level code to create an execution environment whose
privacy and integrity is protected even from processes running at
higher privilege levels.
Trusted execution environment

On the other hand, off-chain computations performed by Cartesi
Machines must be verifiable by a blockchain. The blockchain must
therefore host a reference implementation of the entire architecture. If it is ever to be trusted, this implementation must be easily
auditable. To that end, both the architecture and the implementation must be open and relatively simple. Together, these requirements point to RISC-V. The RISC-V ISA is based on a minimal
32-bit integer instruction set to which several extensions can be
added [Waterman and Asanović 2017a]. Orthogonally, operand andaddress-space widths can be extended to 64-bits (or even 128-bits).
Additionally, the standard defines a privileged architecture [Waterman and Asanović 2017b] with features commonly used by modern
operating systems, such as multiple privilege levels, paged-based

Computations running inside enclaves are not, a priori, reproducible.
Using remote attestation in lieu of verification is equivalent to trusting the hardware manufacturer. Whether this level of centralization
is justifiable or not depends on the application at hand, the manufacturer’s competence, and on the potential for conflicts of interest.
Even setting these issues aside, privacy is not always guaranteed,as recent attacks show [Weichbrodt et al. 2016; Brasser et al. 2017;
Moghimi et al. 2017; Lee et al. 2017].
Enclaves may yet play an important role in the future of blockchain
technology. However, their threat model and security guarantees are3

Version 1.01
Table 1: Instruction counts by extension. Entries in the form x + yrefer to 32- and 64-bit variants of the same facility.
Integer

Mul/Div

Atomics

Privileged

Total

47+12

8+5

11+11

5

71+28=99

Figure 1: The iflags register gives the current privilege level,and specifies whether the machine is temporarily idle waiting forinterrupts, or has been permanently halted.

Table 2: The processor state. Memory-mapped to the lowest 512
bytes in physical memory for external read-only access.
OffsetState

Offset

State

0x000
0x008
···
0x0f8
0x100
0x108
0x110
0x118
0x120
0x128
0x130
0x138
0x140
0x148
0x150
0x158

x0
x1
···
x31
pc
mvendorid
marchid
mimplidmcycleminstret
mstatusmtvec
mscratchmepc
mcause
mtval

0x160
0x168
0x170
0x178
0x180
0x188
0x190
0x198
0x1a0
0x1a8
0x1b0
0x1b8
0x1c0
0x1c8
0x1d0

misa
mie
mip
medeleg
midelegmcounteren
stvec
sscratchsepc
scausestval
satp
scounteren
ilrsc†
iflags††protection. Sv48 provides a 48-bit protected virtual address space,
divided into 4KiB pages, organized by a four-level page table. Thisset of features creates a balanced compromise between the simplicity demanded by a blockchain implementation and the flexibility
expected from off-chain computations.
There are a total of 99 instructions, out of which 28 simply narrowor widen, respectively, their 64-bit or 32-bit counterparts. Table 1
breaks down the instruction count for each extension. This being a
RISC ISA, most instructions are very simple and can be simulated ina few lines of high-level code.2 In fact, the only complex operationis the virtual-to-physical address translation. Instruction decoding isparticularly simple due to the reduced number of formats (only 4,
all taking 32-bits).
The entire processor state fits within 512 bytes, which are divided
into 64 registers, each one holding 64-bits. Most of these registers
are defined by the RISC-V ISA, and consist of 32 general-purpose
integer registers and 26 control and status registers. The remaining
are Cartesi-specific. The processor makes its entire state available,
externally and read-only, by mapping individual registers to thelowest 512 bytes in physical memory. The adjacent 1.5KiB are
reserved for future use. The entire mapping is given in table 2.

Cartesi-specific state.

virtual-memory, timers, interrupts, exceptions and traps, etc. Implementations are free to select the combination of extensions that
better suit their needs.

The registers whose names start with i are Cartesi-specific, andhave the following semantics. The layout for register iflags canbe seen in figure 1. PRV gives the current privilege level, I is set
to 1 when the processor is idle (i.e., waiting for interrupts), and H
is set to 1 to signal the processor has been permanently halted.
Register ilrsc holds the reservation address for the LR/SC atomic
memory operations.

RISC-V was born of research in academia at UC Berkeley. It is now
maintained by its own independent foundation. Larger corporations,
including Google, Samsung, and Tesla, have recently joined forces
with the project [Tilley 2018]. The platform is supported by a vibrantcommunity of developers. Their efforts have produced an extensive
software infrastructure, most notably ports of the Linux operating
system and the GNU toolchain [RISC-V 2018d]. It is important tokeep in mind that RISC-V is not a toy architecture. It is suitable fordirect native hardware implementation, which is indeed currently
commercialized by SiFive Inc. This means that, in the future, Cartesi
will not be limited to emulation or binary translation off-chain.

Default initialization fills the state with the following values:• PRV in iflags is set to 3 (for the Machine privilege level);• misa is set to RV64IMASU;• SXL and UXL in mstatus are set to 2 (for 64-bits);• pc starts at 0x1000 (pointing to ROM);• marchid is set to cartesi� in ASCII.
mvendorid is used to test for matching on-chain and off-chain
implementations. mimplid is incremented with each update to amatching pair. The remaining default state is set to zero.

The Cartesi Machine can be separated into a processor and a board.
The processor performs the computations, executing the traditional
fetch-execute loop while maintaining a variety of registers. The
board defines the surrounding environment with an assortment ofmemories (ROM, RAM, flash) and devices. To make verification
possible, Cartesi Machines map their entire state to physical memory in a well-defined way. This includes the internal states of theprocessor, the board, and of all attached devices. Fortunately, thismodification does not limit the operating system or the applications
it hosts in any significant way.

3.1

3.2

The board

The interaction between board and processor happens through devices mapped to the processor’s physical address space. Table 3
shows this mapping. There are 64KiB of ROM starting at address
0x1000, where execution starts. The central role of this ROM isholding the devicetree [DTSpec 2017] describing the system hardware. In addition, a bootstrap program at ROM-base sets register x10
to 0 (the value of mhartid), x11 to point to the devicetree, and thenjumps to RAM-base at 0x80000000. This is where the entry pointof the boot image is expected to reside. Finally, a number of additional physical memory ranges can be set aside for flash-memory
devices. These will typically be preloaded with file-system images.

The processor

Following RISC-V terminology, Cartesi Machines implement the
RV64IMASU ISA. The letters after RV specify the extension set.
This selection corresponds to a 64-bit machine, Integer arithmetic
with Multiplication and division, Atomic operations, as well as theoptional Supervisor and User privilege levels. In addition, Cartesi
Machines support the Sv48 mode of address translation and memory

2 The x86 ISA defines at least 2000 (potentially complex) instructions.

4Version 1.01
Table 3: Physical memory layout for a Cartesi Machine.

Figure 2: Physical Memory Attributes. The istart and ilengthof each range are aligned to a 4KiB boundary. The 12 LSBs of each64-bit word give attributes for the range.
Two non-memory devices are mapped to the address space. The
Core Local Interruptor (or CLINT) controls the timer interrupt. The
active addresses are 0x0200bff8 and 0x02004000, respectively
mapped to registers mtime and mtimecmp. The CLINT issues ahardware interrupt whenever mtime equals mtimecmp. To ensure
reproducibility, the processor’s clock and the timer are locked by aconstant frequency divisor of 100. In other words, mtime is incremented once for every 100 increments of mcycle. The Host-Target
Interface (HTIF) mediates communication with the external world.
Its active addresses are 0x40000000 (tohost) and 0x40000008(fromhost). It halts the machine when tohost is written to withbits 63–48 set to 0 and bit 0 set to 1. (Bits 47–1 can be set to anarbitrary exit code.) It also works as a rudimentary communications
port during interactive sections.

Processor shadow
Board shadow
ROM (Bootstrap & Devicetree)
Core Local Interruptor
Host-Target Interface
RAM
Flash 0 (Disk 0)···
Flash 7 (Disk 7)

The only salient Cartesi-specific modification pertains to the haltingof the machine. When field H in iflags is set to 1, no further statetransitions are allowed. The condition is set explicitly when HTIF is
instructed to halt the machine.

3.4

The Linux port

Setting up a Linux system from scratch involves a variety of steps.
Unlike stand-alone systems, embedded systems are not usually selfhosting. Instead, components are built in a separate host system,
on which a cross-compiling toolchain for the target architecture
has been installed. The key components are the GNU Compiler
Collection and the GNU C Library. This infrastructure can be foundin the RISC-V GNU toolchain repository [RISC-V 2018a]. Building
this infrastructure is the first step.
The toolchain can then be used to cross-compile the Linux kernel.
Kernel sources can be found in the RISC-V Linux repository [RISCV 2018b]. The kernel runs in supervisor mode, on top of a Supervisor
Binary Interface (SBI) provided by a machine-mode shim: the Berkeley Boot Loader (BBL). BBL can be found in the RISC-V Proxy
Kernel repository [RISC-V 2018e]. The BBL is linked against theLinux kernel and this resulting boot image is preloaded into RAM.
The SBI provides a simple interface through which the kernel interacts with CLINT and HTIF. Besides implementing the SBI, the BBL
also installs a trap that catches invalid instruction exceptions. Thismechanism can be used to emulate floating-point instructions (Seesection 4.3). After installing the trap, BBL switches to supervisor
mode and cedes control to the kernel entry point.

The board supports a total of 32 PMAs, and makes them available,
read-only, starting at offset 2KiB in physical memory. Another 2KiB
are reserved for future use. PMA 0 describes RAM, and PMAs 16–
23 describe flash devices 0–7. These PMAs are user-configurable
during initialization and read-only thereafter. (The RAM istart
field is hard-coded to 0x80000000.) Together, these records boundthe maximum amount of storage accessible during computations.

The state transition function

A computation is a sequence of machine states s0 , s1 , . . . , sh , governed by a transition function step such thatsi+1 = step(si ).

Mapping

0x00000000–0x000003ff
0x00000800–0x00000Bff
0x00001000–0x00010fff
0x02000000–0x020bffff
0x40000000–0x40007fff
0x80000000–*
*–*
···
*–*

value of mcycle. (Note that, since the machine can be occasionallyidle, minstret does not track mcycle.)

The physical memory mapping is described by Physical Memory
Attribute records (PMAs). Each PMA consists of 2 64-bit words.
The first word gives the start of a range and the second word its
length. Since the ranges must be aligned to 4KiB page boundaries,
the lowest 12-bits of each word are available for attributes. Figure 2
shows the meaning of each attribute field. The M, IO, and E bits
are mutually exclusive, and respectively mark the range as memory,
I/O mapped, or excluded. Bits R, W, and X grant read, write, andexecute permissions, respectively. Finally, the IR and IW bits markthe range as idempotent for reads and writes, respectively.

3.3

Physical address

The final step is the creation of a root file-system. This process
starts with a skeleton directory in the host system containing a
few subdirectories (sbin, lib, var, etc) and text files (sbin/init,
etc/fstab, etc/passwd etc). Tiny versions of many common
UNIX utilities (ls, cd, rm, etc) can be combined into a single
binary [Vlasenko 2018]. Target executables often depend on sharedlibraries provided by the toolchain (lib/libm.so, lib/ld.so, andlib/libc.so). Naturally, these libraries must be copied to the root
file-system. Once the root directory is ready, it is copied into an
actual file-system image (e.g., using gene2fs).

(1)

Here, s0 is the initial state and sh is a halting state. The previous
sections described the state space and the transition function for
Cartesi Machines in great detail.
Recall the state consists of the value of each word in the entire 64-bit
address space of the Cartesi Machine. In practice, it takes vastly
fewer than 264 bytes to represent a state. Only regions described intable 3 must be defined explicitly. All remaining values are implicitly
filled with zeros.

These steps can be automated. Cartesi’s SDK makes a preconfigured
host environment available to developers in the convenient form of aDocker container. Complex Linux systems can be built with the helpof Sifive’s fork of Buildroot [Petazzoni 2018], or RISC-V’s port of
the Yocto project [RISC-V 2018c]. The environment in the container
enables developers to customize the boot image and the root filesystem according to the needs of their applications. Thousands ofpackages are available for installation.

The RISC-V ISA manuals [Waterman and Asanović 2017a,b] specify the state transitions corresponding to the execution of each instruction. This means that states are well defined between executed
instructions. Since all instructions can be implemented in O(1) time,
Cartesi defines each state transition to take exactly 1 cycle. The index
of a given state in the sequence can be read from the corresponding5

Version 1.01
memory@80000000 {device_type = "memory";
reg = <0x0 0x80000000 0x0 0x8000000>;};

m = machine{ram {ilength = 0x8000000,
backing = "boot-image.bin"},

flash@8000000000 {#address-cells = <0x2>;#size-cells = <0x2>;
compatible = "mtd-ram";bank-width = <0x4>;
reg = <0x80 0x0 0x0 0x4000000>;
fs0@0 {
label = "root";
reg = <0x0 0x0 0x0 0x4000000>;};};

rom = {
bootargs = "root=/dev/mtdblock0 rw",}

chosen {bootargs = "root=/dev/mtdblock0 rw";};}

Figure 4: The initialization of the off-chain machine automaticallygenerates the devicetree of figure 3.

Figure 3: Partial devicetree for a simple setup with 128MiB of RAM
and a 64MiB flash device to be mounted as the root file-system.

filled automatically or loaded from a backing file. Initialization
returns a machine handle that can be manipulated thereafter.

The root file-system image is installed as a flash device. Additional
flash devices can be used to store the inputs to the computation, orto receive its outputs. The devicetree in ROM is used to inform
Linux of the location of each flash device, the amount of RAM,and any kernel parameters. Figure 3 shows the relevant devicetreesnippet. The first section specifies 128MiB of RAM starting at the2GiB boundary. The middle section adds a 64MiB flash device,
starting at the 512GiB boundary. The mtd-ram driver exposes thedevice as /dev/mtdblock0 under Linux’s virtual file-system. The
last section, giving the kernel parameters bootargs, specifies thedevice to be mounted as root.

machine = machine{
processor = processor ,rom = rom ,ram = ram ,flash0 = drive ,...
flash7 = drive ,clint = clint ,htif = htif ,}processor ::= {x0 = word ,x1 = word ,...
pc = word} | {backing = path}

After completing its own initialization, the kernel eventually cedes
control to /sbin/init. In Cartesi DApps, this is typically a shell
script that invokes the appropriate sequence of commands for performing the desired computation. The kernel passes to /sbin/init
as command-line parameters all arguments after the separator �-�
in bootargs. These can be used to define additional parameters forthe computation to be performed. Upon completion, /sbin/init
uses HTIF to halt the machine with an optional exit code. Thiscan be used as part of the computation output. Arbitrarily complex
inputs, parameters, and outputs can be passed as flash devices.

4

rom ::= {bootargs = string} | {backing = path}

Cartesi Machines off-chain

ram ::= {ilength = word ,backing = path}drive ::= {istart = word ,ilength = word ,backing = path ,shared = bool ,label = string}
clint ::= {mtime = word ,mtimecmp = word
} | {backing = path}htif ::= {fromhost = word ,tohost = word
} | {backing = path}

Figure 4 shows a sample machine call for the devicetree in figure 3.

Off-chain implementations of Cartesi Machines serve two purposes.
Their main role is the execution of the computation itself. The secondary role is supporting the settlement of disputes over the resultsof computations. To provide these services, off-chain implementations of Cartesi Machines must expose a programmable interface.

4.1

flash0 = {label = "root",
istart = 0x8000000000,
ilength = 0x4000000,
backing = "root-file-system.bin",shared = true}

The machine runs until mcycle exceeds a limit value. The function then returns false if the machine is halted, or true otherwise.
bool = machine :run{limit = word }The machine can create a snapshot of its current state. This is alightweight operation. It causes subsequent calls to run to modify
the state under a copy-on-write policy. At a future time, a rollback
operation can restore the snapshot state. Restoring the state lifts
the copy-on-write policy. Consecutive calls to snapshot cause
the previously snapshot state to be committed to memory. Calls
to rollback without a previously snapshot state have no effect:

The scripting interface

The instantiation of a machine can only happen after the initialvalues for its entire physical address space have been defined. The
physical memory layout is parameterized by the total amount ofRAM, and by the starts and lengths of all flash devices. PMAs areautomatically initialized from these parameters. The initial contentsof RAM (e.g., with the boot image) and of the flash devices (e.g., theroot file system), are given by backing files. The backing files forflash devices can be shared, in which case modifications to physicalmemory are saved to the file mapped to the corresponding memory
location. Values that are not explicitly defined are default-initialized.
In particular, the devicetree and the bootstrap in ROM can be either

machine :snapshot()machine :rollback()

The machine provides read-only access to its memory contents. To
that end, invoking word(address) returns the value of a given
64-bit (aligned) word in the address space:word = machine :word{address = word }6

Version 1.01
To backup the contents of the memory range associated to any
component of the machine state, simply choose a file to store it:

facilities. It is distributed as a library and scriptable in the Lua
programming language according to the interface described above.
Backing files for RAM and file-system images take advantage ofthe host’s support for sparse files. Only non-zero blocks take disk
space. This enables the entire state of the machine to be specified
in a convenient and compact form. The snapshot and rollback
mechanism, as well as the shared attribute for backing files, arebuilt on top of the host’s support for virtual memory, using childprocesses and memory-mapped files with copy-on-write semantics.
This makes them at the same time very simple to implement andvery efficient.

bool = machine :backup{
processor = path ,rom = path ,ram = path ,flash0 = path ,...
flash7 = path ,clint = path ,htif = path ,}The machine exposes its entire state as a Merkle tree [Merkle 1979].
(For more on Merkle trees, see section 5.) It returns a proof that a target node belongs to the Merkle tree, given its address and depth:

The functionality for Merkle tree inspection requires additional
support. For storage efficiency, the Merkle tree is maintained in its
PATRICIA form [Morrison 1968]. For time efficiency, the tree is
updated only when needed, in a lazy fashion. Each PMA range hasa bitmap of dirty pages associated to it. Pages of physical memory
are marked dirty in the TLB whenever they are written to. When the
TLB entry for a dirty page is evicted, the corresponding bit is saved
to the bitmap. When the proof function is called, it first updates the
Merkle tree. The update proceeds bottom up, by visiting only thenodes that subtend the dirty pages. After the update, all bitmaps and
TLB entries are marked clean.

proof = machine :prove{address = word ,depth = word}
proof ::= {address = word ,depth = word ,root = hash ,siblings = {hash1 , ..., hashdepth },target = hash}For simplicity, the emulator follows a tight loop decoding and executing each instruction in turn. Other RISC-V emulators are based on
the same approach [Waterman and Lee 2011; Bellard 2017]. In the
future, the emulator will avoid repeated decoding of hot execution
traces [Tröger et al. 2011]. It is possible to translate these traces tothe host instruction set for even better performance [Bellard 2018].
However, the additional gains must be weighted against the reduced
portability and significantly increased complexity.

The entries used for the initialization of individual devices can also
be queried from their base address. The hash of the node at theaddress and depth is returned along with the entry. If the baseaddress does not correspond to any device, or if the range length
implied by the depth causes it to overlap with more than one device,
an error is reported:
slice = machine :slice{address = word ,depth = word}slice ::= {hash = hash ,type = string ,device = device}

device ::=processor
rom
ram
drive
clint
htif

4.3
|
|
|
|
|

Floating-point operations are prevalent off-chain (except, perhaps, inthe context of embedded devices). Therefore, programmers expect
them to be available. If Cartesi hopes to bring a sense of normalcy toblockchain development, it must support floating-point operations.
The difficulty is guaranteeing reproducibility.
Different floating-point implementations can disagree subtly whenostensibly performing the same operation on the same operands.
Some of these differences arise from laxities in the IEEE 754-1985
standard. Although many of these have been tightened in the 2008
revision, several details remain unspecified. These include, but
are not limited to, underflows, the sign of zero, operations involving infinity or NaNs, and the quantum for the rounding of certain
recommended operations (e.g., sin, log etc). Moreover, hardware
implementations often take performance shortcuts that violate thestandards they claim to adhere to. This leads to inconsistencies evenacross successive generations of the same architecture.

The step function advances the machine 1 cycle, logging every
single access to the state along the way. All accesses are 64-bitaligned. Each log entry specifies the operation (read or write),the address, and the word read or written. In addition, each entry
includes the proof produced by a corresponding call to proof for
the address prior to the access.
log = machine :step()log ::= {access1 , access2 , ..., accessk }These issues argue strongly against adding floating-point support toany verifiable computation model. Accordingly, most blockchains
wisely omit them entirely [Nakamoto 2009; Wood 2018; NEO’s VM
2017; Cardano’s VM 2017]. The only way to guarantee consensus is
to emulate floating-point operations with a consistent software layer
based on integer operations. Unlike floating-point operations, theseare portable across different architectures.

access ::= {operation = read | write,
read = word ,written = word ,proof = proof}

The importance of functions prove, slice, and step, and theconvenience of this interface will become clear in section 5.

4.2

Floating-point support

In the RISC-V ISA, floating-point support is defined by extensions
F and D (respectively for single- and double-precision). Together,
these extensions augment the ISA with 32 floating-point registers,
1 control-status register, 30 new instructions, and 1 new instruction
format. The specification adheres strictly to the IEEE 754-2008
standard [IEEE 2008]. Furthermore, it is limited to the required
arithmetic operations that are fully specified.

Reference implementation

Cartesi’s reference off-chain implementation is based on software
emulation. The emulator is written in C/C++ with POSIX dependencies restricted to the terminal, process, and memory-mapping7

Version 1.01
There are many options for adding floating-point support to Cartesi.
In the first two approaches, the ISA does not include the F or D
extensions. Therefore, they require no changes to the blockchain
and off-chain implementations.

his DApp. Charlie, however, trusts neither Alice nor Bob. Naturally,
Alice and Bob do not trust each other either.
Cartesi’s role is to support Charlie’s work. To that end, Cartesi offersa variety of primitives that Charlie uses to mediate the potentiallyadversarial interactions between Alice and Bob. Some primitives
require no interaction, and can be evaluated autonomously in theblockchain from their inputs. The interesting primitives, however,are those that, though completely defined by their inputs, can only
be evaluated off-chain. By construction, when using a Cartesi DApp,
Alice and Bob always agree on the inputs to such primitives. Without
loss of generality, Bob evaluates the primitive off-chain and submits
the result. Alice is then given the chance to accept or reject Bob’s
result. Undisputed results can be used by Charlie’s DApp for the
purpose of his choice. In case of rejection, Cartesi engages with
Alice and Bob in a dispute resolution protocol that arbitrates in favorof the party with just cause. This adjudication always completes
within a few interactions and at a negligible computational cost to
the blockchain. Cartesi automates most of this process in a way thatis extremely convenient to Charlie.

When a RISC-V machine
does not support floating-point instructions, it raises a machinelevel illegal-instruction exception whenever one is found. The idea
is to use an exception handler installed by BBL to emulate thecorresponding floating-point instruction using RISC-V integer instructions. This process is transparent to the supervisor and userlevels, which work as if the ISA supported floating-point operations
natively.
Emulation by RISC-V code: traps

Alternatively, the compiler can be instructed to target a RISC-V ISA that does not include
floating-point operations. It substitutes them with calls to emulation
routines it provides itself. The resulting binaries do not include
floating-point instructions at all. This method is more efficient thanusing traps because it avoids the exception and decoding overhead.
Emulation by RISC-V code: compiler

The most important of these primitives is the Cartesi Machine. Smartcontracts cannot afford to store the states for a Cartesi Machine
within the blockchain, let alone perform the implied computations.
After all, the costs in terms of processing power and storage capacity
would both be prohibitive. To solve these problems, Cartesi uses
cryptographic hashes to concisely represent machine states in theblockchain. From the blockchain’s perspective, a computation is
simply a pair of hashes corresponding to the initial and final states ofthe machine. The contents of the memory subtended by such hashes
are known only off-chain. Cartesi defines a variety of additional
primitives that allow smart contracts to conveniently manipulate thecontents of the states corresponding to these hashes.

The next two approaches add the F or D extensions to the ISA.
Naturally, this means the off-chain machine must implement all
RISC-V floating-point instructions. Furthermore, the blockchain
verifier must include a perfectly matching implementation.
In this approach, floating-point
instructions are still emulated off-chain. However, the emulation
now uses native integer instructions, rather than RISC-V integer
instructions. There are several high-quality open-source soft-float
implementations from which to choose [Bellard 2016; Houser 2017].
This makes the off-chain machine even faster.
Emulation by native integers

The next step in performancecomes from using native floating-point instructions off-chain. Obtaining reproducible results from two distinct fully conformingIEEE 754-2008 implementations requires the cooperation between
language standards, compilers, and, most regrettably, users. The
prospects are improved in Cartesi’s context, since the reference implementation controls all these components and can fully specify
any omissions in the standard. These corner cases include, but are
not limited to, underflows, the sign of zero, and operations involving infinity or NaNs. Even with the added overhead, this approachshould be the fastest one off-chain.
Native off-chain floating-point

5.1

Merkle trees [Merkle 1979] are binary trees where each node contains a hash. In Cartesi, Merkle trees are based on the keccak hashfunction [Dworkin 2015].3 Let s be a Cartesi Machine state, giving
the entire contents of its 64-bit address space. The Merkle tree mfor s, or, equivalently, its root node, is
m = merkle(s).

(2)

The tree is built up from its leaves in the following way. First, thestate is partitioned into 261 64-bit words. The tree leaves containthe hashes for these words. Since there is no chance for ambiguity,
we can simplify notation by identifying each node in the tree withthe associated hash. Then, internal nodes v in the tree are built fromtheir two children u1 and u2 by the relation

At present, the emulator makes the first two options available, that is,
floating-point is emulated by RISC-V integer instructions. Support
for the next two alternatives is planned for the future, when demand
for faster floating-point grows.

5

Machine state representation by hashes

Cartesi Machines in the blockchainv = keccak(u1 , u2 ).

(3)Here, keccak computes the hash of the concatenation of two input
hashes. The procedure builds a tree of depth 61. The set of nodes
at depth d partition the state into 2d ranges with 264 d bytes each.
Each node can therefore be identified by its depth and the starting
address a for its range, which is aligned to a 264 d boundary.

Recall that Cartesi is a platform for the development of decentralized
applications. Cartesi DApps enable parties that do not trust eachother to enter into a binding contract in the blockchain that depends
on the results of off-chain computations. It is convenient to use thecharacters Alice and Bob to represent these parties. Note that Aliceand Bob are roles, not people. They may even represent competingcollective interests. In fact, both roles will be played automaticallyby Cartesi Nodes that defend the interests of whomever controls
the off-chain computer where the node runs. Cartesi DApps are
therefore a collaboration between a set of smart contracts runningin the blockchain, and the off-chain software running on Alice’sand Bob’s nodes. As a general rule, the same DApp developer is
responsible for the smart contracts and the Dapp specific off-chain
software. The role of DApp developer will be played by Charlie.
Alice and Bob trust Charlie, otherwise they would not engage with

Figure 5 shows a sample machine state s. It has the special property
that devices have been aligned to nodes in m. For example, node v4
subtends everything in the machine apart from the flash devices. It
covers the shadows of the processor and the board, the ROM, the
CLINT and HTIF devices, and the RAM. Nodes v0 –v3 and v5 eachcover an independent flash device.
3 This eases integration with the Ethereum blockchain. Like Ethereum,
Cartesi assumes there is no practical way to engineer collisions for the keccak
hash function.

8Version 1.01
Moreover, given a valid proof for v in m, the same procedure canbe used to attest that a root hash m0 results from replacing v in mwith any given node v 0 . These verifications are very efficient, eachrequiring only d applications of the keccak hash.
We are now ready to define the first two Cartesi primitives
v = slice(m, a, d)

andm0 = splice(m, a, d, v 0 ).

(7)

In the absence of disputes, slice returns v and splice returns theresult m0 of replacing v in m with v 0 . To successfully defend theseresults in disputes, one can simply present siblings(m, a, d) and v
to the blockchain.
For convenience, Cartesi defines two additional primitives
and (8)w = read(m, a) , keccak(w) = slice(m, a, 61),
0

0

0

(9)

m = write(m, a, w ) = splice m, a, 61, keccak(w )for directly manipulating words, rather than hashes. Disputes can be
resolved once the blockchain receives siblings(m, a, 61) and w.

5.2

The verification game [Feige and Kilian 1997] is a protocol thatallows an arbiter with limited computational resources to referee agame between two computationally unlimited players. Its use in conjunction with Merkle trees was introduced by Canetti et al. [2011],
and the application to blockchains first appeared in TrueBit [Teutsch
and Reitwießner 2017]. In this scenario, the blockchain is the “referee”, and the “game” is between a “player” Bob that defends a result
for an off-chain computation, and a “player” Alice that disputes it.

Figure 5: The way in which the blockchain and off-chain representations for a machine state relate to each other.
Think of s as the initial state for some machine. In this case, theROM will contain the devicetree describing the hardware, and RAM
will be preloaded with the Linux kernel. The particular choice ofcommands listed in /sbin/init in the root file-system (flash 0)
decides what the machine does. It can, for example, perform anarbitrary computation over an input file-system (flash 1), and store
results in an output file-system (flash 3). The computation can evenbe informed by the contents of an additional independent parameterfile-system (flash 2).

Let s0 be the initial state for the computation, and sn its final state.
Recall that si+1 = step(si ) and mi = merkle(si ). The verification
game is the dispute resolution mechanism for Cartesi’s primitive
mn = compute(m0 , n) = merkle step(n) (s0 ) .

The interval [i, j], for i < j, is said tobe a disagreement interval if the following two conditions are met:
The disagreement step

1. Bob has sent to the blockchain hashes mi and mj , claiming
they correspond to merkle(si ) and merkle(sj );2. Alice has manifested to the blockchain that she agrees with mibut disagrees with mj .
A disagreement step is a disagreement interval where j

The following property of Merkle trees is the foundation for all these
operations: Given a node v, its depth d in tree m, and the starting
address a for the associated memory range, it is possible to verify
that v is indeed part of m. To see this, consider the path from v to m
Then, given the siblings ui for every node wi in the path:(keccak(ui , wi ), if a ^ 264 i ,wi 1 =
keccak(wi , ui ), if ¬(a ^ 264 i ).

i = 1.

When Alice disputes that mn = compute(m0 , n), the range [1, n]
becomes the initial disagreement interval. A partition contract canfind the disagreement step with an interactive binary search, startingfrom [1, n]. At iteration `, the contract starts with a disagreement
interval [i` , j` ]. It requests from Bob the hash mk` = merkle(sk` ),where k` is the middle point between i` and j` . Knowing Bob’s mk` ,Alice then chooses between [i`+1 , j`+1 ] = [i` , k` ] or [k` + 1, j` ] as
the next disagreement interval. This continues until Alice selects aninterval with length one.

(4)

(5)

The procedure finishes after O(log n) interactions between Alice,
Bob, and the partition contract.4 Any party that fails to react withina pre-determined deadline looses the verification game by timeout.
At iteration `, Alice and Bob must independently obtain the state sk`
for the machine. If the machine is always started from scratch, theFor this reason, the sequence
siblings(m, a, d) = (u1 , u2 , . . . , ud )(10)

It is divided into two stages. The first stage finds a single step ofcomputation on which Alice and Bob disagree. The final stage
effectively computes the step that follows. If it matches the state
proposed by Bob, he wins the dispute. Otherwise, Alice wins.

Now assume s halts in state s0 . From the blockchain’s perspective,running m until it halts can be seen as the evaluation of an arbitrary
function v20 = f (v0 , v1 ). Here, v20 is the node in m0 = merkle(s0 )that corresponds to v2 in m. Consider a library of hashes f , eachcorresponding to a different useful function. For example, onesuch function could decrypt the input file-system v0 into the output
file-system v20 , taking a key from the parameter file-system v1 . To
specify this computation in terms of Cartesi Machines with a single
hash m, a smart contract must build m from its components f , v0 ,and v1 . Once it receives m0 , it must be able to settle disputes overwhether m indeed halts as m0 . Finally, it must be able to verify thatif v10 is the node in m0 that corresponds to v1 in m.

wd = v, wd 1 , . . . , w1 , w0 = m.

The verification game

(6)

serves as proof for the claim that v is at address a and depth d in m.
To verify this, simply compute p0 from (5) and compare with m.

4 This can be reduced by changing to an n-ary search.

9

Version 1.01
total incurred off-chain computation is O(n log n). However, bypreserving a snapshot of si` , they can bring the cost down to O(n).

several machines that exchange data with each other. An empty
DAG is first initialized with a call to:dag = dag()At this point, the blockchain has found thedisagreement step [i, i + 1], where i 2 {0, . . . , n 1}. It knows
both mi and mi+1 according to Bob. Alice agrees with mi , but disputes mi+1 . To decide the party with just cause, the blockchain must
effectively compute m0i+1 = merkle step(si ) and compare it with
Bob’s mi+1 . However, the blockchain does not have unrestricted
access to si . All it has is the root hash mi = merkle(si ).
Settling the dispute

Each DAG vertex corresponds to a primitive. A primitive’s inputs
come from the outputs of its children vertices. The primitive’s output
can in turn serve as input to one or more primitives.
Primitives are divided into two categories. Disputable primitives
behave as future values promised to Alice by Bob. Their outputs are
set by Bob, and must be accepted or disputed by Alice. Disputableprimitives can only appear as internal vertices in the expression
DAG. They are the read, write, slice, splice, step, and computeprimitives described in sections 5.1 and 5.2.

Alice is expected to post her off-chain state access log for step(si ) toa memory manager contract. Off-chain, these accesses progressively
modify the state si = (si )0 into (si )1 , (si )2 , . . . until after thekth and last access it becomes (si )k = si+1 . All machine steps
take O(1) time to simulate and number k of accesses is always small.
Entry j in the log, for j 2 {1, . . . , k}, contains

Constant primitives have their outputs set by Charlie. They are are
implicitly accepted by both Alice and Bob throughout their interactions with Charlie’s DApp. These primitives potentially represent
large chunks of data and the availability of their contents has to beguaranteed by Charlie, possibly with help from our data availability
primitives. Naturally, word, hash, string, and id literals are constants.
Cartesi’s blob, resource, and machine primitives, described below,
are also constant. Only constant primitives can appear as DAG
leaves.

1. An operation oj for the access (read or write);
2. An address aj for the access;3. The word rj at aj in (si )j 1 ;30. In case of writes, the word wj at aj in (si )j ;4. The siblings (mi )j 1 , aj , 61 .
The blockchain implementation for the step function is hosted byan emulator contract. Alice’s off-chain implementation must match
this blockchain implementation down to the order in which the state
accesses are logged. As a benefit of this restriction, the blockchain
implementation can read and write to the state as if its whole contents
were available. During its execution, the reference step function
issues a sequence of state accesses to the memory manager. As longas the accesses match Alice’s log, everything works transparently.

Cartesi supported constant and future types are:constant ::= word | hash | string | id
disputable ::= word-future | hash-future

Constant primitives accept only constants as input. In contrast,
disputable primitives accept both constants and disputables:

Formally, as the reference step function performs k0 accesses, thememory manager progressively updates mi = (m0i )0 to (m0i )1 ,(m0i )2 , . . . , until it reaches (m0i )k0 . Access j, for j 2 {1, . . . , k0 },contains the following information

word-type ::= word | word-futurehash-type ::= hash | hash-future

Blob primitives represent arbitrary binary
data stored in the blockchain. The provided hash gives the output.
It must match the root hash for a Merkle tree built from the data,padded with zeros to 264 depth bytes:
Constant primitives

1. An operation o0j for the access (read or write);
2. An address a0j for the access;3. In case of writes, the word wj0 to be written.

hash = dag :blob{hash = hash ,depth = word ,data = string}

As each access is processed, the memory manager:• Checks that j  k, o0j = oj , and a0j = aj ;• Checks that rj = read (m0i )j 1 , aj with the siblings.
Then, for a read access, the memory manager:

Resource primitives describe files stored off-chain. Files are assumed
to be available from the given uri. The download-size can beused to bound, a priori, the total data transfer requirements. Only the
first range-length bytes of the file are considered. This bounds
the memory required to map it into the machine state. The provided
hash output must match the root hash for a Merkle tree built fromthe first range-length bytes of the corresponding file, padded withzeros or truncated to 264 depth bytes:• Sets (m0i )j = (mi )j 1 ;• Returns rj to the emulator contract.
For writes, the memory manager:• Checks that wj0 = wj ;• Sets (m0i )j = write (m0i )j 1 , aj , wj ) with the siblings.
At any point, if a check fails, Alice loses the dispute. If, however,k = k0 and mi+1 6= (m0i )k0 , Alice wins the dispute.

5.3

hash = dag :resource{hash = hash ,depth = word ,range-length = word ,download-size = word ,uri = string}

Cartesi Machines as one of many primitives

Cartesi primitives are made available to Charlie through a functional
programming interface. The goal is isolating the primitives fromthe idiosyncrasies of specific smart contract programming languages
and blockchains. The syntax itself is not important. What matters isthe semantics associated to each primitive.

Machine primitives are used to describe Cartesi Machine states. The
specification follows the scripting interface described in section 4.1.
The only the difference is that backing files are given as paths.
Instead, they are resource constants. The provided hash output
must correspond to the root Merkle tree hash for the corresponding
Cartesi Machine state:Charlie can use this interface to build expression DAGs that represent
complex composite computations. The computations can involve

10

Version 1.01
hash = dag :machine{hash = hash ,processor = processor ,rom = rom ,ram = ram ,flash0 = drive ,...
flash7 = drive ,clint = clint ,htif = htif}

word-future = dag :if{condition = word-type ,if-true = word-type ,if-false = word-type}

The hash primitive builds a 256-bit hash by the concatenation of its
64-bit component words:
hash-future = dag :word4(word-type , word-type ,word-type , word-type )To help with Merkle tree construction, hashes can be built fromwords and from the concatenation of two hashes:

The compute primitive executes a Cartesi
Machine. The initial-state gives the value of m0 and steps
the value of n, so that the future value is compute(m0 , n). Steps
therefore bounds, a priori, the amount of computation required:Disputable primitives

hash-future = dag :keccak(word-type )hash-future = dag :keccak(hash-type , hash-type )For completeness, hashes can also be tested for equality and used as
input for a conditional:

hash-future = dag :compute{initial-state = hash-type ,steps = word-type}

word-future = dag :eq(hash-type , hash-type )word-future = dag :neq(hash-type , hash-type )The Merkle tree manipulation primitives slice, splice, read, andwrite are available as:

hash-future = dag :if{condition = word-type ,if-true = hash-type ,if-false = hash-type}

hash-future = dag :slice{root = hash-type ,address = word-type ,depth = word-type}

Charlie must define the identity ofthe players for the roles of Alice and Bob. Recall that Bob proposesa result and Alice can object or accept it:
DAG and vertex interfaces

hash-future = dag :splice{root = hash-type ,address = word-type ,depth = word-type ,target = hash-type}

dag :proposing-role{id = id , stake = word }dag :objecting-role{id = id , stake = word }The stake argument gives the price for buying Alice’s or Bob’s
position. It measures what is at stake for each of them depending on
the results of the computation. Charlie sets this value to facilitate
Alice and Bob to delegating their roles (section 6.2).

word-future = dag :read{root = hash-type ,address = word-type}

Primitive creation functions return:hash-future = dag :write{
root = hash-type ,address = word-type ,word = word-type}

vertex ::= constant | disputable

A DAG may contain multiple disconnected sub-DAGs. To specify
or retrieve the root vertex for the DAG, Charlie invokes:
dag :root(vertex )Cartesi also provides a variety of simple primitives that increase theexpressive power of expressions. Disputes over such primitives canbe settled within the blockchain directly from their inputs. Several
binary operations on words have the signature:

This value can be later obtained by anyone that calls:
vertex = dag :root()

word-future = dag :bin-op (word-type , word-type )The primitive for any vertex can be queried:

and mirror the RISC-V ISA.They can be divided into arithmetic:

primitive = vertex :primitive()
primitive ::= word | hash | string |blob | resource | machine |read | write | slice | splice |add | sub | ... | geu | if |word4 | keccak | keccak-hh | eq-hh | if-hh

add, sub, mul, mulh, mulhu, mulhsu,
div, divu, rem, remu, sll, srl, sra;

bitwise:or, and, xor;

Likewise, the children can be obtained by name or index:

and comparisons:vertex = vertex :child-by-index(word )vertex = vertex :child-by-name(string )eq, ne, lt, ltu, ge, geu.

Together, the primitive and child functions enable the entire
sub-DAG reachable from a vertex to be traversed.

Signed integers are represented by two’s complement. Boolean
values are returned as words where 1 means true and 0 means false.
Conversely, when a Boolean value is expected by a conditional, 0 is
considered false and any other value is considered true.

The DAGs and vertices can change state during their lifetimes:
dag-state ::= undefined | proposed | accepted |objected | sustained | overruled

Conditionals are available as ternary if primitives whose output is
set to if-true if condition is true, and if-false otherwise:vertex-state ::= undefined | proposed | accepted11Version 1.01
Constant vertices are always in the accepted state. At construction,
the DAG and all its disputable vertices are in the undefined state.
These states can be obtained from the DAG and vertex objects:
dag-state = dag :state()vertex-state = vertex :state()

Figure 6: Expression DAG corresponding to the decryptor example.
Constant vertices corresponding to literal values have been omitted
for brevity. Variable names are shown in gray.

Proposing the value of any vertex changes its state to proposed:
vertex :propose-hash(hash )vertex :propose-word(word )To start a proposal, Bob first invokes:

The following example illustrates the power of theexpression DAG interface:
An example

dag :start-proposal()Then, he proposes the output value for the root vertex. Finally, hecompletes the proposal with a call to:d = dag()decryptor = library{hash = decryptor-machine-hash,dag = d}dag :finish-proposal()This changes the DAG to the proposed state.

input = d:resource{hash = input-hash,depth = decryptor-flash-1-depth,
uri = http://example.com/charlie/input.drive}

The value proposed for any vertex can be checked with a call to:word = vertex :proposed-word()hash = vertex :proposed-hash()

To accept the proposed root for the DAG, Alice calls:

key = d:blob{hash = password-hash,depth = decryptor-flash-2-depth,
data = password}

dag :accept()

This changes the DAG state to accepted.

loaded-decryptor = d:splice{root = d:splice{root = decryptor,
address = decryptor-flash-1-addr,
target = input},
address = decryptor-flash-2-addr
target = key}

To object to the root value for the DAG, Alice invokes:
dag :start-objection()and then proposes a new, distinct value for the root vertex. There
are now two cases to consider. If all immediate children of the root
vertex are in the accepted state, the dispute can be settled by the root
primitive resolution protocol. To that end, Alice simply calls:

executed-decryptor = d:compute{initial-state = loaded-decryptor,
steps = 10*2^32}

dag :finish-objection()

This changes the DAG to the objected state while the protocol iscompleted. If Alice succeeds, the DAG is changed to the sustained
state. Otherwise, it is changed to the overruled state.

iflags = d:read{root = executed-decryptor,
address = machine-processor-iflags-addr,}

If, however, there are any proposed or undefined children, she mustfirst propose values for all vertices in the sub-DAG reachable fromthe root. Only then can she call:tohost = d:read{root = executed-decryptor,
address = machine-htif-tohost-addr}

dag :finish-objection()

This changes the DAG to the objected state. Bob must now find avertex, accessible from the root, for which he accepts all inputs but
objects to the output. To specify this vertex, Bob gives its path fromthe root. He also must specify a distinct value for its output:

halted = d:neq(d:and(iflags, 1), 0)
done = d:eq(d:srl(d:and(tohost, d:srl(-1, 16)), 1), 0)
success = d:and(halted, done)
d:root(success)dag :defend-word(path , word )dag :defend-hash(path , hash )In the example, Charlie defines an expression DAG with root success.
The implied computation starts with a decryptor machine, available
from an off-line library (not shown). Charlie can install his own
library of pre-defined machines in the Cartesi Node, or use a libraryof machine specifications created and stored remotely by anotherdeveloper. Either way, the hash constant ensures machines that havebeen tampered with can be easily identified. Next, input and key
flash devices are spliced into the decryptor machine. This loadeddecryptor is run for at most 2*2^32 steps, and results in an executeddecryptor. The corresponding state is then probed. Inspection of
the processor’s iflags register tells if the machine is halted. The

path ::= {vertex1 , vertex2 , ..., vertexk }If the vertex is undefined, Alice’s dispute is declared ill-formed
and Bob wins immediately. If the path is invalid, Bob’s defense
is declared ill-formed and Alice wins immediately. Otherwise, theprimitive dispute resolution protocol is engaged.
With this setup, arbitrarily complex expressions behave just like
disputable Cartesi primitives: they have agreed-upon inputs andcome equipped with a dispute resolution procedure for their output.

12Version 1.01
value stored in the payload of HTIF’s tohost register tells if themachine halted after it was done decrypting. Figure 6 shows thecorresponding DAG, with literal values (i.e., strings, words, andhashes) omitted.

To download the data for all constant nodes in the main sub-DAG
and verify the computed hashes match the declared hashes:
download-status = off-dag :download{timeout = word }download-status ::= accepted | failed | timedout

Charlie oversees Alice’s and Bob’s interaction with the DAG and its
vertices. After all, Charlie is responsible for the blockchain DApp
component where these objects live. Charlie’s software acting on
Alice or Bob’s behalf can issue events that trigger reactions from theCartesi Nodes representing Alice and Bob. These reactions are also
under Charlie’s control, since he is in charge of the off-chain DApp
components installed in their nodes. He must, as usual, protect his
DApp against attacks by rogue users. Cartesi simplifies part of thisprocess by encapsulating access control in all DAG operations.

6

Once download is complete, all vertices in the main sub-DAG canbe evaluated with a single call to:
off-dag :evaluate()

The upload method submits results back to the blockchain. It also
isolates DApp developers from the details of any potential dispute:
off-dag :upload{fee = word }The fee argument is used for role delegation (section 6.2).

The Cartesi Node

Let v be the root for the main sub-DAG. The upload method checks
whether the role being played is proposing or objecting. The proposing role only acts if v is undefined in the blockchain. In that case,it proposes the value it obtained off-chain for v. The objecting role
only acts if a value for v has been proposed to the blockchain. If thevalue matches what it obtained off-chain, it accepts the value. Thisis how the overwhelming majority of interactions will play out. If,
however, the proposed value for v in the blockchain does not matchthe value computed off-chain, the objecting role starts a dispute. The
ensuing interactions between the blockchain and the Cartesi Nodesof both proposing and objecting roles are automatically handled byCartesi the platform.

The Cartesi Node is the software and hardware infrastructure thathosts the off-chain components of Cartesi DApps. Each user thatwishes to interact with a Cartesi DApp must have a Cartesi Node at
his disposal. Cartesi Nodes will initially be made available as Docker
containers to be run on a computer under the user’s responsibility.
Future plans include their distribution as a multi-platform librarythat developers can link to an executable for users to install as aself-contained DApp.
DApps can include native off-chain components that access the fullstorage and computational power of the hardware where the node isinstalled. In addition, all nodes contain a reference implementationof the Cartesi Machine that DApps can control to perform verifiable
computations. Finally, nodes contain the infrastructure necessary forthe interaction of off-chain and blockchain DApp components.5

With the exception of the compute primitive, disputes can be settled
right away. Compute primitives require multiple interactions withthe blockchain. If a party cannot guarantee the responsivenessof his Cartesi Node throughout a dispute, he could lose by default
judgement. To minimize this risk, Cartesi offers another convenience
to DApp developers: the dispute delegation market.

At the core level, the Cartesi platform gives DApp developers the
freedom to combine native code, reproducible Cartesi Machines,
and the blockchain’s API in any way they see fit. Given the fast pacein which novel applications for blockchain technology appear, thisseems to be the only way to avoid restraining developers’ creativity.
Nevertheless, we can foresee a variety of common tasks, challenges,
and patterns that are likely to arise when using the Cartesi platform.
With time, the Cartesi platform will encapsulate these into a set of
higher-level interfaces built on top of the core [Teixeira and Nehab
2019a]. The core includes only facilities for the automated execution
and verification of Cartesi Machines.

6.1

6.2

Dispute delegation market

A principal party can delegate potential disputes to a proxy by setting the fee argument of the upload method to a non-zero value.
This causes Cartesi to advertise the disputed DAG in the disputedelegation market. The advertising principal is notified as soon as aproxy purchases a dispute. Proxy candidates own Cartesi Nodes on
which Cartesi’s dispute proxy DApp has been enabled. Users of theproxy DApp are in the business of collecting fees for defending theinterests of principal parties that are unwilling to conduct their own
disputes.

Off-chain expression DAGs

Off-chain DApp components need to interact with existing blockchain DAGs. After all, the computations implied by such DAGs
must be performed off-chain within the Cartesi Node. These interactions are mediated by off-chain representations for DAGs, which
can be automatically built from a blockchain instance with a call to:

The proxy DApp download an advertised DAG, computes its value
off-chain, and checks if it matches the value proposed to the blockchain by the role for sale. If so, it can purchase the role for the stakespecified in the DAG. This amount will be returned if and only if
the proxy wins the ensuing dispute. In that case, the proxy is also
rewarded the fee. If the proxy fails in the dispute, the stake isinstead sent to the principal party.

off-dag = off-dag(dag )Off-chain DAGs provide DApps with a high-level interface thatcompletely encapsulates typical use cases.

Guarantees Cartesi guarantees that an honest party can always
win any dispute in which it is involved. This is a strong guarantee,
but it is also the only guarantee. In the absence of disputes, thevalue for the DAG is defined to be whatever the interested parties
proposed and accepted. It is therefore perfectly reasonable to act
on the accepted value, whether or not it is indeed the true result of
the computation defined by the DAG. Any unsatisfied party has the
responsibility of contesting the value.

Bounds for the data transfer, memory, and computation requirements
for the main sub-DAG can be obtained from:bounds = off-dag :bounds()
bounds ::= {data = word,
memory = word,compute = word}

Disputed values, however, may or may not be useful. The situationis truly exceptional: At least one of the parties is being dishonest,
perhaps even both are. The proper way forward must be decided

5 In the case of Ethereum, a light client.

13

Version 1.01
by the DApp developer. One potentially useful bit of information
is whether the objection was overruled or sustained. Note that eventhis bit is only true when at least one of the parties is honest.

should not be immediately passed to the proxy party. Other usability
constructs will be described to facilitate file transfers and reduce
gas costs. Together, these facilities will bring the user experience ofCartesi DApps closer to that of current centralized solutions.

Whenever a principal party wishes to delegate a dispute to a proxy,it has no way to guarantee its interests will be defended in goodfaith. The only solution is to align the interests of the principal andproxy. This is why proxy roles must be purchased by the principal’s
stake in the dispute. If the proxy is honest and wins the dispute on
the principal’s behalf, the only cost to the principal is the fee. He
may receive further benefits from the contract where the disputeoriginated. If the proxy loses the dispute, whether on purpose or by
negligence, the principal keeps the stake. His interest in the originalcontract becomes moot.

A variety of higher-level APIs that encapsulate
typical uses for the core will be available with the release of the
Cartesi SDK. These will include the usability and data availability
solutions described above, as well as the containers for the Cartesi
Node and for the development of Cartesi Machines. In time, the APIs
available within the SDK will greatly reduce the size and complexity
of DApps blockchain components. In turn, this will significantly
increase the portability of DApps to multiple blockchains. The
Cartesi SDK will be distributed in open source and extensively
documented [Teixeira and Nehab 2019b].
The Cartesi SDK

Naturally, no proxy will ever buy disputes from principals playing
dishonest roles. They are, as they should, on their own defending
their interests. Even honest principals may fail to sell disputes if thefee is too low or the stakes too high. To guarantee service availability
to honest principals, Cartesi will maintain a number of nodes withthe dispute proxy DApp installed. These nodes will be configured
to purchase, up to a maximum stake, advertised disputes that are
profitable but have not found a proxy within a preset deadline.

7

Cartesi Machines can beextended with two exciting new devices. The dehashing device
gives applications the power to traverse hash pointer data structures.
Programs running inside a Cartesi Machine can use the dehashingdevice to read the contents of a block given only its hash. Although
this operation is impossible in general, it becomes possible when
the universe of allowed blocks is known by all parties in advance.
The most direct application is to blockchains themselves. When a
Cartesi Machine is running, the dehashing device queries a hashtable, preloaded in the host, for the block that matches the hash. If a
dispute arises, any party can propose the block as proof it matches therequired hash. In this way, the dehashing device enables blockchain
introspection. Parties can enter into contracts that depend on theentire state of the blockchain where the contracts are themselvesdefined. This has a variety of valuable applications, notably infutures markets.
Extensions to the Cartesi Machine

Future work

The focus of this document on the core functionality, and on theinterfaces DApps use to directly specify, control, and verify off-chain
computations. The Cartesi platform will offer several additional
components built over the core, or extending its reach. These will be
described in more detail in future publications [Teixeira and Nehab
2019a,b].
Cartesi remedies the severe storage limitationsof the blockchain by keeping on-chain only Merkel tree hashes ofoff-chain data. As mentioned in section 5.2, Cartesi assumes that all
parties involved in a verification role have access to these data. In
certain applications, this is difficult to guarantee. In particular, therisk for data withholding attacks, where one of the parties submits ahash to the blockchain while refusing to make this data available toothers, must be mitigated.
Data availability

Another planned device is the timely data port. The port enables
reproducible communication between Cartesi Machines by tying thedata packets entering or leaving the machine to the value of mcycle
at the event. DApps can schedule packet delivery to happen at agiven future mcycle. Cartesi Machines can also be rolled back to
the mcycle for delivery. The timely data port breaks new ground in
the progress towards the Web 3.0. It will enable DApps that involvethe direct collaboration between multiple Cartesi Machines.

The problem of data availability is a major concern in the design ofblockchain consensus algorithms [Buterin 2012]. However, the issue
becomes much simpler in the context of local consensus. Teixeira
and Nehab [2019a] provide several design patterns for dealing withdata availability during verification. Data channels, device encryption, and the data ledger ensure availability in all scenarios likely to
be encountered by Cartesi DApps.

It is possible to envision applications that involve
many independent participants, each with some stake in the resultsof an off-chain computation. In such cases, it is vital to prevent a
coordinated crowd of dishonest participants from using sequential
disputes over an honest result as a denial-of-service attack on thecontract. We have developed a variant of the verification game thatenables any honest participant to defend his result against an entire
crowd at negligible cost. When demand becomes apparent, theCartesi platform will be extended to support this variant.
Crowd disputes

One of the key barriers to the wide adoption of blockchain technology is the inconvenience experienced by DApp users.
Although the literature on usability of centralized applications still
applies to decentralized ones, blockchain idiosyncrasies have notyet been fully addressed from the perspective of user experience.
Teixeira and Nehab [2019a] describe several design patterns for thedevelopment of simple and intuitive DApps.
Usability

8

Conclusions

This paper laid the foundations on which the Cartesi platform stands.
Cartesi’s mission is to help DApp developers build ever more compelling products to their clients. As any paradigm shift, the blockchain brings both opportunity for real innovation and the risk of“wheel reinvention”. In a direct application of the principle of least
astonishment, Cartesi’s core enables developers to leverage preexisting knowledge and tools to boost their productivity. The remaining components of the Cartesi platform, described in a future
document [Teixeira and Nehab 2019a], will help developers unleash
their creativity when taking advantage of the blockchain’s uniquepotentials.

As an example, Cartesi will offer an automatic infrastructure for trading tokens. This will free the users from concerns over the different
tokens used inside each DApp. A system for outsourcing deferred
actions will also be provided. This will enable users to turn their machines off even when engaged in a protocol that requires interactingwith the blockchain within strict deadlines. In this situation, a proxy
party will act on the users’ behalf in exchange for a fee. (Much likethe dispute delegation market described in section 6.2.) The use of
cryptographic time-locks [Rivest et al. 1996] will also accommodate
situations in which the user must reveal a secret in the future that14

Version 1.01

References

H OUSER , J. 2017. Berkeley softfloat. Webpage. http://www.
jhauser.us/arithmetic/SoftFloat.html. Release 3d.

B ELLARD , F. 2016. Softfp library. Webpage. https://bellard.
org/softfp/.
B ELLARD , F. 2017. Riscvemu. Source code. https://bellard.
org/riscvemu/.
B ELLARD , F. 2018. A generic and open source machine emulator
and virtualizer. Webpage. https://www.qemu.org.
B EN -S ASSON , E., B ENTOV, I., H ORESH , Y., and R IABZEV, M.
2018. Scalable, transparent, and post-quantum secure computational integrity. IACR Cryptology ePrint Archive, 2018:46.
B EN -S ASSON , E., C HIESA , A., T ROMER , E., and V IRZA , M.
2013. Succinct non-interactive zero knowledge for a von neumann architecture. Cryptology ePrint Archive, Report 2013/879.
https://eprint.iacr.org/2013/879.

IEEE, C. S. 2008. Standard for floating-point arithmetic, IEEE Std
754-2008.
I E XEC ,T. 2017.
Blockchain-based decentralized cloudcomputing. https://iex.ec/whitepaper/iExec-WPv3.0English.pdf.

L ARIMER , D. 2017. Dpos consensus algorithm - the missing white
paper.
https://steemit.com/dpos/@dantheman/dposconsensus-algorithm-this-missing-white-paper.
L EE , S., S HIH , M.-W., G ERA , P., K IM , T., K IM , H., and P EINADO ,M. 2017. Inferring fine-grained control flow inside sgx enclaves
with branch shadowing. In 26th USENIX Security Symposium,
USENIX Security, 16–18.
M ERKLE , R. C. 1979. Secrecy, Authentication, and Public Key
Systems. PhD thesis, Stanford University.
M IERS , I., G ARMAN , C., G REEN , M., and RUBIN , A. D. 2013.
Zerocoin: Anonymous distributed e-cash from bitcoin. http://zerocoin.org/media/pdf/ZerocoinOakland.pdf.
M OGHIMI , A., I RAZOQUI , G., and E ISENBARTH , T. 2017.
CacheZoom: How SGX amplifies the power of cache attacks.
In International Conference on Cryptographic Hardware andEmbedded Systems, 69–90.

B ITANSKY, N., C ANETTI , R., C HIESA , A., and T ROMER , E.
2012. From extractable collision resistance to succinct noninteractive arguments of knowledge, and back again. In Proceedings of the 3rd Innovations in Theoretical Computer Science
Conference, ITCS ’12, New York, NY, USA. ACM, 326–349.
ISBN 978-1-4503-1115-1. http://doi.acm.org/10.1145/
2090236.2090263.
B LUM , M., F ELDMAN , P., and M ICALI , S. 1988. Non-interactive
zero-knowledge and its applications. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, STOC
’88, New York, NY, USA. ACM, 103–112. ISBN 0-89791-264-0.
http://doi.acm.org/10.1145/62212.62222.
B RASSER , F., M ÜLLER , U., D MITRIENKO , A., KOSTIAINEN ,K., C APKUN , S., and S ADEGHI , A.-R. 2017. Software grandexposure: SGX cache attacks are practical. In 11th USENIX
Workshop on Offensive Technologies.

M ORRISON , D. R. 1968. Patricia—Practical Algorithm To Retrieve
Information Coded in Alphanumeric. Journal of the ACM, 15(4):514–534.
NAKAMOTO , S. 2009. Bitcoin: A peer-to-peer electronic cash
system. Whitepaper. http://bitcoin.org/bitcoin.pdf.
NEO’ S VM. 2017. OpCodes. Source code. https://github.
com/neo-project/neo-vm/blob/master/src/neovm/OpCode.cs.

B UTERIN , V. 2012. A note on data availability and erasure coding. https://github.com/ethereum/research/wiki/Anote-on-data-availability-and-erasure-coding.

PARNO , B., H OWELL , J., G ENTRY, C., and R AYKOVA , M. 2013.
Pinocchio: Nearly practical verifiable computation. In 2013 IEEE
Symposium on Security and Privacy, 238–252.
P ETAZZONI , T. 2018. Buildroot. Website. https://buildroot.
org.

B UTERIN , V. 2018. On sharding blockchains. Wiki. https://github.com/ethereum/wiki/wiki/Sharding-FAQs.
B UTERIN , V. 2018. Sharding. GitHub repository. https://github.com/ethereum/sharding.git.
C ANETTI , R., R IVA , B., and ROTHBLUM , G. N. 2011. Practicaldelegation of computation using multiple servers. In Proceedings of the ACM Conference on Computer and Communications
Security, 445–454.

RISC-V. 2018. GNU toolchain. GitHub repository. https://github.com/riscv/riscv-gnu-toolchain.
RISC-V. 2018. Linux. GitHub repository. https://github.com/
riscv/riscv-linux.
RISC-V. 2018. Poky: port of the Yocto project. GitHub repository.
https://github.com/riscv/riscv-poky.
RISC-V. 2018. Project home. GitHub repository. https://github.com/riscv.
RISC-V. 2018. Proxy Kernel. GitHub repository. https://github.com/riscv/riscv-pk.

C ARDANO ’ S VM. 2017.
IELE OpCodes.
Source code.
https://github.com/runtimeverification/ielesemantics/blob/master/iele.md.
C HENG , R., Z HANG , F., KOS , J., H E , W., H YNES , N., J OHNSON ,N. M., J UELS , A., M ILLER , A., and S ONG , D. X. 2018. Ekiden: A platform for confidentiality-preserving, trustworthy, andperformant smart contract execution. CoRR, abs/1804.05141.

R IVEST, R. L., S HAMIR , A., and WAGNER , D. A. 1996. Time-lock
puzzles and timed-release crypto.

DTS PEC . 2017. Devicetree specification. Power.org, Freescale
Semiconductors, IBM, Linaro, and ARM. http://devicetree.
org.

S CHAEFFER , T. 2018.
Zokrates.
https://github.com/
JacobEberhardt/ZoKrates.
S ONG , C., W U , S., L IU , S., FANG , R., and L I , Q.-L. 2018. Distributed cloud computing in trusted hardware. https://ankr.
network/.

DWORKIN , M. J. 2015. SHA-3 standard: Permutation-based hashand extendable-output functions. Technical report.
E NIGMA , T. 2018. Enigma documentation. https://enigma.co/
protocol/.
F EIGE , U. and K ILIAN , J. 1997. Making games short. In Proceedings of STOC, 506–516.
G OLEM , T. 2016. The golem project. https://golem.network/
crowdfunding/Golemwhitepaper.pdf.

SONM, T. 2018. Sonm documentation. https://docs.sonm.
com/.
TEEX, T. 2018. TEEX—TEE-enabled eXecution platform for
public blockchain. https://teex.io.
T EIXEIRA , A. and N EHAB , D. 2019. Cartesi design patterns.

15Version 1.01
Whitepaper. To appear.
T EIXEIRA , A. and N EHAB , D. 2019. The Cartesi SDK. To appear.
T EUTSCH , J. and R EITWIESSNER , C. 2017. A scalable verification
solution for blockchains. Whitepaper. https://people.cs.
uchicago.edu/⇠teutsch/papers/truebit.pdf.
T ILLEY, A. 2018.
Google, Tesla get behind challenge to Arm chip design.
The Information.
https://www.theinformation.com/articles/google-teslaget-behind-challenge-to-arm-chip-design.
T RÖGER , J., M IHO ČKA , D., and K EPPEL , D. 2011. Fast microcode interpretation with transactional commit/abort. In 4thWorkshop on Architectural and Microarchitectural Support for
Binary Translation, San Jose, CA. http://www.emulators.
com/docs/amas-bt2011.pdf.
VAN S ABERHANGEN , N. 2013. Cryptonote v 2.0.
V LASENKO , D. 2018. Busybox. Website. https://busybox.net.
WATERMAN , A. and A SANOVI Ć , K. 2017. The RISC-V Instruction
Set Manual, volume I: User-Level ISA. RISC-V Foundation.
Version 2.2.
WATERMAN , A. and A SANOVI Ć , K. 2017. The RISC-V Instruction Set Manual, volume II: Privileged Architecture. RISC-V
Foundation. Version 1.10.
WATERMAN , A. and L EE , Y. 2011. Spike, a RISC-V ISA simulator. GitHub repository. https://github.com/riscv/riscvisa-sim.
W EBA SSEMBLY , C. G. 2018. WebAssembly specification, release
1.0. https://webassembly.github.io/spec/core/index.
html.
W EICHBRODT, N., K URMUS , A., P IETZUCH , P., and K APITZA ,R. 2016. AsyncShock: Exploiting synchronisation bugs in Intel
SGX enclaves. In European Symposium on Research in Computer
Security, 440–457.
W OOD , G. 2018. Ethereum: A secure decentralised generalised
transaction ledger. Yellowpaper. https://ethereum.github.
io/yellowpaper/paper.pdf. Byzantium version e94ebda –2018-06-05.

16