for PR

Author: nisnislevi

certora/basic/specs/EModeConfiguration.spec

@@ -6,11 +6,37 @@ methods {
 }
 
 
+/*=====================================================================================
+  Rule: setCollateralIntegrity / setBorrowableIntegrity:
+  We check the integrity of the functions setReserveBitmapBit (which is a setter) and 
+  isReserveEnabledOnBitmap (which is a getter), simply by setting an arbitrary value to arbitrary 
+  location, and then reading it using the getter.
+
+  Note: the functions setCollateral and isCollateralAsset are envelopes to the above setter and getter
+  and are implemented in the harness.
+
+  Status: PASS
+  Link: 
+  =====================================================================================*/
 rule setCollateralIntegrity(uint256 reserveIndex, bool collateral) {
   setCollateral(reserveIndex,collateral);
   assert isCollateralAsset(reserveIndex) == collateral;
 }
+rule setBorrowableIntegrity(uint256 reserveIndex, bool borrowable) {
+  setBorrowable(reserveIndex,borrowable);
+  assert isBorrowableAsset(reserveIndex) == borrowable;
+}
+
+
+
+/*=====================================================================================
+  Rule: independencyOfCollateralSetters / independencyOfBorrowableSetters:
+  We check that when calling to setReserveBitmapBit(index,val) only the value at the given
+  index may be altered.
 
+  Status: PASS
+  Link: 
+  =====================================================================================*/
 rule independencyOfCollateralSetters(uint256 reserveIndex, bool collateral) {
   uint256 reserveIndex_other;
 
@@ -20,13 +46,6 @@ rule independencyOfCollateralSetters(uint256 reserveIndex, bool collateral) {
 
   assert (reserveIndex != reserveIndex_other => before == after);
 }
-
-
-rule setBorrowableIntegrity(uint256 reserveIndex, bool borrowable) {
-  setBorrowable(reserveIndex,borrowable);
-  assert isBorrowableAsset(reserveIndex) == borrowable;
-}
-
 rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) {
   uint256 reserveIndex_other;
 

certora/basic/specs/stableRemoved.spec

@@ -89,7 +89,7 @@ rule stableFieldsUntouched(method f, env e, address _asset)
   uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate;
   address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress;
   uint128 currentStableBorrowRate_BEFORE = reserveLegasy.currentStableBorrowRate;
-  address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress;
+  //  address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress;
 
   calldataarg args;
   f(e,args);
@@ -105,6 +105,6 @@ rule stableFieldsUntouched(method f, env e, address _asset)
   assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER;
   assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER;
   assert currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER;
-  assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER;
+  //  assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER;
 
 }