Skip to content

runtimeverification/skribe

Repository files navigation

skribe

Installation

Prerequsites: python >= 3.10, pip >= 20.0.2, poetry >= 1.3.2.

make build
pip install dist/*.whl

skribe-simulation

skribe-simulation is a CLI tool for simulating Stylus smart contracts.

Test cases are written in JSON as sequences of steps that:

  • Deploy contracts
  • Call functions
  • Check expected results

Here is an example test case:

{
  "steps": [
      {
          "type": "setExitCode", "value": 1
      },
      {
          "type": "setStylusContract",
          "id": 1,
          "code": "path/to/contract.wasm"
      },
      {
          "type": "callStylus",
          "to": 1,
          "data": {
              "function": "number", "types": [], "args": []
          },
          "output": {
              "type": "uint256",
              "value": 1
          },
          "value": 0
      },
      {
          "type": "setExitCode", "value": 0
      }
  ]
}

This scenario:

  1. Sets the status code to 1 (indicating failure if the simulation doesn't finish),
  2. Deploys a Stylus contract from a WASM file,
  3. Calls the number() function on the contract and checks the output is 1,
  4. Resets the expected exit code to 0 (indicating success).

Under the hood, JSON scenarios are translated to K terms and executed using Stylus formal semantics via krun. For debugging purposes, you can use skribe-simulation to generate an initial configuration term in Kore format and execute it with krun:

skribe-simulation run path/to/test.json --depth 0 > initial-state.kore
krun --definition $(kdist which stylus-semantics.llvm) initial-state.kore --parser cat --term

For Developers

Use make to run common tasks (see the Makefile for a complete list of available targets).

  • make build: Build wheel
  • make check: Check code style
  • make format: Format code
  • make test-unit: Run unit tests

For interactive use, spawn a shell with poetry shell (after poetry install), then run an interpreter.

About

Property testing for Stylus smart contracts

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •