From 0c9b3d11b05d5c95d90a9b3585e5cbe824b60f7f Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 15 May 2024 06:29:28 -0600 Subject: [PATCH] Update dependency: deps/kontrol_release (#18) * deps/kontrol_release: Set Version 0.1.46 * deps/kontrol_release: Set Version 0.1.47 * deps/kontrol_release: Set Version 0.1.48 * deps/kontrol_release: Set Version 0.1.49 * deps/kontrol_release: Set Version 0.1.50 * deps/kontrol_release: Set Version 0.1.51 * deps/kontrol_release: Set Version 0.1.52 * deps/kontrol_release: Set Version 0.1.53 * deps/kontrol_release: Set Version 0.1.54 * deps/kontrol_release: Set Version 0.1.55 * deps/kontrol_release: Set Version 0.1.56 * deps/kontrol_release: Set Version 0.1.57 * deps/kontrol_release: Set Version 0.1.58 * deps/kontrol_release: Set Version 0.1.59 * deps/kontrol_release: Set Version 0.1.60 * deps/kontrol_release: Set Version 0.1.61 * deps/kontrol_release: Set Version 0.1.62 * deps/kontrol_release: Set Version 0.1.63 * deps/kontrol_release: Set Version 0.1.64 * deps/kontrol_release: Set Version 0.1.65 * deps/kontrol_release: Set Version 0.1.66 * deps/kontrol_release: Set Version 0.1.67 * deps/kontrol_release: Set Version 0.1.68 * deps/kontrol_release: Set Version 0.1.69 * deps/kontrol_release: Set Version 0.1.70 * deps/kontrol_release: Set Version 0.1.71 * deps/kontrol_release: Set Version 0.1.72 * deps/kontrol_release: Set Version 0.1.73 * deps/kontrol_release: Set Version 0.1.74 * deps/kontrol_release: Set Version 0.1.75 * deps/kontrol_release: Set Version 0.1.76 * deps/kontrol_release: Set Version 0.1.77 * deps/kontrol_release: Set Version 0.1.78 * deps/kontrol_release: Set Version 0.1.79 * deps/kontrol_release: Set Version 0.1.80 * deps/kontrol_release: Set Version 0.1.81 * deps/kontrol_release: Set Version 0.1.82 * deps/kontrol_release: Set Version 0.1.83 * deps/kontrol_release: Set Version 0.1.84 * deps/kontrol_release: Set Version 0.1.85 * deps/kontrol_release: Set Version 0.1.86 * deps/kontrol_release: Set Version 0.1.87 * deps/kontrol_release: Set Version 0.1.88 * deps/kontrol_release: Set Version 0.1.89 * deps/kontrol_release: Set Version 0.1.90 * deps/kontrol_release: Set Version 0.1.91 * deps/kontrol_release: Set Version 0.1.92 * deps/kontrol_release: Set Version 0.1.93 * deps/kontrol_release: Set Version 0.1.94 * deps/kontrol_release: Set Version 0.1.95 * deps/kontrol_release: Set Version 0.1.96 * deps/kontrol_release: Set Version 0.1.97 * deps/kontrol_release: Set Version 0.1.98 * deps/kontrol_release: Set Version 0.1.99 * deps/kontrol_release: Set Version 0.1.100 * deps/kontrol_release: Set Version 0.1.101 * deps/kontrol_release: Set Version 0.1.102 * deps/kontrol_release: Set Version 0.1.103 * deps/kontrol_release: Set Version 0.1.104 * deps/kontrol_release: Set Version 0.1.105 * deps/kontrol_release: Set Version 0.1.106 * deps/kontrol_release: Set Version 0.1.107 * deps/kontrol_release: Set Version 0.1.108 * deps/kontrol_release: Set Version 0.1.109 * deps/kontrol_release: Set Version 0.1.110 * deps/kontrol_release: Set Version 0.1.111 * deps/kontrol_release: Set Version 0.1.112 * deps/kontrol_release: Set Version 0.1.113 * deps/kontrol_release: Set Version 0.1.114 * deps/kontrol_release: Set Version 0.1.115 * deps/kontrol_release: Set Version 0.1.116 * deps/kontrol_release: Set Version 0.1.117 * deps/kontrol_release: Set Version 0.1.118 * deps/kontrol_release: Set Version 0.1.119 * deps/kontrol_release: Set Version 0.1.120 * deps/kontrol_release: Set Version 0.1.121 * deps/kontrol_release: Set Version 0.1.122 * deps/kontrol_release: Set Version 0.1.123 * deps/kontrol_release: Set Version 0.1.124 * deps/kontrol_release: Set Version 0.1.125 * deps/kontrol_release: Set Version 0.1.126 * deps/kontrol_release: Set Version 0.1.127 * deps/kontrol_release: Set Version 0.1.128 * deps/kontrol_release: Set Version 0.1.129 * deps/kontrol_release: Set Version 0.1.130 * deps/kontrol_release: Set Version 0.1.131 * deps/kontrol_release: Set Version 0.1.132 * deps/kontrol_release: Set Version 0.1.133 * deps/kontrol_release: Set Version 0.1.134 * deps/kontrol_release: Set Version 0.1.135 * deps/kontrol_release: Set Version 0.1.136 * deps/kontrol_release: Set Version 0.1.137 * deps/kontrol_release: Set Version 0.1.138 * deps/kontrol_release: Set Version 0.1.139 * deps/kontrol_release: Set Version 0.1.140 * deps/kontrol_release: Set Version 0.1.141 * deps/kontrol_release: Set Version 0.1.142 * deps/kontrol_release: Set Version 0.1.143 * deps/kontrol_release: Set Version 0.1.144 * deps/kontrol_release: Set Version 0.1.145 * deps/kontrol_release: Set Version 0.1.146 * deps/kontrol_release: Set Version 0.1.147 * deps/kontrol_release: Set Version 0.1.148 * deps/kontrol_release: Set Version 0.1.149 * deps/kontrol_release: Set Version 0.1.150 * deps/kontrol_release: Set Version 0.1.151 * deps/kontrol_release: Set Version 0.1.152 * deps/kontrol_release: Set Version 0.1.153 * deps/kontrol_release: Set Version 0.1.154 * deps/kontrol_release: Set Version 0.1.155 * deps/kontrol_release: Set Version 0.1.156 * deps/kontrol_release: Set Version 0.1.157 * deps/kontrol_release: Set Version 0.1.158 * deps/kontrol_release: Set Version 0.1.159 * deps/kontrol_release: Set Version 0.1.160 * deps/kontrol_release: Set Version 0.1.161 * deps/kontrol_release: Set Version 0.1.162 * deps/kontrol_release: Set Version 0.1.163 * deps/kontrol_release: Set Version 0.1.164 * deps/kontrol_release: Set Version 0.1.165 * deps/kontrol_release: Set Version 0.1.166 * deps/kontrol_release: Set Version 0.1.167 * deps/kontrol_release: Set Version 0.1.168 * deps/kontrol_release: Set Version 0.1.169 * deps/kontrol_release: Set Version 0.1.170 * deps/kontrol_release: Set Version 0.1.171 * deps/kontrol_release: Set Version 0.1.172 * deps/kontrol_release: Set Version 0.1.173 * deps/kontrol_release: Set Version 0.1.174 * deps/kontrol_release: Set Version 0.1.175 * deps/kontrol_release: Set Version 0.1.176 * deps/kontrol_release: Set Version 0.1.177 * deps/kontrol_release: Set Version 0.1.178 * deps/kontrol_release: Set Version 0.1.179 * deps/kontrol_release: Set Version 0.1.180 * deps/kontrol_release: Set Version 0.1.181 * deps/kontrol_release: Set Version 0.1.182 * deps/kontrol_release: Set Version 0.1.183 * deps/kontrol_release: Set Version 0.1.184 * deps/kontrol_release: Set Version 0.1.185 * deps/kontrol_release: Set Version 0.1.186 * deps/kontrol_release: Set Version 0.1.187 * deps/kontrol_release: Set Version 0.1.188 * deps/kontrol_release: Set Version 0.1.189 * deps/kontrol_release: Set Version 0.1.191 * deps/kontrol_release: Set Version 0.1.192 * deps/kontrol_release: Set Version 0.1.193 * deps/kontrol_release: Set Version 0.1.194 * deps/kontrol_release: Set Version 0.1.195 * deps/kontrol_release: Set Version 0.1.196 * deps/kontrol_release: Set Version 0.1.197 * deps/kontrol_release: Set Version 0.1.198 * deps/kontrol_release: Set Version 0.1.199 * deps/kontrol_release: Set Version 0.1.200 * deps/kontrol_release: Set Version 0.1.201 * deps/kontrol_release: Set Version 0.1.202 * deps/kontrol_release: Set Version 0.1.203 * deps/kontrol_release: Set Version 0.1.204 * deps/kontrol_release: Set Version 0.1.205 * deps/kontrol_release: Set Version 0.1.206 * deps/kontrol_release: Set Version 0.1.207 * deps/kontrol_release: Set Version 0.1.208 * deps/kontrol_release: Set Version 0.1.209 * deps/kontrol_release: Set Version 0.1.210 * deps/kontrol_release: Set Version 0.1.211 * deps/kontrol_release: Set Version 0.1.212 * deps/kontrol_release: Set Version 0.1.213 * deps/kontrol_release: Set Version 0.1.214 * deps/kontrol_release: Set Version 0.1.215 * deps/kontrol_release: Set Version 0.1.216 * deps/kontrol_release: Set Version 0.1.217 * deps/kontrol_release: Set Version 0.1.218 * deps/kontrol_release: Set Version 0.1.219 * deps/kontrol_release: Set Version 0.1.220 * deps/kontrol_release: Set Version 0.1.221 * deps/kontrol_release: Set Version 0.1.222 * deps/kontrol_release: Set Version 0.1.223 * deps/kontrol_release: Set Version 0.1.224 * deps/kontrol_release: Set Version 0.1.225 * deps/kontrol_release: Set Version 0.1.226 * deps/kontrol_release: Set Version 0.1.227 * deps/kontrol_release: Set Version 0.1.228 * deps/kontrol_release: Set Version 0.1.229 * deps/kontrol_release: Set Version 0.1.231 * deps/kontrol_release: Set Version 0.1.232 * deps/kontrol_release: Set Version 0.1.233 * deps/kontrol_release: Set Version 0.1.234 * deps/kontrol_release: Set Version 0.1.235 * deps/kontrol_release: Set Version 0.1.236 * deps/kontrol_release: Set Version 0.1.237 * deps/kontrol_release: Set Version 0.1.238 * deps/kontrol_release: Set Version 0.1.239 * deps/kontrol_release: Set Version 0.1.240 * deps/kontrol_release: Set Version 0.1.241 * deps/kontrol_release: Set Version 0.1.242 * deps/kontrol_release: Set Version 0.1.243 * deps/kontrol_release: Set Version 0.1.244 * deps/kontrol_release: Set Version 0.1.245 * deps/kontrol_release: Set Version 0.1.246 * deps/kontrol_release: Set Version 0.1.247 * deps/kontrol_release: Set Version 0.1.248 * deps/kontrol_release: Set Version 0.1.249 * deps/kontrol_release: Set Version 0.1.250 * deps/kontrol_release: Set Version 0.1.251 * deps/kontrol_release: Set Version 0.1.252 * deps/kontrol_release: Set Version 0.1.253 * deps/kontrol_release: Set Version 0.1.254 * deps/kontrol_release: Set Version 0.1.255 * deps/kontrol_release: Set Version 0.1.256 * deps/kontrol_release: Set Version 0.1.257 * deps/kontrol_release: Set Version 0.1.258 * deps/kontrol_release: Set Version 0.1.259 * deps/kontrol_release: Set Version 0.1.260 * deps/kontrol_release: Set Version 0.1.261 * deps/kontrol_release: Set Version 0.1.262 * deps/kontrol_release: Set Version 0.1.263 * deps/kontrol_release: Set Version 0.1.264 * deps/kontrol_release: Set Version 0.1.265 * deps/kontrol_release: Set Version 0.1.266 * deps/kontrol_release: Set Version 0.1.267 * deps/kontrol_release: Set Version 0.1.268 * deps/kontrol_release: Set Version 0.1.269 * deps/kontrol_release: Set Version 0.1.270 * deps/kontrol_release: Set Version 0.1.271 * deps/kontrol_release: Set Version 0.1.272 * deps/kontrol_release: Set Version 0.1.273 * deps/kontrol_release: Set Version 0.1.274 * deps/kontrol_release: Set Version 0.1.275 * deps/kontrol_release: Set Version 0.1.276 * deps/kontrol_release: Set Version 0.1.277 * deps/kontrol_release: Set Version 0.1.278 * Update `mulWad` and `mulWadUp` specs * Update `forge-std` to `1.7.6` * Remove `run-kevm.sh` * Add `run-kontrol.sh` * Revert "Remove `run-kevm.sh`" This reverts commit 43d233c5b6fbd58798f26d0ac3a96183e9a5bb5d. * FixedPointMathLib.k.sol: actually perform external calls * run-kontrol.sh: remove `--smt-tactic` option * Remove tatus file --------- Co-authored-by: devops Co-authored-by: Juan C --- deps/kontrol_release | 2 +- lib/forge-std | 2 +- tatus | 39 ------------------ test/FixedPointMathLib.k.sol | 24 ++++++++--- test/run-kontrol.sh | 77 ++++++++++++++++++++++++++++++++++++ 5 files changed, 97 insertions(+), 47 deletions(-) delete mode 100644 tatus create mode 100755 test/run-kontrol.sh diff --git a/deps/kontrol_release b/deps/kontrol_release index 6ee33ba2..d7045134 100644 --- a/deps/kontrol_release +++ b/deps/kontrol_release @@ -1 +1 @@ -0.1.45 +0.1.278 diff --git a/lib/forge-std b/lib/forge-std index 1d9650e9..d44c4fbb 160000 --- a/lib/forge-std +++ b/lib/forge-std @@ -1 +1 @@ -Subproject commit 1d9650e951204a0ddce9ff89c32f1997984cef4d +Subproject commit d44c4fbbb9ff054fb334babbdd34f9b6e899b3d6 diff --git a/tatus b/tatus deleted file mode 100644 index b3ce00de..00000000 --- a/tatus +++ /dev/null @@ -1,39 +0,0 @@ -diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml -index 94d499e..ad90341 100644 ---- a/.github/actions/with-docker/action.yml -+++ b/.github/actions/with-docker/action.yml -@@ -18,7 +18,7 @@ runs: - CONTAINER_NAME=${{inputs.container-name}} - CONTAINER_VERSION=${{inputs.container-version}} -  -- docker build --tag kontrol-kup-ci . -+ docker build --tag kontrol-kup-ci --build-arg=KONTROL_RELEASE=$(cat deps/kontrol_release) . -  - docker run \ - --name ${CONTAINER_NAME} \ -@@ -34,4 +34,3 @@ runs: - # Copy the current Checkout direcotry into the container - docker cp . ${CONTAINER_NAME}:/home/ubuntu/workspace - docker exec ${CONTAINER_NAME} chown -R ubuntu:ubuntu /home/ubuntu -- # docker exec ${CONTAINER_NAME} chown -R ubuntu:ubuntu /nix/store -diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml -index 35814eb..88deacb 100644 ---- a/.github/workflows/test-pr.yml -+++ b/.github/workflows/test-pr.yml -@@ -13,7 +13,7 @@ concurrency: - jobs: - new-version-test: - name: 'Test Proofs' -- runs-on: [self-hosted, linux, normal, github-runner-13] -+ runs-on: [self-hosted, linux, normal, fast] - steps: - - name: 'Check out code' - uses: actions/checkout@v3 -@@ -45,7 +45,6 @@ jobs: - - name: 'Test New Tool Versions' - run: | - # Run the following in the running docker container -- docker exec -u ubuntu ${{ env.repository_basename }}-ci bash -c 'export PATH=/home/ubuntu/.foundry/bin:$PATH && which forge' - docker exec -u ubuntu ${{ env.repository_basename }}-ci bash -c './test/run-kevm.sh' -  - - name: 'Stop Docker Container' diff --git a/test/FixedPointMathLib.k.sol b/test/FixedPointMathLib.k.sol index 914f9a63..4ed260c8 100644 --- a/test/FixedPointMathLib.k.sol +++ b/test/FixedPointMathLib.k.sol @@ -10,16 +10,28 @@ contract FixedPointMathLibVerification is Test, KontrolCheats { // Constants uint256 constant WAD = 1e18; + // Public wrapper for mulWad since Kontrol doesn't support vm.expectRevert + // for internal calls, and FixedPointMathLib.mulWad is internal + function mulWad(uint x, uint y) public pure returns (uint256) { + return FixedPointMathLib.mulWad(x, y); + } + + // Public wrapper for mulWadUp since Kontrol doesn't support vm.expectRevert + // for internal calls, and FixedPointMathLib.mulWadUp is internal + function mulWadUp(uint x, uint y) public pure returns (uint256) { + return FixedPointMathLib.mulWadUp(x, y); + } + function testMulWad(uint256 x, uint256 y) public { if(y == 0 || x <= type(uint256).max / y) { uint256 zSpec = (x * y) / WAD; uint256 zImpl = FixedPointMathLib.mulWad(x, y); - assertEq(zImpl, zSpec); + assert(zImpl == zSpec); } else { - vm.expectRevert(); // FixedPointMathLib.MulWadFailed.selector - FixedPointMathLib.mulWad(x, y); + vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector + this.mulWad(x, y); } } @@ -30,10 +42,10 @@ contract FixedPointMathLibVerification is Test, KontrolCheats { uint256 zSpec = ((x * y)/WAD)*WAD < x * y ? (x * y)/WAD + 1 : (x * y)/WAD; uint256 zImpl = FixedPointMathLib.mulWadUp(x, y); - assertEq(zImpl, zSpec); + assert(zImpl == zSpec); } else { - vm.expectRevert(); // FixedPointMathLib.MulWadFailed.selector - FixedPointMathLib.mulWadUp(x, y); + vm.expectRevert(FixedPointMathLib.MulWadFailed.selector); // FixedPointMathLib.MulWadFailed.selector + this.mulWadUp(x, y); } } } diff --git a/test/run-kontrol.sh b/test/run-kontrol.sh new file mode 100755 index 00000000..4dbb42b6 --- /dev/null +++ b/test/run-kontrol.sh @@ -0,0 +1,77 @@ +#!/bin/bash + +set -euxo pipefail + +kontrol_kompile() { + kontrol build \ + --verbose \ + --require ${lemmas} \ + --module-import ${module} \ + ${rekompile} \ + ${regen} \ + ${llvm_library} +} + +kontrol_prove() { + kontrol prove \ + --max-depth ${max_depth} \ + --max-iterations ${max_iterations} \ + --smt-timeout ${smt_timeout} \ + --workers ${workers} \ + ${reinit} \ + ${bug_report} \ + ${break_on_calls} \ + ${auto_abstract} \ + ${tests} \ +} + +lemmas=test/solady-lemmas-mod.k +base_module=SOLADY-LEMMAS +module=FixedPointMathLibVerification:${base_module} + +max_depth=10000 +max_iterations=10000 +smt_timeout=10000000 + + +# Number of processes run by the prover in parallel +# Should be at most (M - 8) / 8 in a machine with M GB of RAM +workers=2 + +regen=--regen +regen= + +rekompile=--rekompile +rekompile= + +# Progress is saved automatically so an unfinished proof can be resumed from where it left off +# Turn on to restart proof from the beginning instead of resuming +reinit=--reinit +reinit= + +break_on_calls=--no-break-on-calls +# break_on_calls= + +auto_abstract=--auto-abstract-gas +auto_abstract= + +bug_report=--bug-report +bug_report= + +# For running the booster +llvm_library=--with-llvm-library +llvm_library= + +# For running the booster +use_booster=--use-booster +use_booster= + +# List of tests to symbolically execute +tests="" +tests+="--match-test FixedPointMathLibVerification.testMulWad(uint256,uint256) " +tests+="--match-test FixedPointMathLibVerification.testMulWadUp " + +# Comment these lines as needed +pkill kore-rpc || true +kontrol_kompile +kontrol_prove