diff --git a/kontrol.toml b/kontrol.toml new file mode 100644 index 00000000..ebe4d015 --- /dev/null +++ b/kontrol.toml @@ -0,0 +1,57 @@ +[build.default] +foundry-project-root = '.' +regen = false +rekompile = false +verbose = true +debug = false +require = 'test/kontrol/lido-lemmas.k' +module-import = 'VetoSignallingTest:LIDO-LEMMAS' + +[prove.default] +foundry-project-root = '.' +verbose = true +debug = false +max-depth = 10000 +max-iterations = 10000 +reinit = false +cse = false +workers = 16 +max-frontier-parallel = 6 +failure-information = true +counterexample-information = true +minimize-proofs = false +fail-fast = true +smt-timeout = 1000 +smt-retry-limit = 5 +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 = [ + "RageQuitTest.testRageQuitDuration", + "VetoCooldownTest.testVetoCooldownDuration", + "VetoSignallingTest.testTransitionNormalToVetoSignalling", + "VetoSignallingTest.testVetoSignallingInvariantsHoldInitially", + "VetoSignallingTest.testVetoSignallingInvariantsArePreserved", + "VetoSignallingTest.testDeactivationNotCancelled", + "EscrowAccountingTest.testRageQuitSupport", + "EscrowAccountingTest.testEscrowInvariantsHoldInitially", + "EscrowLockUnlockTest.testLockStEth", + #"EscrowAccountingTest.testUnlockStEth", + #"EscrowOperationsTest.testCannotUnlockBeforeMinLockTime", + #"EscrowOperationsTest.testCannotLockUnlockInRageQuitEscrowState", + #"EscrowOperationsTest.testCannotWithdrawBeforeEthClaimTimelockElapsed", + "ProposalOperationsTest.testOnlyAdminProposersCanCancelProposals", + "ProposalOperationsTest.testCannotProposeInInvalidState", + #"ActivateNextStateTest.testEscrowStateTransition" + ] +# bug-report = disabled by default + +[show.default] +foundry-project-root = '.' +verbose = true +debug = false \ No newline at end of file diff --git a/test/kontrol/scripts/common.sh b/test/kontrol/scripts/common.sh index 7a631a7b..de684fea 100755 --- a/test/kontrol/scripts/common.sh +++ b/test/kontrol/scripts/common.sh @@ -32,7 +32,7 @@ usage_other() { exit 0 } -# Set Run Directory /packages/contracts-bedrock +# Set Run Directory /, This is where the foundtry.toml file generally is located. WORKSPACE_DIR=$( cd "$SCRIPT_HOME/../../.." >/dev/null 2>&1 && pwd ) pushd "$WORKSPACE_DIR" > /dev/null || exit @@ -170,11 +170,9 @@ copy_to_docker() { } clean_docker(){ - trap if [ "$LOCAL" = false ]; then notif "Cleaning Docker Container" - docker stop "$CONTAINER_NAME" > /dev/null 2>&1 || true - docker rm "$CONTAINER_NAME" > /dev/null 2>&1 || true + docker stop "$CONTAINER_NAME" > /dev/null 2>&1 sleep 2 # Give time for system to clean up container else notif "Not Running in Container. Done." diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh index e8874bc8..46083511 100755 --- a/test/kontrol/scripts/run-kontrol.sh +++ b/test/kontrol/scripts/run-kontrol.sh @@ -5,7 +5,7 @@ SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" # shellcheck source=/dev/null source "$SCRIPT_HOME/common.sh" export RUN_KONTROL=true -CUSTOM_FOUNDRY_PROFILE=kprove +CUSTOM_FOUNDRY_PROFILE=default export FOUNDRY_PROFILE=$CUSTOM_FOUNDRY_PROFILE export OUT_DIR=kout # out dir of $FOUNDRY_PROFILE parse_args "$@" @@ -16,32 +16,14 @@ parse_args "$@" kontrol_build() { notif "Kontrol Build" # shellcheck disable=SC2086 - run kontrol build \ - --verbose \ - --require $lemmas \ - --module-import $module \ - $rekompile + run kontrol build return $? } kontrol_prove() { notif "Kontrol Prove" # shellcheck disable=SC2086 - run kontrol prove \ - --verbose \ - --max-depth $max_depth \ - --max-iterations $max_iterations \ - --smt-timeout $smt_timeout \ - --workers $workers \ - --max-frontier-parallel $max_frontier_parallel \ - --smt-retry-limit 5 \ - $reinit \ - $bug_report \ - $break_on_calls \ - $break_every_step \ - $auto_abstract \ - $tests \ - $use_booster + run kontrol prove return $? } @@ -51,8 +33,8 @@ get_log_results(){ LOG_PATH="$SCRIPT_HOME/logs" RESULTS_LOG="$LOG_PATH/$RESULTS_FILE" - if [ ! -d "$LOG_PATH" ]; then - mkdir "$LOG_PATH" + if [ ! -d $LOG_PATH ]; then + mkdir $LOG_PATH fi notif "Generating Results Log: $LOG_PATH" @@ -62,7 +44,7 @@ get_log_results(){ mv results.tar.gz "$RESULTS_LOG" else docker cp "$CONTAINER_NAME:/home/user/workspace/results.tar.gz" "$RESULTS_LOG" - tar -xzvf "$RESULTS_LOG" + tar -xzvf "$RESULTS_LOG" > /dev/null 2>&1 fi if [ -f "$RESULTS_LOG" ]; then cp "$RESULTS_LOG" "$LOG_PATH/kontrol-results_latest.tar.gz" @@ -79,91 +61,12 @@ get_log_results(){ fi } -######################### -# kontrol build options # -######################### -# NOTE: This script has a recurring pattern of setting and unsetting variables, -# such as `rekompile`. Such a pattern is intended for easy use while locally -# developing and executing the proofs via this script. Comment/uncomment the -# empty assignment to activate/deactivate the corresponding flag -lemmas=test/kontrol/lido-lemmas.k -base_module=LIDO-LEMMAS -module=VetoSignallingTest:$base_module -rekompile=--rekompile -rekompile= -regen=--regen -# shellcheck disable=SC2034 -regen= - -################################# -# Tests to symbolically execute # -################################# -test_list=() -if [ "$SCRIPT_TESTS" == true ]; then - # Here go the list of tests to execute with the `script` option - test_list=( - "RageQuitTest.testRageQuitDuration" - "VetoCooldownTest.testVetoCooldownDuration" - "VetoSignallingTest.testTransitionNormalToVetoSignalling" - "VetoSignallingTest.testVetoSignallingInvariantsHoldInitially" - "VetoSignallingTest.testVetoSignallingInvariantsArePreserved" - "VetoSignallingTest.testDeactivationNotCancelled" - "EscrowAccountingTest.testRageQuitSupport" - "EscrowAccountingTest.testEscrowInvariantsHoldInitially" - "EscrowLockUnlockTest.testLockStEth" - #"EscrowAccountingTest.testUnlockStEth" - #"EscrowOperationsTest.testCannotUnlockBeforeMinLockTime" - #"EscrowOperationsTest.testCannotLockUnlockInRageQuitEscrowState" - #"EscrowOperationsTest.testCannotWithdrawBeforeEthClaimTimelockElapsed" - "ProposalOperationsSetup.testOnlyAdminProposersCanCancelProposals" - "ProposalOperationsSetup.testCannotProposeInInvalidState" - #"ActivateNextStateTest.testEscrowStateTransition" - ) -elif [ "$CUSTOM_TESTS" != 0 ]; then - test_list=( "${@:${CUSTOM_TESTS}}" ) -fi -tests="" -# If test_list is empty, tests will be empty as well -# This will make kontrol execute any `test`, `prove` or `check` prefixed-function -# under the foundry-defined `test` directory -for test_name in "${test_list[@]}"; do - tests+="--match-test $test_name " -done - -######################### -# kontrol prove options # -######################### -max_depth=10000 -max_iterations=10000 -smt_timeout=1000 -max_workers=16 # Should be at most (M - 8) / 8 in a machine with M GB of RAM -# workers is the minimum between max_workers and the length of test_list -# unless no test arguments are provided, in which case we default to max_workers -if [ "$CUSTOM_TESTS" == 0 ] && [ "$SCRIPT_TESTS" == false ]; then - workers=${max_workers} -else - workers=$((${#test_list[@]}>max_workers ? max_workers : ${#test_list[@]})) -fi -max_frontier_parallel=6 -reinit=--reinit -reinit= -break_on_calls=--no-break-on-calls -break_on_calls= -break_every_step=--no-break-every-step -break_every_step= -auto_abstract=--auto-abstract-gas -auto_abstract= -bug_report=--bug-report -bug_report= -use_booster=--no-use-booster -use_booster= - ############# # RUN TESTS # ############# # Set up the trap to run the function on failure -trap on_failure ERR INT +trap on_failure ERR INT TERM trap clean_docker EXIT conditionally_start_docker diff --git a/test/kontrol/scripts/versions.json b/test/kontrol/scripts/versions.json index 4b191f7c..8771b23d 100644 --- a/test/kontrol/scripts/versions.json +++ b/test/kontrol/scripts/versions.json @@ -1,4 +1,4 @@ { - "kontrol": "0.1.409", + "kontrol": "0.1.415", "kontrol-cheatcodes": "master" }