The original context for the definition of the partially synchronous model in [DLS1988] was for “one‑shot” Byzantine Agreement — called “the consensus problem” in that paper. The following argument is used to justify assuming that all messages from the Global Stabilization Time onward are delivered within the upper time bound $\Delta$:

Therefore, we impose an additional constraint: For each execution there is a global stabilization time (GST), unknown to the processors, such that the message system respects the upper bound $\Delta$ from time GST onward.

This constraint might at first seem too strong: In realistic situations, the upper bound cannot reasonably be expected to hold forever after GST, but perhaps only for a limited time. However, any good solution to the consensus problem in this model would have an upper bound $L$ on the amount of time after GST required for consensus to be reached; in this case it is not really necessary that the bound $\Delta$ hold forever after time GST, but only up to time GST $+L$. We find it technically convenient to avoid explicit mention of the interval length $L$ in the model, but will instead present the appropriate upper bounds on time for each of our algorithms.

Several subsequent authors applying the partially synchronous model to block chains appear to have forgotten or neglected this context. In particular, the argument depends on the protocol completing soon after GST. Obviously a block‑chain protocol does not satisfy this assumption; it is not a “one‑shot” consensus problem.

This assumption could be removed, but some authors of papers about block‑chain protocols have taken it to be an essential aspect of modelling partial synchrony. I believe this is contrary to the intent of [DLS1988]:

Instead of requiring that the consensus problem be solvable in the GST model, we might think of separating the correctness conditions into safety and termination properties. The safety conditions are that no two correct processors should ever reach disagreement, and that no correct processor should ever make a decision that is contrary to the specified validity conditions. The termination property is just that each correct processor should eventually make a decision. Then we might require an algorithm to satisfy the safety conditions no matter how asynchronously the message system behaves, that is, even if $\Delta$ does not hold eventually. On the other hand, we might only require termination in case $\Delta$ holds eventually. It is easy to see that these safety and termination conditions are [for the consensus problem] equivalent to our GST condition: If an algorithm solves the consensus problem when $\Delta$ holds from time GST onward, then that algorithm cannot possibly violate a safety property even if the message system is completely asynchronous. This is because safety violations must occur at some finite point in time, and there would be some continuation of the violating execution in which $\Delta$ eventually holds.

This argument is correct as stated, i.e. for the one‑shot consensus problem. Subtly, essentially the same argument can be adapted to protocols with safety properties that need to be satisfied continuously. However, it cannot correctly be applied to liveness properties of non‑terminating protocols. The authors (Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer) would certainly have known this: notice how they carefully distinguish “the GST model” from “partial synchrony”. They cannot plausibly have intended this GST formalization to be applied unmodified to analyze liveness in such protocols, which seems to be common in the block‑chain literature, including in the Ebb-and-Flow paper [NTT2020] and the Streamlet paper [CS2020].

The Ebb-and-Flow paper acknowledges the issue by saying “Although in reality, multiple such periods of (a‑)synchrony could alternate, we follow the long‑standing practice in the BFT literature and study only a single such transition.” This is not adequate: “long‑standing practice” notwithstanding, it is not valid in general to infer that properties holding for the first transition to synchrony also apply to subsequent transitions (where the protocol can be in states that would not occur initially), and it is plausible that this inference could fail for real protocols. The Streamlet paper also refers to “periods of synchrony” which indicates awareness of the issue, but then it uses the unmodified GST model in the proofs.

Informally, to solve this issue it is necessary to also prove that existing progress is maintained during periods of asynchrony, and that during such periods the protocol remains in states where it will be able to take advantage of a future period of synchrony to make further progress.

This provides further motivation to avoid taking the GST formalization of partial synchrony as a basic assumption.

Note that the recent result [CGSW2024] does not contradict anything we say here. Although the GST and Unknown Latency models are “equally demanding” in the sense of existence of protocols that satisfy a given goal, this result does not show that the models are equivalent for any specific protocol. In particular the requirements of the “clock‑slowing” technique fail in practice for any protocol involving Proof‑of‑Work.

Streamlet as described in [CS2020] has three possible states of a block in a player’s view:

• “valid” (but not notarized or final);
• “notarized” (but not final);
• “final”.

By “valid” the Streamlet paper means just that it satisfies the structural property of being part of a block chain with parent hashes. The role of $\ast$bft‑block‑validity in our model corresponds roughly to Streamlet’s “notarized”. It turns out that with some straightforward changes relative to Streamlet, we can identify “origbft‑block‑valid” with “notarized” and consider an origbft‑valid‑chain to only consist of notarized blocks. This is not obvious, but is a useful simplification.

Here is how the paper defines “notarized”:

When a block gains votes from at least $2n/3$ distinct players, it becomes notarized. A chain is notarized if its constituent blocks are all notarized.

