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