From c0ffee66ebd33c60047ada66c71bc493cfcc0227 Mon Sep 17 00:00:00 2001 From: drgorillamd <83670532+drgorillamd@users.noreply.github.com> Date: Sat, 30 Nov 2024 15:19:56 +0100 Subject: [PATCH] test(medusa): properties 13 --- test/invariants/FuzzTest.t.sol | 70 +++++++++++++++++++ test/invariants/PROPERTIES.md | 20 +++--- .../properties/PropertyDisputer.t.sol | 8 ++- .../properties/PropertyFinalize.t.sol | 2 +- .../properties/PropertyRequester.t.sol | 9 ++- 5 files changed, 94 insertions(+), 15 deletions(-) diff --git a/test/invariants/FuzzTest.t.sol b/test/invariants/FuzzTest.t.sol index a2a24a9..210d807 100644 --- a/test/invariants/FuzzTest.t.sol +++ b/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 {} } diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index 1654482..0a5486c 100644 --- a/test/invariants/PROPERTIES.md +++ b/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 diff --git a/test/invariants/properties/PropertyDisputer.t.sol b/test/invariants/properties/PropertyDisputer.t.sol index adeeb82..3780c11 100644 --- a/test/invariants/properties/PropertyDisputer.t.sol +++ b/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); diff --git a/test/invariants/properties/PropertyFinalize.t.sol b/test/invariants/properties/PropertyFinalize.t.sol index 934614f..1bda629 100644 --- a/test/invariants/properties/PropertyFinalize.t.sol +++ b/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? } diff --git a/test/invariants/properties/PropertyRequester.t.sol b/test/invariants/properties/PropertyRequester.t.sol index 7cda835..fb74484 100644 --- a/test/invariants/properties/PropertyRequester.t.sol +++ b/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'); } }