diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index ac9e2534..e24998df 100644 --- a/.github/actions/with-docker/action.yml +++ b/.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 diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 00ffe4b9..f2a81389 100644 --- a/.github/workflows/test-pr.yml +++ b/.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 diff --git a/.gitmodules b/.gitmodules index 0f078158..3713949c 100644 --- a/.gitmodules +++ b/.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 diff --git a/README.md b/README.md index 5e7879cc..02cac830 100644 --- a/README.md +++ b/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 diff --git a/deps/kontrol_release b/deps/kontrol_release index 7e72641b..915812ec 100644 --- a/deps/kontrol_release +++ b/deps/kontrol_release @@ -1 +1 @@ -0.1.22 +0.1.22 \ No newline at end of file diff --git a/foundry.toml b/foundry.toml index 3bedc663..718422e9 100644 --- a/foundry.toml +++ b/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 diff --git a/lib/kontrol-cheatcodes b/lib/kontrol-cheatcodes new file mode 160000 index 00000000..2c48ae1a --- /dev/null +++ b/lib/kontrol-cheatcodes @@ -0,0 +1 @@ +Subproject commit 2c48ae1ab44228c199dca29414c0b4b18a3434e6 diff --git a/tatus b/tatus new file mode 100644 index 00000000..b3ce00de --- /dev/null +++ b/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' diff --git a/test/FixedPointMathLib.k.sol b/test/FixedPointMathLib.k.sol index 59a9f88e..914f9a63 100644 --- a/test/FixedPointMathLib.k.sol +++ b/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); + } } } diff --git a/test/run-kevm.sh b/test/run-kevm.sh old mode 100644 new mode 100755 index 2fd2a998..458e39a4 --- a/test/run-kevm.sh +++ b/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 diff --git a/test/solady-lemmas.k b/test/solady-lemmas.k index f0c8382c..d3f301a5 100644 --- a/test/solady-lemmas.k +++ b/test/solady-lemmas.k @@ -21,15 +21,25 @@ module SOLADY-LEMMAS rule runLemma(T) => doneLemma(T) ... + // // Bool - rule notBool notBool X => X [simplification] + // - rule [boolOfTrue]: bool2Word ( X ) => 1 requires X [simplification] - rule [boolOfFalse]: bool2Word ( X ) => 0 requires notBool X [simplification] + rule bool2Word ( X ) => 1 requires X [simplification] + rule bool2Word ( X ) => 0 requires notBool X [simplification] - rule X /Word Y false - requires X >=Int 0 - andBool Y >=Int 0 + // + // ML + // + + rule #Not ( { false #Equals X:Bool andBool Y:Bool } ) => {true #Equals X } #And { true #Equals Y } [simplification] + + // + // Arithmetic + // + + rule X xorInt maxUInt256 => maxUInt256 -Int X + requires #rangeUInt ( 256 , X ) [simplification] endmodule @@ -38,6 +48,21 @@ module SOLADY-LEMMAS-SPEC imports SOLADY-LEMMAS claim [first-roadblock]: runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int doneLemma(0) ... + claim [mulWad-first-roadblock]: runLemma(bool2Word( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int doneLemma(0) ... requires 0 <=Int X + claim [mulWadUp-second-roadblock]: runLemma( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int doneLemma(false) ... + requires ( notBool ( notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int runLemma( ( ( notBool ( ( notBool ( ( X:Int *Int Y:Int ) /Int 1000000000000000000 ) ==Int 0 ) andBool maxUInt256 /Word ( ( X:Int *Int Y:Int ) /Int 1000000000000000000 ) doneLemma(true) ... + requires notBool ( ( notBool X:Int ==Int 0 ) andBool maxUInt256 /Word X:Int