formal.yaml

name: formal verification
on:
  push:
    tags:
      - "[0-9]+.[0-9]+.[0-9]+"
      - "[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+"
    branches: ["*"]
  pull_request:
    types:
      - opened
      - synchronize
    branches:
      - "release**"
      - "main**"
env:
  DOTNET_ROOT: "/home/github-runner/.dotnet"
  Z3_EXE: "/home/github-runner/bin/z3"
  CVC5_EXE: "/home/github-runner/bin/cvc5"
  BOOGIE_EXE: "/home/github-runner/.dotnet/tools/boogie"
  SOLC_EXE: "/home/github-runner/bin/solc"

jobs:
  formal:
    runs-on: debian-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: 15

      - uses: actions/checkout@v3

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

      - uses: Swatinem/rust-cache@v2.7.3
        with:
          shared-key: "libra-framework"
          cache-all-crates: true        

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

      - name: install diem (for move tests)
        run: |
          wget -O ${{github.workspace}}/diem https://github.com/0LNetworkCommunity/diem/releases/latest/download/diem &&
          chmod +x ${{github.workspace}}/diem &&
          cp ${{github.workspace}}/diem ~/.cargo/bin

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