Skip to content

Commit

Permalink
mod: refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
Stefano Angieri authored and Stefano Angieri committed Nov 9, 2023
1 parent a53f7c0 commit 820eac2
Show file tree
Hide file tree
Showing 2 changed files with 280 additions and 13 deletions.
293 changes: 280 additions & 13 deletions spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,283 @@
# Channel Upgradability Finite State Machines - WIP

This document is an attempt to abstract the [channel upgradability specs](https://github.com/cosmos/ibc/blob/main/spec/core/ics-004-channel-and-packet-semantics/UPGRADES.md) into finite state machines (FSMs).
This document is an attempt to abstract the [channel upgradability specs](https://github.com/cosmos/ibc/blob/main/spec/core/ics-004-channel-and-packet-semantics/UPGRADES.md) into finite state machines (FSMs). For the synopsis and motivation we refer the reader to the specs document.

## Flows

Check failure on line 5 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Headings should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:5 MD022/blanks-around-headings/blanks-around-headers Headings should be surrounded by blank lines [Expected: 1; Actual: 0; Below] [Context: "## Flows"] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md022.md
The protocol defines 3 Main possible flows:
- A starts the process and B follows.

Check failure on line 7 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Lists should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:7 MD032/blanks-around-lists Lists should be surrounded by blank lines [Context: "- A starts the process and B f..."] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md032.md
- B starts the process and A follows.
- A & B start the process (Crossing Hello).

## States

| State | ChannelState A | ChannelState B | ProvableStore A | ProvableStore B | Private Store A | Private Store B |
|---------|---------------------|---------------------|----------------------------------------------------------------|----------------------------------------------------------------|----------------------------------------|----------------------------------------|
| S0 | OPEN | OPEN | | | | |
| S1.1 | OPEN | OPEN | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet; | | | |
| S1.2 | OPEN | OPEN | | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet; | | |
| S2 | OPEN | OPEN | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet 0..1; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet 0..1; | | |
| S3.1 | FLUSHING | OPEN | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet; | | |
| S3.2 | OPEN | FLUSHING | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.VersionSet; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | | |
| S4 | FLUSHING | FLUSHING | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | Priv.Upg.CounterParty TimeoutSet 0..1; | Priv.Upg.CounterParty TimeoutSet 0..1; |
| S5.1 | FLUSHING_COMPLETE | FLUSHING | Upg.UpgradeSet; Chan.UpgradeSequenceSet; Upg.TimeoutSet; Upg.VersionSet; | Upg.UpgradeSet; Chan.UpgradeSequenceSet; Upg.TimeoutSet; Upg.VersionSet; | | Priv.Upg.CounterParty TimeoutSet; |
| S5.2 | FLUSHING | FLUSHING_COMPLETE | Upg.UpgradeSet; Chan.UpgradeSequenceSet; Upg.TimeoutSet; Upg.VersionSet; | Upg.UpgradeSet; Chan.UpgradeSequenceSet; Upg.TimeoutSet; Upg.VersionSet; | Priv.Upg.CounterParty TimeoutSet; | |
| S6 | FLUSHING_COMPLETE | FLUSHING_COMPLETE | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | | |
| S7.1 | OPEN | FLUSHING_COMPLETE | Chan.UpgradeSequenceSet; Chan.VersionSet; Chan.ConnectionHopsSet; Chan.OrderingSet; | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | | Priv.Upg.CounterParty TimeoutSet; |
| S7.2 | FLUSHING_COMPLETE | OPEN | Chan.UpgradeSequenceSet; Upg.UpgradeSet; Upg.TimeoutSet; Upg.VersionSet; | Chan.UpgradeSequenceSet; Chan.VersionSet; Chan.ConnectionHopsSet; Chan.OrderingSet; | Priv.Upg.CounterParty TimeoutSet; | |
| S8 | OPEN | OPEN | Chan.UpgradeSequenceSet; Chan.VersionSet; Chan.ConnectionHopsSet; Chan.OrderingSet; | Chan.UpgradeSequenceSet; Chan.VersionSet; Chan.ConnectionHopsSet; Chan.OrderingSet; | | |


Check failure on line 29 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Multiple consecutive blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:29 MD012/no-multiple-blanks Multiple consecutive blank lines [Expected: 1; Actual: 2] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md012.md
According to the specs the channel upgradiblity handshake protocol defines 5 subprotocols and 7 datagrams that are reproduced here for the reader's convenience.
#### Subprotocols

Check failure on line 31 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Heading levels should only increment by one level at a time

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:31 MD001/heading-increment/header-increment Heading levels should only increment by one level at a time [Expected: h3; Actual: h4] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md001.md

Check failure on line 31 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Headings should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:31 MD022/blanks-around-headings/blanks-around-headers Headings should be surrounded by blank lines [Expected: 1; Actual: 0; Above] [Context: "#### Subprotocols"] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md022.md

Check failure on line 31 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Headings should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:31 MD022/blanks-around-headings/blanks-around-headers Headings should be surrounded by blank lines [Expected: 1; Actual: 0; Below] [Context: "#### Subprotocols"] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md022.md
The channel upgradiblity handshake protocol defines the following sub-protocols: `initUpgradeHandshake`, `startFlushUpgradeHandshake`, `openUpgradeHandshake`, `cancelChannelUpgrade`, and `timeoutChannelUpgrade`.
#### Datagrams

Check failure on line 33 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Headings should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:33 MD022/blanks-around-headings/blanks-around-headers Headings should be surrounded by blank lines [Expected: 1; Actual: 0; Above] [Context: "#### Datagrams"] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md022.md

Check failure on line 33 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Headings should be surrounded by blank lines

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:33 MD022/blanks-around-headings/blanks-around-headers Headings should be surrounded by blank lines [Expected: 1; Actual: 0; Below] [Context: "#### Datagrams"] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md022.md
The datagrams exchanged between the parties during the upgrading process are __ChanUpgradeInit__, __ChanUpgradeTry__, __ChanUpgradeAck__, __ChanUpgradeConfirm__, __ChanUpgradeOpen__, __ChanUpgradeTimeout__, and __ChanUpgradeCancel__.

Check failure on line 34 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Strong style should be consistent

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:34:78 MD050/strong-style Strong style should be consistent [Expected: asterisk; Actual: underscore] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md050.md

Check failure on line 34 in spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md

View workflow job for this annotation

GitHub Actions / lint

Strong style should be consistent

spec/core/ics-004-channel-and-packet-semantics/FSM_UPGRADES.md:34:95 MD050/strong-style Strong style should be consistent [Expected: asterisk; Actual: underscore] https://github.com/DavidAnson/markdownlint/blob/v0.31.1/doc/md050.md

Every datagram may activate a subprotocol, based on the current state, the on-going flow and input.

`RestoreChannel` can be called at any point of the process and will reset the state machine execution to s0.

## Preconditions
- pc0: BothChannelEnds === OPEN

## Conditions
Below we list all the conditions that are verified during the protocol execution. In order for a state transition to occur, cX must evaluate to True.
We assume that the protocol is only executed if pc0 evaluates to True.

- c0: isAuthorizedUpgrader === True
- c1: proposedUpgradeFields.Version !==""
- c2: proposedConnection !== null && proposedConnection.state === OPEN
- c3: proposedConnection.supports(prposedUpgradeFields.ordering) === True
- c4: Upg.UpgradeSet === False
- c5: Upg.UpgradeSet === True
- c6: isCompatibleUpgradeFields === True
- c7: VerifyChannelState === True
- c8: VerifyChannelUpgrade === True
- c9: Upg.CounterParty.Sequence >= Chan.UpgSequence
- c10: Upg.TimeoutHeight !== 0 || Upg.TimeoutTimestamp !== 0
- c11: CounterPartyTimeoutNotExpired === True
- c12: PendingInflightsPacket !== True
- c13: PendingInflightsPacket === True
- c14: Priv.Upg.CounterPartyTimeoutSet === True


## Inputs

#### Enumeration
This is the list of inputs for enumeration:
- i0: A: ChanUpgradeInit --> initUpgradeHandshake
- i1: B: ChanUpgradeInit --> initUpgradeHandshake
- i2: A & B: ChanUpgradeInit --> initUpgradeHandshake
- i3: A: ChanUpgradeInit --> initUpgradeHandshake (incrementUpgradeSeq)
- i4: B: ChanUpgradeInit --> initUpgradeHandshake (incrementUpgradeSeq)
- i5: B: ChanUpgradeTry --> initUpgradeHandshake
- i6: A: ChanUpgradeTry --> initUpgradeHandshake
- i7: A: ChanUpgradeTry --> startFlushUpgradeHandshake -- i6,i7 atomic (c4)
- i8: B: ChanUpgradeTry --> startFlushUpgradeHandshake -- i5,i8 atomic (c4)
- i9: A: ChanUpgradeTry --> startFlushUpgradeHandshake (c5)
- i10: B: ChanUpgradeTry --> startFlushUpgradeHandshake (c5)
- i11: B: ChanUpgradeAck --> startFlushtUpgradeHandshake (c13)
- i12: A: ChanUpgradeAck --> startFlushtUpgradeHandshake (c13)
- i13: A: ChanUpgradeAck --> startFlushtUpgradeHandshake (c12)
- i14: B: ChanUpgradeAck --> startFlushtUpgradeHandshake (c12)
- i15: A: ChanUpgradeConfirm (c12)
- i16: B: ChanUpgradeConfirm (c12)
- i17: A: ChanUpgradeConfirm (c13)
- i18: B: ChanUpgradeConfirm (c13)
- i19: A: PacketHandler -- onlyIf i17 occurs
- i20: B: PacketHandler -- onlyIf i18 occurs
- i21: B: ChanUpgradeConfirm (c12)
- i22: A: ChanUpgradeConfirm (c12)
- i23: B: ChanUpgradeConfirm (c13)
- i24: A: ChanUpgradeConfirm (c13)
- i25: B: PacketHandler -- onlyIf i23 occurs
- i26: A: PacketHandler -- onlyIf i24 occurs
- i27: A: ChanUpgradeConfirm --> OpenUpgradeHandshake -- i22,i27 atomic
- i28: B: ChanUpgradeConfirm --> OpenUpgradeHandshake -- i21,i28 atomic
- i29: A: ChanUpgradeOpen --> OpenUpgradeHandshake
- i30: B: ChanUpgradeOpen --> OpenUpgradeHandshake
- i31: B: ChanUpgradeOpen --> OpenUpgradeHandshake
- i32: A: ChanUpgradeOpen --> OpenUpgradeHandshake

#### Inputs Parametrization

Given:

- ix: [Party, Condition, PreviosInput]: Datagram --> subprotocolActivation -- extraDetails

Each input identifier ix corresponds to a specific action, and the placeholders [Party, Condition, PreviousInput] capture who is involved in the action, any conditions that must be satisfied, and any previous input that must have occurred, respectively.

Thus we can resume the inputs as:

- i0: [Party, , ]: ChanUpgradeInit --> initUpgradeHandshake
- i1: [Party, , ]: ChanUpgradeTry --> initUpgradeHandshake
- i2: [Party, Condition, PreviousInput]: ChanUpgradeTry --> startFlushUpgradeHandshake -- atomic
- i3: [Party, Condition, ]: ChanUpgradeTry --> startFlushUpgradeHandshake
- i4: [Party, Condition, ]: ChanUpgradeAck --> startFlushtUpgradeHandshake
- i5: [Party, Condition, ]: ChanUpgradeConfirm
- i6: [Party, , PreviousInput]: PacketHandler -- onlyIf occurs
- i7: [Party, Condition, PreviousInput]: ChanUpgradeConfirm --> OpenUpgradeHandshake -- atomic
- i8: [Party, , ]: ChanUpgradeOpen --> OpenUpgradeHandshake

Below, we list the expanded representation of the protocol inputs.

- i0: [A, , ]: ChanUpgradeInit --> initUpgradeHandshake
- i0: [B, , ]: ChanUpgradeInit --> initUpgradeHandshake
- i0: [A & B, , ]: ChanUpgradeInit --> initUpgradeHandshake
- i0: [A, incrementUpgradeSeq, ]: ChanUpgradeInit --> initUpgradeHandshake
- i0: [B, incrementUpgradeSeq, ]: ChanUpgradeInit --> initUpgradeHandshake
- i1: [A, , ]: ChanUpgradeTry --> initUpgradeHandshake
- i1: [B, , ]: ChanUpgradeTry --> initUpgradeHandshake
- i2: [A, c4, i1]: ChanUpgradeTry --> startFlushUpgradeHandshake -- atomic
- i2: [B, c4, i1]: ChanUpgradeTry --> startFlushUpgradeHandshake -- atomic
- i3: [A, c5, ]: ChanUpgradeTry --> startFlushUpgradeHandshake
- i3: [B, c5, ]: ChanUpgradeTry --> startFlushUpgradeHandshake
- i4: [A, c12, ]: ChanUpgradeAck --> startFlushtUpgradeHandshake
- i4: [B, c12, ]: ChanUpgradeAck --> startFlushtUpgradeHandshake
- i4: [A, c13, ]: ChanUpgradeAck --> startFlushtUpgradeHandshake
- i4: [B, c13, ]: ChanUpgradeAck --> startFlushtUpgradeHandshake
- i5: [A, c12, ]: ChanUpgradeConfirm
- i5: [B, c12, ]: ChanUpgradeConfirm
- i5: [A, c13, ]: ChanUpgradeConfirm
- i5: [B, c13, ]: ChanUpgradeConfirm
- i6: [A, ,i5(c13)]: PacketHandler -- onlyIf occurs
- i6: [B, ,i5(c13)]: PacketHandler -- onlyIf occurs
- i7: [A, c12, i5]: ChanUpgradeConfirm --> OpenUpgradeHandshake -- atomic
- i7: [B, c12, i5]: ChanUpgradeConfirm --> OpenUpgradeHandshake -- atomic
- i8: [A, , ]: ChanUpgradeOpen --> OpenUpgradeHandshake
- i8: [B, , ]: ChanUpgradeOpen --> OpenUpgradeHandshake


[FSM](https://excalidraw.com/#json=Ts6yP_VuCZ6m7EIBA9lnl,nPWuiHw3msB4xtL7H5X5Vw)
![Picture](img_fsm/FSM_Upgrades.png)

### Admitted State Transitions WIP
Admitted state transitions are expressed as state x input x condition --> state.


- [s0] x [i0] x [c0,c1,c2,c3] -> s1.1
- [s0] x [i1] x [c0,c1,c2,c3] -> s1.2
- [s0] x [i2] x [c0,c1,c2,c3] -> s2

- [s1.1] x [i3] x [c0,c1,c2,c3] -> s1.1
- [s1.1] x [i5] x [c0,c1,c2,c3,c4] -> [s2] x [i8] x [c4,c6,c7,c8,c9,c10] -> s3.2

- [s1.2] x [i4] x [c0,c1,c2,c3] -> s1.2
- [s1.2] x [i6] x [c0,c1,c2,c3,c4] -> [s2] x [i7] x [c4,c6,c7,c8,c9,c10] -> s3.1

- [s2] x [i9] x [c5,c6,c7,c8,c9,c10c4] -> s3.1
- [s2] x [i10] x [c5,c6,c7,c8,c9,c10c4] -> s3.2



:s3.2 -> s4 -> s4 -> s5.1

s0 -> s1.1 -> s2:s3.2 -> s4 -> s5.1
s0 -> s1.1 -> s2:s3.2 -> s5.1

#### Flow 0 : A starts the process and B follows.

#### Flow 1 : B starts the process and A follows.

#### Flow 2 : A & B start the process (Crossing Hello).




# Notes

<details>
<summary>Click to expand!</summary>

The content below is not to be considered.

# IntermediateWork:

#### Inputs



// optimistically accept version that TRY chain proposes and pass this to callback for confirmation.
// in the crossing hello case, we do not modify version that our TRY call returned and instead
// enforce that both TRY calls returned the same version

[FSM_SubProtocols](https://excalidraw.com/#json=0bR7GjjkdWXnD9zvJ-bBk,3FsByRW_n1_YdWFWA679wg)
![Picture](img_fsm/FSM_SubProtocols.png)

### Description
`initUpgradeHandshake` will initialize the channel end for the upgrade handshake. It will validate the upgrade parameters and store the channel upgrade. All packet processing will continue according to the original channel parameters, as this is a signalling mechanism that can remain indefinitely. The new proposed upgrade will be stored in the provable store for counterparty verification. If it is called again before the handshake starts, then the current proposed upgrade will be replaced with the new one and the channel sequence will be incremented.

// initUpgradeHandshake will verify that the channel is in the
// correct precondition to call the initUpgradeHandshake protocol.
// it will verify the new upgrade field parameters, and make the
// relevant state changes for initializing a new upgrade:
// - store channel upgrade
// - incrementing upgrade sequence

The `initUpgradeHandshake` involves states s0;s1.1;s1.2;s2 and it is used in two datagrams, namely ChanUpgradeInit and ChanUpgradeTry. Over these datagrams exchange the protocol guarantees that a Chan.UpgradeVersion is agreed (Both Chains stores the same value on their channel end.)

For this subprotocol to be correctly executed, we require a series of state transition that starting from s0 must end in s2, regardless of the taken path.

In the picture we can see that there are 3 possible paths we could take:

- Crossing Hello (Both Chain A and Chain B start the process): In the case of Crossing Hello, we are sure that both Chains Chan.UpgradeVersion is written in s2
- Chain A starts the process : we are sure that Chain B have Chan.UpgradeVersion written in s2, but Chain A may write the Chan.UpgradeVersion on s3.1.
- Chain B starts the process : In case Chain B starts the process, then we are sure that Chain A have Chan.UpgradeVersion written in s2, but Chain B may write the Chan.UpgradeVersion on s3.2.

The difference between the three is about when the version is actually written in the state.

The protocol guarantee that on s4 both Chains A and B have the Chan.UpgradeVersion written into the channel state of their chain.

### StartFlusUpgradeHandshake

The `startFlushUpgradeHandshake` involves states s2;s3.1;s3.2;s4 and it is used in two datagrams, namely ChanUpgradeTry and ChanUpgradeAck. Over these datagrams exchange the protocol guarantees that a Upg.CounterPartyTimeout is set (Both Chains stores the counterParty value on their channel end.)

That means the protocol guarantees that on s4 both Chains have stored the counterParty Timeout.

For this subprotocol to be correctly executed, we require a series of state transition that starting from s2 must end in s4, regardless of the taken path.

Again the state when this writing to the channel end state happens actually depends on which situation we are:

- Crossing Hello (Both Chain A and Chain B start the process). s4.
- Chain A starts the process : we are sure that Chain B have UpgCounterPartyTimeout written in s3.2, but Chain A may write the Upg.CounterPartyTimeout on s4.
s3.1
- Chain B starts the process : we are sure that Chain A have Upg.CounterPartyTimeout written in s3.1, but Chain A may write the Upg.CounterPartyTimeout on s4.

### OpenUpgradeHandshake


This subprotocol will open the channel and switch the existing channel parameters to the newly agreed-upon upgrade channel fields.
ensures that all new channel information are written into the channel state on both ends and that auxiliary parameters are actually deleted from the state.

The `OpenUpgradeHandshake` involves state s6;s7.1;s7.2;s8. It is used in datagrams `ChanUpgradeOpen` and `ChanUpgradeConfirm`.

Again depending on the starting chain we may have difference times for things being written into the state.

- Crossing Hello (Both Chain A and Chain B start the process). s8.
- Chain A starts the process : we are sure that Chain B have Chan.Info written and auxiliary states deleted in s7.2, but Chain A may write the Chan.Info and deletes auxiliary states on s8.

- Chain B starts the process : we are sure that Chain A have Chan.Info written and auxiliary states deleted in s7.1, but Chain B may write the Chan.Info and deletes auxiliary states on s8.

Similarly to the Version, we can delineate when Upg.CounterPartyTimeout is guaranteed to be written by both chain in the store.

### Guaranteed States
s0,s2;s4;s8. Which means that these states conditions (which information is written) are eligible as invariants for the protocol correctness verification.

### Datagrams consideration

All the functions defined in the Upgrade Handshake protocol, peforms on-chain verification of the stored information and use a subset of the subprotocols.

In particular we have that:
Table


[InitUpgradeHandshake](
https://excalidraw.com/#json=MOyhE_n_X-lSokzJvBBT6,_dZELbWnxq6EKjQlw3-zXQ)

Idea Multi s1.1 --> s1.3 with just channel sequence that will be incremented.


## v0:

# Channel Upgradability Protocol
According to the [specs](https://github.com/cosmos/ibc/blob/main/spec/core/ics-004-channel-and-packet-semantics/UPGRADES.md#upgrade-handshake), we can model the channel upgradability protocol with 2 main flow namely, `UpgradeOk` and `UpgradeNotOk`. `UpgradeOk` can be expanded in 2 subflows namely `UpgradeOkCrossingHello` and `UpgradeOkNotCrossingHello`. `UpgradeNotOk` can be further expanded in 3 subflows namely `UpgradeCanceled`,`UpgradeExpired`, `UpgradeStaled`.
Expand Down Expand Up @@ -135,7 +412,7 @@ ChanUpgradeTry --> getChan(ChanB) :: VerifyChanBis(OPEN)

```typescript
S2 --> S3_1: (OPEN,FLUSHING) --> (FLUSHING,FLUSHING) :: R:A
ChanUpgradeAck --> getChan(ChanA):: VerifyChanAis(OPEN || FLUSHING)
ChanUpgradeAck --> getChan(ChanA):: VerifyChanAis(OPEN)
getConn(ConnB) :: ConstructCounterPartyChannelEnd(); VerifyChannelState(); VerifyChannelUpgrade()
getUpgrade(UpgA) :: VerifyIsCompatibleUpgFields()
StartFlushingUpgradeHandshake --> getChan(ChanA) :: VerifyChanAis(OPEN)
Expand Down Expand Up @@ -304,8 +581,8 @@ Notes:

![Picture](img_fsm/UpgradeOkNotCrossingHello_Conditions.png)

### Upgrade Handshake - UpgradeOkCrossingHello

### Upgrade Handshake - UpgradeOkCrossingHello

## Upgrade Handshake - UpgradeNotOk

Expand All @@ -316,16 +593,6 @@ Notes:
### Upgrade Handshake - UpgradeStaled



# Personal Notes

<details>
<summary>Click to expand!</summary>

The content below is not to be considered.

# IntermediateWork:

Outdated

## Conditions
Expand Down
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.

0 comments on commit 820eac2

Please sign in to comment.