From 406f40436c37d5259ce0e766281c4d7128386f7f Mon Sep 17 00:00:00 2001 From: lucasmt Date: Tue, 28 May 2024 18:32:08 -0500 Subject: [PATCH 1/3] Add files for Kontrol CI --- .github/workflows/lido-ci.yml | 46 ++++++ test/kontrol/scripts/common.sh | 211 ++++++++++++++++++++++++++++ test/kontrol/scripts/run-kontrol.sh | 176 +++++++++++++++++++++++ test/kontrol/scripts/versions.json | 4 + 4 files changed, 437 insertions(+) create mode 100644 .github/workflows/lido-ci.yml create mode 100755 test/kontrol/scripts/common.sh create mode 100755 test/kontrol/scripts/run-kontrol.sh create mode 100644 test/kontrol/scripts/versions.json diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml new file mode 100644 index 00000000..c8204248 --- /dev/null +++ b/.github/workflows/lido-ci.yml @@ -0,0 +1,46 @@ +--- + name: "Test Proofs" + on: + workflow_dispatch: + pull_request: + branches: + - main + jobs: + test: + runs-on: [self-hosted, linux, flyweight] + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + ref: ${{ github.event.pull_request.head.sha }} + + - name: Run Proofs in KaaS + run: | + sha=$(git rev-parse HEAD) + branch_name=$(git rev-parse --abbrev-ref HEAD) + response=$(curl -X POST \ + -w "%{http_code}" \ + -H "Accept: application/vnd.github+json" \ + -H "Authorization: Bearer ${{ secrets.KAAS_COMPUTE_TOKEN }}" \ + https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \ + -d '{ + "ref": "master", + "inputs": { + "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", + "extra_args": "script", + "statuses_sha": "'$sha'", + "org": "runtimeverification", + "repository": "_audits_lidofinance_dual-governance", + "auth_token": "'"${{ secrets.KAAS_COMPUTE_TOKEN }}"'" + } + }') + + if [ "$response" -ge 200 ] && [ "$response" -lt 300 ]; then + echo "The request was successful" + elif [ "$response" -ge 400 ] && [ "$response" -lt 500 ]; then + echo "There was a client error: $response" + exit 1 + else + echo "There was a server error: $response" + exit 1 + fi diff --git a/test/kontrol/scripts/common.sh b/test/kontrol/scripts/common.sh new file mode 100755 index 00000000..7a631a7b --- /dev/null +++ b/test/kontrol/scripts/common.sh @@ -0,0 +1,211 @@ +#!/bin/bash +# Common functions and variables for run-kontrol.sh and make-summary-deployment.sh + +notif() { echo "== $0: $*" >&2 ; } + +# usage function for the run-kontrol.sh script +usage_run_kontrol() { + echo "Usage: $0 [-h|--help] [container|local|dev] [script|tests]" 1>&2 + echo "" 1>&2 + echo " -h, --help Display this help message." 1>&2 + echo "" 1>&2 + echo "Execution modes:" + echo " container Run in docker container. Reproduce CI execution. (Default)" 1>&2 + echo " local Run locally, enforces registered versions.json version for better reproducibility. (Recommended)" 1>&2 + echo " dev Run locally, does NOT enforce registered version. (Useful for developing with new versions and features)" 1>&2 + echo "" 1>&2 + echo "Tests executed:" + echo " script Execute the tests recorded in run-kontrol.sh" 1>&2 + echo " tests Execute the tests provided as arguments" 1>&2 + exit 0 +} + +# placeholder usage function for any other scripts +usage_other() { + echo "Usage: $0 [-h|--help] OPTIONS" 1>&2 + echo "" 1>&2 + echo " -h, --help Display this help message." 1>&2 + echo "" 1>&2 + echo "Further Options:" + echo " option1 Description1. (Default)" 1>&2 + echo " Option2 Description2. (Recommended)" 1>&2 + exit 0 +} + +# Set Run Directory /packages/contracts-bedrock +WORKSPACE_DIR=$( cd "$SCRIPT_HOME/../../.." >/dev/null 2>&1 && pwd ) +pushd "$WORKSPACE_DIR" > /dev/null || exit + +# Variables +export CONTAINER_NAME=kontrol-tests +KONTROLRC=$(jq -r .kontrol < "$WORKSPACE_DIR/test/kontrol/scripts/versions.json") +export KONTROL_RELEASE=$KONTROLRC +export LOCAL=false +export SCRIPT_TESTS=false +SCRIPT_OPTION=false +export CUSTOM_TESTS=0 # Store the position where custom tests start, interpreting 0 as no tests +CUSTOM_OPTION=0 +export RUN_KONTROL=false # true if any functions are called from run-kontrol.sh + +# General usage function, which discerns from which script is being called and displays the appropriate message +usage() { + if [ "$RUN_KONTROL" = "true" ]; then + usage_run_kontrol + else + usage_other + fi +} + + +# Argument Parsing +# The logic behind argument parsing is the following (in order): +# - Execution mode argument: container (or empty), local, dev +# - Tests arguments (first if execution mode empty): script, specific test names +parse_args() { + if [ $# -eq 0 ]; then + export LOCAL=false + export SCRIPT_TESTS=false + export CUSTOM_TESTS=0 + # `script` argument caps the total possible arguments to its position + elif { [ $# -gt 1 ] && [ "$1" == "script" ]; } || { [ $# -gt 2 ] && [ "$2" == "script" ]; }; then + usage + elif [ $# -eq 1 ]; then + SCRIPT_OPTION=false + CUSTOM_OPTION=0 + parse_first_arg "$1" + elif [ $# -eq 2 ] && [ "$2" == "script" ]; then + if [ "$1" != "container" ] && [ "$1" != "local" ] && [ "$1" != "dev" ]; then + notif "Invalid first argument. Must be \`container\`, \`local\` or \`dev\`" + exit 1 + fi + SCRIPT_OPTION=true + CUSTOM_OPTION=0 + parse_first_arg "$1" + else + SCRIPT_OPTION=false + CUSTOM_OPTION=2 + parse_first_arg "$1" + fi +} + +# Parse the first argument passed to `run-kontrol.sh` +parse_first_arg() { + if [ "$1" == "container" ]; then + notif "Running in docker container (DEFAULT)" + export LOCAL=false + export SCRIPT_TESTS=$SCRIPT_OPTION + export CUSTOM_TESTS=$CUSTOM_OPTION + elif [ "$1" == "-h" ] || [ "$1" == "--help" ]; then + usage + elif [ "$1" == "local" ]; then + notif "Running with LOCAL install, .kontrolrc CI version ENFORCED" + export SCRIPT_TESTS=$SCRIPT_OPTION + export CUSTOM_TESTS=$CUSTOM_OPTION + check_kontrol_version + elif [ "$1" == "dev" ]; then + notif "Running with LOCAL install, IGNORING .kontrolrc version" + export LOCAL=true + export SCRIPT_TESTS=$SCRIPT_OPTION + export CUSTOM_TESTS=$CUSTOM_OPTION + elif [ "$1" == "script" ]; then + notif "Running in docker container (DEFAULT)" + export LOCAL=false + NEGATED_SCRIPT_TESTS=$([[ "${SCRIPT_OPTION}" == "true" ]] && echo false || echo true) + export SCRIPT_TESTS=$NEGATED_SCRIPT_TESTS + export CUSTOM_TESTS=$CUSTOM_OPTION + else + notif "Running in docker container (DEFAULT)" + export LOCAL=false + export SCRIPT_TESTS=$SCRIPT_OPTION + export CUSTOM_TESTS=1 # Store the position where custom tests start + fi +} + +check_kontrol_version() { + if [ "$(kontrol version | awk -F': ' '{print$2}')" == "$KONTROLRC" ]; then + notif "Kontrol version matches $KONTROLRC" + export LOCAL=true + else + notif "Kontrol version does NOT match $KONTROLRC" + notif "Please run 'kup install kontrol --version v$KONTROLRC'" + exit 1 + fi +} + +conditionally_start_docker() { + if [ "$LOCAL" == false ]; then + # Is old docker container running? + if [ "$(docker ps -q -f name="$CONTAINER_NAME")" ]; then + # Stop old docker container + notif "Stopping old docker container" + clean_docker + fi + start_docker + fi +} + +start_docker () { + docker run \ + --name "$CONTAINER_NAME" \ + --rm \ + --interactive \ + --detach \ + --env FOUNDRY_PROFILE="$FOUNDRY_PROFILE" \ + --workdir /home/user/workspace \ + runtimeverificationinc/kontrol:ubuntu-jammy-"$KONTROL_RELEASE" + + copy_to_docker +} + +copy_to_docker() { + # Copy test content to container + if [ "$LOCAL" == false ]; then + TMP_DIR=$(mktemp -d) + cp -r "$WORKSPACE_DIR/." "$TMP_DIR" + docker cp --follow-link "$TMP_DIR/." $CONTAINER_NAME:/home/user/workspace + rm -rf "$TMP_DIR" + + docker exec --user root "$CONTAINER_NAME" chown -R user:user /home/user + fi +} + +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 + sleep 2 # Give time for system to clean up container + else + notif "Not Running in Container. Done." + fi +} + + + +docker_exec () { + docker exec --user user --workdir /home/user/workspace $CONTAINER_NAME "${@}" +} + +run () { + if [ "$LOCAL" = true ]; then + notif "Running local" + # shellcheck disable=SC2086 + "${@}" + else + notif "Running in docker" + docker_exec "${@}" + fi +} + +# Define the function to run on failure +on_failure() { + get_log_results + + if [ "$LOCAL" = false ]; then + clean_docker + fi + + notif "Failure Cleanup Complete." + exit 1 +} diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh new file mode 100755 index 00000000..d649f2d8 --- /dev/null +++ b/test/kontrol/scripts/run-kontrol.sh @@ -0,0 +1,176 @@ +#!/bin/bash +set -euo pipefail + +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=default +export FOUNDRY_PROFILE=$CUSTOM_FOUNDRY_PROFILE +export OUT_DIR=out # out dir of $FOUNDRY_PROFILE +parse_args "$@" + +############# +# Functions # +############# +kontrol_build() { + notif "Kontrol Build" + # shellcheck disable=SC2086 + run kontrol build \ + --verbose \ + --require $lemmas \ + --module-import $module \ + $rekompile + return $? +} + +kontrol_prove() { + notif "Kontrol Prove" + # shellcheck disable=SC2086 + run kontrol prove \ + --max-depth $max_depth \ + --max-iterations $max_iterations \ + --smt-timeout $smt_timeout \ + --workers $workers \ + $reinit \ + $bug_report \ + $break_on_calls \ + $break_every_step \ + $auto_abstract \ + $tests \ + $use_booster + return $? +} + +get_log_results(){ + trap clean_docker ERR + RESULTS_FILE="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz" + LOG_PATH="$SCRIPT_HOME/logs" + RESULTS_LOG="$LOG_PATH/$RESULTS_FILE" + + if [ ! -d "$LOG_PATH" ]; then + mkdir "$LOG_PATH" + fi + + notif "Generating Results Log: $LOG_PATH" + + run tar -czvf results.tar.gz "$OUT_DIR" > /dev/null 2>&1 + if [ "$LOCAL" = true ]; then + mv results.tar.gz "$RESULTS_LOG" + else + docker cp "$CONTAINER_NAME:/home/user/workspace/results.tar.gz" "$RESULTS_LOG" + tar -xzvf "$RESULTS_LOG" + fi + if [ -f "$RESULTS_LOG" ]; then + cp "$RESULTS_LOG" "$LOG_PATH/kontrol-results_latest.tar.gz" + else + notif "Results Log: $RESULTS_LOG not found, skipping.." + fi + # Report where the file was generated and placed + notif "Results Log: $(dirname "$RESULTS_LOG") generated" + + if [ "$LOCAL" = false ]; then + notif "Results Log: $RESULTS_LOG generated" + RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log" + docker logs "$CONTAINER_NAME" > "$LOG_PATH/$RUN_LOG" + 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=( "VetoSignallingTest.testTransitionNormalToVetoSignalling" ) +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=100000 +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 +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 clean_docker EXIT +conditionally_start_docker + +results=() +# Run kontrol_build and store the result +kontrol_build +results[0]=$? + +# Run kontrol_prove and store the result +kontrol_prove +results[1]=$? + +get_log_results + +# Now you can use ${results[0]} and ${results[1]} +# to check the results of kontrol_build and kontrol_prove, respectively +if [ ${results[0]} -ne 0 ] && [ ${results[1]} -ne 0 ]; then + echo "Kontrol Build and Prove Failed" + exit 1 +elif [ ${results[0]} -ne 0 ]; then + echo "Kontrol Build Failed" + exit 1 +elif [ ${results[1]} -ne 0 ]; then + echo "Kontrol Prove Failed" + exit 2 + # Handle failure +else + echo "Kontrol Passed" +fi + +notif "DONE" diff --git a/test/kontrol/scripts/versions.json b/test/kontrol/scripts/versions.json new file mode 100644 index 00000000..38350d43 --- /dev/null +++ b/test/kontrol/scripts/versions.json @@ -0,0 +1,4 @@ +{ + "kontrol": "0.1.242", + "kontrol-cheatcodes": "master" +} From 9e8c20a333f7e55d3f728e9de5eb870825f14eff Mon Sep 17 00:00:00 2001 From: lucasmt Date: Thu, 30 May 2024 15:15:28 -0500 Subject: [PATCH 2/3] Tweaks to lido-ci.yml --- .github/workflows/lido-ci.yml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index c8204248..8e66ddee 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -1,13 +1,12 @@ --- name: "Test Proofs" on: - workflow_dispatch: pull_request: branches: - main jobs: test: - runs-on: [self-hosted, linux, flyweight] + runs-on: ubuntu-latest steps: - name: Checkout uses: actions/checkout@v4 @@ -21,7 +20,7 @@ response=$(curl -X POST \ -w "%{http_code}" \ -H "Accept: application/vnd.github+json" \ - -H "Authorization: Bearer ${{ secrets.KAAS_COMPUTE_TOKEN }}" \ + -H "Authorization: Bearer ${{ secrets.RV_COMPUTE_TOKEN }}" \ https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \ -d '{ "ref": "master", @@ -31,7 +30,7 @@ "statuses_sha": "'$sha'", "org": "runtimeverification", "repository": "_audits_lidofinance_dual-governance", - "auth_token": "'"${{ secrets.KAAS_COMPUTE_TOKEN }}"'" + "auth_token": "'"${{ secrets.LIDO_STATUS_TOKEN }}"'" } }') From f6233ec65caff64c6218388340dc5aa84f0ec97d Mon Sep 17 00:00:00 2001 From: lucasmt Date: Fri, 31 May 2024 15:34:22 -0500 Subject: [PATCH 3/3] Further tweaks to lido-ci.yml --- .github/workflows/lido-ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 8e66ddee..9d60dea3 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -28,8 +28,8 @@ "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", "extra_args": "script", "statuses_sha": "'$sha'", - "org": "runtimeverification", - "repository": "_audits_lidofinance_dual-governance", + "org": "lidofinance", + "repository": "dual-governance", "auth_token": "'"${{ secrets.LIDO_STATUS_TOKEN }}"'" } }')