Improved support for Dave in the Cartesi Machine

The Cartesi Machine was original designed as a computational oracle supporting arbitration via the “verification game” algorithm by Canetti et al. 2013. The result is that the emulator was expected to efficiently produce a state hash for a small number of points during the computation (logarithmic on the number of cycles in the computation).

Dave, our new family of dispute resolution algorithms, work in a different way. The emulator is now expected to generate state hashes much more frequently. In fact, it will be expected to generate a new state hash after every microcycle within a range of cycles that we want to make as long as performance allows.

The state-hash update mechanism has been optimized for the “verification game” scenario. The new use pattern would benefit from a variety of changes to this mechanism. The description of all such optimizations is outside the scope of this document, but there are two changes that can be more concisely described.

The first change concerns the way in which the “microarchitecture shadow state” is updated in the state hash. The shadow state is the part of the state that changes most frequently. It includes the microarchitecture cycle counter, the program counter, and its registers. When state-hash updates are infrequent, it makes sense to assume most of this state will need to be updated and simply rehash it in its entirety. However, once state hashes are updated after every microcycle, it makes sense to track the individual words that were modified and update only those. It is likely that this change can make the state-hash update much more efficient.

The second change concerns the layout of the state Merkle tree. In the current implementation, the state Merkle tree is fully balanced. This means that every word in the state is at the same depth (i.e., 61 nodes deep). When state-hashes are updated very frequently, it makes sense to unbalance the tree so that the most frequently-used words are at shallower depths, so they can be updated more efficiently. There are many, many strategies for optimizing the tree for this purpose. However, considerations specific to our project (support for generation of proofs, for updates of entire subtrees etc, required implementation in Solidity) significantly reduce the design space. We believe we have come up with a static tree layout that should capture most of the benefit of more complex approaches. It should also make state-hash update much more efficient, on average.


I was a bit confused here. I expected you to say “as short as performance allows”, in the sense that we’d like to generate state hashes as frequently as possible (or maybe I’m lost and that’s not the goal, hehe)