This implies that blocks can be added to chains independently of notarization. However, the paper also says that an honest leader always proposes a block extending from a notarized chain. Therefore, only notarized chains really matter in the protocol.

In unmodified Streamlet, the order in which a player sees signatures might cause it to view blocks as notarized out of order. Streamlet’s security analysis is in a synchronous model, and assumes for liveness that any vote will have been received by all players (Streamlet nodes) within two epochs.

In Crosslink 2, however, we need origbft‑block‑validity to be an objectively and feasibly verifiable property. We also would prefer reliable message delivery within bounded time not to be a basic assumption of our communication model. (This does not dictate what assumptions about message delivery are made for particular security analyses.) If we did not make a modification to the protocol to take this into account, then some Crosslink 2 nodes might receive a two‑thirds absolute supermajority of voting messages and consider a BFT block to be notarized, while others might never receive enough of those messages.

Obviously a proposal cannot include signatures on itself — but the block formed from it can include proofs about the proposal and signatures. We can therefore say that when a proposal gains a two‑thirds absolute supermajority of signatures, a block is created from it that contains a proof (such as an aggregate signature) that it had such a supermajority. For example, we can have the proposer itself make this proof once it has enough votes, sign the resulting $(P,{\mathsf{proof}}_P)$ to create a block, then submit that block in a separate message. (The proposer has most incentive to do this in order to gain whatever reward attaches to a successful proposal; it can outsource the proving task if needed.) Then the origbft‑block‑validity rule can require a valid supermajority proof, which is objectively and feasibly verifiable. Players that see an origbft‑valid‑block can immediately consider it notarized.

Note that for the liveness analysis to be unaffected, we need to assume that the combined latency of messages, of collecting and aggregating signatures, and of block submission is such that all adapted‑Streamlet nodes will receive a notarized block corresponding to a given proposal (rather than just all of the votes for the proposal) within two epochs. Alternatively we could re‑do the timing analysis.

With this change, “origbft‑block‑valid” and “notarized” do not need to be distinguished.

Streamlet’s finality rule is:

If in any notarized chain, there are three adjacent blocks with consecutive epoch numbers, the prefix of the chain up to the second of the three blocks is considered final. When a block becomes final, all of its prefix must be final too.

We can straightforwardly express this as an $\text{origbft-last-final}$ function of a context block $C$, as required by the model:

For an origbft‑valid‑block $C$, $\text{origbft-last-final}(C)$ is the last origbft‑valid‑block $B{⪯}_{\mathrm{origbft}}C$ such that either $B={\mathcal{O}}_{\mathrm{origbft}}$ or $B$ is the second block of a group of three adjacent blocks with consecutive epoch numbers.

Note that “When a block becomes final, all of its prefix must be final too.” is implicit in the model.

In a Proof‑of‑Work protocol, it is normally possible to check the Proof‑of‑Work of a block using only the header. There is a difficulty adjustment function that determines the target difficulty for a block based on its parent chain. So, checking that the correct difficulty target has been used relies on knowing that the header’s parent chain is valid.

Checking header validity before expending further resources on a purported block can be relevant to mitigating denial‑of‑service attacks that attempt to inflate validation cost.

The literature uses the same name, “common‑prefix property”, for two different properties of very different strength.

[PSS2016, section 3.3] introduced the stronger variant. That paper first describes the weaker variant, calling it the “common‑prefix property by Garay et al [GKL2015].” Then it explains what is essentially a bug in that variant, and describes the stronger variant which it just calls “consistency”:

The common‑prefix property by Garay et al [GKL2015], which was already considered and studied by Nakamoto [Nakamoto2008], requires that in any round $r$, the record chains of any two honest players $i$, $j$ agree on all, but potentially the last $T$, records. We note that this property (even in combination with the other two desiderata [of Chain Growth and Chain Quality]) provides quite weak guarantees: even if any two honest parties perfectly agree on the chains, the chain could be completely different on, say, even rounds and odd rounds. We here consider a stronger notion of consistency which additionally stipulates players should be consistent with their “future selves”.

Let ${\mathsf{consistent}}^T(\mathsf{view})=1$ iff for all rounds $r\le r^{\prime }$, and all players $i$, $j$ (potentially the same) such that $i$ is honest at ${\mathsf{view}}^r$ and $j$ is honest at ${\mathsf{view}}^{r^{\prime }}$, we have that the prefixes of ${\mathcal{C}}_i^r(\mathsf{view})$ and ${\mathcal{C}}_j^{r^{\prime }}(\mathsf{view})$ consisting of the first $\ell =|{\mathcal{C}}_i^r(\mathsf{view})|-T$ records are identical.

