Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions .github/workflows/certora_api.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
name: Certora API

on:
workflow_dispatch:
inputs:
command:
required: true
description: |
The Certora API command to execute. Options are:
- `cancel <group_id>`: Cancel all jobs in the specified group.
- `refresh <group_id>`: Refresh the status of all jobs in the specified group.
server:
required: true
type: choice
description: |
The Certora server to use. Either production, staging, or vaas-dev.
Default is production.
default: production
options:
- production
- staging
- vaas-dev

permissions:
contents: read
id-token: write

jobs:
certora_api_command:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: ./api/
with:
certora-command: ${{ github.event.inputs.command }}
server: ${{ github.event.inputs.server }}
47 changes: 47 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -236,10 +236,57 @@ You typically need:
- **A Cargo lockfile.**
If you do not want to commit it in your repository, you can generate it from the action
by running, for example:

```sh
cargo update -p cvlr-soroban
```

## Certora API Integration

You can also use this action to call Certora API commands such as cancelling or
refreshing jobs in a group. To do so, you can create a workflow like this:

```yml
name: Certora API
on:
workflow_dispatch:
inputs:
command:
required: true
description: |
The Certora API command to execute. Options are:
- `cancel <group_id>`: Cancel all jobs in the specified group.
- `refresh <group_id>`: Refresh the status of all jobs in the specified group.
server:
required: true
type: choice
description: |
The Certora server to use. Either production, staging, or vaas-dev.
Default is production.
default: production
options:
- production
- staging
- vaas-dev

permissions:
contents: read
id-token: write

jobs:
certora_api_command:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: Certora/certora-run-action/api@v2
with:
certora-command: ${{ github.event.inputs.command }}
server: ${{ github.event.inputs.server }}
```

Then, you can trigger this workflow manually from the GitHub Actions UI, providing the
command and the server as inputs.

### Comments on the Pull Request

First, it will add a comment with details about runs:
Expand Down
22 changes: 19 additions & 3 deletions action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,10 @@ inputs:
default: "true"
description: |-
Add a comment to the PR only if the run fails.
replace-comments:
default: "true"
description: |-
Whether to replace previous review comments made by this action. Default is `true`.
debug-level:
default: "0"
description: |-
Expand Down Expand Up @@ -145,6 +149,7 @@ inputs:
description: |-
The version of Vyper to install. Can be latest, or a specific version like 0.3.3.
If not specified, Vyper will not be installed.

runs:
using: "composite"
steps:
Expand Down Expand Up @@ -232,14 +237,25 @@ runs:
CERTORA_API_SUBDOMAIN="data-api-stg"
fi

echo "solc_cache_key=$(md5sum <<< '${{ inputs.solc-versions }}' | awk '{ print $1 }')" >> "$GITHUB_OUTPUT"
echo "solc_cache_key=$(md5sum <<< "'${{ inputs.solc-versions }}'" | awk '{ print $1 }')" >> "$GITHUB_OUTPUT"

# Remove leading spaces, trailing spaces, comments, and empty lines
CERTORA_CONFIGURATIONS_FILE="/tmp/certora-logs/REPORT-${GROUP_ID}-configurations"
sed -r 's/^\s+//; s/\s+$//; /^[[:blank:]]*#/d; s/^#.*//; /^\s*$/d' <<< "$CERTORA_RAW_CONFIGURATIONS" | sort -u > "$CERTORA_CONFIGURATIONS_FILE"

CERTORA_CONFIGURATIONS_HASH="$(md5sum < "$CERTORA_CONFIGURATIONS_FILE" | awk '{ print $1 }')"

echo "CERTORA_ACTION_REF=$CERTORA_ACTION_REF" >> "$GITHUB_ENV"
echo "CERTORA_SUBDOMAIN=$CERTORA_SUBDOMAIN" >> "$GITHUB_ENV"
echo "certora_subdomain=$CERTORA_SUBDOMAIN" >> "$GITHUB_OUTPUT"
echo "CERTORA_API_SUBDOMAIN=$CERTORA_API_SUBDOMAIN" >> "$GITHUB_ENV"
echo "CERTORA_CONFIGURATIONS_FILE=$CERTORA_CONFIGURATIONS_FILE" >> "$GITHUB_ENV"
echo "CERTORA_CONFIGURATIONS_HASH=$CERTORA_CONFIGURATIONS_HASH" >> "$GITHUB_ENV"
echo "certora_configurations_file=$CERTORA_CONFIGURATIONS_FILE" >> "$GITHUB_OUTPUT"
echo "certora_configurations_hash=$CERTORA_CONFIGURATIONS_HASH" >> "$GITHUB_OUTPUT"
env:
CERTORA_ACTION_REF: ${{ github.action_ref }}
CERTORA_RAW_CONFIGURATIONS: "${{ inputs.configurations }}"

