feat: add deploy stkGHO script (#3) #8
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 | |
on: | |
push: | |
branches: | |
- main | |
- certora | |
pull_request: | |
branches: | |
- main | |
- certora | |
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: pip3 install certora-cli | |
- name: Install solc | |
run: | | |
wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux | |
chmod +x solc-static-linux | |
sudo mv solc-static-linux /usr/local/bin/solc8.20 | |
- name: Verify rule ${{ matrix.rule }} | |
run: | | |
cd certora | |
touch applyHarness.patch | |
make munged | |
cd .. | |
echo "key length" ${#CERTORAKEY} | |
certoraRun certora/conf/${{ matrix.rule }} --wait_for_results | |
env: | |
CERTORAKEY: ${{ secrets.CERTORAKEY }} | |
strategy: | |
fail-fast: false | |
max-parallel: 15 | |
matrix: | |
rule: | |
- frontRun.conf --rule front_run__stake | |
- frontRun.conf --rule front_run__stake__on_stakeWithPermit | |
- frontRun.conf --rule front_run__redeem | |
- frontRun.conf --rule front_run__redeem__on_redeemOnBahalf | |
- frontRun.conf --rule front_run__balance | |
- frontRun.conf --rule front_run__cooldown_info | |
- allProps.conf --rule integrityOfStaking noStakingPostSlashingPeriod noSlashingMoreThanMax integrityOfSlashing integrityOfReturnFunds noRedeemOutOfUnstakeWindow totalSupplyDoesNotDropToZero cooldownCorrectness rewardsGetterEquivalentClaim rewardsMonotonicallyIncrease rewardsIncreaseForNonClaimFunctions indexesMonotonicallyIncrease slashingDontDecreaseExchangeRate returnFundsDontIncreaseExchangeRate exchangeRateNeverZero integrityOfRedeem previewStakeEquivalentStake redeem_in_post_slashing_period exchangeRate_cant_changed_unless_slash_returnFunds cooldown_always_updates_cooldown_info when_changing_bal_update_rewards_must_be_called transfer_from_user_to_itself_changes_no_balance slash_increases_exchangeRate returnFunds_decreases_exchangeRate redeem_not_reverting | |
- allProps.conf --rule_sanity none --rule slashing_cant_occur_during_post_slashing_period | |
- propertiesWithSummarization.conf | |
- invariants.conf | |