Merge pull request #8271 from runtimeverification/rv/feature-ci

contracts-bedrock: add Kontrol CI setup

.circleci/config.yml

@@ -1336,6 +1336,45 @@ jobs:
           name: Verify Values Match
           command: |
             ./ops/scripts/ci-match-values-between-files.sh "<< parameters.file1_path >>" "<< parameters.pattern_file1 >>" "<< parameters.file2_path >>" "<< parameters.pattern_file2 >>"
+
+  kontrol-tests:
+    docker:
+      - image: << pipeline.parameters.ci_builder_image >>
+    resource_class: xlarge
+    steps:
+      - checkout
+      - run:
+          name: Checkout Submodule
+          command: |
+            git submodule update --init --recursive
+      - check-changed:
+          patterns: contracts-bedrock/test/kontrol,contracts-bedrock/src/L1/OptimismPortal\.sol
+      - setup_remote_docker:
+          docker_layer_caching: true
+      - run: 
+          name: Install Docker CLI
+          command: |
+            # Add Docker's official GPG key:
+            apt-get update
+            apt-get install ca-certificates curl gnupg
+            install -m 0755 -d /etc/apt/keyrings
+            curl -fsSL https://download.docker.com/linux/debian/gpg | gpg --dearmor -o /etc/apt/keyrings/docker.gpg
+            chmod a+r /etc/apt/keyrings/docker.gpg
+            # Add the repository to Apt sources:
+            echo \
+              "deb [arch=$(dpkg --print-architecture) signed-by=/etc/apt/keyrings/docker.gpg] https://download.docker.com/linux/debian \
+              $(. /etc/os-release && echo "$VERSION_CODENAME") stable" | \
+              tee /etc/apt/sources.list.d/docker.list > /dev/null
+            apt-get update
+            apt-get install -y docker-ce-cli
+      - run:
+          name: Run Kontrol Tests
+          command: |
+            pnpm test:kontrol 
+          working_directory: ./packages/contracts-bedrock
+      - store_artifacts:
+          path: ./packages/contracts-bedrock/kontrol-results_latest.tar.gz
+
 workflows:
   main:
     when:
@@ -1588,6 +1627,7 @@ workflows:
       - check-generated-mocks-op-service
       - cannon-go-lint-and-test
       - cannon-build-test-vectors
+      - kontrol-tests
   release:
     when:
       not:

.kontrolrc

+0.1.74

packages/contracts-bedrock/.gitignore

@@ -3,6 +3,8 @@ artifacts
 forge-artifacts
 cache
 broadcast
+kout
+test/kontrol/kontrol/logs
 
 # Metrics
 coverage.out

packages/contracts-bedrock/foundry.toml

@@ -62,3 +62,13 @@ runs = 512
 
 [profile.lite]
 optimizer = false
+
+################################################################
+#                         PROFILE: KONTROL                     #
+################################################################
+
+[profile.kontrol]
+src = 'src/L1'
+out = 'kout'
+test = 'test/kontrol'
+script = 'scripts-kontrol'

packages/contracts-bedrock/package.json

@@ -18,6 +18,7 @@
     "build:go-ffi": "(cd scripts/go-ffi && go build)",
     "autogen:invariant-docs": "npx tsx scripts/invariant-doc-gen.ts",
     "test": "pnpm build:go-ffi && forge test",
+    "test:kontrol": "./test/kontrol/kontrol/run-kontrol.sh",
     "genesis": "./scripts/generate-l2-genesis.sh",
     "coverage": "pnpm build:go-ffi && forge coverage",
     "coverage:lcov": "pnpm build:go-ffi && forge coverage --report lcov",

packages/contracts-bedrock/test/kontrol/Counter.sol

+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+contract Counter {
+    uint256 public number;
+
+    function setNumber(uint256 newNumber) public {
+        number = newNumber;
+    }
+}

packages/contracts-bedrock/test/kontrol/Counter.t.sol

+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import { Counter } from "./Counter.sol";
+
+contract CounterTest {
+    Counter counter;
+
+    function setUp() public {
+        counter = new Counter();
+    }
+
+    function test_SetNumber(uint256 x) public {
+        counter.setNumber(x);
+        require(counter.number() == x, "Not equal");
+    }
+}

packages/contracts-bedrock/test/kontrol/kontrol/pausability-lemmas.k

+requires "evm.md"
+requires "foundry.md"
+
+module PAUSABILITY-LEMMAS
+    imports BOOL
+    imports FOUNDRY
+    imports INFINITE-GAS
+    imports INT-SYMBOLIC
+
+// Your lemmas go here
+
+endmodule

