Update GhoSteward

certora/steward/specs/rules.spec

@@ -289,19 +289,19 @@ rule updateGhoBorrowCap__correctness() {
     assert BORROW_CAP==newBorrowCap;
 
     uint256 borrow_cap_after = BORROW_CAP;
-    assert borrow_cap_before <= borrow_cap_after && to_mathint(borrow_cap_after) <= 2*borrow_cap_before;
+    assert to_mathint(borrow_cap_after) <= 2*borrow_cap_before;
 }
 
 
 rule updateGhoBorrowRate__correctness() {
     env e;  uint256 newBorrowRate;
-    uint256 borrow_rate_begore = BORROW_RATE;
+    uint256 borrow_rate_before = BORROW_RATE;
     updateGhoBorrowRate(e,newBorrowRate);
     assert FAC.getStrategyByRate(newBorrowRate) == STRATEGY;
 
-    assert (borrow_rate_begore-GHO_BORROW_RATE_CHANGE_MAX() <= to_mathint(newBorrowRate)
+    assert (borrow_rate_before-GHO_BORROW_RATE_CHANGE_MAX() <= to_mathint(newBorrowRate)
             &&
-            to_mathint(newBorrowRate) <= borrow_rate_begore+GHO_BORROW_RATE_CHANGE_MAX());
+            to_mathint(newBorrowRate) <= borrow_rate_before+GHO_BORROW_RATE_CHANGE_MAX());
     assert (newBorrowRate <= GHO_BORROW_RATE_MAX());
 }
 
@@ -313,8 +313,7 @@ rule updateGsmExposureCap__correctness() {
     assert EXPOSURE_CAP==newExposureCap;
 
     uint128 exposure_cap_after = EXPOSURE_CAP;
-    assert exposure_cap_before <= exposure_cap_after &&
-        to_mathint(exposure_cap_after) <= 2*exposure_cap_before;
+    assert to_mathint(exposure_cap_after) <= 2*exposure_cap_before;
 }
 
 

src/contracts/misc/GhoStewardV2.sol

@@ -20,10 +20,10 @@ import {IGhoStewardV2} from './interfaces/IGhoStewardV2.sol';
  * @title GhoStewardV2
  * @author Aave Labs
  * @notice Helper contract for managing parameters of the GHO reserve and GSM
- * @dev This contract must be granted `PoolAdmin` in the Aave V3 Ethereum Pool, `BucketManager` in GHO Token and `Configurator` in every GSM asset to be managed.
+ * @dev This contract must be granted `RiskAdmin` in the Aave V3 Ethereum Pool, `BucketManager` in GHO Token and `Configurator` in every GSM asset to be managed.
  * @dev Only the Risk Council is able to action contract's functions, based on specific conditions that have been agreed upon with the community.
  * @dev Only the Aave DAO is able add or remove approved GSMs.
- * @dev When updating GSM fee strategy the method asumes that the current strategy is FixedFeeStrategy for enforcing parameters
+ * @dev When updating GSM fee strategy the method assumes that the current strategy is FixedFeeStrategy for enforcing parameters
  * @dev FixedFeeStrategy is used when creating a new strategy for GSM
  * @dev FixedRateStrategyFactory is used when creating a new borrow rate strategy for GHO
  */
@@ -136,7 +136,7 @@ contract GhoStewardV2 is Ownable, IGhoStewardV2 {
     ).getConfiguration(GHO_TOKEN);
     uint256 currentBorrowCap = configuration.getBorrowCap();
     require(
-      _isIncreaseLowerThanMax(currentBorrowCap, newBorrowCap, currentBorrowCap),
+      _isDifferenceLowerThanMax(currentBorrowCap, newBorrowCap, currentBorrowCap),
       'INVALID_BORROW_CAP_UPDATE'
     );
 
@@ -186,7 +186,7 @@ contract GhoStewardV2 is Ownable, IGhoStewardV2 {
   ) external onlyRiskCouncil notTimelocked(_gsmTimelocksByAddress[gsm].gsmExposureCapLastUpdated) {
     uint128 currentExposureCap = IGsm(gsm).getExposureCap();
     require(
-      _isIncreaseLowerThanMax(currentExposureCap, newExposureCap, currentExposureCap),
+      _isDifferenceLowerThanMax(currentExposureCap, newExposureCap, currentExposureCap),
       'INVALID_EXPOSURE_CAP_UPDATE'
     );
 
@@ -207,11 +207,11 @@ contract GhoStewardV2 is Ownable, IGhoStewardV2 {
     uint256 currentBuyFee = IGsmFeeStrategy(currentFeeStrategy).getBuyFee(1e4);
     uint256 currentSellFee = IGsmFeeStrategy(currentFeeStrategy).getSellFee(1e4);
     require(
-      _isIncreaseLowerThanMax(currentBuyFee, buyFee, GSM_FEE_RATE_CHANGE_MAX),
+      _isDifferenceLowerThanMax(currentBuyFee, buyFee, GSM_FEE_RATE_CHANGE_MAX),
       'INVALID_BUY_FEE_UPDATE'
     );
     require(
-      _isIncreaseLowerThanMax(currentSellFee, sellFee, GSM_FEE_RATE_CHANGE_MAX),
+      _isDifferenceLowerThanMax(currentSellFee, sellFee, GSM_FEE_RATE_CHANGE_MAX),
       'INVALID_SELL_FEE_UPDATE'
     );
 

src/contracts/misc/interfaces/IGhoStewardV2.sol

@@ -31,7 +31,7 @@ interface IGhoStewardV2 {
   /**
    * @notice Updates the GHO borrow cap, only if:
    * - respects `MINIMUM_DELAY`, the minimum time delay between updates
-   * - the update changes up to 100% upwards
+   * - the update changes up to 100% upwards or downwards
    * @dev Only callable by Risk Council
    * @param newBorrowCap The new borrow cap (in whole tokens)
    */
@@ -50,7 +50,7 @@ interface IGhoStewardV2 {
   /**
    * @notice Updates the exposure cap of the GSM, only if:
    * - respects `MINIMUM_DELAY`, the minimum time delay between updates
-   * - the update changes up to 100% upwards
+   * - the update changes up to 100% upwards or downwards
    * @dev Only callable by Risk Council
    * @param gsm The gsm address to update
    * @param newExposureCap The new exposure cap (in underlying asset terms)
@@ -60,7 +60,7 @@ interface IGhoStewardV2 {
   /**
    * @notice Updates the fixed percent fees of the GSM, only if:
    * - respects `MINIMUM_DELAY`, the minimum time delay between updates
-   * - the update changes up to `GSM_FEE_RATE_CHANGE_MAX` upwards (for both buy and sell individually);
+   * - the update changes up to `GSM_FEE_RATE_CHANGE_MAX` upwards or downwards (for both buy and sell individually)
    * @dev Only callable by Risk Council
    * @param gsm The gsm address to update
    * @param buyFee The new buy fee (expressed in bps) (e.g. 0.0150e4 results in 1.50%)