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 43d233c. * FixedPointMathLib.k.sol: actually perform external calls * run-kontrol.sh: remove `--smt-tactic` option * Remove tatus file --------- Co-authored-by: devops <[email protected]> Co-authored-by: Juan C <[email protected]>
runtimeverification · May 15, 2024 · 0c9b3d1 · 0c9b3d1
1 parent 299d303
commit 0c9b3d1
Show file tree

Hide file tree

Showing 5 changed files with 97 additions and 47 deletions.
diff --git 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
diff --git a/tatus b/tatus
diff --git 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
@@ -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
+1 −0		.gitattributes
+6 −12		.github/workflows/ci.yml
+3 −1		.github/workflows/sync.yml
+0 −3		.gitmodules
+1 −1		README.md
+3 −3		foundry.toml
+0 −1		lib/ds-test
+1 −1		package.json
+635 −0		scripts/vm.py
+518 −225		src/StdAssertions.sol
+28 −12		src/StdChains.sol
+2 −2		src/StdCheats.sol
+9 −3		src/StdInvariant.sol
+11 −11		src/StdJson.sol
+201 −106		src/StdStorage.sol
+179 −0		src/StdToml.sol
+61 −33		src/StdUtils.sol
+4 −4		src/Test.sol
+1,590 −416		src/Vm.sol
+234 −0		src/mocks/MockERC20.sol
+235 −0		src/mocks/MockERC721.sol
+39 −909		test/StdAssertions.t.sol
+35 −32		test/StdChains.t.sol
+20 −12		test/StdCheats.t.sol
+3 −1		test/StdError.t.sol
+49 −0		test/StdJson.t.sol
+8 −8		test/StdMath.t.sol
+159 −11		test/StdStorage.t.sol
+49 −0		test/StdToml.t.sol
+20 −20		test/StdUtils.t.sol
+15 −0		test/Vm.t.sol
+8 −0		test/fixtures/test.json
+6 −0		test/fixtures/test.toml
+441 −0		test/mocks/MockERC20.t.sol
+721 −0		test/mocks/MockERC721.t.sol