name: Formal verification

on:
  push:
    branches:
      - master
      - release-v*
      - formal-verification
  pull_request: {}
  workflow_dispatch: {}

jobs:
  list-scripts:
    runs-on: ubuntu-latest
    outputs:
      matrix: ${{ steps.set-matrix.outputs.matrix }}
    steps:
      - uses: actions/checkout@v2
      - id: set-matrix
        run: echo ::set-output name=matrix::$(cat certora/matrix.json)

  verify:
    runs-on: ubuntu-latest
    needs: list-scripts
    steps:
      - uses: actions/checkout@v2
      # - name: Install python
      #   uses: actions/setup-python@v2
      #   with: { python-version: 3.6, cache: 'pip' }
      # - name: Install java
      #   uses: actions/setup-java@v1
      #   with: { java-version: "11", java-package: jre }
      # - name: Install certora
      #   run: pip install certora-cli
      # - name: Install solc
      #   run: |
      #     wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux
      #     sudo mv solc-static-linux /usr/local/bin/solc
      #     chmod +x /usr/local/bin/solc
      - name: Verify rule ${{ matrix.params }}
        if: matrix.params.disabled != true
        run: |
          echo ${{ matrix.params.file }}
          echo ${{ matrix.params.name }}
          echo ${{ matrix.params.spec }}
        # touch certora/applyHarness.patch
        # make -C certora munged
        # echo "key length" ${#CERTORAKEY}
        # sh ${{ matrix.params }}
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}
    strategy:
      fail-fast: false
      max-parallel: 4
      matrix:
        params: ${{ fromJson(needs.list-scripts.outputs.matrix) }}