test(medusa): properties 13

test/invariants/FuzzTest.t.sol

@@ -1,9 +1,79 @@
 // SPDX-License-Identifier: MIT
 pragma solidity 0.8.26;
 
+import {IEBORequestModule, IOracle} from './Setup.t.sol';
 import {PropertyParent} from './properties/PropertyParent.t.sol';
 
 contract FuzzTest is PropertyParent {
+  /// @custom:property-id 13
+  /// @custom:property each disputeId and responseId can only be tied to one requestId
+  /// TODO: aggregator on arrays...
+  function prop_singleRequestIdForSingleDisputeOrResponseId() public {
+    // for each request
+    for (uint256 currentRequestIdx; currentRequestIdx < _ghost_requests.length; currentRequestIdx++) {
+      bytes32 currentRequestId = _ghost_requests[currentRequestIdx];
+      // for each response of this request
+      for (
+        uint256 currentRequestResponseIdx;
+        currentRequestResponseIdx < _ghost_activeResponses[currentRequestId].length;
+        currentRequestResponseIdx++
+      ) {
+        // for each other request
+        for (uint256 otherRequestsIdx; otherRequestsIdx < _ghost_requests.length; otherRequestsIdx++) {
+          if (otherRequestsIdx == currentRequestIdx) continue;
+
+          bytes32 otherRequestId = _ghost_requests[otherRequestsIdx];
+
+          // for each response of the other request
+          for (
+            uint256 otherRequestResponseIdx;
+            otherRequestResponseIdx < _ghost_activeResponses[otherRequestId].length;
+            otherRequestResponseIdx++
+          ) {
+            // check that it is not pointing to the same request
+            assertTrue(
+              _ghost_activeResponses[currentRequestId][currentRequestResponseIdx]
+                != _ghost_activeResponses[otherRequestId][otherRequestResponseIdx],
+              'prop 13: different response id for same request'
+            );
+          }
+        }
+      }
+    }
+
+    // for each request
+    for (uint256 currentRequestIdx; currentRequestIdx < _ghost_requests.length; currentRequestIdx++) {
+      bytes32 currentRequestId = _ghost_requests[currentRequestIdx];
+      // for each dispute of this request
+      for (
+        uint256 currentRequestDisputeIdx;
+        currentRequestDisputeIdx < _ghost_disputes[currentRequestId].length;
+        currentRequestDisputeIdx++
+      ) {
+        // for each other request
+        for (uint256 otherRequestsIdx; otherRequestsIdx < _ghost_requests.length; otherRequestsIdx++) {
+          if (otherRequestsIdx == currentRequestIdx) continue;
+
+          bytes32 otherRequestId = _ghost_requests[otherRequestsIdx];
+
+          // for each dispute of the other request
+          for (
+            uint256 otherRequestDisputeIdx;
+            otherRequestDisputeIdx < _ghost_disputes[otherRequestId].length;
+            otherRequestDisputeIdx++
+          ) {
+            // check that it is not pointing to the same request
+            assertTrue(
+              _ghost_disputes[currentRequestId][currentRequestDisputeIdx]
+                != _ghost_disputes[otherRequestId][otherRequestDisputeIdx],
+              'prop 13: different dispute id for same request'
+            );
+          }
+        }
+      }
+    }
+  }
+
   //solhint-disable no-empty-blocks
   function test_debug() public {}
 }

test/invariants/PROPERTIES.md

@@ -16,19 +16,19 @@ operator for `caller`)
 
 | Id  | Properties                                                                                                                            | Type | Tested |
 | --- | ------------------------------------------------------------------------------------------------------------------------------------- | ---- | ------ |
-| 1   | requester can always create a request                                                                                                 |      | [ ]    |
-| 2   | there can only be one active request per chainId/epoch at a time                                                                      |      | [ ]    |
-| 3   | a proposer can always propose an answer before the deadline, if no response has been submitted                                        |      | [ ]    |
-| 4   | a proposer can always propose an answer before the deadline, if previous response is disputted and has staked                         |      | [ ]    |
+| 1   | requester can always create a request                                                                                                 |      | [x]    |
+| 2   | there can only be one active request per chainId/epoch at a time                                                                      |      | [x]    |
+| 3   | a proposer can always propose an answer before the deadline, if no response has been submitted                                        |      | [x]    |
+| 4   | a proposer can always propose an answer before the deadline, if previous response is disputted and has staked                         |      | [x]    |
 | 5   | a proposer or a disputer can escalate max MAX_ESCALATION times, each time creating a new tying buffer                                 |      | [ ]    |