Unfortunately, [GKL2020], which is a revised version of [GKL2015], switches to the stronger variant without changing the name.

(The eprint version history may be useful; the change was made in version 20181013:200033, page 17.)

Note that [GKL2020] uses an adaptive‑corruption model, “meaning that the adversary is allowed to take control of parties on the fly”, and so their wording in Definition 3:

... for any pair of honest players $P_1$, $P_2$ adopting the chains ${\mathcal{C}}_1$, ${\mathcal{C}}_2$ at rounds $r_1\le r_2$ in view${}_{\Pi ,\mathcal{A},\mathcal{Z}}^{t,n}$ respectively, it holds that ${\mathcal{C}}_1^{\lceil k}⪯{\mathcal{C}}_2$.

is intended to mean the same as our

... for all times $t\le u$ and all nodes $i$, $j$ (potentially the same) such that $i$ is honest at time $t$ and $j$ is honest at time $u$, we have that ${\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_j^u$.

The latter is closer to [PSS2016].

Incidentally, this property does not seem to be mentioned in [Nakamoto2008], contrary to the [PSS2016] authors’ assertion. Maybe implicitly, but it’s a stretch.

When Prefix Consistency is taken to hold of typical PoW-based block‑chain protocols like Bitcoin (as it often is), this implies that, in the relevant executions, the network of honest nodes is never partitioned — unless any partition lasts only for a short length of time relative to $\sigma$ block times. If node $i$ is on one side of a full partition and node $j$ on the other, then after node $i$’s best chain has been extended by more than $\sigma$ blocks, ${\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }$ will contain information that has no way to get to node $j$. And even if the partition is incomplete, we cannot guarantee that the Prefix Consistency property will hold for any given pair of nodes.

It might be possible to maintain Prefix Consistency if the honest nodes on one side of the partition knew that they should not continue building on their chain until the partition has healed, but it is unclear how that would be done in general without resorting to a BFT protocol (as opposed to in specific cases like a single node being unable to connect to the rest of the network). Certainly there is no mechanism to explicitly detect and respond to partitions in protocols derived from Bitcoin.

And yet, [GKL2020] claims to prove Prefix Consistency from other assumptions. So we know that those assumptions must also rule out a long partition between honest nodes. In fact the required assumption is implicit in the communication model:

• A synchronous network cannot be partitioned.
• A partially synchronous network —that is, providing reliable delivery with bounded but unknown delay— cannot be partitioned for longer than the delay.

We might be concerned that these implicit assumptions are stronger than we would like. In practice, the peer‑to‑peer network protocol of Bitcoin and Zcash attempts to flood blocks to all nodes. This protocol might have weaknesses, but it is not intended to (and plausibly does not) depend on all messages being received. (Incidentally, Streamlet also implicitly floods messages to all nodes.)

Also, Streamlet and many other BFT protocols do not assume for safety that the network is not partitioned. That is, BFT protocols can be safe in a fully asynchronous communication model with unreliable messaging. That is why we avoid taking synchrony or partial synchrony as an implicit assumption of the communication model, or else we could end up with a protocol with weaker safety properties than ${\Pi }_{\mathrm{origbft}}$ alone.

This leaves the question of whether the Prefix Consistency property is still too strong, even if we do not rely on it for the analysis of safety when ${\Pi }_{\mathrm{bft}}$ has not been subverted. In particular, if a particular node $h$ is not well-connected to the rest of the network, then that will inevitably affect node $h$’s security, but should not affect other honest nodes’ security.

Fortunately, it is not the case that disconnecting a single node $h$ from the network causes the security assumption to be voided. The solution is to view $h$ as not honest in that case (even though it would follow the protocol if it could). This achieves the desired effect within the model, because other nodes can no longer rely on $h$’s honest input. Although viewing $h$ as potentially adversarial might seem conservative from the point of view of other nodes, bear in mind that an adversary could censor an arbitrary subset of incoming and outgoing messages from the node, and this may be best modelled by considering it to be effectively controlled by the adversary.

Our security arguments that depend on these properties will all be of the form “in an execution where ⟨safety properties⟩ are not violated, ⟨undesirable thing⟩ cannot happen”.

It is not necessary to involve probability in arguments of this form. Any probabilistic reasoning can be done separately.

In particular, if a statement of this form holds, and ⟨safety properties⟩ are violated with probability at most $p$ under certain conditions, then it immediately follows that under those conditions ⟨undesirable thing⟩ happens with probability at most $p$. Furthermore, ⟨undesirable thing⟩ can only happen after ⟨safety properties⟩ have been violated, because the execution up to that point has been an execution in which ⟨safety properties⟩ are not violated.

With few exceptions, involving probability in a security argument is best done only to account for nondeterministic choices in the protocol itself. This is opinionated advice, but a lot of security proofs would likely be simpler if inherently probabilistic arguments were more distinctly separated from unconditional ones.

In the case of the Prefix Agreement property, an alternative approach would be to prove that Prefix Agreement holds with some probability given Prefix Consistency and some other chain properties. This is what [NTT2020] does in its Theorem 2, which essentially says that under certain conditions Prefix Agreement holds except with probability $e^{-\Omega (\sqrt{\sigma })}$.

The conclusions that can be obtained from this approach are necessarily probabilistic, and depending on the techniques used, the proof may not be tight; that is, the proof may obtain a bound on the probability of failure that is (either asymptotically or concretely) higher than needed. This is the case for [NTT2020, Theorem 2]; footnote 10 in that paper points out that the expression for the probability can be asymptotically improved:

Using the recursive bootstrapping argument developed in [DKT+2020, Section 4.2], it is possible to bring the error probability $e^{-\Omega (\sqrt{\sigma })}$ as close to an exponential decay as possible. In this context, for any $ϵ>0$, it is possible to find constants $A_{ϵ}$, $a_{ϵ}$ such that ${\Pi }_{\mathrm{lc}}(p)$ is secure after C$(\max (\mathsf{GST},\mathsf{GAT}))$ with confirmation time $T_{\mathrm{lc}}=\sigma$ except with probability $A_{ϵ}{e}^{-a_{ϵ}{\sigma }^{1-ϵ}}$.

(Here $p$ is the probability that any given node gets to produce a block in any given time slot.)

In fact none of the proofs of security properties for Snap‑and‑Chat depend on the particular expression $e^{-\Omega (\sqrt{\sigma })}$; for example in the proofs of Lemma 5 and Theorem 1, this probability just “passes through” the proof from the premisses to the conclusion, because the argument is not probabilistic. The same will be true of our safety arguments.

Talking about what is possible in particular executions has further advantages:

• It sidesteps the issue of how to interpret results in the GST model of partial synchrony, when we do not know what C$(\max (\mathsf{GST},\mathsf{GAT}))$ is. See also the critique of applying the GST model to block‑chain protocols under “Discussion of [GKL2020]’s communication model and network partition” above. (This is not an inherent problem with analyzing the protocol in the partially synchronous setting, but only with inappropriate use of the GST model of that setting.)
• We do not require ${\Pi }_{\mathrm{bc}}$ to be a Nakamoto‑style Proof‑of‑Work block chain protocol. Some other kind of protocol could potentially satisfy Prefix Consistency and Prefix Agreement.
• It is not clear whether a $e^{-\Omega (\sqrt{\sigma })}$ probability of failure would be concretely adequate. That would depend on the value of $\sigma$ and the constant hidden by the $\Omega$ notation. The asymptotic property using $\Omega$ tells us whether a sufficiently large $\sigma$ could be chosen, but we are more interested in what needs to be assumed for a given concrete choice of $\sigma$.
• If a violation of a required safety property occurs in a given execution, then the safety argument for Crosslink that depended on the property fails for that execution, regardless of what the probability of that occurrence was. This approach therefore more precisely models the consequences of such violations.

Roughly speaking, the intuition behind both properties is as follows:

Honest nodes are collectively able to find blocks faster than an adversary, and communication between honest nodes is sufficiently reliable that they act as a combined network racing against that adversary. Then by the argument in [Nakamoto2008], modified by [GP2020] to correct an error in the concrete analysis, a private mining attack that attempts to cause a $\sigma$‑block rollback will, with high probability, fail for large enough $\sigma$. A private mining attack is optimal by the argument in [DKT+2020].

Any further analysis of the conditions under which these properties hold should be done in the context of a particular ${\Pi }_{\ast \mathrm{bc}}$.

This strengthens the security property, relative to quantifying over a single time. The question can then be split into several parts:

1. What does the strengthened property mean, intuitively? Consider the full tree of $\ast$bc‑valid-blocks that honest nodes have considered to be part of their $\ast$bc‑best-chain at any times during the execution. This property holds iff, when we strip off all branches of length up to and including $\sigma$ blocks, the resulting tree is $\ast$bc‑linear.
2. Why is the strengthening needed? Suppose that time were split into periods such that honest nodes agreed on one chain in odd periods, and a completely different chain in even periods. This would obviously not satisfy the intent, but it would satisfy a version of the property that did not quantify over different times $t$ and $u$.
3. Why should we expect the strengthened property to hold? If node $j$ were far ahead, i.e. $u\gg t$, then it is obvious that ${\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_j^u{\lceil }_{\ast \mathrm{bc}}^{\sigma }$ should hold. Conversely, if node $i$ were far ahead then it is obvious that ${\mathsf{ch}}_j^u{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }$ should hold. The case where $t=u$ is the same as quantifying over a single time. By considering intermediate cases where $t$ and $u$ converge from the extremes or where they diverge from being equal, you should be able to convince yourself that the property holds for any relative values of $t$ and $u$, in executions of a reasonable best‑chain protocol.

For a bft‑proposal or bft‑block $B$, the role of the bc‑chain snapshot referenced by $B.headers\_bc[0]{\lceil }_{\mathrm{bc}}^1$ is comparable to the ${\Pi }_{\mathrm{lc}}$ snapshot referenced by $B.\mathsf{ch}$ in the Snap‑and‑Chat construction from [NTT2020]. The motivation for the additional headers is to demonstrate, to any party that sees a bft‑proposal (resp. bft‑block), that the snapshot had been confirmed when the proposal (resp. the block’s proposal) was made.

Typically, a node that is validating an honest bft‑proposal or bft‑block will have seen at least the snapshotted bc‑block (and possibly some of the subsequent bc‑blocks in the $headers\_bc$ chain) before. For this not to be the case, the validator’s bc‑best‑chain would have to be more than $\sigma$ bc‑blocks behind the honest proposer’s bc‑best‑chain at a given time, which would violate the Prefix Consistency property of ${\Pi }_{\mathrm{bc}}$.

If the headers do not connect to any bc‑valid‑chain known to the validator, then the validator should be suspicious that the proposer might not be honest. It can assign a lower priority to validating the proposal in this case, or simply drop it. The latter option could drop a valid proposal, but this does not in practice cause a problem as long as a sufficient number of validators are properly synced (so that Prefix Consistency holds for them).

If the headers do connect to a known bc‑valid‑chain, it could still be the case that the whole header chain up to and including $B.headers\_bc[\sigma -1]$ is not a bc‑valid‑chain. Therefore, to limit denial‑of‑service attacks the validator should first check the Proofs‑of‑Work and difficulty adjustment —which it can do locally using only the headers— before attempting to download and validate any bc‑blocks that it has not already seen. This is why we include the full headers rather than just the block hashes. Nodes may “trim” (i.e. not explicitly store) headers in a bft‑block that overlap with those referred to by its ancestor bft‑block(s).

It would be conceptually nice for ${\mathcal{O}}_{\mathrm{bft}}.\mathsf{headers}[0]{\lceil }_{\mathrm{bc}}^1$ to refer to ${\mathcal{O}}_{\mathrm{bc}}$, as well as ${\mathcal{O}}_{\mathrm{bc}}.context\_bft$ being ${\mathcal{O}}_{\mathrm{bft}}$ so that $\text{bft-last-final}({\mathcal{O}}_{\mathrm{bc}}.context\_bft)={\mathcal{O}}_{\mathrm{bft}}$. That reflects the fact that we know “from the start” that neither genesis block can be rolled back.

This is not literally implementable using block hashes because it would involve a hash cycle, but we achieve the same effect by defining a $\mathsf{snapshot}$ function that allows us to “patch” $\mathsf{snapshot}({\mathcal{O}}_{\mathrm{bft}})$ to be ${\mathcal{O}}_{\mathrm{bc}}$. We do it this way around rather than “patching” the link from a bc‑block to a bft‑block, because the genesis bft‑block already needs a special case since there are not $\sigma$ bc‑headers available.

The finality of some bft‑block is only defined in the context of another bft‑block. One possible design would be for a bc‑block to have both $final\_bft$ and $context\_bft$ fields, so that the finality of $final\_bft$ could be checked objectively in the context of $context\_bft$.

However, specifying just the context block is sufficient information to determine its last final ancestor. There would never be any need to give a context block and a final ancestor that is not the last one. The $\text{bft-last-final}$ function can be computed efficiently for typical BFT protocols. Therefore, having just the $context\_bft$ field is sufficient.

When a node’s view of the bc‑best‑chain reorgs to a different fork (even if the reorg is shorter than $\sigma$ blocks), it may be the case that $\mathsf{candidate}({\mathsf{ch}}_i^t)$ rolls back. If Final Agreement of ${\Pi }_{\mathrm{bft}}$ holds up to time $t$, the new snapshot should in that case be an ancestor of the old one. If all is well then this snapshot will subsequently roll forward along the same path. However, we do not want applications using the node to see the temporary rollback.

This ensures that the candidate is at least $\sigma$‑confirmed.

In practice $\mathsf{candidate}(H)$ will rarely differ from $\mathsf{snapshot}(\mathsf{LF}(H))$, but using the former patches over a potential gap in the safety proof. The Last Final Snapshot rule specified later will guarantee that $\mathsf{snapshot}(\mathsf{LF}(H)){⪯}_{\mathrm{bc}}H$, and this ensures that $\mathsf{snapshot}(\mathsf{LF}(H))⪯{⪰}_{\mathrm{bc}}H{\lceil }_{\mathrm{bc}}^{\sigma }$. However, the depth of $\mathsf{snapshot}(\mathsf{LF}(H))$ relative to $H$ is not guaranteed to be $\ge \sigma$. For the proof we will need $\mathsf{candidate}(H){⪯}_{\mathrm{bc}}H{\lceil }_{\mathrm{bc}}^{\sigma }$, so that we can use the Local fin‑depth lemma together with Prefix Agreement of ${\Pi }_{\mathrm{bc}}$ at confirmation depth $\sigma$ to prove Assured Finality.

An alternative would be to change the Last Final Snapshot rule to directly require $\mathsf{snapshot}(\mathsf{LF}(H)){⪯}_{\mathrm{bc}}H{\lceil }_{\mathrm{bc}}^{\sigma }$.

$\text{TODO:}$ Choose between these options based on what works well for the security proofs and finalization latency.

Assume for this discussion that ${\Pi }_{\mathrm{bc}}$ uses PoW.

Depending on the value of $\sigma$, the timestamps of bc‑blocks, and the difficulty adjustment rule, it can be the case that if $\mathsf{fin}{}_i$ switches to a different fork, the difficulty on that fork is greater than on the chain of the previous snapshot. Then, the new bc‑chain could reach a higher score than the previous chain in fewer than $\sigma$ blocks from the fork point, and so ${\mathsf{ch}}_i^t{\lceil }_{\mathrm{bc}}^{\mu }$ might not be a descendant of $\mathsf{fin}{}_i^t$ (which is more likely if $\mu =\sigma$). This can occur even when all safety assumptions are satisfied.

For Zcash’s difficulty adjustment algorithm, the difficulty of each block is adjusted based on the median timestamps and difficulty target thresholds over a range of $\mathsf{PoWAveragingWindow}=17$ blocks, where each median is taken over $\mathsf{PoWMedianBlockSpan}=11$ blocks. Other damping factors and clamps are applied in order to prevent instability and to reduce the influence that adversarially chosen timestamps can have on difficulty adjustment. This makes it unlikely that an adversary could gain a significant advantage by manipulating the difficulty adjustment. So it is safe to use $\mathsf{fin}{}_i^t$ in this case: even though it does not have $\mu$ confirmations relative to ${\mathsf{ch}}_i^t$, it does have at least the required amount of work “on top” of it.

Defining $({\mathsf{ba}}_{\mu }{)}_i^t$ this way also has the advantage of making the proof of the Ledger prefix property trivial.

The reason to separate the validity rules from the honest voting condition, is that the validity rules are objective: they don’t depend on an observer’s view of the bc‑best‑chain. Therefore, they can be checked independently of validator signatures. Even a proposal voted for by 100% of validators will not be considered bft‑proposal‑valid by other nodes unless it satisfies the above rules. If more than two thirds of voting units are cast for an invalid proposal, something is seriously and visibly wrong; in any case, the block will not be accepted as a bft‑valid‑block. Importantly, a purportedly valid bft‑block will not be recognized as such by any honest Crosslink 2 node even if it includes a valid notarization proof, if it does not meet other bft‑block‑validity rules.

This is essential to making the finalized chain safe against a flaw in ${\Pi }_{\mathrm{bft}}$ or its security assumptions (even, say, a complete break of the validator signature algorithm), as long as ${\Pi }_{\mathrm{bc}}$ remains safe.

This rule is key to combining simplicity with strong security properties in Crosslink 2. It essentially says that, in a given bft‑valid‑chain, the snapshots pointed to by blocks in that chain cannot roll back.

This allows the informal safety argument for Crosslink 2 to be rather intuitive.

Informally, if ${\Pi }_{\mathrm{bft}}$ has Final Agreement, then all nodes see only one consistent bft‑linear chain (restricting to bft‑blocks that are final in the context of some bft‑block in honest view). Within such a bft‑chain, the Linearity rule ensures by construction that the sequence of referenced bc‑chain snapshots is bc‑linear. This implies Assured Finality, without needing to assume any safety property of ${\Pi }_{\mathrm{bc}}$.

We will also be able to prove safety of the finalized snapshots based only on safety of ${\Pi }_{\mathrm{bc}}$ (for a confirmation depth of $\sigma$), without needing to assume any safety property of ${\Pi }_{\mathrm{bft}}$. Informally, that is because each node sees each candidate final snapshot at a given time as a $\sigma$-confirmed prefix of its bc‑best‑chain at that time (this can be proven based on the Last Final Snapshot rule and the fact that a snapshot includes $\sigma$ subsequent headers), and Prefix Agreement implies that honest nodes agree on this prefix. We will leave a more detailed argument until after we have presented the ${\Pi }_{\mathrm{bc}}$ changes from ${\Pi }_{\mathrm{origbc}}$.

The Linearity rule replaces the “Increasing Score rule” used in Crosslink 1. The Increasing Score rule required that each snapshot in a bft‑valid‑chain either be the same snapshot, or a higher-scoring snapshot to that of its parent block. Since scores strictly increase within a bc‑valid‑chain, the Linearity rule implies the Increasing Score rule. It retains the same or stronger positive effects:

• It prevents potential attacks that rely on proposing a bc‑valid‑chain that forks from a much earlier block. This is necessary because the difficulty (or stake threshold) at that point could have been much lower.
• It limits the extent of disruption an adversary can feasibly cause to the bounded‑available chain ${\mathsf{ch}}_i$, even if it has subverted ${\Pi }_{\mathrm{bft}}$. Informally, because the finalized chain is a ${\Pi }_{\mathrm{bc}}$ chain, its safety is no worse than ${\Pi }_{\mathrm{bc}}$ alone for a rollback of any depth.
• It ensures that either progress is made (the snapshot advances relative to that of the parent bft‑block), or there is no further validation that needs to be done for the snapshot because it was already validated.

Note that the adversary could take advantage of an “accidental” fork and start its attack from the base of that fork, so that not all of this work is done by it alone. This is also possible in the case of a standard “private mining” attack, and is not so much of a problem in practice because accidental forks are expected to be short. In any case, $\sigma$ should be chosen to take it into account.

The Linearity rule is also critical to removing the need for one of the most complex elements of Snap‑and‑Chat and Crosslink 1, “sanitization”. In those protocols, because bc‑chain snapshots could be unrelated to each other, it was necessary to sanitize the chain formed from these snapshots to remove transactions that were contextually invalid (e.g. because they double‑spend). The negative consequences of this are described in Notes on Snap‑and‑Chat; avoiding it is much simpler.

The linearity property is intentionally always relative to the snapshot of the parent bft‑block, even if it is not final in the context of the current bft‑block. This is because the rule needs to hold if and when it becomes final in the context of some descendant bft‑block.

$\text{TODO:}$ PoS Desideratum: we want leader selection with good security / performance properties that will be relevant to this rule. (Suggested: PoSAT.)

This is necessary in order to preserve liveness of ${\Pi }_{\mathrm{bft}}$ relative to ${\Pi }_{\mathrm{origbft}}$. Liveness of ${\Pi }_{\mathrm{origbft}}$ might require honest proposers to make proposals at a minimum rate. That requirement could be consistently violated if it were not always possible to make a valid proposal. But given that it is allowed to repeat the same snapshot as in the parent bft‑block, neither the Linearity rule nor the Tail Confirmation rule can prevent making a valid proposal — and all other rules of ${\Pi }_{\mathrm{bft}}$ affecting the ability to make valid proposals are the same as in ${\Pi }_{\mathrm{origbft}}$. (In principle, changes to voting in ${\Pi }_{\mathrm{bft}}$ could also affect its liveness; we’ll discuss that in the liveness proof later.)

For example, Streamlet requires three notarized blocks in consecutive epochs in order to finalize a block [CS2020, section 1.1]. Its proof of liveness depends on the assumption that in each epoch for which the leader is honest, that leader will make a proposal, and that during a “period of synchrony” this proposal will be received by every node [CS2020, section 3.6]. This argument can also be extended to adapted‑Streamlet.

We could alternatively have allowed to always make a “null” proposal, rather than to always make a proposal with the same snapshot as the parent. We prefer the latter because the former would require specifying the rules for null proposals in ${\Pi }_{\mathrm{origbft}}$.

As a clarification, no BFT protocol that uses leader election can require a proposal in each epoch, because the leader might be dishonest. The above issue concerns liveness of the protocol when assumptions about the attacker’s share of bft‑validators or stake are met, so that it can be assumed that sufficiently long periods with enough honest leaders to make progress (5 consecutive epochs in the case of Streamlet), will occur with significant probability.

If the length were less than $\sigma +1$ blocks, it would be impossible to construct the $headers\_bc$ field of the proposal.

Note that when the length of the proposer’s bc‑best‑chain is exactly $\sigma +1$ blocks, the snapshot must be of ${\mathcal{O}}_{\mathrm{bc}}.$ But this does not violate the Linearity rule, because ${\mathcal{O}}_{\mathrm{bc}}$ matches the previous snapshot by ${\mathcal{O}}_{\mathrm{bft}}$.

As in the answer to Why is the ‘otherwise’ case in the definition of $({\mathsf{ba}}_{\mu }{)}_i^t$ necessary? above, after a reorg on the bc‑chain, the $\sigma$-confirmed block on the new chain might not be a descendant of the $\sigma$-confirmed block on the old chain, which could break the Linearity rule.

In general the entire referenced bft‑chain needs to be validated, not just the referenced block — and for each bft‑block, the bc‑chain in $headers\_bc$ needs to be validated, and so on recursively. If this sounds overwhelming, note that:

• We should check the requirement that a bft‑valid‑block must have been voted for by a two‑thirds absolute supermajority of validators, and any other non‑recursive bft‑validity rules, first.
• Before validating a bc‑chain referenced by a $headers\_bc$ field, we check that it connects to an already-validated bc‑chain and that the Proofs‑of‑Work are valid. This implies that the amount of bc‑block validation is constrained by how fast the network can find valid Proofs‑of‑Work.
• The Linearity rule reduces the worst‑case validation effort, by ensuring that only one bc‑chain needs to be validated for any bft‑chain. Assuming safety of ${\Pi }_{\mathrm{bft}}$ and that the adversary does not have an overwhelming advantage in computing the Proof‑of‑Work, this is effectively only one bc‑chain overall with, at most, short side branches.

In summary, the order of validation is important to avoid denial‑of‑service — but it already is in Bitcoin and Zcash.

The Confirmed best‑chain criterion is quite subtle. It ensures that $\mathsf{snapshot}(P)=P.headers\_bc[0]{\lceil }_{\mathrm{bc}}^1$ is bc‑block‑valid and has $\sigma$ bc‑block‑valid blocks after it in the validator’s bc‑best‑chain. However, it need not be the case that $P.headers\_bc[\sigma -1]$ is part of the validator’s bc‑best‑chain after it updates its view. That is, the chain could fork after $\mathsf{snapshot}(P)$.

The bft‑proposal‑validity rule must be objective; it can’t depend on what the validator’s bc‑best‑chain is. The validator’s bc‑best‑chain may have been updated to $P.headers\_bc[\sigma -1]$ (if it has the highest score), but it also may not.

However, if the validator’s bc‑best‑chain was updated, that makes it more likely that it will be able to vote for the proposal.

In any case, if the validator does not check that all of the blocks referenced by the headers are bc‑block‑valid, then its vote may be invalid.

Snap‑and‑Chat already had the voting condition:

An honest node only votes for a proposed BFT block $B$ if it views $B.\mathsf{ch}$ as confirmed.

but it did not give the headers potentially needed to update the validator’s view, and it did not require a proposal to be for an objectively confirmed snapshot as a matter of validity.

If a Crosslink‑like protocol were to require an objectively confirmed snapshot but without including the bc‑headers in the proposal, then validators would not immediately know which bc‑blocks to download to check its validity. This would increase latency, and would be likely to lead proposers to be more conservative and only propose blocks that they think will already be in at least a two‑thirds absolute supermajority of validators’ best chains.

That is, showing $P.headers\_bc$ to all of the validators is advantageous to the proposer, because the proposer does not have to guess what blocks the validators might have already seen. It is also advantageous for the protocol goals in general, because it improves the trade‑off between finalization latency and security.

The finality depth must be objectively defined, since it is used in a consensus rule. Therefore it should measure the height of $H$ relative to $\mathsf{snapshot}(\mathsf{LF}(H))$, which is an objectively defined function of $H$, rather than relative to $\mathsf{fin}{}_i^t$. (These will only differ for $H={\mathsf{ch}}_i^t$ when node $i$ has just reorged, and only then in corner cases.)

Note that the Last Final Snapshot rule ensures that it is meaningful to simply use the difference in heights, since $\mathsf{snapshot}(\mathsf{LF}(H)){⪯}_{\mathrm{bc}}H$.

The effect of this would be to tend to more often follow the last bft‑block seen by the producer of the parent bc‑block, if there is a choice. It is not always possible to do so, though: the resulting set of candidates for $C$ might be empty.

Also, it is not clear that giving the parent bc‑block‑producer the chance to “guide” what bft‑block should be chosen next is beneficial, since that producer might be adversarial and the resulting incentives are difficult to reason about.

We could have instead chosen $C$ to maximize the length of $\text{bft-last-final}(C)$. The rule we chose follows Streamlet, which builds on the longest notarized chain, not the longest finalized chain. This may call for more analysis specific to the chosen BFT protocol.

Choosing the bft‑chain that has the last final snapshot with the highest score, tends to inhibit an adversary’s ability to finalize its own chain if it has a lesser score. (If it has a greater score, then it has already won a hash race and we cannot stop the adversary chain from being finalized.)