At the moment, Scilla interpreter has the gas-monad hard coded, and the set of its effects is not extensible to track, e.g., state-collecting semantics. This proposal suggest to generalise the state monad to account for multiple ways to do state-tracking:
state-collecting semantics
trace-collecting semantics
abstract monadic interpreters
As the type-safe embedding is not possible to do in a type-safe way the framework (due to the nature of literals that have to be monomorphic), we are going to rely on the in-place module substitution during the building phase via dune facilities, namely the Virtual libraries & variants feature, which lets one to compile parameterized libraries and delay the selection of concrete implementations until linking an executable.
At the moment, Scilla interpreter has the gas-monad hard coded, and the set of its effects is not extensible to track, e.g., state-collecting semantics. This proposal suggest to generalise the state monad to account for multiple ways to do state-tracking:
As the type-safe embedding is not possible to do in a type-safe way the framework (due to the nature of literals that have to be monomorphic), we are going to rely on the in-place module substitution during the building phase via
dune
facilities, namely the Virtual libraries & variants feature, which lets one to compile parameterized libraries and delay the selection of concrete implementations until linking an executable.