From 641ac357b8787e8a462b418a109b347182482491 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 26 Sep 2024 09:42:52 -0600 Subject: [PATCH] Update dependency: deps/kontrol_release (#48) * deps/kontrol_release: Set Version 1.0.2 * deps/kontrol_release: Set Version 1.0.3 * deps/kontrol_release: Set Version 1.0.4 * deps/kontrol_release: Set Version 1.0.5 * deps/kontrol_release: Set Version 1.0.6 * deps/kontrol_release: Set Version 1.0.7 * deps/kontrol_release: Set Version 1.0.8 * deps/kontrol_release: Set Version 1.0.9 * deps/kontrol_release: Set Version 1.0.10 * deps/kontrol_release: Set Version 1.0.11 * deps/kontrol_release: Set Version 1.0.12 * deps/kontrol_release: Set Version 1.0.17 * deps/kontrol_release: Set Version 1.0.18 * deps/kontrol_release: Set Version 1.0.19 * deps/kontrol_release: Set Version 1.0.21 * deps/kontrol_release: Set Version 1.0.22 * deps/kontrol_release: Set Version 1.0.23 * deps/kontrol_release: Set Version 1.0.24 * deps/kontrol_release: Set Version 1.0.25 * deps/kontrol_release: Set Version 1.0.26 * deps/kontrol_release: Set Version 1.0.27 * deps/kontrol_release: Set Version 1.0.28 * deps/kontrol_release: Set Version 1.0.29 * deps/kontrol_release: Set Version 1.0.30 * deps/kontrol_release: Set Version 1.0.31 * deps/kontrol_release: Set Version 1.0.32 * adapting lemmas * increasing parallelisation * deps/kontrol_release: Set Version 1.0.33 * deps/kontrol_release: Set Version 1.0.34 --------- Co-authored-by: devops Co-authored-by: Petar Maksimovic --- .github/workflows/test-pr.yml | 4 +- deps/kontrol_release | 2 +- kontrol.toml | 50 ++++++++++++++++ test/run-kevm.sh | 104 ---------------------------------- test/run-kontrol.sh | 77 ------------------------- test/solady-lemmas.k | 12 ++-- 6 files changed, 59 insertions(+), 190 deletions(-) create mode 100644 kontrol.toml delete mode 100755 test/run-kevm.sh delete mode 100755 test/run-kontrol.sh diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 8bff053b7..b5ae8c282 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -20,7 +20,7 @@ jobs: with: token: ${{ secrets.JENKINS_GITHUB_PAT }} fetch-depth: 0 - + - name: 'Get Kontrol Version' run: | set -euo pipefail @@ -43,7 +43,7 @@ jobs: - name: 'Run Kontrol' run: | # Run the following in the running docker container - docker exec -u user ${{ env.repository_basename }}-ci bash -c './test/run-kevm.sh' + docker exec -u user ${{ env.repository_basename }}-ci bash -c 'kontrol build; kontrol prove --maintenance-rate 128' - name: 'Stop Docker Container' if: always() diff --git a/deps/kontrol_release b/deps/kontrol_release index 7dea76edb..ffcbe7136 100644 --- a/deps/kontrol_release +++ b/deps/kontrol_release @@ -1 +1 @@ -1.0.1 +1.0.34 diff --git a/kontrol.toml b/kontrol.toml new file mode 100644 index 000000000..8aea2cbe8 --- /dev/null +++ b/kontrol.toml @@ -0,0 +1,50 @@ +[build.default] +foundry-project-root = '.' +regen = true +rekompile = true +verbose = false +debug = false +require = 'test/solady-lemmas.k' +module-import = 'FixedPointMathLibVerification:SOLADY-LEMMAS' +ast = true +auxiliary-lemmas = true + +[prove.default] +foundry-project-root = '.' +verbose = false +debug = false +max-depth = 100000 +max-iterations = 10000 +reinit = false +cse = false +workers = 1 +max-frontier-parallel = 16 +maintenance-rate = 128 +assume-defined = true +no-log-rewrites = true +kore-rpc-command = 'kore-rpc-booster --no-post-exec-simplify' +failure-information = true +counterexample-information = true +minimize-proofs = false +fail-fast = true +smt-timeout = 16000 +smt-retry-limit = 0 +break-every-step = false +break-on-jumpi = false +break-on-calls = false +break-on-storage = false +break-on-basic-blocks = false +break-on-cheatcodes = false +auto_abstract = true +run-constructor = false +match-test = [ + "FixedPointMathLibVerification.testMulWad(uint256,uint256)", + "FixedPointMathLibVerification.testMulWadUp", + "FixedPointMathLibVerification.testLog2" + ] +ast = true + +[show.default] +foundry-project-root = '.' +verbose = true +debug = false \ No newline at end of file diff --git a/test/run-kevm.sh b/test/run-kevm.sh deleted file mode 100755 index c0c996e3d..000000000 --- a/test/run-kevm.sh +++ /dev/null @@ -1,104 +0,0 @@ -#!/bin/bash - -set -euxo pipefail - -forge_build() { - forge build -} - -kontrol_kompile() { - GHCRTS='' kontrol build \ - --verbose \ - --require ${lemmas} \ - --module-import ${module} \ - ${rekompile} -} - -kontrol_prove() { - export GHCRTS='-N6' - 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} \ - --max-frontier-parallel 6 \ - --kore-rpc-command 'kore-rpc-booster --equation-max-recursion 10' -} - -kontrol_claim() { - kevm prove \ - ${lemmas} \ - --claim ${base_module}-SPEC.${claim} \ - --definition out/kompiled \ - --spec-module ${base_module}-SPEC \ - --smt-timeout ${smt_timeout} -} - -lemmas=test/solady-lemmas.k -base_module=SOLADY-LEMMAS -module=FixedPointMathLibVerification:${base_module} - -max_depth=10000 -max_iterations=10000 -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=3 - -# Switch the options below to turn them on or off -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= - -debug=--debug -debug= - -simplify_init=--no-simplify-init -simplify_init= - -implication_every_block=--no-implication-every-block -implication_every_block= - -break_every_step=--break-every-step -break_every_step= - -break_on_calls= -break_on_calls=--no-break-on-calls - -bug_report=--bug-report -bug_report= - -# 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 " -tests+="--match-test FixedPointMathLibVerification.testLog2 " - -# Name of the claim to execute -claim=log2-06 - -# Comment these lines as needed -pkill kore-rpc || true -forge_build -kontrol_kompile -kontrol_prove -#kontrol_claim diff --git a/test/run-kontrol.sh b/test/run-kontrol.sh deleted file mode 100755 index 4dbb42b66..000000000 --- a/test/run-kontrol.sh +++ /dev/null @@ -1,77 +0,0 @@ -#!/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 diff --git a/test/solady-lemmas.k b/test/solady-lemmas.k index 49dcfe4b7..d6440e102 100644 --- a/test/solady-lemmas.k +++ b/test/solady-lemmas.k @@ -96,11 +96,11 @@ module SOLADY-LEMMAS requires 0 <=Int A andBool A A A A /Int C <=Int B + rule A <=Int C *Int B => A /Int C <=Int B requires A modInt C ==Int 0 [simplification, concrete(A, C)] @@ -114,22 +114,22 @@ module SOLADY-LEMMAS syntax Int ::= "cachedBytesConstant" [alias] rule cachedBytesConstant => 6928917744019834342450304135053993530982274426945361611473370484834304 - rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 0 + rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 0 requires 0 <=Int Y andBool Y =Int 16 ) [simplification] - rule ( cachedBytesConstant >>Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 1 + rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 1 requires 0 <=Int Y andBool Y >Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 2 + rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 2 requires 0 <=Int Y andBool Y >Int ( ( maxUInt5 -Int Y ) *Int 8 ) ) modInt 256 => 3 + rule ( cachedBytesConstant >>Int ( 8 *Int ( maxUInt5 -Int Y ) ) ) modInt 256 => 3 requires 0 <=Int Y andBool Y