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 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 latter does refer to “periods of synchrony” which indicates awareness of the issue, but then it uses the unmodified GST model in the proofs.)

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

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 a 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 within two epochs.

In Crosslink, 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 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‑block‑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 players 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.

It is needed for equivalence of the following two ways to construct ${\mathsf{LOG}}_{\{\mathrm{fin},\mathrm{bda}\}}$:

1. Concatenate the transactions from each bft‑block snapshot of a bc‑chain, and sanitize the resulting transaction sequence by including each transaction iff it is contextually valid.
2. Concatenate the bc‑blocks from each bft‑block snapshot of a bc‑chain, remove duplicate blocks, and only then sanitize the resulting transaction sequence by including each transaction iff it is contextually valid.

We want these to be equivalent to enable a crucial optimization. In practice there will be many duplicate blocks from chain prefixes in the input to sanitization, and so a literal implementation of the first variant would have to recheck all duplicate transactions for contextual validity. That would have at least $O(n^2)$ complexity (more likely $O(n^2\log n)$) in the length $n$ of the block chain, because the length of each final snapshot grows with $n$. But in the second variant, we can just concatenate suffixes of each snapshot omitting any bc‑blocks that are common to a previous snapshot.

Given that the only reasons for a transaction to be contextually invalid are double‑spends and missing inputs, the argument for equivalence is that:

• If a transaction is omitted due to a double‑spend, then any subsequent time it is checked, that input will still have been double‑spent.
• If a transaction is omitted due to a missing input, this can only be because an earlier transaction in the input to sanitization was omitted. So the structure of omitted transactions forms a DAG in which parent links must be to earlier omitted transactions. The roots of the DAG are at double-spending transactions, which cannot be reinstated (that is, included after they had previously been excluded). A child cannot be reinstated until its parents have been reinstated. Therefore, no transactions are reinstated.

It might be possible to relax this assumption, but it would require additional analysis to ensure that the above equivalence still holds.

In Zcash, a block logically contains its transactions by having the block header commit to a Merkle tree over txids, and another Merkle tree (in the same transaction order) over witness hashes. A txid and witness hash together authenticate all data fields of a transaction.

For v5 transactions, the txid commits to effecting data (that determines the effect of the transaction) and the witness hash commits to witness data (signatures and proofs). For earlier transaction versions, the witness hash is null and the txid commits to all transaction data.

When a block is downloaded, its transactions are parsed and its header is checked against the transaction data. Assuming no bugs or errors in the design, this is effectively equivalent to the block data being directly authenticated by the header.

There are several Zcash consensus rules that mention block height or position within a block, or that depend on other transactions in a block:

Transaction consensus rule:

• A coinbase transaction for a non‑genesis block MUST have a script that, as its first item, encodes the block height [in a specified way].

In addition, a coinbase transaction is implicitly able to spend the total amount of fees of other transactions in the block.

Block consensus rule:

• The first transaction in a block MUST be a coinbase transaction, and subsequent transactions MUST NOT be coinbase transactions.

Payment of Founders’ Reward:

• [Pre‑Canopy] A coinbase transaction at $\mathsf{height}\in \{\mathrm{1..}\mathsf{FoundersRewardLastBlockHeight}\}$ MUST include at least one output that pays exactly $\mathsf{FoundersReward}(\mathsf{height})$ zatoshi with [details of script omitted].

Payment of Funding Streams:

• [Canopy onward] The coinbase transaction at block height $\mathsf{height}$ MUST contain at least one output per funding stream $\mathsf{fs}$ active at $\mathsf{height}$, that pays $fs.Value(\mathsf{height})$ zatoshi in the prescribed way to the stream’s recipient address [...]

However, none of these need to be treated as contextual validity rules.

The following transaction consensus rule must be modified:

• A transaction MUST NOT spend a transparent output of a coinbase transaction from a block less than 100 blocks prior to the spend. Note that transparent outputs of coinbase transactions include Founders’ Reward outputs and transparent funding stream outputs.

