Reorg IBC specs (#439)

informalsystems · Dec 3, 2020 · 15bac8c · 15bac8c
1 parent 8ddc688
commit 15bac8c
Show file tree

Hide file tree

Showing 19 changed files with 4 additions and 2 deletions.
diff --git 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 → ...spec/tla/fungible-token-transfer/Bank.tla b/docs/spec/fungible-token-transfer/Bank.tla → ...spec/tla/fungible-token-transfer/Bank.tla
diff --git a/docs/spec/fungible-token-transfer/Chain.tla → ...pec/tla/fungible-token-transfer/Chain.tla b/docs/spec/fungible-token-transfer/Chain.tla → ...pec/tla/fungible-token-transfer/Chain.tla
diff --git a/...gible-token-transfer/IBCTokenTransfer.tla → ...gible-token-transfer/IBCTokenTransfer.tla b/...gible-token-transfer/IBCTokenTransfer.tla → ...gible-token-transfer/IBCTokenTransfer.tla
diff --git a/...-transfer/IBCTokenTransferDefinitions.tla → ...-transfer/IBCTokenTransferDefinitions.tla b/...-transfer/IBCTokenTransferDefinitions.tla → ...-transfer/IBCTokenTransferDefinitions.tla
diff --git a/...le-token-transfer/ICS04PacketHandlers.tla → ...le-token-transfer/ICS04PacketHandlers.tla b/...le-token-transfer/ICS04PacketHandlers.tla → ...le-token-transfer/ICS04PacketHandlers.tla
diff --git a/...er/ICS20FungibleTokenTransferHandlers.tla → ...er/ICS20FungibleTokenTransferHandlers.tla b/...er/ICS20FungibleTokenTransferHandlers.tla → ...er/ICS20FungibleTokenTransferHandlers.tla
diff --git a/docs/spec/fungible-token-transfer/README.md → ...pec/tla/fungible-token-transfer/README.md b/docs/spec/fungible-token-transfer/README.md → ...pec/tla/fungible-token-transfer/README.md
diff --git a/docs/spec/relayer/tla/Chain.tla → docs/spec/tla/ibc-core/Chain.tla b/docs/spec/relayer/tla/Chain.tla → docs/spec/tla/ibc-core/Chain.tla
diff --git a/docs/spec/relayer/tla/IBCCore.tla → docs/spec/tla/ibc-core/IBCCore.tla b/docs/spec/relayer/tla/IBCCore.tla → docs/spec/tla/ibc-core/IBCCore.tla
diff --git a/docs/spec/relayer/tla/IBCCoreDefinitions.tla → .../spec/tla/ibc-core/IBCCoreDefinitions.tla b/docs/spec/relayer/tla/IBCCoreDefinitions.tla → .../spec/tla/ibc-core/IBCCoreDefinitions.tla
diff --git a/.../spec/relayer/tla/ICS02ClientHandlers.tla → ...spec/tla/ibc-core/ICS02ClientHandlers.tla b/.../spec/relayer/tla/ICS02ClientHandlers.tla → ...spec/tla/ibc-core/ICS02ClientHandlers.tla
diff --git a/...c/relayer/tla/ICS03ConnectionHandlers.tla → .../tla/ibc-core/ICS03ConnectionHandlers.tla b/...c/relayer/tla/ICS03ConnectionHandlers.tla → .../tla/ibc-core/ICS03ConnectionHandlers.tla
diff --git a/...spec/relayer/tla/ICS04ChannelHandlers.tla → ...pec/tla/ibc-core/ICS04ChannelHandlers.tla b/...spec/relayer/tla/ICS04ChannelHandlers.tla → ...pec/tla/ibc-core/ICS04ChannelHandlers.tla
diff --git a/.../spec/relayer/tla/ICS04PacketHandlers.tla → ...spec/tla/ibc-core/ICS04PacketHandlers.tla b/.../spec/relayer/tla/ICS04PacketHandlers.tla → ...spec/tla/ibc-core/ICS04PacketHandlers.tla
diff --git a/docs/spec/relayer/tla/ICS18Environment.cfg → docs/spec/tla/ibc-core/ICS18Environment.cfg b/docs/spec/relayer/tla/ICS18Environment.cfg → docs/spec/tla/ibc-core/ICS18Environment.cfg
diff --git a/...relayer/tla/ICS18Environment_apalache.tla → ...la/ibc-core/ICS18Environment_apalache.tla b/...relayer/tla/ICS18Environment_apalache.tla → ...la/ibc-core/ICS18Environment_apalache.tla
diff --git a/docs/spec/relayer/tla/ICS18Relayer.tla → docs/spec/tla/ibc-core/ICS18Relayer.tla b/docs/spec/relayer/tla/ICS18Relayer.tla → docs/spec/tla/ibc-core/ICS18Relayer.tla
diff --git a/docs/spec/relayer/tla/README.md → docs/spec/tla/ibc-core/README.md b/docs/spec/relayer/tla/README.md → docs/spec/tla/ibc-core/README.md