# Detailed TLA+ spec for the atomic cyclic swap.

In this blog, we will study the detailed TLA+ specification of the cyclic swap problem explained in [[cyclic swap]](https://hackmd.io/dHQ_0s93T8O0t28iIMoR0g). First, we will define the possible state that a party has. We then discuss the events exchanged between the parties and the state transition resulting from these events. Lastly, we will discuss the invariants imposed during the protocol run and the results.

For better understanding, let's reiterate the steps explained in the previous blog [[cyclic swap]](https://hackmd.io/dHQ_0s93T8O0t28iIMoR0g), which are as fllows:

**step 1**: All the parties involved in the cyclic swap share a unique hash of preimage with each other, i.e., each party will share $dig_i = Hash(pre_i)$.
**step 2**: Once they receive the set of hashes from all the parties, each party will deploy the contract (HTLC) and lock the assets on the respective blockchain network with a hash $H = Hash(dig_1, dig_2, \cdots, dig_n)$.
**step 3**: After the assets are locked, each party should reveal the secret. The discloser of the secret is constrained by the time, i.e., it should be revealed within a certain block height ($B_c$) after the contract is deployed.
**step 4**: After each party reveals the secret, assets are committed to being unlocked to be transferred to the intended recipient. For example, in the cyclic swap between $A$, $B$, and $C$, $A$ transfers to $B$, $B$ to $C$, and $C$ to $A$. We called this phase a ***commit phase***
**step 5**: If some party doesn't receive a secret from at least one party (because of network delay and/or a deliberate attack), then it will publish a refund transaction and enter the ***refund phase***. Note that a party is constrained to publish a refund transaction within a certain time limit, say block height $B_r$ ($B_r > B_c$).
**step 6**: At the block height $B_p$ ($B_p > B_r > B_c$), if all the parties are in the commit phase, then each party unlocks the assets in the contract to facilitate the transfer; else, abort the swap. We called this as a ***payment phase***.

Let's first list down the assumptions before directly jumping to the detailed TLA+ specification. We assume that all the smart contracts are deployed on the respective blockchains with a hash $H$. Given this, we will say that each party is in the *init* phase (explained below). Furthermore, we don't consider the time parameter in the specification. Instead, we do it based on the events. For example, $B_r$ lapses when a party notices that all other parties have moved to the commit phase.

<!-- Before we jump into the TLA+ specification of the protocol, lets list the assumptions. We assume that the -->


The protocol runs in three phases named: commit, refund, and payment, which is represented with the variable *rmState* in the spec. Each party further maintains the list of distinct parties from which the secret has been received. Spec maintain the same in *receivedSecret*. Furthermore, a party maintains the message queue (*msg*), whose value contains the messages other parties sent. Note that *msg* is not the set of messages received by the party. TLA+ handles the received event by varying the delay and/or the drop rate, which results in multiple states. The state of each party $r$ in the spec consists of the protocol phase (*rmState[r]*), the set of parties from which the secret has been received (*receivedSecret[r]*), and lastly, the message received, as depicted in the code snippet above. Modification in any of the state variables results in the new state.


The state of each party is initialized, as shown in the code snippet above. Each party starts with some initial state we called it as a ***init***, while the message queue and the list of received secrets are set to empty, as shown in the above code snippet.


Next, each party $r$ sends a secret to all other parties (line 90). Note that the message queue (*msg*) is read by all the parties. So putting the message in the *msg* is equivalent to broadcasting a message to all the parties. Because we assume each party has an account on all the blockchains involved in the swap, modeling the message queue like this is a valid move.



When the party $r$ receives a secret from any party $r_s$, it adds it to the *receivedSecret[r]*, and the moment it receives the secret from all the parties (line 59), changes the phase from init to commit (line 60). This change in the phase results in the new state for party $r$. For example, in the figure below, which represents the cyclic swap between three parties $A$, $B$, and $C$, party $A$ and $C$ receive secret from all the parties and hence change the phase from init to commit. However, the message disclosing the secret from $A$ takes longer to reach $B$ (red dotted line in the figure below), so it remains in the init phase. So the state of party $A$ and $C$ changes while for $B$, it remains the same. The system's state is represented by the state of each party involved in the swap. So change in the state of at least one party result in a change of the system state.



If either party changes to commit and party $r$ is still in the init phase, it is treated equivalent to the time ($B_c$) lapse for sending the secret and hence changes to the refund phase, as shown in the figure above. Because TLA+ will check for all possible states by varying delays in the message delivery at the party, there exists at least a state where all the parties reach the commit phase.


Once all the parties reach the commit phase, each party $r$ moves to the payment phase. For consistency, our protocol should ensure that all the parties must reach the payment phase or none. This is ensured by adding an invariant (CSConsistency given in the code snippet below), which checks that there shouldn't exist any two parties, one stuck in either refund or init phase while the other reaches to payment phase.



To ensure the correctness, we added another invariant (CSTypeOK represented by the code snippet above), which checks the following constraints:
1. A party shouldn't transit to any other phase apart from init, commit, refund, and payment.
2. A party shouldn't receive a message from other parties not involved in the swap.
3. Parties should exchange the message disclosing a *secret* only. All other messages are treated as invalid, i.e., will violate the constraint.

In the next blog, we will discuss the detailed implementation of our protocol on three different blockchains. We will also emphasize the gaps between actual implementation and the TLA+ specs.

<!-- State of each party further consists of receivedSecret, which maintains the list of distinct nodes from which the secret has been received.

Each party start with some initial state we called it as a ***init***.
-->