openzeppelin-contracts/.github/workflows/formal-verification.yml

name: formal verification

on:
  pull_request:
    types:
      - opened
      - reopened
      - synchronize
      - labeled
  workflow_dispatch: {}

env:
  PIP_VERSION: '3.11'
  JAVA_VERSION: '11'
  SOLC_VERSION: '0.8.27'

concurrency: ${{ github.workflow }}-${{ github.ref }}

jobs:
  apply-diff:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - name: Apply patches
        run: make -C certora apply

  verify:
    runs-on: ubuntu-latest
    if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification')
    steps:
      - uses: actions/checkout@v5
        with:
          fetch-depth: 0
      - name: Set up environment
        uses: ./.github/actions/setup
      - name: identify specs that need to be run
        id: arguments
        run: |
          if [[ ${{ github.event_name }} = 'pull_request' ]];
          then
            RESULT=$(git diff ${{ github.event.pull_request.head.sha }}..${{ github.event.pull_request.base.sha }} --name-only certora/specs/*.spec | while IFS= read -r file; do [[ -f $file ]] && basename "${file%.spec}"; done | tr "\n" " ")
          else
            RESULT='--all'
          fi
          echo "result=$RESULT" >> "$GITHUB_OUTPUT"
      - name: Install python
        uses: actions/setup-python@v5
        with:
          python-version: ${{ env.PIP_VERSION }}
          cache: 'pip'
          cache-dependency-path: 'fv-requirements.txt'
      - name: Install python packages
        run: pip install -r fv-requirements.txt
      - name: Install java
        uses: actions/setup-java@v5
        with:
          distribution: temurin
          java-version: ${{ env.JAVA_VERSION }}
      - name: Install solc
        run: |
          wget https://github.com/ethereum/solidity/releases/download/v${{ env.SOLC_VERSION }}/solc-static-linux
          sudo mv solc-static-linux /usr/local/bin/solc
          chmod +x /usr/local/bin/solc
      - name: Verify specification
        run: |
          make -C certora apply
          node certora/run.js ${{ steps.arguments.outputs.result }} -p 1 -v >> "$GITHUB_STEP_SUMMARY"
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}

  halmos:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - name: Set up environment
        uses: ./.github/actions/setup
      - name: Install python
        uses: actions/setup-python@v5
        with:
          python-version: ${{ env.PIP_VERSION }}
          cache: 'pip'
          cache-dependency-path: 'fv-requirements.txt'
      - name: Install python packages
        run: pip install -r fv-requirements.txt
      - name: Run Halmos
        run: halmos --match-test '^symbolic|^testSymbolic' -vv
        env:
          HALMOS_ALLOW_DOWNLOAD: 1