test(medusa): compliant properties

defi-wonderland · Nov 27, 2024 · 710c3d1 · 710c3d1
1 parent 10a7a07
commit 710c3d1
Show file tree

Hide file tree

Showing 2 changed files with 102 additions and 15 deletions.
diff --git a/test/invariants/helpers/Utils.t.sol b/test/invariants/helpers/Utils.t.sol
@@ -155,6 +155,50 @@ contract Utils {
     }
   }
 
+  function assertLt(uint256 a, uint256 b) internal {
+    assertLt(a, b, 'assertLt: a >= b');
+  }
+
+  function assertLt(uint256 a, uint256 b, string memory reason) internal {
+    if (a >= b) {
+      emit TestFailure(reason);
+      assert(false);
+    }
+  }
+
+  function assertLte(uint256 a, uint256 b) internal {
+    assertLte(a, b, 'assertLte: a > b');
+  }
+
+  function assertLte(uint256 a, uint256 b, string memory reason) internal {
+    if (a > b) {
+      emit TestFailure(reason);
+      assert(false);
+    }
+  }
+
+  function assertGt(uint256 a, uint256 b) internal {
+    assertGt(a, b, 'assertGt: a <= b');
+  }
+
+  function assertGt(uint256 a, uint256 b, string memory reason) internal {
+    if (a <= b) {
+      emit TestFailure(reason);
+      assert(false);
+    }
+  }
+
+  function assertGte(uint256 a, uint256 b) internal {
+    assertGte(a, b, 'assertGte: a < b');
+  }
+
+  function assertGte(uint256 a, uint256 b, string memory reason) internal {
+    if (a < b) {
+      emit TestFailure(reason);
+      assert(false);
+    }
+  }
+
   function assertTrue(bool a) internal {
     assertTrue(a, 'assertTrue: !a');
   }

diff --git a/test/invariants/properties/PropertyRequester.t.sol b/test/invariants/properties/PropertyRequester.t.sol
@@ -9,21 +9,61 @@ contract PropertyRequester is HandlerParent {
   constructor() {}
 
   /// @custom:property-id 1
-  /// @custom:property There can only be one request finalized with response per chainId/epoch
-  function property_onlyOneRequestFinalizedWithResponse(uint256 _requestIdSeed) external {
-    bytes32 requestId = _getRandomRequestId(_requestIdSeed);
-    if (requestId == bytes32(0)) return;
+  /// @custom:property Requester can always create a request as long as the same chainId/epoch isn't finalized with response
+  function property_canAlwaysCreateRequest(uint256 _epoch, uint256 _chainIdSeed) external {
+    _epoch = bound(_epoch, START_EPOCH, block.timestamp);
 
-    IOracle.Request memory requestData = _ghost_requestData[requestId];
-    IEBORequestModule.RequestParameters memory requestParams =
-      abi.decode(requestData.requestModuleData, (IEBORequestModule.RequestParameters));
+    string memory chainId = _getRandomChainId(_chainIdSeed);
+    if (bytes(chainId).length == 0) return;
 
-    uint256 requestsPerEpochChainId = _ghost_requestsPerEpochChainId[requestParams.epoch][requestParams.chainId].length;
-    if (requestsPerEpochChainId < 2) return;
+    uint256 requestsPerEpochChainId = _ghost_requestsPerEpochChainId[_epoch][chainId].length;
+    bytes32 requestId;
+    bool isFinalizedWithResponse;
 
-    for (uint256 i; i < requestsPerEpochChainId - 1; ++i) {
-      requestId = _ghost_requestsPerEpochChainId[requestParams.epoch][requestParams.chainId][i];
-      assertEq(oracle.finalizedResponseId(requestId), 0, 'prop-1: same chainId/epoch request finalized with response');
+    // Create request via EBORequestCreator
+    try eboRequestCreator.createRequest(_epoch, chainId) {
+      // Check if there is a request finalized with response
+      for (uint256 i; i < requestsPerEpochChainId; ++i) {
+        requestId = _ghost_requestsPerEpochChainId[_epoch][chainId][i];
+        if (oracle.finalizedResponseId(requestId) != 0) {
+          isFinalizedWithResponse = true;
+          break;
+        }
+      }
+
+      assertFalse(isFinalizedWithResponse, 'prop-1: same chainId/epoch request already finalized with response');
+
+      // Get current request data
+      IOracle.Request memory requestData = eboRequestCreator.getRequestData();
+
+      // Build request module parameters
+      IEBORequestModule.RequestParameters memory requestParams =
+        abi.decode(requestData.requestModuleData, (IEBORequestModule.RequestParameters));
+      requestParams.epoch = _epoch;
+      requestParams.chainId = chainId;
+      requestData.requestModuleData = abi.encode(requestParams);
+
+      // Calculate request ID using same logic as Oracle
+      bytes32 requestId = keccak256(abi.encode(requestData));
+
+      // Track the request
+      _ghost_requests.push(requestId);
+      _ghost_requestsPerEpochChainId[_epoch][chainId].push(requestId);
+      _ghost_requestData[requestId] = requestData;
+      _ghost_validRequests[requestId] = true;
+
+      emit RequestCreated(requestId, _epoch, chainId);
+    } catch {
+      // Check if there is a request finalized with response
+      for (uint256 i; i < requestsPerEpochChainId; ++i) {
+        requestId = _ghost_requestsPerEpochChainId[_epoch][chainId][i];
+        if (oracle.finalizedResponseId(requestId) != 0) {
+          isFinalizedWithResponse = true;
+          break;
+        }
+      }
+
+      assertTrue(isFinalizedWithResponse, 'prop-1: create request reverted');
     }
   }
 
@@ -38,11 +78,14 @@ contract PropertyRequester is HandlerParent {
       abi.decode(requestData.requestModuleData, (IEBORequestModule.RequestParameters));
 
     uint256 requestsPerEpochChainId = _ghost_requestsPerEpochChainId[requestParams.epoch][requestParams.chainId].length;
-    if (requestsPerEpochChainId < 2) return;
+    uint256 activeRequests;
 
-    for (uint256 i; i < requestsPerEpochChainId - 1; ++i) {
+    // Check if there are active requests
+    for (uint256 i; i < requestsPerEpochChainId; ++i) {
       requestId = _ghost_requestsPerEpochChainId[requestParams.epoch][requestParams.chainId][i];
-      assertNotEq(oracle.finalizedAt(requestId), 0, 'prop-2: same chainId/epoch active request');
+      if (oracle.finalizedAt(requestId) == 0) ++activeRequests;
     }
+
+    assertLte(activeRequests, 1, 'prop-2: same chainId/epoch active requests');
   }
 }