Update dependency: deps/kontrol_release

deps/kontrol_release

@@ -1 +1 @@
-0.1.45
+0.1.278

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);
         }
     }
 }

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