Crosscut

The simple approach to expression-level rewind, implementing it in the runtime, is pretty straight-forward: On every bytecode instruction the runtime executes, it also logs "undo instructions" into an "undo buffer". If executed, those will undo the original instruction. Rewinding just takes instructions out of that undo buffer and executes them.

But what specifically are these undo instructions? They could just be regular instructions. For example, let's look at the expression 1 2 +. Under the hood, this would translate into the following instructions:

1. push 1
2. push 2
3. add

To undo a "push" instruction, we'd just need to remove the value that was pushed. So after executing instructions 1 and 2, the undo buffer would contain "pop, pop". This is an easy case, because every push x instruction would be undone by pop, regardless of what x is.

The add is a bit more complicated. We need to know about its inputs and outputs to undo it. But since we're talking about doing this at runtime, we have all that information. We can undo the add with something like pop (to remove the output), push 1, push 2 (to reconstruct the inputs).