A Trailing Finality Layer for Zcash

This book introduces and specifies a Trailing Finality Layer for the Zcash network. This is version 0.1.0 of the book.

This design augments the existing Zcash Proof-of-Work (PoW) network with a new consensus layer which provides trailing finality. This layer enables transactions included via PoW to become final which assures that they cannot be reverted by the protocol. This enables safer and simpler wallets and other infrastructure, and aids trust-minimized cross-chain bridges. This consensus layer uses Proof-of-Stake consensus, and enables ZEC holders to earn protocol rewards for contributing to the security of the Zcash network. By integrating a PoS layer with the current PoW Zcash protocol, this design specifies a hybrid consensus protocol dubbed PoW+TFL.

The rest of this introductory chapter is aimed at a general audience interested in the context of this proposal within Zcash development, status and next steps, motivations, a primer on finality, and tips to get involved.

A Path to Proof-of-Stake Zcash

The TFL design provides a possible first step in transitioning Zcash to a PoS protocol. Here we describe how a transition to PoS relates to "the Zcash roadmap" and how TFL fits into one approach to a PoS transition.

The Zcash Tech-Tree

There are multiple developer orgs working on different proposed features for Zcash. Some of these involve multiple large distinct upgrade steps, and several of these steps depend on other such steps. This could be represented as a directed acyclic graph. We have begun referring to this space of possible future improvements as the Zcash Tech-Tree, taking inspiration from an analogous concept in gaming.¹

We envision a proof-of-stake transition path as one of the potential paths within this tech-tree which is the primary protocol focus of this proposal. An example visualization of this Zcash Tech-Tree might look like this:

A Proof-of-Stake Transition Path

Given that context, we envision a path within the Zcash Tech-Tree for transitioning Zcash to PoS. At the top level we propose that this path contain at least two major milestones:

1. Transitioning from current Zcash NU5 PoW protocol to a PoW/PoS hybrid consensus protocol dubbed PoW+TFL.
2. Transitioning from PoW+TFL to pure PoS protocol.

After this transition to pure PoS, there are likely to be future improvements to the PoS protocol, or the consensus protocol more generally. This TFL book focuses almost exclusively on the first step in this sequence.

Our primary motivation for proposing (at least) two steps is to minimize disruption to usability, safety, security, and the ecosystem during each step.

This book primarily focuses this first step: the transition to PoW+TFL. To understand the specific goals for that, see Design Goals.

With this approach, the Zcash Tech Tree with the TFL approach might look something like this:

Why Two Steps?

One question we've gotten in proposing this approach is why take a two-step process with an intermediate hybrid consensus protocol, rather than a single transition directly to a PoS protocol?

Here's how we think about those trade-offs:

Considering Single Transition (vs Hybrid Multi-Step)

Pros

• We already understand the current PoW protocol well, and if we transition to an existing proven PoS protocol, then we could skip the complexity of an intermediate hybrid stage.
• The node implementation might be simpler.
• Explaining to people what is happening might be simpler. Something like “Zcash has been PoW since it launched, but on DATE (e.g. at block height X) it will switch to PoS.”
• Given that the issuance in a given time period is bounded by the supply curve, the full amount that was previously allocated to mining rewards becomes immediately available for staking rewards at the switch-over, rather than having to share this amount between mining and staking during the hybrid stage.

Cons

• If there is any unforeseen show-stopping problem in the new protocol or the transition process, we’d have to react to a network-wide issue.
• It may be more likely to cause ecosystem disruption; unforeseen differences between PoW and PoS might cause various kinds of snags or papercuts throughout the ecosystem, and these would all pop up around the same time, which may lead to a loss of confidence/retention/adoption or at the very least inconvenience many users for some time.
• Losing miners: since the transition would be all at once, we may lose some number of miners, who are participants and users in the ecosystem. Miners may leave prior to the transition in order to take care of their own needs. If there is some show-stopper in the transition, one possible short-term mitigation would be to fall back on PoW which is well known, but if we’ve lost most miners, that may no longer be viable.

Considering Hybrid Multi-Step approach (vs Single-Step):

Note: TFL is one instance of a multi-step approach.

Pros

• We can hopefully be less disruptive across the ecosystem so that there are fewer snags and disruptions with each step.
• If there is a show-stopping flaw in any step, the fall-back possibility seems more plausible. For example, if there is a show-stopper when transitioning from PoW to PoW+TFL, falling back to pure PoW seems more feasible, since both protocols rely on mainnet PoW infrastructure, so those participants will be present in either case.
• Retaining miners during a hybrid phase: while it is true that a hybrid protocol will lower miner revenue (since we aim to maintain the issuance schedule constraints), there is also more possibility and likelihood of keeping some of these users engaged. For example, they may begin participating in staking services (either as delegators or as infrastructure operators). If that is successful, then they’re also more likely to remain engaged in the subsequent transition to pure PoS.
• This general approach was demonstrated successfully by Ethereum, which is the largest or second largest cryptocurrency network for several important metrics (e.g. market cap, fees paid, user and developer activity, …). So we know this can be done well without disruptions.

Cons

• The intermediate hybrid step will be a more novel and less well understood protocol. (It will necessarily be fairly different from Ethereum’s Beacon chain era.)
• Consensus nodes will be more complex, involving logic for both sub-protocols as well as their integration. (Ideally this complexity can be modularized so that the nodes are easier to maintain and improve.)
• This may be more complicated to explain to current and potential new users. Something like “Zcash launched as PoW, and on DATE (block height X) it will transition to a hybrid system, then later to a pure PoS system.”
• The available issuance must be shared between mining and staking rewards during the hybrid stage. The security of the PoW layer and of the PoS layer during this stage is partially dependent on the funds allocated to issuance for each protocol, and it is not yet clear to what extent splitting rewards would affect overall security.

Footnotes

Trailing Finality Layer in a Nutshell

The hybrid PoW/PoS protocol proposed in this book is similar to today's Zcash NU5 protocol with the addition of a Trailing Finality Layer:

TODO: Add network topology / software subcomponent diagram #124

The Zcash Trailing Finality Layer refers to a new subprotocol of a new hybrid PoW/PoS protocol, which we refer to as PoW+TFL. This subprotocol introduces assured finality for the Zcash blockchain, ensuring that final blocks (and the transactions within them) may never be rolled back.

We use the term "layer" because we can understand this design as introducing a new layer to the Zcash network, making only minimal changes to the existing network and consensus protocol. This modular separation is present in the consensus rules, the network protocol, and the code architecture.

Why Should Users Care?

There are three categories of users this proposed TFL protocol would impact:

Current ZEC Users

Existing ZEC users who are primarily concerned with storing or receiving ZEC, whether private or transparent may benefit from this change in the short or medium term, because it may help lower delay times for some services, such as exchange deposits. As exchanges come to rely on the new finality guarantee, they can often reduce their deposit wait times. Other services with similar confirmation-depth-based wait times can be improved in a similar way to lower these wait times. Other than this improvement, these users should notice no other changes.

In the longer term, providing finality will be useful in establishing trust-minimized bridges to other blockchains. We anticipate this can enable better connecting ZEC to the Defi ecosystem, and with the introduction of Zcash Shielded Assets, this can enable other assets to connect to the Zcash shielded pool.

Proof-of-Stake Users

Users who are interested in providing finality infrastructure, or users who want to delegate ZEC towards finality, will be able to earn rewards from the protocol for doing so, while also taking on some risk to their funds (to prevent malicious abuse of the protocol). This may be an important new category of ZEC users and use cases.

Miners

Miners who provide Proof-of-Work security will necessarily see some reduction in their block rewards, since this proposal maintains the same issuance schedule and supply cap of ZEC while also spending some rewards on finality.

Important Note: The proportion and details of how much mining rewards will be impacted, and conversely how much finality/PoS providers will earn, are not yet specified in this proposal.

Why is this a Good Approach to a PoS Transition?

This design is appealing as a safer first step in transitioning the Zcash protocol for multiple reasons:

It Enables Proof-of-Stake Mechanisms Conservatively

This transition would enable PoS mechanisms, including the ability to operate PoS infratructure and delegate ZEC towards those providers to earn protocol rewards. While all PoS transitions would accomplish this, this approach does so in a conservative manner: it introduces these mechanics while striving to minimize the impact on existing use cases and protocol security.

In a sense, we can think of this approach as enabling the Zcash community to "dip our toes in the PoS waters" rather than diving in. If the results pan out well, it gives us confidence for further transitions. If we discover challenges, flaws, or risks, we anticipate their impact will be more limited since this is a more cautious transition step.

Minimal Use-Case Disruption

In many cases, existing products, services, and tools can continue using the mainnet chain with no changes to code assuming they rely on existing consensus nodes. We view this as a major benefit which allows Zcash's existing user network effect to continue safely unperturbed.

There will be certain narrow exceptional areas if those products, services, or tools need to be precise in areas where the protocol has changed, such as mining/staking reward calculations, transaction formats (in particular any new PoS-related fields or logic), or chain rollback logic.

Modular Design

By conceptualizing the TFL as a distinct "layer" or subprotocol, the consensus rules can be described in terms of two consensus subprotocols, one embodying most of the current consensus logic of Zcash and another the TFL. These protocols interact through a hybrid construction. See Design at a Glance to learn more about these distinct subprotocols.

Reasoning about the whole protocol can leverage analysis and understanding of each subprotocol and the hybrid construction somewhat independently due to this modular design. Note that although this design is modular, the hybrid construction may require modifications to the [PoW] and/or [PoS] subprotocols to protect safety and liveness properties. Nevertheless, the modularity still improves analysis and reasoning compared to a monolithic design.

Finally, since one subprotocol is very similar to the existing Zcash NU5 protocol, this lessens risk that the consensus properties within that subprotocol compromise current NU5 properties.

Modular Implementation

In addition to the other benefits of protocol design modularity, we anticipate actual implementations can realize this modularity in code. This can help makes implementations more robust, easier to maintain, and more interoperable.

For example, we can envision a standardized interface between PoW & TFL consensus components, enabling different development teams to provide these different components and for "full node" packagers to mix and match them. This is somewhat reminiscent of Ethereum's execution/consensus layer separation which we believe has shown great success in implementation team and product diversity.

Cracking the Nutshell

In the rest of the introductory section of this book, we describe the status and next steps for the TFL proposal, provide a motivation for finality, and suggestions for getting involved.

Status and Next Steps

This is an early and incomplete protocol design proposal. It has not been well vetted for feasibility and safety. It has not had broad review from the Zcash community, so its status on any Zcash roadmap is undetermined.

Current Components

This Book

This book is intended to become both a high-level overview and introduction to TFL, and a full specification.

Crosslink

The current heart of the design work is an in-progress hybrid consensus protocol construction called Crosslink (definition). This is defined in the Crosslink chapter.

simtfl

We've begun creating a simulator called simtfl which we will use to model security and abstract performance concerns. Its development is tracked at https://github.com/zcash/simtfl.

Major Missing Components

• PoS subprotocol selection,
• Issuance and supply mechanics, such as how much ZEC stakers may earn,
• Integrated Zcash transaction semantics,
• A transition plan from current Zcash mainnet to this protocol design,
• ZIPs specifying the above to the level of specificity required by ZIPs,
• Security and safety analyses,
• Economic analyses.

This list may be incomplete, and as the design matures the need for major new components may be revealed.

Next Steps

This design proposal is being developed by Electric Coin Company as the first major milestone in our focus of deploying Proof-of-Stake to the Zcash protocol. Our rough near-term plan for this proposal is as follows:

1. Complete the Crosslink description.
2. Complete core security arguments for Crosslink.
3. Define the Major Missing Components above, including considerations such as issuance mechanics and Proof-of-Stake mechanisms.
4. Complete auxillary security arguments and analyses, such as specific attack scenarios, game-theoretic security, and so forth.
5. Mature simtfl to analyze all cases of interest.
6. Follow the general Zcash process for proposal/review/refinement, including proposing one or more ZIPs.
7. Follow the general Zcash governance process for proposal review and refinement.
8. If accepted, productionize the proposal in ECC products and collaborate with other implementors who implement the proposal.
9. Celebrate when and if the proposal is activated on Mainnet. 🎉

The fine-grained day-to-day goals and tasks for this project are present in the Zcash Developers Hub in the TFL-focused DAG.

Please also see Get Involved if you are interested in tracking this progress more closely, or in contributing.

Motivating Finality

In Zcash currently, consensus relies solely on PoW, which only provides probabilistic finality, rather than assured finality.¹ This style of consensus does not offer a guarantee that any given block may not be rolled back which may invalidate the transactions it contains. Instead, the probability that a block may be rolled back decreases as more blocks are mined subsquently on top of it.²

Let's walk through an example of how Zcash's current PoW with probabilistic finality can impede important use cases. Consider a PoW node which sees this block sequence at time T=0:

When should a user, wallet, or other system choose to act based on a transaction in a block?

For this example, let's assume a bridging system may have received a deposit for ZEC in block f and issued a corresponding number of proxy tokens on a different network.

At a later time, T=1, this same node may see a longer PoW chain which invalidates some previously seen blocks:

