runtimeverification / runtimeverification/kontrol

Integrate symbolic storage generation script into a Kontrol command

Open
#905 0 comments 0 reactions 1 assignee View on GitHub

@palinatolmach is already working on this.

Since Aug 26, 2025.

enhancement
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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.