about ./kevm prove problems

[ricky222368]

I follow README.md and run ./kevm prove tests/specs/ds-token-erc20/transfer-failure-1-a-spec.k -m VERIFICATION it gets #True , but also gets some warnings. Is it important?

[Warning] Internal: execution phase: missing SMTLib translation for #gas .
Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for #gas)
[Warning] Internal: execution phase: missing SMTLib translation for #symCmem .
Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for #symCmem)
[Warning] Internal: execution phase: missing SMTLib translation for _&Int_ .
Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for _&Int_)
[Warning] Internal: execution phase: missing SMTLib translation for log2Int .
Please re-run with the --debug-z3 flag. Search the logs starting with 'Z3
warning' to see the Z3 implication that generated the warning. (missing SMTLib
translation for log2Int)

so i re-run by ./kevm prove tests/specs/ds-token-erc20/transfer-failure-1-a-spec.k --debug-z3

and get this error. didn't find some similar issue. How should I solve it? thanks.

Importing: Source(/home/user/evm-semantics/././tests/specs/ds-token-erc20/transfer-failure-1-a-spec.k)
Importing: Source(/home/user/evm-semantics/tests/specs/ds-token-erc20/transfer-failure-1-a-spec.k)
Importing: Source(/home/user/evm-semantics/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k)
Importing: Source(/home/user/evm-semantics/tests/specs/ds-token-erc20/evm-symbolic.k)
Importing: Source(/home/user/evm-semantics/.build/defn/java/edsl.k)
Importing: Source(/home/user/evm-semantics/.build/defn/java/evm.k)
Importing: Source(/home/user/evm-semantics/.build/defn/java/data.k)
Importing: Source(/home/user/evm-semantics/.build/defn/java/krypto.k)
Importing: Source(/home/user/evm-semantics/.build/defn/java/network.k)
Importing: Source(/home/user/evm-semantics/tests/specs/ds-token-erc20/verification.k)
Importing: Source(/home/user/evm-semantics/tests/specs/ds-token-erc20/evm-data-map-concrete.k)
Importing: Source(/home/user/evm-semantics/tests/specs/lemmas.k)
Parse spec modules [1/1017 rules]                            =  0.016s

Parsing finished:  149.527 s
Pre-processing rule:
  rule <k> G ~> #deductGas => . ... </k>
       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
       <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
    requires #notKLabel(G, "#symCmem")
        Source: /home/user/evm-semantics/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k Location(18,8,21,39)
==================================
Unification failure: #notKLabel(G:Int,, String(#""#symCmem"")) does not unify with Bool(#"true")
Unification failure: #notKLabel(G:Int,, String(#""#symCmem"")) does not unify with Bool(#"true")
[Error] Critical: Rule requires clause evaluates to false:
  rule <k> G ~> #deductGas => . ... </k>
       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM)
</gas>
       <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
    requires #notKLabel(G, "#symCmem")
        Source:
/home/user/evm-semantics/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k
Location(18,8,21,39)

[ehildenb]

The warnings you get are not important, it's saying it could not rely on Z3 to handle some intermediate step, but was able to procede anyway.

The second issue you have is because you're forgetting to pass -m VERIFICATION. But that means you have an outdated version of KEVM, because later versions require you pass it directly after the file you're proving. I would recommend updating KEVM and then reading ./kevm help.

[ricky222368]

I used kevm dockerfile on docker hub so I get outdated version. I use the dockerfile on this github to build new version kevm, and step on step to build by README.md. But when I do this command make build RELEASE=1, I get some problem below.

