wilfredta/symbolic-stack-machines

Library for building symbolically executable stack-based virtual machines

symbolic-stack-machines's Issues

Enable partitioning of memory by address range & assigning permission to partitions

Represent symbolic values & operations w/ in-memory "IR" for translation to z3-rs or smtlib2 formt

Support BitVector's for Memory & Stack Values

Add storage module to optionally mixin

Enable optional symbolic length & content for VM code for dynamic-sized constructor args & immutables in EVM

Support abstract context-switch operation in BaseMachine

Make Extension Environment Generic

In a previous version of symbolic-stack-machines (SSM), each modular component (memory, stack, etc) were all generic over Instruction. The idea was to use Rust's type system to configure the machine's behavior. This turned out to be detrimental to the library's ease of use & ergonomics more specifically.

While climbing out of the so-called "generics-hell", we realized that most of the generics in various components were due to being generic over the type of values stored in the stack, memory, storage, etc. Thus, we created a universal value type that is lazily evaluated; the universal value is actually an AST.

We also introduced a Configuration object for each modular component (StackConfig, MemConfig, etc). These config objects are meant to receive hooks which can be passed to the universal value's AST interpreter. This allows us to treat the universal value in Rust's type system as a single type (thereby drastically simplifying the library's API), while also allowing various components to customize the semantics of that type and specialize it to whichever type is relevant for that component. In other words, it gives us polymorphism across different components as well as polymorphism across different values within a particular component, since the hooks passed to the universal value's interpreter can conditionally evaluate the value as a different type based on the component's state.

The only component that does in fact need to be generic is the ExtEnv. This is because it is meant to be a catch all extension mechanism for implementing symbolic machines with more components, as well as those with bespoke features (e.g., the concept of "gas" in the EVM). Notably, the ExtEnv can also be leveraged to construct register-based machines. The crucial difference between the extension environment component and other components is that it does not have a predefined structure. While other components are well defined though generic over the relevant values on which they operate (a memory is treated as a flat array with some index set and value set; a stack is an abstract data type with API to push, pop, and peek), the ExtEnv has no predefined API nor structural constraints. Thus, we should re-introduce generics to the definition of this component.

Add custom mutable context for handling niche, VM-data