Certora - Addition of Gsm4626 Specs and Report #258
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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@v4 | |
| with: | |
| submodules: recursive | |
| - name: Install python | |
| uses: actions/setup-python@v5 | |
| with: { python-version: 3.9 } | |
| - name: Install java | |
| uses: actions/setup-java@v4 | |
| with: { distribution: 'zulu', 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: | | |
| certoraRun certora/gsm/conf/gsm/${{ matrix.rule }} | |
| env: | |
| CERTORAKEY: ${{ secrets.CERTORAKEY }} | |
| strategy: | |
| fail-fast: false | |
| max-parallel: 16 | |
| matrix: | |
| rule: | |
| - gho-gsm_inverse.conf | |
| - gho-gsm.conf | |
| - balances-buy.conf | |
| - balances-sell.conf | |
| - gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset | |
| - gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset | |
| - gho-fixedPriceStrategy.conf | |
| - fees-buy.conf | |
| - fees-sell.conf | |
| - FixedFeeStrategy.conf | |
| - gho-gsm.conf | |
| - optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2 | |
| - getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL | |
| - finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees | |
| - OracleSwapFreezer.conf |