To achieve the intent, it is sufficient to change this rule to only allow coinbase outputs to be spent if their coinbase transaction has been finalized.

If we assume that coinbase block subsidies and fees, and the position of coinbase transactions as the first transaction in each block have already been checked as $\ast$bc‑block‑validity rules, then the model is sufficient.

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 t^{\prime }$ and all nodes $i$, $j$ (potentially the same) such that $i$ is honest at time $t$ and $j$ is honest at time $t^{\prime }$, we have that ${\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_j^{t^{\prime }}$.

(The latter is closer to [PSS2016].)

Incidentally, I cannot find any variant of this property in [Nakamoto2008]. Maybe implicitly, but it’s a stretch.

Prefix Consistency implies that, in the relevant executions, the network of honest nodes is never partitioned — unless (roughly speaking) 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.

And yet, [GKL2020] claims to prove this property 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 I think a lot of security proofs would 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{confirm}}=\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 partially synchronous model, when we do not know what C$(\max (\mathsf{GST},\mathsf{GAT}))$ is. See also the critique of applying the partially synchronous model to block-chain protocols under “Discussion of [GKL2020]’s communication model and network partition” above.
• 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‑blocks seen by honest nodes 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 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 $t^{\prime }$.
3. Why should we expect the strengthened property to hold? If node $j$ were far ahead, i.e. $t^{\prime }\gg t$, then it is obvious that ${\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_j^{t^{\prime }}{\lceil }_{\ast \mathrm{bc}}^{\sigma }$ should hold. Conversely, if node $i$ were far ahead then it is obvious that ${\mathsf{ch}}_j^{t^{\prime }}{\lceil }_{\ast \mathrm{bc}}^{\sigma }{⪯}_{\ast \mathrm{bc}}{\mathsf{ch}}_i^t{\lceil }_{\ast \mathrm{bc}}^{\sigma }$ should hold. The case where $t=t^{\prime }$ is the same as quantifying over a single time. By considering intermediate cases where $t$ and $t^{\prime }$ 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 $t^{\prime }$, 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.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 $header\_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.

It would be conceptually nice for ${\mathcal{O}}_{\mathrm{bft}}.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.

If this were enforced, it could be an alternative way of ensuring that every bft‑proposal snapshots a new bc‑block with a higher score than previous snapshots, potentially making the Increasing Score rule redundant. However, it would require merging bc‑block producers and bft‑proposers, which could have concerning knock‑on effects (such as concentrating security into fewer participants).

For a contrary view, see What about making the bc‑block‑producer the bft‑proposer? in Potential changes to Crosslink.

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 valid bft‑block. Importantly, a purportedly valid bft‑block will not be recognized as such by any honest Crosslink node even if it includes a valid notarization proof, if it does not meet other bft‑block‑validity rules.

This is essential to making ${\mathsf{LOG}}_{\mathrm{fin}}$ 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 ensures that each snapshot in a bft‑valid‑chain is strictly “better” than the last distinct snapshot (and therefore any earlier distinct snapshot), according to the same metric used to choose the bc‑best‑chain.

This rule has several 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 ${\mathsf{LOG}}_{\mathrm{bda},i}$, even if it has subverted ${\Pi }_{\mathrm{bft}}$. In particular, if transactions are inserted into ${\mathsf{LOG}}_{\mathrm{bda},i}$ at the finalization point, this rule ensures that they can only come from a bc‑valid‑chain that has a higher score than the previous snapshot. And since the adversary must prove that its snapshot is confirmed, there must be at least $\sigma$ blocks’ worth of Proof‑of‑Work on top of that snapshot, at a difficulty close to the current network difficulty. 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.
• A snapshot with a higher score than any previous snapshot cannot be a prefix of a previous snapshot (because score strictly increases within a bc‑valid‑chain). So, this excludes proposals that would be a no‑op for that reason.

The increase in score 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.

==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 Increasing Score 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.

Consider the following variant of the Increasing Score rule: $\mathsf{score}(\mathsf{snapshot}(B{\lceil }_{\mathrm{bft}}^1))\le \mathsf{score}(\mathsf{snapshot}(B))$.

This would allow keeping the same snapshot as the parent as discussed in the previous answer. However, it would also allow continually cycling within a given set of snapshots, without making progress and without needing any new Proof‑of‑Work to be performed. This is worse than not making progress due to the same snapshot continually being proposed, because it increases the number of snapshots that need to be considered for sanitization, and therefore it could potentially be used for a denial‑of‑service.

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 Increasing Score rule, because ${\mathcal{O}}_{\mathrm{bc}}$ matches the previous snapshot by ${\mathcal{O}}_{\mathrm{bft}}$.

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 could be the case that the difficulty on the new bc‑best‑chain increases relative to the chain of the previous snapshot. In that case, when there is a fork, the new chain could reach a higher score than the previous chain in less than $\sigma$ blocks from the fork point, and so its $\sigma$‑confirmed snapshot could be before the previous snapshot.

(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.)

For a variation on the Increasing Score rule that would be automatically satisfied by choosing headers from the proposer’s bc‑best‑chain, see Potential changes to Crosslink.

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.

In other words, 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.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.

We need a way to measure how far ahead a given bc‑block is relative to the corresponding finalization point. ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ is a sequence of transactions, not blocks, so it is not entirely obvious how to do this.

Let $H={\mathsf{ch}}_i^t$, i.e. the tip of node $i$’s bc‑best‑chain at time $t$.

Then, $\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })$ is the bft‑block providing the last ${\Pi }_{\mathrm{bc}}$ snapshot that will be used to construct ${\mathsf{LOG}}_{\mathrm{fin},i}^t$. $\mathsf{tailhead}(H)$ is the last common ancestor of that snapshot and $H$.

