Verify mulWad functions correctness

.github/actions/with-docker/action.yml

@@ -1,9 +1,6 @@
 name: 'With Docker'
 description: 'Run a given stage with Docker Image'
 inputs:
-  container-version:
-    description: 'Docker Image Version'
-    required: true
   container-name:
     description: 'Docker Container Name'
     required: true
@@ -16,17 +13,18 @@ runs:
       set -euxo pipefail
 
       CONTAINER_NAME=${{inputs.container-name}}
-      CONTAINER_VERSION=${{inputs.container-version}}
-
-      docker run                          \
-        --name ${CONTAINER_NAME}          \
-        --rm                              \
-        --interactive                     \
-        --tty                             \
-        --detach                          \
-        --user root                       \
-        --workdir /home/user/workspace            \
-        runtimeverificationinc/kontrol:ubuntu-jammy-${CONTAINER_VERSION}
+      CONTAINER_VERSION=$(cat deps/kontrol_release)
+      KONTROL_RELEASE=$(cat deps/kontrol_release)
+
+      docker run                                                    \
+        --name ${CONTAINER_NAME}                                    \
+        --rm                                                        \
+        --interactive                                               \
+        --tty                                                       \
+        --detach                                                    \
+        --user root                                                 \
+        --workdir /home/user/workspace                            \
+        runtimeverificationinc/kontrol:ubuntu-jammy-${KONTROL_RELEASE}
 
       # Copy the current Checkout direcotry into the container
       docker cp . ${CONTAINER_NAME}:/home/user/workspace

.github/workflows/test-pr.yml

@@ -29,25 +29,23 @@ jobs:
           # Get Repository Base name
           echo "repository_basename=$(basename ${{ github.repository }})" >> $GITHUB_ENV
 
+      - name: Docker Login w/ Github Token
+        uses: docker/login-action@v1
+        with:
+          username: rvdockerhub
+          password: ${{ secrets.DOCKERHUB_PASSWORD }}
+
       - name: "Start Docker Container"
         uses: ./.github/actions/with-docker
         with:
           container-name: '${{ env.repository_basename }}-ci'
-          container-version: '${{ env.kontrol-version }}'
 
       - name: 'Test New Tool Versions'
         run: |
           # Run the following in the running docker container
