From 1ac8a4b38e7f3ad939686fbe22401fe49350e207 Mon Sep 17 00:00:00 2001 From: Christopher Goes Date: Sat, 21 Apr 2018 14:33:21 +0200 Subject: [PATCH] Connection / channel / packet clarifications --- docs/spec/ibc/README.md | 2 +- docs/spec/ibc/appendices.md | 2 +- docs/spec/ibc/channels-and-packets.md | 166 +++++++++++++------------- docs/spec/ibc/connections.md | 28 +++-- 4 files changed, 101 insertions(+), 97 deletions(-) diff --git a/docs/spec/ibc/README.md b/docs/spec/ibc/README.md index eca34c80d..332bf9141 100644 --- a/docs/spec/ibc/README.md +++ b/docs/spec/ibc/README.md @@ -4,7 +4,7 @@ This paper specifies the Cosmos Inter-Blockchain Communication (IBC) protocol. The IBC protocol defines a set of semantics for authenticated, strictly-ordered message passing between two blockchains with independent consensus algorithms. -The core IBC protocol is payload-agnostic. On top of IBC, developers can implement the semantics of a particular application, enabling users to transfer valuable assets between different blockchains while preserving, under particular security assumptions of the underlying blockchains, the contractual guarantees of the asset in question - such as scarcity and fungibility for a currency or global uniqueness for a digital kitty-cat. +The core IBC protocol is payload-agnostic. On top of IBC, developers can implement the semantics of a particular application, enabling users to transfer valuable assets between different blockchains while preserving the contractual guarantees of the asset in question - such as scarcity and fungibility for a currency or global uniqueness for a digital kitty-cat. IBC requires two blockchains with cheaply verifiable rapid finality and Merkle tree substate proofs. The protocol makes no assumptions of block confirmation times or maximum network latency of packet transmissions, and the two consensus algorithms remain completely independent. Each chain maintains a local partial order and inter-chain message sequencing ensures cross-chain linearity. Once the two chains have registered a trust relationship, cryptographically verifiable packets can be sent between them. diff --git a/docs/spec/ibc/appendices.md b/docs/spec/ibc/appendices.md index 736167d2a..14e4ebde6 100644 --- a/docs/spec/ibc/appendices.md +++ b/docs/spec/ibc/appendices.md @@ -74,7 +74,7 @@ In order to prove a merkle root, we must fully define the headers, signatures, a Building Blocks: Header, PubKey, Signature, Commit, ValidatorSet --> needs input/support from Tendermint Core team (and go-crypto) +→ needs input/support from Tendermint Core team (and go-crypto) Registering Chain diff --git a/docs/spec/ibc/channels-and-packets.md b/docs/spec/ibc/channels-and-packets.md index 128a0c01a..353bf7d20 100644 --- a/docs/spec/ibc/channels-and-packets.md +++ b/docs/spec/ibc/channels-and-packets.md @@ -6,29 +6,29 @@ IBC uses a cross-chain message passing model that makes no assumptions about network synchrony. IBC *data packets* (hereafter just *packets*) are relayed from one blockchain to the other by external infrastructure. Chain `A` and chain `B` confirm new blocks independently, and packets from one chain to the other may be delayed or censored arbitrarily. The speed of packet transmission and confirmation is limited only by the speed of the underlying chains. -The IBC protocol as defined here is payload-agnostic. The packet receiver on chain `B` decides how to act upon the incoming message, and may add its own application logic to determine which state transactions to apply according to what data the packet contains. Both chains must only agree that the packet has been received and either accepted or rejected. +The IBC protocol as defined here is payload-agnostic. The packet receiver on chain `B` decides how to act upon the incoming message, and may add its own application logic to determine which state transactions to apply according to what data the packet contains. Both chains must only agree that the packet has been received. To facilitate useful application logic, we introduce an IBC *channel*: a set of reliable messaging queues that allows us to guarantee a cross-chain causal ordering[[5](./references.md#5)] of IBC packets. Causal ordering means that if packet *x* is processed before packet *y* on chain `A`, packet *x* must also be processed before packet *y* on chain `B`. -IBC channels implement a vector clock[[2](references.md#2)] for the restricted case of two processes (in our case, blockchains). Given *x* -> *y* means *x* is causally before *y*, chains `A` and `B`, and *a* => *b* means *a* implies *b*: +IBC channels implement a vector clock[[2](references.md#2)] for the restricted case of two processes (in our case, blockchains). Given *x* → *y* means *x* is causally before *y*, chains `A` and `B`, and *a* ⇒ *b* means *a* implies *b*: -*A:send(msgi )* -> *B:receive(msgi )* +*A:send(msgi )* → *B:receive(msgi )* -*B:receive(msgi )* -> *A:receipt(msgi )* +*B:receive(msgi )* → *A:receipt(msgi )* -*A:send(msgi )* -> *A:send(msgi+1 )* +*A:send(msgi )* → *A:send(msgi+1 )* -*x* -> *A:send(msgi )* => -*x* -> *B:receive(msgi )* +*x* → *A:send(msgi )* ⇒ +*x* → *B:receive(msgi )* -*y* -> *B:receive(msgi )* => -*y* -> *A:receipt(msgi )* +*y* → *B:receive(msgi )* ⇒ +*y* → *A:receipt(msgi )* Every transaction on the same chain already has a well-defined causality relation (order in history). IBC provides an ordering guarantee across two chains which can be used to reason about the combined state of both chains as a whole. For example, an application may wish to allow a single tokenized asset to be transferred between and held on multiple blockchains while preserving fungibility and conservation of supply. The application can mint asset vouchers on chain `B` when a particular IBC packet is committed to chain `B`, and require outgoing sends of that packet on chain `A` to escrow an equal amount of the asset on chain `A` until the vouchers are later redeemed back to chain `A` with an IBC packet in the reverse direction. This ordering guarantee along with correct application logic can ensure that total supply is preserved across both chains and that any vouchers minted on chain `B` can later be redeemed back to chain `A`. -This section provides definitions for packets and channels, a high-level specification of the queue interface, and a list of the necessary proofs. To implement wire-compatible IBC, chain `A` and chain `B` must also use a common encoding format. An example binary encoding format can be found in [Appendix C](appendices.md#appendix-c-merkle-proof-format). +This section provides definitions for packets and channels, a high-level specification of the queue interface, and a list of the necessary proofs. To implement wire-compatible IBC, chain `A` and chain `B` must also use a common encoding format. An example binary encoding format can be found in [Appendix C](appendices.md#appendix-c-merkle-proof-formats). ### 3.2 Definitions @@ -56,11 +56,11 @@ We define an IBC *receipt* `R` as the four-tuple `(sequence, source, destination `destination` is a string uniquely identifying the chain, connection, and channel which should receive this packet -`result` is a code of either `success` or `failure` +`result` is an opaque application result payload #### 3.2.3 Queue -To implement strict message ordering, we introduce an ordered *queue*. A queue can be conceptualized as a slice of an infinite array. Two numerical indices - `q_head` and `q_tail` - bound the slice, such that for every `index` where `q_head <= index < q_tail`, there is a queue element `q[q_index]`. Elements can be appended to the tail (end) and removed from the head (beginning). We introduce one further method, `advance`, to facilitate efficient queue cleanup. +To implement strict message ordering, we introduce an ordered *queue*. A queue can be conceptualized as a slice of an infinite array. Two numerical indices - `q_head` and `q_tail` - bound the slice, such that for every `index` where `q_head <= index < q_tail`, there is a queue element `q[index]`. Elements can be appended to the tail (end) and removed from the head (beginning). We introduce one further method, `advance`, to facilitate efficient queue cleanup. Each IBC-supporting blockchain must provide a queue abstraction with the following functionality: @@ -71,31 +71,31 @@ set q_head = 0 set q_tail = 0 ``` -`peek => e` +`peek ⇒ e` ``` match q_head == q_tail with - true => return nil - false => + true ⇒ return nil + false ⇒ return q[q_head] ``` -`pop => e` +`pop ⇒ e` ``` match q_head == q_tail with - true => return nil - false => + true ⇒ return nil + false ⇒ set q_head = q_head + 1 return q_head - 1 ``` -`retrieve(i) => e` +`retrieve(i) ⇒ e` ``` match q_head <= i < q_tail with - true => return q[i] - false => return nil + true ⇒ return q[i] + false ⇒ return nil ``` `push(e)` @@ -112,13 +112,13 @@ set q_head = i set q_tail = max(q_tail, i) ``` -`head => i` +`head ⇒ i` ``` return q_head ``` -`tail => i` +`tail ⇒ i` ``` return q_tail @@ -132,11 +132,11 @@ An IBC channel consists of four distinct queues, two on each chain: `outgoing_A`: Outgoing IBC packets from chain `A` to chain `B`, stored on chain `A` -`incoming_A`: IBC receipts (execution logs) for incoming IBC packets from chain `B`, stored on chain `A` +`incoming_A`: IBC receipts for incoming IBC packets from chain `B`, stored on chain `A` `outgoing_B`: Outgoing IBC packets from chain `B` to chain `A`, stored on chain `B` -`incoming_B`: IBC receipts (execution logs) for incoming IBC packets from chain `A`, stored on chain `B` +`incoming_B`: IBC receipts for incoming IBC packets from chain `A`, stored on chain `B` ### 3.3 Requirements @@ -148,72 +148,78 @@ We use the previously-defined Merkle proof `M_kvh` to provide the requisite proo The index is stored as a fixed-length unsigned integer in big endian format, so that the lexicographical order of the byte representation of the key is consistent with their sequence number. This allows us to quickly iterate over the queue, as well as prove the content of a packet (or lack of packet) at a given sequence. `head` and `tail` are two special constants that store an integer index, and are chosen such that their serializated representation cannot collide with that of any possible index. -Once written to the queue, a packet must be immutable (except for deletion when popped from the queue). That is, if a value `v` is written to a queue, then every valid proof `M_kvh` must refer to the same `v`. In practice, this means that an IBC implementation must ensure that only the IBC module can write to the IBC subspace of the blockchain's Merkle store. This property is essential to safely process asynchronous messages. +Once written to the queue, a packet must be immutable (except for deletion when popped from the queue). That is, if a value `v` is written to a queue, then every valid proof `M_kvh` must refer to the same `v`. In practice, this means that an IBC implementation must ensure that only the IBC module can write to the IBC subspace of the blockchain's Merkle store. Each incoming & outgoing queue for each connection must be provably associated with another uniquely identified chain, connection, and channel so that an observer can prove that a message was intended for that chain and only that chain. This can easily be done by prefixing the queue keys in the Merkle store with strings unique to the chain (such as chain identifier), connection, and channel. ### 3.4 Sending a packet -{ todo: unify terms, clarify } - To send an IBC packet, an application module on the source chain must call the send method of the IBC module, providing a packet as defined above. The IBC module must ensure that the destination chain was already properly registered and that the calling module has permission to write this packet. If all is in order, the IBC module simply pushes the packet to the tail of `outgoing_a`, which enables all the proofs described above. -The packet must provide routing information in the `type` field, so that different modules can write different kinds of packets and maintain any application-level invariants related to this area. For example, a "coin" module can ensure a fixed supply, or a "NFT" module can ensure token uniqueness. The IBC module on the destination chain must associate every supported packet type with a particular handler (`f_type`) and return an error for unsupported types. +The packet must provide routing information in the `type` field, so that different modules can write different kinds of packets and maintain any application-level invariants related to this area. For example, a "coin" module can ensure a fixed supply, or a "NFT" module can ensure token uniqueness. The IBC module on the destination chain must associate every supported packet type with a particular handler (`f_type`). -`send(P{type, sequence, source, destination, data})` +To send an IBC packet from blockchain `A` to blockchain `B`: -``` -match source == (A, connection, channel) and sequence == tail(outgoing_A) with - true => push(outgoing_A, P); success - false => fail with "wrong sender" -``` - -Note that the `sequence`, `source`, and `destination` can all be encoded in the Merkle tree key for the channel and do not need to be stored for each packet. - -### 3.5 Receiving a packet - -Upon packet receipt, chain `B` must check that the packet is valid, that it was intended for the destination, and that all previous packets have been processed. `receive` must write the receipt queue upon accepting a valid packet, even if the handler execution returned an error, so that future packets can be processed. - -To receive an IBC packet on blockchain `B` from a source chain `A`, with a Merkle proof `M_kvh` and the current set of trusted headers for that chain `T_A`: - -`receive(P{type, sequence, source, destination, data}, M_kvh)` +`send(P{type, sequence, source, destination, data}) ⇒ success | failure` ``` case - incoming_B == nil => fail with "unregistered sender" - destination /= (B, connection, channel) => fail with "wrong destination" - sequence /= head(Incoming_B) => fail with "out of order" - H_h not in T_A => fail with "must submit header for height h" - valid(H_h, M_kvh) == false => fail with "invalid Merkle proof" - otherwise => - set (result, error) = f_type(data) - push(incoming_B, R{}) + source /= (A, connection, channel) ⇒ fail with "wrong sender" + sequence /= tail(outgoing_A) ⇒ fail with "wrong sequence" + otherwise ⇒ + push(outgoing_A, P) + success ``` -{ todo: check that v + k == packet, clearly define connection / channel } +Note that the `sequence`, `source`, and `destination` can all be encoded in the Merkle tree key for the channel and do not need to be stored individually in each packet. + +### 3.5 Receiving a packet + +Upon packet receipt, chain `B` must check that the packet is valid, that it was intended for the destination, and that all previous packets have been processed. `receive` must write the receipt queue upon accepting a valid packet regardless of the result of handler execution so that future packets can be processed. + +To receive an IBC packet on blockchain `B` from a source chain `A`, with a Merkle proof `M_kvh` and the current set of trusted headers for that chain `T_A`: + +`receive(P{type, sequence, source, destination, data}, M_kvh) ⇒ success | failure` + +``` +case + incoming_B == nil ⇒ fail with "unregistered sender" + destination /= (B, connection, channel) ⇒ fail with "wrong destination" + sequence /= head(Incoming_B) ⇒ fail with "out of order" + H_h not in T_A ⇒ fail with "must submit header for height h" + valid(H_h, M_kvh) == false ⇒ fail with "invalid Merkle proof" + otherwise ⇒ + set result = f_type(data) + push(incoming_B, R{tail(incoming_B), (B, connection, channel), (A, connection, channel), result}) + success +``` ### 3.6 Handling a receipt { todo: cleanup logic } -When we wish to create a transaction that atomically commits or rolls back across two chains, we must look at the receipts from sending the original message. For example, if I want to send tokens from Alice on chain `A` to Bob on chain `B`, chain `A` must decrement Alice's account *if and only if* Bob's account was incremented on chain `B`. We can achieve that by storing a protected intermediate state on chain `A` (escrowing the assets in question), which is then committed or rolled back based on the result of executing the transaction on chain `B`. +When we wish to create a transaction that atomically commits or rolls back across two chains, we must look at the execution result returned in the IBC receipt. For example, if I want to send tokens from Alice on chain `A` to Bob on chain `B`, chain `A` must decrement Alice's account *if and only if* Bob's account was incremented on chain `B`. We can achieve that by storing a protected intermediate state on chain `A` (escrowing the assets in question), which is then committed or rolled back based on the result of executing the transaction on chain `B`. -To do this requires that we not only provably send a message from chain `A` to chain `B`, but provably return the result of that message (the receipt) from chain `B` to chain `A`. As one noticed above in the implementation of `receive`, if the valid IBC message was sent from `A` to `B`, then the result of executing it, even if it was an error, is stored in _B:qA.receipt_. Since the receipts are stored in a queue with the same key construction as the sending queue, we can generate the same set of proofs for them, and perform a similar sequence of steps to handle a receipt coming back to _S_ for a message previously sent to _A_: +To do this requires that we not only provably send a packet from chain `A` to chain `B`, but provably return the result of executing that packet (the receipt `data`) from chain `B` to chain `A`. If a valid IBC packet was sent from `A` to `B`, then the result of executing it is stored in `incoming_B`. Since the receipts are stored in a queue with the same key construction as the sending queue, we can generate the same set of proofs for them, and perform a similar sequence of steps to handle a receipt coming back to `A` for a message previously sent to `B`. Receipts, like packets, are processed in order. -`handle_receipt(A, M_kvh)` +To handle an IBC receipt on blockchain `A` received from blockchain `B`, with a Merkle proof `M_kvh` and the current set of trusted headers for that chain `T_B`: + +`handle_receipt(R{sequence, source, destination, data}, M_kvh)` ``` case - outgoing_A == nil => fail with "unregistered sender" - destination /= (A, connection, channel) => fail with "wrong destination" - sequence /= head(incoming_A) => fail with "out of order" - H_h not in T_B => fail with "must submit header for height h" - valid(H_h, M_kvh) == false => fail with "invalid Merkle proof" - * _v = (\_, error)_ ⇒ _(type, data) := pop(qS.send ); rollbacktype(data); Success_ - * _v = (res, success)_ ⇒ _(type, data) := pop(qS.send ); committype(data, res); Success_ + outgoing_A == nil ⇒ fail with "unregistered sender" + destination /= (A, connection, channel) ⇒ fail with "wrong destination" + sequence /= head(incoming_A) ⇒ fail with "out of order" + H_h not in T_B ⇒ fail with "must submit header for height h" + valid(H_h, M_kvh) == false ⇒ fail with "invalid Merkle proof" + otherwise ⇒ + set P{type, _, _, _, _} = outgoing_A[sequence] + f_type(result) + success ``` -This enforces that the receipts are processed in order, to allow applications to make use of some basic assumptions about ordering. It also removes the message from the send queue, as there is now proof it was processed on the receiving chain and no need to store it. +This allows applications to reason about ordering and enforce application-level guarantees by committing or reverting state changes on chain `A` based on the result of packet execution on chain `B`: ![Successful Transaction](images/Receipts.png) @@ -225,28 +231,24 @@ This enforces that the receipts are processed in order, to allow applications to { todo: one relay process can relay all the things } -The blockchain itself only records the *intention* to send the given message to the recipient chain, it doesn't make any network connections as that would add unbounded delays and non-determinism into the state machine. We define the concept of a *relay* process that connects two chain by querying one for all proofs needed to prove outgoing messages and submit these proofs to the recipient chain. +The blockchain itself only records the *intention* to send the given message to the recipient chain - it does not open any actual network connections. We define the concept of a *relay* process that connects two chains by querying one for all outgoing packets & proofs, then committing those packets & proofs to the recipient chain. -The relay process must have access to accounts on both chains with sufficient balance to pay for transaction fees but needs no other permissions. Many *relay* processes may run in parallel without violating any safety consideration. However, they will consume unnecessary fees if they submit the same proof multiple times, so some minimal coordination is ideal. +The relay process must have access to accounts on both chains with sufficient balance to pay for transaction fees but needs no other permissions. Relayers may employ application-level methods to recoup these fees. Any number of *relay* processes may be safely run in parallel. However, they will consume unnecessary fees if they submit the same proof multiple times, so some minimal coordination is ideal. -As an example, here is a naive algorithm for relaying send messages from `A` to `B`, without error handling. We must also concurrently run the relay of receipts from `B` back to `A`, in order to complete the cycle. Note that all reads of variables belonging to a chain imply queries and all function calls imply submitting a transaction to the blockchain. +As an example, here is a naive algorithm for relaying outgoing packets from `A` to `B` and incoming receipts from `B` back to `A`. All reads of variables belonging to a chain imply queries and all function calls imply submitting a transaction to the blockchain. ``` while true - pending := tail(A:qB.send) - received := tail(B:qA.receive) + set pending = tail(outgoing_A) + set received = tail(incoming_B) if pending > received - Uh := A:latestHeader - B:updateHeader(Uh) - for i :=received...pending - k := (B, send, i) - packet := A:Mk,v,h - B:IBCreceive(A, packet) - sleep(desiredLatency) + set U_h = A.latestHeader + if U_h /= B.knownHeaderA + B.updateHeader(U_h) + for i from received to pending + set P = outgoing_A[i] + set M_kvh = A.prove(U_h, P) + B.receive(P, M_kvh) ``` -Note that updating a header is a costly transaction compared to posting a merkle proof for a known header. Thus, a process could wait until many messages are pending, then submit one header along with multiple merkle proofs, rather than a separate header for each message. This decreases total computation cost (and fees) at the price of additional latency and is a trade-off each relay can dynamically adjust. - -In the presence of multiple concurrent relays, any given relay can perform local optimizations to minimize the number of headers it submits, but remember the frequency of header submissions defines the latency of the packet transfer. - -Indeed, it is ideal if each user that initiates the creation of an IBC packet also relays it to the recipient chain. The only constraint is that the relay must be able to pay the appropriate fees on the destination chain. However, in order to avoid bottlenecks, a group may sponsor an account to pay fees for a public relayer that moves all unrelayed packets (perhaps with a high latency). +Note that updating a header is a costly transaction compared to posting a Merkle proof for a known header. Thus, a process could wait until many messages are pending, then submit one header along with multiple Merkle proofs, rather than a separate header for each message. This decreases total computation cost (and fees) at the price of additional latency and is a trade-off each relay can dynamically adjust. diff --git a/docs/spec/ibc/connections.md b/docs/spec/ibc/connections.md index c8bf728d2..0e5c17cfe 100644 --- a/docs/spec/ibc/connections.md +++ b/docs/spec/ibc/connections.md @@ -28,17 +28,19 @@ To facilitate an IBC connection, the two blockchains must provide the following it is possible to prove `H_h'` where `C_h' /= C_h` and `dt(now, H_h) < P` 3. Given a trusted `H_h` and a Merkle proof `M_kvh` it is possible to prove `V_kh` -It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages `U_h'` and `X_h'`. The implementation of these requirements with Tendermint consensus is defined in [Appendix E](). Another algorithm able to provide equally strong guarantees (such as Casper) is also compatible with IBC but must define its own set of update and change messages. +It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages `U_h'` and `X_h'`. The implementation of these requirements with Tendermint consensus is defined in [Appendix F](appendices.md#appendix-f-tendermint-header-proofs). Another algorithm able to provide equally strong guarantees (such as Casper) is also compatible with IBC but must define its own set of update and change messages. The Merkle proof `M_kvh` is a well-defined concept in the blockchain space, and provides a compact proof that the key value pair `(k, v)` is consistent with a Merkle root stored in `H_h`. Handling the case where `k` is not in the store requires a separate proof of non-existence, which is not supported by all Merkle stores. Thus, we define the proof only as a proof of existence. There is no valid proof for missing keys, and we design the algorithm to work without it. -`valid(H_h, M_kvh) => true | false` +Blockchains supporting IBC must implement Merkle proof verification: + +`valid(H_h, M_kvh) ⇒ true | false` ### 2.3 Connection Lifecycle #### 2.3.1 Opening a connection -All proofs require an initial `H_h` and `C_h` for some `h`, where Δ_(now, Hh) < P_. +All proofs require an initial `H_h` and `C_h` for some `h`, where `dt(now, H_h) < P`. Establishing a bidirectional initial root-of-trust between the two blockchains (`A` to `B` and `B` to `A`) — `H_ah` and `C_ah` stored on chain `B`, and `H_bh` and `C_bh` stored on chain `A` — is necessary before any IBC packets can be sent. @@ -46,38 +48,38 @@ Any header may be from a malicious chain (e.g. shadowing a real chain state with #### 2.3.2 Following block headers -We define two messages `U_h` and `X_h`, which together allow us to securely advance our trust from some known `H_n` to some future `H_h` where `h > n`. Some implementations may require that `h == n + 1` (all headers must be processed in order). IBC implemented on top of Tendermint or similar BFT algorithms requires only that `delta vals(C_n, C_h) < ⅓` (each step must have a change of less than one-third of the validator set)[[4](./references.md#4)]. +We define two messages `U_h` and `X_h`, which together allow us to securely advance our trust from some known `H_n` to some future `H_h` where `h > n`. Some implementations may require that `h == n + 1` (all headers must be processed in order). IBC implemented on top of Tendermint or similar BFT algorithms requires only that `delta-vals(C_n, C_h) < ⅓` (each step must have a change of less than one-third of the validator set)[[4](./references.md#4)]. -Either requirement is compatible with IBC. However, by supporting proofs where `h_-_n > 1`, we can follow the block headers much more efficiently in situations where the majority of blocks do not include an IBC packet between chains `A` and `B`, and enable low-bandwidth connections to be implemented at very low cost. If there are packets to relay every block, these two requirements collapse to the same case (every header must be relayed). +Either requirement is compatible with IBC. However, by supporting proofs where `h - n > 1`, we can follow the block headers much more efficiently in situations where the majority of blocks do not include an IBC packet between chains `A` and `B`, and enable low-bandwidth connections to be implemented at very low cost. If there are packets to relay every block, these two requirements collapse to the same case (every header must be relayed). Since these messages `U_h` and `X_h` provide all knowledge of the remote blockchain, we require that they not just be provable, but also attributable. As such, any attempt to violate the finality guarantees in headers posted to chain `B` can be submitted back to chain `A` for punishment, in the same manner that chain `A` would independently punish (slash) identified Byzantine actors. More formally, given existing set of trust `T` = `{(H_i, C_i), (H_j, C_j), …}`, we must provide: -`valid(T, X_h | U_h) => true | false | unknown` +`valid(T, X_h | U_h) ⇒ true | false | unknown` `valid` must fulfill the following properties: ``` if H_h-1 ∈ T then - valid(T, X_h | U_h) => true | false - ∃ (U_h | X_h) => valid(T, X_h | U_h) + valid(T, X_h | U_h) ⇒ true | false + ∃ (U_h | X_h) ⇒ valid(T, X_h | U_h) ``` ``` if C_h ∉ T then - valid(T, U_h) => false + valid(T, U_h) ⇒ false ``` We can then process update transactions as follows: -`update(T, X_h | U_h) => success | failure` +`update(T, X_h | U_h) ⇒ success | failure` ``` update(T, X_h | U_h) = match valid(T, X_h | U_h) with - false => fail with "invalid proof" - unknown => fail with "need a proof between current and h" - true => + false ⇒ fail with "invalid proof" + unknown ⇒ fail with "need a proof between current and h" + true ⇒ set T = T ∪ (H_h, C_h) ```