- name: Install uv
uses: astral-sh/setup-uv@v7
Expand Down Expand Up @@ -337,14 +353,14 @@ runs:
bash "$RUN_CERTORA"
fi
env:
CERTORA_CONFIGURATIONS: "${{ inputs.configurations }}"
CERTORA_SERVER: "${{ inputs.server }}"
CERTORAKEY: "${{ inputs.certora-key }}"
CERTORA_JOB_NAME: "${{ inputs.job-name }}"
CERTORA_COMPILATION_STEPS_ONLY: "${{ inputs.compilation-steps-only }}"
CERTORA_ECOSYSTEM: "${{ inputs.ecosystem }}"
DEBUG_LEVEL: "${{ inputs.debug-level }}"
CERTORA_USE_HARD_LINKS: "${{ inputs.use-hard-links }}"
CERTORA_REPLACE_COMMENTS: "${{ inputs.replace-comments }}"

- name: Add GH Status
if: ${{ steps.certora-run.outputs.total_jobs > 0}}
Expand Down Expand Up @@ -381,5 +397,5 @@ runs:
if: ${{ (failure() || inputs.comment-fail-only == 'false') && (steps.certora-run.outputs.total_jobs > 0 || steps.certora-run.outputs.failed_jobs > 0) }}
uses: mshick/add-pr-comment@v2
with:
message-id: ${{ steps.setup-env.outputs.group_id }}
message-id: ${{ inputs.replace-comments == 'true' && steps.setup-env.outputs.certora_configurations_hash || steps.setup-env.outputs.group_id }}
message-path: ${{ steps.setup-env.outputs.report_file }}
49 changes: 49 additions & 0 deletions api/action.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
# yaml-language-server: $schema=https://raw.githubusercontent.com/SchemaStore/schemastore/refs/heads/master/src/schemas/json/github-action.json
name: Certora API

description: |-
GitHub Action to call Certora API to cancel or refresh a job group.
This action requires that the Certora GitHub App is installed on the repository.

branding:
color: blue
icon: cloud-lightning

inputs:
certora-command:
required: true
description: |-
Command to send to the Certora API. It should be in the format
"<command> <group_id>", where <command> is either "cancel" or "refresh",
and <group_id> is the identifier of a job group to which the command applies.
server:
required: false
description: |-
The Certora server to use. Can be "production" (default). "vaas-dev" or "vaas-stg".
default: "production"
debug-level:
default: "0"
description: |-
The debug level to use for the action command. Default is `0`.
Options: `0`, `1`, `2`, or `3`.

runs:
using: "composite"
steps:
- name: Call Certora API
shell: bash
run: |
RUN_ID="$(cat /proc/sys/kernel/random/uuid)"
CERTORA_LOG_DIR="/tmp/certora-logs/$RUN_ID"
CERTORA_API_SUBDOMAIN="data-api"
if [[ "${{ inputs.server }}" == "vaas-dev" || "${{ inputs.server }}" == "development" ]]; then
CERTORA_API_SUBDOMAIN="data-api-dev"
elif [[ "${{ inputs.server }}" == "staging" || "${{ inputs.server }}" == "vaas-stg" ]]; then
CERTORA_API_SUBDOMAIN="data-api-stg"
fi
export CERTORA_API_SUBDOMAIN
export CERTORA_LOG_DIR
bash "${{ github.action_path }}/../scripts/call-api.sh"
env:
CERTORA_COMMAND: ${{ inputs.certora-command }}
DEBUG_LEVEL: "${{ inputs.debug-level }}"
56 changes: 56 additions & 0 deletions scripts/call-api.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
#!/bin/bash

set -euo pipefail

if [ "${DEBUG_LEVEL:-0}" -gt 0 ]; then
set -x
fi

# Validate required variables
required_vars=(
CERTORA_COMMAND
CERTORA_API_SUBDOMAIN
CERTORA_LOG_DIR
ACTIONS_ID_TOKEN_REQUEST_TOKEN
ACTIONS_ID_TOKEN_REQUEST_URL
)

missing_args=false

for var in "${required_vars[@]}"; do
if [ -z "${!var:-}" ]; then
echo "::error title=Missing variable::$var is required but not set"
missing_args=true
fi
done

if [ "$missing_args" = true ]; then
exit 1
fi

endpoint=""
group_id=""

read -r endpoint group_id <<< "$CERTORA_COMMAND"

# Fetch OIDC token
TOKEN="$(curl -sSfL --retry 3 --max-time 30 -H "Authorization: bearer $ACTIONS_ID_TOKEN_REQUEST_TOKEN" "$ACTIONS_ID_TOKEN_REQUEST_URL" | jq -r .value)"
if [ -z "$TOKEN" ] || [ "$TOKEN" = "null" ]; then
echo "::error title=Token Retrieval Failed::Could not fetch GitHub OIDC token."
exit 1
fi

