Procedure locals, memory, and how they interact with the execution trace/proof

[bitwalker]

One of the things that has come up while I'm digging in to some of the details of the VM is why there is a distinction between the memory for procedure locals and everything else, since they live in the same address space (although conceptually that address space is segmented into reserved and unreserved segments). Perhaps more specifically, why is the memory for locals not managed using a more typical call frame scheme?

In my mind, there are two "standard" ways of handling stack memory:

1. Each new execution context (e.g. thread in a typical program) allocates some predetermined amount of memory from the global heap, and then each call in that context dynamically allocates out of that region as needed. Attempting to allocate beyond the boundaries of that region constitutes a stack overflow, though how such failures are handled can vary.
2. The Harvard architecture approach, seen in Wasm for example, where stack memory is completely separate from other memory, perhaps with a limited subset of operations supported. For example, in Wasm, the details of the call stack are managed by the host and cannot be directly manipulated from Wasm, i.e. there is no "stack pointer" to manipulate, and you can't access/modify anything in the current frame, beyond loading/storing values to locals declared in the current function. Under the covers of course, Wasm hosts might use a typical stack layout and calling convention, but that's all implementation detail. Wasm does at least provide instructions which let you control stack usage to some extent (e.g. return_call for tail calls), but it is very limited.

In both these approaches, the maximum amount of memory usage is determined by some combination of the depth of the call stack + size of the frames at that depth.

In Miden however, it seems like memory for all of the call frames is conceptually allocated up front, which seems wasteful. Particularly since one of the benefits of the MAST representation (AIUI) allows you to avoid paying the cost for parts of the program not executed. My assumption is that a more typical scheme, by virtue of reduced memory usage, would also reduce the size of the resulting trace/proofs, but I'm still not clear on the interaction between memory and proof size in Miden yet, so maybe memory usage has no impact there. Perhaps it is only the volume of reads/writes which affect the trace/proof size?

Putting aside the memory usage aspect, an additional benefit of a more traditional stack management scheme (at least internally in the VM) is that you get stack traces basically for free (something we don't currently get in MASM today, and which is probably difficult, if not impossible, to implement without some kind of adjacent call stack structure anyway).

I have some additional questions, but I'll post those in separate threads 🙂

[bobbinth]

Perhaps more specifically, why is the memory for locals not managed using a more typical call frame scheme?

The answer here is that we went with something that was fairly simple and efficient to support from ZKP standpoint (i.e., to describe using AIR constraints). We didn't pick the simplest approach (the simplest would have been contiguous write-once memory similar to the one used in Cairo), but we also didn't go too far from the simplest approach. There is an overview of other potential approaches here.

In Miden however, it seems like memory for all of the call frames is conceptually allocated up front, which seems wasteful. ... Perhaps it is only the volume of reads/writes which affect the trace/proof size?

Yes, none of the memory is actually allocated until it is written to or read from - so, total amount of memory doesn't really matters. What adds cost is the number of reads and writes to memory. For every read/write, the VM creates an entry in the memory trace table (i.e., here) - and this is what impacts the overall VM trace size.

Putting aside the memory usage aspect, an additional benefit of a more traditional stack management scheme (at least internally in the VM) is that you get stack traces basically for free (something we don't currently get in MASM today, and which is probably difficult, if not impossible, to implement without some kind of adjacent call stack structure anyway).

It is possible to implement more traditional stack management scheme (I think Triton VM is doing something like that) but it does require that the VM manage two stacks separately. I actually don't think stack traces would be too difficult for us to implement once we have proper source-code mappings.