certora.yml

name: certora

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main

  workflow_dispatch:

jobs:
  verify:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v2
        with:
          submodules: recursive

      - name: Install python
        uses: actions/setup-python@v2
        with: { python-version: 3.9 }

      - name: Install java
        uses: actions/setup-java@v1
        with: { java-version: "11", java-package: jre }

      - name: Install certora cli
        run: pip install certora-cli

      - name: Install solc
        run: |
          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
          chmod +x solc-static-linux
          sudo mv solc-static-linux /usr/local/bin/solc8.19

      - name: Verify rule ${{ matrix.rule }}
        run: |
          cd certora
          touch applyHarness.patch
          make munged
          cd ..
          echo "key length" ${#CERTORAKEY}
          certoraRun certora/conf/${{ matrix.rule }}
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}

    strategy:
      fail-fast: false
      max-parallel: 16
      matrix:
        rule:
          - propertiesWithSummarization.conf
          - invariants.conf
          - allProps.conf --rule integrityOfSlashing --rule integrityOfStaking --rule previewStakeEquivalentStake --rule noStakingPostSlashingPeriod --rule noSlashingMoreThanMax --rule noRedeemOutOfUnstakeWindow --rule noEntryUntilSlashingSettled --rule integrityOfRedeem --rule cooldownCorrectness --rule airdropNotMutualized --rule integrityOfReturnFunds --rule slashAndReturnFundsOfZeroDoesntChangeExchangeRate
          - allProps.conf --rule rewardsIncreaseForNonClaimFunctions
          - allProps.conf --rule rewardsMonotonicallyIncrease
          - allProps.conf --rule rewardsGetterEquivalentClaim
          - allProps.conf --rule indexesMonotonicallyIncrease
          - allProps.conf --rule exchangeRateNeverZero
          - allProps.conf --rule totalSupplyDoesNotDropToZero
          - allProps.conf --rule slashingIncreaseExchangeRate
          - allProps.conf --rule returnFundsDecreaseExchangeRate
          - token-v3-general.conf --rule delegateCorrectness
          - token-v3-general.conf --rule sumOfVBalancesCorrectness
          - token-v3-general.conf --rule sumOfPBalancesCorrectness
          - token-v3-general.conf --rule transferDoesntChangeDelegationMode
          - token-v3-erc20.conf
          - token-v3-delegate.conf 
          - token-v3-community.conf