This is a template repo and list of resources for those interested in getting started specifying smart contracts with klab
.
klab is a smart contract specification language and proof explorer. A Klab spec can be thought of as an extremely thorough test suite that can be run against any evm bytecode.
Using klab we can show:
- The spec covers every possible execution (is exhaustive)
- All specified behaviours hold for every possible execution
- Clone the klab repo (
git@github.com:dapphub/klab.git
) - From the repo root run
nix-shell
- Run
make deps
- Run
make deps-haskell
- Klab is now available in your path
In future when you need to use klab you can go to the repo root, run nix-shell
and you will be
dropped into a shell with klab
available on PATH
.
- Read the documentation on the spec format
- Play around with the examples
- Watch @mrchico's talk
- Look at the keybindings
- Work through the DevCon4 workshop: problems, solutions
This repo uses dapp
to handle
solidity related tasks. You can build with dapp build
and run tests with dapp test
.
- Open
spec/spec.act.md
and start writing your spec - Ensure that the mapping from specs to implementations in
config.json
is up to date - Build the k expressions (
klab build
)
- Run
klab prove --dump <path_to_spec.k>
- Run
klab prove-all
- Run
klab debug $(klab hash <path_to_spec.k>)