-| 6   | a disputer can always dispute a response before the finalisation, if no previous dispute has been made                                |      | [ ]    |
-| 7   | a disputer can only escalate the first disputed response                                                                              |      | [ ]    |
-| 8   | a pledger can only pledge for the correct side for an active dispure or resolution, during the tying buffer or before the deadline    |      | [ ]    |
-| 9   | an arbitrator can always settle a dispute if it has not been finalised yet                                                            |      | [ ]    |
-| 10  | an answer can only be finalized after the deadline                                                                                    |      | [ ]    |
+| 6   | a disputer can always dispute a response before the finalisation, if no previous dispute has been made                                |      | [x]    |
+| 7   | a disputer can only escalate the first disputed response                                                                              |      | [x]    |
+| 8   | a pledger can only pledge for the correct side for an active dispure or resolution, during the tying buffer or before the deadline    |      | [x]    |
+| 9   | an arbitrator can always settle a dispute if it has not been finalised yet                                                            |      | [x]    |
+| 10  | an answer can only be finalized after the deadline                                                                                    |      | [x]    |
 | 11  | bonded token can never be used on behalf of someone else, unless allowed by the Horizon staking contract                              |      | [ ]    |
 | 12  | each bonded amount can only be tied to one requestId                                                                                  |      | [ ]    |
-| 13  | each disputeId and responseId can only be tied to one requestId                                                                       |      | [ ]    |
+| 13  | each disputeId and responseId can only be tied to one requestId                                                                       |      | [x]    |
 
 ## Handler coverage
 

test/invariants/properties/PropertyDisputer.t.sol

@@ -10,7 +10,9 @@ contract PropertyDisputer is HandlerParent {
   function property_disputerCanAlwaysCreateDispute(uint256 _requestSeed, uint256 _responseSeed) public {
     // Pick random request
     (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestSeed);
-    if (_requestId == bytes32(0) || !_ghost_validRequests[_requestId]) return;
+    if (_requestId == bytes32(0) || !_ghost_validRequests[_requestId]) {
+      return;
+    }
 
     // Pick random response
     (bytes32 _responseId, IOracle.Response memory _responseData) = _getRandomActiveResponse(_requestId, _responseSeed);
@@ -62,7 +64,9 @@ contract PropertyDisputer is HandlerParent {
   function property_disputerEscalateFirstDisputedResponse(uint256 _requestSeed, uint256 _disputeSeed) public {
     // Pick random request
     (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestSeed);
-    if (_requestId == bytes32(0) || !_ghost_validRequests[_requestId]) return;
+    if (_requestId == bytes32(0) || !_ghost_validRequests[_requestId]) {
+      return;
+    }
 
     // Pick random dispute
     (bytes32 _disputeId, IOracle.Dispute memory _disputeData) = _getRandomDispute(_requestId, _disputeSeed);

test/invariants/properties/PropertyFinalize.t.sol

@@ -25,5 +25,5 @@ contract PropertyFinalize is HandlerParent {
     }
   }
 
-  // TODO: consider adding property for releasing unfinazible ones?
+  // TODO: consider adding property for releasing unfinalizible ones?
 }

test/invariants/properties/PropertyRequester.t.sol

@@ -8,6 +8,8 @@ contract PropertyRequester is HandlerParent {
   //solhint-disable no-empty-blocks
   constructor() {}
 
+  event Test(bool);
+
   /// @custom:property-id 1
   /// @custom:property Requester can always create a request as long as the same chainId/epoch isn't already finalized with response
   /// @custom:property-id 2
@@ -64,14 +66,17 @@ contract PropertyRequester is HandlerParent {
       // Check if there are active requests and a request finalized with response
       for (uint256 i; i < requestsPerEpochChainId; ++i) {
         requestId = _ghost_requestsPerEpochChainId[_epoch][chainId][i];
-        if (oracle.finalizedAt(requestId) == 0) ++activeRequests;
-        if (oracle.finalizedResponseId(requestId) != 0) {
+        if (requestId != bytes32(0) && oracle.finalizedAt(requestId) == 0) ++activeRequests;
+        if (requestId != bytes32(0) && oracle.finalizedResponseId(requestId) != 0) {
           isFinalizedWithResponse = true;
           break;
         }
       }
 
       // property 1 and 2
+      emit RequestCreated(requestId, _epoch, chainId);
+      emit Test(isFinalizedWithResponse);
+      emit Test(activeRequests > 0);
       assertTrue(isFinalizedWithResponse || activeRequests > 0, 'prop-1-2: create request reverted');
     }
   }