The node has observed a longer chain ending at block h', so PoW consensus calls for that new sequence to be treated as consensus. The previously seen blocks f and g are no longer part of the consensus history, and have been rolled back.

Impact of the Rollback

In our example, the bridging system acted in response to a transaction in the original block f at T=0. If the new sequence ending at h' no longer contains the deposit to the bridging system, the integrity of the bridge has been violated³; the associated proxy tokens may have already been used in a complex chain of Defi applications or deposited onto an exchange and sold, which would make any recovery impossible. The proxy tokens on the other network no longer correspond to the correct amount of ZEC on the Zcash network.

Rollback Complications

This example demonstrates how a lack of assured finality can impede many useful real-world scenarios. In practice, systems and services which need greater assurances wait for more block confirmations.

This has several drawbacks:

• it doesn't remove the vulnerability, it only reduces the likelihood;
• different applications/services may require different block depths, making it difficult to compose or chain together different applications/services;
• different block depth policies potentially confuse users, i.e. "why do I have to wait one hour for my deposit in this exchange, but only 30 minutes on that exchange?"; and
• it introduces a long delay which inhibits many useful applications.

In addition to these user-facing and economic drawbacks, correctly handling rollbacks makes the code for nodes, wallets, and other infrastructure more complex. Worse still, many systems may not have correct behavior for rollbacks at different depths, and since large rollbacks are rarer, these implementation flaws may not surface until there is a large rollback. While a large rollback would be disruptive all by itself, it becomes even worse when previously undiscovered bugs exacerbate the situation.

Trailing Finality Benefits

Trailing finality extends the existing PoW consensus so that older blocks become final, assuring they cannot be rolled back, and by extension neither can any of the transactions they contain.

This directly addresses the first two flaws above: it completely removes the vulnerability, and it ensures all systems that need finality behave consistently with each other.

As for delay, trailing finality also introduces delay since final blocks "trail behind" the most recent PoW blocks. This can be an improvement for some applications, depending on their latency requirements. For example, if the delay to finality averages around 10 minutes, then this would enable an improvement for an exchange that requires 60 minutes of PoW blocks for a deposit. On the other hand, it would not be an improvement for an application that needs finality faster than 10 minutes.

Finally, implementations can be simplified by relying on the guarantee of finality. For example, a wallet can describe any transaction as pending or final, and does not need to provide difficult and potentially confusing UX (and the supporting database sophistication) for handling rollbacks.

Footnotes

Get Involved

We welcome contributions!

There are a variety of ways to contribute to this project:

Github

If you have a GitHub account, you can get hands-on via the GitHub repository for this book, including:

• Ask a Question - all questions welcome from basics to in-depth.
• Suggest an Improvement to the content: anything from typo fixes to major design change proposals.
• Report Rendering / Infrastructure Issues in case you're having trouble reading the content, viewing diagrams, rendering on your own computer, etc…

Zcash Forum

The Zcash Forum is a hangout for many Zcash enthusiasts. This is a good spot for more open-ended discussion about this design proposal, alternatives, and other developments in Zcash.

Zcash R&D Discord

You can catch us on the Zcash R&D Discord in this #proof-of-stake channel.

Zcash Arborist Calls

The Zcash Arborist Calls are bi-weekly Zcash protocol development calls, where proposals like this are discussed. Feel free to come lurk, ask questions, or provide feedback or suggestions.

Terminology

This book relies on the following terminology. We strive to keep these definitions as precise as possible and their definitions may deviate from uses elsewhere.

Definitions are sorted alphabetically.

Terms

Assured Finality: A protocol property that assures that transactions cannot be reverted by that protocol. As with all protocol guarantees, a protocol assumes certain conditions must be met. A transaction may either be final or not: transactions which are not final may not become final, whereas once transactions do achieve finality they retain that property indefinitely (so long as protocol requirements are met).

Importantly, it is not feasible for any protocol to prevent reversing final transactions "out of band" from the protocol, such as if a sufficiently large and motivated group of users forks the network to include a specific new validity rule reverting transactions. In some cases this might be desirable, for example to mitigate exploitation of a security flaw. We are investigating the implications for governance and how to incorporate such situations into our security model. In any case, for this reason we eschew the term "absolute finality" sometimes used in technical discussions about consensus protocols.

Consensus Subprotocols: The PoW and PoS subprotocols in PoW+TFL or other hybrid protocols.

Crosslink: A hybrid construction consensus protocol striving to implement the TFL design goals. See Status and Next Steps: Current Components for current status.

Final: A protocol property of transactions. In this book, this always implies assured finality, in contrast to concepts like "probabilistic finality" provided by PoW.

Hybrid Consensus: A consensus protocol that integrates more than one consensus subprotocol. PoW+TFL is an instance of a hybrid protocol integrating PoW and PoS protocols.

Hybrid Construction: The design component of a hybrid consensus which specifies how to integrate subprotocols and what modifications, if any, those subprotocols need to be safely integrated. Examples include Crosslink and Snap-and-Chat.

Liveness: The property of a distributed protocol which ensures that the protocol may progress provided liveness requirements are met. TODO: Fix the definition of Liveness #120

NU5: The Zcash consensus protocol as of NU5.¹

Objective Validity: A validity property of a protocol history (such as a ledger) which can be computed purely from that history with no other context. Objective validity is needed to define consensus rules that will lead to the same protocol state being eventually agreed on by all nodes.

Proof-of-Stake: A PoS protocol achieves consensus on transaction status by taking into account the weighting of staking tokens. PoS protocols exist under a large umbrella and may or may not provide assured finality or other properties this design requires of TFL.

Proof-of-Work: A PoW protocol uses Nakamoto consensus pioneered by Bitcoin. The PoW subprotocol within PoW+TFL is a different consensus protocol from NU5 and encompasses more than narrow Nakamoto PoW consensus, including transaction semantics such as for shielded transfers.

PoW+TFL: the overall complete, integrated consensus protocol specified in this book.

Safety: The property of a distributed protocol that guarantees a participant may safely rely on a consistent local state, provided safety requirements are met. TODO: Provide a rigorous definition of Safety #121

simtfl: a protocol simulator for analyzing TFL security and abstract performance. Development lives at https://github.com/zcash/simtfl. See Status and Next Steps: Current Components for current status.

Snap-and-Chat: A hybrid construction consensus protocol introduced in Ebb-and-Flow Protocols.

TFL: The Trailing Finality Layer subprotocol within PoW+TFL. This is a new PoS subprotocol which provides assured finality for Zcash.

Trailing Finality: A protocol property wherein transactions become final some time after first appearing in PoW blocks.

ZIP: a Zcash Improvement Proposal is the protocol development process the Zcash community uses to safely define potential protocol improvements. See https://zips.z.cash.

TODO: Clarify the distinctions between pure PoW, the PoW subprotocol, NU5, and fork-choice vs all of transaction semantics. #119

Footnotes

Design

Design Overview

This design augments the existing Zcash Proof-of-Work (PoW) network with a new consensus layer which provides trailing finality, called the Trailing Finality Layer (TFL).

This layer enables blocks produced via PoW to become final which ensures they may never be rolled back. This enables safer and simpler wallets and other infrastructure, and aids trust-minimized cross-chain bridges.

This consensus layer uses a finalizing Proof-of-Stake (PoS) consensus protocol, and enables ZEC holders to earn protocol rewards for contributing to the security of the Zcash network. By integrating a PoS layer with the current PoW Zcash protocol, this design specifies a hybrid consensus protocol.

The integration of the current PoW consensus with the TFL produces a new top-level consensus protocol referred to as PoW+TFL.

In the following subchapters we introduce the Design at a Glance, then provide an overview of the major components of the design.

Following this overview chapter, we proceed into a detailed Protocol Specification (TODO).

Design at a Glance

The PoW+TFL consensus protocol is logically an extension of the Zcash consensus rules to introduce trailing finality. This is achieved by compartmentalizing the top-level PoW+TFL protocol into two consensus subprotocols, one embodying most of the current consensus logic of Zcash and another the TFL. These protocols interact through a hybrid construction, which specifies how the protocols interact, and what changes from "off-the-shelf" behavior, if any, need to be imposed on the subprotocols. Each of these components (the two subprotocols and the hybrid construction) are somewhat modular: different subprotocols or hybrid constructions may be combined (with some modification) to produce a candidate PoW+TFL protocol.

TODO: Add a protocol component diagram to "Design at a Glance" #122

Hybrid Construction

The hybrid construction is a major design component of the full consensus protocol which specifies how the subprotocols integrate. So far we have considered three candidates:

1. The implied/loosely defined hybrid construction presented at Zcon4.
2. The Snap-and-Chat from the Ebb-and-Flow paper.
3. The Crosslink construction.

Currently we believe Crosslink is the best candidate, due to security considerations.

TODO: Explain why we're more confident in Crosslink security vs the other hybrid construction candidates #123

Subprotocols

The PoW+TFL hybrid consensus consists of two interacting subprotocols:

1. PoW Subprotocol: this subprotocol is very similar to NU5 consensus. It is a design goal of the TFL design to minimize changes to this subprotocol. Note: the shorthand "PoW" is potentially misleading, because this subprotocol is also responsible for the bulk of all supply and transaction semantic consensus rules.
2. PoS Subprotocol: this is a new subprotocol which provides trailing finality via a finalizing PoS protocol.

TODO: Clarify the distinctions between pure PoW, the PoW subprotocol, NU5, and fork-choice vs all of transaction semantics. #119

Note that the hybrid construction may require modification to the "off-the-shelf" versions of these subprotocols. In particular Crosslink requires each protocol to refer to the state of the other to provide objective validity.

Design Goals

Here we strive to lay out our high level TFL design goals.

Goals, Design, and Trade-offs

Here we lay out ideal goals. As we develop a complete design, we are likely to inevitably encounter trade-offs some of which may preclude achieving the full idealized goals. Wherever possible, we motivate design decisions by these goals, and when goals are impacted by trade-offs we describe that impact and the rationale for the trade-off decision.

For example, one ideal user experience goal below is to avoid disruption to existing wallets. However, the Crosslink construction may require wallets to alter their context of valid transactions differently from the current NU5 protocol.

User Experience and Use Case Goals

We strive to start our protocol design process from user experience (UX) and use case considerations foremost, since at the end of the day all that matters in a protocol is what user needs it meets and how well.

• All currently supported wallet user experience should continue to operate seamlessly without change during or after protocol transitions. This covers the use of addresses, payment flow, transfers, ZEC supply cap and issuance rate, backup/restore, and other features users currently rely on.
• There must be no security or safety degradation due to wallet user behavior introduced by PoS transitions, assuming users follow their current behaviors unchanged and continue to use the same cognitive model of the impacts of their behaviors. This goal encompasses all of security and safety, including privacy and transparency or more explicit disclosures.
• The protocol should enable users of shielded mobile wallets to delegate ZEC to PoS consensus providers and earn a return on that ZEC coming via ZEC issuance or fees. Doing this may expose users to a risk of loss of delegated ZEC (such as through “slashing fees”). The protocol must guarantee that PoS consensus providers have no discretionary control over such delegated funds (including that they cannot steal those funds).
• For any hybrid PoW/PoS protocol (including the PoW+TFL protocol we’re proposing), the process and UX of mining remains unchanged except that the return on investment may be altered. This is true both of consensus-level block miners (i.e. mining pools and solo miners) and mining pool participants.
• Any hybrid PoW/PoS protocol (including PoW+TFL) block explorers will continue to function with the same UX through transitions as far as displaying information about transactions, the mempool, and blocks.
• Block explorers and other network metrics sites may require UX changes with respect to mining rewards and issuance calculations.
• Network metrics sites may require UX changes with respect to the p2p protocol or other network-specific information.
• Users can rely on assured finality with an expected time-to-finality of <30m.¹

Developer Experience Goals

For a full PoS transition, ecosystem developers for products such as consensus nodes, wallets, mining services, chain analytics, and more will certainly need to update their code to support transitions. However, we carve out a few goals as an exception to this for this category of users:

• Wallet developers should not be required to make any changes through protocol transitions as long as they rely solely on the lightwalletd protocol or a full node API (such as the zcashd RPC interface).
• For any hybrid PoW/PoS protocol (including PoW+TFL), mining pools and miners should not be required to make any software or protocol changes as long as they rely on zcashd-compatible GetBlockTemplate. One exception to this is software that bakes in assumptions about the block reward schedule, rather than relying on GetBlockTemplate solely.

Safety, Security, and Privacy Goals

Zcash has always had exemplary safety, security, and privacy, and we aim to continue that tradition:

• For any hybrid PoW/PoS protocol (including PoW+TFL), the cost-of-attack for a 1-hour rollback should not be reduced, given a “reasonably rigorous” security argument.
• For any hybrid PoW/PoS protocol (including PoW+TFL), the cost-of-attack to halt the chain should be larger than the 24 hour revenue of PoW mining rewards, given a “reasonably rigorous” security argument.

TODO: Define privacy goals of TFL #118

TODO: Define PoS Subprotocol desiderata which are distinct from Crosslink integration #117

