From c4f9f43647f43b61709cbf5845e83eccbec38634 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 28 Mar 2024 16:23:43 -0600 Subject: [PATCH 01/10] Move to intall-kontrol action and run kontrol intead of foundry --- .github/workflows/test.yml | 25 +++++++++---------------- README.md | 2 +- doit => run-kontrol.sh | 6 +++--- 3 files changed, 13 insertions(+), 20 deletions(-) rename doit => run-kontrol.sh (98%) mode change 100644 => 100755 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 09880b1..21c3e54 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1,4 +1,4 @@ -name: test +name: Kontrol CI Demo on: workflow_dispatch @@ -10,25 +10,18 @@ jobs: 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 + version: latest - - name: Run Forge build + - name: Run Kontrol Tests run: | - forge --version - forge build --sizes - id: build - - - name: Run Forge tests - run: | - forge test -vvv - id: test + ./run-kontrol.sh diff --git a/README.md b/README.md index 240a747..537da99 100644 --- a/README.md +++ b/README.md @@ -49,7 +49,7 @@ This repository contains the OpenZeppelin ERC20 (took from the latest commit at - 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 [`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 diff --git a/doit b/run-kontrol.sh old mode 100644 new mode 100755 similarity index 98% rename from doit rename to run-kontrol.sh index 32c0b02..d2c600a --- a/doit +++ b/run-kontrol.sh @@ -62,10 +62,10 @@ verbose= verbose=--verbose break_on_calls=--break-on-calls -break_on_calls= +# break_on_calls= bug_report=--bug-report -bug_report= +# bug_report= # Uncomment these lines as needed # pkill kore-rpc || true @@ -101,7 +101,7 @@ kontrol_prove -j9 \ # date # kontrol_prove --reinit # date -# kontrol_prove --reinit +# kontrol_prove --reinitf # date # # test=AssertTest.test_sum_1000 From bdf1763995178da30a759fa03e0c15b7902bf732 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 28 Mar 2024 20:41:37 -0600 Subject: [PATCH 02/10] Fix bash script --- run-kontrol.sh | 69 +++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 34 deletions(-) diff --git a/run-kontrol.sh b/run-kontrol.sh index d2c600a..7320f76 100755 --- a/run-kontrol.sh +++ b/run-kontrol.sh @@ -1,52 +1,53 @@ +#!/usr/bin/env bash set -euxo pipefail kontrol_build() { kontrol build --require lemmas.k --module-import ERC20:DEMO-LEMMAS \ - ${verbose} + "${verbose}" } kontrol_prove() { - kontrol prove ${verbose} \ - ${break_on_calls} \ - ${bug_report} \ - ${fail_fast} "$@" + kontrol prove "${verbose}"\ + "${break_on_calls}"\ + "${bug_report}"\ + "$@" } -kontrol_show() { - kontrol show ${verbose} ${test} "$@" -} +# kontrol_show() { +# kontrol show "${verbose}" "${test}" "$@" +# } -kontrol_to_dot() { - kontrol to-dot ${verbose} ${test} "$@" -} +# kontrol_to_dot() { +# kontrol to-dot "${verbose}" "${test}" "$@" +# } -kontrol_view() { - kontrol view-kcfg ${verbose} ${test} "$@" -} +# kontrol_view() { +# kontrol view-kcfg "${verbose}" "${test}" "$@" +# } -kontrol_list() { - kontrol list ${verbose} "$@" -} +# kontrol_list() { +# kontrol list "${verbose}" "$@" +# } -kontrol_remove_node() { - node_id="$1" ; shift - kontrol remove-node ${verbose} ${test} ${node_id} "$@" -} +# 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_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_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} "$@" -} +# 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 @@ -64,7 +65,7 @@ verbose=--verbose break_on_calls=--break-on-calls # break_on_calls= -bug_report=--bug-report +bug_report="--bug-report=BUGREPORT.bug" # bug_report= # Uncomment these lines as needed From eb6a14a28dd5055a3b75fb7c3e64007e283bc40d Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 28 Mar 2024 21:08:17 -0600 Subject: [PATCH 03/10] Run on pull request --- .github/workflows/test.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 21c3e54..9a93466 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -1,6 +1,11 @@ name: Kontrol CI Demo -on: workflow_dispatch +on: + pull_request: + branches: + - master + + workflow_dispatch: env: FOUNDRY_PROFILE: ci From 1f1656b99f982f8f32b4a15c089275adc1d6a495 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 28 Mar 2024 21:10:21 -0600 Subject: [PATCH 04/10] concurrency --- .github/workflows/test.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9a93466..9e05507 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -12,6 +12,7 @@ env: jobs: check: + concurrency: kontrol-ci-demo strategy: fail-fast: true From 3299f327fb62adaad99e9f18392410ed7e9a49ae Mon Sep 17 00:00:00 2001 From: Freeman <105403280+F-WRunTime@users.noreply.github.com> Date: Fri, 29 Mar 2024 10:07:28 -0600 Subject: [PATCH 05/10] Update run-kontrol.sh Fixing typo probably breaking build Co-authored-by: Palina Tolmach --- run-kontrol.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/run-kontrol.sh b/run-kontrol.sh index 7320f76..0b198fe 100755 --- a/run-kontrol.sh +++ b/run-kontrol.sh @@ -102,7 +102,7 @@ kontrol_prove -j9 \ # date # kontrol_prove --reinit # date -# kontrol_prove --reinitf +# kontrol_prove --reinit # date # # test=AssertTest.test_sum_1000 From 352d5c49c37935e349572b3a1b6c6e735825daba Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 29 Mar 2024 10:10:43 -0600 Subject: [PATCH 06/10] Additions from review --- run-kontrol.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/run-kontrol.sh b/run-kontrol.sh index 0b198fe..a9e848a 100755 --- a/run-kontrol.sh +++ b/run-kontrol.sh @@ -63,7 +63,7 @@ verbose= verbose=--verbose break_on_calls=--break-on-calls -# break_on_calls= +break_on_calls= bug_report="--bug-report=BUGREPORT.bug" # bug_report= From 73314f39a54beb218d8873583b5fc5e8230281b2 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 29 Mar 2024 10:25:09 -0600 Subject: [PATCH 07/10] Adding new git submodule to track cheatcodes repository --- .gitmodules | 3 ++ lib/kontrol-cheatcodes | 1 + lib/kontrol-cheatcodes/README.md | 19 --------- lib/kontrol-cheatcodes/src/KontrolCheats.sol | 44 -------------------- 4 files changed, 4 insertions(+), 63 deletions(-) create mode 160000 lib/kontrol-cheatcodes delete mode 100644 lib/kontrol-cheatcodes/README.md delete mode 100644 lib/kontrol-cheatcodes/src/KontrolCheats.sol 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/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)); - } -} From 3ccafc97822320bc31709eb47964ecc4ac8aca60 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 29 Mar 2024 10:25:39 -0600 Subject: [PATCH 08/10] update cheat code reference in README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 537da99..bd539f7 100644 --- a/README.md +++ b/README.md @@ -119,7 +119,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: From ed815568aa5eeaf9d1fb3b3522650b3f4b9f3984 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 29 Mar 2024 12:46:47 -0600 Subject: [PATCH 09/10] Updating ReADME documentation, run-kontrol script formatting and steps to follow the README example more closely. Adding some media files for Example showing --- .gitattributes | 1 + .gitignore | 1 + README.md | 151 +++++++++++++++++++++------ media/KontrolViewKCFGDemo.png | 3 + media/KontrolViewKCFGStaticDemo.png | 3 + run-kontrol.sh | 154 +++++++++++++++------------- 6 files changed, 211 insertions(+), 102 deletions(-) create mode 100644 .gitattributes create mode 100644 media/KontrolViewKCFGDemo.png create mode 100644 media/KontrolViewKCFGStaticDemo.png 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/.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/README.md b/README.md index bd539f7..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 [`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. +- 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. @@ -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/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 index a9e848a..c78c83a 100755 --- a/run-kontrol.sh +++ b/run-kontrol.sh @@ -1,54 +1,78 @@ #!/usr/bin/env bash -set -euxo pipefail +set -uxo pipefail +##################### +# Sameple Functions # +##################### +verbose="" kontrol_build() { - kontrol build --require lemmas.k --module-import ERC20:DEMO-LEMMAS \ - "${verbose}" + kontrol build "$@" } kontrol_prove() { - kontrol prove "${verbose}"\ - "${break_on_calls}"\ - "${bug_report}"\ - "$@" + kontrol prove "$@" } -# kontrol_show() { -# kontrol show "${verbose}" "${test}" "$@" -# } +kontrol_show() { + kontrol show "${test}" "$@" +} -# kontrol_to_dot() { -# kontrol to-dot "${verbose}" "${test}" "$@" -# } +kontrol_to_dot() { + kontrol to-dot "${test}" "$@" +} -# kontrol_view() { -# kontrol view-kcfg "${verbose}" "${test}" "$@" -# } +kontrol_view() { + kontrol view-kcfg "${test}" "$@" +} -# kontrol_list() { -# kontrol list "${verbose}" "$@" -# } +kontrol_list() { + kontrol list "$@" +} -# kontrol_remove_node() { -# node_id="$1" ; shift -# kontrol remove-node "${verbose}" "${test}" ${node_id} "$@" -# } +kontrol_remove_node() { + node_id="$1" ; shift + kontrol remove-node "${test}" ${node_id} "$@" +} -# kontrol_simplify_node() { -# node_id="$1" ; shift -# kontrol simplify-node "${verbose}" "${test}" ${node_id} "${bug_report}" "$@" -# } +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 "${verbose}" "${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 "${verbose}" "${test}" ${edge_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 @@ -59,55 +83,47 @@ kontrol_prove() { #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=BUGREPORT.bug" -# 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 - +################################### +# 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 From d5cfd337a6bbe5b273733b9968e8547e24468984 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 29 Mar 2024 12:54:42 -0600 Subject: [PATCH 10/10] remove profile definition from env vars --- .github/workflows/test.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9e05507..de4cc4e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -7,9 +7,6 @@ on: workflow_dispatch: -env: - FOUNDRY_PROFILE: ci - jobs: check: concurrency: kontrol-ci-demo