Factor out JSON RPC client from Firefly

ehildenb commented 6 months ago

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 call firefly ... 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).

palinatolmach commented 4 months ago

@ACassimiro I've assigned you to this issue since I've heard you're working on making Kontrol work with the JSON-RPC server — please let me know if not :).

ACassimiro commented 4 months ago

@palinatolmach I am. I'll be creating a branch with the progress that we've had with it so far.

ACassimiro commented 4 months ago

The JSON RPC functionalities are being added to Kontrol under the option vm, and this is actively being developed under the Kontrol-VM branch.

@palinatolmach do we want to keep this issue open until the branch is eventually merged?

runtimeverification / kontrol

Factor out JSON RPC client from Firefly #446