Cleanup & clarification in progress
This commit is contained in:
Christopher Goes
parent
dc2c638f7f
commit
f1c7d1ccea
|
|
@ -4,13 +4,11 @@
|
|||
|
||||
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 protocol requires two blockchains with cheaply verifiable instant finality. 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 provable packets can be sent between the chains.
|
||||
IBC requires two blockchains with cheaply verifiable rapid finality. 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 provable packets can be sent between the chains.
|
||||
|
||||
Each chain maintains a local partial order and inter-chain message sequencing ensures cross-chain linearity. 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, 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.
|
||||
|
||||
IBC was first outlined in the [Cosmos Whitepaper](https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc),
|
||||
and then later described in more detail by the [IBC specification paper](https://github.com/cosmos/ibc/raw/master/CosmosIBCSpecification.pdf).
|
||||
This documentation replaces and supersedes both. It explains the requirements and structure of the protocol and provides sufficient detail for both analysis and implementation, including example pseudocode.
|
||||
IBC was first outlined in the [Cosmos Whitepaper](https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc), and later described in more detail by the [IBC specification paper](https://github.com/cosmos/ibc/raw/master/CosmosIBCSpecification.pdf). This documentation replaces and supersedes both. It explains the requirements and structure of the protocol and provides sufficient detail for both analysis and implementation, including example pseudocode.
|
||||
|
||||
## Contents
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
## 5 Conclusion
|
||||
|
||||
We have demonstrated a secure, performant, and flexible protocol for connecting two blockchains with complete finality using a secure, reliable messaging queue. The algorithm and semantics of all data types have been defined above, which provides a solid basis for reasoning about correctness and efficiency of the algorithm.
|
||||
We have demonstrated a secure, performant, and flexible protocol for cross-blockchain messaging, and provided sufficient detail to reason about the correctness and efficiency of the protocol.
|
||||
|
||||
The observant reader may note that while we have defined a message queue protocol, we have not yet defined how to use that to transfer value within the Cosmos ecosystem. We will shortly release a separate paper on Cosmos IBC that defines the application logic used for direct value transfer as well as routing over the Cosmos hub. That paper builds upon the IBC protocol defined here and provides a first example of how to reason about application logic and global invariants in the context of IBC.
|
||||
This document defines solely a message queue protocol - not the application-level semantics which must sit on top of it to enable asset transfer between two chains. We will shortly release a separate paper on Cosmos IBC that defines the application logic used for direct value transfer as well as routing over the Cosmos hub. That paper builds upon the IBC protocol defined here and provides a first example of how to reason about application logic and global invariants in the context of IBC.
|
||||
|
||||
There is a reference implementation of the Cosmos IBC protocol as part of the Cosmos SDK, written in go and freely usable under the Apache license. For those wish to write an implementation of IBC in another language, or who want to analyze the specification further, the following appendixes define the exact message formats and binary encoding.
|
||||
There is a reference implementation of the Cosmos IBC protocol as part of the Cosmos SDK, written in Golang and released under the Apache license. To facilitate implementations in other langauages which are wire-compatible with the Cosmos implementation, the following appendices define exact message and binary encoding formats.
|
||||
|
|
|
|||
|
|
@ -3,9 +3,6 @@
|
|||
##### 1:
|
||||
[https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc](https://github.com/cosmos/cosmos/blob/master/WHITEPAPER.md#inter-blockchain-communication-ibc)
|
||||
|
||||
##### 2:
|
||||
[http://www.amqp.org/sites/amqp.org/files/amqp.pdf](http://www.amqp.org/sites/amqp.org/files/amqp.pdf)
|
||||
|
||||
##### 3:
|
||||
[https://blog.cosmos.network/consensus-compare-casper-vs-tendermint-6df154ad56ae#215d](https://blog.cosmos.network/consensus-compare-casper-vs-tendermint-6df154ad56ae#215d)
|
||||
|
||||
|
|
|
|||
|
|
@ -2,38 +2,30 @@
|
|||
|
||||
([Back to table of contents](README.md#contents))
|
||||
|
||||
The IBC protocol creates a mechanism by which multiple sovereign replicated fault tolerant state machines my pass messages to each other. These messages provide a base layer for the creation of communicating blockchain architecture that overcomes challenges in the scalability and extensibility of computing blockchain environments.
|
||||
The IBC protocol creates a mechanism by which two replicated fault-tolerant state machines may pass messages to each other. These messages provide a base layer for the creation of communicating blockchain architecture that overcomes challenges in the scalability and extensibility of computing blockchain environments.
|
||||
|
||||
The IBC protocol assumes that multiple applications are running on their own blockchain with their own state and own logic. Communication is achieved over an extremely secure message queue protocol, allowing the creation of complex inter-chain processes without trusted parties. This architecture can be seen as a parallel to microservices in the blockchain space, and the IBC protocol can be seen as an analog to the AMQP messaging protocol[[2](./footnotes.md#2)], used by StormMQ, RabbitMQ, etc.
|
||||
The IBC protocol assumes that multiple applications are running on their own blockchain with their own state and own logic. Communication is achieved over an ordered message queue primitive, allowing the creation of complex inter-chain processes without trusted third parties.
|
||||
|
||||
The message packets are not signed by one psuedonymous account, or even multiple. Rather, IBC effectively assigns authorization of the packets to the blockchain's consensus algorithm itself. Not only are blockchains highly secure, they are auditable and have an extremely high creation cost in comparison to cryptographic key pairs. This prevents Sybil attacks and allows out-of-protocol accountability, since any byzantine behavior is provable and can be published to damage the reputation/value of the other blockchain. By using registered blockchains as "actors" in the system, we can achieve extremely high security through a combination of cryptography and incentives.
|
||||
The message packets are not signed by one psuedonymous account, or even multiple, as in multi-signature sidechain implementations. Rather, IBC assigns authorization of the packets to the source blockchain's consensus algorithm, performing light-client style verification on the destination chain. The Byzantine-fault-tolerant properties of the underlying blockchains are preserved: a user transferring assets between two chains using IBC must trust only the consensus algorithms of both chains.
|
||||
|
||||
In this paper, we define a process of posting block headers and merkle proofs to enable secure verification of individual packets. We then describe how to combine these packets into a messaging queue to guarantee reliable, in-order delivery of message. We then explain how to securely handle receipts (response/error), which enables the creation of asynchronous RPC-like protocols. Finally, we detail some optimizations and how to handle byzantine blockchains.
|
||||
In this paper, we define a process of posting block headers and Merkle tree proofs to enable secure verification of individual packets. We then describe how to combine these packets into a messaging queue to guarantee ordered delivery. We then explain how to handle packet receipts (response/error) on the source chain, which enables the creation of asynchronous RPC-like protocols on top of IBC. Finally, we detail some optimizations and how to handle Byzantine blockchains.
|
||||
|
||||
### 1.1 Definitions
|
||||
### 1.1 Definitions
|
||||
|
||||
_Blockchain_ - an immutable ledger created through distributed consensus, coupled with a deterministic state machine to process the transactions on the ledger. The smallest unit produced through consensus is a block, which may contain many transactions.
|
||||
_Blockchain_ - A replicated fault-tolerant state machine with a distributed consensus algorithm. The smallest unit produced through consensus is a block, which may contain many transactions, each applying some arbitrary mutation to the state.
|
||||
|
||||
_Module_ - we assume that the state machine of the blockchain is comprised of multiple components (modules or smart contracts) that have limited rights, and they can only interact over pre-defined interfaces rather than directly mutating internal state.
|
||||
_Module_ - We assume that the state machine of each blockchain is comprised of multiple components that have limited rights to execute some particular set of state transfers (these are modules in the Cosmos SDK or smart contracts in Ethereum).
|
||||
|
||||
_Finality_ - a guarantee that a given block will not be reverted within some predefined conditions. All proof of work systems offer probabilistic finality, which means the probability of that a block will be reverted approaches 0. A "better", alternative chain could exist, but the cost of creation increases rapidly over time. Many "proof of stake" systems offer much weaker guarantees, based only on the honesty of the miners. However, BFT algorithms such as Tendermint guarantee complete finality upon production of a block, unless over two thirds of the validators collude to break consensus. This collusion is provable and can be punished.
|
||||
_Finality_ - The guarantee that a given block will not be reverted within some predefined conditions of a consensus algorithm. All proof-of-work systems offer probabilistic finality, which means that the difficulty of reverting a block increases as the block is embedded more deeply in the chain. Many proof-of-stake systems offer much weaker guarantees, based only on the honesty of the block producers. BFT algorithms such as Tendermint guarantee complete finality upon production of a block (unless over two thirds of the validators collude to break consensus, in which case the offenders can be identified and punished - further discussion of that scenario is outside the scope of this document).
|
||||
|
||||
_Knowledge_ - what is certain to be true.
|
||||
_Attributable_ - Knowledge of the pseudonymous identity which made a statement, whom we can punish with some deduction of value (slashing) if the statement is false. Synonymous with accountability.
|
||||
|
||||
_Provable_ - the existence of irrefutable mathematical (often cryptographic) proof of the truth of a given statement. These can be expressed as: given knowledge **A** and a statement **s**, then **B** must be true. This is a form of deductive proof and they can be chained together without losing validity.
|
||||
_Unbonding Period_ - Proof-of-stake algorithms need to lock the stake (prevent transfers) for some time to provide a lower bound for the length of a long-range attack [[3](./footnotes.md#3)]. Complete finality is associated with a subset of the proof-of-stake class of consensus algorithms. We assume the proof-of-stake algorithms utilized by the two blockchains have some unbonding period P.
|
||||
|
||||
_Attributable_ - provable knowledge of who made a statement. If a statement is provably false, then it is known which actor lied. Attributable statements allow us to build incentives against lying, which help enforce finality. This is also referred to as accountability.
|
||||
### 1.2 Threat Models
|
||||
|
||||
_Root of Trust_ - any proof depends on some prior assumptions, however simple they are. We refer to the first assumption we make as the root of trust, and all our knowledge of the system is derived from this root through a provable chain of information. We seek to make this root of trust as simple and a verifiable as possible, since if the original assignment of trust is false, all conclusions drawn will also be false.
|
||||
_False statements_ - Any information we receive may be false.
|
||||
|
||||
_Unbonding Period_ - Proof of Stake algorithms need to freeze the stake for some time to provide a lower bound for the length of a long-range attack [[3](./footnotes.md#3)]. Since complete finality is associated with a subset of the Proof of Stake class of consensus algorithms, I will assume all implementations that support IBC have some unbonding period P, such that if my last knowledge of the blockchain is older than P, I can no longer trust any message without a new root of trust.
|
||||
_Network partitions and delays_ - We assume an asynchronous, adversarial network with unbounded latency. Network messages may be modified, reordered, duplicated, or selectively dropped. Actors may be arbitrarily partitioned by a powerful adversary. The IBC protocol favors correctness over liveness (and provides no particular guarantees of the latter).
|
||||
|
||||
The IBC protocol requires each actor to be a blockchain with complete finality. All transitions must be provable and attributable to (at least) one actor. That implies the smallest unit of trust is the consensus algorithm of a blockchain.
|
||||
|
||||
### 1.2 Threat Models
|
||||
|
||||
_False statements_ - any information we receive may be false, all actors must have enough knowledge be able to prove its correctness without external dependencies. All statements should be attributable.
|
||||
|
||||
_Network partitions and delays_ - we assume an asynchronous, adversarial network. Any message may or may not reach the destination. They may be modified or selectively dropped. Messages may reach the destination out of order and may arrive multiple times. There is no upper limit to the time it takes for a message to be received. Actors may be arbitrarily partitioned by a powerful adversary. The protocol favors correctness over liveness. That is, it only acts upon information that is provably correct.
|
||||
|
||||
_Byzantine actors_ - it is possible that an entire blockchain is not acting according to protocol. This must be detectable and provable, allowing the communicating blockchain to revoke trust and take necessary action. Furthermore, we should design application-level protocols on top of IBC to minimize risk exposure in the face of Byzantine actors.
|
||||
_Byzantine actors_ - An entire blockchain may not act according to protocol. This must be detectable and provable, allowing the communicating blockchain to revoke trust and take necessary action. Application-level protocols designed on top of IBC should consider this risk and mitigate it as possible in a manner suitable to their application.
|
||||
|
|
|
|||
|
|
@ -2,37 +2,49 @@
|
|||
|
||||
([Back to table of contents](README.md#contents))
|
||||
|
||||
The basis of IBC is the ability to perform efficient proofs of a message packet on-chain and deterministically. All transactions must be attributable and provable without depending on any information outside of the blockchain. We define the following variables: _H<sub>h</sub>_ is the signed header at height _h_, _C<sub>h</sub>_ are the consensus rules at height _h_, and _P_ is the unbonding period of this blockchain. _V<sub>k,h</sub>_ is the value stored under key _k_ at height _h_. Note that of all these, only _H<sub>h</sub>_ defines a signature and is thus attributable.
|
||||
The basis of IBC is the ability to verify in the on-chain consensus ruleset of chain _B_ that a message packet received on chain _B_ was correctly generated on chain _A_. This establishes a cross-chain linearity guarantee: upon validation of that packet on chain _B_ we know that the packet has been executed on chain _A_ and any associated logic resolved (such as assets being escrowed), and we can safely perform application logic on chain _B_ (such as generating vouchers on chain _B_ for the chain _A_ assets which can later be redeemed with a packet in the opposite direction).
|
||||
|
||||
To support an IBC connection, two actors must be able to make the following proofs to each other:
|
||||
### 2.1 Definitions
|
||||
|
||||
* given a trusted _H<sub>h</sub>_ and _C<sub>h</sub>_ and an attributable update message _U<sub>h'</sub>_ it is possible to prove _H<sub>h'</sub>_ where _C<sub>h'</sub> = C<sub>h</sub>_ and Δ_(now, H<sub>h</sub>) < P_
|
||||
* given a trusted _H<sub>h</sub>_ and _C<sub>h</sub>_ and an attributable change message _X<sub>h'</sub>_ it is possible to prove _H<sub>h'</sub>_ where _C<sub>h'</sub>_ ≠ _C<sub>h</sub>_ and Δ _(now, H<sub>h</sub>) < P_
|
||||
* given a trusted _H<sub>h</sub>_ and a merkle proof _M<sub>k,v,h</sub>_ it is possible to prove _V<sub>k,h</sub>_
|
||||
- Chain _A_ is the source blockchain from which the IBC packet is sent
|
||||
- Chain _B_ is the destination blockchain on which the IBC packet is received
|
||||
- _H<sub>h</sub>_ is the signed header of chain _A_ at height _h_
|
||||
- _C<sub>h</sub>_ is the consensus ruleset of chain _A_ at height _h_
|
||||
- _V<sub>k,h</sub>_ is the value stored on chain _A_ under key _k_ at height _h_
|
||||
- _P_ is the unbonding period of chain _A_, in units of time
|
||||
- Δ_(a, b)_ is the time difference between events _a_ and _b_
|
||||
|
||||
It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages _U<sub>h'</sub>_ and _X<sub>h'</sub>_. The implementation of these requirements with Tendermint is defined in Appendix E. Another engine able to provide equally strong guarantees (such as Casper) should be theoretically compatible with IBC, and must define its own set of update/change messages.
|
||||
Note that of all these, only _H<sub>h</sub>_ defines a signature and is thus attributable.
|
||||
|
||||
### 2.2 Basics
|
||||
|
||||
To facilitate an IBC connection, the two blockchains must provide the following proofs:
|
||||
|
||||
1. Given a trusted _H<sub>h</sub>_ and _C<sub>h</sub>_ and an attributable update message _U<sub>h'</sub>_,
|
||||
it is possible to prove _H<sub>h'</sub>_ where _C<sub>h'</sub> = C<sub>h</sub>_ and Δ_(now, H<sub>h</sub>) < P_
|
||||
2. Given a trusted _H<sub>h</sub>_ and _C<sub>h</sub>_ and an attributable change message _X<sub>h'</sub>_,
|
||||
it is possible to prove _H<sub>h'</sub>_ where _C<sub>h'</sub>_ ≠ _C<sub>h</sub>_ and Δ _(now, H<sub>h</sub>) < P_
|
||||
3. Given a trusted _H<sub>h</sub>_ and a merkle proof _M<sub>k,v,h</sub>_ it is possible to prove _V<sub>k,h</sub>_
|
||||
|
||||
It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages _U<sub>h'</sub>_ and _X<sub>h'</sub>_. 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.
|
||||
|
||||
The merkle proof _M<sub>k,v,h</sub>_ 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<sub>h</sub>_. 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<sub>h </sub>,M<sub>k,v,h </sub>)_ ⇒ _[true | false]_
|
||||
|
||||
### 2.1 Establishing a Root of Trust
|
||||
### 2.3 Establishing a Root of Trust
|
||||
|
||||
As mentioned in the definitions, all proofs are based on an original assumption. In this case it is _H<sub>h</sub>_ and _C<sub>h</sub>_ for some _h_, where Δ_(now, H<sub>h</sub>) < P_.
|
||||
All proofs require an initial _H<sub>h</sub>_ and _C<sub>h</sub>_ for some _h_, where Δ_(now, H<sub>h</sub>) < P_.
|
||||
|
||||
Any header may be from a malicious chain (eg. shadowing a real chain id with a fake validator set), so a subjective decision is required before establishing a connection. This should be performed by on-chain governance to avoid an exploitable position of trust. Establishing a bidirectional root of trust between two blockchains (A trusts B and B trusts A) is a necessary and sufficient prerequisite for all other IBC activity.
|
||||
Any header may be from a malicious chain (e.g. shadowing a real chain state with a fake validator set), so a subjective decision is required before establishing a connection. This can be performed by on-chain governance or a similar decentralized mechanism if desired. Establishing a bidirectional initial root-of-trust between the two blockchains (_A_ to _B_ and _B_ to _A_) is necessary before any IBC packets can be sent.
|
||||
|
||||
Development of a fully open and decentralized PKI for tracking blockchains is an open research question for future iterations of the IBC protocol.
|
||||
### 2.4 Following Block Headers
|
||||
|
||||
### 2.2 Following Block Headers
|
||||
We define two messages _U<sub>h</sub>_ and _X<sub>h</sub>_, which together allow us to securely advance our trust from some known _H<sub>n</sub>_ to some future _H<sub>h</sub>_ 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 Δ_<sub>vals</sub>(C<sub>n</sub>, C<sub>h</sub> ) < ⅓_ (each step must have a change of less than one-third of the validator set)[[4](./footnotes.md#4)].
|
||||
|
||||
We define two messages _U<sub>h</sub>_ and _X<sub>h</sub>_, which together allow us to securely advance our trust from some known _H<sub>n</sub>_ to a future _H<sub>h</sub>_ where _h > n_. Some implementations may provide the additional limitation that _h = n + 1_, which requires us to process every header. Tendermint allows us to exploit knowledge of the BFT algorithm to only require the additional limitation
|
||||
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).
|
||||
|
||||
Δ_<sub>vals</sub>(C<sub>n</sub>, C<sub>h</sub> ) < ⅓_, that each step must have a change of less than one-third of the validator set[[4](./footnotes.md#4)].
|
||||
|
||||
Any of these requirements allows us to support IBC for the given block chain. 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 message between chains A and B, and enable low-bandwidth connections to be implemented at very low cost. If there are messages to relay every block, then these collapse to the same case, relaying every header.
|
||||
|
||||
Since these messages _U<sub>h</sub>_ and _X<sub>h</sub>_ 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 or provide fake proof can be submitted to the remote blockchain for punishment, in the same manner that any violation of the internal consensus algorithm is punished. This incentive enhances the security guarantees and avoids the nothing-at-stake issue in IBC as well.
|
||||
Since these messages _U<sub>h</sub>_ and _X<sub>h</sub>_ 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<sub>i </sub>, C<sub>i </sub>), (H<sub>j </sub>, C<sub>j </sub>), …}_, we must provide:
|
||||
|
||||
|
|
@ -40,19 +52,19 @@ _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ ⇒ _[true | false | u
|
|||
|
||||
_if H<sub>h-1</sub>_ ∈ _T then_:
|
||||
* _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ ⇒ _[true | false]_
|
||||
* _there must exist some U<sub>h</sub> or X<sub>h</sub> that evaluates to true_
|
||||
* ∃ (U<sub>h</sub> | X<sub>h</sub>) ⇒ valid(T, X<sub>h</sub> | U<sub>h</sub>) {aren't there infinite? why is this necessary}
|
||||
|
||||
_if C<sub>h</sub>_ ∉ _T then_
|
||||
* _valid(T, U<sub>h </sub>)_ ⇒ _false_
|
||||
|
||||
and can process update transactions as follows:
|
||||
We can then process update transactions as follows:
|
||||
|
||||
_update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ ⇒
|
||||
_ match valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_
|
||||
* _false_ ⇒ _return Error("invalid proof")_
|
||||
* _unknown_ ⇒ _return Error("need a proof between current and h")_
|
||||
* _true_ ⇒ _T_ ∪ _(H<sub>h </sub>,C<sub>h </sub>)_
|
||||
_update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ ⇒ match _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)_ with
|
||||
* _false_ ⇒ fail with `invalid proof`
|
||||
* _unknown_ ⇒ fail with `need a proof between current and h`
|
||||
* _true_ ⇒ set _T_ = _T_ ∪ _(H<sub>h </sub>,C<sub>h </sub>)_
|
||||
|
||||
We define _max(T)_ as _max(h, where H<sub>h</sub>_ ∈ _T)_ for any _T_ with _max(T) = h-1_. And from above, there must exist some _X<sub>h </sub>|<sub> </sub>U<sub>h</sub>_ so that _max(update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)) = h_. By induction, we can see there must exist a set of proofs, such that _max(update…(T,...)) = h+n_ for any n.
|
||||
Define _max(T)_ as _max(h, where H<sub>h</sub>_ ∈ _T)_. For any _T_ with _max(T) = h-1_, there must exist some _X<sub>h </sub>|<sub> </sub>U<sub>h</sub>_ so that _max(update(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>)) = h_.
|
||||
By induction, there must exist a set of proofs, such that _max(update…(T,...)) = h+n_ for any n.
|
||||
|
||||
We also can see the validity of using bisection as an optimization to discover this set of proofs. That is, given _max(T) = n_ and _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = unknown_, we then try _update(T, X<sub>b </sub>|<sub> </sub>U<sub>b </sub>)_, where _b = (h+n)/2_. The base case is where _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = true_ and is guaranteed to exist if _h=max(T)+1_.
|
||||
Bisection can be used to discover this set of proofs. That is, given _max(T) = n_ and _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = unknown_, we then try _update(T, X<sub>b </sub>|<sub> </sub>U<sub>b </sub>)_, where _b = (h+n)/2_. The base case is where _valid(T, X<sub>h </sub>|<sub> </sub>U<sub>h </sub>) = true_ and is guaranteed to exist if _h=max(T)+1_.
|
||||
|
|
|
|||
Loading…
Reference in New Issue