Saving testable scripts and pnpm package.json additions

.circleci/config.yml

@@ -7,6 +7,9 @@ parameters:
   base_image:
     type: string
     default: ubuntu-2204:2022.07.1
+  kontrol_image:
+    type: string
+    default: runtimeverificationinc/kontrol:ubuntu-jammy-0.1.74
 
 orbs:
   go: circleci/go@1.8.0
@@ -1343,20 +1346,27 @@ jobs:
 
   kontrol-tests:
     docker:
-      - image: runtimeverificationinc/kontrol:ubuntu-jammy-0.1.74
+      - image: << pipeline.parameters.kontrol_image >>
     resource_class: xlarge
     steps:
       - checkout
       - check-changed:
           patterns: contracts-bedrock/test/kontrol,contracts-bedrock/src/L1/OptimismPortal\.sol
+      - attach_workspace: { at: "/home/user" }
+      - run:
+          name: Install pnpm to Kontrol image
+          command: |
+            curl -fsSL https://get.pnpm.io/install.sh | sh -
       - run:
           name: Run Kontrol Tests
           command: |
-            ./packages/contracts-bedrock/scripts/kontrol.sh           
+            pnpm test:kontrol 
+          working_directory: /home/users/packages/contracts-bedrock
       - run:
           name: Create Results Tar
           command: |
-            tar -czvf results.tar.gz packages/contracts-bedrock/kout
+            tar -czvf results.tar.gz test/kontrol/kontrol/kout/proofs
+          working_directory: /home/user/packages/contracts-bedrock
       - store_artifacts:
           path: results.tar.gz
           destination: results

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/scripts/kontrol.sh

 #!/usr/bin/env bash
 set -exuo pipefail
+
+blank_line() { echo '' >&2 ; }
+notif() { echo "== $0: $@" >&2 ; }
+quit()  { notif "[QUITTING]: $@" ; exit 0 ; }
+fatal() { notif "[FATAL]: $@" ; exit 1 ; }
+debug() { if ${do_debug}; then notif "[DEBUG]: $@"; fi ; }
+safe_executor() { if ${do_debug}; then debug $@ ; else "$@" ; fi ; }
+
+# Set Script Directory Variables
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+
+# Set Directory for run-kontrol.sh
+KONTROL_DIR=$CURENT_DIR=$SCRIPT_DIR/../../test/kontrol/kontrol
+CONTRACTS_DIR=$SCRIPT_DIR/..
+
+notif "Run Directory Set to $RUN_DIR"
+
 # Setup Kontrol 
-cd packages/contracts-bedrock && ./test/kontrol/kontrol/run-kontrol.sh

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

@@ -2,18 +2,47 @@
 
 set -euxo pipefail
 
+#####################
+# Support Functions #
+#####################
+blank_line() { echo '' >&2 ; }
+notif() { echo "== $0: $@" >&2 ; }
+
+###########
+# Globals #
+###########
 export FOUNDRY_PROFILE=kontrol
 
-# Create a log file to store standard out and standard error
-LOG_DIRECTORY="test/kontrol/kontrol/logs"
+# 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 
+RUN_DIR="$( cd "$( dirname "$SCRIPT_HOME/../../.." )" >/dev/null 2>&1 && pwd )"
+notif "Run Directory: $RUN_DIR"
+blank_line
+
+# Set Log Directory <root>/packages/contracts-bedrock/test/kontrol/kontrol/logs
+LOG_DIRECTORY=$SCRIPT_HOME/logs
+notif "Log Directory: $LOG_DIRECTORY"
+blank_line
+
 if [ ! -d $LOG_DIRECTORY ] ; then
   mkdir $LOG_DIRECTORY
 fi
+
 LOG_FILE="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
+notif "Logging to $LOG_DIRECTORY/$LOG_FILE"
+blank_line
 exec > >(tee -i $LOG_DIRECTORY/$LOG_FILE)
 exec 2>&1
 
+#############
+# Functions #
+#############
 kontrol_build() {
+    notif "Kontrol Build"
     kontrol build                     \
             --verbose                 \
             --require ${lemmas}       \
@@ -22,6 +51,7 @@ kontrol_build() {
 }
 
 kontrol_prove() {
+    notif "Kontrol Prove"
     kontrol prove                              \
             --max-depth ${max_depth}           \
             --max-iterations ${max_iterations} \
@@ -36,51 +66,54 @@ kontrol_prove() {
             ${use_booster}
 }
 
-###
-# kontrol build options
-###
-
+#########################
+# 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
-
-# NOTE: This script should be executed from the `contracts-bedrock` directory
 lemmas=test/kontrol/kontrol/pausability-lemmas.k
 base_module=PAUSABILITY-LEMMAS
 module=CounterTest:${base_module}
-
 rekompile=--rekompile
 rekompile=
 
-###
-# kontrol prove options
-###
+#########################
+# 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
+#########################################
+# List of tests to symbolically execute #
+#########################################
 tests=""
 tests+="--match-test CounterTest.test_SetNumber "
 
+#############
+# RUN TESTS #
+#############
+pushd $RUN_DIR
+notif "Running Kontrol Build"
+blank_line
 kontrol_build
+
+notif "Running Kontrol Prove"
+blank_line
 kontrol_prove
+
+blank_line
+notif "DONE"
+blank_line
+popd 2>&1 > /dev/null
\ No newline at end of file