certora-gsm.yml

name: certora-gsm

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

  workflow_dispatch:

jobs:
  verify:
    runs-on: ubuntu-latest

    steps:
      - name: Checkout
        uses: actions/checkout@v3
        with:
          submodules: recursive

      - name: Check key
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}
        run: echo "key length" ${#CERTORAKEY}

      - 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==6.1.3

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

      - name: Verify rule ${{ matrix.rule }}
        run: |
          echo "key length" ${#CERTORAKEY}
          certoraRun certora/GSM/conf/${{ matrix.rule }}
        env:
          CERTORAKEY: ${{ secrets.CERTORAKEY }}

    strategy:
      fail-fast: false
      max-parallel: 16
      matrix:
        rule:
          - non-4626/Alex-gho-gsm_inverse.conf
          - non-4626/Alex-gho-gsm.conf
          - non-4626/balances-buy.conf
          - non-4626/balances-sell.conf
          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
          - non-4626/Dominik-gho-fixedPriceStrategy.conf
          - non-4626/fees-buy.conf
          - non-4626/fees-sell.conf
          - non-4626/otakar-FixedFeeStrategy.conf
          - non-4626/Martin-gho-gsm.conf
          - non-4626/antti-optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
          - non-4626/otakar-getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
          - non-4626/otakar-finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
          - non-4626/otakar-OracleSwapFreezer.conf