runtimeverification / runtimeverification/kontrol

Instructions for running Kontrol's JSON RPC server

Open
#695 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

documentation
Dominant language
Python
Stars
122
Forks
16
PR merge metrics
No merged PRs in 30d

Description

Running Kontrol's JSON RPC server:

  1. Clone Kontrol's repo and switch to the kontrol-vm branch;

  2. Run the normal setup commands for Kontrol as seen in the README file of the repo;

  3. To run the kontrol vm module in the debugger mode, you can:
    3.1 Open Kontrol's folder in VSCode;
    3.2 Go to the “Run and Debug” window of VSCode's sidebar;
    3.3 Click on “create a launch.json file” hyperlink below the “Run and Debug” button;
    3.4 Select a Python debugger;
    3.5 VSCode should open a newly created launch.json file. Paste the following content into it:

     {
         "version": "0.2.0",
         "configurations": [
         
             {
                 "name": "Python Debugger: Module",
                 "type": "debugpy",
                 "request": "launch",
                 "justMyCode": false,
                 "module": "kontrol",
                 "args": ["vm"],
                 "cwd": "${workspaceFolder}"
             }
         ]
     }
    

    3.6 Alternatively, you can run poetry run kontrol vm on your terminal, but this will not include the debugger features of VSCode.

  4. On the “Run and Debug” window, click the “play” button on “Python Debugger”. The Kontrol JSON RPC server should be executed now;

  5. To place the #kontrol_requestValue production (sample production for testing) into the K cell and run the rewriting operations (executing exec_request_value), run this curl request in a terminal:

curl -X POST 127.0.0.1:8081 -H 'Content-Type: application/json' -d '{
    "jsonrpc": "2.0",
    "method": "kontrol_requestValue",
    "params": [],
    "id": 0
}'

A sample execution of a transaction can be triggered with the following curl request:

curl -X POST 127.0.0.1:8081 -H 'Content-Type: application/json' -d '{
  "jsonrpc": "2.0",
  "method": "eth_sendTransaction", 
  "params": [{
        "from": "0x06a85356dcb5b307096726fb86a78c59d38e08ee",
        "to": "0x911392821a6b8a3e0bd8078fc7403e04c3ad2416",
        "gas": "0x76c0",
        "gasPrice": "0x9184e72a000",
        "value": "0x9184e72a",
        "data": "0x00"
        }],
  "id": 0
}'

If this is the first executed transaction in the VM, it should return the 0xa5662e60a8915c2e260f3a3707273d7d7c66efb5335e65f901a620b9cd297790 transaction hash, which can be used to fetch the data of the transaction with the following request:

curl -X POST 127.0.0.1:8081 -H 'Content-Type: application/json' -d '{
  "jsonrpc": "2.0",
  "method": "eth_getTransactionByHash", 
  "params": ["0xa5662e60a8915c2e260f3a3707273d7d7c66efb5335e65f901a620b9cd297790"],
  "id": 0
}'

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.

Research direction

Start with the repository README and its existing Kontrol setup instructions, then verify the kontrol vm debugger flow and the JSON-RPC curl examples described here. Done means the repository contains clear, reproducible instructions for starting the server, sending the sample requests, and fetching the transaction.

Written by the indexing model from the issue text.

Assessment

Tech stack
python
Domain
documentation
Issue type
Documentation
Difficulty
2/5
Estimated time
1-3 hours
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
48/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.