Feature/rv compute

.circleci/config.yml

@@ -1443,12 +1443,22 @@ jobs:
           docker_layer_caching: true
       - run:
           name: Run Kontrol Tests
-          command: just test-kontrol
+          command: |
+            curl -X POST \
+              -H "Accept: application/vnd.github+json" \
+              -H "Authorization: Bearer $RV_COMPUTE_TOKEN" \
+              https://api.github.com/repos/runtimeverification/optimism-ci/actions/workflows/optimism-ci.yaml/dispatches \
+              -d '{
+                "ref": "master",
+                "inputs": {
+                  "branch_name": "<<pipeline.git.branch>>",
+                  "extra_args": "script",
+                  "statuses_sha": "<< pipeline.git.revision >>",
+                  "org": "ethereum-optimism",
+                  "repository": "optimism"
+                }
+              }'
           working_directory: ./packages/contracts-bedrock
-      - store_artifacts:
-          path: ./packages/contracts-bedrock/test/kontrol/logs/kontrol-results_latest.tar.gz
-      - store_test_results:
-          path: ./packages/contracts-bedrock
       - notify-failures-on-develop
 
 workflows:
@@ -1990,6 +2000,7 @@ workflows:
       - kontrol-tests:
           context:
             - slack
+            - runtimeverification
 
   scheduled-docker-publish:
     when:

.github/workflows/proof-runner-notification.yml

@@ -0,0 +1,22 @@
+name: Proof Runner Deployment Status
+on:
+  status
+jobs:
+  handle-proof-runner:
+    runs-on: ubuntu-latest
+    if: >-
+      github.event.state == 'error' ||
+      github.event.state == 'failure'
+    steps:
+    - name: Generate Slack Payload
+      run: |
+        echo '{
+          "kontrol_status": "${{ github.event.state }}",
+          "ci_run_link": "${{ github.event.target_url }}"
+        }' > payload.json
+    - name: Send Status Check to Slack
+      uses: slackapi/slack-github-action@v1.26.0
+      with:
+        payload-file-path: "./payload.json"
+      env:
+        SLACK_WEBHOOK_URL: ${{ secrets.SLACK_KONTROL_WEBHOOK_URL }}

packages/contracts-bedrock/test/kontrol/README.md

@@ -190,3 +190,64 @@ Therefore, the snapshots CI check will fail if the committed Kontrol state diff
 Note that the CI check only compares the JSON state diff, not the generated `DeploymentSummary.sol` or `DeploymentSummaryCode` contracts.
 This is for simplicity, as those three files will be in sync upon successful execution of the `make-summary-deployment.sh` script.
 We commit the `DeploymentSummary.sol` and `DeploymentSummaryCode.sol` contracts, because forge fails to build if those contracts are not present—it is simpler to commit these autogenerated files than to workaround their absence in forge builds.
