Skip to content

Commit 596f8ec

Browse files
nisnislevinisnislevi
committed
for PR
1 parent 385287d commit 596f8ec

36 files changed

+61
-2582
lines changed

‎.github/workflows/certora-basic.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
name: certora
1+
name: certora-basic
22

33
concurrency:
44
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
@@ -34,7 +34,7 @@ jobs:
3434
with: { distribution: "zulu", java-version: "11", java-package: jre }
3535

3636
- name: Install certora cli
37-
run: pip install certora-cli==7.17.2
37+
run: pip install certora-cli==7.20.3
3838

3939
- name: Install solc
4040
run: |

‎.github/workflows/certora-stata.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ jobs:
3131
with: { distribution: "zulu", java-version: "11", java-package: jre }
3232

3333
- name: Install certora cli
34-
run: pip install certora-cli==7.17.2
34+
run: pip install certora-cli==7.20.3
3535
- name: Install solc
3636
run: |
3737
wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux

‎certora/basic/conf/NEW-pool-no-summarizations.conf‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@
33
"certora/basic/harness/ATokenHarness.sol",
44
"certora/basic/harness/PoolHarness.sol",
55
"certora/basic/harness/SimpleERC20.sol",
6-
"src/contracts/instances/VariableDebtTokenInstance.sol",
7-
"src/contracts/helpers/AaveProtocolDataProvider.sol",
8-
"src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9-
"src/contracts/protocol/configuration/ACLManager.sol",
10-
"src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
11-
"src/contracts/misc/PriceOracleSentinel.sol",
12-
"src/contracts/protocol/configuration/PoolAddressesProvider.sol",
6+
"certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol",
7+
"certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol",
8+
"certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9+
"certora/basic/munged/contracts/protocol/configuration/ACLManager.sol",
10+
"certora/basic/munged/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
11+
"certora/basic/munged/contracts/misc/PriceOracleSentinel.sol",
12+
"certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol",
1313
],
1414
"link": [
1515
"ATokenHarness:POOL=PoolHarness",

‎certora/basic/conf/NEW-pool-simple-properties.conf‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@
33
"certora/basic/harness/ATokenHarness.sol",
44
"certora/basic/harness/PoolHarness.sol",
55
"certora/basic/harness/SimpleERC20.sol",
6-
"src/contracts/instances/VariableDebtTokenInstance.sol",
7-
"src/contracts/helpers/AaveProtocolDataProvider.sol",
8-
"src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9-
"src/contracts/protocol/libraries/types/DataTypes.sol",
10-
"src/contracts/protocol/configuration/PoolAddressesProvider.sol",
6+
"certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol",
7+
"certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol",
8+
"certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9+
"certora/basic/munged/contracts/protocol/libraries/types/DataTypes.sol",
10+
"certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol",
1111
],
1212
"link": [
1313
"ATokenHarness:POOL=PoolHarness",

‎certora/basic/scripts/run-all.sh‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,9 @@ certoraRun $CMN certora/basic/conf/stableRemoved.conf \
3333
--msg "6: Stable fields are un-touched"
3434

3535
echo
36-
echo "******** Running: 6 EModeConfiguration ***************"
36+
echo "******** Running: 7 EModeConfiguration ***************"
3737
certoraRun $CMN certora/basic/conf/EModeConfiguration.conf \
38-
--msg "6: EModeConfiguration"
38+
--msg "7: EModeConfiguration"
3939

4040

4141
echo

‎certora/basic/specs/EModeConfiguration.spec‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,5 +56,3 @@ rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) {
5656
assert (reserveIndex != reserveIndex_other => before == after);
5757
}
5858

59-
60-

‎certora/basic/specs/NEW-pool-base.spec‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -99,36 +99,36 @@ function calculateCompoundedInterestSummary(uint256 rate, uint40 t0, uint256 t1)
9999
}
100100

101101
function isActiveReserve(env e, address asset) returns bool {
102-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
102+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
103103
DataTypes.ReserveConfigurationMap configuration = data.configuration;
104104
bool isActive = getActive(e, configuration);
105105

106106
return isActive;
107107
}
108108

109109
function isFrozenReserve(env e, address asset) returns bool {
110-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
110+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
111111
DataTypes.ReserveConfigurationMap configuration = data.configuration;
112112
bool isFrozen = getFrozen(e, configuration);
113113

114114
return isFrozen;
115115
}
116116

117117
function isEnabledForBorrow(env e, address asset) returns bool {
118-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
118+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
119119
DataTypes.ReserveConfigurationMap configuration = data.configuration;
120120
bool isBorrowEnabled = getBorrowingEnabled(e, configuration);
121121

122122
return isBorrowEnabled;
123123
}
124124

125125
function getCurrentLiquidityRate(env e, address asset) returns mathint {
126-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
126+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
127127
return data.currentLiquidityRate;
128128
}
129129

130130
function getLiquidityIndex(env e, address asset) returns mathint {
131-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
131+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
132132
return data.liquidityIndex;
133133
}
134134

