KLab

概要

https://gyazo.com/57c3742f6bb6561ce789c006d6a02fed

Dapphubが作った、KEVMでコントラクトの形式的検証をするときのGUI

K proverの実行トレースを対話的に読める

DSL of KLab

eDSLっぽい

操作方法

Installation of KLab

code: shell

== kompile: .build/java/driver-kompiled/timestamp

/Users/nrryuya1/work/blockchain/k/klab/evm-semantics/.build/k/k-distribution/target/release/k/bin/kompile --debug --main-module ETHEREUM-SIMULATION --backend java \

--syntax-module ETHEREUM-SIMULATION .build/java/driver.k --directory .build/java -I .build/java

at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:99)

at org.kframework.utils.errorsystem.KEMException.compilerError(KEMException.java:61)

at org.kframework.kompile.DefinitionParsing.throwExceptionIfThereAreErrors(DefinitionParsing.java:173)

at org.kframework.kompile.DefinitionParsing.resolveConfigBubbles(DefinitionParsing.java:231)

at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:163)

at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:123)

at org.kframework.kompile.Kompile.run(Kompile.java:107)

at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)

at org.kframework.main.FrontEnd.main(FrontEnd.java:53)

at org.kframework.main.Main.runApplication(Main.java:114)

at org.kframework.main.Main.runApplication(Main.java:104)

at org.kframework.main.Main.main(Main.java:53)

十分以上かかった

examples

Klabのリポジトリ内のexampleコントラクトでklabを使ってみる

code: shell

docker exec -it klab bash

root@cc8016d1264a:/klab# cd /docker/examples/SafeAdd

root@cc8016d1264a:/docker/examples/SafeAdd# klab build

root@cc8016d1264a:/docker/examples/SafeAdd# klab run --spec out/specs/proof-SafeAdd_add_succ.k

k-dss(MakerDAO)

マルチコラテラルの仕組みを導入したバージョンアップを行った際、KEVMを使って形式的検証を行った

MakerDAO開発元のDapphubが独自で(?)行い、そのさいにKlabを開発した模様