+
+### Kontrol Proof Execution using KaaS (Kontrol as a Service) & CI Integration
+
+To execute compute intensive Symbolic Kontrol proofs in a CI pipeline, we leverage KaaS (Kontrol as a Service) & CircleCI.
+On each execution a status is returned to the commit checks the execution was run from. The checks for a commit provides a "Details" link to the execution KCFG arrtifacts and kontrol proof summary results. See below for further infromation on how to fetch these artifacts from the summary using the Github API.
+
+A high level overview of the CI Setup is defined in CircleCI and configured within [.circleci/config.yml](../../../../.circleci/config.yml). The CirlceCI flow calls on the Github API to execute Kontrol test proofs utilzing the [test scripts](scripts/run-kontrol.sh) in this repo. CircleCI is configured with a Github fine-grained token provided by Runtime Verification to leverage better machines than available in CircleCI to run Kontrol proofs. The token needed is stored in the CircleCI project as a secret.
+
+The proofs can be run manually using the Github Fine-grained token and providing the appropriate parameters outlind in the below Github API call.
+```bash
+  curl -X POST \
+    -H "Accept: application/vnd.github+json" \
+    -H "Authorization: Bearer $RV_COMPUTE_TOKEN" \
+    https://api.github.com/repos/runtimeverification/optimism-ci/actions/workflows/optimism-ci.yaml/dispatches \
+    -d '{
+      "ref": "master",
+      "inputs": {
+        "branch_name": "<<pipeline.git.branch>>",
+        "extra_args": "script",
+        "statuses_sha": "<< pipeline.git.revision >>",
+        "org": "ethereum-optimism",
+        "repository": "optimism"
+      }
+    }'
+```
+NOTE: Making this call manually and providng a sha will overrite an existing statuses sha commit. It will not remove the history from RV's end but will be removed from the commit checks table in a PR or in the commit statuses.
+
+Parameters to be replaced are:
+- **RV_COMPUTE_TOKEN**: The token used to authenticate to the KaaS service.
+- **pipeline.git.branch**: The branch on which to run the proof.
+- **pipeline.git.revision**: The commit hash for the proof execution.
+- **org**: The organization under which to run the proof.
+- **repository**: The repository for the proof execution.
+
+Artifacts are produced after execution is finished and posted to the summary page. Two artifacts are expected:
+- `kontrol_prove_report.xml` -- This is a Kontrol Generated JUnit XML Report containing results and performance data.
+- `Kontrol Results Folder.zip` -- This contains artifacts produced by kontrol during execution that can be used for debugging. This is expected on pass or failure of a proof run.
+
+To Fetch the artifacts of the execution from KaaS, you can either manually navigate to the summary page using the 'Details' link. Or you can use the GitHub API to pull the artifacts.
+Method 1: GitHub's `gh` CLI tool
+- gh run download RUN_ID
+
+Method 2: [Github API](https://docs.github.com/en/rest/actions/artifacts?apiVersion=2022-11-28)
+List the artifacts for a run:
+- GET /repos/{owner}/{repo}/actions/runs/{run_id}/artifacts -- See [documentaiton](httpshttps://docs.github.com/en/rest/actions/artifacts?apiVersion=2022-11-28#list-workflow-run-artifacts) for more details
+```bash
+curl -L \
+  -H "Accept: application/vnd.github+json" \
+  -H "Authorization: Bearer <RV_COMPUTE_TOKEN>" \
+  -H "X-GitHub-Api-Version: 2022-11-28" \
+  https://api.github.com/repos/runtimeverification/optimism-ci/actions/runs/RUN_ID/artifacts
+```
+Then Download the artifacts:
+- GET /repos/{owner}/{repo}/actions/artifacts/{artifact_id} -- See [documentaiton](https://docs.github.com/en/rest/actions/artifacts?apiVersion=2022-11-28#download-an-artifact) for more details
+```bash
+curl -L \
+  -H "Accept: application/vnd.github+json" \
+  -H "Authorization: Bearer <RV_COMPUTE_TOKEN>" \
+  -H "X-GitHub-Api-Version: 2022-11-28" \
+  https://api.github.com/repos/runtimeverification/optimism-ci/actions/artifacts/ARTIFACT_ID/ARCHIVE_FORMAT
+```

packages/contracts-bedrock/test/kontrol/scripts/common.sh

@@ -35,6 +35,7 @@ usage_make_summary() {
 
 # Set Run Directory <root>/packages/contracts-bedrock
 WORKSPACE_DIR=$( cd "$SCRIPT_HOME/../../.." >/dev/null 2>&1 && pwd )
+pushd "$WORKSPACE_DIR" > /dev/null || exit
 
 # Variables
 export KONTROL_FP_DEPLOYMENT="${KONTROL_FP_DEPLOYMENT:-false}"
@@ -111,7 +112,6 @@ parse_first_arg() {
     export LOCAL=true
     export SCRIPT_TESTS=$SCRIPT_OPTION
     export CUSTOM_TESTS=$CUSTOM_OPTION
-    pushd "$WORKSPACE_DIR" > /dev/null || exit
   elif [ "$1" == "script" ]; then
     notif "Running in docker container (DEFAULT)"
     export LOCAL=false
@@ -130,7 +130,6 @@ check_kontrol_version() {
   if [ "$(kontrol version | awk -F': ' '{print$2}')" == "$KONTROLRC" ]; then
     notif "Kontrol version matches $KONTROLRC"
     export LOCAL=true
-    pushd "$WORKSPACE_DIR" > /dev/null || exit
   else
     notif "Kontrol version does NOT match $KONTROLRC"
     notif "Please run 'kup install kontrol --version v$KONTROLRC'"
@@ -182,11 +181,16 @@ copy_to_docker() {
 }
 
 clean_docker(){
-  notif "Stopping Docker Container"
-  docker stop "$CONTAINER_NAME"
+  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 "${@}"
 }
@@ -200,4 +204,5 @@ run () {
     notif "Running in docker"
     docker_exec "${@}"
   fi
+  return $? # Return the exit code of the command
 }

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

@@ -20,6 +20,7 @@ kontrol_build() {
     --require $lemmas \
     --module-import $module \
     $rekompile
+  return $?
 }
 
 kontrol_prove() {
@@ -38,56 +39,63 @@ kontrol_prove() {
     --init-node-from $state_diff \
     --kore-rpc-command 'kore-rpc-booster --equation-max-recursion 100' \
     --xml-test-report
+  return $?
 }
 
-dump_log_results(){
-  trap clean_docker ERR
-    RESULTS_FILE="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
-    LOG_PATH="test/kontrol/logs"
-    RESULTS_LOG="$LOG_PATH/$RESULTS_FILE"
+get_log_results(){
+  RESULTS_FILE="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
+  LOG_PATH="test/kontrol/logs"
+  RESULTS_LOG="$LOG_PATH/$RESULTS_FILE"
 
-    if [ ! -d $LOG_PATH ]; then
-      mkdir $LOG_PATH
-    fi
-
-    notif "Generating Results Log: $LOG_PATH"
+  if [ ! -d $LOG_PATH ]; then
+    mkdir $LOG_PATH
+  fi
 
-    run tar -czvf results.tar.gz kout-proofs/ > /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"
-    fi
-    if [ -f "$RESULTS_LOG" ]; then
-      cp "$RESULTS_LOG" "$LOG_PATH/kontrol-results_latest.tar.gz"
+  notif "Generating Results Log: $RESULTS_LOG"
+
+  run tar -czf results.tar.gz kout-proofs/ > /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"
+    # Check if kontrol_prove_report.xml exists in the container and copy it out if it does
+    if docker exec "$CONTAINER_NAME" test -f /home/user/workspace/kontrol_prove_report.xml; then
+      docker cp "$CONTAINER_NAME:/home/user/workspace/kontrol_prove_report.xml" "$LOG_PATH/kontrol_prove_report.xml"
+      notif "Copied kontrol_prove_report.xml to $LOG_PATH"
     else
-      notif "Results Log: $RESULTS_LOG not found, skipping.."
+      notif "kontrol_prove_report.xml not found in container"
     fi
-    # Report where the file was generated and placed
-    notif "Results Log: $(dirname "$RESULTS_LOG") generated"
+    tar -xzf "$RESULTS_LOG" > /dev/null 2>&1
+  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
+  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"
+    # Expand the tar folder to kout-proofs for Summary Results and caching
+    tar -xzf "$RESULTS_LOG" -C "$WORKSPACE_DIR"  > /dev/null 2>&1
+  fi
 }
 
 # Define the function to run on failure
 on_failure() {
-  dump_log_results
+  get_log_results
 
   if [ "$LOCAL" = false ]; then
     clean_docker
   fi
 
-  notif "Cleanup complete."
+  notif "Failure Cleanup Complete."
   exit 1
 }
 
-# Set up the trap to run the function on failure
-trap on_failure ERR INT
-
 #########################
 # kontrol build options #
 #########################
@@ -107,21 +115,9 @@ regen=
 #################################
 # Tests to symbolically execute #
 #################################
-
 # Temporarily unexecuted tests
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused0" \ -- This one is executed below.
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused1" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused2" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused3" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused4" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused5" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused6" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused7" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused8" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused9" \
-# "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused10" \
 # "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused0" \
-# "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused1" \ -- This one is executed below.
+# "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused1(" \
 # "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused2" \
 # "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused3" \
 # "OptimismPortal2Kontrol.prove_proveWithdrawalTransaction_paused4" \
@@ -134,13 +130,23 @@ regen=
 
 test_list=()
 if [ "$SCRIPT_TESTS" == true ]; then
-  test_list=( "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused0" \
-              "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused1(" \
-              "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
-              "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
-              "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
-              "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
-              "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
+  test_list=(
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused0" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused1(" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused2" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused3" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused4" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused5" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused6" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused7" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused8" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused9" \
+    "OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused10" \
+    "OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused" \
+    "L1StandardBridgeKontrol.prove_finalizeBridgeERC20_paused" \
+    "L1StandardBridgeKontrol.prove_finalizeBridgeETH_paused" \
+    "L1ERC721BridgeKontrol.prove_finalizeBridgeERC721_paused" \
+    "L1CrossDomainMessengerKontrol.prove_relayMessage_paused"
   )
 elif [ "$CUSTOM_TESTS" != 0 ]; then
   test_list=( "${@:${CUSTOM_TESTS}}" )
@@ -156,9 +162,9 @@ done
 max_depth=10000
 max_iterations=10000
 smt_timeout=100000
-max_workers=7 # Set to 7 since the CI machine has 8 CPUs
-# 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
+max_workers=16 # Set to 16 since there are 16 proofs to run
+# 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
@@ -177,16 +183,35 @@ state_diff="./snapshots/state-diff/Kontrol-31337.json"
 #############
 # RUN TESTS #
 #############
+# Set up the trap to run the function on failure
+trap on_failure ERR INT TERM
+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]=$?
 
-dump_log_results
+get_log_results
 
-if [ "$LOCAL" == false ]; then
-    notif "Stopping docker container"
-    clean_docker
+# 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
+else
+  echo "Kontrol Passed"
 fi
 
 notif "DONE"