From 98e54111097a09512123494c39c954a89cb05b49 Mon Sep 17 00:00:00 2001 From: nisnislevi Date: Wed, 22 May 2024 15:21:17 +0300 Subject: [PATCH] clean and add yml --- .github/workflows/certora.yml | 53 ++++++++++++++++++++++ certora/README.md | 49 -------------------- certora/harness/PoolHarness.sol | 80 --------------------------------- certora/scripts/run-all.sh | 79 -------------------------------- 4 files changed, 53 insertions(+), 208 deletions(-) create mode 100644 .github/workflows/certora.yml delete mode 100644 certora/README.md delete mode 100644 certora/harness/PoolHarness.sol delete mode 100644 certora/scripts/run-all.sh diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000000..f3d8fdcefc --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,53 @@ +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: pip install certora-cli-7.6.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/steward/conf/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - ccip.conf diff --git a/certora/README.md b/certora/README.md deleted file mode 100644 index 860d907b4f..0000000000 --- a/certora/README.md +++ /dev/null @@ -1,49 +0,0 @@ -# Running the certora verification tool - -These instructions detail the process for running CVT on the (TODO: example) contracts. - -Documentation for CVT and the specification language are available -[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) - -## Running the verification - -The scripts in the `certora/scripts` directory are used to submit verification -jobs to the Certora verification service. These scripts should be run from the -root directory; for example by running - -```sh -sh certora/scripts/verifyExampleContract.sh -``` - -TODO: update example above, and add any special information for this customer's -setup - -After the job is complete, the results will be available on -[the staging Certora portal](https://vaas-stg.certora.com/) (by default, the -scripts run on our staging cloud). - -## Adapting to changes - -Some of our rules require the code to be simplified in various ways. Our -primary tool for performing these simplifications is to run verification on a -contract that extends the original contracts and overrides some of the methods. -These "harness" contracts can be found in the `certora/harness` directory. - -This pattern does require some modifications to the original code: some methods -need to be made virtual or public, for example. These changes are handled by -applying a patch to the code before verification. - -When one of the `verify` scripts is executed, it first applies the patch file -`certora/applyHarness.patch` to the `contracts` directory, placing the output -in the `certora/munged` directory. We then verify the contracts in the -`certora/munged` directory. - -If the original contracts change, it is possible to create a conflict with the -patch. In this case, the verify scripts will report an error message and output -rejected changes in the `munged` directory. After merging the changes, run -`make record` in the `certora` directory; this will regenerate the patch file, -which can then be checked into git. - -Note: there have been reports of unexpected behavior on mac, see -[issue CUST-62](https://certora.atlassian.net/browse/CUST-62?atlOrigin=eyJpIjoiZWI1MGFjNGZkZGE0NGFlNjkwYjUwYjY2NmE4ZmQ1OTIiLCJwIjoiaiJ9). - diff --git a/certora/harness/PoolHarness.sol b/certora/harness/PoolHarness.sol deleted file mode 100644 index 11e8b2e6a9..0000000000 --- a/certora/harness/PoolHarness.sol +++ /dev/null @@ -1,80 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.10; - -import {Pool} from '../munged/protocol/pool/Pool.sol'; -import {DataTypes} from '../munged/protocol/libraries/types/DataTypes.sol'; -import {ReserveLogic} from '../munged/protocol/libraries/logic/ReserveLogic.sol'; -import {IPoolAddressesProvider} from '../munged/interfaces/IPoolAddressesProvider.sol'; - -import {IERC20} from '../../contracts/dependencies/openzeppelin/contracts/IERC20.sol'; -import {ReserveConfiguration} from '../munged/protocol/libraries/configuration/ReserveConfiguration.sol'; - - - -contract PoolHarness is Pool { - - using ReserveLogic for DataTypes.ReserveData; - using ReserveLogic for DataTypes.ReserveCache; - - constructor(IPoolAddressesProvider provider) public Pool(provider){} - - function getCurrScaledVariableDebt(address asset) public view returns (uint256){ - DataTypes.ReserveData storage reserve = _reserves[asset]; - DataTypes.ReserveCache memory reserveCache = reserve.cache(); - return reserveCache.currScaledVariableDebt; - } - - function getTotalDebt(address asset) public view returns (uint256) { - uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply(); - uint256 totalStable = IERC20(_reserves[asset].stableDebtTokenAddress).totalSupply(); - return totalVariable + totalStable; - } - - function getTotalATokenSupply(address asset) public view returns (uint256) { - return IERC20(_reserves[asset].aTokenAddress).totalSupply(); - } - - function getReserveLiquidityIndex(address asset) public view returns (uint256) { - return _reserves[asset].liquidityIndex; - } - - function getReserveStableBorrowRate(address asset) public view returns (uint256) { - return _reserves[asset].currentStableBorrowRate; - } - - function getReserveVariableBorrowIndex(address asset) public view returns (uint256) { - return _reserves[asset].variableBorrowIndex; - } - - function getReserveVariableBorrowRate(address asset) public view returns (uint256) { - return _reserves[asset].currentVariableBorrowRate; - } - - function updateReserveIndexes(address asset) public returns (bool) { - ReserveLogic._updateIndexes(_reserves[asset], _reserves[asset].cache()); - return true; - } - - function updateReserveIndexesWithCache(address asset, DataTypes.ReserveCache memory cache) public returns (bool) { - ReserveLogic._updateIndexes(_reserves[asset], cache); - return true; - } - - function cumulateToLiquidityIndex(address asset, uint256 totalLiquidity, uint256 amount) public returns (uint256) { - return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount); - } - - function getActive(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) { - return ReserveConfiguration.getActive(self); - } - - function getFrozen(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) { - return ReserveConfiguration.getFrozen(self); - } - - function getBorrowingEnabled(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) { - return ReserveConfiguration.getBorrowingEnabled(self); - } - - -} diff --git a/certora/scripts/run-all.sh b/certora/scripts/run-all.sh deleted file mode 100644 index d6eb7e986b..0000000000 --- a/certora/scripts/run-all.sh +++ /dev/null @@ -1,79 +0,0 @@ -CMN="--typecheck_only" - - - -echo "******** Running: 1 ***************" -certoraRun $CMN certora/conf/AToken.conf \ - --msg "1: AToken.conf" - -echo "******** Running: 2 ***************" -certoraRun $CMN certora/conf/Pool.conf \ - --msg "2: Pool.conf" - -echo "******** Running: 3 ***************" -certoraRun $CMN certora/conf/ReserveConfiguration.conf \ - --msg "3: ReserveConfiguration.conf" - -echo "******** Running: 4 ***************" -certoraRun $CMN certora/conf/StableTokenCLI.conf \ - --msg "4: StableTokenCLI.conf" - -echo "******** Running: 5 ***************" -certoraRun $CMN certora/conf/UserConfigCLI.conf \ - --msg "5: UserConfigCLI.conf" - -echo "******** Running: 6 ***************" -certoraRun $CMN certora/conf/VariableTokenCLI.conf \ - --msg "6: VariableTokenCLI.conf" - -echo "******** Running: 7 NEW no summarization ***************" -certoraRun $CMN certora/conf/NEW-pool-no-summarizations.conf - --msg "7: NEW-pool-no-summarizations" - - -echo "******** Running: simple:1 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotDepositInInactiveReserve \ - --msg "simple:1: NEW :: cannotDepositInInactiveReserve" - -echo "******** Running: simple:2 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotDepositInFrozenReserve \ - --msg "simple:2: NEW :: cannotDepositInFrozenReserve" - -echo "******** Running: simple:3 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotDepositZeroAmount \ - --msg "simple:3: NEW :: cannotDepositZeroAmount" - -echo "******** Running: simple:4 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotWithdrawZeroAmount \ - --msg "simple:4: NEW :: cannotWithdrawZeroAmount" - -echo "******** Running: simple:5 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotWithdrawFromInactiveReserve \ - --msg "simple:5: NEW :: cannotWithdrawFromInactiveReserve" - -echo "******** Running: simple:6 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotBorrowZeroAmount \ - --msg "simple:6: NEW :: cannotBorrowZeroAmount" - -echo "******** Running: simple:7 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotBorrowOnInactiveReserve \ - --msg "simple:7: NEW :: cannotBorrowOnInactiveReserve" - -echo "******** Running: simple:8 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotBorrowOnReserveDisabledForBorrowing \ - --msg "simple:8: NEW :: cannotBorrowOnReserveDisabledForBorrowing" - -echo "******** Running: simple:9 ***************" -certoraRun $CMN certora/conf/NEW-pool-simple-properties.conf \ - --rule cannotBorrowOnFrozenReserve \ - --msg "simple:9: NEW :: cannotBorrowOnFrozenReserve" - -