Skip to content

Certora review

Certora review #37

Workflow file for this run

name: certora
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
on:
pull_request:
branches:
- certora
- main
push:
branches:
- main
workflow_dispatch:
jobs:
verify:
runs-on: ubuntu-latest
if:
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
steps:
- uses: actions/checkout@v4
- 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==7.14.2
- name: Install solc
run: |
wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
chmod +x solc-static-linux
sudo mv solc-static-linux /usr/local/bin/solc8.19
- name: Verify rule ${{ matrix.rule }}
run: |
cd certora/basic
touch applyHarness.patch
make munged
cd ../..
echo "key length" ${#CERTORAKEY}
certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
strategy:
fail-fast: false
max-parallel: 16
matrix:
rule:
- AToken.conf
- ReserveConfiguration.conf
- UserConfiguration.conf
- VariableDebtToken.conf
- NEW-pool-no-summarizations.conf
- stableRemoved.conf
- EModeConfiguration.conf
- NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
- NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
- NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
- NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
- NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
- NEW-pool-simple-properties.conf --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
- NEW-pool-simple-properties.conf --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
- NEW-pool-simple-properties.conf --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
- NEW-pool-simple-properties.conf --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"