feat: medusa tests

.gitignore

@@ -17,9 +17,8 @@ out-via-ir
 # Keep the latest deployment only
 broadcast/*/*/*
 
-# Out dir
+# Medusa files
 out
 crytic-export
-
-# Echidna corpus
-test/invariants/fuzz/echidna_coverage
+test/invariants/corpus
+test/invariants/fuzz/corpus

.solhint.tests.json

@@ -10,7 +10,7 @@
     "var-name-mixedcase": "off",
     "const-name-snakecase": "off",
     "no-inline-assembly": "off",
-    "no-empty-blocks": "error",
+    "no-empty-blocks": "off",
     "definition-name-capwords": "off",
     "named-parameters-function": "off",
     "no-global-import": "off",

medusa.json

@@ -0,0 +1,87 @@
+{
+  "fuzzing": {
+    "workers": 10,
+    "workerResetLimit": 50,
+    "timeout": 0,
+    "testLimit": 0,
+    "shrinkLimit": 100000,
+    "callSequenceLength": 100,
+    "corpusDirectory": "test/invariants/corpus",
+    "coverageEnabled": true,
+    "targetContracts": ["FuzzTest"],
+    "predeployedContracts": { "ValidatorLib": "0xc0ffee" },
+    "targetContractsBalances": [],
+    "constructorArgs": {},
+    "deployerAddress": "0x30000",
+    "senderAddresses": [
+      "0x10000",
+      "0x20000",
+      "0x30000",
+      "0x40000",
+      "0x50000",
+      "0x60000",
+      "0x70000",
+      "0x80000",
+      "0x90000",
+      "0xa0000"
+    ],
+    "blockNumberDelayMax": 60480,
+    "blockTimestampDelayMax": 604800,
+    "blockGasLimit": 125000000,
+    "transactionGasLimit": 12500000,
+    "testing": {
+      "stopOnFailedTest": true,
+      "stopOnFailedContractMatching": false,
+      "stopOnNoTests": true,
+      "testAllContracts": false,
+      "traceAll": false,
+      "assertionTesting": {
+        "enabled": true,
+        "testViewMethods": true,
+        "panicCodeConfig": {
+          "failOnCompilerInsertedPanic": false,
+          "failOnAssertion": true,
+          "failOnArithmeticUnderflow": false,
+          "failOnDivideByZero": false,
+          "failOnEnumTypeConversionOutOfBounds": false,
+          "failOnIncorrectStorageAccess": false,
+          "failOnPopEmptyArray": false,
+          "failOnOutOfBoundsArrayAccess": false,
+          "failOnAllocateTooMuchMemory": false,
+          "failOnCallUninitializedVariable": false
+        }
+      },
+      "propertyTesting": {
+        "enabled": true,
+        "testPrefixes": ["property_"]
+      },
+      "optimizationTesting": {
+        "enabled": true,
+        "testPrefixes": ["optimize_"]
+      },
+      "targetFunctionSignatures": [],
+      "excludeFunctionSignatures": [""]
+    },
+    "chainConfig": {
+      "codeSizeCheckDisabled": true,
+      "cheatCodes": {
+        "cheatCodesEnabled": true,
+        "enableFFI": false
+      }
+    }
+  },
+  "compilation": {
+    "platform": "crytic-compile",
+    "platformConfig": {
+      "target": "test/invariants/FuzzTest.t.sol",
+      "solcVersion": "",
+      "exportDirectory": "",
+      "args": ["--compile-libraries=(ValidatorLib,0xc0ffee)"]
+    }
+  },
+  "logging": {
+    "level": "info",
+    "logDirectory": "",
+    "noColor": false
+  }
+}

test/invariants/FuzzTest.t.sol

@@ -0,0 +1,90 @@
+// 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. If it does, check it wasn't
+            // finalized without answer
+
+            if (
+              _ghost_activeResponses[currentRequestId][currentRequestResponseIdx]
+                == _ghost_activeResponses[otherRequestId][otherRequestResponseIdx]
+                && (
+                  (oracle.finalizedAt(currentRequestId) == 0 && oracle.finalizedResponseId(currentRequestId) != 0)
+                    || (oracle.finalizedAt(otherRequestId) == 0 && oracle.finalizedResponseId(otherRequestId) != 0)
+                )
+            ) {
+              assertTrue(false, 'prop 13: same response id for different requests');
+            }
+          }
+        }
+      }
+    }
+
+    // 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. If it does, check it wasn't
+            // finalized without answer
+
+            if (
+              _ghost_activeResponses[currentRequestId][currentRequestDisputeIdx]
+                == _ghost_activeResponses[otherRequestId][otherRequestDisputeIdx]
+                && (
+                  (oracle.finalizedAt(currentRequestId) == 0 && oracle.finalizedResponseId(currentRequestId) != 0)
+                    || (oracle.finalizedAt(otherRequestId) == 0 && oracle.finalizedResponseId(otherRequestId) != 0)
+                )
+            ) {
+              assertTrue(false, 'prop 13: same response id for different requests');
+            }
+          }
+        }
+      }
+    }
+  }
+}

