diff --git a/docs/spec/ibc/proofs.md b/docs/spec/ibc/proofs.md
index 59ab96142..c402eae39 100644
--- a/docs/spec/ibc/proofs.md
+++ b/docs/spec/ibc/proofs.md
@@ -2,43 +2,23 @@
([Back to table of contents](specification.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: _Hh _is the signed header at height _h_, _Ch_ are the consensus rules at height _h_, and _P_ is the unbonding period of this blockchain. _Vk,h_ is the value stored under key _k_ at height _h_. Note that of all these, only _Hh_ defines a signature and is thus attributable.
+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: _Hh_ is the signed header at height _h_, _Ch_ are the consensus rules at height _h_, and _P_ is the unbonding period of this blockchain. _Vk,h_ is the value stored under key _k_ at height _h_. Note that of all these, only _Hh_ defines a signature and is thus attributable.
To support an IBC connection, two actors must be able to make the following proofs to each other:
-* given a trusted _Hh_ and _Ch_ and an attributable update message _Uh'_ it is possible to prove _Hh'_ where _Ch' = Ch_ and
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_(now, Hh) < P_
-* given a trusted _Hh_ and _Ch_ and an attributable change message _Xh'_ it is possible to prove _Hh'_ where _Ch' _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_Ch_ and
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_(now, Hh) < P_
+* given a trusted _Hh_ and _Ch_ and an attributable update message _Uh'_ it is possible to prove _Hh'_ where _Ch' = Ch_ and Δ_(now, Hh) < P_
+* given a trusted _Hh_ and _Ch_ and an attributable change message _Xh'_ it is possible to prove _Hh'_ where _Ch'_ ≠ _Ch_ and Δ _(now, Hh) < P_
* given a trusted _Hh_ and a merkle proof _Mk,v,h_ it is possible to prove _Vk,h_
It is possible to make use of the structure of BFT consensus to construct extremely lightweight and provable messages _Uh'_ and _Xh'_. 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.
The merkle proof _Mk,v,h_ 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 _Hh_. 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(Hh ,Mk,v,h ) _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ [true | false]_
+_valid(Hh ,Mk,v,h )_ ⇒ _[true | false]_
### 2.1 Establishing a Root of Trust
-As mentioned in the definitions, all proofs are based on an original assumption. In this case it is _Hh_ and _Ch_ for some _h_, where
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_(now, Hh) < P_.
+As mentioned in the definitions, all proofs are based on an original assumption. In this case it is _Hh_ and _Ch_ for some _h_, where Δ_(now, Hh) < 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.
@@ -48,9 +28,7 @@ Development of a fully open and decentralized PKI for tracking blockchains is an
We define two messages _Uh_ and _Xh_, which together allow us to securely advance our trust from some known _Hn_ to a future _Hh_ 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
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-vals(Cn, Ch ) < ⅓, that each step must have a change of less than one-third of the validator set[[4](./footnotes.md#4)].
+Δ_vals(Cn, Ch ) < ⅓_, 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.
@@ -58,72 +36,23 @@ Since these messages _Uh_ and _Xh_ provide all knowledge o
More formally, given existing set of trust _T_ = _{(Hi , Ci ), (Hj , Cj ), …}_, we must provide:
-_valid(T, Xh | Uh ) _
+_valid(T, Xh | Uh )_ ⇒ _[true | false | unknown]_
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
+_if Hh-1_ ∈ _T then_:
+* _valid(T, Xh | Uh )_ ⇒ _[true | false]_
+* _there must exist some Uh or Xh that evaluates to true_
-_ [true | false | unknown]_
-
-_if Hh-1 _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_T then _
-
-_valid(T, Xh | Uh ) _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ [true | false]_
-
-_there must exist some Uh or Xh that evaluates to true_
-
-_if Ch _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_T then_
-
-_ valid(T, Uh ) _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ false_
+_if Ch_ ∉ _T then_
+* _valid(T, Uh )_ ⇒ _false_
and can process update transactions as follows:
-_update(T, Xh | Uh ) _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
+_update(T, Xh | Uh )_ ⇒
_ match valid(T, Xh | Uh )_
+* _false_ ⇒ _return Error("invalid proof")_
+* _unknown_ ⇒ _return Error("need a proof between current and h")_
+* _true_ ⇒ _T_ ∪ _(Hh ,Ch )_
-_ false _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ return Error("invalid proof")_
-
-_ unknown _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ return Error("need a proof between current and h")_
-
-_ true _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_ T _
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_(Hh ,Ch )_
-
-We define _max(T)_ as _max(h, where Hh_
-
->>>>> gd2md-html alert: equation: use MathJax/LaTeX if your publishing platform supports it.
(Back to top)(Next alert)
>>>>>
-
-_T) _for any _T_ with _max(T) = h-1_. And from above, there must exist some _Xh | Uh_ so that _max(update(T, Xh | Uh )) = h_. By induction, we can see there must exist a set of proofs, such that _max(update…(T,...)) = h+n_ for any n.
+We define _max(T)_ as _max(h, where Hh_ ∈ _T)_ for any _T_ with _max(T) = h-1_. And from above, there must exist some _Xh | Uh_ so that _max(update(T, Xh | Uh )) = h_. By induction, we can see 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, Xh | Uh ) = unknown_, we then try _update(T, Xb | Ub )_, where _b = (h+n)/2_. The base case is where _valid(T, Xh | Uh ) = true_ and is guaranteed to exist if _h=max(T)+1_.