Merge pull request #16 from TokenLogic-com-au/gelato-oracle

Update Certora Harness

Author: miguelmtzinf

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 renamed to 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 renamed to 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;