Gelato Oracle Swap Freezer

certora/gsm/conf/gsm/GelatoOracleSwapFreezer.conf

@@ -0,0 +1,16 @@
+{
+    "files": [
+        "certora/gsm/harness/GelatoOracleSwapFreezerHarness.sol",
+        "src/contracts/facilitators/gsm/swapFreezer/GelatoOracleSwapFreezer.sol",
+    ],
+    "packages": [
+        "aave-v3-origin/=lib/aave-v3-origin/src",
+    ],
+    "assert_autofinder_success": true,
+    "optimistic_loop":true,
+…        "-depth 20",
+    ],
+    "verify":
+        "GelatoOracleSwapFreezerHarness:certora/gsm/specs/gsm/GelatoOracleSwapFreezer.spec",
+    //"build_cache": true,
+}

certora/gsm/conf/gsm/OracleSwapFreezer.conf

@@ -1,7 +1,7 @@
 {
     "files": [
-        "certora/gsm/harness/OracleSwapFreezerHarness.sol",
-        "src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezer.sol",
+        "certora/gsm/harness/ChainlinkOracleSwapFreezerHarness.sol",
+        "src/contracts/facilitators/gsm/swapFreezer/ChainlinkOracleSwapFreezer.sol",
     ],
     "packages": [
         "aave-v3-origin/=lib/aave-v3-origin/src",
@@ -14,13 +14,13 @@
     "solc": "solc8.20",
     "rule_sanity" : "basic",
     "multi_assert_check": true,
-    "msg": "OracleSwapFreezer",
+    "msg": "ChainlinkOracleSwapFreezer",
     "smt_timeout": "4000",
     "prover_args": [
         "-copyLoopUnroll 6",
         "-depth 20",
     ],
     "verify":
-        "OracleSwapFreezerHarness:certora/gsm/specs/gsm/OracleSwapFreezer.spec",
+        "ChainlinkOracleSwapFreezerHarness:certora/gsm/specs/gsm/ChainlinkOracleSwapFreezer.spec",
     //"build_cache": true,
 }

certora/gsm/harness/OracleSwapFreezerHarness.sol → certora/gsm/harness/ChainlinkOracleSwapFreezerHarness.sol

@@ -1,12 +1,13 @@
+// SPDX-License-Identifier: No-License
 pragma solidity ^0.8.0;
 
-import {OracleSwapFreezer} from 'src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezer.sol';
+import {ChainlinkOracleSwapFreezer} from 'src/contracts/facilitators/gsm/swapFreezer/ChainlinkOracleSwapFreezer.sol';
 import {IPoolAddressesProvider} from 'aave-v3-origin/contracts/interfaces/IPoolAddressesProvider.sol';
 import {IPriceOracle} from 'aave-v3-origin/contracts/interfaces/IPriceOracle.sol';
 //import {AutomationCompatibleInterface} from '../dependencies/chainlink/AutomationCompatibleInterface.sol';
 import {IGsm} from 'src/contracts/facilitators/gsm/interfaces/IGsm.sol';
 
-contract OracleSwapFreezerHarness is OracleSwapFreezer {
+contract ChainlinkOracleSwapFreezerHarness is ChainlinkOracleSwapFreezer {
   constructor(
     IGsm gsm,
     address underlyingAsset,
@@ -17,7 +18,7 @@ contract OracleSwapFreezerHarness is OracleSwapFreezer {
     uint128 unfreezeUpperBound,
     bool allowUnfreeze
   )
-    OracleSwapFreezer(
+    ChainlinkOracleSwapFreezer(
       gsm,
       underlyingAsset,
       addressProvider,

certora/gsm/harness/GelatoOracleSwapFreezerHarness.sol

@@ -0,0 +1,84 @@
+// SPDX-License-Identifier: No-License
+pragma solidity ^0.8.0;
+
+import {GelatoOracleSwapFreezer} from 'src/contracts/facilitators/gsm/swapFreezer/GelatoOracleSwapFreezer.sol';
+import {IPoolAddressesProvider} from 'aave-v3-origin/contracts/interfaces/IPoolAddressesProvider.sol';
+import {IPriceOracle} from 'aave-v3-origin/contracts/interfaces/IPriceOracle.sol';
+import {IGsm} from 'src/contracts/facilitators/gsm/interfaces/IGsm.sol';
+
+contract GelatoOracleSwapFreezerHarness is GelatoOracleSwapFreezer {
+  constructor(
+    IGsm gsm,
+    address underlyingAsset,
+    IPoolAddressesProvider addressProvider,
+    uint128 freezeLowerBound,
+    uint128 freezeUpperBound,
+    uint128 unfreezeLowerBound,
+    uint128 unfreezeUpperBound,
+    bool allowUnfreeze
+  )
+    GelatoOracleSwapFreezer(
+      gsm,
+      underlyingAsset,
+      addressProvider,
+      freezeLowerBound,
+      freezeUpperBound,
+      unfreezeLowerBound,
+      unfreezeUpperBound,
+      allowUnfreeze
+    )
+  {}
+
+  function validateBounds(
+    uint128 freezeLowerBound,
+    uint128 freezeUpperBound,
+    uint128 unfreezeLowerBound,
+    uint128 unfreezeUpperBound,
+    bool allowUnfreeze
+  ) external pure returns (bool) {
+    return
+      _validateBounds(
+        freezeLowerBound,
+        freezeUpperBound,
+        unfreezeLowerBound,
+        unfreezeUpperBound,
+        allowUnfreeze
+      );
+  }
+
+  function isActionAllowed(Action actionToExecute) external view returns (bool) {
+    return _isActionAllowed(actionToExecute);
+  }
+
+  function getAction() external view returns (uint8) {
+    Action res = _getAction();
+    if (res == Action.NONE) return 0;
+    if (res == Action.FREEZE) return 1;
+    if (res == Action.UNFREEZE) return 2;
+    return 3;
+  }
+
+  function isSeized() external view returns (bool) {
+    return GSM.getIsSeized();
+  }
+
+  function isFreezeAllowed() external view returns (bool) {
+    return _isActionAllowed(Action.FREEZE);
+  }
+
+  function isUnfreezeAllowed() external view returns (bool) {
+    return _isActionAllowed(Action.UNFREEZE);
+  }
+
+  function isFrozen() external view returns (bool) {
+    return GSM.getIsFrozen();
+  }
+
+  function getPrice() external view returns (uint256) {
+    return IPriceOracle(ADDRESS_PROVIDER.getPriceOracle()).getAssetPrice(UNDERLYING_ASSET);
+  }
+
+  function hasRole() external view returns (bool) {
+    return GSM.hasRole(GSM.SWAP_FREEZER_ROLE(), address(this));
+  }
+}

certora/gsm/specs/gsm/OracleSwapFreezer.spec → certora/gsm/specs/gsm/ChainlinkOracleSwapFreezer.spec

@@ -1,5 +1,5 @@
 
-// verifies properties of OracleSwapFreezer
+// verifies properties of ChainlinkOracleSwapFreezer
 
 methods {
 	function getFreezeBound() external returns (uint128, uint128) envfree;

src/contracts/facilitators/gsm/swapFreezer/ChainlinkOracleSwapFreezer.sol

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {AutomationCompatibleInterface} from 'src/contracts/dependencies/chainlink/AutomationCompatibleInterface.sol';
+import {IPoolAddressesProvider} from 'aave-v3-origin/contracts/interfaces/IPoolAddressesProvider.sol';
+import {IGsm} from 'src/contracts/facilitators/gsm/interfaces/IGsm.sol';
+import {OracleSwapFreezerBase} from 'src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezerBase.sol';
+
+/**
+ * @title ChainlinkOracleSwapFreezer
+ * @notice Chainlink-compatible automated swap freezer for GSM.
+ */
+contract ChainlinkOracleSwapFreezer is OracleSwapFreezerBase, AutomationCompatibleInterface {
+  /**
+   * @dev Constructor
+   * @dev Freeze/unfreeze bounds are specified in USD with 8-decimal precision, like Aave v3 Price Oracles
+   * @dev Unfreeze boundaries are "contained" in freeze boundaries, where freezeLowerBound < unfreezeLowerBound and unfreezeUpperBound < freezeUpperBound
+   * @dev All bound ranges are inclusive
+   * @param gsm The GSM that this contract will trigger freezes/unfreezes on
+   * @param underlyingAsset The address of the collateral asset
+   * @param addressesProvider The Aave Addresses Provider for looking up the Price Oracle
+   * @param freezeLowerBound The lower price bound for freeze operations
+   * @param freezeUpperBound The upper price bound for freeze operations
+   * @param unfreezeLowerBound The lower price bound for unfreeze operations, must be 0 if unfreezing not allowed
+   * @param unfreezeUpperBound The upper price bound for unfreeze operations, must be 0 if unfreezing not allowed
+   * @param allowUnfreeze True if bounds verification should factor in the unfreeze boundary, false otherwise
+   */
+  constructor(
+    IGsm gsm,
+    address underlyingAsset,
+    IPoolAddressesProvider addressesProvider,
+    uint128 freezeLowerBound,
+    uint128 freezeUpperBound,
+    uint128 unfreezeLowerBound,
+    uint128 unfreezeUpperBound,
+    bool allowUnfreeze
+  )
+    OracleSwapFreezerBase(
+      gsm,
+      underlyingAsset,
+      addressesProvider,
+      freezeLowerBound,
+      freezeUpperBound,
+      unfreezeLowerBound,
+      unfreezeUpperBound,
+      allowUnfreeze
+    )
+  {}
+
+  /// @inheritdoc AutomationCompatibleInterface
+  function performUpkeep(bytes calldata) external {
+    _execute();
+  }
+
+  /// @inheritdoc AutomationCompatibleInterface
+  function checkUpkeep(bytes calldata) external view returns (bool, bytes memory) {
+    return (_checkExecute(), '');
+  }
+}

src/contracts/facilitators/gsm/swapFreezer/GelatoOracleSwapFreezer.sol

@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {IGelatoOracleSwapFreezer} from 'src/contracts/facilitators/gsm/swapFreezer/interfaces/IGelatoOracleSwapFreezer.sol';
+import {IPoolAddressesProvider} from 'aave-v3-origin/contracts/interfaces/IPoolAddressesProvider.sol';
+import {IGsm} from 'src/contracts/facilitators/gsm/interfaces/IGsm.sol';
+import {OracleSwapFreezerBase} from 'src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezerBase.sol';
+
+/**
+ * @title GelatoOracleSwapFreezer
+ * @notice Gelato-compatible automated swap freezer for GSM.
+ */
+contract GelatoOracleSwapFreezer is OracleSwapFreezerBase, IGelatoOracleSwapFreezer {
+  /**
+   * @dev Constructor
+   * @dev Freeze/unfreeze bounds are specified in USD with 8-decimal precision, like Aave v3 Price Oracles
+   * @dev Unfreeze boundaries are "contained" in freeze boundaries, where freezeLowerBound < unfreezeLowerBound and unfreezeUpperBound < freezeUpperBound
+   * @dev All bound ranges are inclusive
+   * @param gsm The GSM that this contract will trigger freezes/unfreezes on
+   * @param underlyingAsset The address of the collateral asset
+   * @param addressesProvider The Aave Addresses Provider for looking up the Price Oracle
+   * @param freezeLowerBound The lower price bound for freeze operations
+   * @param freezeUpperBound The upper price bound for freeze operations
+   * @param unfreezeLowerBound The lower price bound for unfreeze operations, must be 0 if unfreezing not allowed
+   * @param unfreezeUpperBound The upper price bound for unfreeze operations, must be 0 if unfreezing not allowed
+   * @param allowUnfreeze True if bounds verification should factor in the unfreeze boundary, false otherwise
+   */
+  constructor(
+    IGsm gsm,
+    address underlyingAsset,
+    IPoolAddressesProvider addressesProvider,
+    uint128 freezeLowerBound,
+    uint128 freezeUpperBound,
+    uint128 unfreezeLowerBound,
+    uint128 unfreezeUpperBound,
+    bool allowUnfreeze
+  )
+    OracleSwapFreezerBase(
+      gsm,
+      underlyingAsset,
+      addressesProvider,
+      freezeLowerBound,
+      freezeUpperBound,
+      unfreezeLowerBound,
+      unfreezeUpperBound,
+      allowUnfreeze
+    )
+  {}
+
+  /**
+   * @dev Performs the swap freeze action depending on the oracle value
+   */
+  function performUpkeep(bytes calldata) external {
+    _execute();
+  }
+
+  /**
+   * @notice Returns whether the action can be performed and the encoded call data for execution.
+   * @return True if the action can be performed, false otherwise.
+   * @return The encoded call data for the action to be executed.
+   */
+  function checkUpkeep(bytes calldata) external view returns (bool, bytes memory) {
+    return (_getAction() == Action.NONE ? false : true, abi.encodeCall(this.performUpkeep, ('')));
+  }
+}

src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezer.sol → src/contracts/facilitators/gsm/swapFreezer/OracleSwapFreezerBase.sol

@@ -3,18 +3,17 @@ pragma solidity ^0.8.10;
 
 import {IPoolAddressesProvider} from 'aave-v3-origin/contracts/interfaces/IPoolAddressesProvider.sol';
 import {IPriceOracle} from 'aave-v3-origin/contracts/interfaces/IPriceOracle.sol';
-import {AutomationCompatibleInterface} from 'src/contracts/dependencies/chainlink/AutomationCompatibleInterface.sol';
 import {IGsm} from 'src/contracts/facilitators/gsm/interfaces/IGsm.sol';
 
 /**
- * @title OracleSwapFreezer
+ * @title OracleSwapFreezerBase
  * @author Aave
  * @notice Swap freezer that enacts the freeze action based on underlying oracle price, GSM's state and predefined price boundaries
- * @dev Chainlink Automation-compatible contract using Aave V3 Price Oracle, where prices are USD denominated with 8-decimal precision
+ * @dev It uses Aave V3 Price Oracle, where prices are USD denominated with 8-decimal precision
  * @dev Freeze action is executable if GSM is not seized, not frozen and price is outside of the freeze bounds
  * @dev Unfreeze action is executable if GSM is not seized, frozen, unfreezing is allowed and price is inside the unfreeze bounds
  */
-contract OracleSwapFreezer is AutomationCompatibleInterface {
+abstract contract OracleSwapFreezerBase {
   enum Action {
     NONE,
     FREEZE,
@@ -37,7 +36,7 @@ contract OracleSwapFreezer is AutomationCompatibleInterface {
    * @dev All bound ranges are inclusive
    * @param gsm The GSM that this contract will trigger freezes/unfreezes on
    * @param underlyingAsset The address of the collateral asset
-   * @param addressProvider The Aave Addresses Provider for looking up the Price Oracle
+   * @param addressesProvider The Aave Addresses Provider for looking up the Price Oracle
    * @param freezeLowerBound The lower price bound for freeze operations
    * @param freezeUpperBound The upper price bound for freeze operations
    * @param unfreezeLowerBound The lower price bound for unfreeze operations, must be 0 if unfreezing not allowed
@@ -47,7 +46,7 @@ contract OracleSwapFreezer is AutomationCompatibleInterface {
   constructor(
     IGsm gsm,
     address underlyingAsset,
-    IPoolAddressesProvider addressProvider,
+    IPoolAddressesProvider addressesProvider,
     uint128 freezeLowerBound,
     uint128 freezeUpperBound,
     uint128 unfreezeLowerBound,
@@ -67,16 +66,18 @@ contract OracleSwapFreezer is AutomationCompatibleInterface {
     );
     GSM = gsm;
     UNDERLYING_ASSET = underlyingAsset;
-    ADDRESS_PROVIDER = addressProvider;
+    ADDRESS_PROVIDER = addressesProvider;
     _freezeLowerBound = freezeLowerBound;
     _freezeUpperBound = freezeUpperBound;
     _unfreezeLowerBound = unfreezeLowerBound;
     _unfreezeUpperBound = unfreezeUpperBound;
     _allowUnfreeze = allowUnfreeze;
   }
 
-  /// @inheritdoc AutomationCompatibleInterface
-  function performUpkeep(bytes calldata) external {
+  /**
+   * @dev Performs the swap freeze action depending on the oracle value
+   */
+  function _execute() internal {
     Action action = _getAction();
     if (action == Action.FREEZE) {
       GSM.setSwapFreeze(true);
@@ -85,9 +86,12 @@ contract OracleSwapFreezer is AutomationCompatibleInterface {
     }
   }
 
-  /// @inheritdoc AutomationCompatibleInterface
-  function checkUpkeep(bytes calldata) external view returns (bool, bytes memory) {
-    return (_getAction() == Action.NONE ? false : true, '');
+  /**
+   * @dev Returns whether the action can be performed
+   * @return True if the action can be performed, false otherwise.
+   */
+  function _checkExecute() internal view returns (bool) {
+    return _getAction() == Action.NONE ? false : true;
   }
 
   /**

src/contracts/facilitators/gsm/swapFreezer/interfaces/IGelatoOracleSwapFreezer.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+interface IGelatoOracleSwapFreezer {
+  function performUpkeep(bytes calldata) external;
+
+  function checkUpkeep(bytes calldata) external view returns (bool, bytes memory);
+}