From 34cd45d5fa8ac650197ed16b72ac08883e0b70a9 Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 20:08:52 +0530 Subject: [PATCH 1/6] fix: remove dead code --- .../contracts/protocol/pool/PoolConfigurator.sol | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/src/core/contracts/protocol/pool/PoolConfigurator.sol b/src/core/contracts/protocol/pool/PoolConfigurator.sol index 8655ce20..228daf6b 100644 --- a/src/core/contracts/protocol/pool/PoolConfigurator.sol +++ b/src/core/contracts/protocol/pool/PoolConfigurator.sol @@ -42,14 +42,6 @@ abstract contract PoolConfigurator is VersionedInitializable, IPoolConfigurator _; } - /** - * @dev Only emergency admin can call functions marked by this modifier. - */ - modifier onlyEmergencyAdmin() { - _onlyEmergencyAdmin(); - _; - } - /** * @dev Only emergency or pool admin can call functions marked by this modifier. */ @@ -603,11 +595,6 @@ abstract contract PoolConfigurator is VersionedInitializable, IPoolConfigurator require(aclManager.isPoolAdmin(msg.sender), Errors.CALLER_NOT_POOL_ADMIN); } - function _onlyEmergencyAdmin() internal view { - IACLManager aclManager = IACLManager(_addressesProvider.getACLManager()); - require(aclManager.isEmergencyAdmin(msg.sender), Errors.CALLER_NOT_EMERGENCY_ADMIN); - } - function _onlyPoolOrEmergencyAdmin() internal view { IACLManager aclManager = IACLManager(_addressesProvider.getACLManager()); require( From 4320de75cc7792db060429167e22f310824288ce Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 20:47:08 +0530 Subject: [PATCH 2/6] test: some fuzzing and missing tests --- .../core/PoolConfigurator.ACLModifiers.t.sol | 201 ++++++++++++++---- tests/core/StableDebtToken.t.sol | 7 +- tests/core/VariableDebtToken.t.sol | 7 +- tests/harness/StableDebtToken.sol | 12 ++ tests/harness/VariableDebtToken.sol | 12 ++ tests/periphery/ParaswapAdapters.t.sol | 14 ++ 6 files changed, 213 insertions(+), 40 deletions(-) create mode 100644 tests/harness/StableDebtToken.sol create mode 100644 tests/harness/VariableDebtToken.sol diff --git a/tests/core/PoolConfigurator.ACLModifiers.t.sol b/tests/core/PoolConfigurator.ACLModifiers.t.sol index 8f841fb6..208309a0 100644 --- a/tests/core/PoolConfigurator.ACLModifiers.t.sol +++ b/tests/core/PoolConfigurator.ACLModifiers.t.sol @@ -12,122 +12,209 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { initTestEnvironment(); } - function test_reverts_notAdmin_initReserves() public { + function test_reverts_notAdmin_initReserves(address caller) public { ConfiguratorInputTypes.InitReserveInput[] memory input; + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isAssetListingAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_ASSET_LISTING_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.initReserves(input); } - function test_reverts_notAdmin_dropReserve() public { + function test_reverts_notAdmin_dropReserve(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.dropReserve(tokenList.usdx); } - function test_reverts_notAdmin_updateAToken() public { + function test_reverts_notAdmin_updateAToken(address caller) public { ConfiguratorInputTypes.UpdateATokenInput memory input; + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.updateAToken(input); } - function test_reverts_notAdmin_updateVariableDebtToken() public { + function test_reverts_notAdmin_updateVariableDebtToken(address caller) public { ConfiguratorInputTypes.UpdateDebtTokenInput memory input; + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.updateVariableDebtToken(input); } - function test_reverts_notAdmin_updateStableDebtToken() public { + function test_reverts_notAdmin_updateStableDebtToken(address caller) public { ConfiguratorInputTypes.UpdateDebtTokenInput memory input; + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.updateStableDebtToken(input); } - function test_reverts_notAdmin_setReserveActive() public { + function test_reverts_notAdmin_setReserveActive(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveActive(tokenList.usdx, true); } - function test_reverts_notAdmin_updateFlashLoanPremiumTotal() public { + function test_reverts_notAdmin_updateFlashLoanPremiumTotal(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.updateFlashloanPremiumTotal(1); } - function test_reverts_notAdmin_updateFlashLoanPremiumProtocol() public { + function test_reverts_notAdmin_updateFlashLoanPremiumProtocol(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.updateFlashloanPremiumToProtocol(1); } - function test_reverts_notRiskAdmin_setReserveBorrowing() public { + function test_reverts_notRiskAdmin_setReserveBorrowing(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveBorrowing(address(0), true); } - function test_reverts_notRiskAdmin_configureReserveAsCollateral() public { + function test_reverts_notRiskAdmin_configureReserveAsCollateral(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.configureReserveAsCollateral(address(0), 1, 1, 1); } - function test_reverts_notRiskAdmin_setReserveStableRateBorrowing() public { + function test_reverts_notRiskAdmin_setReserveStableRateBorrowing(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveStableRateBorrowing(address(0), true); } - function test_reverts_notRiskOrPoolOrEmergencyAdmin_setReserveFreeze() public { + function test_reverts_notRiskOrPoolOrEmergencyAdmin_setReserveFreeze(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + !contracts.aclManager.isEmergencyAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_OR_EMERGENCY_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveFreeze(address(0), true); } - function test_reverts_notRiskAdmin_setReserveFactor() public { + function test_reverts_notRiskAdmin_setReserveFactor(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveFactor(address(0), 10); } - function test_reverts_notRiskAdmin_setBorrowCap() public { + function test_reverts_notRiskAdmin_setBorrowCap(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setBorrowCap(address(0), 10); } - function test_reverts_notRiskAdmin_setSupplyCap() public { + function test_reverts_notRiskAdmin_setSupplyCap(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setSupplyCap(address(0), 10); } - function test_reverts_notRiskAdmin_setReserveInterestRateStrategyAddress() public { + function test_reverts_notRiskAdmin_setReserveInterestRateStrategyAddress(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setReserveInterestRateStrategyAddress( address(0), address(0), @@ -135,24 +222,58 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ); } - function test_reverts_notRiskAdmin_setEModeCategory() public { + function test_reverts_notRiskAdmin_setReserveInterestRateData(address caller, address asset) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); + + vm.prank(caller); + contracts.poolConfiguratorProxy.setReserveInterestRateData( + asset, + bytes('0') + ); + } + + function test_reverts_notRiskAdmin_setEModeCategory(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setEModeCategory(1, 1, 1, 1, address(0), ''); } - function test_reverts_notRiskAdmin_setAssetEModeCategory() public { + function test_reverts_notRiskAdmin_setAssetEModeCategory(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setAssetEModeCategory(address(0), 1); } - function test_reverts_setDebtCeiling() public { + function test_reverts_setDebtCeiling(address caller) public { + vm.assume( + !contracts.aclManager.isPoolAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + caller != address(contracts.poolAddressesProvider) + ); + vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); - vm.prank(alice); + vm.prank(caller); contracts.poolConfiguratorProxy.setDebtCeiling(address(0), 1); } @@ -221,6 +342,10 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { vm.prank(caller); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_OR_EMERGENCY_ADMIN)); contracts.poolConfiguratorProxy.setPoolPause(paused, gracePeriod); + + vm.prank(caller); + vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_OR_EMERGENCY_ADMIN)); + contracts.poolConfiguratorProxy.setPoolPause(paused); } function test_reverts_setPoolPause_noGracePeriod_unauth(address caller, bool paused) public { diff --git a/tests/core/StableDebtToken.t.sol b/tests/core/StableDebtToken.t.sol index 28301755..2394d4b6 100644 --- a/tests/core/StableDebtToken.t.sol +++ b/tests/core/StableDebtToken.t.sol @@ -3,7 +3,7 @@ pragma solidity ^0.8.0; import 'forge-std/Test.sol'; -import {StableDebtTokenInstance} from 'aave-v3-core/instances/StableDebtTokenInstance.sol'; +import {StableDebtTokenHarness as StableDebtTokenInstance} from '../harness/StableDebtToken.sol'; import {Errors} from 'aave-v3-core/contracts/protocol/libraries/helpers/Errors.sol'; import {IAaveIncentivesController} from 'aave-v3-core/contracts/interfaces/IAaveIncentivesController.sol'; import {TestnetERC20} from 'aave-v3-periphery/contracts/mocks/testnet-helpers/TestnetERC20.sol'; @@ -208,6 +208,11 @@ contract StableDebtTokenEventsTests is TestnetProcedures { stDebtToken.burn(address(0), 0); } + function test_default_revision() public { + StableDebtTokenInstance stDebtToken = new StableDebtTokenInstance(IPool(report.poolProxy)); + assertEq(stDebtToken._getRevision(), stDebtToken.DEBT_TOKEN_REVISION()); + } + function test_getAverageStableRate() public view { uint256 avgStableRate = stableDebtToken.getAverageStableRate(); assertEq(avgStableRate, 0); diff --git a/tests/core/VariableDebtToken.t.sol b/tests/core/VariableDebtToken.t.sol index 4c6f6dfc..9435b543 100644 --- a/tests/core/VariableDebtToken.t.sol +++ b/tests/core/VariableDebtToken.t.sol @@ -3,7 +3,7 @@ pragma solidity ^0.8.0; import 'forge-std/Test.sol'; -import {VariableDebtTokenInstance} from 'aave-v3-core/instances/VariableDebtTokenInstance.sol'; +import {VariableDebtTokenHarness as VariableDebtTokenInstance} from '../harness/VariableDebtToken.sol'; import {IAaveIncentivesController} from 'aave-v3-core/contracts/interfaces/IAaveIncentivesController.sol'; import {Errors} from 'aave-v3-core/contracts/protocol/libraries/helpers/Errors.sol'; import {TestnetERC20} from 'aave-v3-periphery/contracts/mocks/testnet-helpers/TestnetERC20.sol'; @@ -162,6 +162,11 @@ contract VariableDebtTokenEventsTests is TestnetProcedures { ); } + function test_default_revision() public { + VariableDebtTokenInstance varDebtToken = new VariableDebtTokenInstance(IPool(report.poolProxy)); + assertEq(varDebtToken._getRevision(), varDebtToken.DEBT_TOKEN_REVISION()); + } + function test_mint_variableDebt_caller_alice() public { VariableDebtTokenInstance debtToken = test_initialize_VariableDebtToken(); TestnetERC20 asset = TestnetERC20(debtToken.UNDERLYING_ASSET_ADDRESS()); diff --git a/tests/harness/StableDebtToken.sol b/tests/harness/StableDebtToken.sol new file mode 100644 index 00000000..c841b9ef --- /dev/null +++ b/tests/harness/StableDebtToken.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.0; + +import {StableDebtTokenInstance, IPool} from 'aave-v3-core/instances/StableDebtTokenInstance.sol'; + +contract StableDebtTokenHarness is StableDebtTokenInstance { + constructor(IPool pool) StableDebtTokenInstance(pool) {} + + function _getRevision() public pure returns (uint256) { + return super.getRevision(); + } +} diff --git a/tests/harness/VariableDebtToken.sol b/tests/harness/VariableDebtToken.sol new file mode 100644 index 00000000..2ca73a61 --- /dev/null +++ b/tests/harness/VariableDebtToken.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.0; + +import {VariableDebtTokenInstance, IPool} from 'aave-v3-core/instances/VariableDebtTokenInstance.sol'; + +contract VariableDebtTokenHarness is VariableDebtTokenInstance { + constructor(IPool pool) VariableDebtTokenInstance(pool) {} + + function _getRevision() public pure returns (uint256) { + return super.getRevision(); + } +} diff --git a/tests/periphery/ParaswapAdapters.t.sol b/tests/periphery/ParaswapAdapters.t.sol index 65f88171..56017b0e 100644 --- a/tests/periphery/ParaswapAdapters.t.sol +++ b/tests/periphery/ParaswapAdapters.t.sol @@ -923,6 +923,20 @@ contract ParaswapAdaptersTest is TestnetProcedures { vm.stopPrank(); } + function test_withdrawSwapAdapter_reverts_flashloan() public { + _seedMarket(); + + vm.prank(alice); + vm.expectRevert('NOT_SUPPORTED'); + contracts.poolProxy.flashLoanSimple( + address(paraSwapWithdrawSwapAdapter), + tokenList.weth, + 1 ether, + '', + 0 + ); + } + function test_rescueTokens() public { deal(tokenList.usdx, address(paraSwapRepayAdapter), 100e6); From 9600e55a29533f8429050848ee82580eb14cb2ab Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 20:47:50 +0530 Subject: [PATCH 3/6] fix: error when .env does not exists --- scripts/misc/LibraryPreCompileTwo.sol | 2 +- src/deployments/contracts/utilities/FfiUtils.sol | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/misc/LibraryPreCompileTwo.sol b/scripts/misc/LibraryPreCompileTwo.sol index 473cdecd..b14ef01c 100644 --- a/scripts/misc/LibraryPreCompileTwo.sol +++ b/scripts/misc/LibraryPreCompileTwo.sol @@ -87,7 +87,7 @@ contract LibraryPreCompileTwo is FfiUtils, Script, DeployUtils { } function verifyEnvironment() internal { - string memory checkCommand = 'grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; + string memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; string[] memory command = new string[](3); command[0] = 'bash'; diff --git a/src/deployments/contracts/utilities/FfiUtils.sol b/src/deployments/contracts/utilities/FfiUtils.sol index 2c199e2b..30ac134b 100644 --- a/src/deployments/contracts/utilities/FfiUtils.sol +++ b/src/deployments/contracts/utilities/FfiUtils.sol @@ -56,7 +56,7 @@ abstract contract FfiUtils { } function _librariesPathExists() internal returns (bool) { - string memory checkCommand = 'grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; + string memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; string[] memory command = new string[](3); command[0] = 'bash'; From ba8a9a6a16200c7d746acd7da7ba50913d349895 Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 21:52:14 +0530 Subject: [PATCH 4/6] test: setLiquidationGracePeriodReserve --- .../protocol/pool/PoolConfigurator.sol | 1 - .../PoolConfigurator.reserveRiskConfig.t.sol | 32 ++++++++++++++----- 2 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/core/contracts/protocol/pool/PoolConfigurator.sol b/src/core/contracts/protocol/pool/PoolConfigurator.sol index 228daf6b..041943e1 100644 --- a/src/core/contracts/protocol/pool/PoolConfigurator.sol +++ b/src/core/contracts/protocol/pool/PoolConfigurator.sol @@ -261,7 +261,6 @@ abstract contract PoolConfigurator is VersionedInitializable, IPoolConfigurator bool paused, uint40 gracePeriod ) public override onlyEmergencyOrPoolAdmin { - // Only setting grace period if the transition is paused -> unpaused if (!paused && gracePeriod != 0) { require(gracePeriod <= MAX_GRACE_PERIOD, Errors.INVALID_GRACE_PERIOD); diff --git a/tests/core/PoolConfigurator.reserveRiskConfig.t.sol b/tests/core/PoolConfigurator.reserveRiskConfig.t.sol index e9314411..9d64fc3e 100644 --- a/tests/core/PoolConfigurator.reserveRiskConfig.t.sol +++ b/tests/core/PoolConfigurator.reserveRiskConfig.t.sol @@ -734,20 +734,36 @@ contract PoolConfiguratorReserveRiskConfigs is TestnetProcedures { } function test_setLiquidationGracePeriodReserve(uint40 gracePeriod) public { - vm.assume(gracePeriod <= contracts.poolConfiguratorProxy.MAX_GRACE_PERIOD()); + vm.assume(gracePeriod <= contracts.poolConfiguratorProxy.MAX_GRACE_PERIOD() && gracePeriod != 0); address asset = tokenList.usdx; uint40 until = uint40(block.timestamp) + gracePeriod; - vm.prank(poolAdmin); + vm.startPrank(poolAdmin); - if (gracePeriod != 0) { - vm.expectEmit(address(contracts.poolConfiguratorProxy)); - emit LiquidationGracePeriodChanged(asset, until); - contracts.poolConfiguratorProxy.setReservePause(asset, false, gracePeriod); - assertEq(contracts.poolProxy.getLiquidationGracePeriod(asset), until); - } + // reserve unpause -> unpause, liquidationGracePeriod would be set + vm.expectEmit(address(contracts.poolConfiguratorProxy)); + emit LiquidationGracePeriodChanged(asset, until); + contracts.poolConfiguratorProxy.setReservePause(asset, false, gracePeriod); + assertEq(contracts.poolProxy.getLiquidationGracePeriod(asset), until); + + // reserve unpause -> pause, liquidationGracePeriod would not be set + contracts.poolConfiguratorProxy.setReservePause(asset, true, gracePeriod + 1); + assertEq(contracts.poolProxy.getLiquidationGracePeriod(asset), until); + assertTrue(contracts.protocolDataProvider.getPaused(asset)); + + // reserve pause -> pause, liquidationGracePeriod would not be set + contracts.poolConfiguratorProxy.setReservePause(asset, true, gracePeriod + 1); + assertEq(contracts.poolProxy.getLiquidationGracePeriod(asset), until); + + // reserve pause -> unpause, liquidationGracePeriod would be set + vm.expectEmit(address(contracts.poolConfiguratorProxy)); + emit LiquidationGracePeriodChanged(asset, until + 1); + contracts.poolConfiguratorProxy.setReservePause(asset, false, gracePeriod + 1); + assertEq(contracts.poolProxy.getLiquidationGracePeriod(asset), until + 1); + + vm.stopPrank(); } function test_setLiquidationGracePeriodPool(uint40 gracePeriod) public { From ffbdeb6f83f29d4f26b622caa41a4f6513eb994f Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 21:55:11 +0530 Subject: [PATCH 5/6] fix: lint --- scripts/misc/LibraryPreCompileTwo.sol | 3 +- .../contracts/utilities/FfiUtils.sol | 3 +- .../core/PoolConfigurator.ACLModifiers.t.sol | 30 +++++++++---------- .../PoolConfigurator.reserveRiskConfig.t.sol | 4 ++- 4 files changed, 22 insertions(+), 18 deletions(-) diff --git a/scripts/misc/LibraryPreCompileTwo.sol b/scripts/misc/LibraryPreCompileTwo.sol index b14ef01c..cab49cec 100644 --- a/scripts/misc/LibraryPreCompileTwo.sol +++ b/scripts/misc/LibraryPreCompileTwo.sol @@ -87,7 +87,8 @@ contract LibraryPreCompileTwo is FfiUtils, Script, DeployUtils { } function verifyEnvironment() internal { - string memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; + string + memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; string[] memory command = new string[](3); command[0] = 'bash'; diff --git a/src/deployments/contracts/utilities/FfiUtils.sol b/src/deployments/contracts/utilities/FfiUtils.sol index 30ac134b..518caf3c 100644 --- a/src/deployments/contracts/utilities/FfiUtils.sol +++ b/src/deployments/contracts/utilities/FfiUtils.sol @@ -56,7 +56,8 @@ abstract contract FfiUtils { } function _librariesPathExists() internal returns (bool) { - string memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; + string + memory checkCommand = '[ -e .env ] && grep -q "FOUNDRY_LIBRARIES" .env && echo true || echo false'; string[] memory command = new string[](3); command[0] = 'bash'; diff --git a/tests/core/PoolConfigurator.ACLModifiers.t.sol b/tests/core/PoolConfigurator.ACLModifiers.t.sol index 208309a0..aad612d2 100644 --- a/tests/core/PoolConfigurator.ACLModifiers.t.sol +++ b/tests/core/PoolConfigurator.ACLModifiers.t.sol @@ -16,7 +16,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ConfiguratorInputTypes.InitReserveInput[] memory input; vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - !contracts.aclManager.isAssetListingAdmin(caller) && + !contracts.aclManager.isAssetListingAdmin(caller) && caller != address(contracts.poolAddressesProvider) ); @@ -29,7 +29,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { function test_reverts_notAdmin_dropReserve(address caller) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -42,7 +42,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ConfiguratorInputTypes.UpdateATokenInput memory input; vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -55,7 +55,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ConfiguratorInputTypes.UpdateDebtTokenInput memory input; vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -68,7 +68,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ConfiguratorInputTypes.UpdateDebtTokenInput memory input; vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -80,7 +80,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { function test_reverts_notAdmin_setReserveActive(address caller) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -92,7 +92,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { function test_reverts_notAdmin_updateFlashLoanPremiumTotal(address caller) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -104,7 +104,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { function test_reverts_notAdmin_updateFlashLoanPremiumProtocol(address caller) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - caller != address(contracts.poolAddressesProvider) + caller != address(contracts.poolAddressesProvider) ); vm.expectRevert(bytes(Errors.CALLER_NOT_POOL_ADMIN)); @@ -155,8 +155,8 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { function test_reverts_notRiskOrPoolOrEmergencyAdmin_setReserveFreeze(address caller) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && - !contracts.aclManager.isRiskAdmin(caller) && - !contracts.aclManager.isEmergencyAdmin(caller) && + !contracts.aclManager.isRiskAdmin(caller) && + !contracts.aclManager.isEmergencyAdmin(caller) && caller != address(contracts.poolAddressesProvider) ); @@ -222,7 +222,10 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { ); } - function test_reverts_notRiskAdmin_setReserveInterestRateData(address caller, address asset) public { + function test_reverts_notRiskAdmin_setReserveInterestRateData( + address caller, + address asset + ) public { vm.assume( !contracts.aclManager.isPoolAdmin(caller) && !contracts.aclManager.isRiskAdmin(caller) && @@ -232,10 +235,7 @@ contract PoolConfiguratorACLModifiersTest is TestnetProcedures { vm.expectRevert(bytes(Errors.CALLER_NOT_RISK_OR_POOL_ADMIN)); vm.prank(caller); - contracts.poolConfiguratorProxy.setReserveInterestRateData( - asset, - bytes('0') - ); + contracts.poolConfiguratorProxy.setReserveInterestRateData(asset, bytes('0')); } function test_reverts_notRiskAdmin_setEModeCategory(address caller) public { diff --git a/tests/core/PoolConfigurator.reserveRiskConfig.t.sol b/tests/core/PoolConfigurator.reserveRiskConfig.t.sol index 9d64fc3e..cd6a28b7 100644 --- a/tests/core/PoolConfigurator.reserveRiskConfig.t.sol +++ b/tests/core/PoolConfigurator.reserveRiskConfig.t.sol @@ -734,7 +734,9 @@ contract PoolConfiguratorReserveRiskConfigs is TestnetProcedures { } function test_setLiquidationGracePeriodReserve(uint40 gracePeriod) public { - vm.assume(gracePeriod <= contracts.poolConfiguratorProxy.MAX_GRACE_PERIOD() && gracePeriod != 0); + vm.assume( + gracePeriod <= contracts.poolConfiguratorProxy.MAX_GRACE_PERIOD() && gracePeriod != 0 + ); address asset = tokenList.usdx; From 910e4c89439d1bec86dae7d74768da1e8986a302 Mon Sep 17 00:00:00 2001 From: Harsh Pandey Date: Wed, 10 Apr 2024 23:08:10 +0530 Subject: [PATCH 6/6] chore: certora cleanup --- .gitignore | 10 +- certora/README.md | 2 + certora/conf/AToken.conf | 28 +- certora/conf/NEW-pool-no-summarizations.conf | 77 ++-- certora/conf/NEW-pool-simple-properties.conf | 81 ++-- certora/conf/ReserveConfiguration.conf | 26 +- certora/conf/StableDebtToken.conf | 24 +- certora/conf/UserConfiguration.conf | 28 +- certora/conf/VariableDebtToken.conf | 20 +- certora/specs/AToken.spec | 419 +++++++++-------- certora/specs/NEW-CVLMath.spec | 257 +++++------ certora/specs/NEW-pool-base.spec | 240 +++++----- certora/specs/NEW-pool-no-summarizations.spec | 238 +++++----- certora/specs/NEW-pool-simple-properties.spec | 215 +++++---- certora/specs/ReserveConfiguration.spec | 201 ++++---- certora/specs/StableDebtToken.spec | 432 +++++++++--------- certora/specs/UserConfiguration.spec | 135 +++--- certora/specs/VariableDebtToken.spec | 194 ++++---- 18 files changed, 1303 insertions(+), 1324 deletions(-) diff --git a/.gitignore b/.gitignore index b3a8504d..b1cd1d7d 100644 --- a/.gitignore +++ b/.gitignore @@ -21,4 +21,12 @@ node_modules # ignore foundry deploy artifacts broadcast/ -.DS_Store \ No newline at end of file +.DS_Store + +# certora +.certora* +.certora*.json +**.last_conf* +certora-logs +certora_debug_log.txt +resource_errors.json diff --git a/certora/README.md b/certora/README.md index 97cf079a..8cbc74c6 100644 --- a/certora/README.md +++ b/certora/README.md @@ -28,6 +28,8 @@ root directory: 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 staging Certora portal](https://prover.certora.com/). diff --git a/certora/conf/AToken.conf b/certora/conf/AToken.conf index e6bf8935..299a8f4e 100644 --- a/certora/conf/AToken.conf +++ b/certora/conf/AToken.conf @@ -1,15 +1,15 @@ { - "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", - "msg": "aToken spec" - } \ No newline at end of file + "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", + "msg": "aToken spec" +} diff --git a/certora/conf/NEW-pool-no-summarizations.conf b/certora/conf/NEW-pool-no-summarizations.conf index 821d1cfc..11f62350 100644 --- a/certora/conf/NEW-pool-no-summarizations.conf +++ b/certora/conf/NEW-pool-no-summarizations.conf @@ -1,40 +1,41 @@ { - "files": [ - "certora/harness/ATokenHarness.sol", - "certora/harness/PoolHarness.sol", - "certora/harness/StableDebtTokenHarness.sol", - "certora/harness/SimpleERC20.sol", - "src/core/instances/VariableDebtTokenInstance.sol", - "src/core/contracts/misc/AaveProtocolDataProvider.sol", - "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol", - "src/core/contracts/protocol/configuration/ACLManager.sol", - "src/core/contracts/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", - "src/core/contracts/protocol/configuration/PriceOracleSentinel.sol", - "src/core/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:stableDebtTokenAddress=StableDebtTokenHarness", - "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" - ], - "parametric_contracts": ["PoolHarness"], - "msg": "pool-no-summarizations::partial rules", + "files": [ + "certora/harness/ATokenHarness.sol", + "certora/harness/PoolHarness.sol", + "certora/harness/StableDebtTokenHarness.sol", + "certora/harness/SimpleERC20.sol", + "src/core/instances/VariableDebtTokenInstance.sol", + "src/core/contracts/misc/AaveProtocolDataProvider.sol", + "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol", + "src/core/contracts/protocol/configuration/ACLManager.sol", + "src/core/contracts/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", + "src/core/contracts/protocol/configuration/PriceOracleSentinel.sol", + "src/core/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:stableDebtTokenAddress=StableDebtTokenHarness", + "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" + ], + "parametric_contracts": ["PoolHarness"], + "msg": "pool-no-summarizations::partial rules", } diff --git a/certora/conf/NEW-pool-simple-properties.conf b/certora/conf/NEW-pool-simple-properties.conf index 9d932cf1..96a78c78 100644 --- a/certora/conf/NEW-pool-simple-properties.conf +++ b/certora/conf/NEW-pool-simple-properties.conf @@ -1,42 +1,43 @@ { - "files": [ - "certora/harness/ATokenHarness.sol", - "certora/harness/PoolHarness.sol", - "certora/harness/StableDebtTokenHarness.sol", - "certora/harness/SimpleERC20.sol", - "src/core/instances/VariableDebtTokenInstance.sol", - "src/core/contracts/misc/AaveProtocolDataProvider.sol", - "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol", - "src/core/contracts/protocol/libraries/types/DataTypes.sol", - "src/core/contracts/protocol/configuration/PoolAddressesProvider.sol", - ], - "link": [ - "ATokenHarness:POOL=PoolHarness", - "ATokenHarness:_underlyingAsset=SimpleERC20", - "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", - ], - "struct_link": [ - "PoolHarness:aTokenAddress=ATokenHarness", - "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness", - "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" - ], - "parametric_contracts": ["PoolHarness"], - "msg": "pool-simple-properties::ALL", + "files": [ + "certora/harness/ATokenHarness.sol", + "certora/harness/PoolHarness.sol", + "certora/harness/StableDebtTokenHarness.sol", + "certora/harness/SimpleERC20.sol", + "src/core/instances/VariableDebtTokenInstance.sol", + "src/core/contracts/misc/AaveProtocolDataProvider.sol", + "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol", + "src/core/contracts/protocol/libraries/types/DataTypes.sol", + "src/core/contracts/protocol/configuration/PoolAddressesProvider.sol", + ], + "link": [ + "ATokenHarness:POOL=PoolHarness", + "ATokenHarness:_underlyingAsset=SimpleERC20", + "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", + ], + "struct_link": [ + "PoolHarness:aTokenAddress=ATokenHarness", + "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness", + "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" + ], + "parametric_contracts": ["PoolHarness"], + "msg": "pool-simple-properties::ALL", } diff --git a/certora/conf/ReserveConfiguration.conf b/certora/conf/ReserveConfiguration.conf index 4277ed2a..2e4e50b6 100644 --- a/certora/conf/ReserveConfiguration.conf +++ b/certora/conf/ReserveConfiguration.conf @@ -1,14 +1,14 @@ { - "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", - "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec" -} \ No newline at end of file + "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", + "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec" +} diff --git a/certora/conf/StableDebtToken.conf b/certora/conf/StableDebtToken.conf index ccb3fb6b..1480d348 100644 --- a/certora/conf/StableDebtToken.conf +++ b/certora/conf/StableDebtToken.conf @@ -1,18 +1,18 @@ //=================================================================================== // IMPORTANT: -// This file can be DELETED, since Stable coins are removed. +// This file can be DELETED, since Stable coins are removed. // In the implementation all the function either revert or return 0 // =================================================================================== { - "cache": "StableToken", - "files": [ - "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness" - ], - "loop_iter": "4", - "msg": "stableTokenCLI", - "optimistic_loop": true, - "process": "emv", - "solc": "solc8.19", - "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec" -} \ No newline at end of file + "cache": "StableToken", + "files": [ + "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness" + ], + "loop_iter": "4", + "msg": "stableTokenCLI", + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.19", + "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec" +} diff --git a/certora/conf/UserConfiguration.conf b/certora/conf/UserConfiguration.conf index 897161ae..65b23d05 100644 --- a/certora/conf/UserConfiguration.conf +++ b/certora/conf/UserConfiguration.conf @@ -1,15 +1,15 @@ { - "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", - "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec" -} \ No newline at end of file + "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", + "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec" +} diff --git a/certora/conf/VariableDebtToken.conf b/certora/conf/VariableDebtToken.conf index 10c0be67..52b9f172 100644 --- a/certora/conf/VariableDebtToken.conf +++ b/certora/conf/VariableDebtToken.conf @@ -1,11 +1,11 @@ { - "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", - "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec" -} \ No newline at end of file + "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", + "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec" +} diff --git a/certora/specs/AToken.spec b/certora/specs/AToken.spec index 940b70d1..bd15c698 100644 --- a/certora/specs/AToken.spec +++ b/certora/specs/AToken.spec @@ -1,35 +1,29 @@ /** - -- values of gRNI passing: ray, 2 * ray - + - 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; +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) ) ; + return (assert_uint256( (x+y) % 2^256) ); } function MINUS256(uint256 x, uint256 y) returns uint256 { - return (assert_uint256( (x-y) % 2^256) ); + return (assert_uint256( (x-y) % 2^256) ); } - definition ray() returns uint = 1000000000000000000000000000; definition bound() returns mathint = ((gRNI() / ray()) + 1 ) / 2; @@ -37,95 +31,94 @@ 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); + 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; + init_state axiom sumAllBalance() == 0; } // summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) ghost gRNI() returns uint256 { - axiom to_mathint(gRNI()) == 7 * ray(); + 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; + 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(); - } + 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; + 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; + 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 + 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 } + 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); + 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. + 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); + 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); } /* @@ -141,41 +134,41 @@ rule additiveMint(address a, address b, address c, uint256 x, uint256 y) { 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 + 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"; - } + 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"; + } } @@ -184,131 +177,133 @@ rule integrityTransfer(address from, address to, uint256 amount) { 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"; + 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'. + 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 + 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 + 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"; + 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. + 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; + 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. + 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; + 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; -} + 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/specs/NEW-CVLMath.spec b/certora/specs/NEW-CVLMath.spec index 4dde507e..a18d40f1 100644 --- a/certora/specs/NEW-CVLMath.spec +++ b/certora/specs/NEW-CVLMath.spec @@ -6,196 +6,193 @@ // 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 ); +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 ); +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 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 _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 _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 abs(mathint x) returns mathint = + x >= 0 ? x : 0 - x; -definition min(mathint x, mathint y) returns mathint = - x > y ? y : 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; +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); +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)); - + ((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; + 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; + 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); + 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()); + return mulDivDownAbstractPlus(x, y, ONE18()); } function mulUpWad(uint256 x, uint256 y) returns uint256 { - return mulDivUpAbstractPlus(x, y, ONE18()); + return mulDivUpAbstractPlus(x, y, ONE18()); } function divDownWad(uint256 x, uint256 y) returns uint256 { - return mulDivDownAbstractPlus(x, ONE18(), y); + return mulDivDownAbstractPlus(x, ONE18(), y); } function divUpWad(uint256 x, uint256 y) returns uint256 { - return mulDivUpAbstractPlus(x, ONE18(), y); + 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; + 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; + 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; + 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); + /// 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); + 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); + mathint SQRT; + require SQRT*SQRT <= to_mathint(x) && (SQRT + 1)*(SQRT + 1) > to_mathint(x); + return require_uint256(SQRT); } diff --git a/certora/specs/NEW-pool-base.spec b/certora/specs/NEW-pool-base.spec index f12b0c49..ac7cfdf0 100644 --- a/certora/specs/NEW-pool-base.spec +++ b/certora/specs/NEW-pool-base.spec @@ -1,10 +1,10 @@ -import "NEW-CVLMath.spec"; - /* 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 */ @@ -14,163 +14,159 @@ using AaveProtocolDataProvider as _dataProvider; using SimpleERC20 as _underlyingAsset; /* - -Methods Summerizations and Enviroment-Free (e.g relative to e.msg variables) Declarations - + 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); - - // StableDebt - function _.mint(address user, address onBehalfOf, uint256 amount, uint256 rate) external => DISPATCHER(true); - function _.burn(address user, uint256 amount) external => DISPATCHER(true); - function _.getSupplyData() 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); - + // 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); + + // StableDebt + function _.mint(address user, address onBehalfOf, uint256 amount, uint256 rate) external => DISPATCHER(true); + function _.burn(address user, uint256 amount) external => DISPATCHER(true); + function _.getSupplyData() 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)); -// definition ACTIVE_MASK() returns uint256 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFFFFFFFFFF; -// definition FROZEN_MASK() returns uint256 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFDFFFFFFFFFFFFFF; - 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]; + 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; + 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); + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveConfigurationMap configuration = data.configuration; + bool isFrozen = getFrozen(e, configuration); - return isFrozen; + 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); + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveConfigurationMap configuration = data.configuration; + bool isBorrowEnabled = getBorrowingEnabled(e, configuration); - return isBorrowEnabled; + return isBorrowEnabled; } function getCurrentLiquidityRate(env e, address asset) returns mathint { - DataTypes.ReserveData data = getReserveDataExtended(e, asset); - return data.currentLiquidityRate; + 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; + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + return data.liquidityIndex; } function aTokenBalanceOf(env e, address user) returns uint256 { - return _aToken.ATokenBalanceOf(e, user); + 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()); + 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); + 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/specs/NEW-pool-no-summarizations.spec b/certora/specs/NEW-pool-no-summarizations.spec index 7ae0c45f..d4dcbe68 100644 --- a/certora/specs/NEW-pool-no-summarizations.spec +++ b/certora/specs/NEW-pool-no-summarizations.spec @@ -1,66 +1,66 @@ 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 _.getAverageStableRate() 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; + 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 _.getAverageStableRate() 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; + counterUpdateIndexes = counterUpdateIndexes + 1; + return true; } function calculateInterestRatesMock(DataTypes.CalculateInterestRatesParams params) returns (uint256, uint256, uint256) { - uint256 liquidityRate = 1; - uint256 stableBorrowRate = 1; - uint256 variableBorrowRate = 1; - return (liquidityRate, stableBorrowRate, variableBorrowRate); + uint256 liquidityRate = 1; + uint256 stableBorrowRate = 1; + uint256 variableBorrowRate = 1; + return (liquidityRate, stableBorrowRate, 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. + @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 - ================================================================================================*/ + 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; + calldataarg args; + + mathint updateIndexesCallCountBefore = counterUpdateIndexes; + f(e, args); + + mathint updateIndexesCallCountAfter = counterUpdateIndexes; + + satisfy updateIndexesCallCountBefore != updateIndexesCallCountAfter; } // @title cumulateToLiquidityIndex does not decrease the liquidity index. @@ -68,91 +68,91 @@ rule _updateIndexesWrapperReachable(env e, method f) { // 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; + 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; + 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. - =========================================================================================== */ + 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(); + 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. - =========================================================================================*/ + 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; + 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/specs/NEW-pool-simple-properties.spec b/certora/specs/NEW-pool-simple-properties.spec index 06c7a4b5..b9e024a3 100644 --- a/certora/specs/NEW-pool-simple-properties.spec +++ b/certora/specs/NEW-pool-simple-properties.spec @@ -1,68 +1,67 @@ import "NEW-pool-base.spec"; methods { - function _._getUserDebtInBaseCurrency(address user, DataTypes.ReserveData storage reserve, uint256 assetPrice, uint256 assetUnit) internal => NONDET; + 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; + 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; +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()) { - return y; + if (x > RAY()) { + require rayMulSummariztionValues[y][x] >= y; } - if (y == RAY()) { - return x; + return rayMulSummariztionValues[y][x]; + } + else { + if (x > RAY()) { + require rayMulSummariztionValues[x][y] >= y; } - - 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]; + 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]; + 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; + calldataarg args; + f(e, args); + satisfy true; } // @title It is impossible to deposit an inactive reserve @@ -70,15 +69,15 @@ rule method_reachability(env e, method f) { // 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); + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + bool reserveIsActive = isActiveReserve(e, asset); - deposit(e, asset, amount, onBehalfOf, referralCode); + deposit(e, asset, amount, onBehalfOf, referralCode); - assert reserveIsActive; + assert reserveIsActive; } // @title It is impossible to deposit a frozen reserve @@ -86,43 +85,43 @@ rule cannotDepositInInactiveReserve(env e) { // 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); + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + bool reserveIsFrozen = isFrozenReserve(e, asset); - deposit(e, asset, amount, onBehalfOf, referralCode); + deposit(e, asset, amount, onBehalfOf, referralCode); - assert !reserveIsFrozen; + 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; + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; - deposit(e, asset, amount, onBehalfOf, referralCode); + deposit(e, asset, amount, onBehalfOf, referralCode); - assert amount != 0; + 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; + address asset; + uint256 amount; + address to; + uint16 referralCode; - withdraw(e, asset, amount, to); + withdraw(e, asset, amount, to); - assert amount != 0; + assert amount != 0; } // @title It is impossible to withdraw an inactive reserve @@ -130,30 +129,30 @@ rule cannotWithdrawZeroAmount(env e) { // 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); + address asset; + uint256 amount; + address to; + uint16 referralCode; + bool reserveIsActive = isActiveReserve(e, asset); - withdraw(e, asset, amount, to); + withdraw(e, asset, amount, to); - assert reserveIsActive; + 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; + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - assert amount != 0; + assert amount != 0; } // @title It is impossible to borrow on inactive reserve. @@ -161,16 +160,16 @@ rule cannotBorrowZeroAmount(env e) { // 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); + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsActive = isActiveReserve(e, asset); - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - assert reserveIsActive; + assert reserveIsActive; } // It is impossible to borrow on a reserve, that is disabled for borrowing. @@ -178,16 +177,16 @@ rule cannotBorrowOnInactiveReserve(env e) { // 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); + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsEnabledForBorrow = isEnabledForBorrow(e, asset); - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - assert reserveIsEnabledForBorrow; + assert reserveIsEnabledForBorrow; } // @title It is impossible to borrow on frozen reserve. @@ -195,14 +194,14 @@ rule cannotBorrowOnReserveDisabledForBorrowing(env e) { // 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); + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsFrozen = isFrozenReserve(e, asset); - borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); - assert !reserveIsFrozen; + assert !reserveIsFrozen; } diff --git a/certora/specs/ReserveConfiguration.spec b/certora/specs/ReserveConfiguration.spec index 39049ad3..cb13162c 100644 --- a/certora/specs/ReserveConfiguration.spec +++ b/certora/specs/ReserveConfiguration.spec @@ -1,186 +1,185 @@ 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 setStableRateBorrowingEnabled(bool) external envfree; - function getStableRateBorrowingEnabled() 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; + 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 setStableRateBorrowingEnabled(bool) external envfree; + function getStableRateBorrowingEnabled() 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; + 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; + 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; + 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; + 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; + 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; + 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; + 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; + 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; + 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; + setBorrowingEnabled(enabled); + assert getBorrowingEnabled() == enabled; } // checks the integrity of set StableRateBorrowingEnabled function and correct retrieval of the corresponding getter. rule setStableRateBorrowingEnabledIntegrity(bool enabled) { - setStableRateBorrowingEnabled(enabled); - assert getStableRateBorrowingEnabled() == enabled; + setStableRateBorrowingEnabled(enabled); + assert getStableRateBorrowingEnabled() == enabled; } // checks the integrity of set ReserveFactor function and correct retrieval of the corresponding getter. rule setReserveFactorIntegrity(uint256 reserveFactor) { - setReserveFactor(reserveFactor); - assert getReserveFactor() == 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; + 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; + 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; + 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; + 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; + 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; + 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); + require 0 <= funcId && funcId <= 10; + require 0 <= otherFuncId && otherFuncId <= 10; + uint256 valueBefore = executeIntGetterById(funcId); + uint256 otherValueBefore = executeIntGetterById(otherFuncId); - executeIntSetterById(funcId, val); + executeIntSetterById(funcId, val); - uint256 valueAfter = executeIntGetterById(funcId); - uint256 otherValueAfter = executeIntGetterById(otherFuncId); + uint256 valueAfter = executeIntGetterById(funcId); + uint256 otherValueAfter = executeIntGetterById(otherFuncId); - assert valueAfter == val; - assert (otherFuncId != funcId => otherValueAfter == otherValueBefore); + 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); + 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/specs/StableDebtToken.spec b/certora/specs/StableDebtToken.spec index e090028f..00937585 100644 --- a/certora/specs/StableDebtToken.spec +++ b/certora/specs/StableDebtToken.spec @@ -1,331 +1,327 @@ - - /*=================================================================================== IMPORTANT: - This file can be DELETED, since Stable coins are removed. + This file can be DELETED, since Stable coins are removed. In the implementation all the function either revert or return 0 ===================================================================================*/ - methods { - function _.calculateCompoundedInterest(uint256 r, uint40 t0, uint256 t1) internal => - calculateCompoundedInterestSummary(r, t0, t1) expect uint256 ALL; - function additionalData(address) external returns uint128 envfree; - function getAverageStableRate() external returns uint256 envfree; - function _.handleAction(address, uint256, uint256) external => NONDET; - - function _.rayMul(uint256 x, uint256 y) internal => rayMulSummariztion(x, y) expect uint256 ALL; - function _.rayDiv(uint256 x, uint256 y) internal => rayDivSummariztion(x, y) expect uint256 ALL; + function _.calculateCompoundedInterest(uint256 r, uint40 t0, uint256 t1) internal => + calculateCompoundedInterestSummary(r, t0, t1) expect uint256 ALL; + function additionalData(address) external returns uint128 envfree; + function getAverageStableRate() external returns uint256 envfree; + function _.handleAction(address, uint256, uint256) external => NONDET; + + function _.rayMul(uint256 x, uint256 y) internal => rayMulSummariztion(x, y) expect uint256 ALL; + function _.rayDiv(uint256 x, uint256 y) internal => rayDivSummariztion(x, y) expect uint256 ALL; } function PLUS256(uint256 x, uint256 y) returns uint256 { - return (assert_uint256( (x+y) % 2^256) ); + return (assert_uint256( (x+y) % 2^256) ); } definition RAY() returns uint = 1000000000000000000000000000; -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; +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 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]; + 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]; } ghost mapping(uint256 => mapping(uint256 => uint256)) rayMulSummariztionValues; function rayMulSummariztion(uint256 x, uint256 y) returns uint256 { - if ((x == 0) || (y == 0)) { - return 0; - } - if (x == RAY()) { - return y; + 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 (y == RAY()) { - return x; + if (x > RAY()) { + require rayMulSummariztionValues[y][x] >= y; } - - if (y > x) { - if (y > RAY()) { - require rayMulSummariztionValues[y][x] >= x; - } - if (x > RAY()) { - require rayMulSummariztionValues[y][x] >= y; - } - return rayMulSummariztionValues[y][x]; + return rayMulSummariztionValues[y][x]; + } + else { + if (x > RAY()) { + require rayMulSummariztionValues[x][y] >= y; } - else { - if (x > RAY()) { - require rayMulSummariztionValues[x][y] >= y; - } - if (y > RAY()) { - require rayMulSummariztionValues[x][y] >= x; - } - return rayMulSummariztionValues[x][y]; + if (y > RAY()) { + require rayMulSummariztionValues[x][y] >= x; } + return rayMulSummariztionValues[x][y]; + } } ghost mapping(uint256 => mapping(uint256 => uint256)) rayDivSummariztionValues; 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; - return rayDivSummariztionValues[x][y]; + if (x == 0) { + return 0; + } + if (y == RAY()) { + return x; + } + if (y == x) { + return RAY(); + } + require y > RAY() => rayDivSummariztionValues[x][y] <= x; + return rayDivSummariztionValues[x][y]; } ghost symbolicCompundInterest(uint256, uint40) returns uint256 { - axiom forall uint256 x. forall uint40 t. symbolicCompundInterest(x, t) >= 1; + axiom forall uint256 x. forall uint40 t. symbolicCompundInterest(x, t) >= 1; } ghost sumAllBalance() returns mathint { - init_state axiom sumAllBalance() == 0; + 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; + havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; } hook Sload uint128 balance _userState[KEY address a].balance { - require sumAllBalance() >= to_mathint(balance); + require sumAllBalance() >= to_mathint(balance); } - invariant principalLessThanBalance(env e, address user) - principalBalanceOf(e, user) <= balanceOf(e, user) - filtered { f -> !disAllowedFunctions(f) } + principalBalanceOf(e, user) <= balanceOf(e, user) + filtered { f -> !disAllowedFunctions(f) } /** -Burning user u amount of x tokens, decreases his balanceOf the user by x. -(balance is decreased by x and not scaled x because of the summarization to one ray) + Burning user u amount of x tokens, decreases his balanceOf the user by x. + (balance is decreased by x and not scaled x because of the summarization to one ray) */ rule integrityBurn(address a, uint256 x) { - env e; - require getIncentivesController(e) == 0; - uint256 index; - uint256 balancebefore = balanceOf(e, a); - burn(e,a,x); - - uint256 balanceAfter = balanceOf(e, a); - assert to_mathint(balanceAfter) == balancebefore - x; + env e; + require getIncentivesController(e) == 0; + uint256 index; + uint256 balancebefore = balanceOf(e, a); + burn(e,a,x); + + uint256 balanceAfter = balanceOf(e, a); + assert to_mathint(balanceAfter) == balancebefore - x; } /** -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) + 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; - require getIncentivesController(e) == 0; - uint256 index; - uint256 balancebefore = balanceOf(e,a); - mint(e, delegatedUser, a, x, index); - - uint256 balanceAfter = balanceOf(e,a); - assert to_mathint(balanceAfter) == balancebefore+x; + env e; + address delegatedUser; + require getIncentivesController(e) == 0; + uint256 index; + uint256 balancebefore = balanceOf(e,a); + mint(e, delegatedUser, a, x, index); + + uint256 balanceAfter = balanceOf(e,a); + assert to_mathint(balanceAfter) == balancebefore+x; } // lastUpdated timestamp must be in the past. -rule integrityTimeStamp(address user, method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } +rule integrityTimeStamp(address user, method f) + filtered { f -> !f.isView && !disAllowedFunctions(f) } { - env e; - require assert_uint256(getUserLastUpdated(e, user)) <= e.block.timestamp; - calldataarg arg; - f(e,arg); - assert assert_uint256(getUserLastUpdated(e, user)) <= e.block.timestamp; + env e; + require assert_uint256(getUserLastUpdated(e, user)) <= e.block.timestamp; + calldataarg arg; + f(e,arg); + assert assert_uint256(getUserLastUpdated(e, user)) <= e.block.timestamp; } 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; + 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; } /* -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 + 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 a, uint256 x, uint256 y) { - env e; - storage initialStorage = lastStorage; - burn(e, a, x); - burn(e, a, y); - uint256 balanceScenario1 = balanceOf(e, a); - uint256 t = PLUS256(x,y); - burn(e, a, t) at initialStorage; - - uint256 balanceScenario2 = balanceOf(e, a); - assert balanceScenario1 == balanceScenario2, "burn is not additive"; + env e; + storage initialStorage = lastStorage; + burn(e, a, x); + burn(e, a, y); + uint256 balanceScenario1 = balanceOf(e, a); + uint256 t = PLUS256(x,y); + burn(e, a, t) at initialStorage; + + uint256 balanceScenario2 = balanceOf(e, a); + assert balanceScenario1 == balanceScenario2, "burn is not additive"; } // minting and then buring Variable Debt Token should have no effect on the users balance rule inverseMintBurn(address a, address delegatedUser, uint256 amount, uint256 rate) { - env e; - uint256 balancebefore = balanceOf(e, a); - mint(e, delegatedUser, a, amount, rate); - burn(e, a, amount); - uint256 balanceAfter = balanceOf(e, a); - assert balancebefore == balanceAfter, "burn is not the inverse of mint"; + env e; + uint256 balancebefore = balanceOf(e, a); + mint(e, delegatedUser, a, amount, rate); + burn(e, a, amount); + uint256 balanceAfter = balanceOf(e, a); + assert balancebefore == balanceAfter, "burn is not the inverse of mint"; } // 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) } + 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).selector || - f.selector == sig:mint(address, address, uint256, uint256).selector)); + 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).selector || + f.selector == sig:mint(address, address, uint256, uint256).selector)); } // only delegationWithSig operation can change the nonce. -rule nonceChangePermits(method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } +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; + 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; } /* -Mint is additive, can performed either all at once or gradually -mint(u,x,index); mint(u,y,index) ~ mint(u,x+y,index) at the same initial state + Mint is additive, can performed either all at once or gradually + mint(u,x,index); mint(u,y,index) ~ mint(u,x+y,index) at the same initial state */ rule additiveMint(address a, uint256 x, uint256 y) { - env e; - address delegatedUser; - require getIncentivesController(e) == 0; - require getUserStableRate(e, a) == 0; - uint256 index; - storage initialStorage = lastStorage; - mint(e, delegatedUser, a, x, index); - mint(e, delegatedUser, a, y, index); - uint256 balanceScenario1 = balanceOf(e, a); - - uint256 t = PLUS256(x,y); - mint(e, delegatedUser, a, t ,index) at initialStorage; - - uint256 balanceScenario2 = balanceOf(e, a); - assert balanceScenario1 == balanceScenario2, "mint is not additive"; + env e; + address delegatedUser; + require getIncentivesController(e) == 0; + require getUserStableRate(e, a) == 0; + uint256 index; + storage initialStorage = lastStorage; + mint(e, delegatedUser, a, x, index); + mint(e, delegatedUser, a, y, index); + uint256 balanceScenario1 = balanceOf(e, a); + + uint256 t = PLUS256(x,y); + mint(e, delegatedUser, a, t ,index) at initialStorage; + + uint256 balanceScenario2 = balanceOf(e, a); + assert balanceScenario1 == balanceScenario2, "mint is not additive"; } /* -Each operation of Stable Debt Token can change at most one user's balance. + Each operation of Stable Debt Token can change at most one user's balance. */ -rule balanceOfChange(address a, address b, method f) - filtered { f -> !f.isView && !disAllowedFunctions(f) } +rule balanceOfChange(address a, address b, method f) + filtered { f -> !f.isView && !disAllowedFunctions(f) } { - env e; - require a != b; - uint256 balanceABefore = balanceOf(e, a); - uint256 balanceBBefore = balanceOf(e, b); - - calldataarg arg; - f(e, arg); - - uint256 balanceAAfter = balanceOf(e, a); - uint256 balanceBAfter = balanceOf(e, b); - - assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter); + env e; + require a != b; + uint256 balanceABefore = balanceOf(e, a); + uint256 balanceBBefore = balanceOf(e, b); + + calldataarg arg; + f(e, arg); + + uint256 balanceAAfter = balanceOf(e, a); + uint256 balanceBAfter = balanceOf(e, b); + + assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter); } // Buring zero amount of tokens should have no effect. rule burnZeroDoesntChangeBalance(address u) { - env e; - uint256 balanceBefore = balanceOf(e, u); - burn(e, u, 0); - uint256 balanceAfter = balanceOf(e, u); - assert balanceBefore == balanceAfter; + env e; + uint256 balanceBefore = balanceOf(e, u); + burn(e, u, 0); + uint256 balanceAfter = balanceOf(e, u); + assert balanceBefore == balanceAfter; } /* -Burning one user atokens should have no effect on other users that are not involved in the action. + Burning one user atokens should have no effect on other users that are not involved in the action. */ rule burnNoChangeToOther(address user, uint256 amount, address other) { - - require other != user; - env e; - uint256 otherDataBefore = additionalData(other); - uint256 otherBalanceBefore = balanceOf(e, other); - - burn(e, user, amount); - - uint256 otherDataAfter = additionalData(other); - uint256 otherBalanceAfter = balanceOf(e, other); - - assert otherDataBefore == otherDataAfter && - otherBalanceBefore == otherBalanceAfter; + require other != user; + env e; + uint256 otherDataBefore = additionalData(other); + uint256 otherBalanceBefore = balanceOf(e, other); + + burn(e, user, amount); + + uint256 otherDataAfter = additionalData(other); + uint256 otherBalanceAfter = balanceOf(e, 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. + 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 rate, address other) { - require other != user && other != onBehalfOf; + require other != user && other != onBehalfOf; - env e; - uint128 userDataBefore = additionalData(user); - uint128 otherDataBefore = additionalData(other); - uint256 userBalanceBefore = balanceOf(e, user); - uint256 otherBalanceBefore = balanceOf(e, other); + env e; + uint128 userDataBefore = additionalData(user); + uint128 otherDataBefore = additionalData(other); + uint256 userBalanceBefore = balanceOf(e, user); + uint256 otherBalanceBefore = balanceOf(e, other); - mint(e, user, onBehalfOf, amount, rate); + mint(e, user, onBehalfOf, amount, rate); - uint128 userDataAfter = additionalData(user); - uint128 otherDataAfter = additionalData(other); - uint256 userBalanceAfter = balanceOf(e, user); - uint256 otherBalanceAfter = balanceOf(e, other); + uint128 userDataAfter = additionalData(user); + uint128 otherDataAfter = additionalData(other); + uint256 userBalanceAfter = balanceOf(e, user); + uint256 otherBalanceAfter = balanceOf(e, other); - if (user != onBehalfOf) { - assert userBalanceBefore == userBalanceAfter && userDataBefore == userDataAfter; - } - - assert otherBalanceBefore == otherBalanceAfter && otherDataBefore == otherDataAfter; + if (user != onBehalfOf) { + assert userBalanceBefore == userBalanceAfter && userDataBefore == userDataAfter; + } + + assert otherBalanceBefore == otherBalanceAfter && otherDataBefore == otherDataAfter; } /* -Ensuring that the defined disallowed functions revert in any case. + 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; + env e; calldataarg args; + f@withrevert(e, args); + assert lastReverted; } diff --git a/certora/specs/UserConfiguration.spec b/certora/specs/UserConfiguration.spec index efea2f48..77404c28 100644 --- a/certora/specs/UserConfiguration.spec +++ b/certora/specs/UserConfiguration.spec @@ -1,108 +1,103 @@ - - 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; + 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"; +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)); + // 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; + 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)); + // 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 isUsingAsCollateralOrBorrowing(uint256 reserveIndex ) + (isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=> + isUsingAsCollateralOrBorrowing(reserveIndex); invariant integrityOfisUsingAsCollateralOne(uint256 reserveIndex, uint256 reserveIndexOther) - isUsingAsCollateral(reserveIndex) && isUsingAsCollateralOne() => - !isUsingAsCollateral(reserveIndexOther) || reserveIndexOther == reserveIndex; + isUsingAsCollateral(reserveIndex) && isUsingAsCollateralOne() => + !isUsingAsCollateral(reserveIndexOther) || reserveIndexOther == reserveIndex; invariant integrityOfisUsingAsCollateralAny(uint256 reserveIndex) - isUsingAsCollateral(reserveIndex) => isUsingAsCollateralAny(); + isUsingAsCollateral(reserveIndex) => isUsingAsCollateralAny(); invariant integrityOfisBorrowingOne(uint256 reserveIndex, uint256 reserveIndexOther) - isBorrowing(reserveIndex) && isBorrowingOne() => !isBorrowing(reserveIndexOther) || reserveIndexOther == reserveIndex; + isBorrowing(reserveIndex) && isBorrowingOne() => !isBorrowing(reserveIndexOther) || reserveIndexOther == reserveIndex; invariant integrityOfisBorrowingAny(uint256 reserveIndex) - isBorrowing(reserveIndex) => isBorrowingAny(); - -invariant integrityOfEmpty(uint256 reserveIndex) - isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(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; + 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; + bool existExactlyOneBorrow = isBorrowingOne(); + bool answer; address asset; + answer, asset = getSiloedBorrowingState(); + assert answer => existExactlyOneBorrow; } - diff --git a/certora/specs/VariableDebtToken.spec b/certora/specs/VariableDebtToken.spec index d8832cb2..4f1c97b0 100644 --- a/certora/specs/VariableDebtToken.spec +++ b/certora/specs/VariableDebtToken.spec @@ -1,108 +1,102 @@ - - methods { - // summarization for elimination the raymul operation in balance of and totalSupply. - function _.getReserveNormalizedVariableDebt(address asset) external => gRNVB() expect uint256 ALL; - // function setAdditionalData(address user, uint128 data) external envfree; - function _.handleAction(address, uint256, uint256) external => NONDET; - function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; - function balanceOf(address) external returns (uint256) envfree; + // 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) ); + 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(); + axiom to_mathint(gRNVB()) == 7 * ray(); } /* -Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. + 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; + 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; + 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; + 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(); - } + 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) } +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)); + 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. + 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) } +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); + 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) } +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; + 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 @@ -116,77 +110,75 @@ rule inverseMintBurn(address a, address delegatedUser, uint256 amount, uint256 i } 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; + 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) + 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); + 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 + 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 + 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 != user2 && balanceOf(user1) == balanceOf(user2)); require user1 != currentContract && user2 != currentContract; - burn(e, user1, x, index); + 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"; - // assert balanceScenario1 == balanceScenario2, "burn is not additive"; + 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 + 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)); + require (user1 != user2 && balanceOf(user1) == balanceOf(user2)); - mint(e, user3, user1, x, index); + 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"; - // assert balanceScenario1 == balanceScenario2, "burn is not additive"; + 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) + 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; @@ -196,15 +188,14 @@ rule integrityMint(address a, uint256 x) { 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); - // assert balanceAfter == balancebefore+x; + assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1); } // Buring zero amount of tokens should have no effect. @@ -217,24 +208,23 @@ rule burnZeroDoesntChangeBalance(address u, uint256 index) { } /* -Burning one user atokens should have no effect on other users that are not involved in the action. + 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. + 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; @@ -245,23 +235,23 @@ rule mintNoChangeToOther(address user, address onBehalfOf, uint256 amount, uint2 mint(e, user, onBehalfOf, amount, index); - uint256 userBalanceAfter = balanceOf(user); + uint256 userBalanceAfter = balanceOf(user); uint256 otherBalanceAfter = balanceOf(other); if (user != onBehalfOf) { - assert userBalanceBefore == userBalanceAfter ; + assert userBalanceBefore == userBalanceAfter ; } assert otherBalanceBefore == otherBalanceAfter ; } /* -Ensuring that the defined disallowed functions revert in any case. + Ensuring that the defined disallowed functions revert in any case. */ rule disallowedFunctionalities(method f) - filtered { f -> disAllowedFunctions(f) } + filtered { f -> disAllowedFunctions(f) } { - env e; calldataarg args; - f@withrevert(e, args); - assert lastReverted; + env e; calldataarg args; + f@withrevert(e, args); + assert lastReverted; }