Design Conservatism Goals

We want to follow some conservative design heuristics to minimize risk and mistakes:

• Rely as much as possible on design components that are already proven in production environments.
• Rely as much as possible on design components with adequate theoretical underpinnings and security analyses.
• Minimize changes or variations on the above: strive to only alter existing work when necessary for overall design goals. For example, Zcash's privacy or issuance constraints are likely less common among existing PoS designs.

Non-goals

These are not goals of the TFL design, either to simplify the scope of the initial design (a.k.a. Out-of-Scope Goals), or because we believe some potential goal should not be supported (a.k.a. Anti-goals).

Out-of-Scope Goals

While these desiderata may be common across the blockchain consensus design space, they are not specific goals for the initial TFL design. Note that these may be goals for future protocol improvements.

• Prioritizing minimal time-to-finality over other considerations (such as protocol simplicity, impact on existing use cases, or other goals above).

• In-protocol liquid staking derivatives.

• Maximizing the PoS staked-voter count ceiling. For example, Tendermint BFT has a relatively low ceiling of ~hundreds of staked voters, whereas Ethereum's Gasper supports hundreds of thousands of staked voters.

• Reducing energy usage. While this would presumably be a goal of a pure PoS transition, it likely cannot be achieved for hybrid PoW/PoS without loss of security.

Anti-Goals

Distinctly from Out-of-Scope Goals we track "anti-goals" which are potential goals that we explicitly reject, which are potential goals we aim to not support even in future protocol improvements.

We currently have no defined anti-goals.

Footnotes

Crosslink

Crosslink is the proposed hybrid construction for the Trailing Finality Layer.

Contents

• The Arguments for Bounded Dynamic Availability and Finality Overrides
• Notes On Snap And Chat
• The Crosslink Construction
• Security Analysis of Crosslink
• Questions About Crosslink
• Potential Changes to Crosslink

The Arguments for Bounded Dynamic Availability and Finality Overrides

This document considers disadvantages of allowing transactions to continue to be included at the chain tip while the gap from the last finalized block becomes unbounded, and what I think should be done instead. This condition is allowed by Ebb‑and‑Flow protocols [NTT2020].

I also argue that it is necessary to allow for the possibility of overriding finalization in order to respond to certain attacks, and that this should be explicitly modelled and subject to a well-defined governance process.

This is a rewritten version of this forum post, adapting the main argument to take into account the discussion of “tail-thrashing attacks” and finalization availability from the Addendum. More details of how bounded dynamic availability could be implemented in the context of a Snap‑and‑Chat protocol are in Notes on Snap‑and‑Chat.

The proposed changes end up being significant enough to give our construction a new name: “Crosslink”, referring to the cross-links between blocks of the BFT and best-chain protocols. Crosslink has evolved somewhat, and now includes other changes not covered in either this document or Notes on Snap‑and‑Chat.

Background

“Ebb‑and‑Flow”, as described in [NTT2020] (arXiv version), is a security model for consensus protocols that provide two transaction logs, one with dynamic availability, and a prefix of it with finality.

The paper proposes an instantiation of this security model called a “Snap‑and‑Chat” construction. It composes two consensus subprotocols, a BFT subprotocol and a best-chain subprotocol (it calls this the “longest chain protocol”). The above logs are obtained from the output of these subprotocols in a non-trivial way.

This is claimed by the paper to “resolve” the tension between finality and dynamic availability. However, a necessary consequence is that in a situation where the “final” log stalls and the “available” log does not, the “finalization gap” between the finalization point and the chain tip can grow without bound. In particular, this means that transactions that spend funds can remain unfinalized for an arbitrary length of time.

In this note, we argue that this is unacceptable, and that it is preferable to sacrifice strict dynamic availability. However, we also argue that the main idea behind Ebb‑and‑Flow protocols is a good one, and that allowing the chain tip to run ahead of the finalization point does make sense and has practical advantages. However, we also argue that it should not be possible to include transactions that spend funds in blocks that are too far ahead of the finalization point.

We argue that losing strict dynamic availability in favour of “bounded dynamic availability” is preferable to the consequences of the unbounded finality gap, if/when a “long finalization stall” occurs.

We also argue that it is beneficial to explicitly allow “finality overrides” under the control of a well-documented governance process. Such overrides allow long rollbacks that may be necessary in the case of an exploited security flaw. This is complementary to the argument for bounded dynamic availability, because the latter limits the period of user transactions that could be affected. The governance process can impose a limit on the length of this long rollback if desired.

Finality + Dynamic availability implies an unbounded finalization gap

Since partition between nodes sufficient for finalization cannot be prevented, loosely speaking the CAP theorem implies that any consistent protocol (and therefore any protocol with finality) may stall for at least as long as the partition takes to heal.

Dynamic availability implies that the chain tip will continue to advance, and so the finalization gap increases without bound.

Partition is not necessarily the only condition that could cause a finalization stall, it is just the one that most easily proves that this conclusion is impossible to avoid.

Problems with allowing spends in an unbounded finalization gap

Both the available protocol, and the subprotocol that provides finality, will be used in practice — otherwise, one or both of them might as well not exist. There is always a risk that blocks may be rolled back to the finalization point, by definition.

Suppose, then, that there is a long finalization stall. The final and available protocols are not separate: there is no duplication of tokens between protocols, but the rules about how to determine best-effort balance and guaranteed balance depend on both protocols, how they are composed, and how the history after the finalization point is interpreted.

As the finalization gap increases, the negative consequences of rolling back user transactions that spend funds increase. (Coinbase transactions do not spend funds; they are a special case that we will discuss later.)

There are several possible —not mutually exclusive— outcomes:

• Users of the currency start to consider the available protocol increasingly unreliable.
• Users start to consider a rollback to be untenable, and lobby to prevent it or cry foul if it occurs.
• Users start to consider finalization increasingly irrelevant. Services that depend on finality become unavailable.
  • There is no free lunch that would allow us to avoid availability problems for services that also depend on finality.
• Service providers adopt temporary workarounds that may not have had adequate security analysis.

Any of these might precipitate a crisis of confidence, and there are reasons to think this effect might be worse than if the chain had switched to a “Safety Mode” designed to prevent loss of user funds. Any such crisis may have a negative effect on token prices and long-term adoption.

Note that adding finalization using an Ebb‑and‑Flow protocol does not by itself increase the probability of a rollback in the available chain, provided the PoW remains as secure against rollbacks of a given length as before. But that is a big proviso. We have a design constraint (motivated by limiting token devaluation and by governance issues) to limit issuance to be no greater than that of the original Zcash protocol up to a given height. Since some of the issuance is likely needed to reward staking, the amount of money available for mining rewards is reduced, which may reduce overall hash rate and security of the PoW. Independently, there may be a temptation for design decisions to rely on finality in a way that reduces security of PoW (“risk compensation”). There is also pressure to reduce the energy usage of PoW, which necessarily reduces the global hash rate, and therefore the cost of performing an attack that depends on the adversary having any given proportion of global hash rate.

It could be argued that the issue of availability of services that depend on finality is mainly one of avoiding over-claiming about what is possible. Nevertheless I think there are also real usability issues if balances as seen by those services can differ significantly and for long periods from balances at the chain tip.

Regardless, incorrect assumptions about the extent to which the finalized and available states can differ are likely to be exposed if there is a finalization stall. And those who made the assumptions may (quite reasonably!) not accept “everything is fine, those assumptions were always wrong” as a satisfactory response.

What is Bounded Dynamic Availability?

An intuitive notion of “availability” for blockchain protocols includes the ability to use the protocol as normal to spend funds. So, just to be clear, in a situation where that cannot happen we have lost availability, even if the block chain is advancing.

Bounded dynamic availability is a weakening of dynamic availability. It means that we intentionally sacrifice availability when some potentially hazardous operation —a “hazard” for short— would occur too far after the current finalization point. For now, assume for simplicity that our only hazard is spending funds. More generally, the notion of bounded dynamic availability can be applied to a wider range of protocols by tailoring the definition of “hazard” to the protocol.

Terminology note

[NTT2020] calls the dynamically available blockchain protocol ${\Pi }_{\mathrm{lc}}$ that provides input to the rest of the contruction, the “longest chain” protocol. There are two reasons to avoid this terminology:

• In Bitcoin, Zcash, and most other PoW-based protocols, what is actually used by each node is not its longest observed chain, but its observed consensus-valid chain with most accumulated work. In Zcash this is called the node’s “best valid block chain”, which we shorten to “best chain”.
• As footnote 2 on page 3 of [NTT2020] says, that paper does not require ${\Pi }_{\mathrm{lc}}$ to be a “longest chain” protocol anyway.

We will use the term “best-chain protocol” instead. Note that this means ${\Pi }_{\mathrm{lc}}$ in the Snap‑and‑Chat construction, not any node’s view of the sanitized ledger ${\mathsf{LOG}}_{\mathrm{da}}$.

How to block hazards

We have not yet decided how to block hazards during a long finalization stall. We could do so directly, or by stopping block production in the more-available protocol. For reasons explained in the section on “Tail-thrashing attacks” below, it’s desirable not to stop block production. And so it’s consistent to have bounded dynamic availability together with another liveness property —which can be defined similarly to dynamic availability— that says the more-available protocol’s chain is still advancing. This is what we will aim for.

We will call this method of blocking hazards, without stopping block production, “going into Safety Mode”.

For Zcash, I propose that the main restriction of Safety Mode should be to require coinbase-only blocks. This achieves a similar effect, for our purposes, as actually stalling the more-available protocol’s chain. Since funds cannot be spent in coinbase-only blocks, the vast majority of attacks that we are worried about would not be exploitable in this state.

A analogy for the effect of this on availability that may be familiar to many people, is that it works like video streaming. All video streaming services use a buffer to paper over short-term interruptions or slow-downs of network access. In most cases, this buffer is bounded. This allows the video to be watched uninterrupted and at a constant rate in most circumstances. But if there is a longer-term network failure or insufficient sustained bandwidth, the playback will unavoidably stall. In our case, block production does not literally stall, but it’s the same as far as users’ ability to perform “hazardous” operations is concerned.

Why is this better?

So, why do I advocate this over:

1. A protocol that only provides dynamic availability;
2. A protocol that only provides finality;
3. An unmodified Ebb‑and‑Flow protocol?

The reason to reject option 1 is straightforward: finality is a valuable security property that is necessary for some use cases.

If a protocol only provides finality (option 2), then short-term availability is directly tied to finalization. It may be possible to make finalization stalls sufficiently rare or short-lived that this is tolerable. But that is more likely to be possible if and when there is a well-established staking ecosystem. Before that ecosystem is established, the protocol may be particularly vulnerable to stalls. Furthermore, it’s difficult to get to such a protocol from a pure PoW system like current Zcash.

We argued in the previous section that allowing hazards in an unbounded finalization gap is bad. Option 3 entails an unbounded finalization gap that will allow hazards. However, that isn’t sufficient to argue that bounded dynamic availability is better. Perhaps there are no good solutions! What are we gaining from a bounded dynamic availability approach that would justify the complexity of a hybrid protocol without obtaining strict dynamic availability?

My argument goes like this:

• It is likely that a high proportion of the situations in which a sustained finalization stall happens will require human intervention. If the finality protocol were going to recover without intervention, there is no reason to think that it wouldn’t do so in a relatively short time.
• When human intervention is required, the fact that the chain tip is still proceeding apace (in protocols with strict dynamic availability) makes restarting the finality protocol harder, for many potential causes of a finalization stall. This may be less difficult when only “non-hazardous” transactions are present— in particular, when only coinbase transactions (which are subject to fairly strict rules in Zcash and other Bitcoin-derived chains) are present. This argument carries even more force when the protocol also allows “finality overrides”, as discussed later in the Complementarity section.
• Nothing about bounded dynamic availability prevents us from working hard to design a system that makes finalization stalls as infrequent and short-lived as possible, just as we would for any other option that provides finality.
• We want to optimistically minimize the finalization gap under good conditions, because this improves the usability of services that depend on finality. This argues against protocols that try to maintain a fixed gap, and motivates letting the gap vary.
• In practice, the likelihood of short finalization stalls is high enough that heuristically retaining availability in those situations is useful.

The argument that it is difficult to completely prevent finalization stalls is supported by experience on Ethereum in May 2023, when there were two stalls within 24 hours, one for about 25 minutes and one for about 64 minutes. This experience is consistent with my arguments:

• Neither stall required short-term human intervention, and the network did in fact recover from them quickly.
• The stalls were caused by a resource exhaustion problem in the Prysm consensus client when handling attestations. It’s plausible to think that if this bug had been more serious, or possibly if Prysm clients had made up more of the network, then it would have required a hotfix release (and/or a significant proportion of nodes switching to another client) in order to resolve the stall. So this lines up with my hypothesis that longer stalls are likely to require manual intervention.
• A bounded dynamic availability protocol would very likely have resulted in either a shorter or no interruption in availability. If, say, the availability bound were set to be roughly an hour, then the first finalization stall would have been “papered over” and the second would have resulted in only a short loss of availability.