test/invariants/PROPERTIES.md

@@ -1,4 +1,161 @@
-| Properties                                        | Type       |
-|---------------------------------------------------|------------|
-| Greeting should never be empty | Valid state |
-| Only the owner can set the greeting | State transition |
+# Properties
+
+## Principles
+Precondition for proposing/disputing: stake(token) and provision on Horizon staking contract
+
+Prophet modules in use (some modified from the example repo):
+- request: eboRequestCreator -> eboRequestModule
+- response: bondedResponseModule
+- dispute: bondedDisputeEscalationModule (claimEscalationReward tries to slash, if revert oog (too many users), then has new fn `slash()` is called)
+- resolution: arbitratorModule + ArbitratorContract (receive resolution, then calls resolveDispute and tries to finalize)
+- finality: eboFinalityModule (emit event and check if request created via eboRequestCreator)
+- AccessControl: every external function is gated, for Horizon operators (ie `caller` is either msg.sender or msg.sender is authorized as
+operator for `caller`)
+
+## Properties & Invariants
+
+| Id  | Properties                                                                                                                            | Type | Tested |
+| --- | ------------------------------------------------------------------------------------------------------------------------------------- | ---- | ------ |
+| 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                                |      | [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                                                                       |      | [x]    |
+
+## Handler coverage
+
+EBORequestCreator
+| Function                                                               | Handler |
+| ---------------------------------------------------------------------- | ------- |
+| createRequest(uint256,string)                                          | []      |
+| addChain(string)                                                       | []      |
+| removeChain(string)                                                    | []      |
+| setRequestModuleData(address,IEBORequestModule.RequestParameters)      | []      |
+| setResponseModuleData(address,IBondedResponseModule.RequestParameters) | []      |
+| setDisputeModuleData(address,IBondEscalationModule.RequestParameters)  | []      |
+| setResolutionModuleData(address,IArbitratorModule.RequestParameters)   | []      |
+| setFinalityModuleData(address)                                         | []      |
+| setEpochManager(IEpochManager)                                         | []      |
+
+EBORequestModule
+| Function                                    | Handler |
+| ------------------------------------------- | ------- |
+| createRequest(bytes32,bytes,address)        | onlyOracle      |
+| addEBORequestCreator(IEBORequestCreator)    | []      |
+| removeEBORequestCreator(IEBORequestCreator) | []      |
+
+BondedResponseModule
+| Function                                                    | Handler |
+| ----------------------------------------------------------- | ------- |
+| propose(IOracle.Request,IOracle.Response,address)           | onlyOracle      |
+| finalizeRequest(IOracle.Request,IOracle.Response,address)   | onlyOracle      |
+| releaseUnutilizedResponse(IOracle.Request,IOracle.Response) | []      |
+
+BondEscalationModule
+| Function                                                                        | Handler |
+| ------------------------------------------------------------------------------- | ------- |
+| disputeResponse(IOracle.Request,IOracle.Response,IOracle.Dispute)               | onlyOracle      |
+| onDisputeStatusChange(bytes32,IOracle.Request,IOracle.Response,IOracle.Dispute) | onlyOracle      |
+| pledgeForDispute(IOracle.Request, IOracle.Dispute)                              | []      |
+| pledgeAgainstDispute(IOracle.Request, IOracle.Dispute)                          | []      |
+| settleBondEscalation(IOracle.Request,IOracle.Response,IOracle.Dispute)          | []      |
+
+CouncilArbitrator
+| Function                                                  | Handler |
+| --------------------------------------------------------- | ------- |
+| resolve(IOracle.Request,IOracle.Response,IOracle.Dispute) | onlyArbitratorModule      |
+| arbitrateDispute(bytes32,IOracle.DisputeStatus)           | []      |
+
+EBOFinalityModule
+| Function                                                  | Handler |
+| --------------------------------------------------------- | ------- |
+| finalizeRequest(IOracle.Request,IOracle.Response,address) | onlyOracle      |
+| amendEpoch(uint256,string[],uint256[])                    | []      |
+| addEBORequestCreator(IEBORequestCreator)                  | []      |
+| removeEBORequestCreator(IEBORequestCreator)               | []      |
+
+HorizonAccountingExtension
+| Function                                                                       | Handler |
+| ------------------------------------------------------------------------------ | ------- |
+| approveModule(address)                                                         | []      |
+| revokeModule(address)                                                          | []      |
+| pledge(address,IOracle.Request,IOracle.Dispute,IERC20,uint256)                 | []      |
+| onSettleBondEscalation(IOracle.Request,IOracle.Dispute,IERC20,uint256,uint256) | []      |
+| claimEscalationReward(bytes32,address)                                         | []      |
+| pay(bytes32,address,address,IERC20,uint256)                                    | onlyAllowedModule      |
+| bond(address,bytes32,IERC20,uint256)                                           | onlyAllowedModule      |
+| bond(address,bytes32,IERC20,uint256,address)                                   | onlyAllowedModule      |
+| release(address,bytes32,IERC20,uint256)                                        | onlyAllowedModule      |
+| slash(bytes32,uint256,uint256)                                                 | []      |
+| setMaxUsersToCheck(uint128)                                                    | []      |
+
+Arbitrable
+| Function                    | Handler |
+| --------------------------- | ------- |
+| setArbitrator(address)      | []      |
+| setPendingCouncil(address)  | []      |
+| confirmCouncil()            | []      |
+
+Oracle
+| Function                                                             | Handler |
+| -------------------------------------------------------------------- | ------- |
+| createRequest(Request,bytes32) external returns (bytes32)            | []      |
+| createRequests(Request[],bytes32[]) external returns (bytes32[])     | []      |
+| listRequestIds(uint256,uint256) external view returns (bytes32[])    | []      |
+| proposeResponse(Request,Response) external returns (bytes32)         | []      |
+| disputeResponse(Request,Response,Dispute) external returns (bytes32) | []      |
+| escalateDispute(Request,Response,Dispute) external                   | []      |
+| resolveDispute(Request,Response,Dispute) external                    | []      |
+| finalize(Request,Response) external                                  | []      |
+
+
+
+
+- Requester
+    - Can always create a request
+    - only one chainId/epoch can be requested at a time (a tuple can have second request if finalized without answer)
+
+- Proposer
+    - Can always send answer before the deadline if enough token to bound in Horizon staking contract AND if any previous response is disputed OR no response at all
+    - Can escalate MAX ESCALATION times
+    - Every escalation creates a new tying buffer for further escalation (even if past deadline)
+
+- Disputer
+    - Can always dispute if before finalisation/during dispute window, if enough token to bound in Horizon staking and not previously disputed
+    - only first disputed response is escalated (others go to resolution)
+    - Can escalate MAX ESCALATION times
+    - every escalation creates a new tying buffer for further escalation (even if past deadline)
+
+- Pledgers:
+    - can pledge on any active dispute or resolution, during tying buffer/before deadline, if it’s that side’s turn
+    - Can only pledge one pledge at a time (you can only surpass other team by one pledge at a time), first to tie then to out-pledge (always 2 ties by side)
+
+- Protocol
+    - finalise only after deadline
+    - no possible way for a given actor to use another one’s bonded token (no bonding or pledging/claiming on behalf of someone else if not allowed in the Horison staking contract)
+    - bonded amount only accessible by one requestId
+    - disputeId and responseId can only be tied to a given requestId
+    - arbitrator: can always settled a dispute if not finalised (can be a no resolution)
+
+
+- disputer
+
+wins → his money + proposer bonded amt
+loose loose all
+no resolution his money (when no pledging or max escalation on both side or other resolution module logic if only dispute module)
+
+- pledger
+wins → their money + enemy
+no resolution -> their money
+
+**winning determined by *pledgers* (b, c)**
+
+bonded dispute goes to resolution if: escalateDispute or tie

test/invariants/Reproducers.t.sol

@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.26;
+
+import {FuzzTest} from './FuzzTest.t.sol';
+import {IEBORequestModule, IOracle} from './Setup.t.sol';
+
+contract Reproducers is FuzzTest {
+}