diff --git a/.gitignore b/.gitignore index 7eb9a7436d..f204c457b0 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ /src /package/pkg /package/src +/media/*.pdf diff --git a/Jenkinsfile b/Jenkinsfile index 7b8653ed00..f3ef802e7b 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -73,7 +73,7 @@ pipeline { sh ''' nprocs=$(nproc) [ "$nprocs" -gt '6' ] && nprocs='6' - make test-proof -j"$nprocs" + make test-prove -j"$nprocs" ''' } } diff --git a/Makefile b/Makefile index 342a50d488..a66ecf3bb4 100644 --- a/Makefile +++ b/Makefile @@ -40,7 +40,7 @@ export LUA_PATH defn java-defn ocaml-defn node-defn haskell-defn llvm-defn \ test test-all test-conformance test-slow-conformance test-all-conformance \ test-vm test-slow-vm test-all-vm test-bchain test-slow-bchain test-all-bchain \ - test-proof test-klab-prove test-parse test-failure \ + test-prove test-klab-prove test-parse test-failure \ test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search test-interactive-firefly \ media media-pdf sphinx metropolis-theme .SECONDARY: @@ -448,7 +448,7 @@ test-bchain: $(quick_bchain_tests:=.run) proof_specs_dir:=tests/specs proof_tests=$(wildcard $(proof_specs_dir)/*/*-spec.k) -test-proof: $(proof_tests:=.prove) +test-prove: $(test_prove_specs:=.prove) test-klab-prove: $(smoke_tests_prove:=.klab-prove) # Parse Tests @@ -497,7 +497,10 @@ media: sphinx media-pdf ### Media generated PDFs -media_pdfs:=201710-presentation-devcon3 201801-presentation-csf +media_pdfs := 201710-presentation-devcon3 \ + 201801-presentation-csf \ + 201905-exercise-k-workshop \ + 201908-trufflecon-workshop 201908-trufflecon-firefly media/%.pdf: media/%.md media/citations.md @echo "== media: $@" diff --git a/README.md b/README.md index 47f28804e5..bf3b059650 100644 --- a/README.md +++ b/README.md @@ -98,7 +98,7 @@ git submodule update --init --recursive If you haven't already setup K's OCaml dependencies more recently than February 1, 2019, then you also need to setup the K OCaml dependencies: ```sh -./.build/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev +./deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev ``` Finally, you can install repository specific dependencies and build the semantics: @@ -146,7 +146,7 @@ On Arch, you'll also need `crypto++` package. And you need to setup Rust: ```sh -.build/k/llvm-backend/src/main/native/llvm-backend/install-rust +./deps/k/llvm-backend/src/main/native/llvm-backend/install-rust ``` Additionally, you need to setup the remaining LLVM dependencies. diff --git a/kevm b/kevm index 610153b04d..04416bbb22 100755 --- a/kevm +++ b/kevm @@ -5,7 +5,7 @@ shopt -s extglob kevm_dir="${KEVM_DIR:-.}" build_dir="$kevm_dir/.build" -defn_dir="$build_dir/defn" +defn_dir="${KEVM_DEFN_DIR:-$build_dir/defn}" lib_dir="$build_dir/local/lib" k_release_dir="${K_RELEASE:-$kevm_dir/deps/k/k-distribution/target/release/k}" diff --git a/media/201905-exercise-k-workshop.md b/media/201905-exercise-k-workshop.md new file mode 100644 index 0000000000..7976f95eab --- /dev/null +++ b/media/201905-exercise-k-workshop.md @@ -0,0 +1,142 @@ +--- +title: 'K Workshop' +subtitle: 'Understanding the K Prover' +author: +- Everett Hildenbrandt +institute: +- Runtime Verification +- ConsenSys +date: '\today' +theme: metropolis +fontsize: 8pt +--- + +Overview +-------- + +- Install KEVM and KLab on your machine +- Simple uses of the `./kevm` script +- (Brief) introduction to KEVM +- Verification examples: KEVM lemma proofs, ERC20 `transfer` function +- Open verification challenge + +Install KEVM +------------ + +### KEVM + +- Branch `kevm-lemmas` of KEVM: +- Build instructions in README. + + ```sh + make deps + make build-java + make build-ocaml + ``` + +- Should be able to run: + + ```sh + make test-prove-verified + make test-prove-gen -j3 + ``` + +. . . + +### KLab + +- Branch `master` of KLab: +- Build instructions in README. + + ```sh + make deps-npm + ``` + +- Should be able to run (in KEVM repo with `klab/bin` on your `PATH`): + + ```sh + make tests/specs/verified/kevm-lemmas-spec.k + ./kevm klab-prove tests/specs/verified/kevm-lemmas-spec.k --boundary-cells k,pc + ``` + +`./kevm help` +------------- + +```sh +$ ./kevm help + +usage: ./kevm (run|kast) [--backend (ocaml|java|llvm|haskell)] * + ./kevm interpret [--backend (ocaml|llvm)] + ./kevm prove [--backend (java|haskell)] * + ./kevm klab-(run|prove) * + + ./kevm run : Run a single EVM program + ./kevm interpret : Run JSON EVM programs without K Frontend (external parser) + ./kevm prove : Run an EVM K proof + ./kevm klab-(run|prove) : Run or prove a spec and launch KLab on the execution graph. + + Note: is a path to a file containing an EVM program/test. + is a K specification to be proved. + are any arguments you want to pass to K when executing/proving. + + KLab: Make sure that the 'klab/bin' directory is on your PATH to use this option. +``` + +`./kevm` examples +----------------- + +> - Run a test: `MODE=... SCHEDULE=... ./kevm run tests/etheremu-tests/...` +> - Interpret a test (fast): `MODE=... SCHEDULE=... ./kevm interpret tests/etheremu-tests/...` +> - Run a proof: `./kevm prove tests/specs/*-spec.k` +> - Run a test under KLab: `MODE=... SCHEDULE=... ./kevm klab-run tests/ethereum-tests/...` +> - Run a proof under KLab: `./kevm klab-prove tests/ethereum-tests/...` + +Introduction to KEVM +-------------------- + +- File [data.md](../data.md) defines data-structures of EVM. +- File [evm.md](../evm.md) defines the semantics itself. +- File [driver.md](../driver.md) defines the testing harness. +- File [edsl.md](../edsl.md) defines a DSL for aiding specification for proofs. + +Verification Examples +--------------------- + +### KEVM Lemmas + +- File [kevm-lemmas-spec.md](../kevm-lemmas-spec.k) +- Summaries of the "positive" cases of arithmetic opcodes and push +- Work through how to use KLab to discover preconditions +- Complete the push, push, add specification + +```sh +make test-prove-verified +``` + +. . . + +### ERC20 `transfer` functions + +- Run proof. + + ```sh + make test-prove-gen + ``` + +- Explain ini file format of [ds-token-erc20-spec.ini](../tests/specs/ds-token-erc20/ds-token-erc20-spec.ini) +- Delete all except the `transfer` blocks +- Remove `requires` clauses to explore result in KLab + +Open Verification Challenge +--------------------------- + +Rest of time. + +- Work on `transferFrom` function? +- Try to setup your own contract? + +Thanks! +------- + +- ConsenSys for hosting us! +- You all for attending! diff --git a/media/201908-trufflecon-firefly.md b/media/201908-trufflecon-firefly.md new file mode 100644 index 0000000000..20768ded3b --- /dev/null +++ b/media/201908-trufflecon-firefly.md @@ -0,0 +1,180 @@ +--- +title: 'Firefly' +subtitle: 'Solidity testing using KEVM' +author: +- Everett Hildenbrandt +- Grigore Rosu +institute: +- Runtime Verification +date: '\today' +theme: metropolis +fontsize: 8pt +--- + +Overview +-------- + +- (Brief) Introduction to KEVM +- Introduction to Firefly +- Firefly Demo +- Future Directions + +(Brief) Introduction to KEVM +---------------------------- + +- Repository: +- Considered the canonical spec of EVM: +- All K tooling is derived automatically: + - Reference EVM interpreter + - Symbolic execution engine + - EVM bytecode formal verification engine + - Several EVM bytecode debugger options + +Introduction to Firefly +----------------------- + +- `npm` package here: . +- Drop-in replacement for `ganache-cli`, can be used directly by Truffle. + + Instead of: + + ```sh + npx ganache-cli + ``` + + run: + + ```sh + npx kevm-ganache-cli + ``` + +. . . + +### Why?? + +- Higher confidence in results (run tests with both!). +- More features to come: + - Test coverage metrics. + - Automated property verification. + - Test generation. + - Contract symbolic execution. + - ... your ideas?? + +Firefly Demo - Setup +-------------------- + +Instructions from : + +. . . + +### Install KEVM (once) + +**TODO**: Update release URL. + +```sh +sudo apt install nodejs npm curl git +curl --location 'https://github.com/kframework/evm-semantics/releases/download/v1.0.0-a47e4b2/kevm_1.0.0_amd64.deb' \ + --output kevm_1.0.0_amd64.deb +sudo apt install ./kevm_1.0.0_amd64.deb +``` + +. . . + +### Install `npx` (once) + +```sh +sudo npm install -g npx +``` + +Firefly Demo - Run OpenZeppelin Tests +------------------------------------- + +### Start `kevm-ganache-cli` + +```sh +npx kevm-ganache-cli \ + --gasLimit 0xfffffffffff \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501200,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501201,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501202,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501203,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501204,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501205,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501206,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501207,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501208,1000000000000000000000000" \ + --account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501209,1000000000000000000000000" +``` + +. . . + +### Run OpenZeppelin tests + +```sh +git clone 'https://github.com/OpenZeppelin/openzeppelin-contracts.git' +cd openzeppelin-contracts +git checkout b8c8308 +npm install +npx truffle test test/token/ERC20/ERC20.test.js +``` + +KEVM Extensions - Event Monitoring +---------------------------------- + +Compile semantics with additional file `media/201908-trufflecon/kevm-ltl.md`. + +```k + syntax LTLEvent ::= "overflow" + // ------------------------------ + rule ADD W0 W1 ... + EVENTS (.Set => SetItem(overflow)) + requires notBool overflow in EVENTS + andBool W0 +Word W1 =/=Int W0 +Int W1 + [priority(24)] + + syntax LTLEvent ::= "revert" + // ---------------------------- + rule REVERT _ _ ... + EVENTS (.Set => SetItem(revert)) + requires notBool revert in EVENTS + [priority(24)] +``` + +- Monitors built-in to the KEVM semantics as an extension. +- Can build arbitrary LTL formula over the monitors. + +KEVM Extensions - LTL Model Checking +------------------------------------ + +### Input file `addition.evm` + +```evm +load { "gas" : 10000000 + // Query: always ((~ overflow) \/ eventually revert) + // , "code" : UNSAFEADD(100 , 100) // True + // , "code" : UNSAFEADD(maxUInt256 , 100) // False + // , "code" : SAFEADD(100 , 100) // True + , "code" : SAFEADD(maxUInt256 , 100) // True + } + +start +``` + +. . . + +### Query + +```sh +./kevm run --backend llvm media/201908-trufflecon/addition.evm -cLTLFORMULA='always (overflow -> eventually revert)' +``` + +Truffle Firefly Plugin +---------------------- + +- Developed with help from Truffle devs today as plugin! +- Modified OpenZeppelin test-suite which links to `truffle-plugin-firefly`. + +```sh +npx truffle run firefly SafeMath 'always (overflow -> eventually revert)' +``` + diff --git a/media/201908-trufflecon-workshop.md b/media/201908-trufflecon-workshop.md new file mode 100644 index 0000000000..0e65694486 --- /dev/null +++ b/media/201908-trufflecon-workshop.md @@ -0,0 +1,190 @@ +--- +title: 'K/KEVM Formal Verification Workshop' +subtitle: 'Understanding the K Prover and Runtime Verification' +author: +- Everett Hildenbrandt +- Grigore Rosu +institute: +- Runtime Verification +date: '\today' +theme: metropolis +fontsize: 8pt +--- + +Overview +-------- + +- Install KEVM and KLab on your machine +- Simple uses of the `./kevm` script +- (Brief) introduction to KEVM +- Verification examples: Single opcode (`ADD`), ERC20 `transfer` function +- LTL runtime verification example + +Install KEVM: Docker Way +------------------------ + +### Get Docker Container + +```sh +docker login +# it will ask for username and password +# email will NOT work, they need their dockerhub USERNAME +# Proxy user: ehildenbproxy +# Proxy pass: ehildenb-proxy + +docker run -it -u user -w /home/user/evm-semantics \ + runtimeverificationinc/evm-semantics:trufflecon +``` + +### Setup Environment + +```sh +cd ../ +eval $(cat env) +cd evm-semantics +which klab +``` + +Install KEVM: From Source +------------------------- + +### KEVM + +- Branch `trufflecon` of KEVM: +- Build instructions in README. + + ```sh + make llvm-deps + make build-java + ``` + +. . . + +### KLab + +- Branch `master` of KLab: +- Build instructions in README. + + ```sh + make deps-npm + ``` + +- Patch KLab (comment lines 90 - 94 of `lib/behavior.js`). +- Should be able to run (in KEVM repo with `klab/bin` on your `PATH`): + + ```sh + ./kevm klab-prove add-spec.k + ./kevm klab-view add-spec.k + ``` + +`./kevm help` +------------- + +```sh +usage: ./kevm run [--backend (ocaml|java|llvm|haskell)] * + ./kevm interpret [--backend (ocaml|llvm)] * + ./kevm kast [--backend (ocaml|java)] * + ./kevm prove [--backend (java|haskell)] * -m + ./kevm search [--backend (java|haskell)] * + ./kevm klab-run * + ./kevm klab-prove * -m + ./kevm klab-view + + ./kevm run : Run a single EVM program + ./kevm interpret : Run JSON EVM programs without K Frontend (external parser) + ./kevm kast : Parse an EVM program and output it in a supported format + ./kevm prove : Run an EVM K proof + ./kevm search : Search for a K pattern in an EVM program execution + ./kevm klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read + ./kevm klab-view : View the statelog associated with a given program or spec + + Note: is a path to a file containing an EVM program/test. + is a K specification to be proved. + is an argument you want to pass to K. + is an argument you want to pass to the derived interpreter. + is the format for Kast to output the term in. + is the configuration pattern to search for. + is the module to take as axioms when doing verification. + + klab-view: Make sure that the 'klab/bin' directory is on your PATH to use this option. +``` + +`./kevm` examples +----------------- + +- Run a test: `./kevm run tests/etheremu-tests/...` +- Interpret a test (fast): `./kevm interpret tests/etheremu-tests/...` +- Run a proof: `./kevm prove tests/specs/*-spec.k` +- Run a test under KLab: `./kevm klab-run tests/ethereum-tests/...` +- Run a proof under KLab: `./kevm klab-prove tests/ethereum-tests/...` + +- Environment variables `MODE` and `SCHEDULE` control how KEVM executes. +- `MODE` can be `NORMAL` or `VMTESTS`. +- `SCHEDULE` can be `DEFAULT`, `FRONTIER`, `HOMESTEAD`, `TANGERINE_WHISTLE`, `SPURIOUS_DRAGON`, `BYZANTIUM`, `CONSTANTINOPLE`, or `PETERSBURG`. + +Introduction to KEVM +-------------------- + +- [data.md](../data.md) defines data-structures of EVM. +- [network.md](../network.md) defines the EVMC status codes. +- [evm.md](../evm.md) defines the semantics itself. +- [driver.md](../driver.md) defines the testing harness. +- [edsl.md](../edsl.md) defines a DSL for aiding specification for proofs. +- [evm-node.md](../evm-node.md) defines the protobuf interface to use KEVM over RPC. + +Understanding the K Prover: Single Opcode +----------------------------------------- + +File `add-spec.k`: + +```k +requires "evm.k" + +module ADD-SPEC + imports EVM + + rule #next [ ADD ] => . ... + SCHEDULE + W0 : W1 : WS => chop(W0 +Int W1) : WS + PCOUNT => PCOUNT +Int 1 + G => G -Int Gverylow < SCHEDULE > + requires G >=Int Gverylow < SCHEDULE > + andBool notBool ( #stackUnderflow ( W0 : W1 : WS , ADD ) + orBool #stackOverflow ( W0 : W1 : WS , ADD ) + ) +endmodule +``` + +. . . + +- `./kevm prove add-spec.k --def-module EVM` +- `./kevm klab-prove add-spec.k --def-module EVM` +- `./kevm klab-view add-spec.k --def-module EVM` + +. . . + +- Try with side-conditions removed. + +LTL Runtime Verification +------------------------ + +- Compile semantics with `media/201908-trufflecon/kevm-ltl.md`, which instruments semantics (*without* modifying it). +- Build definition: + + ```sh + cp media/201908-trufflecon/kevm-ltl.md kevm-ltl.md + make MAIN_MODULE=KEVM-LTL MAIN_DEFN_FILE=kevm-ltl build-llvm + ``` + +- Try verifying a property: + + ```sh + ./kevm run --backend llvm media/201908-trufflecon/addition.evm -cLTLFORMULA='eventually revert' + ./kevm run --backend llvm media/201908-trufflecon/addition.evm -cLTLFORMULA='always ((~ overflow) \/ eventually revert)' + ``` + +Thanks! +------- + +- TruffleCon for hosting us! +- You all for attending! diff --git a/media/201908-trufflecon/add-gas-spec.k b/media/201908-trufflecon/add-gas-spec.k new file mode 100644 index 0000000000..f72dcaebf9 --- /dev/null +++ b/media/201908-trufflecon/add-gas-spec.k @@ -0,0 +1,14 @@ +requires "evm.k" + +module ADD-GAS-SPEC + imports EVM + + rule #next [ ADD ] => . ... + SCHEDULE + W0 : W1 : WS => chop(W0 +Int W1) : WS + PCOUNT => PCOUNT +Int 1 + G => G -Int Gverylow < SCHEDULE > + requires notBool ( #stackUnderflow ( W0 : W1 : WS , ADD ) + orBool #stackOverflow ( W0 : W1 : WS , ADD ) + ) +endmodule diff --git a/media/201908-trufflecon/add-overflow-spec.k b/media/201908-trufflecon/add-overflow-spec.k new file mode 100644 index 0000000000..86c28ead47 --- /dev/null +++ b/media/201908-trufflecon/add-overflow-spec.k @@ -0,0 +1,14 @@ +requires "evm.k" + +module ADD-OVERFLOW-SPEC + imports EVM + + rule #next [ ADD ] => . ... + SCHEDULE + W0 : W1 : WS => chop(W0 +Int W1) : WS + PCOUNT => PCOUNT +Int 1 + G => G -Int Gverylow < SCHEDULE > + requires G >=Int Gverylow < SCHEDULE > + andBool notBool ( #stackUnderflow ( W0 : W1 : WS , ADD ) + ) +endmodule diff --git a/media/201908-trufflecon/add-spec.k b/media/201908-trufflecon/add-spec.k new file mode 100644 index 0000000000..4d01e97045 --- /dev/null +++ b/media/201908-trufflecon/add-spec.k @@ -0,0 +1,15 @@ +requires "evm.k" + +module ADD-SPEC + imports EVM + + rule #next [ ADD ] => . ... + SCHEDULE + W0 : W1 : WS => chop(W0 +Int W1) : WS + PCOUNT => PCOUNT +Int 1 + G => G -Int Gverylow < SCHEDULE > + requires G >=Int Gverylow < SCHEDULE > + andBool notBool ( #stackUnderflow ( W0 : W1 : WS , ADD ) + orBool #stackOverflow ( W0 : W1 : WS , ADD ) + ) +endmodule diff --git a/media/201908-trufflecon/addition.evm b/media/201908-trufflecon/addition.evm new file mode 100644 index 0000000000..ee44b00f30 --- /dev/null +++ b/media/201908-trufflecon/addition.evm @@ -0,0 +1,9 @@ +load { "gas" : 10000000 + // Query: always ((~ overflow) \/ eventually revert) + // , "code" : UNSAFEADD(100 , 100) // True + // , "code" : UNSAFEADD(maxUInt256 , 100) // False + // , "code" : SAFEADD(100 , 100) // True + , "code" : SAFEADD(maxUInt256 , 100) // True + } + +start diff --git a/media/201908-trufflecon/kevm-ltl.md b/media/201908-trufflecon/kevm-ltl.md new file mode 100644 index 0000000000..344b2228d7 --- /dev/null +++ b/media/201908-trufflecon/kevm-ltl.md @@ -0,0 +1,169 @@ +```k +requires "evm.k" + +module LTL + imports BOOL + imports SET + imports LIST + + configuration + + $LTLFORMULA:LTLFormula + .EventId + .Set + .List + + + syntax EventId ::= ".EventId" + // ----------------------------- + + syntax KItem ::= EventId "{" Set "}" + // ------------------------------------ + + syntax KItem ::= LTLFormula + // --------------------------- + + syntax LTLFormula ::= LTLderive ( LTLFormula , Set ) [function] + // --------------------------------------------------------------- + + syntax LTLEvent + // --------------- + + syntax LTLAtom ::= "True" + | "False" + // -------------------------- + rule LTLderive(LTLA:LTLAtom, _) => LTLA + + syntax LTLFormula ::= "(" LTLFormula ")" [bracket] + | LTLAtom + | LTLEvent + // ------------------------------ + rule LTLderive(E:LTLEvent, ES) => True requires E in ES + rule LTLderive(E:LTLEvent, ES) => False requires notBool E in ES + + syntax LTLFormula ::= "~" LTLFormula + | LTLFormula "\\/" LTLFormula + | LTLFormula "/\\" LTLFormula + // ------------------------------------------------- + rule ~ True => False [anywhere] + rule ~ False => True [anywhere] + + rule True \/ FORM2 => True [anywhere] + rule FORM1 \/ True => True [anywhere] + + rule False \/ FORM2 => FORM2 [anywhere] + rule FORM1 \/ False => FORM1 [anywhere] + + rule True /\ FORM2 => FORM2 [anywhere] + rule FORM1 /\ True => FORM1 [anywhere] + + rule False /\ FORM2 => False [anywhere] + rule FORM1 /\ False => False [anywhere] + + rule LTLderive(~ FORM , ES) => ~ LTLderive(FORM, ES) + rule LTLderive(FORM1 \/ FORM2 , ES) => LTLderive(FORM1, ES) \/ LTLderive(FORM2, ES) + rule LTLderive(FORM1 /\ FORM2 , ES) => LTLderive(FORM1, ES) /\ LTLderive(FORM2, ES) + + syntax LTLFormula ::= LTLFormula "->" LTLFormula + // ------------------------------------------------ + rule FORM1 -> FORM2 => (~ FORM1) \/ FORM2 [macro] + + syntax LTLFormula ::= "always" LTLFormula + | "eventually" LTLFormula + // --------------------------------------------- + rule LTLderive(always FORM, ES) => LTLderive(FORM, ES) /\ always FORM + rule LTLderive(eventually FORM, ES) => LTLderive(FORM, ES) \/ eventually FORM + + syntax LTLFormula ::= LTLterminate ( LTLFormula ) [function] + // ------------------------------------------------------------ + rule LTLterminate(~ FORM1) => ~ LTLterminate(FORM1) + rule LTLterminate(FORM1 /\ FORM2) => LTLterminate(FORM1) /\ LTLterminate(FORM2) + rule LTLterminate(FORM1 \/ FORM2) => LTLterminate(FORM1) \/ LTLterminate(FORM2) + + rule LTLterminate(always _) => True + rule LTLterminate(eventually _) => False +endmodule + +module KEVM-LTL + imports EVM + imports LTL + + configuration + + + + + + syntax EthereumSimulation ::= EthereumCommand | EthereumCommand EthereumSimulation + // ---------------------------------------------------------------------------------- + rule ETC:EthereumCommand ETS:EthereumSimulation => ETC ~> ETS ... + + syntax JSON ::= OpCodes | Int + // ----------------------------- + + syntax EthereumCommand ::= "load" JSON | "start" + // ------------------------------------------------ + rule load { "gas" : GAVAIL , "code" : OPS:OpCodes , .JSONList } => . ... + _ => GAVAIL + _ => #asMapOpCodes(OPS) + _ => 0 + + rule start => #execute ... + + syntax OpCodes ::= UNSAFEADD ( Int , Int ) [function] + | SAFEADD ( Int , Int ) [function] + // ----------------------------------------------------- + rule UNSAFEADD(X, Y) => PUSH(32, X) ; PUSH(32, Y) ; ADD ; .OpCodes + rule SAFEADD(X, Y) => PUSH(32, X) ; PUSH(32, Y) ; ADD ; PUSH(32, 0) ; MSTORE // add + ; PUSH(32, X) ; PUSH(32, 0) ; MLOAD ; GT ; PUSH(32, 372) ; JUMPI // check overflow + ; PUSH(32, Y) ; PUSH(32, 0) ; MLOAD ; GT ; PUSH(32, 372) ; JUMPI // check overflow + ; PUSH(32, 0) ; PUSH(32, 0) ; REVERT // revert + ; JUMPDEST ; PUSH(32, 0) ; MLOAD ; .OpCodes // no revert + + syntax EventId ::= Int + // ---------------------- + rule #execute ... + PCOUNT + FORM => LTLderive(FORM, EVENTS) + EID => PCOUNT + EVENTS => .Set + TRACE:List (.List => ListItem(EID { EVENTS })) + requires EID =/=K PCOUNT + [priority(24)] + + rule #halt + FORM => LTLderive(FORM, EVENTS) + EID => .EventId + EVENTS => .Set + TRACE:List (.List => ListItem(EID { EVENTS })) + requires EID =/=K .EventId + [priority(24)] + + rule #halt + FORM => LTLterminate(FORM) + .EventId + requires notBool isLTLAtom(FORM) + + syntax LTLEvent ::= "overflow" + // ------------------------------ + rule ADD W0 W1 ... + EVENTS (.Set => SetItem(overflow)) + requires notBool overflow in EVENTS + andBool W0 +Word W1 =/=Int W0 +Int W1 + [priority(24)] + + syntax LTLEvent ::= "revert" + // ---------------------------- + rule REVERT _ _ ... + EVENTS (.Set => SetItem(revert)) + requires notBool revert in EVENTS + [priority(24)] + + syntax LTLEvent ::= "invalid" + // ----------------------------- + rule INVALID ... + EVENTS (.Set => SetItem(invalid)) + requires notBool invalid in EVENTS + [priority(24)] +endmodule +``` diff --git a/media/images/k-overview.png b/media/images/k-overview.png index 90a9e36a5d..8dc8cdc74f 100644 Binary files a/media/images/k-overview.png and b/media/images/k-overview.png differ