runtimeverification / runtimeverification/kontrol
Factor out JSON RPC client from Firefly
Open
Nobody has claimed this yet.
enhancement
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
Blocked on: https://github.com/runtimeverification/pyk/issues/1019
Blocked on: https://github.com/runtimeverification/kontrol/issues/454
The tool https://github.com/runtimeverification/firefly has a JSON RPC server (ethereum client) built into KEVM. At the time, it was used for concrete execution only (specifically for advanced coverage measurement), but now that we use an RPC server for interacting with symbolic backends, we could also do symbolic execution with it.
Steps could be:
- Pull out JSON-RPC K modules into its own repository and have its own tests. Or as a part of the K prelude?
- Include JSON-RPC module into Kontrol, and pull over the implementation of the Eth RPC calls into Kontrol. Implement
kontrol client ...command (like Anvil for Kontrol), or just callfirefly ...still. - Enable symbolic execution over this RPC interface as well.
- Connect Simbolik DAP to this RPC interface as well (in addition to connecting it to Foundry).
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.