Machine Swapping and Micro Architecture technique

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`](https://esolangs.org/wiki/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](https://ethresear.ch/t/machine-swapping/14159) a different way to see this technique. In any case, I hope this was useful.

Cheers!