Retaining short-term availability does not result in a risk compensation hazard:

• A finalization stall is still very visible, and directly affects applications relying on finality.
• Precisely because of the availability bound, it is obvious that it could affect all applications if it lasted long enough.

A potential philosophical objection to lack of strict dynamic availability is that it creates a centralization risk to availability. That is, it becomes more likely that a coalition of validators can deliberately cause a denial of service. I think this objection may be more prevalent among people who would object to adding a finality layer or PoS at all.

Finality Overrides

Consensus protocols sometimes fail. Potential causes of failure include:

• A design problem with the finality layer that causes a stall, or allows a stall to be provoked.
• A balance violation or spend authorization flaw that is being exploited or is sufficiently likely to be exploited.
• An implementation bug in a widely used node implementation that causes many nodes to diverge from consensus.

In these situations, overriding finality may be better than any other alternative.

An example is a balance violation flaw due to a 64-bit integer overflow that was exploited on Bitcoin mainnet on 15th August 2010. The response was to roll back the chain to before the exploitation, which is widely considered to have been the right decision. The time between the exploit (at block height 74638) and the forked chain overtaking the exploited chain (at block height 74691) was 53 blocks, or around 9 hours.

Of course, Bitcoin used and still uses a pure PoW consensus. But the applicability of the example does not depend on that: the flaw was independent of the consensus mechanism.

Another example of a situation that prompted this kind of override was the DAO recursion exploit on the Ethereum main chain in June 2016. The response to this was the forced balance adjustment hard fork on 20th July 2016 commonly known as the DAO fork. Although this adjustment was not implemented as a rollback, and although Ethereum was using PoW at the time and did not make any formal finality guarantees, it did override transfers that would heuristically have been considered final at the fork height. Again, this flaw was independent of the consensus mechanism.

The DAO fork was of course much more controversial than the Bitcoin fork, and a substantial minority of mining nodes split off to form Ethereum Classic. In any case, the point of this example is that it’s always possible to override finality in response to an exceptional situation, and that a chain’s community may decide to do so. The fact that Ethereum 2.0 now does claim a finality guarantee, would not in practice prevent a similar response in future that would override that guarantee.

The question then is whether the procedure to override finality should be formalised or ad hoc. I argue that it should be formalised, including specifying the governance process to be used.

This makes security analysis — of the consensus protocol per se, of the governance process, and of their interaction — much more feasible. Arguably a complete security analysis is not possible at all without it.

It also front-loads arguing about what procedure should be followed, and so it is more likely that stakeholders will agree to follow the process in any time-critical incident.

A way of modelling overrides that is insufficient

There is another possible way to model a protocol that claims finality but can be overridden in practice. We could say that the protocol after the override is a brand new protocol and chain (inheriting balances from the previous one, possibly modulo adjustments such as those that happened in the DAO fork).

Although that would allow saying that the finality property has technically not been violated, it does not match how users think about an override situation. They are more likely to think of it as a protocol with finality that can be violated in exceptional cases — and they would reasonably want to know what those cases are and how they will be handled. It also does nothing to help with security analysis of such cases.

Complementarity

Finality overrides and bounded dynamic availability are complementary in the following way: if a problem is urgent enough, then validators can be asked to stop validating. For genuinely harmful problems, it is likely to be in the interests of enough validators to stop that this causes a finalization stall. If this lasts longer than the availability bound then the protocol will go into Safety Mode, giving time for the defined governance process to occur and decide what to do. And because the unfinalized consensus chain will contain only a limited period of user transactions that spend funds, the option of a long rollback remains realistically open.

If, on the other hand, there is time pressure to make a governance decision about a rollback in order to reduce its length, that may result in a less well-considered decision.

A possible objection is that there might be a coalition of validators who ignore the request to stop (possibly including the attacker or validators that an attacker can bribe), in which case the finalization stall would not happen. But that just means that we don’t gain the advantage of more time to make a governance decision; it isn’t actively a disadvantage relative to alternative designs. This outcome can also be thought of as a feature rather than a bug: going into Safety Mode should be a last resort, and if the argument given for the request to stop failed to convince a sufficient number of validators that it was reason enough to do so, then perhaps it wasn’t a good enough reason.

It is also possible to make the argument that the threshold of stake needed is imposed by technical properties of the finality protocol and by the resources of the attacker, which might not be ideal for the purpose described above. However, I would argue that it does not need to be ideal, and will be in the right ballpark in practice.

There’s a caveat related to doing intentional rollbacks when using the Safety Mode approach, where block production in the more-available protocol continues during a long finalization stall. What happens to incentives of block producers (miners in the case of Proof-of-Work), given that they know the consensus chain might be intentionally rolled back? They might reasonably conclude that it is less valuable to produce those blocks, leading to a reduction of hash rate or other violations of the security assumptions of ${\Pi }_{\mathrm{lc}}$.

This is actually fairly easy to solve. We have the governance procedures say that if we do an intentional rollback, the coinbase-only mining rewards will be preserved. I.e. we produce a block or blocks that include those rewards paid to the same addresses (adjusting the consensus to allow them to be created from thin air if necessary), have everyone check it thoroughly, and require the chain to restart from that block. So as long as block producers believe that this governance procedure will be followed and that the chain will eventually recover at a reasonable coin price, they will still have incentive to produce on ${\Pi }_{\mathrm{lc}}$, at least for a time.

Tail-thrashing attacks

Earlier we said that there were two possible approaches to preventing hazards during a long finalization stall:

a) go into a Safety Mode that directly disallows hazardous transactions (for example, by requiring ${\Pi }_{\mathrm{lc}}$ blocks to be coinbase-only in Zcash);

b) temporarily cause the more-available chain to stall.

This section describes an important class of potential attacks on approach b) that are difficult to resolve. They are based on the fact that when the unfinalized chain stalls, an adversary has more time to find blocks, and this might violate security assumptions of the more-available protocol. For instance, if the more-available protocol is PoW-based, then its security in the steady state is predicated on the fact that an adversary with a given proportion of hash power has only a limited time to use that power, before the rest of the network finds another block.

During a chain stall, the adversary no longer has a limited time to construct a forking chain. If, say, the adversary has 10% hash power, then it can on average find a block in 10 block times. And so in 100 block times it can create a 10-block fork.

It may in fact be worse than this: once miners know that a finalization stall is happening, their incentive to continue mining is reduced, since they know that there is a greater chance that their blocks might be rolled back. So we would expect the global hash rate to fall —even before the finality gap bound is hit— and then the adversary would have a greater proportion of hash rate.

The problem is that the more-available chain does not necessarily just halt during a chain stall. In fact, for a finality gap bound of $k$ blocks, an adversary could cause the $k$-block “tail” of the chain as seen by any given node to “thrash” between different chains. I will call this a tail-thrashing attack.

If a protocol allowed such attacks then it would be a regression relative to the security we would normally expect from an otherwise similar PoW-based protocol. It only occurs during a finalization stall, but note that we cannot exclude the possibility of an adversary being able to provoke a finalization stall.

Note that in the Snap‑and‑Chat construction, snapshots of ${\Pi }_{\mathrm{lc}}$ are used as input to the BFT protocol. That implies that the tail-thrashing problem could also affect the input to that protocol, which would be bad (not least for security analysis of availability, which seems somewhat intractable in that case).

Also, when restarting ${\Pi }_{\mathrm{lc}}$, we would need to take account of the fact that the adversary has had an arbitrary length of time to build long chains from every block that we could potentially restart from. It could be possible to invalidate those chains by requiring blocks after the restart to be dependent on fresh randomness, but that sounds quite tricky (especially given that we want to restart without manual intervention if possible), and there may be other attacks we haven’t thought of. This motivates using approach a) instead.

Note that we have still glossed over precisely how consensus rules would change to enforce a). I recommend reading Notes on Snap‑and‑Chat next, followed by The Crosslink Construction.

Notes on Snap‑and‑Chat

The discussion in The Argument for Bounded Dynamic Availability and Finality Overrides is at an abstract level, applying to any Ebb‑and‑Flow-like protocol.

This document considers specifics of the Snap‑and‑Chat construction proposed in [NTT2020] (arXiv version).

Effect on consensus

A general problem with the Snap‑and‑Chat construction is that it does not follow, from enforcement of the original consensus rules on blocks produced in ${\Pi }_{\mathrm{lc}}$, that the properties they are intended to enforce hold for the ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ or ${\mathsf{LOG}}_{\mathrm{da},i}^t$ ledgers. Less obviously, the converse also does not follow: enforcing unmodified consensus rules on ${\Pi }_{\mathrm{lc}}$ blocks is both too lax and too strict.

Recall from the paper how ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and ${\mathsf{LOG}}_{\mathrm{da},i}^t$ are constructed (starting at the end of page 8 of [NTT2020]):

3. Ledger extraction: Finally, how honest nodes compute ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and ${\mathsf{LOG}}_{\mathrm{da},i}^t$ from ${\mathsf{Ch}}_i^t$ and ${\mathsf{ch}}_i^t$ is illustrated in Figure 6. Recall that ${\mathsf{Ch}}_i^t$ is an ordering of snapshots, i.e., a chain of chains of LC blocks. First, ${\mathsf{Ch}}_i^t$ is flattened, i.e. the chains of blocks are concatenated as ordered to arrive at a single sequence of LC blocks. Then, all but the first occurrence of each block are removed (sanitized) to arrive at the finalized ledger ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ of LC blocks. To form the available ledger ${\mathsf{LOG}}_{\mathrm{da},i}^t$, ${\mathsf{ch}}_i^t$, which is a sequence of LC blocks, is appended to ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and the result again sanitized.

This says that ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and ${\mathsf{LOG}}_{\mathrm{da},i}^t$ are sequences of transactions, not sequences of blocks. Therefore, consensus rules defined at the block level are not applicable.

Since ${\mathsf{LOG}}_{\mathrm{da},i}^t$ does not have blocks, it is not well-defined whether it has "coinbase-only blocks" when in Safety Mode. That by itself is not so much of a problem because it would be sufficient for it to have only coinbase transactions in that mode.

Effect on issuance

The issuance schedule of Zcash was designed under the assumption that blocks only come from a single chain, and that the difficulty adjustment algorithm keeps the rate of block mining roughly constant over time.

For Snap‑and‑Chat, if there is a rollback longer than $\sigma$ blocks in ${\Pi }_{\mathrm{lc}}$, additional coinbase transactions from the rolled-back chain will be included in ${\mathsf{LOG}}_{\mathrm{fin}}$.

We can argue that this will happen rarely enough not to cause any significant problem for the overall issuance schedule. However, it does mean that issuance is less predictable, because the block subsidies will be computed according to their depth in the ${\Pi }_{\mathrm{lc}}$ chain on which they were mined. So it will no longer be the case that coinbase transactions issue a deterministic, non-increasing sequence of block subsidies.

Effect on transaction ordering

The order of transactions in any particular ${\mathsf{ch}}_i^t$ is not in general preserved in either ${\mathsf{LOG}}_{\mathrm{fin}}$ or ${\mathsf{LOG}}_{\mathrm{da}}$. This is considered in the paper (middle of the left column on page 10) but it is very easy to miss it:

Thus, snapshots taken by different nodes or at different times can conflict. However, ${\Pi }_{\mathrm{bft}}$ is still safe and thus orders these snapshots linearly. Any transactions invalidated by conflicts are sanitized during ledger extraction.

That is, a transaction from one snapshot might double-spend an output already spent in a different transaction of a different snaphot earlier in the flattening order. If it is omitted, then later transactions could depend on the outputs of the omitted one. The paper is saying that each transaction is only included if (in Bitcoin and Zcash terminology) it satisfies contextual checks for double-spending and existence of inputs at the point in the ledger where it would be added.

Since nullifiers for shielded spends are public, it is possible to do this even for shielded transactions. Each node $i$ will construct commitment trees in the order given by ${\mathsf{LOG}}_{\mathrm{da},i}^t.$

Subtlety in the definition of sanitization

There are two possible ways to interpret how ${\mathsf{LOG}}_{\{\mathrm{fin},\mathrm{da}\}}$ are constructed in Snap‑and‑Chat:

1. Concatenate the transactions from each final BFT block snapshot of an LC chain, and sanitize the resulting transaction sequence by including each transaction iff it is contextually valid.
2. Concatenate the blocks from each final BFT block snapshot of an LC chain, remove duplicate blocks, and only then sanitize the resulting transaction sequence by including each transaction iff it is contextually valid.

These are equivalent, but the argument for their equivalence is not obvious. We definitely want them to be equivalent: 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$.

The only reasons for a transaction to be contextually invalid are double-spends and missing inputs. The argument for equivalence is:

• 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. A child cannot be reinstated until its parents have been reinstated. Therefore, no transactions are reinstated.

Note that any other reason for transactions to be contextually invalid might interfere with this argument. Therefore, strictly speaking Snap‑and‑Chat should require of ${\Pi }_{\mathrm{lc}}$ that there is no such other reason. I cannot see this explicitly stated anywhere in [NTT2020].

Spending finalized outputs

