Skip to content

Try different braces in CI yml file for rule lists #43

Try different braces in CI yml file for rule lists

Try different braces in CI yml file for rule lists #43

Workflow file for this run

name: certora
on:
push:
branches:
- master
- certora
pull_request:
branches:
- master
- certora
workflow_dispatch:
jobs:
verify:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- 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
- 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
touch applyHarness.patch
make munged
cd ..
echo "key length" ${#CERTORAKEY}
certoraRun certora/conf/${{ matrix.rule }}
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
strategy:
fail-fast: false
max-parallel: 16
matrix:
rule:
- AToken.conf
- Pool.conf --msg "Martins rules"
- PoolAccurate.conf --msg "Index non decreasing part 1" --rule {"_updateIndexesWrapperReachable", "indexChangesOnlyWith_updateIndexes", "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex"}
- PoolAccurate.conf --msg "Index non decreasing part 2" --rule ["indexesNonDecresingFor_updateIndexes"]
- PoolAccurate.conf --msg "Deposit updates AToken scaled balance" --rule {"depositUpdatesUserATokenSuperBalance", "depositUpdatesUserATokenSuperBalance_sanity"}
- PoolAccurate.conf --msg "Deposit cannot change other users scaled balance" --rule {"depositCannotChangeOthersATokenSuperBalance"}
- ReserveConfiguration.conf
- UserConfigCLI.conf
- StableTokenCLI.conf
- VariableTokenCLI.conf
- PoolSimpleProperties.conf --msg "Deposit functionality" --rule {"cannotDepositInInactiveReserve", "cannotDepositInFrozenReserve", "cannotDepositZeroAmount"}
- PoolSimpleProperties.conf --msg "Withdraw functionality PLUS reachability" --rule {"method_reachability", "cannotWithdrawZeroAmount", "cannotWithdrawFromInactiveReserve"}
- PoolSimpleProperties.conf --msg "Borrow functionality" --rule {"cannotBorrowZeroAmount", "cannotBorrowOnInactiveReserve", "cannotBorrowOnReserveDisabledForBorrowing", "cannotBorrowOnFrozenReserve"}