/bin/sh: 1: cd: can't cd to tests/openzeppelin-contracts
/bin/sh: 1: cd: can't cd to tests/openzeppelin-contracts
/bin/sh: 1: cd: can't cd to tests/synthetix
/bin/sh: 1: cd: can't cd to tests/synthetix
cd /home/user/evm-semantics/.build/defn/web3/build && cmake /home/user/evm-semantics/cmake/client -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/usr/local && make
-- Configuring done
-- Generating done
-- Build files have been written to: /home/user/evm-semantics/.build/defn/web3/build
make[1]: Entering directory '/home/user/evm-semantics/.build/defn/web3/build'
make[2]: Entering directory '/home/user/evm-semantics/.build/defn/web3/build'
make[3]: Entering directory '/home/user/evm-semantics/.build/defn/web3/build'
make[3]: Leaving directory '/home/user/evm-semantics/.build/defn/web3/build'
make[3]: Entering directory '/home/user/evm-semantics/.build/defn/web3/build'
[ 16%] Linking CXX executable kevm-client
/home/user/evm-semantics/deps/k/k-distribution/target/release/k/bin/llvm-kompile: line 27: 15630 Segmentation fault      (core dumped) "$(dirname "$0")"/llvm-kompile-codegen "$definition" "$dt_dir"/dt.yaml "$dt_dir" $debug > "$mod"
CMakeFiles/kevm-client.dir/build.make:199: recipe for target 'kevm-client' failed
make[3]: *** [kevm-client] Error 139
make[3]: Leaving directory '/home/user/evm-semantics/.build/defn/web3/build'
CMakeFiles/Makefile2:67: recipe for target 'CMakeFiles/kevm-client.dir/all' failed
make[2]: *** [CMakeFiles/kevm-client.dir/all] Error 2
make[2]: Leaving directory '/home/user/evm-semantics/.build/defn/web3/build'
Makefile:129: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/user/evm-semantics/.build/defn/web3/build'
Makefile:268: recipe for target '/home/user/evm-semantics/.build/defn/web3/build/kevm-client' failed
make: *** [/home/user/evm-semantics/.build/defn/web3/build/kevm-client] Error 2

I can run ./kevm run tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json, but ./kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k -m VERIFICATION will be

[Error] Compiler: Could not find main module with name -m in definition. Use
--main-module to specify one.

I use ./kevm --version can find

== KEVM Version
4328d87
== K Version
RV-K version 1.0-SNAPSHOT
Git revision: 280480e
Git branch: UNKNOWN
Build date: Mon Feb 03 02:28:54 CST 2020
== Kore Version
K framework version 0.0.1.0
Git:
  revision:     c3b49acf34aa1f3bf0255ecab75adf326ade525e
  branch:       HEAD
  last commit:  2020 Jan 30 10:21:34 -0600
Build date:     2020 Feb 04 04:26:48 +0000
== Z3 Version
Z3 version 4.6.0 - 64 bit

Do I have wrong step? thanks for replying.

[ehildenb]

The RELEASE build is broken at the moment, it's being tracked and should be fixed within a week or so. You should be able to do make build (without the RELEASE=1) to get it to build correctly.

[ehildenb]

Also, if you only need to do proving, depending on the backend you want, you can just do make build-java build-haskell -j2, and skip building the llvm backend (which is not used for proving).

[ricky222368]

I can do make build (without RELEASE=1) to build it. I do make build and make -j2 , and I build correctly . But ./kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k -m VERIFICATION still be

[Error] Compiler: Could not find main module with name -m in definition. Use
--main-module to specify one.

And sorry for that are there any user guide (like what krun doing, kprove doing...) for freshman. sorry for too much problem. thanks.

[ehildenb]

You need to do ./kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k VERIFICATION (without the -m).

I recently updated it to not require the -m, ./kevm help should be updated.

Whenever you're not sure, check ./kevm help.

[ricky222368]

I also want to ask some questions, I don't know my idea is correct or not. ./kevm run the file xxx.json is written by bytecode (like using Solidity language to compile to bytecode), and the command will produce the bytecode with K type? ./kevm prove the file xxx.k is written by the code which ./kevm run produce, and this command will prove the smart contract with bytecode type is true or not?

thanks.

[ehildenb]

No, that's not how it works.

./kevm run SOME_PROGRAM can accept SOME_PROGRAM in either (1) the testing format for cliets, or (2) our custom EthereumSimulation format. For some examples, SOME_PROGRAM can be tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json or it can be tests/interactive/sumTo10.evm.

