Machine Swapping and Micro Architecture technique

[GCdePaula]

Amazing project and great goals! Multiple fault-proof modules is definitely the way to go, and likewise for optimizing for simplicity.

There’s a (I believe novel) technique used by Cartesi called machine swapping that simplify parts of the fault-proof system, which may be of interest to you. It's a clever approach to keep the proving machine/environment stupid simple, and yet have the execution machine/environment support more software. The insight is leveraging the good compilers that exist for high-level languages.

However, since the goal of this technique is to support more intricate execution environments (which is a goal of Cartesi), it does make parts of the system more complex, and may thus be contrary to Asterisc's goals. Nevertheless, I’ll post a short description here, with explanatory purpose only, in case it interests you.

Motivation

Let's suppose we're writing our emulators and dapps in C, and we have trusted C compilers that can target x86, RISC-V with a load of extensions, and RISC-V with bare minimum extensions. This is reasonable. (In case of Cartesi, we're using C++ and GCC, but this is more of an implementation detail and there are many languages/implementations where this is also reasonable.)

And for simplicity's sake, without loss of generality, suppose we're dealing with special kind of rollups where there's only a single input. This way, the program is already instantiated with this single input, and the program will execute it until halt, or some maximum number of predefined cycles.

Our machine model is given as a step function over some state S, which performs the state transition from S[k] to S[k+1]. Now, for a fault-proof system we need the step function implemented both offchain (in C) and onchain (in Solidity). From the point of view of these step functions, we'd want the simplest architecture possible. Think something like subleq. Or perhaps a bit less extreme and with a lot more support: a minimalist RISC-V ISA like rv64i (let's call it uarch, for micro-architecture).

The issue with this choice is, of course, from the point of view of development and execution. There are not many things one can compile to subleq, and execution will be sluggish. In uarch things are not as bad, but still not ideal. We'd love to develop on and emulate something like rv64gc instead of rv64i.

Now, to the insight. Couldn't a rv64gc emulator be emulated by a rv64i emulator? Even further, couldn't we reuse exactly the same rv64gc emulator codebase, but just compile it instead to rv64i?

Machines and States

Imagine we have a pair of deterministic machines/emulators written in C: the big-machine (running the bigarch, think rv64gc ISA) and the micro-machine (running uarch, think rv64i ISA). The former is what we want to write our programs on and execute, and the latter what we wish we had to code in Solidity. We compile both bigstep and ustep to bare-metal (think x86).

And imagine these two machines can operate over the same state. So one could call either bigstep or ustep on S. Suppose things like registers/ROM/RAM from each machine are completely distinct parts of S.

Back to the insight: since we can put any program inside our micro-machine, we could put a program that knows how to emulate a single instruction of bigarch and halt. This program is exactly what we get when we compile bigstep to uarch ISA. Of course, we then put the code of our dapp (compiled to bigarch), as well as its single input, on the big-machine, which is nested inside the micro-machine.

Now, if we could reset the micro-machine to its pristine state (right before starting to emulate one instruction of bigarch), while preserving the state of the big-machine, then we would be able to run our entire dapp, start to finish, just doing a bunch of ustep followed by a ureset and loop.

Swapping

Of course, just running ustep would be very very slow. But what we have is two ways to compute a big state transition: we can either run a bunch of ustep followed by a single ureset, or we could just run bigstep. If our compiler generated sound code, they will always match.

Therefore, we normally only turn on the big machine. When there's a dispute, we first turn on the big-machine to find the first divergence, and only after that we turn on the micro-machine to find on which micro-instruction players diverge (or if they diverged on the ureset operation).

We call this approach of changing which machine is running machine swapping.

There are more hidden details here, like fixed-point states, avoiding doing two partitions/bisections (or I guess three if it's rollups with many inputs). But that's the overall gist of it.

What's really cool is that ustep is super simple without sacrificing which programs we can run on a rollup. Additionally, we can improve bigarch (e.g. adding more extensions, optimizing code) without having to change Solidity ustep.

Addendum: Extending to bare-metal execution

There's an extra level of swap we can add above the big machine: bare-metal execution. Although it must be done with care. Suppose we coded a deterministic program. We could compile it to bigarch and to bare-metal (say, x86). Then we normally only run on bare-metal, and start turning on the other machines when there's a dispute. However, we need to slightly change the way the machine works; the big-machine has to be lambda-like, with its own pristine state, mirroring the micro-machine.

---

Here's a different way to see this technique. In any case, I hope this was useful.

Cheers!