diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..24a8e87 --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.png filter=lfs diff=lfs merge=lfs -text diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 09880b1..de4cc4e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1,34 +1,30 @@ -name: test +name: Kontrol CI Demo -on: workflow_dispatch - -env: - FOUNDRY_PROFILE: ci +on: + pull_request: + branches: + - master + + workflow_dispatch: jobs: check: + concurrency: kontrol-ci-demo strategy: fail-fast: true - name: Foundry project - runs-on: ubuntu-latest + name: Kontrol Demo Project + runs-on: [self-hosted, linux, normal] steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: submodules: recursive - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 + - name: Install Kontrol + uses: runtimeverification/install-kontrol@v1.0.0 with: - version: nightly - - - name: Run Forge build - run: | - forge --version - forge build --sizes - id: build + version: latest - - name: Run Forge tests + - name: Run Kontrol Tests run: | - forge test -vvv - id: test + ./run-kontrol.sh diff --git a/.gitignore b/.gitignore index 4921ba7..6f0dfce 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ # Compiler files cache/ out/ +*.tar # Ignores development broadcast logs !/broadcast diff --git a/.gitmodules b/.gitmodules index 888d42d..9d84bdd 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "lib/forge-std"] path = lib/forge-std url = https://github.com/foundry-rs/forge-std +[submodule "lib/kontrol-cheatcodes"] + path = lib/kontrol-cheatcodes + url = https://github.com/runtimeverification/kontrol-cheatcodes.git diff --git a/README.md b/README.md index 240a747..5597445 100644 --- a/README.md +++ b/README.md @@ -1,15 +1,27 @@ -First Steps ------------ +# Highlights This repository contains a suite of property tests tailored for the OpenZeppelin ERC20 Solidity smart contract. +We want to demonstrate the usability and value of Kontrol for property testing and verification of smart contracts. + It also includes a very basic Foundry set up ready to be your first steps into the toolchain. -For kontrol documentation and more examples check [docs.runtimeverification.com/kontrol/](https://docs.runtimeverification.com/kontrol/). +For kontrol documentation and more examples check [docs.runtimeverification.com/kontrol/](https://docs.runtimeverification.com/kontrol/). + Follow the instructions below to run your first property tests using [KONTROL!](https://github.com/runtimeverification/kontrol). -Note that the instructions are for linux systems. However, they should be reproducible on Windows using the [Windows Subsystem for Linux](https://docs.microsoft.com/en-us/windows/wsl/). -Let's start with installing the tools we need. + +Note that the instructions are for linux systems. + + +# Table of Content +- [Machine Setup](#machine-setup) +- [Test Breakdown](#test-breakdown) +- [Property Testing Using Foundry](#property-testing-using-foundry) + + + +# Machine Setup Installing Foundry ------------------ @@ -46,13 +58,16 @@ Repository contents ------------------- This repository contains the OpenZeppelin ERC20 (took from the latest commit at that time, `1a60b061d5bb809c3d7e4ee915c77a00b1eca95d`) and the associated property tests. -- the [`src`](./src) directory contains the Solidity source code. -- the [`test`](./test) directory contains the Foundry property tests. -- the [`exclude`](./exclude) file contains proofs that are expected to fail. -- the [`doit`](./doit) file contains examples of Kontrol commands that you can use. -- the [`erc20.sh`](./erc20.sh) file contains a script that runs all the ERC20 proofs and times them. +- The [`src`](./src) directory contains the Solidity source code. +- The [`test`](./test) directory contains the Foundry property tests. +- The [`exclude`](./exclude) file contains proofs that are expected to fail. +- The [`run-kontrol.sh`](./run-kontrol.sh) file contains examples of Kontrol commands that you can use. +- The [`erc20.sh`](./erc20.sh) file contains a script that runs all the ERC20 proofs and times them. -### Contracts +# Test Breakdown + +Contracts +--------- In the [`src`](./src) subdirectory, you will find multiple files: @@ -68,7 +83,8 @@ In the [`src`](./src) subdirectory, you will find multiple files: However, note that we don't have the source code of the alUSD token, and much less a file or something similar with the current state of alUSD on the blockchain. Thus, we must use Foundry's extra capabilities to excercise the test correctly. -### Tests +Tests +----- In the [`test`](./test) subdirectory, you will find tests of varying difficulty: @@ -85,7 +101,10 @@ We will use foundry for: - Building the project (i.e. compiling the files), and - Running the property tests on randomized inputs. -### Building the project +# Build the Project (Kontrol / Forge) + +Build with Forge +---------------- To build the project we only need to run this command in any folder of the repo: @@ -95,7 +114,8 @@ forge build As simple as that. -### Running tests with Foundry +Run Tests with Foundry +---------------------- Since we have several different tests with different needs, we will tell Foundry which test to exercise. This is done with the options `--match` or `--match-path`, which match a string against the name of the test (executing all matches) or against the path of a file. @@ -119,7 +139,7 @@ But don't forget to add the `--fork-url`! Otherwise the test in `exclusiveToken. For ERC20, most of these tests are designed to work with symbolic execution and will most likely fail when used with Foundry. The main differences are that: -1. We use [KontrolCheats.sol](./lib/kontrol-cheatcodes/src/KontrolCheats.sol), which are not implemented in `forge`. +1. We use [KontrolCheats.sol](https://github.com/runtimeverification/kontrol-cheatcodes/tree/master), which are not implemented in `forge`. 2. We use `vm.assume` to set a precondition or an assumption, instead of filtering input values. As example, the following would reject all inputs in forge: @@ -131,14 +151,16 @@ As example, the following would reject all inputs in forge: assertEq(erc20.balanceOf(alice), amount); } ``` -Property Verification using KEVM --------------------------------- +# Property Verification using KEVM ( Kontrol ) + +Marking here for rewrite - This could be more detailed on highlighting benefits of Kontrol over Forge -- please advise With kontrol installed, you'll also have the option to do property verification! -This is a big step up in assurance from property testing, but is more computationally expensive, and often requires manual intervention. +This is a big step up in assurance from property testing, but is more computationally expensive, and often requires manual intervention. Be advised that these tests usually have a longer execution time (from a few mins up to an hour and a half), depending on the machine and the complexity of the test. -### Build with kontrol +Build with kontrol +------------------ First, we need to build a K definition for this Foundry property test suite: @@ -152,36 +174,97 @@ For example: - If you change the Solidity code, you need to re-run the above `build` command with the option `--regen` added. - If you add/modify K lemmas in `lemmas.k`, you need to rerun the above `build` command with the `--rekompile` option added. -Once you have kompiled the definition, you can now run proofs! + +Run the Proofs +-------------- +Once you have kompiled the definition, you can now run proofs! For example, to run some simple proofs from [`test/simple.t.sol`](test/simple.t.sol), you could do: ```sh kontrol prove --match-test Examples.test_assert_bool_failing --match-test Examples.test_assert_bool_passing -j2 ``` -Notice you can use `--match-test ContractName.testName` to filter tests to run, and can use `-jN` to run listed proofs in parallel! +Notice you can use `--match-test ContractName.testName` to filter tests to run, and can use `-jN` where `N` is number of threads to run listed proofs in parallel! +We suggest to not exceed 2x the number of cores in your machine. If you're machine is limited on RAM resources it's suggested to reduce parallel threads equal to Number of Cores. +CPU information is avaulable is viewable on Linux by running the command `lscpu` in the terminal. - -You can list the status of the proofs with: +For example: + ```sh + HOST:~/../kontrol-demo$ lscpu + Architecture: x86_64 + CPU op-mode(s): 32-bit, 64-bit + Address sizes: 39 bits physical, 48 bits virtual + Byte Order: Little Endian + CPU(s): 8 + On-line CPU(s) list: 0-7 + Vendor ID: GenuineIntel + Model name: 11th Gen Intel(R) Core(TM) i7-1165G7 @ 2.80GHz + CPU family: 6 + Model: 140 + Thread(s) per core: 2 + Core(s) per socket: 4 + Socket(s): 1 + ``` +Better suggestions? ^^ + +# Insights by Kontrol + +Kontrol List +------------ +You can list the status of the proofs with `kontrol list`: ```sh -kontrol list +HOST:~/../kontrol-demo$ kontrol list +APRProof: test%Examples.test_assert_bool_failing(bool):0 + status: ProofStatus.FAILED + admitted: False + nodes: 7 + pending: 1 + failing: 1 + vacuous: 0 + stuck: 0 + terminal: 2 + refuted: 0 + bounded: 0 + execution time: 45s +Subproofs: 0 + +APRProof: test%Examples.test_assert_bool_passing(bool):0 + status: ProofStatus.PASSED + admitted: False + nodes: 7 + pending: 0 + failing: 0 + vacuous: 0 + stuck: 0 + terminal: 3 + refuted: 0 + bounded: 0 + execution time: 41s +Subproofs: 0 ``` -You can visualize the result of proofs using the following command: +Kontrol View +------------ +You can visualize the result of proofs with `kontrol view-kcfg` +Lets view `Examples.test_assert_bool_failing` ```sh kontrol view-kcfg Examples.test_assert_bool_failing ``` This launches an interactive visualizer where you can click on individual nodes and edges in the generated KCFG (K Control Flow Graph) to inspect them. -There is also static visualization you can use: +![Kontrol View KCFG Demo](media/KontrolViewKCFGDemo.png) + +There is also static visualization you can use: ```sh kontrol show Examples.test_assert_bool_failing ``` -This command takes extra parameters if needed: +![Kontrol View KCFG Static Demo](media/KontrolViewKCFGStaticDemo.png) + +`Kontrol view` command takes extra parameters if needed: - `--no-minimize`: Do not omit details in node and edge output. - `--node NODE_ID`: Output the given node fully as well as the KCFG (repeats allowed). @@ -192,19 +275,21 @@ You recompile using the command above and the `--rekompile` flag. Next call `simplify-node` on the node, and check that it simplifies. For example, if there is a branch that should not happen: -You add a lemma, and call `rekompile`, then check that it simplifies the bad branch to `bottom` on using `simplify-node`. -After you're satisfied it won't branch again, you call `remove-node` on the node prior to the branch. +You add a lemma, and call `rekompile`, then check that it simplifies the bad branch to `bottom` on using `simplify-node`. +After you're satisfied it won't branch again, you call `remove-node` on the node prior to the branch. Then recall `prove` but without `--reinit` flag, to resume execution. ------- -And this is it! If you followed the instructions you just ran your first Foundry tests! +And that is it! If you followed the instructions you just ran your first Foundry tests! + +To go from here we recommend checking out [Kontrol Homepage](https://kontrol.runtimeverification.com) +And reading the [Foundry book](https://book.getfoundry.sh). -To go from here we recommend reading the [Foundry book](https://book.getfoundry.sh). -Have fun building! +🎉 Have fun building! 🎉 --------------- -**DISCLAIMER**: The files in this repository are toy examples only meant to illustrate how Foundry works. +**DISCLAIMER**: The files in this repository are toy examples only meant to illustrate how Foundry works. They are not to be used in real-world cases. -Runtime Verification will not be held accountable should you do otherwise. +Runtime Verification will not be held accountable should you do otherwise. diff --git a/doit b/doit deleted file mode 100644 index 32c0b02..0000000 --- a/doit +++ /dev/null @@ -1,112 +0,0 @@ -set -euxo pipefail - -kontrol_build() { - kontrol build --require lemmas.k --module-import ERC20:DEMO-LEMMAS \ - ${verbose} -} - -kontrol_prove() { - kontrol prove ${verbose} \ - ${break_on_calls} \ - ${bug_report} \ - ${fail_fast} "$@" -} - -kontrol_show() { - kontrol show ${verbose} ${test} "$@" -} - -kontrol_to_dot() { - kontrol to-dot ${verbose} ${test} "$@" -} - -kontrol_view() { - kontrol view-kcfg ${verbose} ${test} "$@" -} - -kontrol_list() { - kontrol list ${verbose} "$@" -} - -kontrol_remove_node() { - node_id="$1" ; shift - kontrol remove-node ${verbose} ${test} ${node_id} "$@" -} - -kontrol_simplify_node() { - node_id="$1" ; shift - kontrol simplify-node ${verbose} ${test} ${node_id} ${bug_report} "$@" -} - -kontrol_step_node() { - node_id="$1" ; shift - kontrol step-node ${verbose} ${test} ${node_id} ${bug_report} "$@" -} - -kontrol_section_edge() { - edge_id="$1" ; shift - kontrol section-edge ${verbose} ${test} ${edge_id} ${bug_report} "$@" -} - -#test=Examples.test_assert_bool_failing -#test=Examples.test_assert_bool_passing -#test=Examples.test_wmul_increasing_overflow -#test=Examples.test_wmul_increasing -#test=Examples.test_wmul_increasing_positive -#test=Examples.test_wmul_weakly_increasing_positive -#test=Examples.test_wmul_increasing_ge_one -#test=Examples.test_wmul_wdiv_inverse_underflow -#test=Examples.test_wmul_wdiv_inverse - -verbose= -verbose=--verbose - -break_on_calls=--break-on-calls -break_on_calls= - -bug_report=--bug-report -bug_report= - -# Uncomment these lines as needed -# pkill kore-rpc || true -kontrol_build --rekompile --regen -# kontrol_list -# kontrol_remove_node 4b6c47..d6d6d3 -kontrol_prove -j9 \ - --match-test Examples.test_assert_bool_failing \ - --match-test Examples.test_assert_bool_passing \ - --match-test Examples.test_wmul_increasing_overflow \ - --match-test Examples.test_wmul_increasing \ - --match-test Examples.test_wmul_increasing_positive \ - --match-test Examples.test_wmul_increasing_gt_one \ - --match-test Examples.test_wmul_weakly_increasing_positive \ - --match-test Examples.test_wmul_wdiv_inverse_underflow \ - --match-test Examples.test_wmul_wdiv_inverse -# kontrol_prove --reinit -# kontrol_section_edge --sections 4 d38e0e..ee4ec8,593be8..e93e52 -# kontrol_show # --no-minimize --node 35880c..e4389e --node 17e757..6c2e55 -# kontrol_view -# for test in ERC20Test.testAllowance ERC20Test.testApproveFailure_0 ERC20Test.testApproveFailure_1 ERC20Test.testApproveSuccess ERC20Test.testBalanceOf ERC20Test.testDecimals ERC20Test.testNameAndSymbol ERC20Test.testTotalSupply ERC20Test.testTransferFailure_0 ERC20Test.testTransferFailure_1 ERC20Test.testTransferFailure_2 ERC20Test.testTransferFromFailure ERC20Test.testTransferFromSuccess_0 ERC20Test.testTransferFromSuccess_1 ERC20Test.testTransferSuccess_0 ERC20Test.testTransferSuccess_1; do -# kontrol_to_dot -# done - -# test=AssertTest.test_sum_10 -# date -# kontrol_prove --reinit -# date -# kontrol_prove --reinit -# date -# -# test=AssertTest.test_sum_100 -# date -# kontrol_prove --reinit -# date -# kontrol_prove --reinit -# date -# -# test=AssertTest.test_sum_1000 -# date -# kontrol_prove --reinit -# date -# kontrol_prove --reinit -# date diff --git a/lib/kontrol-cheatcodes b/lib/kontrol-cheatcodes new file mode 160000 index 0000000..0048278 --- /dev/null +++ b/lib/kontrol-cheatcodes @@ -0,0 +1 @@ +Subproject commit 0048278ebdfb04f452a448bf1fe19a06205efae3 diff --git a/lib/kontrol-cheatcodes/README.md b/lib/kontrol-cheatcodes/README.md deleted file mode 100644 index be180d3..0000000 --- a/lib/kontrol-cheatcodes/README.md +++ /dev/null @@ -1,19 +0,0 @@ -# Kontrol Cheatcodes - -Kontrol cheatcodes complement [Foundry's cheatcodes](https://book.getfoundry.sh/cheatcodes/) to enhance the expressivity of your symbolic specifications even further. With these cheatcodes, you can, for instance, make the storage of a given address symbolic, create new symbolic values, or expect that no further calls are made. - -Check out our [Kontrol documentation](https://docs.runtimeverification.com/kontrol/overview/readme) to start writing and executing symbolic tests for your project! - -Join our [Discord](https://discord.gg/9nFGwVRfMD) to ask any questions you may have. - -## Installation - -You can install this repository either via `forge` or as a `git` submodule: - -``` -forge install runtimeverification/kontrol-cheatcodes -``` - -``` -git submodule add https://github.com/runtimeverification/kontrol-cheatcodes -``` diff --git a/lib/kontrol-cheatcodes/src/KontrolCheats.sol b/lib/kontrol-cheatcodes/src/KontrolCheats.sol deleted file mode 100644 index b09b204..0000000 --- a/lib/kontrol-cheatcodes/src/KontrolCheats.sol +++ /dev/null @@ -1,44 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity >=0.6.2 <0.9.0; -pragma experimental ABIEncoderV2; - -interface KontrolCheatsBase { - // Expects a call using the CALL opcode to an address with the specified calldata. - function expectRegularCall(address,bytes calldata) external; - // Expects a call using the CALL opcode to an address with the specified msg.value and calldata. - function expectRegularCall(address,uint256,bytes calldata) external; - // Expects a static call to an address with the specified calldata. - function expectStaticCall(address,bytes calldata) external; - // Expects a delegate call to an address with the specified calldata. - function expectDelegateCall(address,bytes calldata) external; - // Expects that no contract calls are made after invoking the cheatcode. - function expectNoCall() external; - // Expects the given address to deploy a new contract, using the CREATE opcode, with the specified value and bytecode. - function expectCreate(address,uint256,bytes calldata) external; - // Expects the given address to deploy a new contract, using the CREATE2 opcode, with the specified value and bytecode (appended with a bytes32 salt). - function expectCreate2(address,uint256,bytes calldata) external; - // Makes the storage of the given address completely symbolic. - function symbolicStorage(address) external; - // Adds an address to the whitelist. - function allowCallsToAddress(address) external; - // Adds an address and a storage slot to the whitelist. - function allowChangesToStorage(address,uint256) external; - // Sets the remaining gas to an infinite value. - function infiniteGas() external; - // Sets the current cell to the supplied amount. - function setGas(uint256) external; - // Returns a symbolic unsigned integer - function freshUInt(uint8) external returns (uint256); - // Returns a symbolic boolean value - function freshBool() external returns (uint256); -} - -abstract contract KontrolCheats { - KontrolCheatsBase public constant kevm = KontrolCheatsBase(address(uint160(uint256(keccak256("hevm cheat code"))))); - - // Checks if an address matches one of the built-in addresses. - function notBuiltinAddress(address addr) internal pure returns (bool) { - return (addr != address(645326474426547203313410069153905908525362434349) && - addr != address(728815563385977040452943777879061427756277306518)); - } -} diff --git a/media/KontrolViewKCFGDemo.png b/media/KontrolViewKCFGDemo.png new file mode 100644 index 0000000..f24839a --- /dev/null +++ b/media/KontrolViewKCFGDemo.png @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f93806986bc665f708a6ee51fc676e69ba2eb87e0181ba4a5ed44652fa10c285 +size 47983 diff --git a/media/KontrolViewKCFGStaticDemo.png b/media/KontrolViewKCFGStaticDemo.png new file mode 100644 index 0000000..228e367 --- /dev/null +++ b/media/KontrolViewKCFGStaticDemo.png @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:0cdb2c9e48d45c8fa43ac24ed4db52667d080472ada719efdc948715d6c2d12a +size 57890 diff --git a/run-kontrol.sh b/run-kontrol.sh new file mode 100755 index 0000000..c78c83a --- /dev/null +++ b/run-kontrol.sh @@ -0,0 +1,129 @@ +#!/usr/bin/env bash +set -uxo pipefail + +##################### +# Sameple Functions # +##################### +verbose="" +kontrol_build() { + kontrol build "$@" +} + +kontrol_prove() { + kontrol prove "$@" +} + +kontrol_show() { + kontrol show "${test}" "$@" +} + +kontrol_to_dot() { + kontrol to-dot "${test}" "$@" +} + +kontrol_view() { + kontrol view-kcfg "${test}" "$@" +} + +kontrol_list() { + kontrol list "$@" +} + +kontrol_remove_node() { + node_id="$1" ; shift + kontrol remove-node "${test}" ${node_id} "$@" +} + +kontrol_simplify_node() { + node_id="$1" ; shift + kontrol simplify-node "${test}" ${node_id} "${bug_report}" "$@" +} + +kontrol_step_node() { + node_id="$1" ; shift + kontrol step-node "${test}" ${node_id} "${bug_report}" "$@" +} + +kontrol_section_edge() { + edge_id="$1" ; shift + kontrol section-edge "${test}" ${edge_id} "${bug_report}" "$@" +} + +################################# +# Kore RPC Server Stuck? Run .. # +################################# +# pkill kore-rpc || true + +kontrol_build --require lemmas.k --module-import ERC20:DEMO-LEMMAS --verbose +kontrol_list +kontrol_prove -j8 \ + --verbose \ + --bug-report=BUGREPORT.bug \ + --match-test Examples.test_assert_bool_failing + # --match-test Examples.test_assert_bool_passing\ + # --match-test Examples.test_wmul_increasing_overflow\ + # --match-test Examples.test_wmul_increasing\ + # --match-test Examples.test_wmul_increasing_positive\ + # --match-test Examples.test_wmul_increasing_gt_one\ + # --match-test Examples.test_wmul_weakly_increasing_positive\ + # --match-test Examples.test_wmul_wdiv_inverse_underflow\ + # --match-test Examples.test_wmul_wdiv_inverse +kontrol_list --verbose + +########################### +# Additional Tests to Run # +########################### +#test=Examples.test_assert_bool_failing +#test=Examples.test_assert_bool_passing +#test=Examples.test_wmul_increasing_overflow +#test=Examples.test_wmul_increasing +#test=Examples.test_wmul_increasing_positive +#test=Examples.test_wmul_weakly_increasing_positive +#test=Examples.test_wmul_increasing_ge_one +#test=Examples.test_wmul_wdiv_inverse_underflow +#test=Examples.test_wmul_wdiv_inverse + +################################### +# Review Assert bool Failing Test # +################################### +test=Examples.test_assert_bool_failing +kontrol_show --verbose + +################ +# Modify Nodes # +################ +kontrol_remove_node 4b6c47..d6d6d3 +kontrol_prove --reinit + +############################## +# Additional Reinit Examples # +############################## +# test=AssertTest.test_sum_10 +# date +# kontrol_prove --reinit +# date +# kontrol_prove --reinit +# date +# test=AssertTest.test_sum_100 +# date +# kontrol_prove --reinit +# date +# kontrol_prove --reinit +# date +# test=AssertTest.test_sum_1000 +# date +# kontrol_prove --reinit +# date +# kontrol_prove --reinit +# date + +########################## +# Additional Run Example # +########################## +# kontrol_prove --reinit +# kontrol_section_edge --sections 4 d38e0e..ee4ec8,593be8..e93e52 +# kontrol_show # --no-minimize --node 35880c..e4389e --node 17e757..6c2e55 +# kontrol_view +# for test in ERC20Test.testAllowance ERC20Test.testApproveFailure_0 ERC20Test.testApproveFailure_1 ERC20Test.testApproveSuccess ERC20Test.testBalanceOf ERC20Test.testDecimals ERC20Test.testNameAndSymbol ERC20Test.testTotalSupply ERC20Test.testTransferFailure_0 ERC20Test.testTransferFailure_1 ERC20Test.testTransferFailure_2 ERC20Test.testTransferFromFailure ERC20Test.testTransferFromSuccess_0 ERC20Test.testTransferFromSuccess_1 ERC20Test.testTransferSuccess_0 ERC20Test.testTransferSuccess_1; do +# kontrol_to_dot +# done