Skip to content

Modular Gho Stewards #107

Modular Gho Stewards

Modular Gho Stewards #107

Workflow file for this run

name: certora-gho
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==4.13.1
- 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: |
cd certora/gho
touch applyHarness.patch
make munged
cd ../..
echo "key length" ${#CERTORAKEY}
certoraRun certora/gho/conf/${{ matrix.rule }}
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
strategy:
fail-fast: false
max-parallel: 16
matrix:
rule:
- verifyUpgradeableGhoToken.conf
- verifyGhoToken.conf
- verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
- verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
- verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
- verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken
- verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint
- verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt
- verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate
- verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance
- verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent
- verifyGhoVariableDebtToken.conf --rule disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy user_index_up_to_date
- verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh
- verifyGhoVariableDebtTokenInternal.conf
- verifyGhoVariableDebtToken-rayMulDiv-summarization.conf