GHINT_LOG="$CERTORA_LOG_DIR/gh-call.json"

CERT_GH_APP_LINK='https://github.com/apps/certora-run'
CERT_GH_ACTION_LINK='https://github.com/Certora/certora-run-action'
ERROR_MSG="There was an issue executing the API call (Please have a look at $CERT_GH_APP_LINK, $CERT_GH_ACTION_LINK)."

# Make API request to verify GitHub App integration
curl -sSL --proto '=https' --tlsv1.2 --retry 10 --max-time 60 --retry-connrefused --fail-with-body -X POST "https://$CERTORA_API_SUBDOMAIN.certora.com/v1/github-app/$endpoint?groupId=$group_id" \
-H "Authorization: Bearer $TOKEN" \
-H "Content-Type: application/json" >"$GHINT_LOG" || {
echo "::error title=Certora GitHub Application Integration Missing::$(jq -r '"Error \(.status_code): \(.detail)"' "$GHINT_LOG") - $ERROR_MSG"
cat "$GHINT_LOG"
exit 1
}
6 changes: 5 additions & 1 deletion scripts/gh-app-integration.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ required_vars=(
ACTIONS_ID_TOKEN_REQUEST_TOKEN
ACTIONS_ID_TOKEN_REQUEST_URL
GITHUB_EVENT_PATH
CERTORA_CONFIGURATIONS_HASH
CERTORA_REPLACE_COMMENTS
)

missing_args=false
Expand Down Expand Up @@ -52,8 +54,10 @@ PAYLOAD=$(jq -n \
--arg group_id "$GROUP_ID" \
--arg commit "$COMMIT_SHA" \
--arg action_ref "$CERTORA_ACTION_REF" \
--arg config_hash "$CERTORA_CONFIGURATIONS_HASH" \
--argjson replace_comments "$CERTORA_REPLACE_COMMENTS" \
--argjson pr_number "${PR_NUMBER:-null}" \
'{group_id: $group_id, commit: $commit, action_ref: $action_ref, pr_number: $pr_number}')
'{group_id: $group_id, commit: $commit, action_ref: $action_ref, config_hash: $config_hash, replace_comments: $replace_comments, pr_number: $pr_number}')

# Make API request to verify GitHub App integration
curl -sSL --proto '=https' --tlsv1.2 --retry 10 --max-time 60 --retry-connrefused --fail-with-body -X POST "https://$CERTORA_API_SUBDOMAIN.certora.com/v1/github-app/verify" \
Expand Down
17 changes: 9 additions & 8 deletions scripts/run-certora.sh
Original file line number Diff line number Diff line change
Expand Up @@ -13,20 +13,21 @@ pids=()
configs=()
logs=()

# Remove leading spaces, trailing spaces, comments, and empty lines
CERTORA_CONFIGURATIONS="$(sed -r 's/^\s+//; s/\s+$//; /^[[:blank:]]*#/d; s/^#.*//; /^\s*$/d' <<<"$CERTORA_CONFIGURATIONS")"

IFS=$'\n' read -rd '' -a confs <<<"$(echo "$CERTORA_CONFIGURATIONS" | sort -u)"
# Read configurations from file specified by $CERTORA_CONFIGURATIONS_FILE
if [[ -z "$CERTORA_CONFIGURATIONS_FILE" ]]; then
echo "::error title=Missing Configurations File::CERTORA_CONFIGURATIONS_FILE is not set."
exit 1
fi

IFS=$'\n' read -rd '' -a confs < "$CERTORA_CONFIGURATIONS_FILE"

echo "Configurations: ${confs[*]}"

if [[ ${#confs[@]} -gt 1 ]]; then
# Extract the common prefix from the configurations
# Sed script to extract the common prefix
# For the first line, copy pattern space to hold space and delete the pattern space
# Append a newline and the hold space to the pattern space, capture the common prefix
# Copy the pattern space to the hold space and delete the pattern space until the last line
common_prefix="$(echo "$CERTORA_CONFIGURATIONS" | sed -e '1{h;d;}' -e 'G;s,\(.*\).*\n\1.*,\1,;s,\(.*[/ ]\).*$,\1,;h;$!d' | tr -d '\n')"
# Use the contents of the file for prefix extraction
common_prefix="$(sed -e '1{h;d;}' -e 'G;s,\(.*\).*\n\1.*,\1,;s,\(.*[/ ]\).*$,\1,;h;$!d' "$CERTORA_CONFIGURATIONS_FILE" | tr -d '\n')"
elif [[ "${confs[0]}" == */* ]]; then
# Keep the file name only
common_prefix="$(echo "${confs[0]}" | sed 's/\(.*\/\)[^\/]*$/\1/')"
Expand Down
Loading