Transactions in ${\mathsf{ch}}_i^t$ need to be able to spend outputs that are not necessarily from any previous transaction in ${\mathsf{ch}}_i^t$. This is because, from the point of view of a user of node $i$ at time $t$, the block chain includes all transactions in ${\mathsf{LOG}}_{\mathrm{da},i}^t$. All of the transactions after the finalization point are guaranteed to also be in ${\mathsf{ch}}_i^t$, but the ones before the finalization point (i.e. in ${\mathsf{LOG}}_{\mathrm{fin},i}^t$) are not, because they could be from some other ${\mathsf{ch}}_j^u$ for $u\le t$ and $j\ne i$ (intuitively, from some long chain fork that was once considered confirmed by enough nodes).

A user must be able to spend outputs for which they hold the spending key from any finalized transaction, otherwise there would be no point to the finalization.

I think the authors of [NTT2020] probably just missed this: the paper only has evidence that they simulated their construction, rather than implementing it for Bitcoin or any other concrete block chain as ${\Pi }_{\mathrm{lc}}$. Let's try to repair it.

Suppose that node $j$ is trying to determine whether ${\mathsf{ch}}_i^t$ is a consensus-valid chain, which is necessary for deterministic consensus in ${\Pi }_{\mathrm{lc}}$. It cannot decide whether to allow transactions in ${\mathsf{ch}}_i^t$ to spend outputs not in the history of ${\mathsf{ch}}_i^t$ on the basis of its own finalized view ${\mathsf{LOG}}_{\mathrm{fin},j}^t,$ because ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and ${\mathsf{LOG}}_{\mathrm{fin},j}^t$ are not in general the same.

Of course, we hope that ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ and ${\mathsf{LOG}}_{\mathrm{fin},j}^t$ are consistent, i.e. one is a prefix of the other. But even if they are consistent, they are not necessarily the same length. In particular, if ${\mathsf{LOG}}_{\mathrm{fin},j}^t$ is shorter than ${\mathsf{LOG}}_{\mathrm{fin},i}^t,$ then node $j$ does not have enough information to fill in the gap — and so it may incorrectly view a transaction in ${\mathsf{ch}}_i^t$ as spending an output that does not exist, when actually it does exist in ${\mathsf{LOG}}_{\mathrm{fin},i}^t\setminus {\mathsf{LOG}}_{\mathrm{fin},j}^t.$ Conversely if ${\mathsf{LOG}}_{\mathrm{fin},j}^t$ were longer and node $j$ were to allow spending an output in ${\mathsf{LOG}}_{\mathrm{fin},j}^t\setminus {\mathsf{LOG}}_{\mathrm{fin},i}^t,$ that would be using information that is not necessarily available to other nodes, and so node $j$ could diverge from consensus.

Consensus validity of the block at the tip of ${\mathsf{ch}}_i^t$ can only be a deterministic function of the block itself and its ancestors in ${\mathsf{ch}}_i^t$. It is crucial to be able to eventually spend outputs from the finalized chain. We are forced to conclude that the chain ${\mathsf{ch}}_i^t$ must include the information needed to calculate ${\mathsf{LOG}}_{\mathrm{fin},i}^{t^{\prime }}$ for some $t^{\prime }$ not too far behind $t$. That is, ${\Pi }_{\mathrm{lc}}$ must be modified to ensure that this is the case. This leads us to strengthen the required properties of an Ebb‑and‑Flow protocol to include another property, "finalization availability".

Finalization Availability

In the absence of security flaws and under the security assumptions required by the finality layer, the finalization point will not be seen by any honest node to roll back. However, that does not imply that all nodes will see the same finalized height — which is impossible given network delays and unreliable messaging.

Both in order to optimize the availability of applications that require finality, and in order to solve the technical issue of spending finalized outputs described in the previous section, we need to consider availability of the information needed to finalize the chain up to a particular point.

Note that in Bitcoin-like consensus protocols, we don't generally consider it to be an availability flaw that a block header only commits to the previous block hash and to the Merkle tree of transactions in the block, rather than including them directly. These commitments allow nodes to check that they have the correct information, which can then be requested separately.

Suppose, then, that each block header in ${\Pi }_{\mathrm{lc}}$ commits to the latest final BFT block known by the ${\Pi }_{\mathrm{lc}}$ block producer. For a block header $H$, we will refer to this commitment as $\text{final-bft}(H)$.

This rule does not prevent the BFT chain from rolling back, if the security assumptions of ${\Pi }_{\mathrm{bft}}$ were violated. However, it means that if a node $i$ does not observe a rollback in ${\Pi }_{\mathrm{lc}}$ at confirmation depth $\sigma$, then it will also not observe any instability in ${\mathsf{LOG}}_{\mathrm{fin},i}$, even if the security assumptions of ${\Pi }_{\mathrm{bft}}$ are violated. This property holds by construction, and in fact regardless of ${\Pi }_{\mathrm{bft}}$.

Now suppose that, in a Snap‑and‑Chat protocol, the BFT consensus finalizes a ${\Pi }_{\mathrm{lc}}$ snapshot that does not extend the snapshot in the previous block (which can happen if either ${\Pi }_{\mathrm{bft}}$ is unsafe, or ${\Pi }_{\mathrm{lc}}$ suffers a rollback longer than $\sigma$ blocks). In that case we will initially not be able to spend outputs from the old snapshot in the new chain. But eventually for some node $i$ that sees the header $H$ at the tip of its best chain at time $t$, $\text{final-bft}(H)$ will be such that from then on (i.e. at time $t^{\prime }\ge t$), ${\mathsf{LOG}}_{\mathrm{fin},i}^{t^{\prime }}$ includes the output that we want to spend. This assumes liveness of ${\Pi }_{\mathrm{lc}}$ and safety of ${\Pi }_{\mathrm{bft}}$.

That is, including a reference to a recent final BFT block in ${\Pi }_{\mathrm{lc}}$ block headers both incentivizes nodes to propagate this information, and can be used to solve the "spending finalized outputs" problem.

Optionally, we could incentivize the block producer to include the latest information it has, for example by burning part of the block reward or by giving the producer some limited mining advantage that depends on how many ${\Pi }_{\mathrm{lc}}$ blocks back the finalization information is.

This raises the question of how we measure how far ahead a given block is relative to the finalization information it provides. As we said before, ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ is a sequence of transactions, not blocks. The transactions will in general be in a different order, and also some transactions from ${\mathsf{ch}}_i^t$ may have been omitted from ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ (and even ${\mathsf{LOG}}_{\mathrm{da},i}^t$) because they were not contextually valid.

It turns out there is a good way to measure this. Assume that a block unambiguously specifies its ancestor chain. For a block $H$, define:$$\begin{gathered} \mathsf{tailhead}(H):=\text{last-common-ancestor}(\mathsf{snapshot}(\text{final-bft}(H)),H) \\ \text{finality-depth}(H):=\mathsf{height}(H)-\mathsf{height}(\mathsf{tailhead}(H)) \end{gathered}$$

Here $\text{final-bft}(H)$ is the BFT block we are providing information for, and $\mathsf{snapshot}(\text{final-bft}(H))$ is the corresponding ${\Pi }_{\mathrm{lc}}$ snapshot. For a node $i$ that sees $\text{final-bft}(H)$ as the most recent final BFT block at time $t$, ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ will definitely contain transactions from blocks up to $\mathsf{tailhead}(H)$, but usually will not contain subsequent transactions on $H$'s fork.

We could alternatively just rely on the fact that some proportion of block producers are honest and will include the latest information they have. However, it turns out that having a definition of finality depth will also be useful to enforce going into Safety Mode.

Specifically, if we accept the above definition of finality depth, then the security property we want is

Note that a node that is validating a chain ${\mathsf{ch}}_i^t$ must fetch all the chains referenced by BFT blocks reachable from it (back to an ancestor that it has seen before). In theory, there could be a partition that causes there to be multiple disjoint snapshots that get added to the BFT chain in quick succession. However, in practice we expect such long rollbacks to be rare if ${\Pi }_{\mathrm{lc}}$ is meeting its security goals.

Going into Safety Mode if there is a long finalization stall helps to reduce the cost of validation when the stall resolves. That is, if there is a partition and nodes build on several long chains, then in unmodified Snap‑and‑Chat, it could be necessary to validate an arbitrary number of transactions on each chain when the stall resolves. Having only coinbase transactions after a certain point in each chain would significantly reduce the concrete validation costs in this situation.

Nodes should not simply trust that the BFT blocks are correct; they should check validator signatures (or aggregate signatures) and finalization rules. Similarly, ${\Pi }_{\mathrm{lc}}$ snapshots should not be trusted just because they are referenced by BFT blocks; they should be fully validated, including the proofs-of-work.

It is also possible for a snapshot reference to include the subsequent $\sigma$ block headers, which are guaranteed to be available for a confirmed snapshot. Having all nodes validate the proofs-of-work in these headers is likely to significantly increase the work that an attacker would need to perform to cause disruption under a partial failure of either ${\Pi }_{\mathrm{bft}}$ or ${\Pi }_{\mathrm{lc}}$'s security properties.

Enforcing Finalization Availability and Safety Mode

The following idea for enforcing finalization availability and a bound on the finality gap was originally conceived before I had switched to advocating the Safety Mode approach. It's simpler to explain first in that variant; bear with me.

Suppose that for a $L$-block availability bound, we required each block header to include the information necessary for a node to finalize to $L$ blocks back. This would automatically enforce a chain stall after the availability bound without any further explicit check, because it would be impossible to produce a block after the bound.

Note that if full nodes have access to the BFT chain, knowing $\text{final-bft}(H)$ is sufficient to tell whether the correct version of any given BFT block in $\text{final-bft}(H)$'s ancestor chain has been obtained.

Suppose that the finality gap bound is $L$ blocks. Having already defined $\text{finality-depth}$, the necessary ${\Pi }_{\mathrm{lc}}$ consensus rule is attractively simple:

To adapt this approach to enforce Safety Mode instead of stalling the chain, we can allow the alternative of producing a block that follows the Safety Mode restrictions:

Note that Safety Mode will be exited automatically as soon as the finalization point catches up to within $L$ blocks (if it does without an intentional rollback). Typically, after recovery from whatever was causing the finalization stall, the validators will be able to obtain consensus on the same chain as ${\mathsf{LOG}}_{\mathrm{da}}$, and so there will be no rollback (or at least not a long one) of ${\mathsf{LOG}}_{\mathrm{da}}$.

Comment on security assumptions

Consider Lemma 5:

Moreover, for a BFT block to become final in the view of an honest node $i$ under $({\mathcal{A}}_2^{\ast },{\mathcal{Z}}_2)$, at least one vote from an honest node is required, and honest nodes only vote for a BFT block if they view the referenced LC block as confirmed.

The stated assumptions are:

$({\mathcal{A}}_2(\beta ),{\mathcal{Z}}_2)$ formalizes the model of P2, a synchronous network under dynamic participation, with respect to a bound $\beta$ on the fraction of awake nodes that are adversarial:

• At all times, ${\mathcal{A}}_2$ is required to deliver all messages sent between honest nodes in at most $\Delta$ slots.
• At all times, ${\mathcal{A}}_2$ determines which honest nodes are awake/asleep and when, subject to the constraint that at all times at most fraction $\beta$ of awake nodes are adversarial and at least one honest node is awake.

$({\mathcal{A}}_2^{\ast },{\mathcal{Z}}_2)$ is defined as $({\mathcal{A}}_2(\frac{1}{2},{\mathcal{Z}}_2))$.

Now consider this statement and figure:

Even if ${\Pi }_{\mathrm{bft}}$ is unsafe (Figure 9c), finalization of a snapshot requires at least one honest vote, and thus only valid snapshots become finalized.

This argument is technically correct but has to be interpreted with care. It only applies when the number of malicious nodes $f$ is such that $n/3<f<n/2$. What we are trying to do with Crosslink is to ensure that a similar conclusion holds even if ${\Pi }_{\mathrm{bft}}$ is completely subverted, i.e. the adversary has 100% of validators (but only < 50% of ${\Pi }_{\mathrm{lc}}$ hash rate).

The Crosslink Construction

We are now ready to give a description of a variant of Snap‑and‑Chat that takes into account the issues described in Notes on Snap‑and‑Chat, and that implements bounded dynamic availability. I call this the “Crosslink” construction. I will try to make the description relatively self-contained, but knowledge of the Snap‑and‑Chat construction from [NTT2020] (arXiv version) is assumed.

Conventions

“$\ast$” is a metavariable for the name of a protocol. We also use it as a wildcard in protocol names of a particular type, for example “$\ast$bc” for the name of some best‑chain protocol.

Protocols are referred to as ${\Pi }_{\ast }$ for a name “$\ast$”. Where it is useful to avoid ambiguity, when referring to a concept defined by ${\Pi }_{\ast }$ we prefix it with “$\ast$‑”.

We do not take synchrony or partial synchrony as an implicit assumption of the communication model; that is, unless otherwise specified, messages between protocol participants can be arbitrarily delayed or dropped. A given message is received at most once, and messages are nonmalleably authenticated as originating from a given sender whenever needed by the applicable protocol. Particular subprotocols may require a stronger model.

