Merge pull request #2 from bgd-labs/feat/stable-rate-removal

Stable rate removal

Makefile

@@ -36,4 +36,5 @@ download :; cast etherscan-source --chain ${chain} -d src/etherscan/${chain}_${a
 git-diff :
 	@mkdir -p diffs
 	@npx prettier ${before} ${after} --write
-	@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --diff-algorithm=patience --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md
+	@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md
+

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

@@ -2,7 +2,6 @@
   "files": [
     "certora/harness/ATokenHarness.sol",
     "certora/harness/PoolHarness.sol",
-    "certora/harness/StableDebtTokenHarness.sol",
     "certora/harness/SimpleERC20.sol",
     "src/contracts/instances/VariableDebtTokenInstance.sol",
     "src/contracts/helpers/AaveProtocolDataProvider.sol",
@@ -20,7 +19,6 @@
   ],
   "struct_link": [
     "PoolHarness:aTokenAddress=ATokenHarness",
-    "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
     "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
     "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
   ],

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

@@ -2,7 +2,6 @@
   "files": [
     "certora/harness/ATokenHarness.sol",
     "certora/harness/PoolHarness.sol",
-    "certora/harness/StableDebtTokenHarness.sol",
     "certora/harness/SimpleERC20.sol",
     "src/contracts/instances/VariableDebtTokenInstance.sol",
     "src/contracts/helpers/AaveProtocolDataProvider.sol",
@@ -17,7 +16,6 @@
   ],
   "struct_link": [
     "PoolHarness:aTokenAddress=ATokenHarness",
-    "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
     "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
     "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
   ],

certora/harness/PoolHarness.sol

@@ -23,8 +23,7 @@ contract PoolHarness is PoolInstance {
 
   function getTotalDebt(address asset) public view returns (uint256) {
     uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply();
-    uint256 totalStable = IERC20(_reserves[asset].stableDebtTokenAddress).totalSupply();
-    return totalVariable + totalStable;
+    return totalVariable;
   }
 
   function getTotalATokenSupply(address asset) public view returns (uint256) {
@@ -35,10 +34,6 @@ contract PoolHarness is PoolInstance {
     return _reserves[asset].liquidityIndex;
   }
 
-  function getReserveStableBorrowRate(address asset) public view returns (uint256) {
-    return _reserves[asset].currentStableBorrowRate;
-  }
-
   function getReserveVariableBorrowIndex(address asset) public view returns (uint256) {
     return _reserves[asset].variableBorrowIndex;
   }

certora/harness/ReserveConfigurationHarness.sol

@@ -131,18 +131,6 @@ contract ReserveConfigurationHarness {
     return ReserveConfiguration.getBorrowingEnabled(reservesConfig);
   }
 
-  // Enables or disables stable rate borrowing on the reserve
-  function setStableRateBorrowingEnabled(bool enabled) public {
-    DataTypes.ReserveConfigurationMap memory configNew = reservesConfig;
-    ReserveConfiguration.setStableRateBorrowingEnabled(configNew, enabled);
-    reservesConfig.data = configNew.data;
-  }
-
-  // Gets the stable rate borrowing state of the reserve
-  function getStableRateBorrowingEnabled() public view returns (bool) {
-    return ReserveConfiguration.getStableRateBorrowingEnabled(reservesConfig);
-  }
-
   // Sets the reserve factor of the reserve
   function setReserveFactor(uint256 reserveFactor) public {
     DataTypes.ReserveConfigurationMap memory configNew = reservesConfig;
@@ -302,16 +290,14 @@ contract ReserveConfigurationHarness {
 
   // Executes a setter of a bool parameter according to the given id
   function executeBoolSetterById(uint256 id, bool val) public {
-    require(id >= 0 && id <= 5);
+    require(id >= 0 && id <= 4);
     if (id == 0) {
       setActive(val);
     } else if (id == 1) {
       setFrozen(val);
     } else if (id == 2) {
       setBorrowingEnabled(val);
     } else if (id == 3) {
-      setStableRateBorrowingEnabled(val);
-    } else if (id == 4) {
       setPaused(val);
     } else {
       setBorrowableInIsolation(val);
@@ -320,16 +306,14 @@ contract ReserveConfigurationHarness {
 
   // Executes a getter of a bool parameter according to the given id
   function executeBoolGetterById(uint256 id) public view returns (bool) {
-    require(id >= 0 && id <= 5);
+    require(id >= 0 && id <= 4);
     if (id == 0) {
       return getActive();
     } else if (id == 1) {
       return getFrozen();
     } else if (id == 2) {
       return getBorrowingEnabled();
     } else if (id == 3) {
-      return getStableRateBorrowingEnabled();
-    } else if (id == 4) {
       return getPaused();
     } else {
       return getBorrowableInIsolation();

certora/specs/NEW-pool-base.spec

@@ -64,11 +64,6 @@ methods {
   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);
 

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

@@ -11,7 +11,6 @@ methods {
 
   //  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);
 
@@ -37,11 +36,10 @@ function ghostUpdate() returns bool {
 }
 
 
-function calculateInterestRatesMock(DataTypes.CalculateInterestRatesParams params) returns (uint256, uint256, uint256) {
+function calculateInterestRatesMock(DataTypes.CalculateInterestRatesParams params) returns (uint256, uint256) {
   uint256 liquidityRate = 1;
-  uint256 stableBorrowRate = 1;
   uint256 variableBorrowRate = 1;
-  return (liquidityRate, stableBorrowRate, variableBorrowRate);
+  return (liquidityRate, variableBorrowRate);
 }
 
 

certora/specs/ReserveConfiguration.spec

@@ -19,8 +19,6 @@ methods {
   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;
@@ -104,12 +102,6 @@ rule setBorrowingEnabledIntegrity(bool 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;
-}
-
 // checks the integrity of set ReserveFactor function and correct retrieval of the corresponding getter.
 rule setReserveFactorIntegrity(uint256 reserveFactor) {
   setReserveFactor(reserveFactor);