runtimeverification / runtimeverification/kontrol
Instructions for running Kontrol's JSON RPC server
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
Running Kontrol's JSON RPC server:
-
Clone Kontrol's repo and switch to the
kontrol-vmbranch; -
Run the normal setup commands for Kontrol as seen in the README file of the repo;
-
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 vmon your terminal, but this will not include the debugger features of VSCode. -
On the “Run and Debug” window, click the “play” button on “Python Debugger”. The Kontrol JSON RPC server should be executed now;
-
To place the
#kontrol_requestValueproduction (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
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.
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