diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index f015bff..1654482 100644 --- a/test/invariants/PROPERTIES.md +++ b/test/invariants/PROPERTIES.md @@ -12,55 +12,23 @@ Prophet modules in use (some modified from the example repo): - AccessControl: every external function is gated, for Horizon operators (ie `caller` is either msg.sender or msg.sender is authorized as operator for `caller`) - -- 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 - ## Properties & Invariants -| Id | Properties | Type | -| --- | ---------- | ---- | -| | requester can always create a request | | -| | there can only be one active request per chainId/epoch at a time | | - +| 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 | | [ ] | +| 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 | | [ ] | +| 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 | | [ ] | ## Handler coverage @@ -147,3 +115,47 @@ Oracle | 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