formal.yaml

name: formal verification
on:
  push:
    tags: # only on releases, not RC, since we've tested already
      - "[0-9]+.[0-9]+.[0-9]+"
    branches: ["**"] # glob pattern to allow slash /
  pull_request:
    types:
      - opened
      - synchronize
    branches:
      - "release**"
      - "main**"
env:
  DOTNET_ROOT: "/home/runner/.dotnet"
  Z3_EXE: "/home/runner/bin/z3"
  CVC5_EXE: "/home/runner/bin/cvc5"
  BOOGIE_EXE: "/home/runner/.dotnet/tools/boogie"
  SOLC_EXE: "/home/runner/bin/solc"

jobs:
  formal:
    runs-on: ubuntu-latest
    steps:
      # NOTE: for debugging CI this allow shell access to github runner. Will print out tmate.io terminal url
      # - name: Setup tmate session
      #   uses: mxschmitt/action-tmate@v3
      #   with:
      #     detached: true
      #   timeout-minutes: 3

      - uses: actions/checkout@v3

      - name: setup env
        uses: ./.github/actions/build_env

      - name: install prover dependencies
        run: |
          bash util/dev_setup.sh -byp

      # Move prover tests
      - name: prover tests
        working-directory: ./framework
        run: make -f prover.mk prove