For simplicity, we assume that all events occur at global times in a total ordering. This assumption is not realistic in an asynchronous communication model, but it is not essential to the design or analysis and could be removed (essentially: replace times with events and use a partial happens-before ordering on events, in place of a total ordering on times).

A $\ast$‑execution is the complete set of events (message sends/receives and decisions by protocol participants) that occur in a particular run of ${\Pi }_{\ast }$ from its initiation up to a given time. A prefix of a $\ast$‑execution is also a $\ast$‑execution. Since executions always start from protocol initiation, a strict suffix of a $\ast$‑execution is not a $\ast$‑execution.

If $\ast$ maintains a (single) block chain, ${\mathcal{O}}_{\ast }$ refers to the genesis block of a $\ast$‑chain.

Let $\text{chain-txns}(\mathsf{ch})$ be the sequence of transactions in the given chain $\mathsf{ch}$, starting from genesis.

For convenience we conflate $\ast$‑blocks with $\ast$‑chains; that is, we identify a chain with the block at its tip. This is justified because, assuming that the hash function used for parent links is collision-resistant, there can be only one $\ast$‑chain corresponding to a $\ast$‑block.

If $\mathsf{ch}$ is a $\ast$‑chain, $\mathsf{ch}{\lceil }_{\ast }^{\sigma }$ means $\mathsf{ch}$ with the last $\sigma$ blocks pruned, except that if $\sigma \ge \mathsf{len}(\mathsf{ch})$, the result is the $\ast$‑chain consisting only of ${\mathcal{O}}_{\ast }$.

The block at depth $k\in {\mathbb{N}}^{+}$ in a $\ast$‑chain $\mathsf{ch}$ is defined to be the tip of $\mathsf{ch}{\lceil }_{\ast }^k$. Thus the block at depth $k$ in a chain is the last one that cannot be affected by a rollback of length $k$.

For $\ast$‑blocks $B$ and $C$,

• the notation $B{⪯}_{\ast }C$ means that the $\ast$‑chain with tip $B$ is a prefix of the one with tip $C$. This includes the case $B=C$.
• the notation $B⪯{⪰}_{\ast }C$ means that either $B{⪯}_{\ast }C$ or $C{⪯}_{\ast }B$. That is, “one of $B$ and $C$ is a prefix of the other”.

We also use $\mathsf{log}⪯{\mathsf{log}}^{\prime }$ (without a subscript on $⪯$) to mean that the transaction ledger $\mathsf{log}$ is a prefix of ${\mathsf{log}}^{\prime }$. Similarly to $⪯{⪰}_{\ast }$ above, $\mathsf{log}⪯⪰{\mathsf{log}}^{\prime }$ means that either $\mathsf{log}⪯{\mathsf{log}}^{\prime }$ or ${\mathsf{log}}^{\prime }⪯\mathsf{log}$; that is, “one of $\mathsf{log}$ and ${\mathsf{log}}^{\prime }$ is a prefix of the other”.

The notation $[f(X)\text{ for }X{⪯}_{\ast }Y]$ means the sequence of $f(X)$ for each $\ast$‑block $X$ in chain order from genesis up to and including $Y$. ($X$ is a bound variable within this construct.)

Subprotocols

As in Snap‑and‑Chat, we depend on a BFT protocol ${\Pi }_{\mathrm{origbft}}$, and a best‑chain protocol ${\Pi }_{\mathrm{origbc}}$.

We modify ${\Pi }_{\mathrm{origbft}}$ (resp. ${\Pi }_{\mathrm{origbc}}$) to give ${\Pi }_{\mathrm{bft}}$ (resp. ${\Pi }_{\mathrm{bc}}$) by adding structural elements, changing validity rules, and potentially changing the specified behaviour of honest nodes.

A Crosslink node must participate in both ${\Pi }_{\mathrm{bft}}$ and ${\Pi }_{\mathrm{bc}}$; that is, it must maintain a view of the state of each protocol. Acting in more specific roles such as bft‑proposer, bft‑validator, or bc‑block‑producer is optional, but we assume that all such actors are Crosslink nodes.

Model for BFT protocols (Π_{{origbft,bft}})

A player’s view in ${\Pi }_{\ast \mathrm{bft}}$ includes a set of $\ast$bft‑block chains each rooted at a fixed genesis $\ast$bft‑block ${\mathcal{O}}_{\ast \mathrm{bft}}$. There is a $\ast$bft‑block‑validity rule (specified below), which depends only on the content of the block and its ancestors. A non‑genesis block can only be $\ast$bft‑block‑valid if its parent is $\ast$bft‑block‑valid. A $\ast$bft‑valid‑chain is a chain of $\ast$bft‑block‑valid blocks.

Execution proceeds in a sequence of epochs. In each epoch, an honest proposer for that epoch may make a $\ast$bft‑proposal.

A $\ast$bft‑proposal refers to a parent $\ast$bft‑block, and specifies the proposal’s epoch. The content of a proposal is signed by the proposer using a strongly unforgeable signature scheme. We consider the proposal to include this signature. There is a $\ast$bft‑proposal‑validity rule, depending only on the content of the proposal and its parent block, and the validity of the proposer’s signature.

For each epoch, there is a fixed number of voting units distributed between the players, which they use to vote for a $\ast$bft‑proposal. We say that a voting unit has been cast for a $\ast$bft‑proposal $P$ at a given time in a $\ast$bft‑execution, if and only if $P$ is $\ast$bft‑proposal‑valid and a ballot for $P$ authenticated by the holder of the voting unit exists at that time.

Using knowledge of ballots cast for a $\ast$bft‑proposal $P$ that collectively satisfy a notarization rule at a given time in a $\ast$bft‑execution, and only with such knowledge, it is possible to obtain a valid $\ast$bft‑notarization‑proof ${\mathsf{proof}}_P$. The notarization rule must require at least a two‑thirds absolute supermajority of voting units in $P$’s epoch to have been cast for $P$. It may also require other conditions.

A voting unit is cast non‑honestly for an epoch’s proposal iff:

• it is cast other than by the holder of the unit (due to key compromise or any flaw in the voting protocol, for example); or
• it is double‑cast (i.e. there are at least two ballots casting it for distinct proposals); or
• the holder of the unit following the conditions for honest voting in ${\Pi }_{\ast \mathrm{bft}}$, according to its view, should not have cast that vote.

A $\ast$bft‑block consists of $(P,{\mathsf{proof}}_P)$ re‑signed by the same proposer using a strongly unforgeable signature scheme. It is $\ast$bft‑block‑valid iff:

• $P$ is $\ast$bft‑proposal‑valid; and
• ${\mathsf{proof}}_P$ is a valid proof that some subset of ballots cast for $P$ are sufficient to satisfy the notarization rule; and
• the proposer’s outer signature on $(P,{\mathsf{proof}}_P)$ is valid.

A $\ast$bft‑proposal’s parent reference hashes the entire parent $\ast$bft‑block, i.e. proposal, proof, and outer signature.

There is an efficiently computable function $\ast \text{bft‑last‑final}::\ast \text{bft‑block}\to \ast \text{bft‑block}\cup \{\perp \}$. For a $\ast$bft‑block‑valid input block $C$, this function outputs the last ancestor of $C$ that is final in the context of $C$.

$\ast \text{bft‑last‑final}$ must satisfy all of the following:

• $\ast \text{bft-last-final}(C)=\perp ⟺C$ is not $\ast$bft‑block‑valid.
• If $C$ is $\ast$bft‑block‑valid, then:
  • $\ast \text{bft-last-final}(C){⪯}_{\ast \mathrm{bft}}C$ (and therefore it must also be $\ast$bft‑block‑valid);
  • for all $\ast$bft‑valid‑blocks $D$ such that $C{⪯}_{\ast \mathrm{bft}}D$, $\ast \text{bft-last-final}(C){⪯}_{\ast \mathrm{bft}}\ast \text{bft-last-final}(D)$.
• $\ast \text{bft-last-final}({\mathcal{O}}_{\ast \mathrm{bft}})={\mathcal{O}}_{\ast \mathrm{bft}}$.

A particular BFT protocol might need adaptations to fit it into this model for ${\Pi }_{\mathrm{origbft}}$, before we apply the Crosslink modifications to obtain ${\Pi }_{\mathrm{bft}}$. Any such adaptions are necessarily protocol-specific. In particular,

• origbft‑proposal‑validity should correspond to the strongest property of an origbft‑proposal that is objectively and feasibly verifiable from the content of the proposal and its parent origbft‑block at the time the proposal is made. It must include verification of the proposer’s signature.
• origbft‑block‑validity should correspond to the strongest property of an origbft‑block that is objectively and feasibly verifiable from the content of the block and its ancestors at the time the block is added to an origbft‑chain. It should typically include all of the relevant checks from origbft‑proposal‑validity that apply to the created block (or equivalent checks). It must also include verification of the notarization proof and the proposer’s outer signature.
• If a node observes an origbft‑valid block $C$, then it should be infeasible for an adversary to cause a rollback in that node’s view past $\text{origbft-last-final}(C)$, and the view of the chain up to $\text{origbft-last-final}(C)$ should agree with that of all other honest nodes. This is formalized in the next section.

Safety of ${\Pi }_{\ast \mathrm{bft}}$

The intuition behind the following safety property is that:

• For ${\Pi }_{\ast \mathrm{bft}}$ to be safe, it should never be the case that two honest nodes observe (at any time) $\ast$bft‑blocks $B$ and $B^{\prime }$ respectively that they each consider final in some context, but $B⪯{⪰}_{\ast \mathrm{bft}}{B}^{\prime }$ does not hold.
• By definition, an honest node observes a $\ast$bft‑block to be final in the context of another $\ast$bft‑block $C$, iff $B{⪯}_{\ast \mathrm{bft}}\ast \text{bft-last-final}(C)$.

We say that a $\ast$bft‑block is “in honest view” if a party observes it at some time at which that party is honest.

Note that it is possible for this property to hold for an execution of a BFT protocol in an asynchronous communication model. The following caveat applies: if the one‑third bound on non‑honest voting property is ever broken at any time in an execution, then it may not be possible to maintain Final Agreement from that point on. This is an area of possible improvement in the design and analysis, left for future work.

Model for best-chain protocols (Π_{origbc,bc})

A node’s view in ${\Pi }_{\ast \mathrm{bc}}$ includes a set of $\ast$bc‑block chains each rooted at a fixed genesis $\ast$bc‑block ${\mathcal{O}}_{\ast \mathrm{bc}}$. There is a $\ast$bc‑block‑validity rule (often described as a collection of “consensus rules”), depending only on the content of the block and its ancestors. A non‑genesis block can only be $\ast$bc‑block‑valid if its parent is $\ast$bc‑block‑valid. By “$\ast$bc‑valid‑chain” we mean a chain of $\ast$bc‑block‑valid blocks.

The definition of $\ast$bc‑block‑validity is such that it is hard for a block producer to extend a $\ast$bc‑valid‑chain unless they are selected by a random process that chooses a block producer in proportion to their resources with an approximately known and consistent time distribution, subject to some assumption about the total proportion of resources held by honest nodes.

There is a function $\mathsf{score}::\ast \text{bc‑valid‑chain}\to \mathsf{Score}$, with $<$ a strict total ordering on $\mathsf{Score}$. An honest node will choose one of the $\ast$bc‑valid‑chains with highest score as the $\ast$bc‑best‑chain in its view. Any rule can be specified for breaking ties.

The $\mathsf{score}$ function is required to satisfy $\mathsf{score}(\mathsf{ch}{\lceil }_{\ast \mathrm{bc}}^1)<\mathsf{score}(\mathsf{ch})$ for any non‑genesis $\ast$bc‑valid‑chain $\mathsf{ch}$.

Unless an adversary is able to censor knowledge of other chains from the node’s view, it should be difficult to cause the node to switch to a chain with a last common ancestor more than $\sigma$ blocks back from the tip of their previous $\ast$bc‑best‑chain.

Following [NTT2020], we use the notation ${\mathsf{ch}}_i^t$ for node $i$’s $\ast$bc‑best‑chain at time $t$.

A $\ast$bc‑context allows testing whether a given transaction is contextually valid (“$\ast$bc‑context‑valid”), and adding it to the context if it is. Given a context $\mathsf{ctx}$, the resulting sequence of contextually valid transactions since genesis can be obtained as $\text{context-txns}(\mathsf{ctx})$. It is possible to obtain a $\ast$bc‑context corresponding to the state after the genesis $\ast$bc‑block.

We assume that the only reasons for a transaction to be contextually invalid are that it double‑spends, or that an input is missing.

A $\ast$bc‑block logically contains a sequence of transactions. In addition to other rules, a block is only $\ast$bc‑block‑valid if its transactions, taken in order, are all $\ast$bc‑context‑valid given previous blocks and previous transactions in the block.

A “coinbase transaction” is a $\ast$bc‑transaction that only distributes newly issued funds and has no inputs.

