add the get/set rules for EMode

Certora · Sep 23, 2024 · f04eef0 · f04eef0
1 parent 67b7e19
commit f04eef0
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 16 deletions.
diff --git a/.github/workflows/certora-basic.yml b/.github/workflows/certora-basic.yml
@@ -69,6 +69,7 @@ jobs:
           - VariableDebtToken.conf
           - NEW-pool-no-summarizations.conf
           - stableRemoved.conf
+          - EModeConfiguration.conf
           - NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"

diff --git a/certora/basic/harness/EModeConfigurationHarness.sol b/certora/basic/harness/EModeConfigurationHarness.sol
@@ -8,24 +8,23 @@ import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.
 contract EModeConfigurationHarness {
   DataTypes.EModeCategory public eModeCategory;
 
-  function setCollateral(uint256 reserveIndex,bool collateral) public {
+  function setCollateral(uint256 reserveIndex, bool enabled) public {
     DataTypes.EModeCategory memory emode_new = eModeCategory;
-    EModeConfiguration.setCollateral(emode_new, reserveIndex, collateral);
-    eModeCategory.isCollateralBitmap = emode_new.isCollateralBitmap;
+    eModeCategory.collateralBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.collateralBitmap, reserveIndex, enabled);
   }
 
   function isCollateralAsset(uint256 reserveIndex) public returns (bool) {
-    return EModeConfiguration.isCollateralAsset(eModeCategory.isCollateralBitmap, reserveIndex);
+    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.collateralBitmap, reserveIndex);
   }
 
 
-  function setBorrowable(uint256 reserveIndex,bool borrowable) public {
+
+  function setBorrowable(uint256 reserveIndex,bool enabled) public {
     DataTypes.EModeCategory memory emode_new = eModeCategory;
-    EModeConfiguration.setBorrowable(emode_new, reserveIndex, borrowable);
-    eModeCategory.isBorrowableBitmap = emode_new.isBorrowableBitmap;
+    eModeCategory.borrowableBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.borrowableBitmap, reserveIndex, enabled);
   }
-
+  
   function isBorrowableAsset(uint256 reserveIndex) public returns (bool) {
-    return EModeConfiguration.isBorrowableAsset(eModeCategory.isBorrowableBitmap, reserveIndex);
+    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.borrowableBitmap, reserveIndex);
   }
 }
diff --git a/certora/basic/scripts/run-all.sh b/certora/basic/scripts/run-all.sh
@@ -1,4 +1,4 @@
-#CMN="--compilation_steps_only"
+CMN="--compilation_steps_only"
 #CMN="--typecheck_only"
 
 
@@ -32,10 +32,10 @@ echo "******** Running:  6 Stable fields are un-touched ***************"
 certoraRun $CMN certora/basic/conf/stableRemoved.conf \
            --msg "6: Stable fields are un-touched"
 
-#echo
-#echo "******** Running:  6 EModeConfiguration ***************"
-#certoraRun $CMN certora/basic/conf/EModeConfiguration.conf \
-#           --msg "6: EModeConfiguration"
+echo
+echo "******** Running:  6 EModeConfiguration ***************"
+certoraRun $CMN certora/basic/conf/EModeConfiguration.conf \
+           --msg "6: EModeConfiguration"
 
 
 echo

diff --git a/certora/basic/specs/EModeConfiguration.spec b/certora/basic/specs/EModeConfiguration.spec
@@ -1,7 +1,7 @@
 methods {
-  function setCollateral(uint256 reserveIndex,bool collateral) external envfree;
+  function setCollateral(uint256 reserveIndex,bool enabled) external envfree;
   function isCollateralAsset(uint256 reserveIndex) external returns (bool) envfree;
-  function setBorrowable(uint256 reserveIndex,bool borrowable) external envfree;
+  function setBorrowable(uint256 reserveIndex,bool enabled) external envfree;
   function isBorrowableAsset(uint256 reserveIndex) external returns (bool) envfree;
 }