From 18c69df77916713d8c345217aed0fcd1fd4dc8c8 Mon Sep 17 00:00:00 2001 From: Zarko Milosevic Date: Thu, 3 Dec 2020 15:54:36 +0100 Subject: [PATCH] Reorg IBC specs --- docs/spec/README.md | 6 ++++-- docs/spec/{ => tla}/fungible-token-transfer/Bank.tla | 0 docs/spec/{ => tla}/fungible-token-transfer/Chain.tla | 0 .../{ => tla}/fungible-token-transfer/IBCTokenTransfer.tla | 0 .../fungible-token-transfer/IBCTokenTransferDefinitions.tla | 0 .../fungible-token-transfer/ICS04PacketHandlers.tla | 0 .../ICS20FungibleTokenTransferHandlers.tla | 0 docs/spec/{ => tla}/fungible-token-transfer/README.md | 0 docs/spec/{relayer/tla => tla/ibc-core}/Chain.tla | 0 docs/spec/{relayer/tla => tla/ibc-core}/IBCCore.tla | 0 .../{relayer/tla => tla/ibc-core}/IBCCoreDefinitions.tla | 0 .../{relayer/tla => tla/ibc-core}/ICS02ClientHandlers.tla | 0 .../tla => tla/ibc-core}/ICS03ConnectionHandlers.tla | 0 .../{relayer/tla => tla/ibc-core}/ICS04ChannelHandlers.tla | 0 .../{relayer/tla => tla/ibc-core}/ICS04PacketHandlers.tla | 0 .../spec/{relayer/tla => tla/ibc-core}/ICS18Environment.cfg | 0 .../tla => tla/ibc-core}/ICS18Environment_apalache.tla | 0 docs/spec/{relayer/tla => tla/ibc-core}/ICS18Relayer.tla | 0 docs/spec/{relayer/tla => tla/ibc-core}/README.md | 0 19 files changed, 4 insertions(+), 2 deletions(-) rename docs/spec/{ => tla}/fungible-token-transfer/Bank.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/Chain.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/IBCTokenTransfer.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/IBCTokenTransferDefinitions.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/ICS04PacketHandlers.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla (100%) rename docs/spec/{ => tla}/fungible-token-transfer/README.md (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/Chain.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/IBCCore.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/IBCCoreDefinitions.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS02ClientHandlers.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS03ConnectionHandlers.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS04ChannelHandlers.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS04PacketHandlers.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS18Environment.cfg (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS18Environment_apalache.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/ICS18Relayer.tla (100%) rename docs/spec/{relayer/tla => tla/ibc-core}/README.md (100%) diff --git a/docs/spec/README.md b/docs/spec/README.md index 4f3e71fec9..6adf6bb24d 100644 --- a/docs/spec/README.md +++ b/docs/spec/README.md @@ -1,5 +1,7 @@ # Specification and verification of IBC protocols - * [relayer](./relayer) comprises TLA+ specification for the IBC relayer algorithms (ICS 018). + * [tla](./tla) comprises TLA+ specification for the IBC specification. - * [connection-handshake](./connection-handshake) contains English and TLA+ specifications for the IBC Connection Handshake Protocol (ICS 003). + * [connection-handshake](./connection-handshake) [Deprecated] contains English and TLA+ specifications for the IBC Connection Handshake Protocol (ICS 003). + + * [relayer](./relayer) contains English specification of the relayer. diff --git a/docs/spec/fungible-token-transfer/Bank.tla b/docs/spec/tla/fungible-token-transfer/Bank.tla similarity index 100% rename from docs/spec/fungible-token-transfer/Bank.tla rename to docs/spec/tla/fungible-token-transfer/Bank.tla diff --git a/docs/spec/fungible-token-transfer/Chain.tla b/docs/spec/tla/fungible-token-transfer/Chain.tla similarity index 100% rename from docs/spec/fungible-token-transfer/Chain.tla rename to docs/spec/tla/fungible-token-transfer/Chain.tla diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransfer.tla b/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla similarity index 100% rename from docs/spec/fungible-token-transfer/IBCTokenTransfer.tla rename to docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla diff --git a/docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla b/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla similarity index 100% rename from docs/spec/fungible-token-transfer/IBCTokenTransferDefinitions.tla rename to docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla diff --git a/docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla b/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla similarity index 100% rename from docs/spec/fungible-token-transfer/ICS04PacketHandlers.tla rename to docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla diff --git a/docs/spec/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla b/docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla similarity index 100% rename from docs/spec/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla rename to docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla diff --git a/docs/spec/fungible-token-transfer/README.md b/docs/spec/tla/fungible-token-transfer/README.md similarity index 100% rename from docs/spec/fungible-token-transfer/README.md rename to docs/spec/tla/fungible-token-transfer/README.md diff --git a/docs/spec/relayer/tla/Chain.tla b/docs/spec/tla/ibc-core/Chain.tla similarity index 100% rename from docs/spec/relayer/tla/Chain.tla rename to docs/spec/tla/ibc-core/Chain.tla diff --git a/docs/spec/relayer/tla/IBCCore.tla b/docs/spec/tla/ibc-core/IBCCore.tla similarity index 100% rename from docs/spec/relayer/tla/IBCCore.tla rename to docs/spec/tla/ibc-core/IBCCore.tla diff --git a/docs/spec/relayer/tla/IBCCoreDefinitions.tla b/docs/spec/tla/ibc-core/IBCCoreDefinitions.tla similarity index 100% rename from docs/spec/relayer/tla/IBCCoreDefinitions.tla rename to docs/spec/tla/ibc-core/IBCCoreDefinitions.tla diff --git a/docs/spec/relayer/tla/ICS02ClientHandlers.tla b/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla similarity index 100% rename from docs/spec/relayer/tla/ICS02ClientHandlers.tla rename to docs/spec/tla/ibc-core/ICS02ClientHandlers.tla diff --git a/docs/spec/relayer/tla/ICS03ConnectionHandlers.tla b/docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla similarity index 100% rename from docs/spec/relayer/tla/ICS03ConnectionHandlers.tla rename to docs/spec/tla/ibc-core/ICS03ConnectionHandlers.tla diff --git a/docs/spec/relayer/tla/ICS04ChannelHandlers.tla b/docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla similarity index 100% rename from docs/spec/relayer/tla/ICS04ChannelHandlers.tla rename to docs/spec/tla/ibc-core/ICS04ChannelHandlers.tla diff --git a/docs/spec/relayer/tla/ICS04PacketHandlers.tla b/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla similarity index 100% rename from docs/spec/relayer/tla/ICS04PacketHandlers.tla rename to docs/spec/tla/ibc-core/ICS04PacketHandlers.tla diff --git a/docs/spec/relayer/tla/ICS18Environment.cfg b/docs/spec/tla/ibc-core/ICS18Environment.cfg similarity index 100% rename from docs/spec/relayer/tla/ICS18Environment.cfg rename to docs/spec/tla/ibc-core/ICS18Environment.cfg diff --git a/docs/spec/relayer/tla/ICS18Environment_apalache.tla b/docs/spec/tla/ibc-core/ICS18Environment_apalache.tla similarity index 100% rename from docs/spec/relayer/tla/ICS18Environment_apalache.tla rename to docs/spec/tla/ibc-core/ICS18Environment_apalache.tla diff --git a/docs/spec/relayer/tla/ICS18Relayer.tla b/docs/spec/tla/ibc-core/ICS18Relayer.tla similarity index 100% rename from docs/spec/relayer/tla/ICS18Relayer.tla rename to docs/spec/tla/ibc-core/ICS18Relayer.tla diff --git a/docs/spec/relayer/tla/README.md b/docs/spec/tla/ibc-core/README.md similarity index 100% rename from docs/spec/relayer/tla/README.md rename to docs/spec/tla/ibc-core/README.md