Define $\text{is-coinbase-only-block}::\ast \text{bc-block}\to \mathsf{boolean}$ so that $\text{is-coinbase-only-block}(B)=\mathsf{true}$ iff $B$ has exactly one transaction that is a coinbase transaction.

Each $\ast$bc‑block is summarized by a $\ast$bc‑header that commits to the block. There is a notion of $\ast$bc‑header‑validity that is necessary, but not sufficient, for validity of the block. We will only make the distinction between $\ast$bc‑headers and $\ast$bc‑blocks when it is necessary to avoid ambiguity.

Typically, Bitcoin‑derived best chain protocols do not need much adaptation to fit into this model. The model still omits some details that would be important to implementing Crosslink, but distracting for this level of abstraction.

Safety of ${\Pi }_{\ast \mathrm{bc}}$

We make an assumption on executions of ${\Pi }_{\mathrm{origbc}}$ that we will call Prefix Consistency (introduced in [PSS2016, section 3.3] as just “consistency”):

Prefix Consistency compares the $\sigma$-truncated chain of some node $i$ with the untruncated chain of node $j$. For our analysis of safety of the derived ledgers, we will also need to make an assumption on executions of ${\Pi }_{\mathrm{origbc}}$ that at any given time $t$, any two honest nodes $i$ and $j$ agree on their confirmed prefixes — with only the caveat that one may have observed more of the chain than the other. That is:

Safety Mode

Let ${\mathsf{LOG}}_{\mathrm{fin},i}^t::[\text{bc-transaction}]$ be the finalized ledger seen by node $i$ at time $t$, and let ${\mathsf{LOG}}_{\mathrm{bda},i,\mu }^t::[\text{bc-transaction}]$ be the more-available ledger at bc‑confirmation‑depth $\mu$ seen by node $i$ at time $t$.

The following definition is rough and only intended to provide intuition.

Consider, at a point in time $t$, the number of bc‑blocks of transactions that have entered ${\mathsf{LOG}}_{\mathrm{bda},i,0}^t$ but have not (yet) entered ${\mathsf{LOG}}_{\mathrm{fin},i}^t$. We call this the “finality gap” at time $t$. Under an assumption about the distribution of bc‑block intervals, if this gap stays roughly constant then it corresponds to the approximate time that transactions added to ${\mathsf{LOG}}_{\mathrm{bda},i,0}$ have taken to enter ${\mathsf{LOG}}_{\mathrm{fin},i}$ (if they do so at all) just prior to time $t$.

As explained in detail by The Arguments for Bounded Dynamic Availability and Finality Overrides, if this bound exceeds a reasonable threshold then it likely signals an exceptional or emergency condition, in which it is undesirable to keep accepting user transactions that spend funds into ${\mathsf{LOG}}_{\mathrm{bda},i,0}$.

The condition that the network enters in such cases will be called “Safety Mode”. For a given higher‑level transaction protocol, we can define a policy for which bc‑blocks will be accepted in Safety Mode. This will be modelled by a predicate $\text{is-safety-block}::\text{bc-block}\to \mathsf{boolean}$. A bc‑block for which $\text{is-safety-block}$ returns $\mathsf{true}$ is called a “safety block”.

Note that a bc‑block producer is only constrained to produce safety blocks while, roughly speaking, its view of the finalization point remains stalled. In particular an adversary that has subverted the BFT protocol in a way that does not keep it in a stalled state can always avoid being constrained by Safety Mode.

The desired properties of safety blocks and a possible Safety Mode policy for Zcash are discussed in the How to block hazards section of The Arguments for Bounded Dynamic Availability and Finality Overrides.

Parameters

Crosslink is parameterized by a bc‑confirmation‑depth $\sigma \in {\mathbb{N}}^{+}$ (as in Snap‑and‑Chat), and also a finalization gap bound $L\in {\mathbb{N}}^{+}$ with $L$ significantly greater than $\sigma$.

Each node $i$ always uses the fixed confirmation depth $\sigma$ to obtain its view of the finalized ledger ${\mathsf{LOG}}_{\mathsf{fin},i}::[\text{bc-transaction}]$.

Each node $i$ chooses a potentially different bc‑confirmation‑depth $\mu \in \mathbb{N}$ to obtain its view of the bounded‑dynamically‑available ledger ${\mathsf{LOG}}_{\mathsf{bda},i,\mu }::[\text{bc-transaction}]$. We will assume that $\mu \le \sigma$, since there is no reason to choose $\mu >\sigma$. Choosing $\mu <\sigma$ is at the node’s own risk and may increase the risk of rollback attacks against ${\mathsf{LOG}}_{\mathsf{bda},i,\mu }$ (it does not affect ${\mathsf{LOG}}_{\mathsf{fin},i}$). The default should be $\mu =\sigma$.

Structural additions

1. Each bc‑header has, in addition to origbc‑header fields, a $context\_bft$ field that commits to a bft‑block.
2. Each bft‑proposal has, in addition to origbft‑proposal fields, a $headers\_bc$ field containing a sequence of exactly $\sigma$ bc‑headers (zero‑indexed, deepest first).
3. Each non‑genesis bft‑block has, in addition to origbft‑block fields, a $headers\_bc$ field containing a sequence of exactly $\sigma$ bc‑headers (zero-indexed, deepest first). The genesis bft‑block has $headers\_bc=\varnothing$.
4. Each bc‑transaction has, in addition to origbc‑transaction fields, a $block\_bc$ field labelling it with the bc‑block that it comes from. (This is not used directly by Crosslink but it may be needed to check ${\Pi }_{\mathrm{bc}}$ consensus rules.)

For a bft‑block or bft‑proposal $B$, define $$\mathsf{snapshot}(B)=\{\begin{array}{ll}{\mathcal{O}}_{\mathrm{bc}},& \text{if }B.headers\_bc=\varnothing \\ B.headers\_bc[0]{\lceil }_{\mathrm{bc}}^1,& \text{otherwise.}\end{array}$$

Π_bft changes from Π_origbft

Π_bft proposal and block validity

${\mathcal{O}}_{\mathrm{bft}}$ is bft‑valid.

A bft‑proposal (resp. non‑genesis bft‑block) $B$ is bft‑proposal‑valid (resp. bft‑block‑valid) iff all of the following hold:

• Inherited origbft rules: The corresponding origbft‑proposal‑validity (resp. origbft‑block‑validity) rules hold for $B$.
• Increasing Score rule: Either $\mathsf{score}(\mathsf{snapshot}(B{\lceil }_{\mathrm{bft}}^1))<\mathsf{score}(\mathsf{snapshot}(B))$ or $\mathsf{snapshot}(B{\lceil }_{\mathrm{bft}}^1)=\mathsf{snapshot}(B)$.
• Tail Confirmation rule: $B.headers\_bc$ form the $\sigma$‑block tail of a bc‑valid‑chain.

The “corresponding validity rules” are assumed to include the Parent rule that $B$’s parent is bft‑valid.

Note: origbft‑block‑validity rules may be different to origbft‑proposal‑validity rules. For example, in adapted Streamlet, a origbft‑block needs evidence that it was voted for by a supermajority, and an origbft‑proposal doesn’t. Such differences also apply to bft‑block‑validity vs bft‑proposal‑validity.

Π_bft block finality in context

The finality rule for bft‑blocks in a given context is unchanged from origbft‑finality. That is, $\text{bft-last-final}$ is defined in the same way as $\text{origbft-last-final}$ (modulo referring to bft‑block‑validity and ${\mathcal{O}}_{\mathrm{bft}}$).

Π_bft honest proposal

An honest proposer of a bft‑proposal $P$ chooses $P.headers\_bc$ as the $\sigma$‑block tail of its bc‑best‑chain, provided that it is consistent with the Increasing Score rule. If it would not be consistent with that rule, it sets $P.headers\_bc$ to the same $headers\_bc$ field as $P$’s parent bft‑block. It does not make proposals until its bc‑best‑chain is at least $\sigma +1$ blocks long.

Π_bft honest voting

An honest validator considering a proposal $P$, first updates its view of both subprotocols with the bc‑headers given in $P.headers\_bc$, downloading bc‑blocks for these headers and checking their bc‑block‑validity.

For each downloaded bc‑block, the bft‑chain referenced by its $context\_bft$ field might need to be validated if it has not been seen before.

After updating its view, the validator will vote for a proposal $P$ only if:

• Valid proposal criterion: it is bft‑proposal‑valid, and
• Confirmed best‑chain criterion: $\mathsf{snapshot}(P)$ is part of the validator’s bc‑best‑chain at a bc‑confirmation‑depth of at least $\sigma$.

Π_bc changes from Π_origbc

Definitions of LOG^t_fin,i and LOG^t_bda,i,μ

In Snap‑and‑Chat, a node $i$ at time $t$ obtains ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ from its latest view of bft‑finality.

In Crosslink, it obtains ${\mathsf{LOG}}_{\mathrm{fin},i}^t$ from the view of bft‑finality given by ${\mathsf{ch}}_i^t{\lceil }_{\mathrm{bc}}^{\sigma }$, i.e. the block at depth $\sigma$ in node $i$’s bc‑best‑chain at time $t$.

Specifically,$$\begin{array}{rcl}\text{san-ctx}& ::& [\text{bc-chain}]\to \text{bc-context}\\ \text{san-ctx}(S)& :=& \mathsf{sanitize}(\mathsf{concat}([\text{chain-txns}(C)\text{ for }C\text{ in }S]))\\ \mathsf{LF}(H)& :=& \text{bft-last-final}(H.context\_bft)\\ \text{fin}& ::& \text{bc-block}\to [\text{bc-chain}]\\ \mathsf{fin}(H)& :=& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })]\\ \text{fin-ctx}(H)& :=& \text{san-ctx}(\mathsf{fin}(H))\\ \text{bda-ctx}(H,\mu )& :=& \text{san-ctx}(\mathsf{fin}(H)||[H{\lceil }_{\mathrm{bc}}^{\mu }])\\ {\mathsf{LOG}}_{\mathrm{fin},i}^t& :=& \text{context-txns}(\text{fin-ctx}({\mathsf{ch}}_i^t))\\ {\mathsf{LOG}}_{\mathrm{bda},i,\mu }^t& :=& \text{context-txns}(\text{bda-ctx}({\mathsf{ch}}_i^t,\mu ))\end{array}$$

For the definitions that use it, $\mu \in \mathbb{N}$ is a confirmation depth.

Sanitization is the same as in Snap‑and‑Chat: it does a left fold over an input sequence of transactions, adding each of them to a running bc‑context if they are bc‑context‑valid. The initial bc‑context for this fold corresponds to the state after the genesis bc‑block. This process can be optimized by immediately discarding duplicate bc‑blocks in the concatenated snapshot chains after their first occurrence.

Π_bc contextual validity change

In Crosslink or Snap‑and‑Chat, contextual validity is used in three different cases:

a) sanitization of the constructed ledgers ${\mathsf{LOG}}_{\mathrm{fin},i}$ and ${\mathsf{LOG}}_{\mathrm{bda},i,\mu }$;

b) checking whether a block is bc‑block‑valid in order to append it to a chain;

c) checking whether a transaction in the mempool could be included in a block.

Note that the model we presented earlier considers only adding a transaction to an origbc‑context. It is straightforward to apply this to the sanitization use case a), as described in the previous section. However, the other two use cases raise the question of which starting bc‑context to use.

We resolve this by saying that new blocks and mempool transactions are checked in the bc‑context obtained from $\text{bda-ctx}(H^{\prime },0)$, where $H^{\prime }$ is the relevant parent bc‑block.

Π_bc block validity

Genesis rule: For the genesis bc‑block we must have ${\mathcal{O}}_{\mathrm{bc}}.context\_bft={\mathcal{O}}_{\mathrm{bft}}$, and therefore $\text{bft-last-final}({\mathcal{O}}_{\mathrm{bc}}.context\_bft)={\mathcal{O}}_{\mathrm{bft}}$.

A bc‑block $H$ is bc‑block‑valid iff all of the following hold:

• Inherited origbc rules: $H$ satisfies the corresponding origbc‑block‑validity rules.
• Valid context rule: $H.context\_bft$ is bft‑block‑valid.
• Extension rule: $\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^1){⪯}_{\mathrm{bft}}\mathsf{LF}(H)$.
• Finality depth rule: Define: $$\begin{array}{rl}\mathsf{tailhead}(H):=& \text{last-common-ancestor}(\mathsf{snapshot}(\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })),H)\\ \text{finality-depth}(H):=& \mathsf{height}(H)-\mathsf{height}(\mathsf{tailhead}(H))\end{array}$$ Then either $\text{finality-depth}(H)\le L$ or $\text{is-safety-block}(H)$.

Π_bc honest block production

An honest producer of a bc‑block $H$ must follow the consensus rules under ${\Pi }_{\mathrm{bc}}$ block validity above. In particular, it must produce a safety block if required to do so by the Finality depth rule. It also must only include transactions that are valid in the context specified under ${\Pi }_{\mathrm{bc}}$ contextual validity change above.