-          docker exec -u user ${{ env.repository_basename }}-ci bash -c ' 
-            set -euo pipefail
-            # If all scripts in test.sh pass then the test is successful, else fail 
-            # and print the name of the script that failed
-            for script in ./test/*.sh; do
-                if ! bash "$script"; then
-                    echo "Test failed: $script"
-                    exit 1
-                else
-                    echo "Test passed: $script"
-                fi
-            done
-          '
+          docker exec -u user ${{ env.repository_basename }}-ci bash -c './test/run-kevm.sh'
+
+      - name: 'Stop Docker Container'
+        if: always()
+        run: |
+          docker stop --time=0 ${{ env.repository_basename }}-ci

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "lib/solady"]
 	path = lib/solady
 	url = https://github.com/vectorized/solady
+[submodule "lib/kontrol-cheatcodes"]
+	path = lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes

README.md

@@ -10,9 +10,11 @@ We employ two different types of specification for function verification: functi
 
 ### Verified functions
 
-| Name             | Location           | Equivalence           | Property           |
-|------------------|--------------------|-----------------------|--------------------|
-| FooName : string | FooLocation : path | FooEquivalence : Bool | FooProperty : Bool |
+| Name       | Location                                                                                                                 | Equivalence | Property |
+|------------|--------------------------------------------------------------------------------------------------------------------------|-------------|----------|
+| `wadMul`   | [solady/src/utils/FixedPointMathLib.sol](https://github.com/Vectorized/solady/blob/main/src/utils/FixedPointMathLib.sol) | No          | Yes      |
+| `wadMulUp` | [solady/src/utils/FixedPointMathLib.sol](https://github.com/Vectorized/solady/blob/main/src/utils/FixedPointMathLib.sol) | No          | Yes      |
+
 
 ## Repository Structure
 

deps/kontrol_release

@@ -1 +1 @@
-0.1.11
+0.1.20

foundry.toml

@@ -4,5 +4,6 @@ out = 'out'
 libs = ['lib']
 test = 'test/'
 cache_path  = 'forge-cache'
+solc-version = "0.8.16"
 
 # See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options

tatus

@@ -0,0 +1,39 @@
+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'

test/FixedPointMathLib.k.sol

@@ -3,36 +3,37 @@ pragma solidity ^0.8.13;
 
 import "forge-std/Test.sol";
 import "solady/src/utils/FixedPointMathLib.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
 
-import "./KevmUtil.sol";
-
-contract FixedPointMathLibVerification is Test, KevmUtil {
+contract FixedPointMathLibVerification is Test, KontrolCheats {
 
     // Constants
     uint256 constant WAD = 1e18;
 
-    function setUp() public {
-        // Make KEVM abstract gas computations
-        kevm.infiniteGas();
-    }
+    function testMulWad(uint256 x, uint256 y) public {
 
-    function testMulWadInRange(uint256 x, uint256 y) public {
-        // Assume x * y won't overflow
-        vm.assume(y == 0 || x <= type(uint256).max / y);
+        if(y == 0 || x <= type(uint256).max / y) {
+            uint256 zSpec = (x * y) / WAD;
+            uint256 zImpl = FixedPointMathLib.mulWad(x, y);
 
-        uint256 zSpec = (x * y) / WAD;
-        uint256 zImpl = FixedPointMathLib.mulWad(x, y);
+            assertEq(zImpl, zSpec);
+        } else {
+            vm.expectRevert(); // FixedPointMathLib.MulWadFailed.selector
+            FixedPointMathLib.mulWad(x, y);
+        }
 
-        assertEq(zImpl, zSpec);
     }
 
-    function testMulWadUpInRange(uint256 x, uint256 y) public {
-        // Assume x * y + WAD/2 won't overflow
-        vm.assume(y == 0 || x <= (type(uint256).max)/y);
+    function testMulWadUp(uint256 x, uint256 y) public {
 
-        uint256 zSpec = ((x * y)/WAD)*WAD < x * y ? (x * y)/WAD + 1 : (x * y)/WAD;
-        uint256 zImpl = FixedPointMathLib.mulWadUp(x, y);
+        if(y == 0 || x <= (type(uint256).max)/y) {
+            uint256 zSpec = ((x * y)/WAD)*WAD < x * y ? (x * y)/WAD + 1 : (x * y)/WAD;
+            uint256 zImpl = FixedPointMathLib.mulWadUp(x, y);
 
-        assertEq(zImpl, zSpec);
+            assertEq(zImpl, zSpec);
+        } else {
+            vm.expectRevert(); // FixedPointMathLib.MulWadFailed.selector
+            FixedPointMathLib.mulWadUp(x, y);
+        }
     }
 }

test/run-kevm.sh

@@ -6,63 +6,55 @@ forge_build() {
     forge build
 }
 
-foundry_kompile() {
-    kevm foundry-kompile --verbose \
-        --require ${lemmas}        \
-        --module-import ${module}  \
-        ${rekompile}               \
-        ${regen}                   \
-        ${llvm_library}
+kontrol_kompile() {
+    kontrol build                     \
+            --verbose                 \
+            --require ${lemmas}       \
+            --module-import ${module} \
+            ${rekompile}
 }
 
-foundry_prove() {
-    kevm foundry-prove                     \
-        --max-depth ${max_depth}           \
-        --max-iterations ${max_iterations} \
-        --bmc-depth ${bmc_depth}           \
-        --workers ${workers}               \
-        --verbose                          \
-        ${reinit}                          \
-        ${debug}                           \
-        ${simplify_init}                   \
-        ${implication_every_block}         \
-        ${break_every_step}                \
-        ${break_on_calls}                  \
-        ${auto_abstract}                   \
-        ${bug_report}                      \
-        ${tests}                           \
-        ${use_booster}                     \
-#        --kore-rpc-command "${kore_rpc_command}"
+kontrol_prove() {
+    kontrol prove                              \
+            --max-depth ${max_depth}           \
+            --max-iterations ${max_iterations} \
+            --smt-timeout ${smt_timeout}       \
+            --workers ${workers}               \
+            --verbose                          \
+            ${reinit}                          \
+            ${debug}                           \
+            ${bug_report}                      \
+            ${simplify_init}                   \
+            ${implication_every_block}         \
+            ${break_every_step}                \
+            ${break_on_calls}                  \
+            ${tests}                           \
+            ${use_booster}
 }
 
-foundry_claim() {
-    kevm prove ${lemmas}                      \
-        --claim ${base_module}-SPEC.${claim}  \
+kontrol_claim() {
+    kevm prove                               \
+        ${lemmas}                            \
+        --claim ${base_module}-SPEC.${claim} \
         --definition out/kompiled            \
-        --spec-module ${base_module}-SPEC
+        --spec-module ${base_module}-SPEC    \
+        --smt-timeout ${smt_timeout}
 }
 
 lemmas=test/solady-lemmas.k
 base_module=SOLADY-LEMMAS
 module=FixedPointMathLibVerification:${base_module}
 
-claim=first-roadblock
-
 max_depth=10000
 max_iterations=10000
-
-bmc_depth=3
+smt_timeout=100000
 
 # 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=16
+workers=12
 
 # Switch the options below to turn them on or off
-# TODO: Describe this thoroughly
-regen=--regen # Regenerates all of the K definition files
-regen=
-
-rekompile=--rekompile # Rekompiles
+rekompile=--rekompile
 #rekompile=
 
 # Progress is saved automatically so an unfinished proof can be resumed from where it left off
@@ -85,33 +77,25 @@ break_every_step=
 break_on_calls=
 break_on_calls=--no-break-on-calls
 
-auto_abstract=--auto-abstract
-auto_abstract=
-auto_abstract=--auto-abstract-gas
-
 bug_report=--bug-report
 bug_report=
 
 # For running the booster
-llvm_library=
-llvm_library=--with-llvm-library
-
-# For running the booster
-use_booster=
 use_booster=--use-booster
-
-kore_rpc_command=
-kore_rpc_command=kore-rpc-booster\ --simplify-after-exec\ --llvm-backend-library\ out/kompiled/llvm-library/interpreter.so
+#use_booster=
 
 # List of tests to symbolically execute
 
 tests=""
-tests+="--test FixedPointMathLibVerification.testMulWadInRange "
-#tests+="--test FixedPointMathLibVerification.testMulWadUpInRange "
+tests+="--test FixedPointMathLibVerification.testMulWad(uint256,uint256) "
+tests+="--test FixedPointMathLibVerification.testMulWadUp "
+
+# Name of the claim to execute
+claim=mulWadUp-first-roadblock
 
 # Comment these lines as needed
 pkill kore-rpc || true
 forge_build
-foundry_kompile
-foundry_prove
-#foundry_claim
+kontrol_kompile
+kontrol_prove
+#kontrol_claim