diff --git a/.github/workflows/certora-basic.yml b/.github/workflows/certora-basic.yml index 4e418d0e..c3641210 100644 --- a/.github/workflows/certora-basic.yml +++ b/.github/workflows/certora-basic.yml @@ -25,21 +25,16 @@ jobs: steps: - uses: actions/checkout@v4 - - name: Check key - env: - CERTORAKEY: ${{ secrets.CERTORAKEY }} - run: echo "key length" ${#CERTORAKEY} - - name: Install python - uses: actions/setup-python@v2 + uses: actions/setup-python@v5 with: { python-version: 3.9 } - name: Install java - uses: actions/setup-java@v1 - with: { java-version: "11", java-package: jre } + 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 + run: pip install certora-cli==7.17.2 - name: Install solc run: | @@ -75,7 +70,7 @@ jobs: - 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" + - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount" + - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve" + - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing" + - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve" diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml index f01da4fd..4a451edd 100644 --- a/.github/workflows/certora-stata.yml +++ b/.github/workflows/certora-stata.yml @@ -18,20 +18,20 @@ jobs: github.ref == format('refs/heads/{0}', github.event.repository.default_branch)) steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 with: submodules: recursive - name: Install python - uses: actions/setup-python@v2 + uses: actions/setup-python@v5 with: { python-version: 3.9 } - name: Install java - uses: actions/setup-java@v1 - with: { java-version: "11", java-package: jre } + 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 + run: pip install certora-cli==7.17.2 - name: Install solc run: | wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux diff --git a/certora/basic/scripts/run-all.sh b/certora/basic/scripts/run-all.sh index 3185e1d3..6d49ffef 100644 --- a/certora/basic/scripts/run-all.sh +++ b/certora/basic/scripts/run-all.sh @@ -1,4 +1,4 @@ -CMN="--compilation_steps_only" +#CMN="--compilation_steps_only" #CMN="--typecheck_only" @@ -72,24 +72,28 @@ echo echo "******** Running: simple:6 ***************" certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ --rule cannotBorrowZeroAmount \ + --rule_sanity none \ --msg "simple:6: NEW :: cannotBorrowZeroAmount" echo echo "******** Running: simple:7 ***************" certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ --rule cannotBorrowOnInactiveReserve \ + --rule_sanity none \ --msg "simple:7: NEW :: cannotBorrowOnInactiveReserve" echo echo "******** Running: simple:8 ***************" certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ --rule cannotBorrowOnReserveDisabledForBorrowing \ + --rule_sanity none \ --msg "simple:8: NEW :: cannotBorrowOnReserveDisabledForBorrowing" echo echo "******** Running: simple:9 ***************" certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ --rule cannotBorrowOnFrozenReserve \ + --rule_sanity none \ --msg "simple:9: NEW :: cannotBorrowOnFrozenReserve" diff --git a/certora/basic/specs/EModeConfiguration.spec b/certora/basic/specs/EModeConfiguration.spec index 5158a2a9..c3823476 100644 --- a/certora/basic/specs/EModeConfiguration.spec +++ b/certora/basic/specs/EModeConfiguration.spec @@ -6,11 +6,37 @@ methods { } +/*===================================================================================== + Rule: setCollateralIntegrity / setBorrowableIntegrity: + We check the integrity of the functions setReserveBitmapBit (which is a setter) and + isReserveEnabledOnBitmap (which is a getter), simply by setting an arbitrary value to arbitrary + location, and then reading it using the getter. + + Note: the functions setCollateral and isCollateralAsset are envelopes to the above setter and getter + and are implemented in the harness. + + Status: PASS + Link: + =====================================================================================*/ rule setCollateralIntegrity(uint256 reserveIndex, bool collateral) { setCollateral(reserveIndex,collateral); assert isCollateralAsset(reserveIndex) == collateral; } +rule setBorrowableIntegrity(uint256 reserveIndex, bool borrowable) { + setBorrowable(reserveIndex,borrowable); + assert isBorrowableAsset(reserveIndex) == borrowable; +} + + + +/*===================================================================================== + Rule: independencyOfCollateralSetters / independencyOfBorrowableSetters: + We check that when calling to setReserveBitmapBit(index,val) only the value at the given + index may be altered. + Status: PASS + Link: + =====================================================================================*/ rule independencyOfCollateralSetters(uint256 reserveIndex, bool collateral) { uint256 reserveIndex_other; @@ -20,13 +46,6 @@ rule independencyOfCollateralSetters(uint256 reserveIndex, bool collateral) { assert (reserveIndex != reserveIndex_other => before == after); } - - -rule setBorrowableIntegrity(uint256 reserveIndex, bool borrowable) { - setBorrowable(reserveIndex,borrowable); - assert isBorrowableAsset(reserveIndex) == borrowable; -} - rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) { uint256 reserveIndex_other; diff --git a/certora/basic/specs/stableRemoved.spec b/certora/basic/specs/stableRemoved.spec index 59e0bbbc..bbd7f3ee 100644 --- a/certora/basic/specs/stableRemoved.spec +++ b/certora/basic/specs/stableRemoved.spec @@ -89,7 +89,7 @@ rule stableFieldsUntouched(method f, env e, address _asset) uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate; address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress; uint128 currentStableBorrowRate_BEFORE = reserveLegasy.currentStableBorrowRate; - address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress; + // address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress; calldataarg args; f(e,args); @@ -105,6 +105,6 @@ rule stableFieldsUntouched(method f, env e, address _asset) assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER; assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER; assert currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER; - assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER; + // assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER; } diff --git a/certora/stata/applyHarness.patch b/certora/stata/applyHarness.patch index 9756bc6b..e0525293 100644 --- a/certora/stata/applyHarness.patch +++ b/certora/stata/applyHarness.patch @@ -9,9 +9,9 @@ diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstanc --- src/contracts/instances/ATokenInstance.sol 2024-09-05 19:01:54 +++ src/contracts/instances/ATokenInstance.sol 2024-09-05 11:33:23 @@ -35,15 +35,15 @@ - + _domainSeparator = _calculateDomainSeparator(); - + - emit Initialized( - underlyingAsset, - address(POOL), @@ -34,12 +34,12 @@ diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstanc + // ); } } -diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol ---- src/contracts/extensions/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54 -+++ src/contracts/extensions/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31 +diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/stata-token/ERC20AaveLMUpgradeable.sol +--- src/contracts/extensions/stata-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54 ++++ src/contracts/extensions/stata-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31 @@ -147,7 +147,7 @@ } - + ///@inheritdoc IERC20AaveLM - function rewardTokens() external view returns (address[] memory) { + function rewardTokens() public view returns (address[] memory) { diff --git a/certora/stata/harness/StataTokenV2Harness.sol b/certora/stata/harness/StataTokenV2Harness.sol index 8b61aec7..1c552930 100644 --- a/certora/stata/harness/StataTokenV2Harness.sol +++ b/certora/stata/harness/StataTokenV2Harness.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.10; import {IERC20} from 'openzeppelin-contracts/contracts/interfaces/IERC20.sol'; -import {StataTokenV2, IPool, IRewardsController} from '../munged/src/contracts/extensions/static-a-token/StataTokenV2.sol'; +import {StataTokenV2, IPool, IRewardsController} from '../munged/src/contracts/extensions/stata-token/StataTokenV2.sol'; import {SymbolicLendingPool} from './pool/SymbolicLendingPool.sol'; contract StataTokenV2Harness is StataTokenV2 { diff --git a/src/contracts/extensions/stata-token/README.md b/src/contracts/extensions/stata-token/README.md index 68463073..83e85b2f 100644 --- a/src/contracts/extensions/stata-token/README.md +++ b/src/contracts/extensions/stata-token/README.md @@ -1,7 +1,7 @@ # stataToken - Static aToken vault/wrapper

- +

## About