Skip to content

test: add tests for ccip rate limit changes (#427) #234

test: add tests for ccip rate limit changes (#427)

test: add tests for ccip rate limit changes (#427) #234

Workflow file for this run

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