test(medusa): assert prop-7

test/invariants/handlers/BaseHandler.t.sol

@@ -82,7 +82,7 @@ contract BaseHandler is Setup, Actors {
   function _getRandomDispute(bytes32 _requestId, uint256 _seed) internal view returns (bytes32, IOracle.Dispute memory) {
     bytes32[] storage disputes = _ghost_disputes[_requestId];
     if (disputes.length == 0) {
-      return (bytes32(0), IOracle.Dispute(address(0), address(0), bytes32(0), 0));
+      return (bytes32(0), IOracle.Dispute(address(0), address(0), bytes32(0), bytes32(0)));
     }
     bytes32 disputeId = disputes[_seed % disputes.length];
     return (disputeId, _ghost_disputeData[disputeId]);

test/invariants/handlers/HandlerOracle.t.sol

@@ -62,30 +62,37 @@ contract HandlerOracle is BaseHandler {
     _ghost_disputes[requestId].push(disputeId);
     _ghost_disputeData[disputeId] = dispute;
     _ghost_bonds[disputer][requestId] += DISPUTE_BOND_SIZE;
+    if (_ghost_disputes[requestId].length > 1) {
+      _ghost_escalatedDisputes[disputeId] = true;
+    }
 
     emit DisputeCreated(requestId, responseId, disputeId);
 
     return disputeId;
   }
 
-  function handleEscalateDispute(uint256 _requestSeed, uint256 _disputeIndex) external {
+  function handleEscalateDispute(uint256 _requestSeed, uint256 _disputeSeed) external {
     (bytes32 requestId, IOracle.Request memory request) = _getRandomRequest(_requestSeed);
-    if (requestId == bytes32(0)) return;
+    if (requestId == bytes32(0) || !_ghost_validRequests[requestId]) return;
 
-    (, IOracle.Dispute memory dispute) = _getRandomDispute(requestId, _disputeIndex);
-    if (dispute.requestId == bytes32(0)) return;
+    (bytes32 disputeId, IOracle.Dispute memory dispute) = _getRandomDispute(requestId, _disputeSeed);
+    if (disputeId == bytes32(0)) return;
 
-    if (oracle.disputeStatus(keccak256(abi.encode(dispute))) != IOracle.DisputeStatus.Escalated) return;
+    if (oracle.disputeStatus(disputeId) != IOracle.DisputeStatus.Active) return;
 
     IOracle.Response memory response = _ghost_responseData[dispute.responseId];
+
     oracle.escalateDispute(request, response, dispute);
+
+    // Track escalated dispute
+    _ghost_escalatedDisputes[disputeId] = true;
   }
 
-  function handleResolveDispute(uint256 _requestSeed, uint256 _disputeIndex) external {
+  function handleResolveDispute(uint256 _requestSeed, uint256 _disputeSeed) external {
     (bytes32 requestId, IOracle.Request memory request) = _getRandomRequest(_requestSeed);
     if (requestId == bytes32(0)) return;
 
-    (, IOracle.Dispute memory dispute) = _getRandomDispute(requestId, _disputeIndex);
+    (, IOracle.Dispute memory dispute) = _getRandomDispute(requestId, _disputeSeed);
     if (dispute.requestId == bytes32(0)) return;
 
     IOracle.Response memory response = _ghost_responseData[dispute.responseId];

test/invariants/helpers/MockHorizonStaking.t.sol

@@ -27,8 +27,10 @@ contract MockHorizonStaking {
     uint32 _maxVerifierCut,
     uint64 _thawingPeriod
   ) external {
+    IHorizonStaking.Provision storage prov = provisions[_serviceProvider][_verifier];
+
     provisions[_serviceProvider][_verifier] = IHorizonStaking.Provision({
-      tokens: _tokens,
+      tokens: prov.tokens + _tokens,
       tokensThawing: 0,
       sharesThawing: 0,
       maxVerifierCut: _maxVerifierCut,

test/invariants/properties/PropertyDisputer.t.sol

@@ -7,13 +7,13 @@ import {HandlerParent} from '../handlers/HandlerParent.t.sol';
 contract PropertyDisputer is HandlerParent {
   /// @custom:property-id 6
   /// @custom:property A disputer can always dispute a response before the finalisation, if no previous dispute has been made
-  function property_disputerCanAlwaysCreateDispute(uint256 _requestIdSeed, uint256 _responseIdSeed) public {
+  function property_disputerCanAlwaysCreateDispute(uint256 _requestSeed, uint256 _responseSeed) public {
     // Pick random request
-    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestIdSeed);
+    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestSeed);
     if (_requestId == bytes32(0) || !_ghost_validRequests[_requestId]) return;
 
     // Pick random response
-    (bytes32 _responseId, IOracle.Response memory _responseData) = _getRandomActiveResponse(_requestId, _responseIdSeed);
+    (bytes32 _responseId, IOracle.Response memory _responseData) = _getRandomActiveResponse(_requestId, _responseSeed);
     if (_responseId == bytes32(0)) return;
 
     IOracle.Dispute memory _disputeData = IOracle.Dispute({
@@ -23,12 +23,13 @@ contract PropertyDisputer is HandlerParent {
       requestId: _requestId
     });
 
-    // Stake some GRT in Horizon
+    // Stake and provision some GRT in Horizon
     _stakeGRT(DISPUTE_BOND_SIZE);
     _provisionGRT(DISPUTE_BOND_SIZE);
 
     bytes32 _prevDisputeId = oracle.disputeOf(_responseId);
 
+    // Dispute response
     vm.prank(msg.sender);
     try oracle.disputeResponse(_requestData, _responseData, _disputeData) returns (bytes32 _disputeId) {
       // check if no previous dispute
@@ -38,6 +39,9 @@ contract PropertyDisputer is HandlerParent {
       _ghost_disputes[_requestId].push(_disputeId);
       _ghost_disputeData[_disputeId] = _disputeData;
       _ghost_bonds[msg.sender][_requestId] += DISPUTE_BOND_SIZE;
+      if (_ghost_disputes[_requestId].length > 1) {
+        _ghost_escalatedDisputes[_disputeId] = true;
+      }
 
       emit DisputeCreated(_requestId, _responseId, _disputeId);
     } catch {
@@ -55,40 +59,51 @@ contract PropertyDisputer is HandlerParent {
 
   /// @custom:property-id 7
   /// @custom:property A disputer can only escalate the first disputed response
-  function prop_disputerEscalateFirstDisputedResponse(
-    uint256 _requestIdSeed,
-    uint256 _responseIdSeed,
-    uint256 _disputeSeed
-  ) public {
-    _stakeGRT(DISPUTE_BOND_SIZE);
+  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;
 
-    // Pick random Dispute
-    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestIdSeed);
-    (bytes32 _responseId, IOracle.Response memory _responseData) = _getRandomActiveResponse(_requestId, _responseIdSeed);
+    // Pick random dispute
     (bytes32 _disputeId, IOracle.Dispute memory _disputeData) = _getRandomDispute(_requestId, _disputeSeed);
+    if (_disputeId == bytes32(0)) return;
 
-    // Escalate it
+    // Get disputed response
+    IOracle.Response memory _responseData = _ghost_responseData[_disputeData.responseId];
+
+    // Stake and provision some GRT in Horizon
+    _stakeGRT(DISPUTE_BOND_SIZE);
+    _provisionGRT(DISPUTE_BOND_SIZE);
+
+    // Escalate dispute
     vm.prank(msg.sender);
     try oracle.escalateDispute(_requestData, _responseData, _disputeData) {
       // check that the dispute is the first one
-      assertEq(_ghost_activeResponses[_requestId][0], _disputeData.requestId, 'property 7: not first dispute');
+      assertEq(_ghost_activeResponses[_requestId][0], _disputeData.responseId, 'property 7: not first dispute');
+
+      // add to ghost escalated disputes
+      _ghost_escalatedDisputes[_disputeId] = true;
     } catch {
-      // not first dispute or
-      // not past the bond escalation deadline
-      // past deadline/tying buffer or
-      // already escalated or
-      // bond not tied or
-      //
+      // not first dispute, or
+      // not past the bond escalation deadline, or
+      // already escalated, or
+      // bond not tied
+      assertTrue(
+        _ghost_activeResponses[_requestId][0] != _disputeData.responseId
+          || block.timestamp <= oracle.disputeCreatedAt(_disputeId) + DISPUTE_DEADLINE
+          || _ghost_escalatedDisputes[_disputeId],
+        'property 7: fails on first disputed response'
+      );
     }
   }
 
   /// @custom:property-id 8a
   /// @custom:property A pledger can only pledge for the correct side for an active dispute or resolution, during the tying buffer or before the deadline
-  function prop_pledgerCanPledgeFor(uint256 _requestIdSeed, uint256 _disputeSeed) public {
+  function property_pledgerCanPledgeFor(uint256 _requestSeed, uint256 _disputeSeed) public {
     _stakeGRT(DISPUTE_BOND_SIZE);
 
     // Pick random dispute
-    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestIdSeed);
+    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestSeed);
     (bytes32 _disputeId, IOracle.Dispute memory _disputeData) = _getRandomDispute(_requestId, _disputeSeed);
 
     vm.prank(msg.sender);
@@ -104,11 +119,11 @@ contract PropertyDisputer is HandlerParent {
 
   /// @custom:property-id 8b
   /// @custom:property A pledger can only pledge for the correct side for an active dispute or resolution, during the tying buffer or before the deadline
-  function prop_pledgerCanPledgeAgainst(uint256 _requestIdSeed, uint256 _disputeSeed) public {
+  function property_pledgerCanPledgeAgainst(uint256 _requestSeed, uint256 _disputeSeed) public {
     _stakeGRT(DISPUTE_BOND_SIZE);
 
     // Pick random dispute
-    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestIdSeed);
+    (bytes32 _requestId, IOracle.Request memory _requestData) = _getRandomRequest(_requestSeed);
     (bytes32 _disputeId, IOracle.Dispute memory _disputeData) = _getRandomDispute(_requestId, _disputeSeed);
 
     vm.prank(msg.sender);
@@ -124,9 +139,9 @@ contract PropertyDisputer is HandlerParent {
 
   /// @custom:property-id 9
   /// @custom:property An arbitrator can always settle a dispute if it has not been finalised yet
-  function prop_arbitratorCanSettle(uint256 _requestIdSeed, uint256 _disputeSeed, uint256 _whoWonSeed) public {
+  function property_arbitratorCanSettle(uint256 _requestSeed, uint256 _disputeSeed, uint256 _whoWonSeed) public {
     // Pick random dispute
-    (bytes32 _requestId,) = _getRandomRequest(_requestIdSeed);
+    (bytes32 _requestId,) = _getRandomRequest(_requestSeed);
     (bytes32 _disputeId,) = _getRandomDispute(_requestId, _disputeSeed);
 
     // Pick random outcome (won, lost, noResolution)

test/invariants/properties/PropertyProposer.t.sol

@@ -9,9 +9,9 @@ contract PropertyProposer is HandlerParent {
   /// @custom:property A proposer can always propose an answer before the deadline, if no response has been submitted
   /// @custom:property-id 4
   /// @custom:property A proposer can always propose an answer before the deadline, if previous response is disputed and has staked
-  function property_proposerProposeBeforeDeadlineAndNoAnswer(uint256 _requestIdSeed, bytes calldata _response) public {
+  function property_proposerProposeBeforeDeadlineAndNoAnswer(uint256 _requestSeed, bytes calldata _response) public {
     // Pick random request
-    (bytes32 requestId, IOracle.Request memory requestData) = _getRandomRequest(_requestIdSeed);
+    (bytes32 requestId, IOracle.Request memory requestData) = _getRandomRequest(_requestSeed);
     if (requestId == bytes32(0) || !_ghost_validRequests[requestId]) return;
 
     // Build response data