‎certora/basic/specs/NEW-pool-no-summarizations.spec‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ rule liquidityIndexNonDecresingFor_cumulateToLiquidityIndex() {
8181

8282

8383
function get_AToken_of_asset(env e, address asset) returns address {
84-
DataTypes.ReserveData data = getReserveDataExtended(e, asset);
84+
DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
8585
return data.aTokenAddress;
8686
}
8787

‎certora/basic/specs/aux/aToken.spec‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,7 @@ function indexForToken(address token, env e) returns uint256 {
131131

132132
// todo: adjust for stable debt token
133133
function aTokenBalanceOfCVL(address token, address user, env e) returns uint256 {
134+
require token != 0;
134135
uint storedBalance = balanceOfCVL(token, user);
135136
if (aTokenToUnderlying[token] == 0) {
136137
// not a properly initialized aToken, return the regular ERC20 balance

‎certora/basic/specs/stableRemoved.spec‎

Lines changed: 37 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import "aux/aToken.spec";
44
//import "AddressProvider.spec";
55

66
methods {
7-
function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree;
7+
// function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree;
88
function getReserveData(address) external returns (DataTypes.ReserveDataLegacy memory) envfree;
99

1010
function ValidationLogic.validateLiquidationCall(
@@ -21,22 +21,43 @@ methods {
2121
DataTypes.CalculateUserAccountDataParams memory params
2222
) internal returns (uint256, uint256, uint256, uint256, uint256, bool) => NONDET;
2323

24-
function LiquidationLogic._calculateDebt(
24+
/* function LiquidationLogic._calculateDebt(
2525
DataTypes.ReserveCache memory debtReserveCache,
2626
DataTypes.ExecuteLiquidationCallParams memory params,
2727
uint256 healthFactor
28-
) internal returns (uint256, uint256) => NONDET;
28+
) internal returns (uint256, uint256) => NONDET;*/
2929

3030
function LiquidationLogic._calculateAvailableCollateralToLiquidate(
31-
DataTypes.ReserveData storage collateralReserve,
32-
DataTypes.ReserveCache memory debtReserveCache,
33-
address collateralAsset,
34-
address debtAsset,
35-
uint256 debtToCover,
36-
uint256 userCollateralBalance,
37-
uint256 liquidationBonus,
38-
address // IPriceOracleGetter
39-
) internal returns (uint256,uint256,uint256) => NONDET;
31+
DataTypes.ReserveConfigurationMap memory collateralReserveConfiguration,
32+
uint256 collateralAssetPrice,
33+
uint256 collateralAssetUnit,
34+
uint256 debtAssetPrice,
35+
uint256 debtAssetUnit,
36+
uint256 debtToCover,
37+
uint256 userCollateralBalance,
38+
uint256 liquidationBonus
39+
) internal returns (uint256, uint256, uint256, uint256) => NONDET;
40+
}
41+
42+
43+
// For flashloan
44+
methods {
45+
function _.executeOperation(
46+
address[] assets,
47+
uint256[] amounts,
48+
uint256[] premiums,
49+
address initiator,
50+
bytes params
51+
) external => NONDET; // expect bool;
52+
53+
// simple receiver
54+
function _.executeOperation(
55+
address asset,
56+
uint256 amount,
57+
uint256 premium,
58+
address initiator,
59+
bytes params
60+
) external => NONDET; // expect bool;
4061
}
4162

4263

@@ -55,9 +76,9 @@ function init_state() {
5576
}
5677

5778

58-
hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) {
59-
assert false, "writing the field __deprecatedStableBorrowRate";
60-
}
79+
//hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) {
80+
// assert false, "writing the field __deprecatedStableBorrowRate";
81+
//}
6182

6283
hook Sstore _reserves[KEY address a].__deprecatedStableDebtTokenAddress address stable (address old_stable) {
6384
assert false, "writing the field __deprecatedStableDebtTokenAddress";
@@ -82,29 +103,19 @@ rule stableFieldsUntouched(method f, env e, address _asset)
82103
aTokenToUnderlying[currentContract._reserves[asset].aTokenAddress]==asset
83104
&&
84105
aTokenToUnderlying[currentContract._reserves[asset].variableDebtTokenAddress]==asset;
106+
85107

86-
DataTypes.ReserveData reserve = getReserveDataExtended(_asset);
87108
DataTypes.ReserveDataLegacy reserveLegasy = getReserveData(_asset);
88109

89-
uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate;
90-
address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress;
91110
uint128 currentStableBorrowRate_BEFORE = reserveLegasy.currentStableBorrowRate;
92-
// address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress;
93111

94112
calldataarg args;
95113
f(e,args);
96114

97-
DataTypes.ReserveData reserve2 = getReserveDataExtended(_asset);
98115
DataTypes.ReserveDataLegacy reserveLegasy2 = getReserveData(_asset);
99116

100-
uint128 __deprecatedStableBorrowRate_AFTER = reserve2.__deprecatedStableBorrowRate;
101-
address __deprecatedStableDebtTokenAddress_AFTER = reserve2.__deprecatedStableDebtTokenAddress;
102117
uint128 currentStableBorrowRate_AFTER = reserveLegasy2.currentStableBorrowRate;
103118
address stableDebtTokenAddress_AFTER = reserveLegasy2.stableDebtTokenAddress;
104119

105-
assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER;
106-
assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER;
107120
assert currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER;
108-
// assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER;
109-
110121
}

0 commit comments

Comments
 (0)