The idea behind the above definition is that:

• If $\mathsf{snapshot}(\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma }))$ is an ancestor of $H$, then it is equal to $\mathsf{tailhead}(H)$, and that is the last bc‑block that contributes to ${\mathsf{LOG}}_{\mathrm{fin},i}^t$. If the best chain were to continue from $H$ without a rollback, then the bc‑blocks to be finalized next would be the ones from $\mathsf{tailhead}(H)$ to $H$, and so the number of those blocks gives the finality depth.
• Otherwise, $\mathsf{snapshot}(\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma }))$ must be on a different fork, and the bc‑blocks to be finalized next would resume from the fork point toward $H$ — unless some of those blocks have already been included, as discussed below. ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ will definitely contain transactions from blocks up to $\mathsf{tailhead}(H)$, but usually not subsequent transactions on $H$’s fork. So it is still reasonable to measure the finality depth from $\mathsf{tailhead}(H)$ to $H$.

Strictly speaking, it is possible that a previous bft‑block took a snapshot $H^{\prime }$ that is between $\mathsf{tailhead}(H)$ and $H$. This can only happen if there have been at least two rollbacks longer than $\sigma$ blocks (i.e. we went more than $\sigma$ blocks down $H$’s fork from $\mathsf{tailhead}(H)$, then reorged to more than $\sigma$ blocks down the fork to $\mathsf{snapshot}(\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma }))$, then reorged again to $H$’s fork). In that case, the finalized ledger would already have the non‑conflicting transactions from blocks between $\mathsf{tailhead}(H)$ and $H^{\prime }$ — and it could be argued that the correct definition of finality depth in such cases is the number of blocks from $H^{\prime }$ to $H$, not from $\mathsf{tailhead}(H)$ to $H$.

However,

• The definition above is simpler and easier to compute.
• The effect of overestimating the finality depth in such corner cases would only cause us to enforce Safety Mode slightly sooner, which seems fine (and even desirable) in any situation where there have been at least two rollbacks longer than $\sigma$ blocks.

By the way, the “tailhead” of a tailed animal is the area where the posterior of the tail joins the rump (also called the “dock” in some animals).

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.)

If we switch to using the Increasing Tip Score rule, then it would be more consistent to also change this tie‑breaking rule to use the tip score, i.e. $\mathsf{score}(\mathsf{tip}(\text{bft-last-final}(C)))$.