packages/contracts-bedrock/test/kontrol/kontrol/run-kontrol.sh

+#!/bin/bash
+set -euo pipefail
+
+#####################
+# Support Functions #
+#####################
+blank_line() { echo '' >&2 ; }
+notif() { echo "== $0: $*" >&2 ; }
+
+#############
+# Variables #
+#############
+# Set Script Directory Variables <root>/packages/contracts-bedrock/test/kontrol/kontrol
+SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+notif "Script Home: $SCRIPT_HOME"
+blank_line
+
+# Set Run Directory <root>/packages/contracts-bedrock 
+WORKSPACE_DIR=$( cd "${SCRIPT_HOME}/../../.." >/dev/null 2>&1 && pwd )
+notif "Run Directory: ${WORKSPACE_DIR}"
+blank_line
+
+export FOUNDRY_PROFILE=kontrol
+export CONTAINER_NAME=kontrol-tests
+KONTROLRC=$(cat "${WORKSPACE_DIR}/../../.kontrolrc")
+export KONTROL_RELEASE=${KONTROLRC}
+
+
+#############
+# Functions #
+#############
+kontrol_build() {
+    notif "Kontrol Build"
+    docker_exec kontrol build                       \
+                        --verbose                   \
+                        --require ${lemmas}         \
+                        --module-import ${module}   \
+                        ${rekompile}
+            }
+
+kontrol_prove() {
+    notif "Kontrol Prove"
+    docker_exec kontrol prove                              \
+                        --max-depth ${max_depth}           \
+                        --max-iterations ${max_iterations} \
+                        --smt-timeout ${smt_timeout}       \
+                        --bmc-depth ${bmc_depth}           \
+                        --workers ${workers}               \
+                        ${reinit}                          \
+                        ${bug_report}                      \
+                        ${break_on_calls}                  \
+                        ${auto_abstract}                   \
+                        ${tests}                           \
+                        ${use_booster}
+}
+
+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 test content to container
+    docker cp --follow-link "${WORKSPACE_DIR}/." ${CONTAINER_NAME}:/home/user/workspace
+    docker exec --user root ${CONTAINER_NAME} chown -R user:user /home/user
+}
+
+docker_exec () {
+    docker exec --workdir /home/user/workspace ${CONTAINER_NAME} "${@}"
+}
+
+dump_log_results(){
+  trap clean_docker ERR
+
+  notif "Something went wrong. Running cleanup..."
+  blank_line
+
+  notif "Creating Tar of Proof Results"
+  docker exec ${CONTAINER_NAME} tar -czvf results.tar.gz kout/proofs
+  RESULTS_LOG="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
+  notif "Copying Tests Results to Host"
+  docker cp ${CONTAINER_NAME}:/home/user/workspace/results.tar.gz "${RESULTS_LOG}"
+  if [ -f "${RESULTS_LOG}" ]; then
+    cp "${RESULTS_LOG}" kontrol-results_latest.tar.gz 
+  else
+    notif "Results Log: ${RESULTS_LOG} not found, did not pull from container."
+  fi
+  blank_line
+  
+  notif "Dump RUN Logs"
+  RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
+  docker logs ${CONTAINER_NAME} > "${RUN_LOG}"
+}
+
+clean_docker(){
+  notif "Stopping Docker Container"
+  docker stop ${CONTAINER_NAME}
+  blank_line
+}
+
+# Define the function to run on failure
+on_failure() {
+  dump_log_results
+
+  clean_docker
+
+  notif "Cleanup complete."
+  blank_line
+  exit 1
+}
+
+# Set up the trap to run the function on failure
+trap on_failure ERR INT
+
+#########################
+# 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/kontrol/pausability-lemmas.k
+base_module=PAUSABILITY-LEMMAS
+module=CounterTest:${base_module}
+rekompile=--rekompile
+rekompile=
+
+#########################
+# kontrol prove options #
+#########################
+max_depth=10000
+max_iterations=10000
+smt_timeout=100000
+bmc_depth=10
+workers=2
+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=
+use_booster=--use-booster
+# use_booster=
+
+#########################################
+# List of tests to symbolically execute #
+#########################################
+tests=""
+tests+="--match-test CounterTest.test_SetNumber "
+
+#############
+# RUN TESTS #
+#############
+
+# 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
+    blank_line
+fi
+
+start_docker
+
+kontrol_build
+kontrol_prove
+
+dump_log_results
+
+clean_docker
+
+blank_line
+notif "DONE"
+blank_line
\ No newline at end of file