To choose $H.context\_bft$, the producer considers a subset of the tips of bft‑valid‑chains in its view: $$\{T:T\text{ is bft‑block‑valid and }\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^1){⪯}_{\mathrm{bft}}\text{bft-last-final}(T)\}$$ It chooses one of the longest of these chains, $C$, breaking ties by maximizing $\mathsf{score}(\mathsf{snapshot}(\text{bft-last-final}(C)))$. If there is still a tie then it is broken arbitrarily.

The honest block producer then sets $H.context\_bft:=C$.

At this point we have completed the definition of Crosslink. In Security Analysis of Crosslink, we will prove it secure.

Security Analysis of Crosslink

This document analyses the security of Crosslink in terms of liveness and safety. It assumes that you have read The Crosslink Construction which defines the protocol.

Liveness argument

First note that Crosslink intentionally sacrifices availability if there is a long finalization stall.

It would still be a bug if there were any situation in which ${\Pi }_{\mathrm{bc}}$ failed to be live, though, because that would allow tail‑thrashing attacks.

Crosslink involves a bidirectional dependence between ${\Pi }_{\mathsf{bft}}$ and ${\Pi }_{\mathsf{bc}}$. The Ebb‑and‑Flow paper [NTT2020] argues in Appendix E ("Bouncing Attack on Casper FFG") that it can be more difficult to reason about liveness given a bidirectional dependence between protocols:

To ensure consistency among the two tiers [of Casper FFG], the fork choice rule of the blockchain is modified to always respect ‘the justified checkpoint of the greatest height [*]’ [22]. There is thus a bidirectional interaction between the block proposal and the finalization layer: blocks proposed by the blockchain are input to finalization, while justified checkpoints constrain future block proposals. This bidirectional interaction is intricate to reason about and a gateway for liveness attacks.

The argument is correct as far as it goes. The main reason why this does not present any great difficulty to proving liveness of Crosslink, is due to a fundamental difference from Casper FFG: in Crosslink the fork‑choice rule of ${\Pi }_{\mathrm{bc}}$ is not modified.

Let $\mathcal{S}$ be the subset of bc‑blocks $\{B:\text{is-coinbase-only-block}(B)\text{ and }\text{is-safety-block}(B)\}$. Assume that $\mathcal{S}$ is such that a bc‑block‑producer can always produce a block in $\mathcal{S}$.

In that case it is straightforward to convince ourselves that the additional bc‑block‑validity rules are never an obstacle to producing a new bc‑block in $\mathcal{S}$:

• The changes to the definition of contextual validity do not interfere with liveness, since they do not affect coinbase transactions, and therefore do not affect blocks in $\mathcal{S}$. That is, the bc‑block‑producer can always just omit non‑coinbase transactions that are contextually invalid.
• The Genesis rule doesn't apply to new bc‑blocks.
• The Valid context rule and Extension rule are always satisfiable by referencing the same context bft‑block as the parent bc‑block.
• The Finality depth rule always allows the option of producing a safety block, and therefore does not affect blocks in $\mathcal{S}$.

The instructions to an honest bc‑block‑producer allow it to produce a block in $\mathcal{S}$. Therefore, ${\Pi }_{\mathrm{bc}}$ remains live under the same conditions as ${\Pi }_{\mathrm{origbc}}$.

The additional bft‑proposal‑validity, bft‑block‑validity, bft‑finality, and honest voting rules are also not an obstacle to making, voting for, or finalizing bft‑proposals:

• Because ${\Pi }_{\mathrm{bc}}$ is live, there will always be some point in time at which a fresh valid bc‑header chain that satisfies both the Increasing score rule and the Tail confirmation rule exists for use in the $P.headers\_bc$ field.
• If no fresh valid bc‑header chain is available, the Increasing score rule and Tail confirmation rule allow an honest bft‑proposer to choose $headers\_bc$ to be the same as in the previous bft‑block. So, if liveness of ${\Pi }_{\mathrm{origbft}}$ depends on an honest proposer always being able to make a proposal (as it does in adapted‑Streamlet for example), then this requirement will not be violated.
• The changes to voting are only requiring a vote to be for a proposal that could have been honestly proposed.
• The bft‑finality rules are unchanged from origbft‑finality.

Therefore, ${\Pi }_{\mathrm{bft}}$ remains live under the same conditions as in Snap‑and‑Chat applied to ${\Pi }_{\mathrm{origbft}}$.

The only other possibility for a liveness issue relative to Snap‑and‑Chat would be if the change to the construction of ${\mathsf{LOG}}_{\mathrm{fin}}$ could cause it to stall, even when ${\Pi }_{\mathrm{bft}}$ and ${\Pi }_{\mathrm{bc}}$ are both still live.

However, liveness of ${\Pi }_{\mathrm{bft}}$ and the Increasing score rule together imply that at each point in time, provided there are sufficient honest bft‑proposers/validators, eventually a new bft‑block with a higher-scoring snapshot will become final in the context of the longest bft‑valid‑chain. ==TODO make that more precise.==

Because of the Extension rule, this new bft‑block must be a descendent of the previous final bft‑block in the context visible to bc‑block‑producers. Therefore, the new finalized chain will extend the old finalized chain. It could be the case that all of the new transactions are sanitized out, but that would only happen if they double‑spend or use outputs that were nonexistent in the context computed by $\text{bda-ctx}$ at the point at which they are to be contextually checked.

Finally, we need to show that Safety Mode is only triggered when it should be; that is, when the assumptions needed for liveness of ${\Pi }_{\mathrm{bft}}$ are violated. Informally, that is the case because, as long as there are sufficient honest bc‑block‑producers and sufficient honest bft‑proposers/validators, the finalization point implied by the $context\_bft$ field at the tip of the bc‑best chain in any node's view will advance fast enough for the finalization gap bound $L$ not to be hit. This depends on the value of $L$ relative to $\sigma$, the network delay, the hash rate of honest bc‑block‑producers, the number of honest bft‑proposers and the proportion of voting units they hold, and other details of the BFT protocol. ==TODO: more detailed argument needed, especially for the dependence on $L$.==

Safety argument

Discussion

The Extension rule ensures that, informally, if a given node $i$'s view of its bc‑best‑chain at a depth of $\sigma$ blocks does not roll back, then neither does its view of the bft‑final block referenced by its bc‑best‑chain, and therefore neither does its view of ${\mathsf{LOG}}_{\mathrm{fin},i}^t$.

This does not by itself imply that all nodes are seeing the "same" confirmed bc‑best‑chain (up to propagation timing), or the same ${\mathsf{LOG}}_{\mathrm{fin},i}^t$. If the network is partitioned and ${\Pi }_{\mathrm{bft}}$ is subverted, it could be that the nodes on each side of the partition follow a different fork, and the adversary arranges for each node's view of the last final bft‑block to be consistent with the fork it is on. It can potentially do this if it has more than one third of validators, because if the validators are partitioned in the same way as other nodes, it can vote with an additional one third of them on each side of the fork.

This is, if you think about it, unavoidable. ${\Pi }_{\mathrm{bc}}$ doesn't include the mechanisms needed to maintain finality under partition; it takes a different position on the CAP trilemma. In order to maintain finality under partition, we need ${\Pi }_{\mathrm{bft}}$ not to be subverted (and to actually work!)

So what is the strongest security property we can realistically get? It is stronger than what Snap‑and‑Chat provides. Snap‑and‑Chat is unsafe even without a partition if ${\Pi }_{\mathrm{bft}}$ is subverted. Ideally we would have a protocol with safety that is only limited by attacks "like" the unavoidable attack described above --- which also applies to ${\Pi }_{\mathrm{bc}}$ used on its own.

Proof of safety for LOG_fin

In order to capture the intuition that it is hard in practice to cause a consistent partition of the kind described in the previous section, we will need to assume that the Prefix Agreement safety property holds for the relevant executions of ${\Pi }_{\mathrm{bc}}$. The structural and consensus modifications to ${\Pi }_{\mathrm{bc}}$ relative to ${\Pi }_{\mathrm{origbc}}$ seem unlikely to have any significant effect on this property, given that we proved above that they do not affect liveness. ==TODO: that is a handwave; we should be able to do better, as we do for ${\Pi }_{\mathrm{bft}}$ below.== So, to the extent that it is reasonable to assume that Prefix Agreement holds for executions of ${\Pi }_{\mathrm{origbc}}$ under some conditions, it should also be reasonable to assume it holds for executions of ${\Pi }_{\mathrm{bc}}$ under the same conditions.

Recall that $\mathsf{LF}(H):=\text{bft-last-final}(H.context\_bft)$.

Using the Prefix Lemma once for each direction, we can transfer the Prefix Agreement property to the referenced bft‑blocks:

(The notation $B⪯{⪰}_{\ast }C$ means that either $B{⪯}_{\ast }C$ or $C{⪯}_{\ast }B$. That is, "one of $B$ and $C$ is a prefix of the other".)

Recall that $$\begin{array}{rcl}\text{san-ctx}& ::& [\text{bc-chain}]\to \text{bc-context}\\ \text{san-ctx}(S)& :=& \mathsf{sanitize}(\mathsf{concat}([\text{chain-txns}(C)\text{ for }C\text{ in }S]))\\ \mathsf{LF}(H)& :=& \text{bft-last-final}(H.context\_bft)\\ \text{fin}& ::& \text{bc-block}\to [\text{bc-chain}]\\ \mathsf{fin}(H)& :=& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })]\\ \text{fin-ctx}(H)& :=& \text{san-ctx}(\mathsf{fin}(H))\\ \text{bda-ctx}(H,\mu )& :=& \text{san-ctx}(\mathsf{fin}(H)||[H{\lceil }_{\mathrm{bc}}^{\mu }])\\ {\mathsf{LOG}}_{\mathrm{fin},i}^t& :=& \text{context-txns}(\text{fin-ctx}({\mathsf{ch}}_i^t))\\ {\mathsf{LOG}}_{\mathrm{bda},i,\mu }^t& :=& \text{context-txns}(\text{bda-ctx}({\mathsf{ch}}_i^t,\mu ))\end{array}$$

Because $\mathsf{fin}$ takes the form $\mathsf{fin}(H):=[f(X)\text{ for }X{⪯}_{\mathrm{bft}}g(H)]$, we have that $g(H){⪯}_{\mathrm{bft}}g(H^{\prime })⟹\mathsf{fin}(H)⪯\mathsf{fin}(H^{\prime })$. (This would be true for any well‑typed $f$ and $g$.)

By this observation and the Prefix Agreement Lemma, we also have that, in an execution of Crosslink where ${\Pi }_{\mathrm{bc}}$ has the Prefix Agreement safety property at confirmation depth $\sigma$, for all times $t$, $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 }$, $\mathsf{fin}({\mathsf{ch}}_i^t)⪯⪰\mathsf{fin}({\mathsf{ch}}_j^{t^{\prime }})$.

Because $\mathsf{sanitize}$ only considers previous state, $\text{context-txns}$ ∘ $\text{san-ctx}$ must be a prefix-preserving map; that is, if $S_1⪯S_2$ then $\text{context-txns}(\text{san-ctx}(S_1))⪯\text{context-txns}(\text{san-ctx}(S_2))$. Therefore:

Notice that this does not depend on any safety property of ${\Pi }_{\mathrm{bft}}$, and is an elementary proof. ([NTT2020, Theorem 2] is a much more complicated proof that takes nearly 3 pages, not counting the reliance on results from [PS2017].)

In addition, just as in Snap‑and‑Chat, safety of ${\mathsf{LOG}}_{\mathrm{fin}}$ can be inferred from safety of ${\Pi }_{\mathrm{bft}}$, which follows from safety of ${\Pi }_{\mathrm{origbft}}$. We prove this based on the Final Agreement property for executions of ${\Pi }_{\mathrm{origbft}}$:

The changes in ${\Pi }_{\mathrm{bft}}$ relative to ${\Pi }_{\mathrm{origbft}}$ only add structural components and tighten bft‑block‑validity and bft‑proposal‑validity rules. So for any legal execution of ${\Pi }_{\mathrm{bft}}$ there is a corresponding legal execution of ${\Pi }_{\mathrm{origbft}}$, with the structural additions erased and with the same nodes honest at any given time. A safety property, by definition, only asserts that executions not satisfying the property do not occur. Safety properties of ${\Pi }_{\mathrm{origbft}}$ necessarily do not refer to the added structural components in ${\Pi }_{\mathrm{bft}}$. Therefore, for any safety property of ${\Pi }_{\mathrm{origbft}}$, including Final Agreement, the corresponding safety property holds for ${\Pi }_{\mathrm{bft}}$.

By the definition of $\mathsf{fin}$ as above, in an execution of Crosslink where ${\Pi }_{\mathrm{bft}}$ has Final Agreement, for all times $t$, $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 }$, $\mathsf{fin}({\mathsf{ch}}_i^t)⪯⪰\mathsf{fin}({\mathsf{ch}}_j^{t^{\prime }})$. Therefore, by an argument similar to the one above using the fact that $\text{context-txns}$ ∘ $\text{san-ctx}$ is a prefix-preserving map: