test(medusa): properties md update

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