./kevm prove SOME_SPECIFICATION can accept SOME_SPECIFICATION in the K prover language. For example, SOME_SPECIFICATION can be tests/specs/erc20/ds/allowance-spec.k, which is the specification for the correctness of the DS-token ERC20 specification.

[ricky222368]

oh, but how the SOME_PROGRAM in ./kevm run SOME_PROGRAM produce ? (the xxx.son file looks like a bytecode format compiled by high level language). And SOME_SPECIFICATION is the same problem... (SOME_SPECIFICATION is written by user?) I still stuck at the whole workflow. It makes me confuse. If I want to use my smart contract code (ex. written by Solidity) and verify its correctness. The first step is compile it and take the bytecode to run ./kevm run SOME_PROGRAM ? Or..

thanks.

[ehildenb]

No, the first step is to write down in natural language (English for me, whatever is your native language) and mathematics what you expect your contract to do.

Then you need to take that mathematical description and translate it into a specification that a prover can handle. In the case of KEVM, that means you need to translate it to the format of tests/specs/*-spec.k file. Then you can call ./kevm prove ... on that file, and K will tell you whether your specification is true or not.

It's a long process, but the very first thing you need to do is have a description of what you want to verify about your contract. Saying "this contract is formally verified" doesn't make sense. You need to say "this contract is formally verified to have some property".

[ricky222368]

./kevm run SOME_PROGRAM just run a EVM program. What it prints, it doesn't run for what?

You means that I need to define a spec what property I want the smart contract has, and verify the contract has this property or not? (This is ./kevm prove do) but, how to translate that into a prover can handle. Or is it for users to think for themselves?

[ehildenb]

./kevm run prints out the final state after running an EVM program. Try out ./kevm run tests/interactive/sumTo10.evm to see.

Well you probably need to learn K first to know how to translate it into something the prover can handle. I would recommend starting with the K tutorial: https://github.com/kframework/k/tree/master/k-distribution/tutorial

Also, if you want more help, I would recommend joining the K chat too: https://riot.im/app/#/room/#k:matrix.org

[ricky222368]

The xxx.json and xxx.evm looks like a bytecode type? How the example code produced, did it make a smart contract be compiled to bytecode and use it?

I have seen some examples like add1.json exp0.json sumTo10.evm... Does the file .json .evm have some format to code? Are any xxx.json or xxx.evm examples (step by step) can let me know how to write it?

[ricky222368]

I do some prove tests in /tests/specs/bihu/forwardToHotWallet-failure-3-spec.k but get this error

[Warning] Critical: Found variable _ on right hand side of rule, not bound on
left hand side. Did you mean "?_"?
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/bihu/forwardToHotWallet-failure-3-spec.k)
        Location(16,23,16,24)

do the README.md instruction ./kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k VERIFICATION also get

  while evaluating function keccak
  while evaluating function keccakIntList
  while evaluating function keccak
[Warning] Critical: Found variable _ on right hand side of rule, not bound on
left hand side. Did you mean "?_"?
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/erc20/ds/transfer-failure-1-a-spec.k)
        Location(16,23,16,24)

I could see True or False before, but now get some error. it means something need to modify in -spec.k?

I do make test-prove to test, but get many error like this (just a part of error)

Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/benchmarks/abstract-semantics.k)
        Location(22,15,22,39)
[Warning] Critical: Found klabel #getKLabelString not defined in any
production.
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/benchmarks/abstract-semantics.k)
        Location(29,15,29,39)
[Warning] Critical: Found klabel #isConcrete not defined in any production.
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/benchmarks/ecrec-symbolic.k)
        Location(14,22,14,39)
[Warning] Critical: Found klabel #isConcrete not defined in any production.
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/benchmarks/ecrec-symbolic.k)
        Location(20,22,20,39)
[Warning] Critical: Found klabel #notKLabel not defined in any production.
Note: this warning will become an error in subsequent releases.
        Source(/home/user/evm-semantics/tests/specs/benchmarks/abstract-semantics-segmented-gas.k)
        Location(21,14,21,39)