runtimeverification / runtimeverification/kontrol
Integrate symbolic storage generation script into a Kontrol command
@palinatolmach is already working on this.
Since Aug 26, 2025.
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
We should integrate the symbolic storage generation functionality developed by @lucasmt into Kontrol as a separate command.
Specifically, this python script reads the storage layout of a contract in JSON format and automatically generates a Solidity file with constants indicating the storage slot and offset for each storage variable. The files it generates look like this, and this shell script exemplifies how to use it.
This is very useful when we need to setup the contract storage with symbolic variables and other cases where we need to use the load and store cheatcodes, because it means that instead of hardcoding the slots and offsets we can just use the constants, and if the storage layout changes and variables get moved around, we just need to re-run the script to update the values.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.