From e3b363e3f086317d0a4ca93e2a95c4dd8139e6cf Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Tue, 1 Dec 2020 12:01:19 +0100 Subject: [PATCH 1/6] Allow overriding peer_id, height and hash in light add command (#429) * Allow overriding peer_id, height and hash in light add command * Update changelog --- CHANGELOG.md | 2 + relayer-cli/src/commands/light/add.rs | 188 +++++++++++++++----------- 2 files changed, 114 insertions(+), 76 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 95c1196dfb..e5b06f6174 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -23,6 +23,7 @@ Special thanks to external contributors for this release: @CharlyCst ([#347]). - Implement the relayer CLI for connection handshake messages ([#358], [#359], [#360]) - Implement the relayer CLI for channel handshake messages ([#371], [#372], [#373], [#374]) - Implement commands to add and list keys for a chain ([#363]) + - Allow overriding peer_id, height and hash in light add command ([#428]) - [proto-compiler] - Refactor and allow specifying a commit at which the Cosmos SDK should be checked out ([#366]) - Add a `--tag` option to the `clone-sdk` command to check out a tag instead of a commit ([#369]) @@ -48,6 +49,7 @@ Special thanks to external contributors for this release: @CharlyCst ([#347]). [#374]: https://github.com/informalsystems/ibc-rs/issues/374 [#389]: https://github.com/informalsystems/ibc-rs/issues/389 [#403]: https://github.com/informalsystems/ibc-rs/issues/403 +[#428]: https://github.com/informalsystems/ibc-rs/issues/428 [proto-compiler]: https://github.com/informalsystems/ibc-rs/tree/master/proto-compiler ### IMPROVEMENTS diff --git a/relayer-cli/src/commands/light/add.rs b/relayer-cli/src/commands/light/add.rs index 6e32be31cf..a5d3a34687 100644 --- a/relayer-cli/src/commands/light/add.rs +++ b/relayer-cli/src/commands/light/add.rs @@ -18,16 +18,16 @@ use crate::prelude::*; #[derive(Command, Debug, Options)] pub struct AddCmd { - /// RPC network address + /// RPC network address (required) #[options(free)] address: Option, - /// identifier of the chain + /// identifier of the chain (required) #[options(short = "c")] chain_id: Option, - /// Path to light client store for this peer - store_path: Option, + /// path to light client store for this peer (required) + store: Option, /// whether this is the primary peer primary: bool, @@ -37,6 +37,38 @@ pub struct AddCmd { /// skip confirmation yes: bool, + + /// override peer id (optional) + #[options(no_short)] + peer_id: Option, + + /// override height (optional) + #[options(no_short)] + height: Option, + + /// override hash (optional) + #[options(no_short)] + hash: Option, +} + +impl AddCmd { + fn cmd(&self) -> Result<(), BoxError> { + let config = (*app_config()).clone(); + let options = AddOptions::from_cmd(self).map_err(|e| format!("invalid options: {}", e))?; + + options + .validate() + .map_err(|e| format!("invalid options: {}", e))?; + + add(config, options) + } +} + +impl Runnable for AddCmd { + fn run(&self) { + self.cmd() + .unwrap_or_else(|e| fatal_error(app_reader().deref(), &*e)) + } } #[derive(Clone, Debug)] @@ -47,12 +79,21 @@ struct AddOptions { /// RPC network address address: net::Address, - /// Path to light client store for this peer - store_path: PathBuf, - /// whether this is the primary peer or not primary: bool, + /// path to light client store for this peer + store: PathBuf, + + /// override peer id + override_peer_id: Option, + + /// override height + override_height: Option, + + /// override hash + override_hash: Option, + /// allow overriding an existing peer force: bool, @@ -64,34 +105,28 @@ impl AddOptions { fn from_cmd(cmd: &AddCmd) -> Result { let chain_id = cmd.chain_id.clone().ok_or("missing chain identifier")?; let address = cmd.address.clone().ok_or("missing RPC network address")?; - let store_path = cmd.store_path.clone().ok_or("missing store path")?; - let primary = cmd.primary; - let force = cmd.force; - let yes = cmd.yes; + let store_path = cmd.store.clone().ok_or("missing store path")?; Ok(AddOptions { chain_id, address, - store_path, - primary, - force, - yes, + store: store_path, + override_peer_id: cmd.peer_id, + override_height: cmd.height, + override_hash: cmd.hash, + primary: cmd.primary, + force: cmd.force, + yes: cmd.yes, }) } fn validate(&self) -> Result<(), BoxError> { - if !self.store_path.exists() { - return Err( - format!("Store path '{}' does not exists", self.store_path.display()).into(), - ); + if !self.store.exists() { + return Err(format!("Store path '{}' does not exists", self.store.display()).into()); } - if !self.store_path.is_dir() { - return Err(format!( - "Store path '{}' is not a directory", - self.store_path.display() - ) - .into()); + if !self.store.is_dir() { + return Err(format!("Store path '{}' is not a directory", self.store.display()).into()); } Ok(()) @@ -103,8 +138,8 @@ pub struct NodeStatus { chain_id: ChainId, address: net::Address, peer_id: PeerId, - latest_hash: Hash, - latest_height: Height, + hash: Hash, + height: Height, } impl fmt::Display for NodeStatus { @@ -112,41 +147,29 @@ impl fmt::Display for NodeStatus { writeln!(f, " chain id: {}", self.chain_id)?; writeln!(f, " address: {}", self.address)?; writeln!(f, " peer id: {}", self.peer_id)?; - writeln!(f, " height: {}", self.latest_height)?; - writeln!(f, " hash: {}", self.latest_hash)?; + writeln!(f, " height: {}", self.height)?; + writeln!(f, " hash: {}", self.hash)?; Ok(()) } } -fn confirm(status: &NodeStatus, primary: bool) -> Result { - print!("Light client configuration:\n{}", status); - println!(" primary: {}", primary); - - loop { - print!("\n? Do you want to add a new light client with these trust options? (y/n) > "); - io::stdout().flush()?; // need to flush stdout since stdout is often line-buffered - - let mut choice = String::new(); - io::stdin().read_line(&mut choice)?; - - match choice.trim_end() { - "y" | "yes" => return Ok(true), - "n" | "no" => return Ok(false), - _ => continue, - } - } -} - fn add(mut config: Config, options: AddOptions) -> Result<(), BoxError> { - let status = fetch_status(options.chain_id.clone(), options.address.clone())?; + // Fetch the status from the node + let mut status = fetch_status(options.chain_id.clone(), options.address.clone())?; + + // Override the fetched status with command line arguments, if given + override_status(&mut status, &options); + // Ask the user for confirmation if --yes was not supplied if !(options.yes || confirm(&status, options.primary)?) { return Ok(()); } + // Update the in-memory configuration let new_primary = update_config(options, status.clone(), &mut config)?; + // Write the updated configuration to disk let config_path = crate::config::config_path()?; relayer::config::store(&config, config_path)?; @@ -165,18 +188,51 @@ fn fetch_status(chain_id: ChainId, address: net::Address) -> Result Result { + print!("Light client configuration:\n{}", status); + println!(" primary: {}", primary); + + loop { + print!("\n? Do you want to add a new light client with these trust options? (y/n) > "); + io::stdout().flush()?; // need to flush stdout since stdout is often line-buffered + + let mut choice = String::new(); + io::stdin().read_line(&mut choice)?; + + match choice.trim_end() { + "y" | "yes" => return Ok(true), + "n" | "no" => return Ok(false), + _ => continue, + } + } +} + fn update_config( options: AddOptions, status: NodeStatus, @@ -209,10 +265,10 @@ fn update_config( peer_id: status.peer_id, address: status.address.clone(), timeout: config::default::timeout(), - trusted_header_hash: status.latest_hash, - trusted_height: status.latest_height, + trusted_header_hash: status.hash, + trusted_height: status.height, store: StoreConfig::Disk { - path: options.store_path.join(status.peer_id.to_string()), + path: options.store.join(status.peer_id.to_string()), }, }; @@ -231,23 +287,3 @@ fn update_config( Ok(peers_config.primary) } - -impl AddCmd { - fn cmd(&self) -> Result<(), BoxError> { - let config = (*app_config()).clone(); - let options = AddOptions::from_cmd(self).map_err(|e| format!("invalid options: {}", e))?; - - options - .validate() - .map_err(|e| format!("invalid options: {}", e))?; - - add(config, options) - } -} - -impl Runnable for AddCmd { - fn run(&self) { - self.cmd() - .unwrap_or_else(|e| fatal_error(app_reader().deref(), &*e)) - } -} From be5ff322e874401b2f559946abcd50f7dd9bfd2f Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 1 Dec 2020 17:14:01 +0100 Subject: [PATCH 2/6] TLA+ for IBC Core -- ICF deliverable (#427) * receive formalized * bla * connection versions * ics04 channel handshake fixes * ics04 packet fixes and timeout handlers * ics04 packets * upated readme * links in readme * readme fixes Co-authored-by: Josef Widder --- docs/spec/relayer/tla/Chain.tla | 29 +- docs/spec/relayer/tla/IBCCore.tla | 20 +- docs/spec/relayer/tla/IBCCoreDefinitions.tla | 326 +++++++++++++----- docs/spec/relayer/tla/ICS02ClientHandlers.tla | 11 +- .../relayer/tla/ICS03ConnectionHandlers.tla | 94 ++--- .../spec/relayer/tla/ICS04ChannelHandlers.tla | 180 +++++----- docs/spec/relayer/tla/ICS04PacketHandlers.tla | 193 +++++++++-- docs/spec/relayer/tla/ICS18Relayer.tla | 217 ++++++------ docs/spec/relayer/tla/README.md | 103 +++--- 9 files changed, 751 insertions(+), 422 deletions(-) diff --git a/docs/spec/relayer/tla/Chain.tla b/docs/spec/relayer/tla/Chain.tla index 7ec400d0df..413d06e809 100644 --- a/docs/spec/relayer/tla/Chain.tla +++ b/docs/spec/relayer/tla/Chain.tla @@ -7,6 +7,7 @@ EXTENDS Integers, FiniteSets, IBCCoreDefinitions, CONSTANTS MaxHeight, \* maximal chain height ChainID, \* chain identifier ChannelOrdering, \* indicate whether the channels are ordered or unordered + MaxVersion, \* maximal connection / channel version (we assume versions are integers) MaxPacketSeq \* maximal packet sequence number VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end @@ -155,15 +156,17 @@ SendPacket == /\ LET packet == AsPacket([ sequence |-> appPacketSeq, timeoutHeight |-> MaxHeight + 1, - srcChannelID |-> GetChannelID(ChainID), - dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))]) IN + srcPortID |-> chainStore.connectionEnd.channelEnd.portID, + srcChannelID |-> chainStore.connectionEnd.channelEnd.channelID, + dstPortID |-> chainStore.connectionEnd.channelEnd.counterpartyPortID, + dstChannelID |-> chainStore.connectionEnd.channelEnd.counterpartyChannelID]) IN \* update chain store with packet committment /\ chainStore' = WritePacketCommitment(chainStore, packet) \* log sent packet - /\ packetLog' = Append(packetLog, AsPacketLogEntry( - [type |-> "PacketSent", + /\ packetLog' = Append(packetLog, AsPacketLogEntry([ + type |-> "PacketSent", srcChainID |-> ChainID, - sequence |-> packet.sequence , + sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight])) \* increase application packet sequence /\ appPacketSeq' = appPacketSeq + 1 @@ -211,11 +214,12 @@ HandleIncomingDatagrams == ***************************************************************************) \* Initial state predicate \* Initially -\* - each chain is initialized to InitChain (defined in RelayerDefinitions.tla) +\* - each chain is initialized to some element of the set +\* InitChainStores (defined in IBCCoreDefinitions.tla) \* - pendingDatagrams for each chain is empty \* - the packetSeq is set to 1 Init == - /\ chainStore = InitChainStore(ChannelOrdering) + /\ chainStore \in InitChainStore(MaxVersion, ChannelOrdering) /\ incomingDatagrams = AsSetDatagrams({}) /\ incomingPacketDatagrams = AsSeqDatagrams(<<>>) /\ history = InitHistory @@ -242,13 +246,14 @@ Fairness == Invariants ***************************************************************************) \* Type invariant -\* ChainStores and Datagrams are defined in RelayerDefinitions.tla +\* ChainStores, Datagrams, PacketLogEntries are defined in IBCCoreDefinitions.tla TypeOK == - /\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq) - /\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq) + /\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq, MaxVersion) + /\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq, MaxVersion) + /\ incomingPacketDatagrams \in Seq(Datagrams(MaxHeight, MaxPacketSeq, MaxVersion)) /\ history \in Histories /\ appPacketSeq \in 1..MaxPacketSeq - /\ packetLog \in SUBSET Packets(MaxHeight, MaxPacketSeq) + /\ packetLog \in Seq(PacketLogEntries(MaxHeight, MaxPacketSeq)) (*************************************************************************** Properties @@ -260,5 +265,5 @@ HeightDoesntDecrease == ============================================================================= \* Modification History -\* Last modified Wed Sep 30 13:47:16 CEST 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 10:40:51 CET 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/IBCCore.tla b/docs/spec/relayer/tla/IBCCore.tla index b34ce30fe2..05e3c0c697 100644 --- a/docs/spec/relayer/tla/IBCCore.tla +++ b/docs/spec/relayer/tla/IBCCore.tla @@ -4,10 +4,11 @@ This is the main module in the specification of the IBC core protocols. ***************************************************************************) -EXTENDS Integers, FiniteSets, Sequences, RelayerDefinitions +EXTENDS Integers, FiniteSets, Sequences, IBCCoreDefinitions CONSTANTS MaxHeight, \* maximal height of all the chains in the system - MaxPacketSeq, \* maximal packet sequence number (will be used later) + MaxVersion, \* maximal connection / channel version (we assume versions are integers) + MaxPacketSeq, \* maximal packet sequence number ClientDatagramsRelayer1, \* toggle generation of client datagrams for Relayer1 ClientDatagramsRelayer2, \* toggle generation of client datagrams for Relayer2 ConnectionDatagramsRelayer1, \* toggle generation of connection datagrams for Relayer1 @@ -16,21 +17,21 @@ CONSTANTS MaxHeight, \* maximal height of all the chains in the system ChannelDatagramsRelayer2, \* toggle generation of channel datagrams for Relayer2 ChannelOrdering \* indicate whether the channels are ordered or unordered -VARIABLES chainAstore, \* store of ChainA - chainBstore, \* store of ChainB - incomingDatagramsChainA, \* set of datagrams incoming to ChainA - incomingDatagramsChainB, \* set of datagrams incoming to ChainB +VARIABLES chainAstore, \* chain store of ChainA + chainBstore, \* chain store of ChainB + incomingDatagramsChainA, \* set of (client, connection, channel) datagrams incoming to ChainA + incomingDatagramsChainB, \* set of (client, connection, channel) datagrams incoming to ChainB incomingPacketDatagramsChainA, \* sequence of packet datagrams incoming to ChainA incomingPacketDatagramsChainB, \* sequence of packet datagrams incoming to ChainB relayer1Heights, \* the client heights of Relayer1 relayer2Heights, \* the client heights of Relayer2 - outgoingDatagrams, \* sets of datagrams outgoing of the relayers + outgoingDatagrams, \* sets of (client, connection, channel) datagrams outgoing of the relayers outgoingPacketDatagrams, \* sequences of packet datagrams outgoing of the relayers closeChannelA, \* flag that triggers closing of the channel end at ChainA closeChannelB, \* flag that triggers closing of the channel end at ChainB historyChainA, \* history variables for ChainA historyChainB, \* history variables for ChainB - packetLog, \* a set of packets sent by both chains + packetLog, \* packet log appPacketSeqChainA, \* packet sequence number from the application on ChainA appPacketSeqChainB \* packet sequence number from the application on ChainB @@ -332,7 +333,6 @@ ChannelCloseInv == /\ ~IsChannelTryOpen(GetChainByID("chainB")) /\ ~IsChannelOpen(GetChainByID("chainB"))) - (*************************************************************************** Invariant [IBCInv] ***************************************************************************) @@ -565,5 +565,5 @@ IBCDelivery == ============================================================================= \* Modification History -\* Last modified Fri Sep 18 18:56:16 CEST 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 10:32:04 CET 2020 by ilinastoilkovska \* Created Fri Jun 05 16:48:22 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/IBCCoreDefinitions.tla b/docs/spec/relayer/tla/IBCCoreDefinitions.tla index 56f21a14dd..7020184f78 100644 --- a/docs/spec/relayer/tla/IBCCoreDefinitions.tla +++ b/docs/spec/relayer/tla/IBCCoreDefinitions.tla @@ -17,6 +17,7 @@ UnorderedChannelEndType == state |-> STRING, order |-> STRING, channelID |-> STRING, + counterpartyPortID |-> STRING, counterpartyChannelID |-> STRING ] @@ -26,6 +27,7 @@ OrderedChannelEndType == state |-> STRING, order |-> STRING, channelID |-> STRING, + counterpartyPortID |-> STRING, counterpartyChannelID |-> STRING, nextSendSeq |-> Int, nextRcvSeq |-> Int, @@ -43,12 +45,14 @@ ConnectionEndType == clientID |-> STRING, counterpartyConnectionID |-> STRING, counterpartyClientID |-> STRING, - channelEnd |-> ChannelEndType + channelEnd |-> ChannelEndType, + versions |-> {Int} ] \* packet commitment type PacketCommitmentType == [ + portID |-> STRING, channelID |-> STRING, sequence |-> Int, timeoutHeight |-> Int @@ -57,6 +61,7 @@ PacketCommitmentType == \* packet receipt type PacketReceiptType == [ + portID |-> STRING, channelID |-> STRING, sequence |-> Int ] @@ -64,17 +69,20 @@ PacketReceiptType == \* packet acknowledgement type PacketAcknowledgementType == [ - channelID |-> STRING, + portID |-> STRING, + channelID |-> STRING, sequence |-> Int, acknowledgement |-> BOOLEAN - ] - + ] + \* packet type PacketType == [ sequence |-> Int, timeoutHeight |-> Int, + srcPortID |-> STRING, srcChainID |-> STRING, + dstPortID |-> STRING, dstChainID |-> STRING ] @@ -129,6 +137,7 @@ ConnectionDatagramType == clientID |-> STRING, counterpartyConnectionID |-> STRING, counterpartyClientID |-> STRING, + version |-> {Int}, proofHeight |-> Int, consensusHeight |-> Int ] @@ -162,7 +171,10 @@ DatagramType == counterpartyClientID |-> STRING, connectionID |-> STRING, counterpartyConnectionID |-> STRING, + version |-> {Int}, + portID |-> STRING, channelID |-> STRING, + counterpartyPortID |-> STRING, counterpartyChannelID |-> STRING, packet |-> PacketType, acknowledgement |-> BOOLEAN @@ -209,6 +221,7 @@ AsSetPacketCommitment(PC) == PC <: {PacketCommitmentType} AsPacketReceipt(pr) == pr <: PacketReceiptType AsSetPacketReceipt(PR) == PR <: {PacketReceiptType} +AsSeqPacketReceipt(PR) == PR <: Seq(PacketReceiptType) AsPacketAcknowledgement(pa) == pa <: PacketAcknowledgementType AsSetPacketAcknowledgement(PA) == PA <: {PacketAcknowledgementType} @@ -222,21 +235,20 @@ ChainIDs == {"chainA", "chainB"} ClientIDs == {"clA", "clB"} ConnectionIDs == {"connAtoB", "connBtoA"} ChannelIDs == {"chanAtoB", "chanBtoA"} +PortIDs == {"portA", "portB"} nullHeight == 0 nullClientID == "none" nullConnectionID == "none" nullChannelID == "none" +nullPortID == "none" ConnectionStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN"} ChannelStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN", "CLOSED"} ChannelOrder == {"ORDERED", "UNORDERED"} -ClientDatagramTypes == {"CreateClient", "UpdateClient"} <: {STRING} -ConnectionDatagramTypes == {"ConnOpenInit", "ConnOpenTry", "ConnOpenAck", "ConnOpenConfirm"} <: {STRING} -ChannelDatagramTypes == {"ChanOpenInit", "ChanOpenTry", "ChanOpenAck", "ChanOpenConfirm", "ChanCloseInit", "ChanCloseConfirm"} <: {STRING} - Max(S) == CHOOSE x \in S: \A y \in S: y <= x +Min(S) == CHOOSE x \in S: \A y \in S: y >= x (******************************* ChannelEnds ******************************* A set of channel end records. @@ -257,20 +269,30 @@ Max(S) == CHOOSE x \in S: \A y \in S: y <= x is going to be received, nextAckSeq -- stores the sequence number of the next packet that is going to be acknowledged. - + + - portID -- a port identifier + Stores the port identifier of this channel end. + - channelID -- a channel identifier Stores the channel identifier of this channel end. + - counterpartyPortID -- a port identifier + Stores the port identifier of the counterparty channel end. + - counterpartyChannelID -- a channel identifier Stores the channel identifier of the counterparty channel end. + + Note: we omit channel versions and connection hops. ***************************************************************************) -ChannelEnds(channelOrdering, maxPacketSeq) == +ChannelEnds(channelOrdering, maxPacketSeq, maxVersion) == IF channelOrdering = "UNORDERED" THEN \* set of unordered channels [ state : ChannelStates, order : {"UNORDERED"}, + portID : PortIDs \union {nullPortID}, channelID : ChannelIDs \union {nullChannelID}, + counterpartyPortID : PortIDs \union {nullPortID}, counterpartyChannelID : ChannelIDs \union {nullChannelID} ] <: {ChannelEndType} ELSE \* set of ordered channels @@ -280,7 +302,9 @@ ChannelEnds(channelOrdering, maxPacketSeq) == nextSendSeq : 0..maxPacketSeq, nextRcvSeq : 0..maxPacketSeq, nextAckSeq : 0..maxPacketSeq, + portID : PortIDs \union {nullPortID}, channelID : ChannelIDs \union {nullChannelID}, + counterpartyPortID : PortIDs \union {nullPortID}, counterpartyChannelID : ChannelIDs \union {nullChannelID} ] <: {ChannelEndType} @@ -290,6 +314,7 @@ ChannelEnds(channelOrdering, maxPacketSeq) == ***************************************************************************) PacketCommitments(maxHeight, maxPacketSeq) == [ + portID : PortIDs, channelID : ChannelIDs, sequence : 1..maxPacketSeq, timeoutHeight : 1..maxHeight @@ -297,12 +322,14 @@ PacketCommitments(maxHeight, maxPacketSeq) == PacketReceipts(maxPacketSeq) == [ + portID : PortIDs, channelID : ChannelIDs, sequence : 1..maxPacketSeq ] <: {PacketReceiptType} PacketAcknowledgements(maxPacketSeq) == [ + portID : PortIDs, channelID : ChannelIDs, sequence : 1..maxPacketSeq, acknowledgement : BOOLEAN @@ -327,18 +354,23 @@ PacketAcknowledgements(maxPacketSeq) == - counterpartyClientID -- a client identifier Stores the counterparty client identifier associated with this connection end. + + - versions -- a set of versions + Stores the set of supported connection versions. At the end of a handshake, + it should be a singleton set. - channelEnd : a channel end record Stores data about the channel associated with this connection end. ***************************************************************************) -ConnectionEnds(channelOrdering, maxPacketSeq) == +ConnectionEnds(channelOrdering, maxPacketSeq, maxVersion) == [ state : ConnectionStates, connectionID : ConnectionIDs \union {nullConnectionID}, - clientID : ClientIDs \union {nullClientID}, counterpartyConnectionID : ConnectionIDs \union {nullConnectionID}, - counterpartyClientID : ClientIDs \union {nullClientID}, - channelEnd : ChannelEnds(channelOrdering, maxPacketSeq) + clientID : ClientIDs \union {nullClientID}, + counterpartyClientID : ClientIDs \union {nullClientID}, + versions : SUBSET 1..maxVersion, + channelEnd : ChannelEnds(channelOrdering, maxPacketSeq, maxVersion) ] <: {ConnectionEndType} (********************************* Packets ********************************* @@ -348,7 +380,9 @@ Packets(maxHeight, maxPacketSeq) == [ sequence : 1..maxPacketSeq, timeoutHeight : 1..maxHeight, + srcPortID : PortIDs, srcChannelID : ChannelIDs, + dstPortID : PortIDs, dstChannelID : ChannelIDs ] <: {PacketType} @@ -369,7 +403,7 @@ Packets(maxHeight, maxPacketSeq) == A packet commitment is added to this set when a chain sends a packet to the counterparty - - packetCommitments : a set of packet receipts + - packetReceipts : a set of packet receipts A packet receipt is added to this set when a chain received a packet from the counterparty @@ -380,13 +414,13 @@ Packets(maxHeight, maxPacketSeq) == - packetsToAcknowledge : a sequence of packets ***************************************************************************) -ChainStores(maxHeight, channelOrdering, maxPacketSeq) == +ChainStores(maxHeight, channelOrdering, maxPacketSeq, maxVersion) == [ height : 1..maxHeight, counterpartyClientHeights : SUBSET(1..maxHeight), - connectionEnd : ConnectionEnds(channelOrdering, maxPacketSeq), + connectionEnd : ConnectionEnds(channelOrdering, maxPacketSeq, maxVersion), packetCommitments : SUBSET(PacketCommitments(maxHeight, maxPacketSeq)), - packetReceipts : SUBSET(PacketReceipts(maxPacketSeq)), + packetReceipts : SUBSET(PacketReceipts(maxPacketSeq)), packetAcknowledgements : SUBSET(PacketAcknowledgements(maxPacketSeq)), packetsToAcknowledge : Seq(Packets(maxHeight, maxPacketSeq)) ] <: {ChainStoreType} @@ -394,43 +428,112 @@ ChainStores(maxHeight, channelOrdering, maxPacketSeq) == (******************************** Datagrams ******************************** A set of datagrams. ***************************************************************************) -Datagrams(maxHeight, maxPacketSeq) == - [type : {"CreateClient"}, clientID : ClientIDs, height : 1..maxHeight] - \union - [type : {"ClientUpdate"}, clientID : ClientIDs, height : 1..maxHeight] - \union - [type : {"ConnOpenInit"}, connectionID : ConnectionIDs, clientID : ClientIDs, - counterpartyConnectionID : ConnectionIDs, counterpartyClientID : ClientIDs] - \union - [type : {"ConnOpenTry"}, connectionID : ConnectionIDs, - counterpartyConnectionID : ConnectionIDs, counterpartyClientID : ClientIDs, - clientID : ClientIDs, proofHeight : 1..maxHeight, consensusHeight : 1..maxHeight] - \union - [type : {"ConnOpenAck"}, connectionID : ConnectionIDs, proofHeight : 1..maxHeight, - consensusHeight : 1..maxHeight ] - \union - [type : {"ConnOpenConfirm"}, connectionID : ConnectionIDs, proofHeight : 1..maxHeight] - \union - [type : {"ChanOpenInit"}, channelID : ChannelIDs, counterpartyChannelID : ChannelIDs] - \union - [type : {"ChanOpenTry"}, channelID : ChannelIDs, counterpartyChannelID : ChannelIDs, - proofHeight : 1..maxHeight] - \union - [type : {"ChanOpenAck"}, channelID : ChannelIDs, proofHeight : 1..maxHeight] - \union - [type : {"ChanOpenConfirm"}, channelID : ChannelIDs, proofHeight : 1..maxHeight] - \union - [type : {"ChanCloseInit"}, channelID : ChannelIDs] - \union - [type : {"ChanCloseConfirm"}, channelID : ChannelIDs, proofHeight : 1..maxHeight] - \union - [type : {"PacketRecv"}, packet : Packets(maxHeight, maxPacketSeq), proofHeight : 1..maxHeight] - \union - [type : {"PacketAck"}, packet : Packets(maxHeight, maxPacketSeq), acknowledgement : BOOLEAN, proofHeight : 1..maxHeight] +Datagrams(maxHeight, maxPacketSeq, maxVersion) == + [ + type : {"ClientCreate"}, + clientID : ClientIDs, + height : 1..maxHeight + ] \union [ + type : {"ClientUpdate"}, + clientID : ClientIDs, + height : 1..maxHeight + ] \union [ + type : {"ConnOpenInit"}, + connectionID : ConnectionIDs, + counterpartyConnectionID : ConnectionIDs, + clientID : ClientIDs, + counterpartyClientID : ClientIDs + ] \union [ + type : {"ConnOpenTry"}, + desiredConnectionID : ConnectionIDs, + counterpartyConnectionID : ConnectionIDs, + clientID : ClientIDs, + counterpartyClientID : ClientIDs, + versions : SUBSET 1..maxVersion, + proofHeight : 1..maxHeight, + consensusHeight : 1..maxHeight + ] \union [ + type : {"ConnOpenAck"}, + connectionID : ConnectionIDs, + proofHeight : 1..maxHeight, + consensusHeight : 1..maxHeight + ] \union [ + type : {"ConnOpenConfirm"}, + connectionID : ConnectionIDs, + proofHeight : 1..maxHeight + ] \union [ + type : {"ChanOpenInit"}, + portID : PortIDs, + channelID : ChannelIDs, + counterpartyPortID : PortIDs, + counterpartyChannelID : ChannelIDs + ] \union [ + type : {"ChanOpenTry"}, + portID : PortIDs, + channelID : ChannelIDs, + counterpartyPortID : PortIDs, + counterpartyChannelID : ChannelIDs, + proofHeight : 1..maxHeight + ] \union [ + type : {"ChanOpenAck"}, + portID : PortIDs, + channelID : ChannelIDs, + proofHeight : 1..maxHeight + ] \union [ + type : {"ChanOpenConfirm"}, + portID : PortIDs, + channelID : ChannelIDs, + proofHeight : 1..maxHeight + ] \union [ + type : {"ChanCloseInit"}, + portID : PortIDs, + channelID : ChannelIDs + ] \union [ + type : {"ChanCloseConfirm"}, + portID : PortIDs, + channelID : ChannelIDs, + proofHeight : 1..maxHeight + ] \union [ + type : {"PacketRecv"}, + packet : Packets(maxHeight, maxPacketSeq), + proofHeight : 1..maxHeight + ] \union [ + type : {"PacketAck"}, + packet : Packets(maxHeight, maxPacketSeq), + acknowledgement : BOOLEAN, + proofHeight : 1..maxHeight + ] <: {DatagramType} NullDatagram == [type |-> "null"] <: DatagramType + +(**************************** PacketLogEntries ***************************** + A set of packet log entries. + ***************************************************************************) +PacketLogEntries(maxHeight, maxPacketSeq) == + [ + type : {"PacketSent"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + timeoutHeight : 1..maxHeight + ] \union [ + type : {"PacketRecv"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + portID : PortIDs, + channelID : ChannelIDs, + timeoutHeight : 1..maxHeight + ] \union [ + type : {"WriteAck"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + portID : PortIDs, + channelID : ChannelIDs, + timeoutHeight : 1..maxHeight, + acknowledgement : BOOLEAN + ] + <: {PacketLogEntryType} NullPacketLogEntry == [type |-> "null"] <: PacketLogEntryType @@ -444,7 +547,8 @@ Histories == chanTryOpen : BOOLEAN, chanOpen : BOOLEAN, chanClosed : BOOLEAN - ] <: {HistoryType} + ] + <: {HistoryType} (*************************************************************************** Initial values of a channel end, connection end, chain @@ -452,61 +556,79 @@ Histories == \* Initial value of an unordered channel end: \* - state is "UNINIT" \* - order is "UNORDERED" -\* - channelID, counterpartyChannelID are uninitialized +\* - channelID, counterpartyPortID, counterpartyChannelID are uninitialized InitUnorderedChannelEnd == - [state |-> "UNINIT", - order |-> "UNORDERED", - channelID |-> nullChannelID, - counterpartyChannelID |-> nullChannelID] <: ChannelEndType + [ + state |-> "UNINIT", + order |-> "UNORDERED", + portID |-> nullPortID, + channelID |-> nullChannelID, + counterpartyPortID |-> nullPortID, + counterpartyChannelID |-> nullChannelID + ] \* Initial value of an ordered channel end: \* - state is "UNINIT" \* - order is "ORDERED" \* - nextSendSeq, nextRcvSeq, nextAckSeq are set to 0 -\* - channelID, counterpartyChannelID are uninitialized +\* - channelID, counterpartyPortID, counterpartyChannelID are uninitialized InitOrderedChannelEnd == - [state |-> "UNINIT", - order |-> "ORDERED", - nextSendSeq |-> 0, - nextRcvSeq |-> 0, - nextAckSeq |-> 0, - channelID |-> nullChannelID, - counterpartyChannelID |-> nullChannelID] <: ChannelEndType + [ + state |-> "UNINIT", + order |-> "ORDERED", + nextSendSeq |-> 0, + nextRcvSeq |-> 0, + nextAckSeq |-> 0, + portID |-> nullPortID, + channelID |-> nullChannelID, + counterpartyPortID |-> nullPortID, + counterpartyChannelID |-> nullChannelID + ] \* Initial value of a connection end: \* - state is "UNINIT" \* - connectionID, counterpartyConnectionID are uninitialized -\* - clientID, counterpartyClientID are uninitialized +\* - clientID, counterpartyClientID are uninitialized +\* - versions is an arbitrary subset of the set {1, .., maxVersion} \* - channelEnd is initialized based on channelOrdering -InitConnectionEnd(channelOrdering) == +InitConnectionEnds(maxVersion, channelOrdering) == IF channelOrdering = "ORDERED" - THEN [state |-> "UNINIT", - connectionID |-> nullConnectionID, - clientID |-> nullClientID, - counterpartyConnectionID |-> nullConnectionID, - counterpartyClientID |-> nullClientID, - channelEnd |-> InitOrderedChannelEnd] - ELSE [state |-> "UNINIT", - connectionID |-> nullConnectionID, - clientID |-> nullClientID, - counterpartyConnectionID |-> nullConnectionID, - counterpartyClientID |-> nullClientID, - channelEnd |-> InitUnorderedChannelEnd] - <: ConnectionEndType + THEN [ + state : {"UNINIT"}, + connectionID : {nullConnectionID}, + clientID : {nullClientID}, + counterpartyConnectionID : {nullConnectionID}, + counterpartyClientID : {nullClientID}, + versions : (SUBSET 1..maxVersion) \ {{}}, + channelEnd : {InitOrderedChannelEnd} + ] + ELSE [ + state : {"UNINIT"}, + connectionID : {nullConnectionID}, + clientID : {nullClientID}, + counterpartyConnectionID : {nullConnectionID}, + counterpartyClientID : {nullClientID}, + versions : (SUBSET 1..maxVersion) \ {{}}, + channelEnd : {InitUnorderedChannelEnd} + ] \* Initial value of the chain store: \* - height is initialized to 1 \* - the counterparty light client is uninitialized \* - the connection end is initialized to InitConnectionEnd -InitChainStore(channelOrdering) == - [height |-> 1, - counterpartyClientHeights |-> AsSetInt({}), - connectionEnd |-> InitConnectionEnd(channelOrdering), - packetCommitments |-> AsSetPacketCommitment({}), - packetReceipts |-> AsSetPacketReceipt({}), - packetAcknowledgements |-> AsSetPacketAcknowledgement({}), - packetsToAcknowledge |-> AsSeqPacket(<<>>) - ] <: ChainStoreType +InitChainStore(maxVersion, channelOrdering) == + [ + height : {1}, + counterpartyClientHeights : {AsSetInt({})}, + connectionEnd : InitConnectionEnds(maxVersion, channelOrdering), + + packetCommitments : {AsSetPacketCommitment({})}, + packetReceipts : {AsSetPacketReceipt({})}, + packetAcknowledgements : {AsSetPacketAcknowledgement({})}, + packetsToAcknowledge : {AsSeqPacket(<<>>)} + + ] + <: {ChainStoreType} \* Initial value of history flags @@ -582,6 +704,14 @@ GetCounterpartyConnectionID(chainID) == \* get the connection end at chainID GetConnectionEnd(chain) == AsConnectionEnd(chain.connectionEnd) + +\* pick the minimal version from a set of versions +PickVersion(versions) == + IF versions /= AsSetInt({}) + THEN LET minVersion == Min(versions) IN + {minVersion} + ELSE AsSetInt({}) + \* returns true if the connection end on chainID is UNINIT IsConnectionUninit(chain) == @@ -618,6 +748,22 @@ GetCounterpartyChannelID(chainID) == ELSE IF chainID = "chainB" THEN AsID("chanAtoB") ELSE AsID(nullChannelID) + +\* get the port ID at chainID +GetPortID(chainID) == + IF chainID = "chainA" + THEN AsID("portA") + ELSE IF chainID = "chainB" + THEN AsID("portB") + ELSE AsID(nullPortID) + +\* get the port ID at chainID's counterparty chain +GetCounterpartyPortID(chainID) == + IF chainID = "chainA" + THEN AsID("portB") + ELSE IF chainID = "chainB" + THEN AsID("portA") + ELSE AsID(nullPortID) \* get the channel end at the connection end of chainID GetChannelEnd(chain) == @@ -645,5 +791,5 @@ IsChannelClosed(chain) == ============================================================================= \* Modification History -\* Last modified Wed Sep 30 13:32:32 CEST 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 10:41:22 CET 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska \ No newline at end of file diff --git a/docs/spec/relayer/tla/ICS02ClientHandlers.tla b/docs/spec/relayer/tla/ICS02ClientHandlers.tla index fcdefe7a7c..0f4cd9574c 100644 --- a/docs/spec/relayer/tla/ICS02ClientHandlers.tla +++ b/docs/spec/relayer/tla/ICS02ClientHandlers.tla @@ -1,21 +1,16 @@ --------------------------- MODULE ClientHandlers --------------------------- +----------------------- MODULE ICS02ClientHandlers ------------------------- (*************************************************************************** This module contains definitions of operators that are used to handle client datagrams ***************************************************************************) -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, IBCCoreDefinitions (*************************************************************************** Client datagram handlers ***************************************************************************) -\* client heights: -\* good version: add all client heights from datagrams to counterpartyClientHeights -\* bad version: add only Max of client heights from datagrams to counterpartyClientHeights -\* if Max > Max(counterpartyClientHeights) - \* Handle "CreateClient" datagrams HandleCreateClient(chainID, chain, datagrams) == \* get "CreateClient" datagrams with valid clientID @@ -76,5 +71,5 @@ HandleClientUpdate(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Thu Sep 10 15:43:27 CEST 2020 by ilinastoilkovska +\* Last modified Thu Nov 26 17:40:19 CET 2020 by ilinastoilkovska \* Created Tue Apr 07 16:42:47 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla b/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla index 765ec4178c..b90f919abd 100644 --- a/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla +++ b/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla @@ -1,11 +1,11 @@ -------------------------- MODULE ConnectionHandlers ------------------------- +---------------------- MODULE ICS03ConnectionHandlers ---------------------- (*************************************************************************** This module contains definitions of operators that are used to handle connection datagrams ***************************************************************************) -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, IBCCoreDefinitions (*************************************************************************** Connection datagram handlers @@ -26,9 +26,10 @@ HandleConnOpenInit(chainID, chain, datagrams) == LET connOpenInitConnectionEnd == AsConnectionEnd([ state |-> "INIT", connectionID |-> connOpenInitDgr.connectionID, - clientID |-> connOpenInitDgr.clientID, counterpartyConnectionID |-> connOpenInitDgr.counterpartyConnectionID, + clientID |-> connOpenInitDgr.clientID, counterpartyClientID |-> connOpenInitDgr.counterpartyClientID, + versions |-> chain.connectionEnd.versions, channelEnd |-> chain.connectionEnd.channelEnd ]) IN LET connOpenInitChain == AsChainStore([ @@ -46,102 +47,117 @@ HandleConnOpenTry(chainID, chain, datagrams) == \* get "ConnOpenTry" datagrams, with a valid connection ID and valid height LET connOpenTryDgrs == {dgr \in datagrams : /\ dgr.type = "ConnOpenTry" - /\ dgr.connectionID = GetConnectionID(chainID) + /\ dgr.desiredConnectionID = GetConnectionID(chainID) /\ dgr.consensusHeight <= chain.height /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF connOpenTryDgrs /= AsSetDatagrams({}) \* if there are valid "ConnOpenTry" datagrams, update the connection end THEN LET connOpenTryDgr == CHOOSE dgr \in connOpenTryDgrs : TRUE IN - LET connOpenTryConnectionEnd == AsConnectionEnd([ + LET versionIntersection == chain.connectionEnd.versions \intersect connOpenTryDgr.versions IN + + \* if the versions from the datagram overlap with the supported versions of the connnection end + IF /\ versionIntersection /= AsSetInt({}) + \* if the connection end is uninitialized + /\ \/ chain.connectionEnd.state = "UNINIT" + \* of if it is initialized, and all fields match the datagram fields + \/ /\ chain.connectionEnd.state = "INIT" + /\ chain.connectionEnd.connectionID + = connOpenTryDgr.desiredConnectionID + /\ chain.connectionEnd.counterpartyConnectionID + = connOpenTryDgr.counterpartyConnectionID + /\ chain.connectionEnd.clientID + = connOpenTryDgr.clientID + /\ chain.connectionEnd.counterpartyClientID + = connOpenTryDgr.counterpartyClientID + \* update the connection end in the chain store + THEN LET connOpenTryConnectionEnd == AsConnectionEnd([ state |-> "TRYOPEN", - connectionID |-> connOpenTryDgr.connectionID, - clientID |-> connOpenTryDgr.clientID, + connectionID |-> connOpenTryDgr.desiredConnectionID, counterpartyConnectionID |-> connOpenTryDgr.counterpartyConnectionID, + clientID |-> connOpenTryDgr.clientID, counterpartyClientID |-> connOpenTryDgr.counterpartyClientID, + versions |-> PickVersion(versionIntersection), channelEnd |-> chain.connectionEnd.channelEnd ]) IN - - IF \/ chain.connectionEnd.state = "UNINIT" - \/ /\ chain.connectionEnd.state = "INIT" - /\ chain.connectionEnd.counterpartyConnectionID - = connOpenTryConnectionEnd.counterpartyConnectionID - /\ chain.connectionEnd.clientID - = connOpenTryConnectionEnd.clientID - /\ chain.connectionEnd.counterpartyClientID - = connOpenTryConnectionEnd.counterpartyClientID - \* if the connection end on the chain is in "UNINIT" or it is in "INIT", - \* but the fields are the same as in the datagram, update the connection end - THEN LET connOpenTryChain == AsChainStore([ + LET connOpenTryChain == AsChainStore([ chain EXCEPT !.connectionEnd = connOpenTryConnectionEnd ]) IN connOpenTryChain - \* otherwise, do not update the chain store - ELSE chain + \* otherwise, do not update the chain store + ELSE chain ELSE chain \* Handle "ConnOpenAck" datagrams HandleConnOpenAck(chainID, chain, datagrams) == + \* get existing connection end + LET connectionEnd == chain.connectionEnd IN \* get "ConnOpenAck" datagrams, with a valid connection ID and valid height LET connOpenAckDgrs == {dgr \in datagrams : /\ dgr.type = "ConnOpenAck" - /\ dgr.connectionID = GetConnectionID(chainID) + /\ dgr.connectionID = connectionEnd.connectionID /\ dgr.consensusHeight <= chain.height /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - IF connOpenAckDgrs /= AsSetDatagrams({}) \* if there are valid "ConnOpenAck" datagrams, update the connection end - THEN IF \/ chain.connectionEnd.state = "INIT" - \/ chain.connectionEnd.state = "TRYOPEN" - \* if the connection end on the chain is in "INIT" or it is in "TRYOPEN", + IF connOpenAckDgrs /= AsSetDatagrams({}) + THEN LET connOpenAckDgr == CHOOSE dgr \in connOpenAckDgrs : TRUE IN + \* if the connection end on the chain is in "INIT" and the version set + \* from the datagram is a subset of the supported versions in the connection end + IF \/ /\ connectionEnd.state = "INIT" + /\ connOpenAckDgr.versions \subseteq connectionEnd.versions + \* or the connection end is in "TRYOPEN" and the version set + \* from the datagram is equal to the version set in the connection end + \/ /\ connectionEnd.state = "TRYOPEN" + /\ connOpenAckDgr.versions = connectionEnd.versions \* update the connection end - THEN LET connOpenAckDgr == CHOOSE dgr \in connOpenAckDgrs : TRUE IN - LET connOpenAckConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.state = "OPEN", - !.connectionID = connOpenAckDgr.connectionID + THEN LET connOpenAckConnectionEnd == AsConnectionEnd([ + connectionEnd EXCEPT !.state = "OPEN", + !.versions = connOpenAckDgr.versions ]) IN LET connOpenAckChain == AsChainStore([ chain EXCEPT !.connectionEnd = connOpenAckConnectionEnd ]) IN connOpenAckChain - \* otherwise, do not update the chain store - ELSE chain + \* otherwise, do not update the chain store + ELSE chain ELSE chain \* Handle "ConnOpenConfirm" datagrams HandleConnOpenConfirm(chainID, chain, datagrams) == + \* get existing connection end + LET connectionEnd == chain.connectionEnd IN \* get "ConnOpenConfirm" datagrams, with a valid connection ID and valid height LET connOpenConfirmDgrs == {dgr \in datagrams : /\ dgr.type = "ConnOpenConfirm" - /\ dgr.connectionID = GetConnectionID(chainID) + /\ dgr.connectionID = connectionEnd.connectionID /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF connOpenConfirmDgrs /= AsSetDatagrams({}) \* if there are valid "connOpenConfirmDgrs" datagrams, update the connection end - THEN IF chain.connectionEnd.state = "TRYOPEN" + THEN IF connectionEnd.state = "TRYOPEN" \* if the connection end on the chain is in "TRYOPEN", update the connection end THEN LET connOpenConfirmDgr == CHOOSE dgr \in connOpenConfirmDgrs : TRUE IN LET connOpenConfirmConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.state = "OPEN", - !.connectionID = connOpenConfirmDgr.connectionID + connectionEnd EXCEPT !.state = "OPEN" ]) IN LET connOpenConfirmChain == AsChainStore([ chain EXCEPT !.connectionEnd = connOpenConfirmConnectionEnd ]) IN connOpenConfirmChain - \* otherwise, do not update the chain store - ELSE chain + \* otherwise, do not update the chain store + ELSE chain ELSE chain ============================================================================= \* Modification History -\* Last modified Wed Sep 09 14:21:25 CEST 2020 by ilinastoilkovska +\* Last modified Mon Nov 30 13:56:55 CET 2020 by ilinastoilkovska \* Created Tue Apr 07 16:09:26 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/ICS04ChannelHandlers.tla b/docs/spec/relayer/tla/ICS04ChannelHandlers.tla index fb06267ea5..d2850f7363 100644 --- a/docs/spec/relayer/tla/ICS04ChannelHandlers.tla +++ b/docs/spec/relayer/tla/ICS04ChannelHandlers.tla @@ -1,11 +1,11 @@ --------------------------- MODULE ChannelHandlers -------------------------- +------------------------ MODULE ICS04ChannelHandlers ----------------------- (*************************************************************************** This module contains definitions of operators that are used to handle channel datagrams ***************************************************************************) -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, IBCCoreDefinitions (*************************************************************************** Channel datagram handlers @@ -13,121 +13,140 @@ EXTENDS Integers, FiniteSets, RelayerDefinitions \* Handle "ChanOpenInit" datagrams HandleChanOpenInit(chainID, chain, datagrams) == - \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN - \* get "ChanOpenInit" datagrams, with a valid channel ID + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN + \* get "ChanOpenInit" datagrams, with a valid port and channel ID LET chanOpenInitDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenInit" + /\ dgr.portID = GetPortID(chainID) /\ dgr.channelID = GetChannelID(chainID)} IN \* if there are valid "ChanOpenInit" datagrams and the connection is not "UNINIT", \* initialize the channel end and update the chain IF /\ chanOpenInitDgrs /= AsSetDatagrams({}) - /\ chain.connectionEnd.state /= "UNINIT" - /\ channelEnd.state = "UNINIT" + /\ connectionEnd.state /= "UNINIT" + /\ connectionEnd.channelEnd.state = "UNINIT" THEN LET chanOpenInitDgr == CHOOSE dgr \in chanOpenInitDgrs : TRUE IN LET chanOpenInitChannelEnd == - IF channelEnd.order = "ORDERED" - THEN AsChannelEnd([channelEnd EXCEPT - !.state = "INIT", - !.channelID = chanOpenInitDgr.channelID, - !.counterpartyChannelID = chanOpenInitDgr.counterpartyChannelID, - !.nextSendSeq = 1, - !.nextRcvSeq = 1, - !.nextAckSeq = 1 + IF connectionEnd.channelEnd.order = "ORDERED" + THEN AsChannelEnd([ + state |-> "INIT", + order |-> "ORDERED", + nextSendSeq |-> 1, + nextRcvSeq |-> 1, + nextAckSeq |-> 1, + portID |-> chanOpenInitDgr.portID, + channelID |-> chanOpenInitDgr.channelID, + counterpartyPortID |-> chanOpenInitDgr.counterpartyPortID, + counterpartyChannelID |-> chanOpenInitDgr.counterpartyChannelID ]) - ELSE AsChannelEnd([channelEnd EXCEPT - !.state = "INIT", - !.channelID = chanOpenInitDgr.channelID, - !.counterpartyChannelID = chanOpenInitDgr.counterpartyChannelID + ELSE AsChannelEnd([ + state |-> "INIT", + order |-> "UNORDERED", + portID |-> chanOpenInitDgr.portID, + channelID |-> chanOpenInitDgr.channelID, + counterpartyPortID |-> chanOpenInitDgr.counterpartyPortID, + counterpartyChannelID |-> chanOpenInitDgr.counterpartyChannelID ]) IN LET chanOpenInitConnectionEnd == AsConnectionEnd([ chain.connectionEnd EXCEPT !.channelEnd = chanOpenInitChannelEnd ]) IN LET chanOpenInitChain == AsChainStore([ - chain EXCEPT !.connectionEnd = chanOpenInitConnectionEnd + chain EXCEPT !.connectionEnd = chanOpenInitConnectionEnd ]) IN chanOpenInitChain + \* otherwise, do not update the chain store ELSE chain \* Handle "ChanOpenTry" datagrams HandleChanOpenTry(chainID, chain, datagrams) == - \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN - \* get "ChanOpenTry" datagrams, with a valid channel ID + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN + \* get "ChanOpenTry" datagrams, with a valid port and channel ID LET chanOpenTryDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenTry" + /\ dgr.portID = GetPortID(chainID) /\ dgr.channelID = GetChannelID(chainID) /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN \* if there are valid "ChanOpenTry" datagrams and the connection is "OPEN", \* update the channel end IF /\ chanOpenTryDgrs /= AsSetDatagrams({}) - /\ chain.connectionEnd.state = "OPEN" + /\ chain.connectionEnd = "OPEN" THEN LET chanOpenTryDgr == CHOOSE dgr \in chanOpenTryDgrs : TRUE IN - LET chanOpenTryChannelEnd == - IF channelEnd.order = "ORDERED" - THEN AsChannelEnd([channelEnd EXCEPT - !.state = "TRYOPEN", - !.channelID = chanOpenTryDgr.channelID, - !.counterpartyChannelID = chanOpenTryDgr.counterpartyChannelID, - !.nextSendSeq = 1, - !.nextRcvSeq = 1, - !.nextAckSeq = 1 + \* if the channel end is uninitialized + IF \/ connectionEnd.channelEnd.state = "UNINIT" + \* of if it is initialized, and all fields match the datagram fields + \/ /\ connectionEnd.channelEnd.state = "INIT" + /\ connectionEnd.channelEnd.counterpartyPortID + = chanOpenTryDgr.counterpartyPortID + /\ connectionEnd.channelEnd.counterpartyChannelID + = chanOpenTryDgr.counterpartyChannelID + \* update the channel end in the chain store + THEN LET chanOpenTryChannelEnd == + IF connectionEnd.channelEnd.order = "ORDERED" + THEN AsChannelEnd([ + state |-> "TRYOPEN", + order |-> "ORDERED", + nextSendSeq |-> 1, + nextRcvSeq |-> 1, + nextAckSeq |-> 1, + portID |-> chanOpenTryDgr.portID, + channelID |-> chanOpenTryDgr.channelID, + counterpartyPortID |-> chanOpenTryDgr.counterpartyPortID, + counterpartyChannelID |-> chanOpenTryDgr.counterpartyChannelID ]) - ELSE AsChannelEnd([channelEnd EXCEPT - !.state = "TRYOPEN", - !.channelID = chanOpenTryDgr.channelID, - !.counterpartyChannelID = chanOpenTryDgr.counterpartyChannelID + ELSE AsChannelEnd([ + state |-> "TRYOPEN", + order |-> "UNORDERED", + portID |-> chanOpenTryDgr.portID, + channelID |-> chanOpenTryDgr.channelID, + counterpartyPortID |-> chanOpenTryDgr.counterpartyPortID, + counterpartyChannelID |-> chanOpenTryDgr.counterpartyChannelID ]) IN - IF \/ channelEnd.state = "UNINIT" - \/ /\ channelEnd.state = "INIT" - /\ channelEnd.counterpartyChannelID - = chanOpenTryChannelEnd.counterpartyChannelID - \* if the channel end on the chain is in "UNINIT" or it is in "INIT", - \* but the fields are the same as in the datagram, update the channel end - THEN LET chanOpenTryConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.channelEnd = chanOpenTryChannelEnd + LET chanOpenTryConnectionEnd == AsConnectionEnd([ + connectionEnd EXCEPT !.channelEnd = chanOpenTryChannelEnd ]) IN + LET chanOpenTryChain == AsChainStore([ chain EXCEPT !.connectionEnd = chanOpenTryConnectionEnd ]) IN chanOpenTryChain - \* otherwise, do not update the chain store + \* otherwise, do not update the chain store ELSE chain - \* otherwise, do not update the chain store ELSE chain \* Handle "ChanOpenAck" datagrams HandleChanOpenAck(chainID, chain, datagrams) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN + LET channelEnd == connectionEnd.channelEnd IN \* get "ChanOpenAck" datagrams, with a valid channel ID LET chanOpenAckDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenAck" - /\ dgr.channelID = GetChannelID(chainID) + /\ dgr.portID = channelEnd.portID + /\ dgr.channelID = channelEnd.channelID /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN \* if there are valid "ChanOpenAck" datagrams, update the channel end IF /\ chanOpenAckDgrs /= AsSetDatagrams({}) - /\ chain.connectionEnd.state = "OPEN" + /\ connectionEnd.state = "OPEN" THEN \* if the channel end on the chain is in "INIT" or it is in "TRYOPEN", \* update the channel end IF \/ channelEnd.state = "INIT" \/ channelEnd.state = "TRYOPEN" THEN LET chanOpenAckDgr == CHOOSE dgr \in chanOpenAckDgrs : TRUE IN LET chanOpenAckChannelEnd == AsChannelEnd([ - channelEnd EXCEPT - !.state = "OPEN", - !.channelID = chanOpenAckDgr.channelID + channelEnd EXCEPT !.state = "OPEN" ]) IN LET chanOpenAckConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.channelEnd = chanOpenAckChannelEnd + connectionEnd EXCEPT !.channelEnd = chanOpenAckChannelEnd ]) IN LET chanOpenAckChain == AsChainStore([ chain EXCEPT !.connectionEnd = chanOpenAckConnectionEnd @@ -135,109 +154,116 @@ HandleChanOpenAck(chainID, chain, datagrams) == chanOpenAckChain - \* otherwise, do not update the chain store + \* otherwise, do not update the chain store ELSE chain - \* otherwise, do not update the chain store ELSE chain \* Handle "ChanOpenConfirm" datagrams HandleChanOpenConfirm(chainID, chain, datagrams) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN + LET channelEnd == connectionEnd.channelEnd IN \* get "ChanOpenConfirm" datagrams, with a valid channel ID LET chanOpenConfirmDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenConfirm" - /\ dgr.channelID = GetChannelID(chainID) + /\ dgr.portID = channelEnd.portID + /\ dgr.channelID = channelEnd.channelID /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN \* if there are valid "ChanOpenConfirm" datagrams, update the channel end IF /\ chanOpenConfirmDgrs /= AsSetDatagrams({}) - /\ chain.connectionEnd.state = "OPEN" + /\ connectionEnd.state = "OPEN" THEN \* if the channel end on the chain is in "TRYOPEN", update the channel end IF channelEnd.state = "TRYOPEN" THEN LET chanOpenConfirmDgr == CHOOSE dgr \in chanOpenConfirmDgrs : TRUE IN LET chanOpenConfirmChannelEnd == AsChannelEnd([ - channelEnd EXCEPT - !.state = "OPEN", - !.channelID = chanOpenConfirmDgr.channelID + channelEnd EXCEPT !.state = "OPEN" ]) IN LET chanOpenConfirmConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.channelEnd = chanOpenConfirmChannelEnd + connectionEnd EXCEPT !.channelEnd = chanOpenConfirmChannelEnd ]) IN LET chanOpenConfirmChain == AsChainStore([ chain EXCEPT !.connectionEnd = chanOpenConfirmConnectionEnd ]) IN chanOpenConfirmChain - \* otherwise, do not update the chain store - - ELSE chain + \* otherwise, do not update the chain store + ELSE chain ELSE chain \* Handle "ChanCloseInit" datagrams HandleChanCloseInit(chainID, chain, datagrams) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN + LET channelEnd == connectionEnd.channelEnd IN \* get "ChanCloseInit" datagrams, with a valid channel ID LET chanCloseInitDgrs == {dgr \in datagrams : /\ dgr.type = "ChanCloseInit" - /\ dgr.channelID = GetChannelID(chainID)} IN + /\ dgr.portID = channelEnd.portID + /\ dgr.channelID = channelEnd.channelID} IN \* if there are valid "ChanCloseInit" datagrams IF /\ chanCloseInitDgrs /= AsSetDatagrams({}) \* and the channel end is neither UNINIT nor CLOSED /\ channelEnd.state \notin {"UNINIT", "CLOSED"} \* and the connection end is OPEN - /\ chain.connectionEnd.state = "OPEN" + /\ connectionEnd.state = "OPEN" THEN \* then close the channel end LET chanCloseInitChannelEnd == AsChannelEnd([ channelEnd EXCEPT !.state = "CLOSED" ]) IN LET chanCloseInitConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.channelEnd = chanCloseInitChannelEnd + connectionEnd EXCEPT !.channelEnd = chanCloseInitChannelEnd ]) IN LET chanCloseInitChain == AsChainStore([ chain EXCEPT !.connectionEnd = chanCloseInitConnectionEnd ]) IN chanCloseInitChain + \* otherwise, do not update the chain store ELSE chain \* Handle "ChanCloseConfirm" datagrams HandleChanCloseConfirm(chainID, chain, datagrams) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN + LET channelEnd == connectionEnd.channelEnd IN \* get "ChanCloseConfirm" datagrams, with a valid channel ID LET chanCloseConfirmDgrs == {dgr \in datagrams : - /\ dgr.type = "ChanCloseConfirm" - /\ dgr.channelID = GetChannelID(chainID) - /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN + /\ dgr.type = "ChanCloseConfirm" + /\ dgr.portID = channelEnd.portID + /\ dgr.channelID = channelEnd.channelID + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN \* if there are valid "ChanCloseConfirm" datagrams IF /\ chanCloseConfirmDgrs /= AsSetDatagrams({}) \* and the channel end is neither UNINIT nor CLOSED /\ channelEnd.state \notin {"UNINIT", "CLOSED"} \* and the connection end is OPEN - /\ chain.connectionEnd.state = "OPEN" + /\ connectionEnd.state = "OPEN" THEN \* then close the channel end LET chanCloseConfirmChannelEnd == AsChannelEnd([ channelEnd EXCEPT !.state = "CLOSED" ]) IN LET chanCloseConfirmConnectionEnd == AsConnectionEnd([ - chain.connectionEnd EXCEPT !.channelEnd = chanCloseConfirmChannelEnd + connectionEnd EXCEPT !.channelEnd = chanCloseConfirmChannelEnd ]) IN LET chanCloseConfirmChain == AsChainStore([ chain EXCEPT !.connectionEnd = chanCloseConfirmConnectionEnd ]) IN chanCloseConfirmChain + \* otherwise, do not update the chain store ELSE chain ============================================================================= \* Modification History -\* Last modified Thu Sep 10 15:43:25 CEST 2020 by ilinastoilkovska +\* Last modified Mon Nov 30 13:59:29 CET 2020 by ilinastoilkovska \* Created Tue Apr 07 16:58:02 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/ICS04PacketHandlers.tla b/docs/spec/relayer/tla/ICS04PacketHandlers.tla index 05eeab42a7..49040c1131 100644 --- a/docs/spec/relayer/tla/ICS04PacketHandlers.tla +++ b/docs/spec/relayer/tla/ICS04PacketHandlers.tla @@ -1,11 +1,11 @@ ---------------------------- MODULE PacketHandlers --------------------------- +------------------------ MODULE ICS04PacketHandlers ------------------------ (*************************************************************************** This module contains definitions of operators that are used to handle packet datagrams ***************************************************************************) -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, Sequences, IBCCoreDefinitions (*************************************************************************** Packet datagram handlers @@ -16,42 +16,48 @@ HandlePacketRecv(chainID, chain, packetDatagram, log) == \* get chainID's connection end LET connectionEnd == chain.connectionEnd IN \* get chainID's channel end - LET channelEnd == chain.connectionEnd.channelEnd IN + LET channelEnd == connectionEnd.channelEnd IN \* get packet LET packet == packetDatagram.packet IN IF \* if the channel and connection ends are open for packet transmission - /\ channelEnd.state /= "UNINIT" /\ channelEnd.state = "OPEN" - /\ connectionEnd.state /= "UNINIT" /\ connectionEnd.state = "OPEN" \* if the packet has not passed the timeout height /\ \/ packet.timeoutHeight = 0 \/ chain.height < packet.timeoutHeight - \* if the "PacketRecv" datagram can be verified + \* if the "PacketRecv" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.counterpartyPortID /\ packet.srcChannelID = channelEnd.counterpartyChannelID + /\ packet.dstPortID = channelEnd.portID /\ packet.dstChannelID = channelEnd.channelID + \* if "PacketRecv" datagram can be verified /\ packetDatagram.proofHeight \in chain.counterpartyClientHeights THEN \* construct log entry for packet log LET logEntry == AsPacketLogEntry( [type |-> "PacketRecv", srcChainID |-> chainID, sequence |-> packet.sequence, + portID |-> packet.dstPortID, channelID |-> packet.dstChannelID, timeoutHeight |-> packet.timeoutHeight ]) IN \* if the channel is unordered and the packet has not been received IF /\ channelEnd.order = "UNORDERED" - /\ AsPacketReceipt([channelID |-> packet.dstChannelID, sequence |-> packet.sequence]) - \notin chain.packetReceipts + /\ AsPacketReceipt([ + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence + ]) \notin chain.packetReceipts THEN LET newChainStore == [chain EXCEPT - \* record that the packet has been received - !.packetReceipts = chain.packetReceipts - \union - {AsPacketReceipt( - [channelID |-> packet.dstChannelID, - sequence |-> packet.sequence])}, + \* record that the packet has been received + !.packetReceipts = + chain.packetReceipts + \union + {AsPacketReceipt([channelID |-> packet.dstChannelID, + portID |-> packet.dstPortID, + sequence |-> packet.sequence])}, \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN @@ -85,20 +91,22 @@ HandlePacketAck(chainID, chain, packetDatagram, log) == LET packet == packetDatagram.packet IN \* get packet committment that should be in chain store LET packetCommitment == AsPacketCommitment( - [channelID |-> packet.srcChannelID, + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]) IN IF \* if the channel and connection ends are open for packet transmission - /\ channelEnd.state /= "UNINIT" /\ channelEnd.state = "OPEN" - /\ connectionEnd.state /= "UNINIT" /\ connectionEnd.state = "OPEN" \* if the packet committment exists in the chain store /\ packetCommitment \in chain.packetCommittments - \* if the "PacketAck" datagram can be verified + \* if the "PacketRecv" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* if the "PacketAck" datagram can be verified /\ packetDatagram.proofHeight \in chain.counterpartyClientHeights THEN \* if the channel is ordered and the packet sequence is nextAckSeq LET newChainStore == @@ -135,6 +143,11 @@ WritePacketCommitment(chain, packet) == /\ channelEnd.state \notin {"UNINIT", "CLOSED"} \* connection end is initialized /\ connectionEnd.state /= "UNINIT" + \* if the packet has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID \* timeout height has not passed /\ \/ packet.timeoutHeight = 0 \/ latestClientHeight < packet.timeoutHeight @@ -144,7 +157,8 @@ WritePacketCommitment(chain, packet) == /\ packet.sequence = channelEnd.nextSendSeq THEN [chain EXCEPT !.packetCommitments = - chain.packetCommitments \union {[channelID |-> packet.srcChannelID, + chain.packetCommitments \union {[portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]}, !.connectionEnd.channelEnd.nextSendSeq = channelEnd.nextSendSeq + 1 @@ -156,7 +170,8 @@ WritePacketCommitment(chain, packet) == /\ channelEnd.order = "UNORDERED" THEN [chain EXCEPT !.packetCommitments = - chain.packetCommitments \union {[channelID |-> packet.srcChannelID, + chain.packetCommitments \union {[portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]} ] @@ -165,15 +180,17 @@ WritePacketCommitment(chain, packet) == \* write acknowledgements to chain store WriteAcknowledgement(chain, packet) == + \* create a packet acknowledgement for this packet + LET packetAcknowledgement == AsPacketAcknowledgement( + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> TRUE]) IN + \* if the acknowledgement for the packet has not been written - IF packet \notin chain.packetAcknowledgements + IF packetAcknowledgement \notin chain.packetAcknowledgements THEN \* write the acknowledgement to the chain store and remove \* the packet from the set of packets to acknowledge - LET packetAcknowledgement == - AsPacketAcknowledgement( - [channelID |-> packet.dstChannelID, - sequence |-> packet.sequence, - acknowledgement |-> TRUE]) IN [chain EXCEPT !.packetAcknowledgements = chain.packetAcknowledgements \union @@ -181,7 +198,7 @@ WriteAcknowledgement(chain, packet) == !.packetsToAcknowledge = Tail(chain.packetsToAcknowledge)] - \* remove the packet from the set of packets to acknowledge + \* remove the packet from the sequence of packets to acknowledge ELSE [chain EXCEPT !.packetsToAcknowledge = Tail(chain.packetsToAcknowledge)] @@ -195,14 +212,134 @@ LogAcknowledgement(chainID, chain, log, packet) == [type |-> "WriteAck", srcChainID |-> chainID, sequence |-> packet.sequence, + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, timeoutHeight |-> packet.timeoutHeight, acknowledgement |-> TRUE]) IN Append(log, packetLogEntry) \* do not add anything to the log ELSE log + +\* check if a packet timed out +TimeoutPacket(chain, counterpartyChain, packet, proofHeight) == + \* get connection end + LET connectionEnd == chain.connectionEnd IN + \* get channel end + LET channelEnd == connectionEnd.channelEnd IN + \* get counterparty channel end + LET counterpartyChannelEnd == counterpartyChain.channelEnd IN + + \* get packet committment that should be in chain store + LET packetCommitment == AsPacketCommitment( + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]) IN + \* get packet receipt that should be absent in counterparty chain store + LET packetReceipt == AsPacketReceipt( + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence]) IN + + \* if channel end is open + IF /\ channelEnd.state = "OPEN" + \* srcChannelID and srcPortID match channel and port IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + \* dstChannelID and dstPortID match counterparty channel and port IDs + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* packet has timed out + /\ packet.timeoutHeight > 0 + /\ proofHeight >= packet.timeoutHeight + \* chain has sent the packet + /\ packetCommitment \in chain.packetCommitments + \* counterparty chain has not received the packet + /\ \/ /\ channelEnd.order = "ORDERED" + /\ counterpartyChannelEnd.nextRcvSeq <= packet.sequence + \/ /\ channelEnd.order = "UNORDERED" + /\ packetReceipt \notin counterpartyChain.packetReceipts + \* counterparty channel end has dstPortID and dstChannelID + /\ counterpartyChannelEnd.portID = packet.dstPortID + /\ counterpartyChannelEnd.channelID = packet.dstChannelID + \* close ordered channel and remove packet commitment + THEN LET updatedChannelEnd == [channelEnd EXCEPT + !.state = IF channelEnd.order = "ORDERED" + THEN "CLOSED" + ELSE channelEnd.state] IN + LET updatedConnectionEnd == [connectionEnd EXCEPT + !.channelEnd = updatedChannelEnd] IN + LET updatedChainStore == [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \ {packetCommitment}, + !.connectionEnd = updatedConnectionEnd] IN + + updatedChainStore + + \* otherwise, do not update the chain store + ELSE chain + +\* check if a packet timed out on close +TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == + \* get connection end + LET connectionEnd == chain.connectionEnd IN + \* get channel end + LET channelEnd == connectionEnd.channelEnd IN + \* get counterparty channel end + LET counterpartyChannelEnd == counterpartyChain.connectionEnd.channelEnd IN + + \* get packet committment that should be in chain store + LET packetCommitment == AsPacketCommitment( + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]) IN + \* get packet receipt that should be absent in counterparty chain store + LET packetReceipt == AsPacketReceipt( + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence]) IN + + + \* if srcChannelID and srcPortID match channel and port IDs + IF /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + \* if dstChannelID and dstPortID match counterparty channel and port IDs + /\ packet.dstPort = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* chain has sent the packet + /\ packetCommitment \in chain.packetCommitments + \* counterparty channel end is closed and its fields are as expected + /\ counterpartyChannelEnd.state = "CLOSED" + /\ counterpartyChannelEnd.portID = packet.dstPortID + /\ counterpartyChannelEnd.channelID = packet.dstChannelID + /\ counterpartyChannelEnd.counterpartyPortID = packet.srcPortID + /\ counterpartyChannelEnd.counterpartyChannelID = packet.srcChannelID + \* counterparty chain has not received the packet + /\ \/ /\ channelEnd.order = "ORDERED" + /\ counterpartyChannelEnd.nextRcvSeq <= packet.sequence + \/ /\ channelEnd.order = "UNORDERED" + /\ packetReceipt \notin counterpartyChain.packetReceipts + \* close ordered channel and remove packet commitment + THEN LET updatedChannelEnd == [channelEnd EXCEPT + !.state = IF channelEnd.order = "ORDERED" + THEN "CLOSED" + ELSE channelEnd.state] IN + LET updatedConnectionEnd == [connectionEnd EXCEPT + !.channelEnd = updatedChannelEnd] IN + LET updatedChainStore == [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \ {packetCommitment}, + !.connectionEnd = updatedConnectionEnd] IN + + updatedChainStore + + \* otherwise, do not update the chain store + ELSE chain + ============================================================================= \* Modification History -\* Last modified Fri Nov 06 20:43:25 CET 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 10:31:13 CET 2020 by ilinastoilkovska \* Created Wed Jul 29 14:30:04 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/ICS18Relayer.tla b/docs/spec/relayer/tla/ICS18Relayer.tla index 16d736c0e4..87f0c9a26e 100644 --- a/docs/spec/relayer/tla/ICS18Relayer.tla +++ b/docs/spec/relayer/tla/ICS18Relayer.tla @@ -1,11 +1,11 @@ ------------------------------- MODULE Relayer ------------------------------ +--------------------------- MODULE ICS18Relayer ---------------------------- (*************************************************************************** This module contains the specification of a relayer, which is an off-chain process running a relayer algorithm ***************************************************************************) -EXTENDS Integers, FiniteSets, Sequences, RelayerDefinitions +EXTENDS Integers, FiniteSets, Sequences, IBCCoreDefinitions CONSTANTS GenerateClientDatagrams, \* toggle generation of client datagrams GenerateConnectionDatagrams, \* toggle generation of connection datagrams @@ -16,6 +16,7 @@ ASSUME /\ GenerateClientDatagrams \in BOOLEAN /\ GenerateChannelDatagrams \in BOOLEAN CONSTANTS MaxHeight, \* set of possible heights of the chains in the system + MaxVersion, \* maximal connection / channel version (we assume versions are integers) MaxPacketSeq \* maximal packet sequence number VARIABLES chainAstore, \* store of ChainA @@ -71,19 +72,19 @@ ClientDatagrams(srcChainID, dstChainID, relayer) == LET dstDatagrams == IF srcClientHeight = AsInt(nullHeight) THEN \* the src client does not exist on dstChainID - {AsDatagram( - [type |-> "CreateClient", - height |-> srcChainHeight, - clientID |-> srcClientID] - )} + {AsDatagram([ + type |-> "ClientCreate", + height |-> srcChainHeight, + clientID |-> srcClientID + ])} ELSE \* the src client exists on dstChainID IF srcClientHeight < srcChainHeight THEN \* the height of the src client on dstChainID is smaller than the height of the src chain - {AsDatagram( - [type |-> "ClientUpdate", - height |-> srcChainHeight, - clientID |-> srcClientID] - )} + {AsDatagram([ + type |-> "ClientUpdate", + height |-> srcChainHeight, + clientID |-> srcClientID + ])} ELSE emptySetDatagrams IN [datagrams|-> dstDatagrams, relayerUpdate |-> updatedRelayer] @@ -110,41 +111,43 @@ ConnectionDatagrams(srcChainID, dstChainID) == LET dstDatagrams == IF dstConnectionEnd.state = "UNINIT" /\ srcConnectionEnd.state = "UNINIT" THEN - {AsDatagram( - [type |-> "ConnOpenInit", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - clientID |-> GetCounterpartyClientID(dstChainID), \* "clA" - counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" - counterpartyClientID |-> GetCounterpartyClientID(srcChainID)] \* "clB" - )} + {AsDatagram([ + type |-> "ConnOpenInit", + connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + clientID |-> GetCounterpartyClientID(dstChainID), \* "clA" + counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" + counterpartyClientID |-> GetCounterpartyClientID(srcChainID) \* "clB" + ])} - ELSE IF srcConnectionEnd.state = "INIT" /\ \/ dstConnectionEnd.state = "UNINIT" + ELSE IF srcConnectionEnd.state = "INIT" /\ \/ dstConnectionEnd.state = "UNINIT" \/ dstConnectionEnd.state = "INIT" THEN - {AsDatagram( - [type |-> "ConnOpenTry", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - clientID |-> srcConnectionEnd.counterpartyClientID, \* "clA" - counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" - counterpartyClientID |-> srcConnectionEnd.clientID, \* "clB" - proofHeight |-> srcHeight, - consensusHeight |-> srcClientHeight] - )} + {AsDatagram([ + type |-> "ConnOpenTry", + desiredConnectionID |-> srcConnectionEnd.counterpartyConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + counterpartyConnectionID |-> srcConnectionEnd.connectionID, \* "connAtoB" + clientID |-> srcConnectionEnd.counterpartyClientID, \* "clA" + counterpartyClientID |-> srcConnectionEnd.clientID, \* "clB" + versions |-> srcConnectionEnd.versions, + proofHeight |-> srcHeight, + consensusHeight |-> srcClientHeight + ])} ELSE IF srcConnectionEnd.state = "TRYOPEN" /\ \/ dstConnectionEnd.state = "INIT" \/ dstConnectionEnd.state = "TRYOPEN" THEN - {AsDatagram( - [type |-> "ConnOpenAck", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight, - consensusHeight |-> srcClientHeight] - )} + {AsDatagram([ + type |-> "ConnOpenAck", + connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + versions |-> srcConnectionEnd.versions, + proofHeight |-> srcHeight, + consensusHeight |-> srcClientHeight + ])} ELSE IF srcConnectionEnd.state = "OPEN" /\ dstConnectionEnd.state = "TRYOPEN" THEN - {AsDatagram( - [type |-> "ConnOpenConfirm", - connectionID |-> dstConnectionEnd.connectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight] - )} + {AsDatagram([ + type |-> "ConnOpenConfirm", + connectionID |-> dstConnectionEnd.connectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + proofHeight |-> srcHeight + ])} ELSE emptySetDatagrams IN dstDatagrams @@ -161,6 +164,9 @@ ChannelDatagrams(srcChainID, dstChainID) == LET srcChannelEnd == GetChannelEnd(srcChain) IN LET dstChannelEnd == GetChannelEnd(dstChain) IN + LET srcPortID == GetPortID(srcChainID) IN + LET dstPortID == GetPortID(dstChainID) IN + LET srcChannelID == GetChannelID(srcChainID) IN LET dstChannelID == GetChannelID(dstChainID) IN @@ -170,64 +176,59 @@ ChannelDatagrams(srcChainID, dstChainID) == LET dstDatagrams == IF dstChannelEnd.state = "UNINIT" /\ srcChannelEnd.state = "UNINIT" THEN - {AsDatagram( - [type |-> "ChanOpenInit", - channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - counterpartyChannelID |-> srcChannelID] \* "chanAtoB" - )} + {AsDatagram([ + type |-> "ChanOpenInit", + portID |-> dstPortID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelID, \* "chanBtoA" + counterpartyPortID |-> srcPortID, \* "portA" + counterpartyChannelID |-> srcChannelID \* "chanAtoB" + ])} ELSE IF srcChannelEnd.state = "INIT" /\ \/ dstChannelEnd.state = "UNINIT" \/ dstChannelEnd.state = "INIT" THEN - {AsDatagram( - [type |-> "ChanOpenTry", - channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - counterpartyChannelID |-> srcChannelID, \* "chanAtoB" - proofHeight |-> srcHeight] - )} + {AsDatagram([ + type |-> "ChanOpenTry", + portID |-> dstPortID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelID, \* "chanBtoA" + counterpartyPortID |-> srcPortID, \* "portA" + counterpartyChannelID |-> srcChannelID, \* "chanAtoB" + proofHeight |-> srcHeight + ])} ELSE IF srcChannelEnd.state = "TRYOPEN" /\ \/ dstChannelEnd.state = "INIT" \/ dstChannelEnd.state = "TRYOPEN" THEN - {AsDatagram( - [type |-> "ChanOpenAck", - channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight] - )} + {AsDatagram([ + type |-> "ChanOpenAck", + portID |-> dstChannelEnd.portID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelEnd.channelID, \* "chanBtoA" + proofHeight |-> srcHeight + ])} ELSE IF srcChannelEnd.state = "OPEN" /\ dstChannelEnd.state = "TRYOPEN" THEN - {AsDatagram( - [type |-> "ChanOpenConfirm", - channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight] - )} + {AsDatagram([ + type |-> "ChanOpenConfirm", + portID |-> dstChannelEnd.portID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelEnd.channelID, \* "chanBtoA" + proofHeight |-> srcHeight + ])} \* channel closing datagrams creation only for open channels ELSE IF dstChannelEnd.state = "OPEN" /\ GetCloseChannelFlag(dstChannelID) THEN - {AsDatagram( - [type |-> "ChanCloseInit", - channelID |-> dstChannelEnd.channelID] \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - )} + {AsDatagram([ + type |-> "ChanCloseInit", + portID |-> dstChannelEnd.portID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelEnd.channelID \* "chanBtoA" + ])} ELSE IF /\ srcChannelEnd.state = "CLOSED" /\ dstChannelEnd.state /= "CLOSED" /\ dstChannelEnd.state /= "UNINIT" THEN - {AsDatagram( - [type |-> "ChanCloseConfirm", - channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight] - )} - - (** channel closing datagrams creation for channels which are still in handshake: - the propery ChanOpenInitDelivery is violated - - ELSE IF dstChannelEnd.state /= "CLOSED" /\ dstChannelEnd.state /= "UNINIT" /\ GetCloseChannelFlag(dstChannelID) THEN - {[type |-> "ChanCloseInit", - channelID |-> dstChannelEnd.channelID]} \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - - ELSE IF srcChannelEnd.state = "CLOSED" /\ dstChannelEnd.state /= "CLOSED" /\ dstChannelEnd.state /= "UNINIT" THEN - {[type |-> "ChanCloseConfirm", - channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight]} - **) + {AsDatagram([ + type |-> "ChanCloseConfirm", + portID |-> dstChannelEnd.portID, \* "portB" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelEnd.channelID, \* "chanBtoA" + proofHeight |-> srcHeight + ])} ELSE emptySetDatagrams IN @@ -238,27 +239,36 @@ ChannelDatagrams(srcChainID, dstChainID) == ***************************************************************************) \* Compute a packet datagram based on the packetLogEntry PacketDatagram(packetLogEntry) == - \* get srcChainID and its channel end + \* get chainID and its channel end LET chainID == packetLogEntry.srcChainID IN LET channelEnd == GetChainByID(chainID).connectionEnd.channelEnd IN + + \* get portID and counterpartyPortID + LET portID == channelEnd.portID IN \* "portA" (if srcChainID = "chainA") + LET counterpartyPortID == channelEnd.counterpartyPortID IN \* "portB" (if srcChainID = "chainA") + \* get channelID and counterpartyChannelID LET channelID == channelEnd.channelID IN \* "chanAtoB" (if srcChainID = "chainA") LET counterpartyChannelID == channelEnd.counterpartyChannelID IN \* "chanBtoA" (if srcChainID = "chainA") - LET srcHeight == GetLatestHeight(GetChainByID(srcChainID)) IN + LET srcHeight == GetLatestHeight(GetChainByID(chainID)) IN \* the srcChannelID of the packet that is received is channelID, \* the dstChannelID of the packet that is received is counterpartyChannelID LET recvPacket(logEntry) == AsPacket([sequence |-> logEntry.sequence, timeoutHeight |-> logEntry.timeoutHeight, + srcPortID |-> portID, srcChannelID |-> channelID, + dstPortID |-> counterpartyPortID, dstChannelID |-> counterpartyChannelID]) IN \* the srcChannelID of the packet that is acknowledged is counterpartyChannelID, \* the dstChannelID of the packet that is acknowledged is channelID LET ackPacket(logEntry) == AsPacket([sequence |-> logEntry.sequence, timeoutHeight |-> logEntry.timeoutHeight, + srcPortID |-> counterpartyPortID, srcChannelID |-> counterpartyChannelID, + dstPortID |-> portID, dstChannelID |-> channelID]) IN IF packetLogEntry.type = "PacketSent" @@ -276,25 +286,25 @@ PacketDatagram(packetLogEntry) == Compute client, connection, channel datagrams (from srcChainID to dstChainID) ***************************************************************************) \* Currently supporting: -\* - ICS 002: Client updates -\* - ICS 003: Connection handshake -\* - ICS 004: Channel handshake +\* - ICS 02: Client updates +\* - ICS 03: Connection handshake +\* - ICS 04: Channel handshake ComputeDatagrams(srcChainID, dstChainID) == - \* ICS 002 : Clients + \* ICS 02 : Clients \* - Determine if light clients needs to be updated LET clientDatagrams == IF GenerateClientDatagrams THEN ClientDatagrams(srcChainID, dstChainID, relayerHeights) ELSE [datagrams |-> AsSetDatagrams({}), relayerUpdate |-> relayerHeights] IN - \* ICS3 : Connections + \* ICS 03 : Connections \* - Determine if any connection handshakes are in progress LET connectionDatagrams == IF GenerateConnectionDatagrams THEN ConnectionDatagrams(srcChainID, dstChainID) ELSE AsSetDatagrams({}) IN - \* ICS4 : Channels & Packets + \* ICS 04 : Channels & Packets \* - Determine if any channel handshakes are in progress LET channelDatagrams == IF GenerateChannelDatagrams @@ -352,32 +362,25 @@ RelayPacketDatagram(packetLogEntry) == UpdateClient == \E chainID \in ChainIDs : UpdateRelayerClientHeight(chainID) -\* create client, connection, channel datagrams +\* create client, connection, channel, packet datagrams CreateDatagrams == \E srcChainID \in ChainIDs : \E dstChainID \in ChainIDs : + \* client, connection, channel datagrams /\ Relay(srcChainID, dstChainID) /\ \/ /\ packetLog /= AsPacketLog(<<>>) /\ Head(packetLog).srcChainID = srcChainID + \* packet datagrams /\ outgoingPacketDatagrams' = RelayPacketDatagram(AsPacketLogEntry(Head(packetLog))) /\ packetLog' = Tail(packetLog) \/ /\ UNCHANGED <> - -\* \* scan packet log and create packet datagrams -\* ScanPacketLog == -\* /\ packetLog /= AsPacketLog(<<>>) -\* /\ outgoingPacketDatagrams' = RelayPacketDatagram(AsPacketLogEntry(Head(packetLog))) -\* /\ packetLog' = Tail(packetLog) -\* /\ UNCHANGED <> -\* /\ UNCHANGED <> - - (*************************************************************************** Specification ***************************************************************************) \* Initial state predicate \* Initially: \* - the relayer heights are uninitialized (i.e., their height is nullHeight) +\* - there are no datagrams Init == /\ relayerHeights = [chainID \in ChainIDs |-> AsInt(nullHeight)] /\ outgoingDatagrams = [chainID \in ChainIDs |-> AsSetDatagrams({})] @@ -386,8 +389,7 @@ Init == \* Next state action \* The relayer either: \* - updates its clients, or -\* - creates datagrams, -\* - scans the packet log and creates packet datagrams, or +\* - creates datagrams, or \* - does nothing Next == \/ UpdateClient @@ -397,7 +399,7 @@ Next == \* Fairness constraints Fairness == /\ \A chainID \in ChainIDs : - WF_vars(UpdateRelayerClients(chainID)) + WF_vars(UpdateRelayerClientHeight(chainID)) /\ \A srcChainID \in ChainIDs : \A dstChainID \in ChainIDs : WF_vars(Relay(srcChainID, dstChainID)) @@ -407,9 +409,10 @@ Fairness == \* Type invariant TypeOK == /\ relayerHeights \in [ChainIDs -> Heights \union {nullHeight}] - /\ outgoingDatagrams \in [ChainIDs -> SUBSET Datagrams(MaxHeight, MaxPacketSeq)] + /\ outgoingDatagrams \in [ChainIDs -> SUBSET Datagrams(MaxHeight, MaxPacketSeq, MaxVersion)] + /\ outgoingPacketDatagrams \in [ChainIDs -> Seq(Datagrams(MaxHeight, MaxPacketSeq, MaxVersion))] ============================================================================= \* Modification History -\* Last modified Wed Nov 11 17:26:08 CEST 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 10:50:40 CET 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/tla/README.md b/docs/spec/relayer/tla/README.md index a7ff4375f8..d529f4c556 100644 --- a/docs/spec/relayer/tla/README.md +++ b/docs/spec/relayer/tla/README.md @@ -1,6 +1,6 @@ # TLA+ specification of the IBC Core protocols -A TLA+ specification of the IBC Core protocols ([ICS02](), [ICS03](), [ICS04](), [ICS18]()). +A TLA+ specification of the IBC Core protocols ([ICS02](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-002-client-semantics), [ICS03](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-003-connection-semantics), [ICS04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics), [ICS18](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-018-relayer-algorithms)). In particular, the main module is [IBCCore.tla](IBCCore.tla) and models the system consisting of two chains and two relayers. The model allows to express concurrency aspects of a system with multiple (correct) relayers. @@ -30,7 +30,7 @@ Next == where `UpdateClient` and `CreateDatagrams` are scheduled non-deterministically. `UpdateClient` picks a light client on the relayer for some chain and updates it. `CreateDatagrams` picks a direction (a pair of source and destination chain) and creates client, connection, channel, and packet datagrams (i.e., it captures the -logic of [`pendingDatagrams()`](https://github.com/cosmos/ics/tree/master/spec/ics-018-relayer-algorithms#pending-datagrams)). +logic of [`pendingDatagrams()`](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-018-relayer-algorithms#pending-datagrams)). ### [`Chain.tla`](Chain.tla) The chain state is represented by a chain store, which is a snapshot of the provable and private stores, to the extent necessary for IBC. Additionally, a chain has dedicated @@ -50,7 +50,7 @@ Next == where: - `AdvanceChain`: increments the height of the chain, - `HandleIncomingDatagrams`: dispatches the datagrams to the appropriate handlers. -This captures the logic of the [routing module](https://github.com/cosmos/ics/tree/master/spec/ics-026-routing-module). +This captures the logic of the [routing module](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-026-routing-module). - `SendPacket`: models user/application-defined calls to send a packet. As this specification does not have a specific application in mind, we abstract away from the packet data, and allow sending packets non-deterministically. The packet commitment is written in the chain store, and the sent packet is logged, which triggers the relayer to create a `PacketRecv` datagram. @@ -61,8 +61,8 @@ which triggers the relayer to create a `PacketRecv` datagram. These TLA+ modules contain definitions of operators that handle client, connection handshake, channel handshake, and packet datagrams, respectively. -These operators capture the logic of the handlers defined in [ICS02](), [ICS03](), and -[ICS04](). +These operators capture the logic of the handlers defined in [ICS02](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-002-client-semantics), [ICS03](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-003-connection-semantics), and +[ICS04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics). @@ -82,101 +82,108 @@ modules. ### System-level properties -We specify three kinds of properties for the IBC core protocols: +We specify three kinds of properties for the IBC core protocols in the module [IBCCore.tla](IBCCore.tla): -- **IBCSafety**: Bad datagrams are not used to update the chain stores. +- `IBCSafety`: Bad datagrams are not used to update the chain stores. -- **IBCValidity**: If `ChainB` receives a datagram from `ChainA`, then the datagram was sent by `ChainA` +- `IBCValidity`: If `ChainB` receives a datagram from `ChainA`, then the datagram was sent by `ChainA` -- **IBCDelivery**: If `ChainA` sends a datagram to `ChainB`, then `ChainB` eventually receives the datagram +- `IBCDelivery`: If `ChainA` sends a datagram to `ChainB`, then `ChainB` eventually receives the datagram -TODO: add links to where they are -### Packet -ICS 04 specifies the following list of ["Desired -Properties"](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#desired-properties) +### Packets -#### [Efficiency](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#efficiency) +[ICS04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics) specifies the following list of ["Desired +Properties"](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics#desired-properties) + +#### [Efficiency](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics#efficiency) Efficiency seems to be too vague to formalize. In particular the formulation ignores relayers that are the active components in packet -transmission. It is not clear what a suitable way is to formalize it +transmission. It is not clear what a suitable way is to formalize it. -#### [Exactly-once delivery](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#exactly-once-delivery) +#### [Exactly-once delivery](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics#exactly-once-delivery) These properties are also vague as: * in the absence of a relayer no packets can be delivered * ignores timeouts -* unspecific what "sent" means. We suggest it means that a packet - datagram is put wherever (TODO: Ilina please help) rather than - executing `SendPacket` +* unspecific what "sent" means. We suggest it means that a packet commitment is written in the provable store (in our model `ChainStore`) rather than executing `SendPacket`. As a result we suggest that the property should be decomposed into to properties: -* (at most once) if a valid chain delivers packet p, it will - not deliver packet p again in the future +* (at most once) For each packer `p`, if a chain performs `RecvPacket(p)` successfully (without abort), it will + not perform `RecvPacket(p)` successfully in the future. + * (typical case) If * sender and receiver chain are valid, and * there is a correct relayer, and * communication is bounded in time, and - * the timeoutheights and times are luckily chosen, and - * the receiver chain does not censor the packet, and - * ... + * the `timeoutHeights` and times are luckily chosen, and + * the receiver chain does not censor the packet then the packet will be delivered. The second property ignores that timeouts can happen. +If this is the confirmed intended behavior, these properties can be expressed +and verified +by a slight modification of the specification, in particular, the way in which +the packet receipts are stored in the chain store (in a set vs. in a sequence). -#### [Ordering](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#ordering) +#### [Ordering](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics#ordering) - ordered channels: It is not clear what "if packet x is sent before packet y by a channel end on chain A" meant in a context where chain A performs invalid transitions: then a packet with sequence number *i* can be sent after *i+1*. If this happens, the IBC implementation may be broken (depends on the relayer). -We thus formalize it in the context of two valid chains. +In the context of two valid chains, this property can be +expressed and verified by adding a history +variable on the receiving side, which is modified by transitions of the receiving chain. - no property defined for unordered. -#### [Permissioning](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#permissioning) +#### [Permissioning](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics#permissioning) -I guess we can formalize it as constraints about parameters and data when send is called. TODO with Ilina. +This property is about capabilities. We do not capture capabilities in the TLA+ specification. ### Channel -As there are no explicit properties regarding channels given in [ICS 04](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics) in textual form, we have formalized that the channel handshake does not deviate from the channel lifecycle provided as a [figure](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics#channel-lifecycle-management). They are given in TODO under the names TODO +As there are no explicit properties regarding channels given in [ICS 04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics) in textual form, we have formalized that the channel handshake does not deviate from the channel lifecycle provided as a [figure](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics/channel-state-machine.png). They are given in [IBCCore.tla](IBCCore.tla) under the names + +- `ChannelInitSafety` +- `ChannelTryOpenSafety` +- `ChannelOpenSafety` +- `ChannelCloseSafety` ### Connection Handshake -We formalize [these properties](https://github.com/cosmos/ics/tree/master/spec/ics-003-connection-semantics#properties--invariants) as follows: -> Connection identifiers are first-come-first-serve: once a connection has been negotiated, a unique identifier pair exists between two chains. -[ICS3-Proto-1-ConnectionUniqueness](https://github.com/informalsystems/ibc-rs/blob/master/docs/spec/connection-handshake/L1_2.md#guarantees) A module accepts (i.e., initializes on) a connection end at most once. +Similar to Channel handshake, we have formalized that the connection handshake does not deviate from the channel lifecycle provided as a [figure](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-003-connection-semantics/state.png). They are given in [IBCCore.tla](IBCCore.tla) under the names -> The connection handshake cannot be man-in-the-middled by another blockchain's IBC handler. +- `ConnectionInitSafety` +- `ConnectionTryOpenSafety` +- `ConnectionOpenSafety` +We formalize [these properties](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-003-connection-semantics#properties--invariants) as follows: +> Connection identifiers are first-come-first-serve: once a connection has been negotiated, a unique identifier pair exists between two chains. -## Invariants TODO: Find a place for this section +[ICS3-Proto-1-ConnectionUniqueness](https://github.com/informalsystems/ibc-rs/blob/master/docs/spec/connection-handshake/L1_2.md#guarantees) A module accepts (i.e., initializes on) a connection end at most once. + +> The connection handshake cannot be man-in-the-middled by another blockchain's IBC handler. -To check invariants with [Apalache](https://github.com/informalsystems/apalache/), we introduce a history variable, which keeps track of the state of the connections -and channels. -We define the invariant **IBCInv**, which states that -once a connection or channel end reaches a certain state, -it does not go back to the previous state. +The scenario is not clear, so we did not formalize it. -For example, if the connection end on `ChainA` has -reached state `OPEN`, it never goes back to the state `UNINIT`. ## Using the Model ### Constants -The module `ICS18Environment.tla` is parameterized by the constants: +The module `IBCCore.tla` is parameterized by the constants: - `ClientDatagramsRelayer_i`, for `i in {1, 2}`, a Boolean flag defining if `Relayer_i` creates client datagrams, - `ConnectionDatagramsRelayer_i`, for `i in {1, 2}`, a Boolean flag defining if `Relayer_i` creates connection datagrams, - `ChannelDatagramsRelayer_i`, for `i in {1, 2}`, a Boolean flag defining if `Relayer_i` creates channel datagrams, @@ -188,22 +195,16 @@ The module `ICS18Environment.tla` is parameterized by the constants: ## Importing the specification into TLA+ toolbox To import the specification in the TLA+ toolbox and run TLC: - - add a new spec in TLA+ toolbox with the root-module file `ICS18Environment.tla` + - add a new spec in TLA+ toolbox with the root-module file `IBCCore.tla` - create a model - assign a value to the constants - choose "Temporal formula" as the behavior spec, and use the formula `Spec` - - add the properties `ICS18Safety` and `ICS18Delivery` + - add the properties `IBCSafety` and `IBCDelivery` - run TLC on the model #### Assigning values to the constants in a TLC model -The Boolean flags, defined as constants in the module `ICS18Environment.tla`, allow us to run experiments in different settings. For example, if we set both `ClientDatagramsRelayer_1` and `ClientDatagramsRelayer_2` to `TRUE` in a TLC model, then the two relayers in the system concurrently create datagrams related to client creation and client update, and the model checker will check the temporal properties related to client datagrams. +The Boolean flags, defined as constants in the module `IBCCore.tla`, allow us to run experiments in different settings. For example, if we set both `ClientDatagramsRelayer_1` and `ClientDatagramsRelayer_2` to `TRUE` in a TLC model, then the two relayers in the system concurrently create datagrams related to client creation and client update, and the model checker will check the temporal properties related to client datagrams. Observe that the setting where, for example, `ClientDatagramsRelayer_1 = TRUE`, `ConnectionDatagramsRelayer_2 = TRUE`, `ChannelDatagramsRelayer_1 = TRUE`, and the remaining flags are `FALSE`, is equivalent to a single relayer, as there is no concurrency in the creation of datagrams between the two relayers. -## Checking the invariant `ICS18Inv` with Apalache - -To check the `ICS18Environment.tla` specification with [Apalache](https://github.com/informalsystems/apalache/), we use the file `ICS18Environment_apalache`, where we define the values of the model constants. To run the model checker and check the invariant `ICS18Inv`, we run the command: -```shell -apalache check --inv=ICS18Inv ICS18Environment_apalache.tla -``` From 60e8edd44704c8d2dbb85f7f47de9175667a6f67 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 1 Dec 2020 17:24:34 +0100 Subject: [PATCH 3/6] final ICS20 tla spec fixes (#430) --- docs/spec/fungible-token-transfer/Chain.tla | 9 ++- .../IBCTokenTransfer.tla | 6 +- .../IBCTokenTransferDefinitions.tla | 12 +-- .../ICS04PacketHandlers.tla | 76 +++++++++++++------ docs/spec/fungible-token-transfer/README.md | 25 ++++-- 5 files changed, 84 insertions(+), 44 deletions(-) diff --git a/docs/spec/fungible-token-transfer/Chain.tla b/docs/spec/fungible-token-transfer/Chain.tla index e11d5872cf..c7f01d4286 100644 --- a/docs/spec/fungible-token-transfer/Chain.tla +++ b/docs/spec/fungible-token-transfer/Chain.tla @@ -28,14 +28,15 @@ Heights == 1..MaxHeight \* set of possible heights of the chains in the system \* Create a packet: Abstract away from timestamp. \* Assume timeoutHeight is MaxHeight + 1 CreatePacket(packetData) == + LET channelEnd == chainStore.channelEnd IN AsPacket([ sequence |-> appPacketSeq, timeoutHeight |-> MaxHeight + 1, data |-> packetData, - srcChannelID |-> GetChannelID(ChainID), - srcPortID |-> GetPortID(ChainID), - dstChannelID |-> GetCounterpartyChannelID(ChainID), - dstPortID |-> GetCounterpartyPortID(ChainID) + srcPortID |-> channelEnd.portID, + srcChannelID |-> channelEnd.channelID, + dstPortID |-> channelEnd.counterpartyPortID, + dstChannelID |-> channelEnd.counterpartyChannelID ]) diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla b/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla index d458b04dcf..2a8672a190 100644 --- a/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla +++ b/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla @@ -47,7 +47,7 @@ ChainB == INSTANCE Chain appPacketSeq <- appPacketSeqChainB (*************************************************************************** - ICS02Environment operators + Environment operators ***************************************************************************) \* get chain store by ID @@ -86,7 +86,7 @@ PacketDatagram(srcChainID, dstChainID, packetLogEntry) == LET dstChannelID == GetChannelID(dstChainID) IN \* "chanBtoA" (if dstChainID = "chainB") LET srcPortID == GetPortID(srcChainID) IN \* "portA" (if srcChainID = "chainA") - LET dstPortID == GetPortID(dstChainID) IN \* "portb" (if dstChainID = "chainB") + LET dstPortID == GetPortID(dstChainID) IN \* "portB" (if dstChainID = "chainB") LET srcHeight == GetLatestHeight(GetChainByID(srcChainID)) IN @@ -120,7 +120,7 @@ PacketDatagram(srcChainID, dstChainID, packetLogEntry) == ELSE NullDatagram (*************************************************************************** - ICS02Environment actions + Environment actions ***************************************************************************) \* update the client height of some chain UpdateClients == diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla b/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla index d7a69db37d..80276bc019 100644 --- a/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla +++ b/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla @@ -191,9 +191,10 @@ ChannelEnds == [ state : ChannelStates, order : {"UNORDERED"}, + portID : PortIDs \union {nullPortID}, channelID : ChannelIDs \union {nullChannelID}, - counterpartyChannelID : ChannelIDs \union {nullChannelID}, counterpartyPortID : PortIDs \union {nullPortID}, + counterpartyChannelID : ChannelIDs \union {nullChannelID}, version : {"ics20-1"} ] @@ -246,10 +247,10 @@ Packets(maxHeight, maxPacketSeq, maxBalance, Denominations) == sequence : 1..maxPacketSeq, timeoutHeight : 1..maxHeight, data : FungibleTokenPacketData(maxBalance, Denominations), - srcChannelID : ChannelIDs, srcPortID : PortIDs, - dstChannelID : ChannelIDs, - dstPortID : PortIDs + srcChannelID : ChannelIDs, + dstPortID : PortIDs, + dstChannelID : ChannelIDs ] <: {PacketType} @@ -378,9 +379,10 @@ GetLatestHeight(chain) == InitUnorderedChannelEnd(ChainID) == [state |-> "OPEN", order |-> "UNORDERED", + portID |-> GetPortID(ChainID), channelID |-> GetChannelID(ChainID), - counterpartyChannelID |-> GetCounterpartyChannelID(ChainID), counterpartyPortID |-> GetCounterpartyPortID(ChainID), + counterpartyChannelID |-> GetCounterpartyChannelID(ChainID), version |-> "ics20-1"] diff --git a/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla b/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla index 0dd6c8994c..0b69901358 100644 --- a/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla +++ b/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla @@ -25,8 +25,10 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, accounts, escrowAccounts, \* if the packet has not passed the timeout height /\ \/ packet.timeoutHeight = 0 \/ chain.height < packet.timeoutHeight - \* if the "PacketRecv" datagram can be verified + \* if the "PacketRecv" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.counterpartyPortID /\ packet.srcChannelID = channelEnd.counterpartyChannelID + /\ packet.dstPortID = channelEnd.portID /\ packet.dstChannelID = channelEnd.channelID THEN \* call application function OnPacketRecv LET OnPacketRecvOutcome == @@ -34,13 +36,17 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, accounts, escrowAccounts, \* if OnPacketRecv is successful IF /\ ~OnPacketRecvOutcome.error \* if the packet has not been received - /\ [channelID |-> packet.dstChannelID, sequence |-> packet.sequence] - \notin chain.packetReceipts + /\ AsPacketReceipt([ + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence + ]) \notin chain.packetReceipts THEN \* construct log entry for packet log LET logEntry == AsPacketLogEntry( [type |-> "PacketRecv", srcChainID |-> chainID, sequence |-> packet.sequence, + portID |-> packet.dstPortID, channelID |-> packet.dstChannelID, timeoutHeight |-> packet.timeoutHeight ]) IN @@ -89,7 +95,8 @@ HandlePacketAck(chain, packetDatagram, log, accounts, escrowAccounts, maxBalance LET ack == packetDatagram.acknowledgement IN \* get packet committment that should be in chain store LET packetCommitment == AsPacketCommitment( - [channelID |-> packet.srcChannelID, + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]) IN @@ -101,9 +108,12 @@ HandlePacketAck(chain, packetDatagram, log, accounts, escrowAccounts, maxBalance /\ channelEnd.state = "OPEN" \* if the packet commitment exists in the chain store /\ packetCommitment \in chain.packetCommitments - \* if the "PacketAck" datagram can be verified + \* if the "PacketAck" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* remove packet commitment THEN LET updatedChainStore == [chain EXCEPT !.packetCommitments = @@ -131,6 +141,11 @@ WritePacketCommitment(chain, packet) == IF \* channel end is neither null nor closed /\ channelEnd.state \notin {"UNINIT", "CLOSED"} + \* if the packet has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID \* timeout height has not passed /\ \/ packet.timeoutHeight = 0 \/ latestClientHeight < packet.timeoutHeight @@ -138,8 +153,8 @@ WritePacketCommitment(chain, packet) == !.packetCommitments = chain.packetCommitments \union - {[channelID |-> packet.srcChannelID, - portID |-> packet.srcPortID, + {[portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, data |-> packet.data, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]} @@ -153,16 +168,17 @@ WriteAcknowledgement(chain, packetToAck) == LET packet == packetToAck[1] IN LET ack == packetToAck[2] IN + \* create a packet acknowledgement for this packet + LET packetAcknowledgement == AsPacketAcknowledgement( + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> ack]) IN + \* if the acknowledgement for the packet has not been written - IF packet \notin chain.packetAcknowledgements + IF packetAcknowledgement \notin chain.packetAcknowledgements THEN \* write the acknowledgement to the chain store and remove \* the packet from the set of packets to acknowledge - LET packetAcknowledgement == - AsPacketAcknowledgement( - [channelID |-> packet.dstChannelID, - portID |-> packet.dstChannelID, - sequence |-> packet.sequence, - acknowledgement |-> ack]) IN [chain EXCEPT !.packetAcknowledgements = chain.packetAcknowledgements \union @@ -188,6 +204,8 @@ LogAcknowledgement(chainID, chain, log, packetToAck) == [type |-> "WriteAck", srcChainID |-> chainID, sequence |-> packet.sequence, + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, timeoutHeight |-> packet.timeoutHeight, acknowledgement |-> ack, data |-> packet.data]) IN @@ -202,15 +220,15 @@ TimeoutPacket(chain, counterpartyChain, accounts, escrowAccounts, LET channelEnd == chain.channelEnd IN \* get packet committment that should be in chain store LET packetCommitment == AsPacketCommitment( - [channelID |-> packet.srcChannelID, - portID |-> packet.srcPortID, + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, data |-> packet.data, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]) IN \* get packet receipt that should be absent in counterparty chain store LET packetReceipt == AsPacketReceipt( - [channelID |-> packet.dstChannelID, - portID |-> packet.dstPortID, + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, sequence |-> packet.sequence]) IN \* call application function OnTimeoutPacket @@ -219,9 +237,12 @@ TimeoutPacket(chain, counterpartyChain, accounts, escrowAccounts, \* if channel end is open IF /\ channelEnd.state = "OPEN" + \* srcChannelID and srcPortID match channel and port IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID \* dstChannelID and dstPortID match counterparty channel and port IDs - /\ packet.dstChannelID = channelEnd.counterpartyChannelID /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID \* packet has timed out /\ packet.timeoutHeight > 0 /\ proofHeight >= packet.timeoutHeight @@ -252,29 +273,34 @@ TimeoutOnClose(chain, counterpartyChain, accounts, escrowAccounts, \* get packet committment that should be in chain store LET packetCommitment == AsPacketCommitment( - [channelID |-> packet.srcChannelID, - portID |-> packet.srcPortID, + [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, data |-> packet.data, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]) IN \* get packet receipt that should be absent in counterparty chain store LET packetReceipt == AsPacketReceipt( - [channelID |-> packet.dstChannelID, - portID |-> packet.dstPortID, + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, sequence |-> packet.sequence]) IN \* call application function OnTimeoutPacket LET OnTimeoutPacketOutcome == OnTimeoutPacket(accounts, escrowAccounts, packet, maxBalance) IN + \* if srcChannelID and srcPortID match channel and port IDs + IF /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID \* if dstChannelID and dstPortID match counterparty channel and port IDs - IF /\ packet.dstChannelID = channelEnd.counterpartyChannelID /\ packet.dstPort = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID \* chain has sent the packet /\ packetCommitment \in chain.packetCommitments \* counterparty channel end is closed and its fields are as expected /\ counterpartyChannelEnd.state = "CLOSED" /\ counterpartyChannelEnd.order = "UNORDERED" + /\ counterpartyChannelEnd.portID = packet.dstPortID + /\ counterpartyChannelEnd.channelID = packet.dstChannelID /\ counterpartyChannelEnd.counterpartyChannelID = packet.srcChannelID /\ counterpartyChannelEnd.counterpartyPortID = packet.srcPortID /\ counterpartyChannelEnd.version = channelEnd.version @@ -295,5 +321,5 @@ TimeoutOnClose(chain, counterpartyChain, accounts, escrowAccounts, ============================================================================= \* Modification History -\* Last modified Mon Nov 23 17:22:59 CET 2020 by ilinastoilkovska +\* Last modified Tue Dec 01 16:59:04 CET 2020 by ilinastoilkovska \* Created Thu Oct 19 18:29:58 CET 2020 by ilinastoilkovska diff --git a/docs/spec/fungible-token-transfer/README.md b/docs/spec/fungible-token-transfer/README.md index 33446f2ebf..d7b1dbf989 100644 --- a/docs/spec/fungible-token-transfer/README.md +++ b/docs/spec/fungible-token-transfer/README.md @@ -2,7 +2,7 @@ This document describes the TLA+ model of the core logic of the English specification [ICS -20](https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer). We +20](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer). We start by discussing [the model of the protocol](#the-model-of-the-protocol). Then this document provides links to our TLA+ formalization of [Properties and @@ -24,16 +24,16 @@ modules](#helper-modules). ### Port and Channel Setup and Channel lifecycle management -In the model we assume that the [`setup()`](https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer#port--channel-setup) function has been called +In the model we assume that the [`setup()`](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#port--channel-setup) function has been called before. The [channel handshake -functions]((https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer#channel-lifecycle-management)) +functions]((https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#channel-lifecycle-management)) are also considered being already executed. Our model starts from a state where the channel handshake has completed successfully. ### Packet Relay -The [core callback functions](https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer#packet-relay) +The [core callback functions](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transferr#packet-relay) `createOutgoingPacket()`, `onRecvPacket()`, `onRecvPacket()` and `onTimeoutPacket()`, as well as the auxiliary function `refundTokens()` are modeled in @@ -53,7 +53,7 @@ discussed here. We will discuss it the last. This module captures the functions specifying packet flow and handling from [ICS -04](https://github.com/cosmos/ics/tree/master/spec/ics-004-channel-and-packet-semantics). +04](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-004-channel-and-packet-semantics). #### [Bank.tla](bank.tla) The bank module encodes functions defined by the Cosmos bank @@ -113,7 +113,7 @@ Next == ### Properties and invariants The English specification provides informal requirements as "[desired properties]( -https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer#desired-properties)". +https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#desired-properties)". #### Preservation of fungibility @@ -124,7 +124,7 @@ on chain B wants to return them, then the tokens can be returned. For this we require the assumption (which is somewhat implicit it its [correctness -argument](https://github.com/cosmos/ics/tree/master/spec/ics-020-fungible-token-transfer#correctness)) that the source chain only performs valid transitions. +argument](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-020-fungible-token-transfer#correctness)) that the source chain only performs valid transitions. This is implemented in the property `ICS20Prop` in the file [IBCTokenTransfer.tla](IBCTokenTransfer.tla). @@ -197,3 +197,14 @@ To import the specification in the TLA+ toolbox and run TLC: - assign a value to the constants - choose "Temporal formula" as the behavior spec, and use the formula `Spec` - run TLC on the model + +### Basic checks + +We ran TLC on the model and verified the invariant `IBC20Inv` in 26 seconds and +the property `IBC20Prop` in four minutes. +We note that the specification currently models two transfers: one from `ChainA` to `ChainB`, and vice versa, in their respective native denominations. +Both chains are correct, and there is no malicious relayer. +The relayer implements the logic from [ICS 18](https://github.com/cosmos/ics/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-018-relayer-algorithms), in particular, it does not +relay timeouts. +However, the packet timeout handlers are specified in [`ICS04PacketHandlers.tla`](ICS04PacketHandlers.tla) +for future use. \ No newline at end of file From ce08ac037685cc6e71075d30149ebc9bbca17687 Mon Sep 17 00:00:00 2001 From: Adi Seredinschi Date: Wed, 2 Dec 2020 17:58:47 +0100 Subject: [PATCH 4/6] Prep for releasing 005 (#435) --- CHANGELOG.md | 88 +++++++++++++++++++++++++++--------------- modules/Cargo.toml | 2 +- relayer-cli/Cargo.toml | 2 +- relayer/Cargo.toml | 2 +- 4 files changed, 60 insertions(+), 34 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e5b06f6174..f79db22df0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,18 +2,28 @@ ## Unreleased Changes -Special thanks to external contributors for this release: @CharlyCst ([#347]). + +## v0.0.5 +*December 2, 2020* + +This release focuses on implementing relayer and relayer-cli functionality towards a full v0 implementation. +We now have the full-stack implementation for supporting client creation & updates, as well as connection- and channel handshakes. +We also consolidated our TLA+ specs into an "IBC Core TLA+ specification," and added ICS 020 spec. + +Special thanks to external contributors for this release: @CharlyCst ([#347], [#419]). ### FEATURES - Update to tendermint-rs version `0.17-RC3` ([#403]) - [changelog] Added "unreleased" section in `CHANGELOG.MD` to help streamline releases ([#274]) -- [relayer] Integrate relayer spike into relayer crate ([#335]) - [modules] - Implement flexible connection id selection ([#332]) - ICS 4 Domain Types for channel handshakes and packets ([#315], [#95]) - Introduce LightBlock support for MockContext ([#389]) -- [relayer] +- [relayer] + - Retrieve account sequence information from a chain using a GRPC client (#337) + - Implementation of chain runtime for v0 ([#330]) + - Integrate relayer spike into relayer crate ([#335]) - Implement `query_header_at_height` via plain RPC queries (no light client verification) ([#336]) - Implement the relayer logic for connection handshake messages ([#358], [#359], [#360]) - Implement the relayer logic for channel handshake messages ([#371], [#372], [#373], [#374]) @@ -22,56 +32,72 @@ Special thanks to external contributors for this release: @CharlyCst ([#347]). - CLI for client update message ([#277]) - Implement the relayer CLI for connection handshake messages ([#358], [#359], [#360]) - Implement the relayer CLI for channel handshake messages ([#371], [#372], [#373], [#374]) + - Added basic client, connection, and channel lifecyle in relayer v0 ([#376], [#377], [#378]) - Implement commands to add and list keys for a chain ([#363]) - - Allow overriding peer_id, height and hash in light add command ([#428]) + - Allow overriding of peer_id, height and hash in light add command ([#428]) - [proto-compiler] - Refactor and allow specifying a commit at which the Cosmos SDK should be checked out ([#366]) - Add a `--tag` option to the `clone-sdk` command to check out a tag instead of a commit ([#369]) -- [ibc-proto] Refactor and allow specifying a commit at which the Cosmos SDK should be checked out ([#366]) + - Fix `--out` command line parameter (instead of `--path`) ([#419]) +- [spec/relayer] + - ICS 020 spec in TLA+ ([#386]) + - Prepare IBC Core TLA+ specs ([#404]) + +### IMPROVEMENTS + +- [relayer] + - Pin chain runtime against Tokio 0.2 by downgrading for 0.3 to avoid dependency hell ([#415], follow up to [#402]) +- [relayer-cli] + - Split tasks spawned by CLI commands into their own modules ([#331]) + - V0 command implementation ([#346]) +- [modules] + - Split `msgs.rs` of ICS002 in separate modules ([#367]) + - Fixed inconsistent versioning for ICS003 and ICS004 ([#97]) + - Fixed `get_sign_bytes` method for messages ([#98]) + - Homogenize ConnectionReader trait so that all functions return owned objects ([#347]) + - Align with tendermint-rs in the domain type definition of `block::Id` ([#338]) + [#95]: https://github.com/informalsystems/ibc-rs/issues/95 +[#97]: https://github.com/informalsystems/ibc-rs/issues/97 +[#98]: https://github.com/informalsystems/ibc-rs/issues/98 [#274]: https://github.com/informalsystems/ibc-rs/issues/274 +[#277]: https://github.com/informalsystems/ibc-rs/issues/277 [#315]: https://github.com/informalsystems/ibc-rs/issues/315 +[#330]: https://github.com/informalsystems/ibc-rs/issues/330 [#332]: https://github.com/informalsystems/ibc-rs/issues/332 -[#335]: https://github.com/informalsystems/ibc-rs/pulls/335 +[#335]: https://github.com/informalsystems/ibc-rs/pull/335 [#336]: https://github.com/informalsystems/ibc-rs/issues/336 -[#348]: https://github.com/informalsystems/ibc-rs/pulls/348 +[#337]: https://github.com/informalsystems/ibc-rs/issues/337 +[#338]: https://github.com/informalsystems/ibc-rs/issues/338 +[#346]: https://github.com/informalsystems/ibc-rs/issues/346 +[#347]: https://github.com/informalsystems/ibc-rs/issues/347 +[#348]: https://github.com/informalsystems/ibc-rs/pull/348 [#358]: https://github.com/informalsystems/ibc-rs/issues/358 -[#358]: https://github.com/informalsystems/ibc-rs/issues/359 -[#358]: https://github.com/informalsystems/ibc-rs/issues/360 +[#359]: https://github.com/informalsystems/ibc-rs/issues/359 +[#360]: https://github.com/informalsystems/ibc-rs/issues/360 [#363]: https://github.com/informalsystems/ibc-rs/issues/363 [#366]: https://github.com/informalsystems/ibc-rs/issues/366 +[#367]: https://github.com/informalsystems/ibc-rs/issues/367 [#368]: https://github.com/informalsystems/ibc-rs/issues/368 -[#369]: https://github.com/informalsystems/ibc-rs/pulls/369 +[#369]: https://github.com/informalsystems/ibc-rs/pull/369 [#371]: https://github.com/informalsystems/ibc-rs/issues/371 [#372]: https://github.com/informalsystems/ibc-rs/issues/372 [#373]: https://github.com/informalsystems/ibc-rs/issues/373 [#374]: https://github.com/informalsystems/ibc-rs/issues/374 +[#376]: https://github.com/informalsystems/ibc-rs/issues/376 +[#377]: https://github.com/informalsystems/ibc-rs/issues/377 +[#378]: https://github.com/informalsystems/ibc-rs/issues/378 +[#386]: https://github.com/informalsystems/ibc-rs/issues/386 [#389]: https://github.com/informalsystems/ibc-rs/issues/389 +[#402]: https://github.com/informalsystems/ibc-rs/issues/402 [#403]: https://github.com/informalsystems/ibc-rs/issues/403 +[#404]: https://github.com/informalsystems/ibc-rs/issues/404 +[#419]: https://github.com/informalsystems/ibc-rs/issues/419 +[#415]: https://github.com/informalsystems/ibc-rs/issues/415 [#428]: https://github.com/informalsystems/ibc-rs/issues/428 -[proto-compiler]: https://github.com/informalsystems/ibc-rs/tree/master/proto-compiler - -### IMPROVEMENTS - -- [relayer-cli] - - Split tasks spawned by CLI commands into their own modules ([#331]) - - V0 command implementation ([#346]) -- [modules] - - Homogenize ConnectionReader trait so that all functions return owned objects ([#347]) - - Align with tendermint-rs in the domain type definition of `block::Id` ([#338]) - -[#274]: https://github.com/informalsystems/ibc-rs/issues/274 -[#277]: https://github.com/informalsystems/ibc-rs/issues/277 -[#331]: https://github.com/informalsystems/ibc-rs/pulls/331 -[#332]: https://github.com/informalsystems/ibc-rs/issues/332 -[#335]: https://github.com/informalsystems/ibc-rs/pulls/335 -[#336]: https://github.com/informalsystems/ibc-rs/issues/336 -[#338]: https://github.com/informalsystems/ibc-rs/issues/338 -[#347]: https://github.com/informalsystems/ibc-rs/issues/347 -[#346]: https://github.com/informalsystems/ibc-rs/issues/346 -[#348]: https://github.com/informalsystems/ibc-rs/pulls/348 [changelog]: https://github.com/informalsystems/ibc-rs/tree/master/CHANGELOG.md +[proto-compiler]: https://github.com/informalsystems/ibc-rs/tree/master/proto-compiler ## v0.0.4 *October 19, 2020* diff --git a/modules/Cargo.toml b/modules/Cargo.toml index 5aeee146a5..664cf45e61 100644 --- a/modules/Cargo.toml +++ b/modules/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "ibc" -version = "0.0.4" +version = "0.0.5" edition = "2018" license = "Apache-2.0" readme = "README.md" diff --git a/relayer-cli/Cargo.toml b/relayer-cli/Cargo.toml index d16eaa9da2..ba4fd6ea3d 100644 --- a/relayer-cli/Cargo.toml +++ b/relayer-cli/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "relayer-cli" -version = "0.0.4" +version = "0.0.5" edition = "2018" authors = [ "Informal Systems " diff --git a/relayer/Cargo.toml b/relayer/Cargo.toml index 590f36f830..37e0545a34 100644 --- a/relayer/Cargo.toml +++ b/relayer/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "relayer" -version = "0.0.4" +version = "0.0.5" edition = "2018" authors = [ "Informal Systems " From a473bec7733e6448d1f2d0be29dd92a198660a82 Mon Sep 17 00:00:00 2001 From: Adi Seredinschi Date: Wed, 2 Dec 2020 18:40:55 +0100 Subject: [PATCH 5/6] Bump up proto crate version & deps. (#436) --- modules/Cargo.toml | 2 +- proto/Cargo.toml | 2 +- relayer/Cargo.toml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/modules/Cargo.toml b/modules/Cargo.toml index 664cf45e61..58baeefdaa 100644 --- a/modules/Cargo.toml +++ b/modules/Cargo.toml @@ -21,7 +21,7 @@ mocks = [ "tendermint-testgen" ] [dependencies] # Proto definitions for all IBC-related interfaces, e.g., connections or channels. -ibc-proto = { version = "0.4.0", path = "../proto" } +ibc-proto = { version = "0.5.0", path = "../proto" } anomaly = "0.2.0" chrono = "0.4" diff --git a/proto/Cargo.toml b/proto/Cargo.toml index bc7cb07746..01215b7e89 100644 --- a/proto/Cargo.toml +++ b/proto/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "ibc-proto" -version = "0.4.0" +version = "0.5.0" authors = ["Greg Szabo "] edition = "2018" license = "Apache-2.0" diff --git a/relayer/Cargo.toml b/relayer/Cargo.toml index 37e0545a34..60f0030985 100644 --- a/relayer/Cargo.toml +++ b/relayer/Cargo.toml @@ -8,7 +8,7 @@ authors = [ [dependencies] ibc = { path = "../modules" } -ibc-proto = { version = "0.4.0", path = "../proto" } +ibc-proto = { version = "0.5.0", path = "../proto" } anomaly = "0.2.0" async-trait = "0.1.24" humantime-serde = "1.0.0" From be001ebddcc064e1473ffe758a9718ee43b83151 Mon Sep 17 00:00:00 2001 From: Anca Zamfir Date: Wed, 2 Dec 2020 22:30:09 +0100 Subject: [PATCH 6/6] Changes for the tendermint dep rebase (#437) * Changes for the tendermint dep rebase * error format * Changes for integration with tm pr#706 * remove event_monitor.rs file --- Cargo.toml | 3 +- modules/src/ics07_tendermint/header.rs | 2 +- relayer/src/chain/cosmos.rs | 30 +---- relayer/src/event/monitor.rs | 8 +- relayer/src/event_monitor.rs | 156 ------------------------- 5 files changed, 10 insertions(+), 189 deletions(-) delete mode 100644 relayer/src/event_monitor.rs diff --git a/Cargo.toml b/Cargo.toml index 39e6021cfb..549ac13f08 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -16,4 +16,5 @@ exclude = [ tendermint = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } tendermint-rpc = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } tendermint-proto = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } -tendermint-light-client = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } \ No newline at end of file +tendermint-light-client = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } +tendermint-testgen = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/skip-verif" } \ No newline at end of file diff --git a/modules/src/ics07_tendermint/header.rs b/modules/src/ics07_tendermint/header.rs index 1014fe4498..9be97b1f9a 100644 --- a/modules/src/ics07_tendermint/header.rs +++ b/modules/src/ics07_tendermint/header.rs @@ -132,7 +132,7 @@ pub mod test_util { 281_815_u64.try_into().unwrap(), ); - let vs = ValidatorSet::new(vec![v1], Some(v1), 281_815_u64.try_into().unwrap()); + let vs = ValidatorSet::new(vec![v1], Some(v1), None); Header { signed_header: shdr, diff --git a/relayer/src/chain/cosmos.rs b/relayer/src/chain/cosmos.rs index de5f09d5c7..d80dafef52 100644 --- a/relayer/src/chain/cosmos.rs +++ b/relayer/src/chain/cosmos.rs @@ -1,4 +1,4 @@ -use std::convert::{TryFrom, TryInto}; +use std::convert::TryFrom; use std::future::Future; use std::str::FromStr; use std::sync::{Arc, Mutex}; @@ -19,7 +19,7 @@ use tendermint::account::Id as AccountId; use tendermint::block::Height; use tendermint::consensus::Params; -use tendermint_light_client::types::{LightBlock as TMLightBlock, ValidatorSet}; +use tendermint_light_client::types::LightBlock as TMLightBlock; use tendermint_rpc::Client; use tendermint_rpc::HttpClient; @@ -376,8 +376,8 @@ impl Chain for CosmosSDKChain { Ok(TMHeader { trusted_height, signed_header: target_light_block.signed_header.clone(), - validator_set: fix_validator_set(&target_light_block)?, - trusted_validator_set: fix_validator_set(&trusted_light_block)?, + validator_set: target_light_block.validators, + trusted_validator_set: trusted_light_block.validators, }) } @@ -411,28 +411,6 @@ impl Chain for CosmosSDKChain { } } -fn fix_validator_set(light_block: &TMLightBlock) -> Result { - let validators = light_block.validators.validators(); - // Get the proposer. - let proposer = validators - .iter() - .find(|v| v.address == light_block.signed_header.header.proposer_address) - .ok_or(Kind::EmptyResponseValue)?; - - let voting_power: u64 = validators.iter().map(|v| v.voting_power.value()).sum(); - - // Create the validator set with the proposer from the header. - // This is required by IBC on-chain validation. - let validator_set = ValidatorSet::new( - validators.clone(), - Some(*proposer), - voting_power - .try_into() - .map_err(|e| Kind::EmptyResponseValue.context(e))?, - ); - Ok(validator_set) -} - /// Perform a generic `abci_query`, and return the corresponding deserialized response data. async fn abci_query( chain: &CosmosSDKChain, diff --git a/relayer/src/event/monitor.rs b/relayer/src/event/monitor.rs index 673d4eeab4..561b9d9f4e 100644 --- a/relayer/src/event/monitor.rs +++ b/relayer/src/event/monitor.rs @@ -134,11 +134,9 @@ impl EventMonitor { // Shut down previous client debug!("Gracefully shutting down previous client"); - self.rt - .lock() - .map_err(|_| Kind::PoisonedMutex)? - .block_on(websocket_client.close()) - .map_err(|e| format!("Failed to close previous WebSocket client: {}", e))?; + if let Err(e) = websocket_client.close() { + error!("Previous websocket client closing failure {}", e); + } self.rt .lock() diff --git a/relayer/src/event_monitor.rs b/relayer/src/event_monitor.rs deleted file mode 100644 index a2a7e0c62a..0000000000 --- a/relayer/src/event_monitor.rs +++ /dev/null @@ -1,156 +0,0 @@ -use ibc::events::IBCEvent; -use tendermint::{chain, net, Error as TMError}; -use tendermint_rpc::{ - query::EventType, query::Query, Subscription, SubscriptionClient, WebSocketClient, -}; -use tokio::stream::StreamExt; -use tokio::sync::mpsc::Sender; - -use futures::{stream::select_all, Stream}; -use tokio::task::JoinHandle; -use tracing::{debug, error, info}; - -type SubscriptionResult = Result; -type SubscriptionStream = dyn Stream + Send + Sync + Unpin; - -/// Connect to a TM node, receive push events over a websocket and filter them for the -/// event handler. -pub struct EventMonitor { - chain_id: chain::Id, - /// WebSocket to collect events from - websocket_client: WebSocketClient, - /// Async task handle for the WebSocket client's driver - websocket_driver_handle: JoinHandle>, - /// Channel to handler where the monitor for this chain sends the events - channel_to_handler: Sender<(chain::Id, Vec)>, - /// Node Address - node_addr: net::Address, - /// Queries - event_queries: Vec, - /// All subscriptions combined in a single stream - subscriptions: Box, -} - -impl EventMonitor { - /// Create an event monitor, connect to a node and subscribe to queries. - pub async fn create( - chain_id: chain::Id, - rpc_addr: net::Address, - channel_to_handler: Sender<(chain::Id, Vec)>, - ) -> Result> { - let (websocket_client, websocket_driver) = WebSocketClient::new(rpc_addr.clone()).await?; - let websocket_driver_handle = tokio::spawn(async move { websocket_driver.run().await }); - - // TODO: move them to config file(?) - let event_queries = vec![Query::from(EventType::Tx), Query::from(EventType::NewBlock)]; - - Ok(EventMonitor { - chain_id, - websocket_client, - websocket_driver_handle, - channel_to_handler, - node_addr: rpc_addr.clone(), - event_queries, - subscriptions: Box::new(futures::stream::empty()), - }) - } - - /// Clear the current subscriptions, and subscribe again to all queries. - pub async fn subscribe(&mut self) -> Result<(), Box> { - let mut subscriptions = vec![]; - - for query in &self.event_queries { - let subscription = self.websocket_client.subscribe(query.clone()).await?; - subscriptions.push(subscription); - } - - self.subscriptions = Box::new(select_all(subscriptions)); - - Ok(()) - } - - /// Event monitor loop - pub async fn run(&mut self) { - info!(chain.id = % self.chain_id, "running listener for"); - - loop { - match self.collect_events().await { - Ok(..) => continue, - Err(err) => { - debug!("Web socket error: {}", err); - - // Try to reconnect - let (mut websocket_client, websocket_driver) = - WebSocketClient::new(self.node_addr.clone()) - .await - .unwrap_or_else(|e| { - debug!("Error on reconnection: {}", e); - panic!("Abort on failed reconnection"); - }); - let mut websocket_driver_handle = - tokio::spawn(async move { websocket_driver.run().await }); - - // Swap the new client with the previous one which failed, - // so that we can shut the latter down gracefully. - std::mem::swap(&mut self.websocket_client, &mut websocket_client); - std::mem::swap( - &mut self.websocket_driver_handle, - &mut websocket_driver_handle, - ); - - debug!("Reconnected"); - - // Shut down previous client - debug!("Gracefully shutting down previous client"); - websocket_client.close().await.unwrap_or_else(|e| { - error!("Failed to close previous WebSocket client: {}", e); - }); - websocket_driver_handle - .await - .unwrap_or_else(|e| { - Err(tendermint_rpc::Error::client_internal_error(format!( - "failed to terminate previous WebSocket client driver: {}", - e - ))) - }) - .unwrap_or_else(|e| { - error!("Previous WebSocket client driver failed with error: {}", e); - }); - - // Try to resubscribe - if let Err(err) = self.subscribe().await { - debug!("Error on recreating subscriptions: {}", err); - panic!("Abort during reconnection"); - }; - } - } - } - } - - /// Collect the IBC events from the subscriptions - pub async fn collect_events(&mut self) -> Result<(), TMError> { - tokio::select! { - Some(event) = self.subscriptions.next() => { - match event { - Ok(event) => { - match ibc::events::get_all_events(event.clone()) { - Ok(ibc_events) => { - self.channel_to_handler - .send((self.chain_id.clone(), ibc_events)) - .await? - }, - Err(err) => { - error!("Error {} when extracting IBC events from {:?}: ", err, event); - } - } - } - Err(err) => { - error!("Error on collecting events from subscriptions: {}", err); - } - } - }, - } - - Ok(()) - } -} \ No newline at end of file