diff --git a/.github/workflows/certora-basic.yml b/.github/workflows/certora-basic.yml index c3641210..88873279 100644 --- a/.github/workflows/certora-basic.yml +++ b/.github/workflows/certora-basic.yml @@ -1,4 +1,4 @@ -name: certora +name: certora-basic concurrency: group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} @@ -34,7 +34,7 @@ jobs: with: { distribution: "zulu", java-version: "11", java-package: jre } - name: Install certora cli - run: pip install certora-cli==7.17.2 + run: pip install certora-cli==7.20.3 - name: Install solc run: | diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml index 4a451edd..46719c95 100644 --- a/.github/workflows/certora-stata.yml +++ b/.github/workflows/certora-stata.yml @@ -31,7 +31,7 @@ jobs: with: { distribution: "zulu", java-version: "11", java-package: jre } - name: Install certora cli - run: pip install certora-cli==7.17.2 + run: pip install certora-cli==7.20.3 - name: Install solc run: | wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux diff --git a/certora/basic/conf/NEW-pool-no-summarizations.conf b/certora/basic/conf/NEW-pool-no-summarizations.conf index 3c158029..65043ace 100644 --- a/certora/basic/conf/NEW-pool-no-summarizations.conf +++ b/certora/basic/conf/NEW-pool-no-summarizations.conf @@ -3,13 +3,13 @@ "certora/basic/harness/ATokenHarness.sol", "certora/basic/harness/PoolHarness.sol", "certora/basic/harness/SimpleERC20.sol", - "src/contracts/instances/VariableDebtTokenInstance.sol", - "src/contracts/helpers/AaveProtocolDataProvider.sol", - "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", - "src/contracts/protocol/configuration/ACLManager.sol", - "src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", - "src/contracts/misc/PriceOracleSentinel.sol", - "src/contracts/protocol/configuration/PoolAddressesProvider.sol", + "certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol", + "certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol", + "certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", + "certora/basic/munged/contracts/protocol/configuration/ACLManager.sol", + "certora/basic/munged/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", + "certora/basic/munged/contracts/misc/PriceOracleSentinel.sol", + "certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol", ], "link": [ "ATokenHarness:POOL=PoolHarness", diff --git a/certora/basic/conf/NEW-pool-simple-properties.conf b/certora/basic/conf/NEW-pool-simple-properties.conf index e3492cfa..3ce69459 100644 --- a/certora/basic/conf/NEW-pool-simple-properties.conf +++ b/certora/basic/conf/NEW-pool-simple-properties.conf @@ -3,11 +3,11 @@ "certora/basic/harness/ATokenHarness.sol", "certora/basic/harness/PoolHarness.sol", "certora/basic/harness/SimpleERC20.sol", - "src/contracts/instances/VariableDebtTokenInstance.sol", - "src/contracts/helpers/AaveProtocolDataProvider.sol", - "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", - "src/contracts/protocol/libraries/types/DataTypes.sol", - "src/contracts/protocol/configuration/PoolAddressesProvider.sol", + "certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol", + "certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol", + "certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", + "certora/basic/munged/contracts/protocol/libraries/types/DataTypes.sol", + "certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol", ], "link": [ "ATokenHarness:POOL=PoolHarness", diff --git a/certora/basic/scripts/run-all.sh b/certora/basic/scripts/run-all.sh index 6d49ffef..d0a36377 100644 --- a/certora/basic/scripts/run-all.sh +++ b/certora/basic/scripts/run-all.sh @@ -33,9 +33,9 @@ certoraRun $CMN certora/basic/conf/stableRemoved.conf \ --msg "6: Stable fields are un-touched" echo -echo "******** Running: 6 EModeConfiguration ***************" +echo "******** Running: 7 EModeConfiguration ***************" certoraRun $CMN certora/basic/conf/EModeConfiguration.conf \ - --msg "6: EModeConfiguration" + --msg "7: EModeConfiguration" echo diff --git a/certora/basic/specs/EModeConfiguration.spec b/certora/basic/specs/EModeConfiguration.spec index c3823476..2e5f5960 100644 --- a/certora/basic/specs/EModeConfiguration.spec +++ b/certora/basic/specs/EModeConfiguration.spec @@ -56,5 +56,3 @@ rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) { assert (reserveIndex != reserveIndex_other => before == after); } - - diff --git a/certora/basic/specs/NEW-pool-base.spec b/certora/basic/specs/NEW-pool-base.spec index cc91ac2e..72d9efa5 100644 --- a/certora/basic/specs/NEW-pool-base.spec +++ b/certora/basic/specs/NEW-pool-base.spec @@ -99,7 +99,7 @@ function calculateCompoundedInterestSummary(uint256 rate, uint40 t0, uint256 t1) } function isActiveReserve(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); DataTypes.ReserveConfigurationMap configuration = data.configuration; bool isActive = getActive(e, configuration); @@ -107,7 +107,7 @@ function isActiveReserve(env e, address asset) returns bool { } function isFrozenReserve(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); DataTypes.ReserveConfigurationMap configuration = data.configuration; bool isFrozen = getFrozen(e, configuration); @@ -115,7 +115,7 @@ function isFrozenReserve(env e, address asset) returns bool { } function isEnabledForBorrow(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); DataTypes.ReserveConfigurationMap configuration = data.configuration; bool isBorrowEnabled = getBorrowingEnabled(e, configuration); @@ -123,12 +123,12 @@ function isEnabledForBorrow(env e, address asset) returns bool { } function getCurrentLiquidityRate(env e, address asset) returns mathint { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); return data.currentLiquidityRate; } function getLiquidityIndex(env e, address asset) returns mathint { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); return data.liquidityIndex; } diff --git a/certora/basic/specs/NEW-pool-no-summarizations.spec b/certora/basic/specs/NEW-pool-no-summarizations.spec index 826b0fb7..b5d9e9c6 100644 --- a/certora/basic/specs/NEW-pool-no-summarizations.spec +++ b/certora/basic/specs/NEW-pool-no-summarizations.spec @@ -81,7 +81,7 @@ rule liquidityIndexNonDecresingFor_cumulateToLiquidityIndex() { function get_AToken_of_asset(env e, address asset) returns address { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveDataLegacy data = getReserveData(e, asset); return data.aTokenAddress; } diff --git a/certora/basic/specs/aux/aToken.spec b/certora/basic/specs/aux/aToken.spec index cdbe7310..219b6f59 100644 --- a/certora/basic/specs/aux/aToken.spec +++ b/certora/basic/specs/aux/aToken.spec @@ -131,6 +131,7 @@ function indexForToken(address token, env e) returns uint256 { // todo: adjust for stable debt token function aTokenBalanceOfCVL(address token, address user, env e) returns uint256 { + require token != 0; uint storedBalance = balanceOfCVL(token, user); if (aTokenToUnderlying[token] == 0) { // not a properly initialized aToken, return the regular ERC20 balance diff --git a/certora/basic/specs/stableRemoved.spec b/certora/basic/specs/stableRemoved.spec index bbd7f3ee..64c68be4 100644 --- a/certora/basic/specs/stableRemoved.spec +++ b/certora/basic/specs/stableRemoved.spec @@ -4,7 +4,7 @@ import "aux/aToken.spec"; //import "AddressProvider.spec"; methods { - function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree; + // function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree; function getReserveData(address) external returns (DataTypes.ReserveDataLegacy memory) envfree; function ValidationLogic.validateLiquidationCall( @@ -21,22 +21,43 @@ methods { DataTypes.CalculateUserAccountDataParams memory params ) internal returns (uint256, uint256, uint256, uint256, uint256, bool) => NONDET; - function LiquidationLogic._calculateDebt( + /* function LiquidationLogic._calculateDebt( DataTypes.ReserveCache memory debtReserveCache, DataTypes.ExecuteLiquidationCallParams memory params, uint256 healthFactor - ) internal returns (uint256, uint256) => NONDET; + ) internal returns (uint256, uint256) => NONDET;*/ function LiquidationLogic._calculateAvailableCollateralToLiquidate( - DataTypes.ReserveData storage collateralReserve, - DataTypes.ReserveCache memory debtReserveCache, - address collateralAsset, - address debtAsset, - uint256 debtToCover, - uint256 userCollateralBalance, - uint256 liquidationBonus, - address // IPriceOracleGetter - ) internal returns (uint256,uint256,uint256) => NONDET; + DataTypes.ReserveConfigurationMap memory collateralReserveConfiguration, + uint256 collateralAssetPrice, + uint256 collateralAssetUnit, + uint256 debtAssetPrice, + uint256 debtAssetUnit, + uint256 debtToCover, + uint256 userCollateralBalance, + uint256 liquidationBonus + ) internal returns (uint256, uint256, uint256, uint256) => NONDET; +} + + +// For flashloan +methods { + function _.executeOperation( + address[] assets, + uint256[] amounts, + uint256[] premiums, + address initiator, + bytes params + ) external => NONDET; // expect bool; + + // simple receiver + function _.executeOperation( + address asset, + uint256 amount, + uint256 premium, + address initiator, + bytes params + ) external => NONDET; // expect bool; } @@ -55,9 +76,9 @@ function init_state() { } -hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) { - assert false, "writing the field __deprecatedStableBorrowRate"; -} +//hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) { +// assert false, "writing the field __deprecatedStableBorrowRate"; +//} hook Sstore _reserves[KEY address a].__deprecatedStableDebtTokenAddress address stable (address old_stable) { assert false, "writing the field __deprecatedStableDebtTokenAddress"; @@ -82,29 +103,19 @@ rule stableFieldsUntouched(method f, env e, address _asset) aTokenToUnderlying[currentContract._reserves[asset].aTokenAddress]==asset && aTokenToUnderlying[currentContract._reserves[asset].variableDebtTokenAddress]==asset; + - DataTypes.ReserveData reserve = getReserveDataExtended(_asset); DataTypes.ReserveDataLegacy reserveLegasy = getReserveData(_asset); - uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate; - address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress; uint128 currentStableBorrowRate_BEFORE = reserveLegasy.currentStableBorrowRate; - // address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress; calldataarg args; f(e,args); - DataTypes.ReserveData reserve2 = getReserveDataExtended(_asset); DataTypes.ReserveDataLegacy reserveLegasy2 = getReserveData(_asset); - uint128 __deprecatedStableBorrowRate_AFTER = reserve2.__deprecatedStableBorrowRate; - address __deprecatedStableDebtTokenAddress_AFTER = reserve2.__deprecatedStableDebtTokenAddress; uint128 currentStableBorrowRate_AFTER = reserveLegasy2.currentStableBorrowRate; address stableDebtTokenAddress_AFTER = reserveLegasy2.stableDebtTokenAddress; - assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER; - assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER; assert currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER; - // assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER; - } diff --git a/certora/deprecated/Makefile b/certora/deprecated/Makefile deleted file mode 100644 index 5f56e195..00000000 --- a/certora/deprecated/Makefile +++ /dev/null @@ -1,24 +0,0 @@ -default: help - -PATCH = applyHarness.patch -CONTRACTS_DIR = ../src/ -MUNGED_DIR = munged - -help: - @echo "usage:" - @echo " make clean: remove all generated files (those ignored by git)" - @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" - @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" - -munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) - rm -rf $@ - cp -r $(CONTRACTS_DIR) $@ - patch -p0 -d $@ < $(PATCH) - -record: - diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./src/++g' | sed 's+munged/++g' > $(PATCH) - -clean: - git clean -fdX - touch $(PATCH) - diff --git a/certora/deprecated/README.md b/certora/deprecated/README.md deleted file mode 100644 index 201ac15b..00000000 --- a/certora/deprecated/README.md +++ /dev/null @@ -1,56 +0,0 @@ -# Running the certora verification tool - -These instructions detail the process for running CVT on the contracts. - -Documentation for CVT and the specification language are available -[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) - -## Running the verification - -Initial step: if certora prover is not installed follow the steps [here](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) - -First step is to create the munged/ directory. Enter the certora/ directory and run the following: - -```sh -touch applyHarness.patch -``` - -```sh -make munged -``` - -The second and major step is to run all the verification rules. -The script `certora/scripts/run-all.sh` is used to submit all verification -jobs to the Certora verification service. These scripts should be run from the -root directory: - -```sh -bash certora/scripts/run-all.sh -``` - -_Note: When running the rules locally, please remove the solc version from the `.conf` files as when using solc-select solc version should not be specified in `.conf`_ - -After the jobs are complete, the results will be available on -[the Certora portal](https://prover.certora.com/). - -## 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. diff --git a/certora/deprecated/applyHarness.patch b/certora/deprecated/applyHarness.patch deleted file mode 100644 index 06b4e1ca..00000000 --- a/certora/deprecated/applyHarness.patch +++ /dev/null @@ -1,47 +0,0 @@ -diff -ruN contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol ---- contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2024-03-27 12:57:15.497294747 +0200 -+++ contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2024-03-27 13:08:22.155984803 +0200 -@@ -34,7 +34,7 @@ - } - - /// @inheritdoc IScaledBalanceToken -- function scaledBalanceOf(address user) external view override returns (uint256) { -+ function scaledBalanceOf(address user) public view override returns (uint256) { - return super.balanceOf(user); - } - -diff -ruN contracts/instances/ATokenInstance.sol contracts/instances/ATokenInstance.sol ---- contracts/instances/ATokenInstance.sol 2024-03-27 12:57:15.497294747 +0200 -+++ contracts/instances/ATokenInstance.sol 2024-03-27 13:14:17.971198372 +0200 -@@ -35,15 +35,15 @@ - - _domainSeparator = _calculateDomainSeparator(); - -- emit Initialized( -- underlyingAsset, -- address(POOL), -- treasury, -- address(incentivesController), -- aTokenDecimals, -- aTokenName, -- aTokenSymbol, -- params -- ); -+ // emit Initialized( -+ // underlyingAsset, -+ // address(POOL), -+ // treasury, -+ // address(incentivesController), -+ // aTokenDecimals, -+ // aTokenName, -+ // aTokenSymbol, -+ // params -+ //); - } - } -diff -ruN .gitignore .gitignore ---- .gitignore 1970-01-01 02:00:00.000000000 +0200 -+++ .gitignore 2024-03-27 13:08:22.155984803 +0200 -@@ -0,0 +1,2 @@ -+* -+!.gitignore diff --git a/certora/deprecated/conf/AToken.conf b/certora/deprecated/conf/AToken.conf deleted file mode 100644 index fcf73ac5..00000000 --- a/certora/deprecated/conf/AToken.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "certora/harness/ATokenHarness.sol", - "certora/harness/SimpleERC20.sol" - ], - "link": [ - "ATokenHarness:_underlyingAsset=SimpleERC20" - ], - "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic". - "optimistic_loop": true, - "process": "emv", - "solc": "solc8.19", - "verify": "ATokenHarness:certora/specs/AToken.spec", -// "build_cache": true, - "msg": "aToken spec" -} diff --git a/certora/deprecated/conf/NEW-pool-no-summarizations.conf b/certora/deprecated/conf/NEW-pool-no-summarizations.conf deleted file mode 100644 index bcf611fc..00000000 --- a/certora/deprecated/conf/NEW-pool-no-summarizations.conf +++ /dev/null @@ -1,40 +0,0 @@ -{ - "files": [ - "certora/harness/ATokenHarness.sol", - "certora/harness/PoolHarness.sol", - "certora/harness/SimpleERC20.sol", - "src/contracts/instances/VariableDebtTokenInstance.sol", - "src/contracts/helpers/AaveProtocolDataProvider.sol", - "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", - "src/contracts/protocol/configuration/ACLManager.sol", - "src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", - "src/contracts/misc/PriceOracleSentinel.sol", - "src/contracts/protocol/configuration/PoolAddressesProvider.sol", - ], - "link": [ - "ATokenHarness:POOL=PoolHarness", - "ATokenHarness:_underlyingAsset=SimpleERC20", - "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", - "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider", - ], - "struct_link": [ - "PoolHarness:aTokenAddress=ATokenHarness", - "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance", - "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2", - ], - "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. - "optimistic_loop": true, - "process": "emv", - "global_timeout": "7198", - "prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it. - "solc": "solc8.19", - "verify": "PoolHarness:certora/specs/NEW-pool-no-summarizations.spec", - "rule": [ - "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex", - "depositUpdatesUserATokenSuperBalance", - "depositCannotChangeOthersATokenSuperBalance" - ], -// "build_cache": true, - "parametric_contracts": ["PoolHarness"], - "msg": "pool-no-summarizations::partial rules", -} diff --git a/certora/deprecated/conf/NEW-pool-simple-properties.conf b/certora/deprecated/conf/NEW-pool-simple-properties.conf deleted file mode 100644 index da979e32..00000000 --- a/certora/deprecated/conf/NEW-pool-simple-properties.conf +++ /dev/null @@ -1,42 +0,0 @@ -{ - "files": [ - "certora/harness/ATokenHarness.sol", - "certora/harness/PoolHarness.sol", - "certora/harness/SimpleERC20.sol", - "src/contracts/instances/VariableDebtTokenInstance.sol", - "src/contracts/helpers/AaveProtocolDataProvider.sol", - "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", - "src/contracts/protocol/libraries/types/DataTypes.sol", - "src/contracts/protocol/configuration/PoolAddressesProvider.sol", - ], - "link": [ - "ATokenHarness:POOL=PoolHarness", - "ATokenHarness:_underlyingAsset=SimpleERC20", - "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", - ], - "struct_link": [ - "PoolHarness:aTokenAddress=ATokenHarness", - "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance", - "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2", - ], - "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. - "optimistic_loop": true, - "process": "emv", - "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it. - "solc": "solc8.19", - "verify": "PoolHarness:certora/specs/NEW-pool-simple-properties.spec", - "rule": [ - "cannotDepositInInactiveReserve", - "cannotDepositInFrozenReserve", - "cannotDepositZeroAmount", - "cannotWithdrawZeroAmount", - "cannotWithdrawFromInactiveReserve", - "cannotBorrowZeroAmount", - "cannotBorrowOnInactiveReserve", - "cannotBorrowOnReserveDisabledForBorrowing", - "cannotBorrowOnFrozenReserve" - ], -// "build_cache": true, - "parametric_contracts": ["PoolHarness"], - "msg": "pool-simple-properties::ALL", -} diff --git a/certora/deprecated/conf/ReserveConfiguration.conf b/certora/deprecated/conf/ReserveConfiguration.conf deleted file mode 100644 index ed3fc42f..00000000 --- a/certora/deprecated/conf/ReserveConfiguration.conf +++ /dev/null @@ -1,15 +0,0 @@ -{ - "files": [ - "certora/harness/ReserveConfigurationHarness.sol" - ], - "msg": "ReserveConfiguration", - "optimistic_loop": true, - "process": "emv", - "prover_args": [ - "-useBitVectorTheory" - ], - "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic" - "solc": "solc8.19", -// "build_cache": true, - "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec" -} diff --git a/certora/deprecated/conf/UserConfiguration.conf b/certora/deprecated/conf/UserConfiguration.conf deleted file mode 100644 index 2d85039b..00000000 --- a/certora/deprecated/conf/UserConfiguration.conf +++ /dev/null @@ -1,16 +0,0 @@ -{ - "files": [ - "certora/harness/UserConfigurationHarness.sol" - ], - // No rule sanity because a there are invariant s.t. the invariant can be proven - // without assuming it first. (for some of the functions.) - "msg": "UserConfiguration All spec", - "optimistic_loop": true, - "process": "emv", - "prover_args": [ - "-useBitVectorTheory" - ], - "solc": "solc8.19", -// "build_cache": true, - "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec" -} diff --git a/certora/deprecated/conf/VariableDebtToken.conf b/certora/deprecated/conf/VariableDebtToken.conf deleted file mode 100644 index 90050b61..00000000 --- a/certora/deprecated/conf/VariableDebtToken.conf +++ /dev/null @@ -1,12 +0,0 @@ -{ - "files": [ - "certora/harness/VariableDebtTokenHarness.sol" - ], - "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. - "msg": "variable debt token", - "optimistic_loop": true, - "process": "emv", - "solc": "solc8.19", -// "build_cache": true, - "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec" -} diff --git a/certora/deprecated/harness/ATokenHarness.sol b/certora/deprecated/harness/ATokenHarness.sol deleted file mode 100644 index bcb5d32a..00000000 --- a/certora/deprecated/harness/ATokenHarness.sol +++ /dev/null @@ -1,45 +0,0 @@ -// SPDX-License-Identifier: agpl-3.0 -pragma solidity ^0.8.19; - -import {Pool} from '../munged/contracts/protocol/pool/Pool.sol'; -import {ATokenInstance} from '../munged/contracts/instances/ATokenInstance.sol'; -import {WadRayMath} from '../munged/contracts/protocol/libraries/math/WadRayMath.sol'; -import {ScaledBalanceTokenBase} from '../munged/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol'; -import {IScaledBalanceToken} from '../munged/contracts/interfaces/IScaledBalanceToken.sol'; - -/* - * @title Certora harness for Aave ERC20 AToken - * - * @dev Certora's harness contract for the verification of Aave ERC20 AToken. - */ -contract ATokenHarness is ATokenInstance { - using WadRayMath for uint256; - - constructor(Pool pool) public ATokenInstance(pool) {} - - function scaledTotalSupply() - public - view - override(IScaledBalanceToken, ScaledBalanceTokenBase) - returns (uint256) - { - uint256 val = super.scaledTotalSupply(); - return val; - } - - function additionalData(address user) public view returns (uint128) { - return _userState[user].additionalData; - } - - function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { - return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset)); - } - - function ATokenBalanceOf(address user) public view returns (uint256) { - return super.balanceOf(user); - } - - function superBalance(address user) public view returns (uint256) { - return scaledBalanceOf(user); - } -} diff --git a/certora/deprecated/harness/PoolHarness.sol b/certora/deprecated/harness/PoolHarness.sol deleted file mode 100644 index 96ad8637..00000000 --- a/certora/deprecated/harness/PoolHarness.sol +++ /dev/null @@ -1,79 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; - -import {PoolInstance} from '../munged/contracts/instances/PoolInstance.sol'; -import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; -import {ReserveLogic} from '../munged/contracts/protocol/libraries/logic/ReserveLogic.sol'; -import {IPoolAddressesProvider} from '../munged/contracts/interfaces/IPoolAddressesProvider.sol'; - -import {IERC20} from '../../src/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; -import {ReserveConfiguration} from '../munged/contracts/protocol/libraries/configuration/ReserveConfiguration.sol'; - -contract PoolHarness is PoolInstance { - using ReserveLogic for DataTypes.ReserveData; - using ReserveLogic for DataTypes.ReserveCache; - - constructor(IPoolAddressesProvider provider) public PoolInstance(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(); - return totalVariable; - } - - 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 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/deprecated/harness/ReserveConfigurationHarness.sol b/certora/deprecated/harness/ReserveConfigurationHarness.sol deleted file mode 100644 index b74bd81a..00000000 --- a/certora/deprecated/harness/ReserveConfigurationHarness.sol +++ /dev/null @@ -1,322 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; -pragma experimental ABIEncoderV2; - -import {ReserveConfiguration} from '../munged/contracts/protocol/libraries/configuration/ReserveConfiguration.sol'; -import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; - -contract ReserveConfigurationHarness { - DataTypes.ReserveConfigurationMap public reservesConfig; - mapping(uint256 => uint256) public intSettersUpperBounds; - mapping(uint256 => uint256) public intSetterslowerBounds; - mapping(uint256 => uint256) public boolSettersCompare; - - // Sets the Loan to Value of the reserve - function setLtv(uint256 ltv) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setLtv(configNew, ltv); - reservesConfig.data = configNew.data; - } - - // Gets the Loan to Value of the reserve - function getLtv() public view returns (uint256) { - return ReserveConfiguration.getLtv(reservesConfig); - } - - // Sets the liquidation threshold of the reserve - function setLiquidationThreshold(uint256 threshold) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setLiquidationThreshold(configNew, threshold); - reservesConfig.data = configNew.data; - } - - // Gets the liquidation threshold of the reserve - function getLiquidationThreshold() public view returns (uint256) { - return ReserveConfiguration.getLiquidationThreshold(reservesConfig); - } - - // Sets the liquidation bonus of the reserve - function setLiquidationBonus(uint256 bonus) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setLiquidationBonus(configNew, bonus); - reservesConfig.data = configNew.data; - } - - // Gets the liquidation bonus of the reserve - function getLiquidationBonus() public view returns (uint256) { - return ReserveConfiguration.getLiquidationBonus(reservesConfig); - } - - // Sets the decimals of the underlying asset of the reserve - function setDecimals(uint256 decimals) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setDecimals(configNew, decimals); - reservesConfig.data = configNew.data; - } - - // Gets the decimals of the underlying asset of the reserve - function getDecimals() public view returns (uint256) { - return ReserveConfiguration.getDecimals(reservesConfig); - } - - // Sets the active state of the reserve - function setActive(bool active) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setActive(configNew, active); - reservesConfig.data = configNew.data; - } - - // Gets the active state of the reserve - function getActive() public view returns (bool) { - return ReserveConfiguration.getActive(reservesConfig); - } - - // Sets the frozen state of the reserve - function setFrozen(bool frozen) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setFrozen(configNew, frozen); - reservesConfig.data = configNew.data; - } - - // Gets the frozen state of the reserve - function getFrozen() public view returns (bool) { - return ReserveConfiguration.getFrozen(reservesConfig); - } - - // Sets the paused state of the reserve - function setPaused(bool paused) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setPaused(configNew, paused); - reservesConfig.data = configNew.data; - } - - // Gets the paused state of the reserve - function getPaused() public view returns (bool) { - return ReserveConfiguration.getPaused(reservesConfig); - } - - // Sets the borrowable in isolation flag for the reserve. - function setBorrowableInIsolation(bool borrowable) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setBorrowableInIsolation(configNew, borrowable); - reservesConfig.data = configNew.data; - } - - // Gets the borrowable in isolation flag for the reserve. - function getBorrowableInIsolation() public view returns (bool) { - return ReserveConfiguration.getBorrowableInIsolation(reservesConfig); - } - - // Sets the siloed borrowing flag for the reserve. - function setSiloedBorrowing(bool siloed) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setSiloedBorrowing(configNew, siloed); - reservesConfig.data = configNew.data; - } - - // Gets the siloed borrowing flag for the reserve. - function getSiloedBorrowing() public view returns (bool) { - return ReserveConfiguration.getSiloedBorrowing(reservesConfig); - } - - // Enables or disables borrowing on the reserve - function setBorrowingEnabled(bool enabled) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setBorrowingEnabled(configNew, enabled); - reservesConfig.data = configNew.data; - } - - // Gets the borrowing state of the reserve - function getBorrowingEnabled() public view returns (bool) { - return ReserveConfiguration.getBorrowingEnabled(reservesConfig); - } - - // Sets the reserve factor of the reserve - function setReserveFactor(uint256 reserveFactor) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setReserveFactor(configNew, reserveFactor); - reservesConfig.data = configNew.data; - } - - // Gets the reserve factor of the reserve - function getReserveFactor() public view returns (uint256) { - return ReserveConfiguration.getReserveFactor(reservesConfig); - } - - // Sets the borrow cap of the reserve - function setBorrowCap(uint256 borrowCap) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setBorrowCap(configNew, borrowCap); - reservesConfig.data = configNew.data; - } - - // Gets the borrow cap of the reserve - function getBorrowCap() public view returns (uint256) { - return ReserveConfiguration.getBorrowCap(reservesConfig); - } - - // Sets the supply cap of the reserve - function setSupplyCap(uint256 supplyCap) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setSupplyCap(configNew, supplyCap); - reservesConfig.data = configNew.data; - } - - // Gets the supply cap of the reserve - function getSupplyCap() public view returns (uint256) { - return ReserveConfiguration.getSupplyCap(reservesConfig); - } - - // Sets the debt ceiling in isolation mode for the asset - function setDebtCeiling(uint256 ceiling) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setDebtCeiling(configNew, ceiling); - reservesConfig.data = configNew.data; - } - - // Gets the debt ceiling for the asset if the asset is in isolation mode - function getDebtCeiling() public view returns (uint256) { - return ReserveConfiguration.getDebtCeiling(reservesConfig); - } - - // Sets the liquidation protocol fee of the reserve - function setLiquidationProtocolFee(uint256 liquidationProtocolFee) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setLiquidationProtocolFee(configNew, liquidationProtocolFee); - reservesConfig.data = configNew.data; - } - - // Gets the liquidation protocol fee - function getLiquidationProtocolFee() public view returns (uint256) { - return ReserveConfiguration.getLiquidationProtocolFee(reservesConfig); - } - - // Sets the unbacked mint cap of the reserve - function setUnbackedMintCap(uint256 unbackedMintCap) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setUnbackedMintCap(configNew, unbackedMintCap); - reservesConfig.data = configNew.data; - } - - // Gets the unbacked mint cap of the reserve - function getUnbackedMintCap() public view returns (uint256) { - return ReserveConfiguration.getUnbackedMintCap(reservesConfig); - } - - // Sets the eMode asset category - function setEModeCategory(uint256 category) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setEModeCategory(configNew, category); - reservesConfig.data = configNew.data; - } - - // Gets the eMode asset category - function getEModeCategory() public view returns (uint256) { - return ReserveConfiguration.getEModeCategory(reservesConfig); - } - - // Sets the flashloanble flag for the reserve - function setFlashLoanEnabled(bool flashLoanEnabled) public { - DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; - ReserveConfiguration.setFlashLoanEnabled(configNew, flashLoanEnabled); - reservesConfig.data = configNew.data; - } - - // Gets the flashloanable flag for the reserve - function getFlashLoanEnabled() public view returns (bool) { - return ReserveConfiguration.getFlashLoanEnabled(reservesConfig); - } - - // returns the entire data in form of unit256 - function getData() public view returns (uint256) { - return reservesConfig.data; - } - - // Executes a setter of an int parameter according to the given id - function executeIntSetterById(uint256 id, uint256 val) public { - require(id >= 0 && id <= 10); - if (id == 0) { - setLtv(val); - } else if (id == 1) { - setLiquidationThreshold(val); - } else if (id == 2) { - setLiquidationBonus(val); - } else if (id == 3) { - setDecimals(val); - } else if (id == 4) { - setReserveFactor(val); - } else if (id == 5) { - setBorrowCap(val); - } else if (id == 6) { - setSupplyCap(val); - } else if (id == 7) { - setLiquidationProtocolFee(val); - } else if (id == 8) { - setEModeCategory(val); - } else if (id == 9) { - setUnbackedMintCap(val); - } else { - setDebtCeiling(val); - } - } - - // Executes a getter of an int parameter according to the given id - function executeIntGetterById(uint256 id) public view returns (uint256) { - require(id >= 0 && id <= 10); - if (id == 0) { - return getLtv(); - } else if (id == 1) { - return getLiquidationThreshold(); - } else if (id == 2) { - return getLiquidationBonus(); - } else if (id == 3) { - return getDecimals(); - } else if (id == 4) { - return getReserveFactor(); - } else if (id == 5) { - return getBorrowCap(); - } else if (id == 6) { - return getSupplyCap(); - } else if (id == 7) { - return getLiquidationProtocolFee(); - } else if (id == 8) { - return getEModeCategory(); - } else if (id == 9) { - return getUnbackedMintCap(); - } else { - return getDebtCeiling(); - } - } - - // Executes a setter of a bool parameter according to the given id - function executeBoolSetterById(uint256 id, bool val) public { - require(id >= 0 && id <= 4); - if (id == 0) { - setActive(val); - } else if (id == 1) { - setFrozen(val); - } else if (id == 2) { - setBorrowingEnabled(val); - } else if (id == 3) { - setPaused(val); - } else { - setBorrowableInIsolation(val); - } - } - - // Executes a getter of a bool parameter according to the given id - function executeBoolGetterById(uint256 id) public view returns (bool) { - require(id >= 0 && id <= 4); - if (id == 0) { - return getActive(); - } else if (id == 1) { - return getFrozen(); - } else if (id == 2) { - return getBorrowingEnabled(); - } else if (id == 3) { - return getPaused(); - } else { - return getBorrowableInIsolation(); - } - } -} diff --git a/certora/deprecated/harness/SimpleERC20.sol b/certora/deprecated/harness/SimpleERC20.sol deleted file mode 100644 index 68733603..00000000 --- a/certora/deprecated/harness/SimpleERC20.sol +++ /dev/null @@ -1,58 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; - -import {IERC20} from '../munged/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; - -/** -A simple ERC implementation used as the underlying_asset for the verification process. - */ -contract SimpleERC20 is IERC20 { - uint256 t; - mapping(address => uint256) b; - mapping(address => mapping(address => uint256)) a; - - function add(uint a, uint b) internal pure returns (uint256) { - uint c = a + b; - require(c >= a); - return c; - } - - function sub(uint a, uint b) internal pure returns (uint256) { - require(a >= b); - return a - b; - } - - function totalSupply() external view override returns (uint256) { - return t; - } - - function balanceOf(address account) external view override returns (uint256) { - return b[account]; - } - - function transfer(address recipient, uint256 amount) external override returns (bool) { - b[msg.sender] = sub(b[msg.sender], amount); - b[recipient] = add(b[recipient], amount); - return true; - } - - function allowance(address owner, address spender) external view override returns (uint256) { - return a[owner][spender]; - } - - function approve(address spender, uint256 amount) external override returns (bool) { - a[msg.sender][spender] = amount; - return true; - } - - function transferFrom( - address sender, - address recipient, - uint256 amount - ) external override returns (bool) { - b[sender] = sub(b[sender], amount); - b[recipient] = add(b[recipient], amount); - a[sender][msg.sender] = sub(a[sender][msg.sender], amount); - return true; - } -} diff --git a/certora/deprecated/harness/SymbolicPriceOracle.sol b/certora/deprecated/harness/SymbolicPriceOracle.sol deleted file mode 100644 index d268e5d0..00000000 --- a/certora/deprecated/harness/SymbolicPriceOracle.sol +++ /dev/null @@ -1,22 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; - -import {IPriceOracleGetter} from '../munged/contracts/interfaces/IPriceOracleGetter.sol'; - -contract SymbolicPriceOracle is IPriceOracleGetter { - address public base; - uint256 public unit; - mapping(address => uint256) public price; - - function BASE_CURRENCY() external view returns (address) { - return base; - } - - function BASE_CURRENCY_UNIT() external view override returns (uint256) { - return unit; - } - - function getAssetPrice(address asset) external view override returns (uint256) { - return price[asset]; - } -} diff --git a/certora/deprecated/harness/UserConfigurationHarness.sol b/certora/deprecated/harness/UserConfigurationHarness.sol deleted file mode 100644 index 3f1637ea..00000000 --- a/certora/deprecated/harness/UserConfigurationHarness.sol +++ /dev/null @@ -1,74 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; -pragma experimental ABIEncoderV2; - -import {UserConfiguration} from '../munged/contracts/protocol/libraries/configuration/UserConfiguration.sol'; -import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; -import {PoolStorage} from '../munged/contracts/protocol/pool/PoolStorage.sol'; - -/* -A wrapper contract for calling functions from the library UserConfiguration. -*/ -contract UserConfigurationHarness is PoolStorage { - DataTypes.UserConfigurationMap public usersConfig; - - // Sets if the user is borrowing the reserve identified by reserveIndex - function setBorrowing(uint256 reserveIndex, bool borrowing) public { - UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing); - } - - //Sets if the user is using as collateral the reserve identified by reserveIndex - function setUsingAsCollateral(uint256 reserveIndex, bool _usingAsCollateral) public { - UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral); - } - - // Returns if a user has been using the reserve for borrowing or as collateral - function isUsingAsCollateralOrBorrowing(uint256 reserveIndex) public view returns (bool) { - return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex); - } - - // Validate a user has been using the reserve for borrowing - function isBorrowing(uint256 reserveIndex) public view returns (bool) { - return UserConfiguration.isBorrowing(usersConfig, reserveIndex); - } - - // Validate a user has been using the reserve as collateral - function isUsingAsCollateral(uint256 reserveIndex) public view returns (bool) { - return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex); - } - - // Checks if a user has been supplying only one reserve as collateral - function isUsingAsCollateralOne() public view returns (bool) { - return UserConfiguration.isUsingAsCollateralOne(usersConfig); - } - - // Checks if a user has been supplying any reserve as collateral - function isUsingAsCollateralAny() public view returns (bool) { - return UserConfiguration.isUsingAsCollateralAny(usersConfig); - } - - // Checks if a user has been borrowing only one asset - function isBorrowingOne() public view returns (bool) { - return UserConfiguration.isBorrowingOne(usersConfig); - } - - // Checks if a user has been borrowing from any reserve - function isBorrowingAny() public view returns (bool) { - return UserConfiguration.isBorrowingAny(usersConfig); - } - - // Checks if a user has not been using any reserve for borrowing or supply - function isEmpty() public view returns (bool) { - return UserConfiguration.isEmpty(usersConfig); - } - - // Returns the Isolation Mode state of the user - function getIsolationModeState() public view returns (bool, address, uint256) { - return UserConfiguration.getIsolationModeState(usersConfig, _reserves, _reservesList); - } - - // Returns the siloed borrowing state for the user - function getSiloedBorrowingState() public view returns (bool, address) { - return UserConfiguration.getSiloedBorrowingState(usersConfig, _reserves, _reservesList); - } -} diff --git a/certora/deprecated/harness/VariableDebtTokenHarness.sol b/certora/deprecated/harness/VariableDebtTokenHarness.sol deleted file mode 100644 index ca2696a6..00000000 --- a/certora/deprecated/harness/VariableDebtTokenHarness.sol +++ /dev/null @@ -1,16 +0,0 @@ -// SPDX-License-Identifier: BUSL-1.1 -pragma solidity ^0.8.19; - -import {VariableDebtTokenInstance} from '../munged/contracts/instances/VariableDebtTokenInstance.sol'; -import {WadRayMath} from '../munged/contracts/protocol/libraries/math/WadRayMath.sol'; -import {IPool} from '../munged/contracts/interfaces/IPool.sol'; - -contract VariableDebtTokenHarness is VariableDebtTokenInstance { - using WadRayMath for uint256; - - constructor(IPool pool) public VariableDebtTokenInstance(pool) {} - - function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { - return bal.rayMul(POOL.getReserveNormalizedVariableDebt(_underlyingAsset)); - } -} diff --git a/certora/deprecated/munged/.gitignore b/certora/deprecated/munged/.gitignore deleted file mode 100644 index d6b7ef32..00000000 --- a/certora/deprecated/munged/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore diff --git a/certora/deprecated/scripts/run-all.sh b/certora/deprecated/scripts/run-all.sh deleted file mode 100644 index ab9685d4..00000000 --- a/certora/deprecated/scripts/run-all.sh +++ /dev/null @@ -1,71 +0,0 @@ -#CMN="--compilation_steps_only" - - - -echo "******** Running: 1 ***************" -certoraRun $CMN certora/conf/AToken.conf \ - --msg "1: AToken.conf" - -echo "******** Running: 2 ***************" -certoraRun $CMN certora/conf/ReserveConfiguration.conf \ - --msg "2: ReserveConfiguration.conf" - -echo "******** Running: 3 ***************" -certoraRun $CMN certora/conf/UserConfiguration.conf \ - --msg "3: UserConfiguration.conf" - -echo "******** Running: 4 ***************" -certoraRun $CMN certora/conf/VariableDebtToken.conf \ - --msg "4: VariableDebtToken.conf" - -echo "******** Running: 5 NEW no summarization ***************" -certoraRun $CMN certora/conf/NEW-pool-no-summarizations.conf \ - --msg "5: 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" - - diff --git a/certora/deprecated/specs/AToken.spec b/certora/deprecated/specs/AToken.spec deleted file mode 100644 index bd15c698..00000000 --- a/certora/deprecated/specs/AToken.spec +++ /dev/null @@ -1,309 +0,0 @@ -/** - - values of gRNI passing: ray, 2 * ray -*/ -using SimpleERC20 as _underlyingAsset; - -methods { - function nonces(address) external returns (uint256) envfree; - function allowance(address, address) external returns (uint256) envfree; - function _.handleAction(address, uint256, uint256) external => NONDET; - function _.getReserveNormalizedIncome(address u) external => gRNI() expect uint256 ALL; - function balanceOf(address) external returns (uint256) envfree; - function additionalData(address) external returns uint128 envfree; - function _.finalizeTransfer(address, address, address, uint256, uint256, uint256) external => NONDET; - - function scaledTotalSupply() external returns (uint256); - function scaledBalanceOf(address) external returns (uint256); - function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; -} - -function PLUS256(uint256 x, uint256 y) returns uint256 { - return (assert_uint256( (x+y) % 2^256) ); -} -function MINUS256(uint256 x, uint256 y) returns uint256 { - return (assert_uint256( (x-y) % 2^256) ); -} - -definition ray() returns uint = 1000000000000000000000000000; -definition bound() returns mathint = ((gRNI() / ray()) + 1 ) / 2; - -/* - Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. -*/ -definition bounded_error_eq(uint x, uint y, uint scale) returns bool = - to_mathint(x) <= to_mathint(y) + (bound() * scale) && - to_mathint(x) + (bound() * scale) >= to_mathint(y); - -persistent ghost sumAllBalance() returns mathint { - init_state axiom sumAllBalance() == 0; -} - -// summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) -ghost gRNI() returns uint256 { - axiom to_mathint(gRNI()) == 7 * ray(); -} - -hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) { - havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; -} - -invariant totalSupplyEqualsSumAllBalance(env e) - totalSupply(e) == scaledBalanceOfToBalanceOf(require_uint256(sumAllBalance())) - filtered { f -> !f.isView } - { - preserved mint(address caller, address onBehalfOf, uint256 amount, uint256 index) with (env e2) { - require index == gRNI(); - } - preserved burn(address from, address receiverOfUnderlying, uint256 amount, uint256 index) with (env e3) { - require index == gRNI(); - } - } - -// Rule to verify that permit sets the allowance correctly. -rule permitIntegrity(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { - env e; - uint256 nonceBefore = nonces(owner); - permit(e, owner, spender, value, deadline, v, r, s); - assert allowance(owner, spender) == value; - assert to_mathint(nonces(owner)) == nonceBefore + 1; -} - -// can't mint zero Tokens -rule mintArgsPositive(address user, uint256 amount, uint256 index) { - env e; - address caller; - mint@withrevert(e, caller, user, amount, index); - assert amount == 0 => lastReverted; -} - -/** - Check that each possible operation changes the balance of at most two users -*/ -rule balanceOfChange(address a, address b, address c, method f ) - filtered { f -> !f.isView } -{ - env e; - require a!=b && a!=c && b!=c; - uint256 balanceABefore = balanceOf(a); - uint256 balanceBBefore = balanceOf(b); - uint256 balanceCBefore = balanceOf(c); - - calldataarg arg; - f(e, arg); - - uint256 balanceAAfter = balanceOf(a); - uint256 balanceBAfter = balanceOf(b); - uint256 balanceCAfter = balanceOf(c); - - assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter || balanceCBefore == balanceCAfter); -} - -/** - Mint to user u amount of x tokens, increases his balanceOf the underlying asset by x and - AToken total suplly should increase. -*/ -rule integrityMint(address a, address b, uint256 x) { - env e; - uint256 indexRay = gRNI(); - - uint256 underlyingBalanceBefore = balanceOf(a); - uint256 atokenBlanceBefore = scaledBalanceOf(e, a); - uint256 totalATokenSupplyBefore = scaledTotalSupply(e); - - mint(e,b,a,x,indexRay); - - uint256 underlyingBalanceAfter = balanceOf(a); - uint256 atokenBlanceAfter = scaledBalanceOf(e, a); - uint256 totalATokenSupplyAfter = scaledTotalSupply(e); - - assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore; - assert totalATokenSupplyAfter > totalATokenSupplyBefore; - assert bounded_error_eq(underlyingBalanceAfter, PLUS256(underlyingBalanceBefore,x), 1); -} - -/* - Mint is additive, can performed either all at once or gradually - mint(u,x); mint(u,y) ~ mint(u,x+y) at the same initial state -*/ -rule additiveMint(address a, address b, address c, uint256 x, uint256 y) { - env e; - uint256 indexRay = gRNI(); - require(balanceOf(a) == balanceOf(b) && a != b); - uint256 balanceScenario0 = balanceOf(a); - mint(e,c,a,x,indexRay); - mint(e,c,a,y,indexRay); - uint256 balanceScenario1 = balanceOf(a); - mint(e, c, b, PLUS256(x,y) ,indexRay); - - uint256 balanceScenario2 = balanceOf(b); - assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "mint is not additive"; -} - -/* - transfers amount from _userState[from].balance to _userState[to].balance - while balance of returns _userState[account].balance normalized by gNRI(); - transfer is incentivizedERC20 -*/ -rule integrityTransfer(address from, address to, uint256 amount) { - env e; - require e.msg.sender == from; - address other; // for any address including from, to, currentContract the underlying asset balance should stay the same - - uint256 balanceBeforeFrom = balanceOf(from); - uint256 balanceBeforeTo = balanceOf(to); - uint256 underlyingBeforeOther = _underlyingAsset.balanceOf(e, other); - - require(amount <= balanceBeforeFrom); // Add this require inorder to move to CVL2 - - transfer(e, to, amount); - - uint256 balanceAfterFrom = balanceOf(from); - uint256 balanceAfterTo = balanceOf(to); - uint256 underlyingAfterOther = _underlyingAsset.balanceOf(e, other); - - assert underlyingAfterOther == underlyingBeforeOther, "unexpected change in underlying asserts"; - - if (from != to) { - assert bounded_error_eq(balanceAfterFrom, MINUS256(balanceBeforeFrom,amount), 1) && - bounded_error_eq(balanceAfterTo, PLUS256(balanceBeforeTo,amount), 1), "unexpected balance of from/to, when from!=to"; - } else { - assert balanceAfterFrom == balanceAfterTo , "unexpected balance of from/to, when from==to"; - } -} - - -/* - Transfer is additive, can performed either all at once or gradually - transfer(from,to,x); transfer(from,to,y) ~ transfer(from,to,x+y) at the same initial state -*/ -rule additiveTransfer(address from1, address from2, address to1, address to2, uint256 x, uint256 y) { - env e1; - env e2; - uint256 indexRay = gRNI(); - require ( - from1 != from2 && to1 != to2 && from1 != to2 && from2 != to1 && - (from1 == to1 <=> from2 == to2) && - balanceOf(from1) == balanceOf(from2) && balanceOf(to1) == balanceOf(to2) - ); - - require e1.msg.sender == from1; - require e2.msg.sender == from2; - transfer(e1, to1, x); - transfer(e1, to1, y); - uint256 balanceFromScenario1 = balanceOf(from1); - uint256 balanceToScenario1 = balanceOf(to1); - - transfer(e2, to2, PLUS256(x,y)); - - uint256 balanceFromScenario2 = balanceOf(from2); - uint256 balanceToScenario2 = balanceOf(to2); - - assert - bounded_error_eq(balanceFromScenario1, balanceFromScenario2, 3) && - bounded_error_eq(balanceToScenario1, balanceToScenario2, 3), "transfer is not additive"; -} - - -/* - Burn scaled amount of Atoken from 'user' and transfers amount of the underlying asset to 'to'. -*/ -rule integrityBurn(address user, address to, uint256 amount) { - env e; - uint256 indexRay = gRNI(); - - require user != currentContract; - uint256 balanceBeforeUser = balanceOf(user); - uint256 balanceBeforeTo = balanceOf(to); - uint256 underlyingBeforeTo = _underlyingAsset.balanceOf(e, to); - uint256 underlyingBeforeUser = _underlyingAsset.balanceOf(e, user); - uint256 underlyingBeforeSystem = _underlyingAsset.balanceOf(e, currentContract); - uint256 totalSupplyBefore = totalSupply(e); - - require(amount <= underlyingBeforeSystem); // Add this require inorder to move to CVL2 - require(amount <= balanceBeforeUser); // Add this require inorder to move to CVL2 - require(amount <= totalSupplyBefore); // Add this require inorder to move to CVL2 - - burn(e, user, to, amount, indexRay); - - uint256 balanceAfterUser = balanceOf(user); - uint256 balanceAfterTo = balanceOf(to); - uint256 underlyingAfterTo = _underlyingAsset.balanceOf(e, to); - uint256 underlyingAfterUser = _underlyingAsset.balanceOf(e, user); - uint256 underlyingAfterSystem = _underlyingAsset.balanceOf(e, currentContract); - uint256 totalSupplyAfter = totalSupply(e); - - if (user != to) { - assert balanceAfterTo == balanceBeforeTo && // balanceOf To should not change - bounded_error_eq(underlyingBeforeUser, underlyingAfterUser, 1), "integrity break on user!=to"; - } - - if (to != currentContract) { - assert bounded_error_eq(underlyingAfterSystem, MINUS256(underlyingBeforeSystem,amount), 1) && // system transfer underlying_asset - bounded_error_eq(underlyingAfterTo, PLUS256(underlyingBeforeTo,amount), 1) , "integrity break on to!=currentContract"; - } else { - assert underlyingAfterSystem == underlyingBeforeSystem, "integrity break on to==currentContract"; - } - - assert bounded_error_eq(totalSupplyAfter, MINUS256(totalSupplyBefore,amount), 1), "total supply integrity"; // total supply reduced - assert bounded_error_eq(balanceAfterUser, MINUS256(balanceBeforeUser,amount), 1), "integrity break"; // user burns ATokens to recieve underlying -} - -/* - Burn is additive, can performed either all at once or gradually - burn(from,to,x,index); burn(from,to,y,index) ~ burn(from,to,x+y,index) at the same initial state -*/ -rule additiveBurn(address user1, address user2, address to1, address to2, uint256 x, uint256 y) { - env e; - uint256 indexRay = gRNI(); - require ( - user1 != user2 && to1 != to2 && user1 != to2 && user2 != to1 && - (user1 == to1 <=> user2 == to2) && - balanceOf(user1) == balanceOf(user2) && balanceOf(to1) == balanceOf(to2) - ); - require user1 != currentContract && user2 != currentContract; - - burn(e, user1, to1, x, indexRay); - burn(e, user1, to1, y, indexRay); - uint256 balanceUserScenario1 = balanceOf(user1); - - burn(e, user2, to2, PLUS256(x,y), indexRay); - uint256 balanceUserScenario2 = balanceOf(user2); - - assert bounded_error_eq(balanceUserScenario1, balanceUserScenario2, 3), "burn is not additive"; -} - -/* - Burning one user atokens should have no effect on other users that are not involved in the action. -*/ -rule burnNoChangeToOther(address user, address recieverOfUnderlying, uint256 amount, uint256 index, address other) { - require other != user && other != recieverOfUnderlying; - env e; - uint256 otherDataBefore = additionalData(other); - uint256 otherBalanceBefore = balanceOf(other); - - burn(e, user, recieverOfUnderlying, amount, index); - - uint256 otherDataAfter = additionalData(other); - uint256 otherBalanceAfter = balanceOf(other); - - assert otherDataBefore == otherDataAfter && - otherBalanceBefore == otherBalanceAfter; -} - -/* - Minting ATokens for a user should have no effect on other users that are not involved in the action. -*/ -rule mintNoChangeToOther(address user, uint256 amount, uint256 index, address other) { - require other != user; - - env e; - uint128 otherDataBefore = additionalData(other); - uint256 otherBalanceBefore = balanceOf(other); - address caller; - mint(e, caller, user, amount, index); - - uint128 otherDataAfter = additionalData(other); - uint256 otherBalanceAfter = balanceOf(other); - - assert otherBalanceBefore == otherBalanceAfter && otherDataBefore == otherDataAfter; -} diff --git a/certora/deprecated/specs/NEW-CVLMath.spec b/certora/deprecated/specs/NEW-CVLMath.spec deleted file mode 100644 index a18d40f1..00000000 --- a/certora/deprecated/specs/NEW-CVLMath.spec +++ /dev/null @@ -1,198 +0,0 @@ -/****************************************** ------------ CVL Math Library -------------- -*******************************************/ - -// A restriction on the value of w = x * y / z -// The ratio between x (or y) and z is a rational number a/b or b/a. -// Important : do not set a = 0 or b = 0. -// Note: constRatio(x,y,z,a,b,w) <=> constRatio(x,y,z,b,a,w) -definition constRatio(uint256 x, uint256 y, uint256 z, uint256 a, uint256 b, uint256 w) returns bool = - ( a * x == b * z && to_mathint(w) == (b * y) / a ) || - ( b * x == a * z && to_mathint(w) == (a * y) / b ) || - ( a * y == b * z && to_mathint(w) == (b * x) / a ) || - ( b * y == a * z && to_mathint(w) == (a * x) / b ); - -// A restriction on the value of w = x * y / z -// The division quotient between x (or y) and z is an integer q or 1/q. -// Important : do not set q=0 -definition constQuotient(uint256 x, uint256 y, uint256 z, uint256 q, uint256 w) returns bool = - ( to_mathint(x) == q * z && to_mathint(w) == q * y ) || - ( q * x == to_mathint(z) && to_mathint(w) == y / q ) || - ( to_mathint(y) == q * z && to_mathint(w) == q * x ) || - ( q * y == to_mathint(z) && to_mathint(w) == x / q ); - -/// Equivalent to the one above, but with implication -definition constQuotientImply(uint256 x, uint256 y, uint256 z, uint256 q, uint256 w) returns bool = - ( to_mathint(x) == q * z => to_mathint(w) == q * y ) && - ( q * x == to_mathint(z) => to_mathint(w) == y / q ) && - ( to_mathint(y) == q * z => to_mathint(w) == q * x ) && - ( q * y == to_mathint(z) => to_mathint(w) == x / q ); - -definition ONE18() returns uint256 = 1000000000000000000; -definition RAY() returns uint256 = 10^27; - -definition _monotonicallyIncreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = - (x > y => fx >= fy); - -definition _monotonicallyDecreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = - (x > y => fx <= fy); - -definition abs(mathint x) returns mathint = - x >= 0 ? x : 0 - x; - -definition min(mathint x, mathint y) returns mathint = - x > y ? y : x; - -definition max(mathint x, mathint y) returns mathint = - x > y ? x : y; - -/// Returns whether y is equal to x up to error bound of 'err' (18 decs). -/// e.g. 10% relative error => err = 1e17 -definition relativeErrorBound(mathint x, mathint y, mathint err) returns bool = - (x != 0 - ? abs(x - y) * ONE18() <= abs(x) * err - : abs(y) <= err); - -/// Axiom for a weighted average of the form WA = (x * y) / (y + z) -/// This is valid as long as z + y > 0 => make certain of that condition in the use of this definition. -definition weightedAverage(mathint x, mathint y, mathint z, mathint WA) returns bool = - ((x > 0 && y > 0) => (WA >= 0 && WA <= x)) - && - ((x < 0 && y > 0) => (WA <= 0 && WA >= x)) - && - ((x > 0 && y < 0) => (WA <= 0 && WA - x <= 0)) - && - ((x < 0 && y < 0) => (WA >= 0 && WA + x <= 0)) - && - ((x == 0 || y == 0) => (WA == 0)); - - -function mulDivDownAbstract(uint256 x, uint256 y, uint256 z) returns uint256 { - require z !=0; - uint256 xy = require_uint256(x * y); - uint256 res; - mathint rem; - require z * res + rem == to_mathint(xy); - require rem < to_mathint(z); - return res; -} - -function mulDivDownAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { - uint256 res; - require z != 0; - uint256 xy = require_uint256(x * y); - uint256 fz = require_uint256(res * z); - - require xy >= fz; - require fz + z > to_mathint(xy); - return res; -} - -function mulDivUpAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { - uint256 res; - require z != 0; - uint256 xy = require_uint256(x * y); - uint256 fz = require_uint256(res * z); - require xy >= fz; - require fz + z > to_mathint(xy); - - if (xy == fz) { - return res; - } - return require_uint256(res + 1); -} - -function mulDownWad(uint256 x, uint256 y) returns uint256 { - return mulDivDownAbstractPlus(x, y, ONE18()); -} - -function mulUpWad(uint256 x, uint256 y) returns uint256 { - return mulDivUpAbstractPlus(x, y, ONE18()); -} - -function divDownWad(uint256 x, uint256 y) returns uint256 { - return mulDivDownAbstractPlus(x, ONE18(), y); -} - -function divUpWad(uint256 x, uint256 y) returns uint256 { - return mulDivUpAbstractPlus(x, ONE18(), y); -} - -function discreteQuotientMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 { - uint256 res; - require z != 0 && noOverFlowMul(x, y); - // Discrete quotients: - require( - ((x ==0 || y ==0) && res == 0) || - (x == z && res == y) || - (y == z && res == x) || - constQuotient(x, y, z, 2, res) || // Division quotient is 1/2 or 2 - constQuotient(x, y, z, 5, res) || // Division quotient is 1/5 or 5 - constQuotient(x, y, z, 100, res) // Division quotient is 1/100 or 100 - ); - return res; -} - -function discreteRatioMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 { - uint256 res; - require z != 0 && noOverFlowMul(x, y); - // Discrete ratios: - require( - ((x ==0 || y ==0) && res == 0) || - (x == z && res == y) || - (y == z && res == x) || - constRatio(x, y, z, 2, 1, res) || // f = 2*x or f = x/2 (same for y) - constRatio(x, y, z, 5, 1, res) || // f = 5*x or f = x/5 (same for y) - constRatio(x, y, z, 2, 3, res) || // f = 2*x/3 or f = 3*x/2 (same for y) - constRatio(x, y, z, 2, 7, res) // f = 2*x/7 or f = 7*x/2 (same for y) - ); - return res; -} - -function noOverFlowMul(uint256 x, uint256 y) returns bool { - return x * y <= max_uint; -} - -/// @doc Ghost power function that incorporates mathematical pure x^y axioms. -/// @warning Some of these axioms might be false, depending on the Solidity implementation -/// The user must bear in mind that equality-like axioms can be violated because of rounding errors. -ghost _ghostPow(uint256, uint256) returns uint256 { - /// x^0 = 1 - axiom forall uint256 x. _ghostPow(x, 0) == ONE18(); - /// 0^x = 1 - axiom forall uint256 y. _ghostPow(0, y) == 0; - /// x^1 = x - axiom forall uint256 x. _ghostPow(x, ONE18()) == x; - /// 1^y = 1 - axiom forall uint256 y. _ghostPow(ONE18(), y) == ONE18(); - - /// I. x > 1 && y1 > y2 => x^y1 > x^y2 - /// II. x < 1 && y1 > y2 => x^y1 < x^y2 - axiom forall uint256 x. forall uint256 y1. forall uint256 y2. - x >= ONE18() && y1 > y2 => _ghostPow(x, y1) >= _ghostPow(x, y2); - axiom forall uint256 x. forall uint256 y1. forall uint256 y2. - x < ONE18() && y1 > y2 => (_ghostPow(x, y1) <= _ghostPow(x, y2) && _ghostPow(x,y2) <= ONE18()); - axiom forall uint256 x. forall uint256 y. - x < ONE18() && y > ONE18() => (_ghostPow(x, y) <= x); - axiom forall uint256 x. forall uint256 y. - x < ONE18() && y <= ONE18() => (_ghostPow(x, y) >= x); - axiom forall uint256 x. forall uint256 y. - x >= ONE18() && y > ONE18() => (_ghostPow(x, y) >= x); - axiom forall uint256 x. forall uint256 y. - x >= ONE18() && y <= ONE18() => (_ghostPow(x, y) <= x); - /// x1 > x2 && y > 0 => x1^y > x2^y - axiom forall uint256 x1. forall uint256 x2. forall uint256 y. - x1 > x2 => _ghostPow(x1, y) >= _ghostPow(x2, y); -} - -function CVLPow(uint256 x, uint256 y) returns uint256 { - if (y == 0) {return ONE18();} - if (x == 0) {return 0;} - return _ghostPow(x, y); -} - -function CVLSqrt(uint256 x) returns uint256 { - mathint SQRT; - require SQRT*SQRT <= to_mathint(x) && (SQRT + 1)*(SQRT + 1) > to_mathint(x); - return require_uint256(SQRT); -} diff --git a/certora/deprecated/specs/NEW-pool-base.spec b/certora/deprecated/specs/NEW-pool-base.spec deleted file mode 100644 index 68e386d8..00000000 --- a/certora/deprecated/specs/NEW-pool-base.spec +++ /dev/null @@ -1,167 +0,0 @@ -/* - This is a Base Specification File for Smart Contract Verification with the Certora Prover. - This file is meant to be included -*/ - -import "NEW-CVLMath.spec"; - -/* - Declaration of contracts used in the spec -*/ -using ATokenHarness as _aToken; -using PoolHarness as PH; -using AaveProtocolDataProvider as _dataProvider; -using SimpleERC20 as _underlyingAsset; - -/* - Methods Summerizations and Enviroment-Free (e.g relative to e.msg variables) Declarations -*/ - -methods { - // Pool - function _.handleAction(address, uint256, uint256) external => NONDET; - function _.getAssetPrice(address) external => NONDET; - function _.getPriceOracle() external => ALWAYS(2); - function _.getPriceOracleSentinel() external => ALWAYS(4); - - function _.calculateCompoundedInterest(uint256 x, uint40 t0, uint256 t1) internal => calculateCompoundedInterestSummary(x, t0, t1) expect uint256 ALL; - - // ERC20 - function _.transfer(address, uint256) external => DISPATCHER(true); - function _.transferFrom(address, address, uint256) external => DISPATCHER(true); - function _.approve(address, uint256) external => DISPATCHER(true); - //function _.mint(address, uint256) external => DISPATCHER(true); - //function _.burn(uint256) external => DISPATCHER(true); - function _.balanceOf(address) external => DISPATCHER(true); - - function _.totalSupply() external => DISPATCHER(true); - - // ATOKEN - //function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true); - //function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true); - function _.mintToTreasury(uint256 amount, uint256 index) external => DISPATCHER(true); - function _.transferOnLiquidation(address from, address to, uint256 value) external => DISPATCHER(true); - function _.transferUnderlyingTo(address user, uint256 amount) external => DISPATCHER(true); - // function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true); - function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external => DISPATCHER(true); - function _.ATokenBalanceOf(address user) external => DISPATCHER(true); - - // Unsat Core Based - function _.getParams(DataTypes.ReserveConfigurationMap memory self) internal => NONDET; - - function _.calculateUserAccountData(mapping(address => DataTypes.ReserveData) storage reservesData,mapping(uint256 => address) storage reservesList,mapping(uint8 => DataTypes.EModeCategory) storage eModeCategories,DataTypes.CalculateUserAccountDataParams memory params) internal => NONDET; - function _._getUserBalanceInBaseCurrency(address user,DataTypes.ReserveData storage reserve,uint256 assetPrice,uint256 assetUnit) internal => NONDET; - function _.wadDiv(uint256 a, uint256 b) internal => NONDET; - function _.wadToRay(uint256 a) internal => NONDET; - function _._calculateDomainSeparator() internal => NONDET; - - - // Debt Tokens - function _.scaledTotalSupply() external => DISPATCHER(true); - - function _.getReserveNormalizedIncome(address asset) external => DISPATCHER(true); - function _.getReserveNormalizedVariableDebt(address asset) external => DISPATCHER(true); - function _.getACLManager() external => DISPATCHER(true); - //function _.isBridge(address) external => DISPATCHER(true); - - // variableDebt - function _.burn(address user, uint256 amount, uint256 index) external => DISPATCHER(true); - - function getActive(DataTypes.ReserveConfigurationMap) external returns (bool); - function getFrozen(DataTypes.ReserveConfigurationMap) external returns (bool); - function getBorrowingEnabled(DataTypes.ReserveConfigurationMap) external returns (bool); -} - -/* definitions and functions to be used within the spec file */ - -definition IS_UINT256(uint256 x) returns bool = ((x >= 0) && (x <= max_uint256)); - -function first_term(uint256 x, uint256 y) returns uint256 { return x; } - -ghost mapping(uint256 => mapping(uint256 => uint256)) calculateCompoundedInterestSummaryValues; - -function calculateCompoundedInterestSummary(uint256 rate, uint40 t0, uint256 t1) returns uint256 -{ - uint256 deltaT = assert_uint256( (t1-t0) % 2^256 ); - if (deltaT == 0) { - return RAY(); - } - if (rate == RAY()) { - return RAY(); - } - if (rate >= RAY()) { - require calculateCompoundedInterestSummaryValues[rate][deltaT] >= rate; - } - else { - require calculateCompoundedInterestSummaryValues[rate][deltaT] < rate; - } - return calculateCompoundedInterestSummaryValues[rate][deltaT]; -} - -function isActiveReserve(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - DataTypes.ReserveConfigurationMap configuration = data.configuration; - bool isActive = getActive(e, configuration); - - return isActive; -} - -function isFrozenReserve(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - DataTypes.ReserveConfigurationMap configuration = data.configuration; - bool isFrozen = getFrozen(e, configuration); - - return isFrozen; -} - -function isEnabledForBorrow(env e, address asset) returns bool { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - DataTypes.ReserveConfigurationMap configuration = data.configuration; - bool isBorrowEnabled = getBorrowingEnabled(e, configuration); - - return isBorrowEnabled; -} - -function getCurrentLiquidityRate(env e, address asset) returns mathint { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - return data.currentLiquidityRate; -} - -function getLiquidityIndex(env e, address asset) returns mathint { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - return data.liquidityIndex; -} - -function aTokenBalanceOf(env e, address user) returns uint256 { - return _aToken.ATokenBalanceOf(e, user); -} - -function rayMulPreciseSummarization(uint256 x, uint256 y) returns uint256 { - if ((x == 0) || (y == 0)) { - return 0; - } - if (x == RAY()) { - return y; - } - if (y == RAY()) { - return x; - } - - mathint c = x * y; - return require_uint256(c / RAY()); -} - -function rayDivPreciseSummarization(uint256 x, uint256 y) returns uint256 { - require y != 0; - if (x == 0) { - return 0; - } - if (y == RAY()) { - return x; - } - if (y == x) { - return RAY(); - } - mathint c = x * RAY(); - return require_uint256(c / y); -} diff --git a/certora/deprecated/specs/NEW-pool-no-summarizations.spec b/certora/deprecated/specs/NEW-pool-no-summarizations.spec deleted file mode 100644 index 826b0fb7..00000000 --- a/certora/deprecated/specs/NEW-pool-no-summarizations.spec +++ /dev/null @@ -1,156 +0,0 @@ -import "NEW-pool-base.spec"; - -methods { - function _.hasRole(bytes32 b ,address a) external => DISPATCHER(true); - - function _.getReservesList() external => DISPATCHER(true); - function _.getReserveData(address a) external => DISPATCHER(true); - - function _.symbol() external => DISPATCHER(true); - function _.isFlashBorrower(address a) external => DISPATCHER(true); - - // function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true); - - function _.isPoolAdmin(address a) external => DISPATCHER(true); - function _.getConfiguration(address a) external => DISPATCHER(true); - - function _.rayMul(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, b, 10^27) expect uint256 ALL; - function _.rayDiv(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, 10^27, b) expect uint256 ALL; - - // IPriceOracleSentinel - function _.isBorrowAllowed() external => DISPATCHER(true); - function _.isLiquidationAllowed() external => DISPATCHER(true); - function _.setSequencerOracle(address newSequencerOracle) external => DISPATCHER(true); - function _.setGracePeriod(uint256 newGracePeriod) external => DISPATCHER(true); - function _.getGracePeriod() external => DISPATCHER(true); - - // Modification of index is tracked by incrementCounter: - function _.incrementCounter() external => ghostUpdate() expect bool ALL; -} - -ghost mathint counterUpdateIndexes; - -function ghostUpdate() returns bool { - counterUpdateIndexes = counterUpdateIndexes + 1; - return true; -} - - -function calculateInterestRatesMock(DataTypes.CalculateInterestRatesParams params) returns (uint256, uint256) { - uint256 liquidityRate = 1; - uint256 variableBorrowRate = 1; - return (liquidityRate, variableBorrowRate); -} - - -/* ================================================================================================= - @title Rule checking, that the ghostUpdate summary is correct and that it is being applied - This rule is part of a check, that the liquidity index cannot decrease. - - Nissan remark on 26/03/2024: This rule fails! - See here: https://prover.certora.com/output/66114/812c9675658a4d4d935a8e0a3e1f4a99/?anonymousKey=46e0337ab421a402e525e156b4aa1fb7a9b2fce9 - ================================================================================================ */ -rule _updateIndexesWrapperReachable(env e, method f) { - calldataarg args; - - mathint updateIndexesCallCountBefore = counterUpdateIndexes; - f(e, args); - - mathint updateIndexesCallCountAfter = counterUpdateIndexes; - - satisfy updateIndexesCallCountBefore != updateIndexesCallCountAfter; -} - -// @title cumulateToLiquidityIndex does not decrease the liquidity index. -// This rule is part of a check, that the liquidity index cannot decrease. -// Proved here: -// https://prover.certora.com/output/40577/bb018f9a52b64b27a0ac364e0c22cd79/?anonymousKey=21613bfbfc0f479ed2c99ce5fa2dd16e581baf5e -rule liquidityIndexNonDecresingFor_cumulateToLiquidityIndex() { - address asset; - uint256 totalLiquidity; - uint256 amount; - env e; - - uint256 reserveLiquidityIndexBefore = getReserveLiquidityIndex(e, asset); - require reserveLiquidityIndexBefore >= RAY(); - - uint256 reserveLiquidityIndexAfter = cumulateToLiquidityIndex(e, asset, totalLiquidity, amount); - - assert reserveLiquidityIndexAfter >= reserveLiquidityIndexBefore; -} - - -function get_AToken_of_asset(env e, address asset) returns address { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - return data.aTokenAddress; -} - - -/* =========================================================================================== - When a user deposits X amount of an asset and the current liquidity index for this asset is 1, - his scaled balance (=superBalance) increases by X. - - Note: Using superBalance is easier for the prover as we do not need to compute the balance - from the scaled balance. - WE ALLOW OFF BY ONE RAY. - =========================================================================================== */ -rule depositUpdatesUserATokenSuperBalance(env e) { - address asset; - uint256 amount; - address onBehalfOf; - uint16 referralCode; - - require to_mathint(amount) == 30*RAY(); //under approx - require asset != onBehalfOf; - require onBehalfOf != _aToken; - require e.msg.sender != _aToken; - require e.msg.sender != asset; - require asset == _aToken.UNDERLYING_ASSET_ADDRESS(e); - require get_AToken_of_asset(e,asset) == _aToken; - - mathint superBalanceBefore = _aToken.superBalance(e, onBehalfOf); - require superBalanceBefore == 20*RAY(); //under approx - mathint liquidityIndexBefore = getLiquidityIndex(e, asset); - require liquidityIndexBefore == 1*RAY(); //under approx - mathint currentLiquidityRateBefore = getCurrentLiquidityRate(e, asset); - require currentLiquidityRateBefore == 1; //under approx - - deposit(e, asset, amount, onBehalfOf, referralCode); - - mathint superBalanceAfter = _aToken.superBalance(e, onBehalfOf); - mathint currentLiquidityRateAfter = getCurrentLiquidityRate(e, asset); - require currentLiquidityRateAfter == currentLiquidityRateBefore; - - mathint liquidityIndexAfter = getLiquidityIndex(e, asset); - - require liquidityIndexAfter == liquidityIndexBefore; - assert superBalanceAfter >= superBalanceBefore + amount - 1 * RAY(); - assert superBalanceAfter <= superBalanceBefore + amount + 1 * RAY(); -} - -/* =========================================================================================== - Depositing on behalf of user A does not change balance of user other than A. - ========================================================================================= */ -rule depositCannotChangeOthersATokenSuperBalance(env e) { - address asset; - uint256 amount; - address onBehalfOf; - address otherUser; - uint16 referralCode; - - require to_mathint(amount) == 30*RAY(); //under approx - require asset != onBehalfOf; - require onBehalfOf != _aToken; - require e.msg.sender != _aToken; - require e.msg.sender != asset; - require asset == _aToken.UNDERLYING_ASSET_ADDRESS(e); - require otherUser != onBehalfOf; - require otherUser != _aToken; - - mathint superBalanceBefore = _aToken.superBalance(e, otherUser); - - deposit(e, asset, amount, onBehalfOf, referralCode); - - mathint superBalanceAfter = _aToken.superBalance(e, otherUser); - assert superBalanceAfter == superBalanceBefore; -} diff --git a/certora/deprecated/specs/NEW-pool-simple-properties.spec b/certora/deprecated/specs/NEW-pool-simple-properties.spec deleted file mode 100644 index b9e024a3..00000000 --- a/certora/deprecated/specs/NEW-pool-simple-properties.spec +++ /dev/null @@ -1,207 +0,0 @@ -import "NEW-pool-base.spec"; - -methods { - function _._getUserDebtInBaseCurrency(address user, DataTypes.ReserveData storage reserve, uint256 assetPrice, uint256 assetUnit) internal => NONDET; - - function _.rayMul(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, b, 10^27) expect uint256 ALL; - function _.rayDiv(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, 10^27, b) expect uint256 ALL; -} - -ghost mapping(uint256 => mapping(uint256 => uint256)) rayMulSummariztionValues; -ghost mapping(uint256 => mapping(uint256 => uint256)) rayDivSummariztionValues; - -function rayMulSummariztion(uint256 x, uint256 y) returns uint256 { - if ((x == 0) || (y == 0)) { - return 0; - } - if (x == RAY()) { - return y; - } - if (y == RAY()) { - return x; - } - - if (y > x) { - if (y > RAY()) { - require rayMulSummariztionValues[y][x] >= x; - } - if (x > RAY()) { - require rayMulSummariztionValues[y][x] >= y; - } - return rayMulSummariztionValues[y][x]; - } - else { - if (x > RAY()) { - require rayMulSummariztionValues[x][y] >= y; - } - if (y > RAY()) { - require rayMulSummariztionValues[x][y] >= x; - } - return rayMulSummariztionValues[x][y]; - } -} - -function rayDivSummariztion(uint256 x, uint256 y) returns uint256 { - if (x == 0) { - return 0; - } - if (y == RAY()) { - return x; - } - if (y == x) { - return RAY(); - } - require y > RAY() => rayDivSummariztionValues[x][y] <= x; - require y < RAY() => x <= rayDivSummariztionValues[x][y]; - return rayDivSummariztionValues[x][y]; -} - -// Passing for PoolHarness: -// https://prover.certora.com/output/40577/e75bfa369a10490ca0cc71992984dc54/?anonymousKey=c12450d39df13d66fd92b82819c9dcc7f66d2012 -rule method_reachability(env e, method f) { - calldataarg args; - f(e, args); - satisfy true; -} - -// @title It is impossible to deposit an inactive reserve -// Proved: -// https://prover.certora.com/output/40577/b8bd6244053e42e4bddb129f04e1dd93/?anonymousKey=5374001e512e1149d120f0efa19c18a3d531d115 -// Note, that getFlags must not be NONDET. -rule cannotDepositInInactiveReserve(env e) { - address asset; - uint256 amount; - address onBehalfOf; - uint16 referralCode; - bool reserveIsActive = isActiveReserve(e, asset); - - deposit(e, asset, amount, onBehalfOf, referralCode); - - assert reserveIsActive; -} - -// @title It is impossible to deposit a frozen reserve -// Proved: -// https://prover.certora.com/output/40577/d4f2bfae10ae4092bb7dab309e72b166/?anonymousKey=a370279a63e87a810fd79cb20d33ef00aead7c2b -// Note, that getFlags must not be NONDET. -rule cannotDepositInFrozenReserve(env e) { - address asset; - uint256 amount; - address onBehalfOf; - uint16 referralCode; - bool reserveIsFrozen = isFrozenReserve(e, asset); - - deposit(e, asset, amount, onBehalfOf, referralCode); - - assert !reserveIsFrozen; -} - -// @title It is impossible to deposit zero amount -// Proved -// https://prover.certora.com/output/40577/400f77e9ca1948b9896ca35435b0ea03/?anonymousKey=760e8acd1473e9eb801aa4bcaf60d50927f9f026 -rule cannotDepositZeroAmount(env e) { - address asset; - uint256 amount; - address onBehalfOf; - uint16 referralCode; - - deposit(e, asset, amount, onBehalfOf, referralCode); - - assert amount != 0; -} - -// @title It is impossible to withdraw zero amount -// Proved -// https://prover.certora.com/output/40577/869e48220a2d40369884dd6a0cbd1734/?anonymousKey=7cf6aced7660c59314f767f4f14de508e38a37ea -rule cannotWithdrawZeroAmount(env e) { - address asset; - uint256 amount; - address to; - uint16 referralCode; - - withdraw(e, asset, amount, to); - - assert amount != 0; -} - -// @title It is impossible to withdraw an inactive reserve -// Proved -// https://prover.certora.com/output/40577/a4eb1d4472ae43c2a1bfe202f070453a/?anonymousKey=05c0ddc494d371d6a28fc40ed4cc1902bba29eba -// Note, that getFlags must not be NONDET. -rule cannotWithdrawFromInactiveReserve(env e) { - address asset; - uint256 amount; - address to; - uint16 referralCode; - bool reserveIsActive = isActiveReserve(e, asset); - - withdraw(e, asset, amount, to); - - assert reserveIsActive; -} - -// @title It is impossible to borrow zero amount -// Proved -// https://prover.certora.com/output/40577/13a0a08cbc6f448888bcdb28716d856b/?anonymousKey=48621623ac7255815e8a6465d72d38f39d55f0f4 -rule cannotBorrowZeroAmount(env e) { - address asset; - uint256 amount; - uint256 interestRateMode; - uint16 referralCode; - address onBehalfOf; - - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - - assert amount != 0; -} - -// @title It is impossible to borrow on inactive reserve. -// Proved -// https://prover.certora.com/output/40577/2e93cd5ce80f4aa491b9d648e1a73583/?anonymousKey=64bbd85099c3ae4a387bd0a24ce565c23094ee4f -// Note, that getFlags must not be NONDET. -rule cannotBorrowOnInactiveReserve(env e) { - address asset; - uint256 amount; - uint256 interestRateMode; - uint16 referralCode; - address onBehalfOf; - bool reserveIsActive = isActiveReserve(e, asset); - - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - - assert reserveIsActive; -} - -// It is impossible to borrow on a reserve, that is disabled for borrowing. -// Proved -// https://prover.certora.com/output/40577/1b50faf4cbb3459c9563e4af75658525/?anonymousKey=e04b8838d1f6eceb3fb29504969ecf0817269679 -// Note, that getFlags must not be NONDET. -rule cannotBorrowOnReserveDisabledForBorrowing(env e) { - address asset; - uint256 amount; - uint256 interestRateMode; - uint16 referralCode; - address onBehalfOf; - bool reserveIsEnabledForBorrow = isEnabledForBorrow(e, asset); - - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - - assert reserveIsEnabledForBorrow; -} - -// @title It is impossible to borrow on frozen reserve. -// Proved -// https://prover.certora.com/output/40577/b25ecb5e5b804832b3aa75e3bd54079c/?anonymousKey=8029d9f6ac5edf386f4795c4de0e7928f0487722 -// Note, that getFlags must not be NONDET. -rule cannotBorrowOnFrozenReserve(env e) { - address asset; - uint256 amount; - uint256 interestRateMode; - uint16 referralCode; - address onBehalfOf; - bool reserveIsFrozen = isFrozenReserve(e, asset); - - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - - assert !reserveIsFrozen; -} diff --git a/certora/deprecated/specs/ReserveConfiguration.spec b/certora/deprecated/specs/ReserveConfiguration.spec deleted file mode 100644 index b927763b..00000000 --- a/certora/deprecated/specs/ReserveConfiguration.spec +++ /dev/null @@ -1,177 +0,0 @@ -methods { - function setLtv(uint256) external envfree; - function getLtv() external returns (uint256) envfree; - function setLiquidationThreshold(uint256) external envfree; - function getLiquidationThreshold() external returns (uint256) envfree; - function setLiquidationBonus(uint256) external envfree; - function getLiquidationBonus() external returns (uint256) envfree; - function setDecimals(uint256) external envfree; - function getDecimals() external returns (uint256) envfree; - function setActive(bool) external envfree; - function getActive() external returns (bool) envfree; - function setFrozen(bool) external envfree; - function getFrozen() external returns (bool) envfree; - function setPaused(bool) external envfree; - function getPaused() external returns (bool) envfree; - function setBorrowableInIsolation(bool) external envfree; - function getBorrowableInIsolation() external returns (bool) envfree; - function setSiloedBorrowing(bool) external envfree; - function getSiloedBorrowing() external returns (bool) envfree; - function setBorrowingEnabled(bool) external envfree; - function getBorrowingEnabled() external returns (bool) envfree; - function setReserveFactor(uint256) external envfree; - function getReserveFactor() external returns (uint256) envfree; - function setBorrowCap(uint256) external envfree; - function getBorrowCap() external returns (uint256) envfree; - function setSupplyCap(uint256) external envfree; - function getSupplyCap() external returns (uint256) envfree; - function setDebtCeiling(uint256) external envfree; - function getDebtCeiling() external returns (uint256) envfree; - function setLiquidationProtocolFee(uint256) external envfree; - function getLiquidationProtocolFee() external returns (uint256) envfree; - function setUnbackedMintCap(uint256) external envfree; - function getUnbackedMintCap() external returns (uint256) envfree; - function setEModeCategory(uint256) external envfree; - function getEModeCategory() external returns (uint256) envfree; - function setFlashLoanEnabled(bool) external envfree; - function getFlashLoanEnabled() external returns (bool) envfree; - function getData() external returns uint256 envfree; - function executeIntSetterById(uint256, uint256) external envfree; - function executeIntGetterById(uint256) external returns uint256 envfree; - function executeBoolSetterById(uint256, bool) external envfree; - function executeBoolGetterById(uint256) external returns bool envfree; -} - -// checks the integrity of set LTV function and correct retrieval of the corresponding getter. -rule setLtvIntegrity(uint256 ltv) { - setLtv(ltv); - assert getLtv() == ltv; -} - -// checks the integrity of set LiquidationThreshold function and correct retrieval of the corresponding getter. -rule setLiquidationThresholdIntegrity(uint256 threshold) { - setLiquidationThreshold(threshold); - assert getLiquidationThreshold() == threshold; -} - -// checks the integrity of set LiquidationBonus function and correct retrieval of the corresponding getter. -rule setLiquidationBonusIntegrity(uint256 bonus) { - setLiquidationBonus(bonus); - assert getLiquidationBonus() == bonus; -} - -// checks the integrity of set Decimals function and correct retrieval of the corresponding getter. -rule setDecimalsIntegrity(uint256 decimals) { - setDecimals(decimals); - assert getDecimals() == decimals; -} - -// checks the integrity of set Active function and correct retrieval of the corresponding getter. -rule setActiveIntegrity(bool active) { - setActive(active); - assert getActive() == active; -} - -// checks the integrity of set Frozen function and correct retrieval of the corresponding getter. -rule setFrozenIntegrity(bool frozen) { - setFrozen(frozen); - assert getFrozen() == frozen; -} - -// checks the integrity of set Paused function and correct retrieval of the corresponding getter. -rule setPausedIntegrity(bool paused) { - setPaused(paused); - assert getPaused() == paused; -} - -// checks the integrity of set BorrowableInIsolation function and correct retrieval of the corresponding getter. -rule setBorrowableInIsolationIntegrity(bool borrowable) { - setBorrowableInIsolation(borrowable); - assert getBorrowableInIsolation() == borrowable; -} - -// checks the integrity of set SiloedBorrowing function and correct retrieval of the corresponding getter. -rule setSiloedBorrowingIntegrity(bool siloed) { - setSiloedBorrowing(siloed); - assert getSiloedBorrowing() == siloed; -} - -// checks the integrity of set BorrowingEnabled function and correct retrieval of the corresponding getter. -rule setBorrowingEnabledIntegrity(bool enabled) { - setBorrowingEnabled(enabled); - assert getBorrowingEnabled() == enabled; -} - -// checks the integrity of set ReserveFactor function and correct retrieval of the corresponding getter. -rule setReserveFactorIntegrity(uint256 reserveFactor) { - setReserveFactor(reserveFactor); - assert getReserveFactor() == reserveFactor; -} - -// checks the integrity of set BorrowCap function and correct retrieval of the corresponding getter. -rule setBorrowCapIntegrity(uint256 borrowCap) { - setBorrowCap(borrowCap); - assert getBorrowCap() == borrowCap; -} - -// checks the integrity of set SupplyCap function and correct retrieval of the corresponding getter. -rule setSupplyCapIntegrity(uint256 supplyCap) { - setSupplyCap(supplyCap); - assert getSupplyCap() == supplyCap; -} - -// checks the integrity of set DebtCeiling function and correct retrieval of the corresponding getter. -rule setDebtCeilingIntegrity(uint256 ceiling) { - setDebtCeiling(ceiling); - assert getDebtCeiling() == ceiling; -} - -// checks the integrity of set LiquidationProtocolFee function and correct retrieval of the corresponding getter. -rule setLiquidationProtocolFeeIntegrity(uint256 liquidationProtocolFee) { - setLiquidationProtocolFee(liquidationProtocolFee); - assert getLiquidationProtocolFee() == liquidationProtocolFee; -} - -// checks the integrity of set UnbackedMintCap function and correct retrieval of the corresponding getter. -rule setUnbackedMintCapIntegrity(uint256 unbackedMintCap) { - setUnbackedMintCap(unbackedMintCap); - assert getUnbackedMintCap() == unbackedMintCap; -} - -// checks the integrity of set EModeCategory function and correct retrieval of the corresponding getter. -rule setEModeCategoryIntegrity(uint256 category) { - setEModeCategory(category); - assert getEModeCategory() == category; -} - -// checks for independence of int parameters - if one parameter is being set, non of the others is being changed -rule integrityAndIndependencyOfIntSetters(uint256 funcId, uint256 otherFuncId, uint256 val) { - require 0 <= funcId && funcId <= 10; - require 0 <= otherFuncId && otherFuncId <= 10; - uint256 valueBefore = executeIntGetterById(funcId); - uint256 otherValueBefore = executeIntGetterById(otherFuncId); - - executeIntSetterById(funcId, val); - - uint256 valueAfter = executeIntGetterById(funcId); - uint256 otherValueAfter = executeIntGetterById(otherFuncId); - - assert valueAfter == val; - assert (otherFuncId != funcId => otherValueAfter == otherValueBefore); -} - -// checks for independence of bool parameters - if one parameter is being set, non of the others is being changed -rule integrityAndIndependencyOfBoolSetters(uint256 funcId, uint256 otherFuncId, bool val) { - require 0 <= funcId && funcId <= 10; - require 0 <= otherFuncId && otherFuncId <= 10; - bool valueBefore = executeBoolGetterById(funcId); - bool otherValueBefore = executeBoolGetterById(otherFuncId); - - executeBoolSetterById(funcId, val); - - bool valueAfter = executeBoolGetterById(funcId); - bool otherValueAfter = executeBoolGetterById(otherFuncId); - - assert valueAfter == val; - assert (otherFuncId != funcId => otherValueAfter == otherValueBefore); -} diff --git a/certora/deprecated/specs/UserConfiguration.spec b/certora/deprecated/specs/UserConfiguration.spec deleted file mode 100644 index 77404c28..00000000 --- a/certora/deprecated/specs/UserConfiguration.spec +++ /dev/null @@ -1,103 +0,0 @@ -methods { - function setBorrowing(uint256, bool) external envfree; - function setUsingAsCollateral(uint256, bool) external envfree; - function isUsingAsCollateralOrBorrowing(uint256) external returns bool envfree; - function isBorrowing(uint256) external returns bool envfree; - function isUsingAsCollateral(uint256) external returns bool envfree; - function isUsingAsCollateralOne() external returns bool envfree; - function isUsingAsCollateralAny() external returns bool envfree; - function isBorrowingOne() external returns (bool) envfree; - function isBorrowingAny() external returns bool envfree; - function isEmpty() external returns bool envfree; - function getIsolationModeState() external returns (bool, address, uint256) envfree; - function getSiloedBorrowingState() external returns (bool, address) envfree; -} - - -// checks the integrity of set Borrowing function and correct retrieval of the corresponding getter -rule setBorrowing(uint256 reserveIndex, bool borrowing) { - setBorrowing(reserveIndex, borrowing); - assert isBorrowing(reserveIndex) == borrowing, "unexpected result"; -} - -// checks that changes made to a specific borrowing asset doesnt effect the other assets -rule setBorrowingNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing) { - // reserveIndexOther info - bool otherReserveBorrowingBefore = isBorrowing(reserveIndexOther); - bool otherReserveCollateralBefore = isUsingAsCollateral(reserveIndexOther); - - setBorrowing(reserveIndex, borrowing); - - // reserveIndex info - bool ReserveBorrowingAfter = isBorrowing(reserveIndex); - // reserveIndexOther info - bool otherReserveBorrowingAfter = isBorrowing(reserveIndexOther); - bool otherReserveCollateralAfter = isUsingAsCollateral(reserveIndexOther); - - assert (reserveIndex != reserveIndexOther => - (otherReserveBorrowingAfter == otherReserveBorrowingBefore && - otherReserveCollateralAfter == otherReserveCollateralBefore)); -} - -// checks the integrity of set UsingAsCollateral function and correct retrieval of the corresponding getter -rule setUsingAsCollateral(uint256 reserveIndex, bool usingAsCollateral) { - setUsingAsCollateral(reserveIndex, usingAsCollateral); - assert isUsingAsCollateral(reserveIndex) == usingAsCollateral; -} - -// checks that changes made to a specific borrowing asset doesnt effect the other assets -rule setCollateralNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral) { - // reserveIndexOther info - bool otherReserveBorrowingBefore = isBorrowing(reserveIndexOther); - bool otherReserveCollateralBefore = isUsingAsCollateral(reserveIndexOther); - - setUsingAsCollateral(reserveIndex, usingAsCollateral); - - // reserveIndex info - bool ReserveBorrowingAfter = isBorrowing(reserveIndex); - // reserveIndexOther info - bool otherReserveBorrowingAfter = isBorrowing(reserveIndexOther); - bool otherReserveCollateralAfter = isUsingAsCollateral(reserveIndexOther); - - assert (reserveIndex != reserveIndexOther => - (otherReserveBorrowingAfter == otherReserveBorrowingBefore && - otherReserveCollateralAfter == otherReserveCollateralBefore)); -} - -invariant isUsingAsCollateralOrBorrowing(uint256 reserveIndex ) - (isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=> - isUsingAsCollateralOrBorrowing(reserveIndex); - -invariant integrityOfisUsingAsCollateralOne(uint256 reserveIndex, uint256 reserveIndexOther) - isUsingAsCollateral(reserveIndex) && isUsingAsCollateralOne() => - !isUsingAsCollateral(reserveIndexOther) || reserveIndexOther == reserveIndex; - -invariant integrityOfisUsingAsCollateralAny(uint256 reserveIndex) - isUsingAsCollateral(reserveIndex) => isUsingAsCollateralAny(); - -invariant integrityOfisBorrowingOne(uint256 reserveIndex, uint256 reserveIndexOther) - isBorrowing(reserveIndex) && isBorrowingOne() => !isBorrowing(reserveIndexOther) || reserveIndexOther == reserveIndex; - -invariant integrityOfisBorrowingAny(uint256 reserveIndex) - isBorrowing(reserveIndex) => isBorrowingAny(); - -invariant integrityOfEmpty(uint256 reserveIndex) - isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex); - -// if IsolationModeState is active then there must be exactly one asset register as collateral. -// note that this is a necessary requirement, but it is not sufficient. -rule integrityOfIsolationModeState() { - bool existExactlyOneCollateral = isUsingAsCollateralOne(); - bool answer; address asset; uint256 ceiling; - answer, asset, ceiling = getIsolationModeState(); - assert answer => existExactlyOneCollateral; -} - -// if IsolationModeState is active then there must be exactly one asset register as collateral. -// note that this is a necessary requirement, but it is not sufficient. -rule integrityOfSiloedBorrowingState() { - bool existExactlyOneBorrow = isBorrowingOne(); - bool answer; address asset; - answer, asset = getSiloedBorrowingState(); - assert answer => existExactlyOneBorrow; -} diff --git a/certora/deprecated/specs/VariableDebtToken.spec b/certora/deprecated/specs/VariableDebtToken.spec deleted file mode 100644 index 4f1c97b0..00000000 --- a/certora/deprecated/specs/VariableDebtToken.spec +++ /dev/null @@ -1,257 +0,0 @@ -methods { - // summarization for elimination the raymul operation in balance of and totalSupply. - function _.getReserveNormalizedVariableDebt(address asset) external => gRNVB() expect uint256 ALL; - function _.handleAction(address, uint256, uint256) external => NONDET; - function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; - function balanceOf(address) external returns (uint256) envfree; -} - -function PLUS256(uint256 x, uint256 y) returns uint256 { - return (assert_uint256( (x+y) % 2^256) ); -} - -definition ray() returns uint = 1000000000000000000000000000; -definition bound() returns mathint = ((gRNVB() / ray()) + 1 ) / 2; - -// summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) -ghost gRNVB() returns uint256 { - axiom to_mathint(gRNVB()) == 7 * ray(); -} - -/* - Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. -*/ -definition bounded_error_eq(mathint x, mathint y, mathint scale) returns bool = - x <= y + (bound() * scale) && x + (bound() * scale) >= y; - -definition disAllowedFunctions(method f) returns bool = - f.selector == sig:transfer(address, uint256).selector || - f.selector == sig:allowance(address, address).selector || - f.selector == sig:approve(address, uint256).selector || - f.selector == sig:transferFrom(address, address, uint256).selector || - f.selector == sig:increaseAllowance(address, uint256).selector || - f.selector == sig:decreaseAllowance(address, uint256).selector; - -ghost sumAllBalance() returns mathint { - init_state axiom sumAllBalance() == 0; -} -hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) { - havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; -} - -invariant totalSupplyEqualsSumAllBalance(env e) - totalSupply(e) == scaledBalanceOfToBalanceOf(require_uint256(sumAllBalance())) - filtered { f -> !f.isView && !disAllowedFunctions(f) } - { - preserved mint(address user, address onBehalfOf, uint256 amount, uint256 index) with (env e2) { - require index == gRNVB(); - } - preserved burn(address from, uint256 amount, uint256 index) with (env e3) { - require index == gRNVB(); - } - } - -// Only the pool with burn or mint operation can change the total supply. (assuming the getReserveNormalizedVariableDebt is not changed) -rule whoChangeTotalSupply(method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } -{ - env e; - uint256 oldTotalSupply = totalSupply(e); - calldataarg args; - f(e, args); - uint256 newTotalSupply = totalSupply(e); - assert oldTotalSupply != newTotalSupply => - (e.msg.sender == POOL(e) && - (f.selector == sig:burn(address, uint256, uint256).selector || - f.selector == sig:mint(address, address, uint256, uint256).selector)); -} - -/* - Each operation of Variable Debt Token can change at most one user's balance. -*/ -rule balanceOfChange(address a, address b, method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } -{ - env e; - require a != b; - uint256 balanceABefore = balanceOf(a); - uint256 balanceBBefore = balanceOf(b); - - calldataarg arg; - f(e, arg); - - uint256 balanceAAfter = balanceOf(a); - uint256 balanceBAfter = balanceOf(b); - - assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter); -} - -// only delegationWithSig operation can change the nonce. -rule nonceChangePermits(method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } -{ - env e; - address user; - uint256 oldNonce = nonces(e, user); - calldataarg args; - f(e, args); - uint256 newNonce = nonces(e, user); - assert oldNonce != newNonce => f.selector == sig:delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; -} - -// minting and then buring Variable Debt Token should have no effect on the users balance -rule inverseMintBurn(address a, address delegatedUser, uint256 amount, uint256 index) { - env e; - uint256 balancebefore = balanceOf(a); - mint(e, delegatedUser, a, amount, index); - burn(e, a, amount, index); - uint256 balanceAfter = balanceOf(a); - assert balancebefore == balanceAfter, "burn is not the inverse of mint"; -} - -rule integrityDelegationWithSig(address delegator, address delegatee, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { - env e; - uint256 oldNonce = nonces(e, delegator); - delegationWithSig(e, delegator, delegatee, value, deadline, v, r, s); - assert to_mathint(nonces(e, delegator)) == oldNonce + 1 - && - borrowAllowance(e, delegator, delegatee) == value; -} - -/** - Burning user u amount of amount tokens, decreases his balanceOf the user by amount. - (balance is decreased by amount and not scaled amount because of the summarization to one ray) -*/ -rule integrityOfBurn(address u, uint256 amount) { - env e; - uint256 index = gRNVB(); - uint256 balanceBeforeUser = balanceOf(u); - uint256 totalSupplyBefore = totalSupply(e); - - burn(e, u, amount, index); - - uint256 balanceAfterUser = balanceOf(u); - uint256 totalSupplyAfter = totalSupply(e); - - assert bounded_error_eq(totalSupplyAfter, totalSupplyBefore - amount, 1), "total supply integrity"; // total supply reduced - assert bounded_error_eq(balanceAfterUser, balanceBeforeUser - amount, 1), "integrity break"; // user burns ATokens to recieve underlying -} - -/* - Burn is additive, can performed either all at once or gradually - burn(from,to,x,index); burn(from,to,y,index) ~ burn(from,to,x+y,index) at the same initial state -*/ -rule additiveBurn(address user1, address user2, uint256 x, uint256 y) { - env e; - uint256 index = gRNVB(); - require (user1 != user2 && balanceOf(user1) == balanceOf(user2)); - require user1 != currentContract && user2 != currentContract; - - burn(e, user1, x, index); - burn(e, user1, y, index); - uint256 balanceScenario1 = balanceOf(user1); - - burn(e, user2, PLUS256(x,y), index); - uint256 balanceScenario2 = balanceOf(user2); - - assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "burn is not additive"; -} - -/* - Mint is additive, can performed either all at once or gradually - mint(from,to,x,index); mint(from,to,y,index) ~ mint(from,to,x+y,index) at the same initial state -*/ -rule additiveMint(address user1, address user2, address user3, uint256 x, uint256 y) { - env e; - uint256 index = gRNVB(); - require (user1 != user2 && balanceOf(user1) == balanceOf(user2)); - - mint(e, user3, user1, x, index); - mint(e, user3, user1, y, index); - uint256 balanceScenario1 = balanceOf(user1); - - mint(e, user3, user2, PLUS256(x,y), index); - uint256 balanceScenario2 = balanceOf(user2); - - assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "burn is not additive"; -} - -/** - Mint to user u amount of x tokens, increases his balanceOf the user by x. - (balance is increased by x and not scaled x because of the summarization to one ray) -*/ -rule integrityMint(address a, uint256 x) { - env e; - address delegatedUser; - uint256 index = gRNVB(); - uint256 underlyingBalanceBefore = balanceOf(a); - uint256 atokenBlanceBefore = scaledBalanceOf(e, a); - uint256 totalATokenSupplyBefore = scaledTotalSupply(e); - mint(e, delegatedUser, a, x, index); - - uint256 underlyingBalanceAfter = balanceOf(a); - uint256 atokenBlanceAfter = scaledBalanceOf(e, a); - uint256 totalATokenSupplyAfter = scaledTotalSupply(e); - - assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore; - assert totalATokenSupplyAfter > totalATokenSupplyBefore; - assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1); -} - -// Buring zero amount of tokens should have no effect. -rule burnZeroDoesntChangeBalance(address u, uint256 index) { - env e; - uint256 balanceBefore = balanceOf(u); - burn@withrevert(e, u, 0, index); - uint256 balanceAfter = balanceOf(u); - assert balanceBefore == balanceAfter; -} - -/* - Burning one user atokens should have no effect on other users that are not involved in the action. -*/ -rule burnNoChangeToOther(address user, uint256 amount, uint256 index, address other) { - require other != user; - - env e; - uint256 otherBalanceBefore = balanceOf(other); - - burn(e, user, amount, index); - - uint256 otherBalanceAfter = balanceOf(other); - - assert otherBalanceBefore == otherBalanceAfter; -} - -/* - Minting ATokens for a user should have no effect on other users that are not involved in the action. -*/ -rule mintNoChangeToOther(address user, address onBehalfOf, uint256 amount, uint256 index, address other) { - require other != user && other != onBehalfOf; - - env e; - uint256 userBalanceBefore = balanceOf(user); - uint256 otherBalanceBefore = balanceOf(other); - - mint(e, user, onBehalfOf, amount, index); - - uint256 userBalanceAfter = balanceOf(user); - uint256 otherBalanceAfter = balanceOf(other); - - if (user != onBehalfOf) { - assert userBalanceBefore == userBalanceAfter ; - } - - assert otherBalanceBefore == otherBalanceAfter ; -} - -/* - Ensuring that the defined disallowed functions revert in any case. -*/ -rule disallowedFunctionalities(method f) - filtered { f -> disAllowedFunctions(f) } -{ - env e; calldataarg args; - f@withrevert(e, args); - assert lastReverted; -}