The zebra-crosslink Book

zebra-crosslink is Shielded Labs's implementation of Zcash Crosslink, a hybrid PoW/PoS consensus protocol for Zcash. Refer to the Rationale, Scope, and Goals to understand our effort. See our roadmap for current progress status.

Prototype Workshops

Shielded Labs hosts semi-regular workshops as the prototype progresses; if you're interested in joining, get in touch!

Prototype Codebase

Status: This codebase is an early prototype, and suitable for the adventurous or curious who want to explore rough experimental releases.

This zebra-crosslink codebase is a fork of zebra. If you simply want a modern Zcash production-ready mainnet node, please use that upstream node.

Build and Usage

To try out the software and join the testnet, see Build and Usage.

Design and Implementation

This book is entirely focused on this implementation of Zcash Crosslink. For general Zebra usage or development documentation, please refer to the official Zebra Book. We strive to document the Design and Implementation changes in this book.

Maintainers

zebra-crosslink is maintained by Shielded Labs, makers of fine Zcash software.

Contributing

Our github issues are open for feedback. We will accept pull requests after the prototyping phase is done.

License

Zebra is distributed under the terms of both the MIT license and the Apache License (Version 2.0). Some Zebra crates are distributed under the MIT license only, because some of their code was originally from MIT-licensed projects. See each crate's directory for details.

See LICENSE-APACHE and LICENSE-MIT.

User Documentation

This section contains details on how to install, run, and instrument Zebra.

Building zebra-crosslink

These are the build and usage instructions for a generic linux system. nix users should check out nix Support.

Building zebra-crosslink requires Rust, libclang, and a C++ compiler.

Dependencies

1. Install cargo and rustc.

2. Install zebra-crosslink's build dependencies:

   • libclang is a library that might have different names depending on your package manager. Typical names are libclang, libclang-dev, llvm, or llvm-dev.
   • clang or another C++ compiler: g++ (all platforms) or Xcode (macOS).
   • protoc

TODO: We need to add prerequisites for the visualizer.

cargo build --locked zebrad

Usage

cargo run

To connect to the current prototype testnet, see crosslink-testnet.md.

nix Support

The flake* files/directories provide a nix flake for zebra-crosslink. This page assumes you have flake support enabled (or pass the temporary cli flags for flake support).

Standard flake commands

Standard flake commands all work:

• nix build
• nix flake check
• nix develop
• nix flake install .
• nix flake install 'github:shieldedlabs/zebra-crosslink'

The built package includes the zebrad binary and this book (rendered).

Crosslink Design

The zebra-crosslink design fleshes out and adapts the abstract Crosslink 2 into a working implementation. This includes extending and adapting that construction to include a fully functional BFT protocol, and including staking mechanics, accounting, and associated security reasoning and arguments. Additionally, we explicitly alter some trade-offs, or terminology compared to the abstract construction.

This Design chapter focuses specifically on differences from pure PoW Zcash (using zebra as a reference implementation) and the Crosslink 2 construction. We assume basic familiarity with both. Also, please see our Terminology for terms specific to this project.

We will be refining a ZIP Draft which will enter the formal ZIP process as the prototype approaches maturity and we switch focus to productionization.

WARNINGS

• These extensions and changes from the Crosslink 2 construction may violate some of the assumptions in the ssecurity proofs. This still needs to be reviewed after this design is more complete.
• We are using a custom-fit in-house BFT protocol for prototyping. It's own security properties need to be more thoroughly verified.
• All trade-off decisions need to be thoroughly vetted for market fit, while ensuring we maintain a minimum high bar for safety befitting Zcash's pedigree. Part of our implementation approach is to do rapid prototyping to explore the market fit more directly while modifying trade-offs in the design.

It is especially important that we identify deviations from Zcash PoW consensus, the Crosslink 2 construction, and the upstream zebra implementation. In particular, it is important for us to clarify our rationale for deviation, which may fit one of these general categories:

• We intentionally prefer a different trade-off to the original design; in which case we should have very explicit rationale documentation about the difference (in an ADR). One example (TODO: not-yet-done) is our ADR-0001 selects a different approach to on-chain signatures than (TODO: link to TFL section).
• Something about the more abstract design makes assumptions we cannot uphold in practice with all of the other implementation constraints. In this case, we need to determine if the upstream design needs to be improved, or we need to alter our implementation constraints.
• As an expedient, we found it quicker and easier to do something different to get the prototype working, even though we believe the upstream makes better trade-offs. These are prime candidates for improvement during productionization to match the design, or else require persuasive rationale that a "short cut" is worth the trade-offs and risks.

Scope for Crosslink

What are our goals for the first deployment of Crosslink?

Rationale

Why add a Proof-of-Stake finality gadget?

• The Proof-of-Stake finality gadget adds crosslink finality, which protects users from being robbed, improves the safety and efficiency of bridges, and enables centralized exchanges, decentralized exchanges, and other services to reduce and unify deposit times.
• Proof-of-Stake provides a different and complementary kind of security that pure Proof-of-Work doesn't, by allowing the value at stake (which inventivizes defenders to protect users) to be cumulative instead of transient. This makes Zcash more secure—it provides better security for the same security budget. It also makes Zcash more sustainable—it provides long-term security even as the rate of issuance shrinks, which strengthens assurance that the 21M supply cap will be maintained.
• Proof-of-Stake replaces some of the sell pressure from miners with buy pressure from finalizers. This is good because the price of ZEC is the fuel for the mission and attracts users.
• Proof-of-Stake allows a larger number of users to participate actively in the network than mining does, and to become direct recipients of ZEC issued by the blockchain. This increases the size and diversity of the set of users and stakeholders ¹.

Why Keep the Proof-of-Work blockchain?

• Proof-of-Work provides a different and complementary kind of security that pure Proof-of-Stake doesn’t, by requiring a recurring, non-reusable, and non-recoverable expenditure (by defenders and potential attackers). This prevents attackers from re-using resources in attacks (whether simultaneous or successive attacks). Crosslink security is therefore more robust and self-healing against large-scale attacks than pure Proof-of-Stake security.
• Proof-of-Work provides excellent liveness, availability, and censorship-resistance (which complements the censorship-resistance provided by using end-to-end-encryption whenever possible).
• Proof-of-Work allows people to earn ZEC by mining, even if they don’t already own any ZEC and they can’t acquire ZEC any other way.
• Keeping Proof-of-Work in addition to adding Proof-of-Stake means that in addition to adding the stakers, we also keep miners as active participants in the network and recipients of ZEC, increasing the size and diversity of the Zcash network and the ZEC economy.

UX goals

This list of UX Goals is tracked on GitHub.

• CEXes (GH #131) and decentralized services like DEXes/bridges (GH #128) are willing to rely on Zcash transaction finality. E.g. Coinbase reduces its required confirmations to no longer than Crosslink finality. All or most services rely on the same canonical (protocol-provided) finality instead of enforcing their own additional delays or conditions, so users get predictable transaction finality across services.
• GH #127: Casual users (who understand little about crypto and do not use specialized tools such as a Linux user interface) delegate ZEC and get rewards from their mobile wallet. GH #124 They have to learn a minimal set of new concepts in order to do this.
• GH #158: Users can get compounding returns by leaving their stake plus their rewards staked, without them or their wallet having to take action.
• GH #126: Skilled users (who understand more and can use specialized tools) run finalizers and get rewards.
• GH #214: Skilled users can easily collect records of finalizer behavior and performaance.

Shielded Labs’s First Deployment of Crosslink is not done until substantial numbers of real users are actually gaining the above benefits.

Deployment Goals

This list of Deployment Goals is tracked on GitHub.

• GH #125: Zcash transactions come with a kind of finality which protects the users as much as possible against all possible attacks, and is sufficient for services such as cross-chain bridges and centralized exchanges.
• GH #124: Users can delegate their ZEC and earn rewards, safely and while needing to learn only the minimal number of new concepts.
  • Delegating to a finalizer does not enable the finalizer to steal your funds.
  • Delegating to a finalizer does not leak information that links the user's action to other information about them, such as their IP address, their other ZEC holdings that they are choosing not to stake, or their previous or future transactions.
• GH #123: The time-to-market and the risk of Shielded Labs's First Deployment of Crosslink is minimized: the benefits listed above start accruing to users as soon as safely possible.
• GH #122: Activating Crosslink on Zcash mainnet retains as much as possible of Zcash users' safety, security, privacy, and availability guarantees.

Trade-offs

Goals which we currently believe are not safely achievable in this first deployment without losing some of the above goals:

• Improving Zcash's bandwidth (number of transactions per time) or latency (time for a transaction).
• Deploying cross-chain interoperation such as the Inter-Blockchain Communication protocol (IBC) or Cross-Chain Interoperability Protocol (CCIP).
• Supporting a large number of finalizers so that any user who wants to run their own finalizer can do so.
• Supporting casual users, with little computer expertise, running finalizers.

Non-Goals

• The consensus mechanism is needed primarily to prevent double-spending/multi-spending/rollback attacks. It is not the primary provider of censorship-resistance, since that is provided primarily by end-to-end encryption, and it is not the primary provider of counterfeiting-resistance, since that is provided by proofs and turnstiles. So censorship-resistance and counterfeiting-resistance are not primary goals for (at least) the first deployment of Crosslink.
• This is neutral with regard to Zcash governance —-- it doesn't change anything about Zcash governance.

1. In Proof-of-Work, smaller miners have a substantial economic disadvantage compared to larger mining operations, resulting in almost all hashpower being controlled by a few large miners. This economic disadvantage is reduced in Proof-of-Stake finalization—smaller finalizers have less of an economic disadvantage compared to larger finalizers. The economic disadvantage is almost eliminated in Proof-of-Stake delegation—smaller delegators compete on a level playing field with larger delegators, earning roughly the same reward with roughly the same risk. ↩

Engineering Deliverables for Shielded Lab's Crosslink Deployment

This is a draft list of SL's engineering deliverables as part of our Crosslink Deployment project. This list may be refined as the project develops, both to provide greater precision or clarity around deliverables, or to add or potentially remove deliverables (ideally only in early phases of the project lifecycle).

Code Products

The active list of Code Deliverables is evolving on GitHub, and includes these major components:

• a full node implementation of the Crosslink protocol - intended for use by all full node users
  • GH #105 augmentation of existing RPC APIs for blocks and transactions to include finality status
  • GH #104 new RPC APIs related to Proof-of-Stake: finalizer identities, staking weights, delegation info
  • GH #172 new RPC APIs related to Crosslink: contingency mode, finality traversal
• GH #154 a basic working commandline finalizer (probably as a configured mode of the full node) - potentially used by production finalizers
• GH #106 a basic, minimal stake delegation tool - this will not be an easily usable or recommended product for end users
• GH #112 all necessary Continuous Integration / Continuous Deployment source code is an explicit code deliverable

All code products will be open source and suitable for merging or bundling with zebra source and binary distributions.

All code products will be first developed and released as testnet prototypes which are then matured into production-ready status as the target activation date approaches.

Technical Documentation

The active list of Documentation Deliverables is evolving on GitHub, and includes these important components:

• User facing documentation about Crosslink finality and safety considerations, including links to assessments, analyses, and audits by other parties.
• User facing documentation for users of all code deliverables.
• Design notes on prototype design trade-offs, delegation secure UX considerations, and a "Staking in Zcash" primer for PoS protocol-expert audiences.
• A Productionization Plan describing the process to develop the prototype into a safe mainnet production deployment and activation process.
• Process documentation for code releases, testnet deployments, and documentation releases intended for current and future maintainers, and developers.

External Validation Partnerships

While not deliverables per se, a key strategy we'll use for gauging our success is to establish working relationships with partner teams which are representative stakeholders for these categories:

• Wallet developers
• Finalizers
• Exchanges
• Bridges, DEXes, or other protocol-integration product teams

Our success criteria require user-facing in-production products in these categories (with the first three prioritized). In order to meet these criteria, we need to engage with high quality partners to serve as representative stakeholders relatively early in the process, as the prototype approaches a usable state. We track ongoing Partner Validation goals on GitHub.

Crosslink Security Properties

Crosslink is designed and can be analyzed with respect to the following security properties:

Irreversible Finality

Transactions enter a finalized state, and finalized transactions cannot be rolled back. Failure of this security property is called “rollback attack”.

Importantly, all participants who are sufficiently in sync with the consensus agree on finality status, or if there is a failure by the protocol to provide finality, all of those participants agree that this failure occurred. This contrasts with PoW which provides “probabilistic finality” and subtly this means every participant must select their own rollback threshold at which point they consider a protocol failure event to have occurred (including potential malicious “rollback attacks”). Because these thresholds vary over users, rollbacks naturally fragment users into groups with competing interests in the event of protocol failures.

Liveness/Availability

It is possible for any user to get at least some of their transactions paying sufficiently high fees to be included in one of the next few blocks. Failure of this security property is called a “denial-of-service for blockspace attack” (aka “blockspace DoS”). Two example attacks illustrate different attack approaches: in one case, an attacker has enough mining capacity to exclude all transactions (except perhaps their own); in another approach an attacker pays fees higher than any legitimate user for so many transactions that any other user cannot effectively get any of their transactions included.

Finality Progress

Blocks become final or they are removed from the chain within a finite amount of time. A failure of “finality progress” is called a “finality stall attack”. This is subtly distinct from a general liveness failure: a finality stall may occur even while new blocks containing transactions are continually produced. The longer that finality stalls while new blocks arrive with new transactions, the more likely it is that those users who require finality and those users who do not rely on finality will diverge in their expectations and behavior, which is a growing economic and governance risk, so finality stalls may be especially pernicious.

Censorship-resistance

It is possible to get new transactions processed even in the presence of an adversary who tries to prevent those specific transactions. Failure of this security property is called “censorship attack”. This kind of attack is distinct from blockspace DoS attacks because of the narrower targeting policy. In practice more general DoS attacks use different techniques than more targeted censorship.

Broadly speaking, an adversary may have a “censorship policy” based on a variety of criteria including both on-chain behavior and correlated metadata from many different domains.

Because censorship (and other privacy attacks) often rely on a wide array of data sources, practical protection also relies on a wide array of techniques and technologies out of scope for Crosslink’s design. One key area where we assume supporting defensive technologies (such as mixnets) is around network privacy for wallets (especially) and potentially other Crosslink infrastructure.

Supply-integrity

The total supply of ZEC is correct and any user can verify that it is correct. Failure of this security property is called “counterfeiting attack”.

TODO: Where does the following live?

What is the difference between liveness and censorship-resistance? The difference is whether specific transactions are targeted (a censorship attack) or (a stall attack). An important fact is that a stall attack would be immediately noticed and a wide set of users would be able to agree that the stall attack is happening. In contrast, a censorship attack would tend to go unnoticed except by the victims, and it might be difficult to achieve widespread recognition that it had happened. For this reason, part of the design of Crosslink is intended to “convert censorship attacks into stall attacks” – make it impossible for an attacker to censor targeted transactions without causing the entire service to stall.

The Five Component Model

There are five components of the system. Each component is responsible for preventing certain attacks, or for holding other components accountable.

Wallets

The job of the wallet is to protect a user’s funds and to enable sending or receiving funds safely.

When receiving funds, the wallet verifies that the incoming funds total to a specific amount, safe against rollbacks, and available to be respent in the future. Additionally, wallets that prioritize user privacy often ensure all incoming funds become shielded to protect the user against unintentional on-chain privacy leaks.

When sending funds, the wallet minimizes all information leakage except those details a user explicitly requests to disclose to certain parties, or those details which must be disclosed. Zcash relies on strong encryption for all information where possible given a transaction type. Privacy is also a protection against censorship, since a censor must either identify specific transactions to censor, or perform blanket or probabilistic censorship in a less effective manner. However, some information disclosures or leakages are inevitable:

• Some information disclosures are always necessary for certain transactions:
• The amount, timing, and memo always needs to be disclosed to the recipient.
• The recipient’s receiving address is always known to a sender.
• Some other kinds of transactions require that some of the information is disclosed to specific parties or to the public in order to achieve certain kinds of desirable transparency. Examples include coin-voting, bridges/DEXes/L2’s, CEXes, turnstile migrations, t-addresses for backward compatibility, staking, unstaking, and redelegating.
• Some information “leakage” occurs even when not theoretically necessary for a given kind of transaction, especially by correlation with off-chain activity, such as:
• The recipient will often know something about the sender’s relationship with them, may be able to learn the sender’s IP address, etc. Therefore if the recipient colludes with the attacker, encryption cannot entirely protect against censorship by itself.
• It is also the responsibility of the wallet to protect the user against censorship attacks that leverage network-level information leakage. Wallets can and should use network-level protections against information leakage such as Tor or Nym.

Miners

The job of the miners is to include transactions and advance the blockchain, which provides an additional kind of censorship-resistance, in addition to the kind of censorship-resistance provided by wallets encrypting the transaction contents when possible. This function of miners also provides liveness. However the miners cannot unilaterally violate finality, even if an attacker controls >½ of the hashpower, because the finalizers ensure finality regardless of the behavior of the miners. A majority of the miners (>½ of the hashpower) can violate censorship-resistance (except when it can be provided by the wallet with encryption).

Finalizers

The job of the finalisers is to ensure finality (i.e. to prevent rollback attacks) but finalisers cannot unilaterally compromise liveness or censorship-resistance (even if an attacker controls >⅔ of the stake-weighted votes) because miners ensure those properties. Also the finalisers cannot unilaterally execute rollback attacks even though they can prevent rollback attacks. A plurality of the finalisers (controlling >⅓ of the stake-weighted votes) could execute stall attacks (i.e. violate liveness).

Stakers

It is the job of the stakers to hold the finalisers accountable by detecting and punishing misbehavior on the part of the finalizers by redelegating stake away from ill-behaved finalizers to well-behaved finalizers.

Users

It is the duty of the users, collectively, to hold the stakers accountable for doing their job. If the stakers fail in their duty to hold the finalizers accountable, they can be disempowered and punished for this failure by the users with an emergency user-led hard fork (which is what happened in the STEEM/HIVE hard fork). We clarify how we envision this could work with more safety and preparedeness by the Zcash community in the User-Led Emergency Hardforks.

Attacker Resource Scenarios

When considering these components, it is useful to consider scenarios where an attacker has compromised some portion of each kind of component, as a coarse means of assessing the robustness of Crosslink in maintaining the security properties.

• A collusion that controlled both >½ of the hashpower and >⅔ of the stake.

• ...could violate finality.

• A collusion that included both a majority of the miners (controlling >½ of the hashpower) and a supermajority of the finalizers (controlling >⅔ of the stake-weighted votes)

• ...could execute rollback and unavailability attacks.

Censorship-resistance is necessary for stakers to stake, unstake, and redelegate, which means censorship-resistance is necessary for stakers to be able to perform their duty of holding the finalizers accountable. Therefore, if an attacker controls >½ of the hashpower (and is thereby able to censor), then the attacker can prevent the stakers from holding the finalizers accountable.

An important and under-investigated consideration is what security properties hold when an attacker controls a minority of the hashpower. In a pure-PoW system, an attacker that controls some hashpower but ≤½ of it can not completely censor transactions, but can force them to be delayed.

• A collusion that controls >⅔ of the stake and <½ of the hashpower.

User-Led Emergency Hardforks

In The Five Component Model we describe a key role of users is their governance capability to initiate a user-led hardfork in the event of an emergency.

In the context of Crosslink, we believe it's beneficial to gain community agreement on a norm for when such emergency hardforks are called for. Having an up-front agreement can help reduce confusion, debate, or contention during specific kinds of emergencies.

A Proposed Governance ZIP for the Use of an Emergency User-Led Hard Fork to Correct Layer-1 Security Failures

An emergency user-led hard fork is an extraordinary intervention that reflects a core value of cryptocurrencies: the ability of users to assert sovereignty over the protocol in response to a failure of its most fundamental security guarantees. This form of intervention is distinct from ordinary network upgrades, which change consensus rules prospectively and only with broad user acceptance. Because an emergency user-led hard fork carries significant social, economic, and political consequences, the Zcash community should establish a clear and limited social consensus in advance about when it is legitimate.

This Governance ZIP establishes that a user-led hard fork should be considered only to rectify and hold consensus operators accountable for failures of the layer-1 consensus system itself, specifically failures to prevent rollback or double-spend attacks, failures to ensure network liveness or availability, and failures to ensure censorship resistance or freedom of participation, including situations in which would-be miners, finalizers, or stakers are being systematically censored or prevented from participating in block production, finalization, or staking. These grounds are intended to capture violations of finality, liveness, and censorship resistance at the base layer and define the exclusive scope of legitimate emergency intervention under this framework.

This Governance ZIP explicitly rejects the use of an emergency user-led hard fork to mitigate harm arising from application-layer failures or to alter outcomes that, while undesirable, do not constitute violations of layer-1 security properties. It does not apply to wallet bugs, smart contract failures, bridge exploits, custodial failures, key management errors, user mistakes, or other application-level attacks or economic losses. A user-led hard fork must not be used to reverse or “make whole” thefts or hacks, to rewrite application-layer outcomes, or for purposes analogous to Ethereum’s DAO hard fork, the SUI blockchain hard fork, or similar interventions motivated by dissatisfaction with economic outcomes rather than base-layer security failure. Control over a large share of hashpower, finalization power, or stake does not itself constitute a violation, and a user-led hard fork must not be used to disadvantage miners, finalizers, or stakers solely for being large, nor to resolve governance disputes or enforce social policy outcomes.

This Governance ZIP also does not apply to ordinary prospective rule changes adopted through standard upgrade processes, including the introduction of new transaction types, new features, or protocol cleanups. It does not apply to monetary policy, economic parameters, or protocol design choices such as shielded pool deprecations, fee changes, new fee mechanisms, staking or unbonding parameters, or funding mechanisms. All such matters fall within the domain of future community governance and must be decided through ordinary governance and network upgrade processes, not through an emergency user-led hard fork justified under this security framework.

Even when one of the legitimate layer-1 security grounds is clearly met, any emergency user-led hard fork should be narrowly scoped to address only the specific security failure, avoid unnecessary collateral changes, minimize downstream disruption, and preserve continuity of honest user state where technically feasible. Possible interventions may include correcting a critical consensus bug, changing a security-critical consensus mechanism that failed to prevent the violation, or, where directly relevant, neutralizing counterfeit or illegitimate base-layer state created by the failure. The objective of such intervention is the restoration of neutral protocol function, not broad protocol re-engineering under crisis conditions.

This Governance ZIP is a proposed expression of social consensus. Its force derives solely from the degree to which the Zcash community chooses to adopt and uphold it. Whether any particular emergency intervention is ultimately acceptable will depend not only on technical criteria, but also on whether it aligns with the community’s explicit or assumed social values. By committing to these constraints in advance, the community strengthens credible neutrality, reduces moral hazard, and increases confidence that the protocol will not be arbitrarily rewritten.

Crosslink Design in a Nutshell

This chapter covers the major components of the design. This presents the design positively, without rationales, trade-offs, safety anlyses, or other supporting information. This will eventually be entirely redundant with, or simply link to, a canonical Zcash Improvement Proposal submission. Treat this chapter as a provisional sketch.

It assumes and leverages familiarity with Zcash PoW and only describes new differences from today's mainnet.

CAVEATS: A lot of the terminology and descriptions will be adjusted as we go to follow conventions and specifications in the Zcash Protocol Specification and the Zcash Improvement Proposals.

Roles and Capabilities

We rely on several roles described in the Five Component Model in this nutshell section along with their intended capabilities. The absence of an explicit capability description for a role implies that role should not be able to perform that capability

Changes to Transactions

Changes to the Coinbase Transaction

The coinbase transaction is an exceptional transaction Zcash inherited from Bitcoin which follows exceptional rules, including the distribution of newly issued tokens. This transaction is created by a block's miner.

The consensus rules are updated to require this transaction to make transfers of a portion of newly issued ZEC dedicated to Crosslink rewards only when this block updates finality to a greater height, and then as the sum of all pending finalization rewards since the previous finalization.

For each block produced which does not update finality, the per-block Crosslink rewards are collected into a running total, and a block which updates finality must then distributed this entire pending amount to the stakers and finalizers determined from the active set used to produce the finality update.

The pending finalizaiton rewards, $R$, in a block which updates finality must be distributed by the coinbase transaction to finalizers and stakers proportionally to their reward slice, $S_{participant}$, where the active set (defined below) refers to the state as of the most recent final block, prior to this update.

This is calculated as follows where we let $W_{participant}$ be the total stake weight for that participant:

• For finalizers in the active set: $S_{finalizer}=COMMISSIO{N}_{F}E{E}_{R}ATE\ast \frac{W_{finalizer}}{W_{t}otal}$

  The constant $COMMISSIO{N}_{F}E{E}_{R}ATE=0.1$ is a fixed protocol parameter called the commission fee rate.

• For all stakers: $S_{staker}=(1.0-COMMISSIO{N}_{F}E{E}_{R}ATE)\frac{W_{staker}}{W_{t}otal}$

  The constant $1.0-COMMISSIO{N}_{F}E{E}_{R}ATE=0.9$ is called the staker reward rate.

  Note that $W_{staker}$ is the total weight of all staking positions of the given staker regardless of whether or not it is assigned to an finalizer in the active set.

Another nuance: the sum of all commission fees and staker rewards adds up to $S_{t}otal$ or less, with the difference coming from stake assigned to finalizers outside the active set.

New Transaction Format & Staking Actions

A new transaction format is introduced which contains a new optional field for staking actions, which enable operations such as staking ZEC to a finalizer, beginning or completing an unstaking action, or redelegating an existing staking position to a different delegator.

The ZEC flowing into staking actions, or flowing out of completing unstaking transactions must balance as part of the transactions chain value pool balancing. See The Zcash Protocol §4.17 Chain Value Pool Balances.

Additionally, we introduce a new restricting consensus rule on context-free transaction validity¹:

Crosslink Staking Orchard Restriction:

A transaction which contains any staking actions must not contain any other fields contributing to or withdrawing from the Chain Value Pool Balances except Orchard actions, explicit transaction fees, and/or explicit ZEC burning fields.

Abstractly, the staking actions include:

• _stake - This creates a new staking position assigning a transparent ZEC amount, which must be a power of 10, to a finalizer and including a cryptographic signature verification key intended for only the signing-key holder of the position to redelegate or unstake.
• redelegate - This identifies a specific staking position, a new finalizer to reassign to, and a signature valid with the position's published verification key to authorize the transition.
• unbond - This initiates an "unbonding process" which puts the staking position into an unbonding state and includes the ZEC amount, the current block height, and the signature verification key to authorize a later claim. Once in this state, redelegations are not valid and the ZEC amount does not contribute to staking weight for finalizers or the staker.
• claim - This action removes a position in the unbonding state and contributes the bonded ZEC into the transaction's Chain Value Pool Balance, where because of the "Crosslink Staking Orchard Restriction, it may only be distributed into an Orchard destination and/or transaction fees.

Further Restrictions on Staking Actions

We furthermore introduce the following consensus rule restrictions on transactions involving staking actions which rely on a staking epoch design:

Staking Epoch Definition:

Once Crosslink activates at block height $H_{crosslin{k}_{a}ctivation}$, staking epochs begin, which are continguous spans of block heights with two phases: staking day and the locked phase. The number of blocks for staking day is a protocol parameter constant roughly equivalent to 24 hours given assumptions about the Difficulty Adjustment Algorithm. The number of blocks for the locked phase is also a constant roughly equivalent to 6*24 hour periods, so that staking day is approximately one day per week.

Given the staking epoch definition, we introduce the following restrictions in the consensus rules:

Locked Staking Actions Restriction:

If a transaction includes any staking actions except for redelegate, and that transaction is in a block height in a locked phase of the staking epoch, then that block is invalid.

Also:

Unbonding Delay:

If a transaction is block height $H$ includes any claim staking actions which refer to unbonding state positions which have not existed in the unbonding state for at least one full staking epoch, that block is invalid.

Note: An implication of the Unbonding Delay is that the same staking day cannot include both an unbond and claim for the same position.

A final restriction (already mentioned above in introducing the staking action is:

Stake Action Amount Quantization:

If a transaction includes any staking actions with an amount which is not a power of 10 ZEC (or ZAT), that transaction is invalid.

Changes to Ledger State

The Ledger State is a conceptual and practical data structure which can be computed by fully verifying nodes solely from the sequence of blocks starting from the genesis block.² To this Ledger State, Crosslink introduces the roster which is a table containing all of the information about all ZEC staked to finalizers.

The Roster

Crosslink's addition to Ledger State is embodied in the PoS roster, aka the roster for short. Which tracks staking positions created by Stakers, and attached to specific Finalizers. A Finalizer has a "voting weight" equal to the sum of all staking positions attached to it (see below in FIXME).

Each staking position is composed of at least a single specific target finalizer verification key, a staked ZEC amount, and a unstaking/redelegation verification key. The finalizer verification key designates a cryptographic signature verification key which serves as the sole on-chain reference to a specific finalizer³. People may mean a specific person, organization, entity, computer server, etc... when they say "finalizer", but for the rest of this document we will use the term finalizer as a shorthand for "whichever entity controls the verification key for a given finalizer verification key.

The unstaking/redelegation verifying key enables unstaking or redelegating that position from the participant that created that position (or more precisely anyone who controls the associated verifying key, which should be managed by a good wallet on behalf of users without their need to directly know or care about these keys for safe operation). These are unique to the position itself (and not linked on-chain to a user's other potential staking positions or other activity).

The sum of outstanding staking positions designating a specific finalizer verification key at a given block height is called the stake weight of that finalizer. At a given block height the top K (currently 100) finalizers by stake weight are called the active set of finalizers.

Ledger State Invariants

We adopt a design invariant around the Ledger State changes Crosslink makes against mainnet Zcash:

General Ledger State Design Invariant:

All changes to Ledger State can be computed entirely from (PoW) blocks, transactions, and data transitively referred to by such. This includes all existing Ledger State in mainnet Zcash today, the PoS and BFT roster state (see below), and the finality status of blocks and transactions.

All current mainnet Zcash Ledger State and almost all Crosslink Ledger State is height-immediate Ledger State: the value for height $H$ can be computed from height $H$ itself (and implicitly all prior heights and contents). Some examples of height-immediate values are the total ZEC issued, the UTXOs spendable by the same P2PKH t-addr, the block's zero-knowledge commitment anchor values, and so on. In Crosslink examples include all of the roster state (e.g. the active set, finalizer verification keys, staking positions, ...).

Height-Eventual Ledger State

Crosslink introduces a novel category of Ledger State not present in Zcash mainnet, which is height-eventual Ledger State. This is a property or value about height $H$ which is only computable at a later larger height (of which the implicit block at $H$ must be an ancestor). The sole example of this is finality status.

The finality status of a block at height $H$ (and by extension any transactions it contains and all previous block contents) is a property which guarantees[^guarantees] to the verifying node that this block (and all txns and previous content) is final and cannot be reverted or rolled back. Furthermore, the presence of this property also provides a guarantee that a majority of finalizers already agree on the finality status of this block and also that all verifying nodes which see a sufficient number of subsequent blocks will also agree on the finality status.

[^guarantees] In this book, whenever we say a protocol "guarantees" some condition, we mean that so long as the security assumptions truly hold verifying nodes can and should safely rely on that condition.

The finality status of a block at height $H$ (which we'll call a finality-candidate block here for precision) is computable from a block at a later height $>H$ (which we'll call the attesting block). All verifying nodes who have observed the that attesting block will agree on the finality of the candidate block even though they may observe the attesting block rollback. In the event of such a rollback, the protocol guarantees that an alternative block will eventually attest to the finality status of the same candidate block.

Finality, Transaction Semantics, Ledger State, and the Roster

It bears pointing out a nuance: the Ledger State, including the Roster and the Active Set are all determined by valid transactions within PoW blocks. Every PoW block height thus has a specific unambiguous Ledger State. This comes into play later when we consider finality which is a property of a given block height which is only verifiable at a later block height.

The BFT Sub-Protocol

TODO: Flesh out this section

TODOS from deep dive:

• rewards distribution to stakers and finalizers requires changes to the Coinbase transaction.
• how finality status is calculated
• how BFT operates, votes, network, etc...
• active set selection
• quantization of amounts / time
• the power of 10 restriction on amount is only applied to "stake" (create position)
• how do staking actions pay fees?

1. A context-free transaction validity check may be performed on the bytes of the transaction itself without the need to access any chain state or index. ↩

2. Theoretically all of the Ledger State could be purely computed on demand from prior blocks, so literal Ledger State representations in memory can be thought of as chain indices or optimizing caches for verifying consensus rules. In some cases components of the Ledger State must be committed to within the blockchain state itself (for example, commitment anchors) which constrains how lazy a theoretical implementation can be. Real implementations trade off caching vs lazy-computation in a fine-grained way to achieve practical goals. ↩

3. Any particular entity may produce any number of finalizer verifying keys of course, although for economic or social reasons, we expect many finalizers to be motivated to hang their reputation on 1 or just a few well-known finalizer verifying keys. ↩

Terminology

Here we introduce terminology specific to this design, especially when it may deviate from other consensus systems or common terminology used in the consensus protocol field.

Crosslink Finality

Crosslink provides a kind of finality which we call crosslink finality. Crosslink finality has these properties:

• It is accountable because the chain contains explicit voting records which indicate each participating finalizer's on-chain behavior.
• It is irreversible within the protocol scope. The only way to "undo" a final block is to modify the software to do so, which requires intervention by the user. Note that because a finality safety violation is always theoretically possible, this implies the only recovery from such a violation is out-of-band to the protocol and requires human intervention.
• It is objectively verifiable because it is possible to determine finality from a local block history without any out-of-band information.
• It is globally consistent meaning that all nodes which have received a sufficient number of valid blocks agree on the finality status, and also can rely on all other nodes in this set arriving at the same conclusion.
• It provides asymmetric cost-of-attack defense (TODO: Describe this better.)

The Crosslink 2 Construction

We are now ready to give a description of a protocol that takes into account the issues described in Notes on Snap‑and‑Chat, and that implements bounded availability. We call this the “Crosslink” construction; more precisely the version described here is “Crosslink 2”.

This description will attempt to be self-contained, but [NTT2020] (arXiv version) is useful background on the general model of Ebb-and-Flow protocols.

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.

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.

Times are modelled as values of a totally ordered type $\mathsf{Time}$ with minimum value $0$. For convenience, we consider all protocol executions to start at time $0$.

A “$\ast$‑node” is a participant in ${\Pi }_{\ast }$ (the protocol may be implicit). A $\ast$‑node is “honest at time $t$” in a given execution iff it has followed the protocol up to and including time $t$ in that execution.

A time series on type $U$ is a function $S⦂\mathsf{Time}\to U$ assigning a value of $U$ to each time in an execution. By convention, we will write the time $t$ as a superscript: $S^t=S(t)$.

A $\ast$‑chain is a nonempty sequence of $\ast$‑blocks, starting at the “genesis block” ${\mathcal{O}}_{\ast }$, in which each subsequent block refers to its preceding or “parent block” by a collision‑resistant hash. The “tip” of a $\ast$‑chain is its last element.

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 is exactly one $\ast$‑chain corresponding to a $\ast$‑block; and conversely there is exactly one $\ast$‑block at the tip of a $\ast$‑chain.

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

The block at depth $k\in \mathbb{N}$ in a $\ast$‑chain $C$ is defined to be the tip of $C{\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$ (this also applies when $\mathsf{len}(C)\le k$ because the genesis $\ast$‑chain cannot roll back).

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”. This also includes the case $B=C$.
• The notation $B/⪯{⪰}_{\ast }C$ means that both $B/{⪯}_{\ast }C$ and $C/{⪯}_{\ast }B$. That is, “neither of $B$ and $C$ is a prefix of the other”.

A function $S⦂I\to \ast \text{-block}$ is $\ast$‑linear iff for every $t,u⦂I$ where $t\le u$ we have $S(t){⪯}_{\ast }S(u)$. (This definition can be applied to time series where $I=\mathsf{Time}$, or to sequences of $\ast$‑blocks where values of $I$ are indices.)

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

$\text{TODO:}$ remove this if not used:

We 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”.

Views

In the simplest case, a block‑chain protocol ${\Pi }_{\ast }$ provides a single “view” that, for a given $\ast$‑execution, provides each $\ast$‑node with a time series on $\ast$‑chains. More generally a protocol may define several “views” that provide each $\ast$‑node with time series on potentially different chain types.

We model a $\ast$‑view as a function $V⦂\mathsf{Node}\times \mathsf{Time}\to \ast \text{-chain}$. By convention, we will write the node index $i$ as a subscript and the time $t$ as a superscript: $V_i^t=V(i,t)$.

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 changing the specified behaviour of honest nodes.

A Crosslink 2 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 2 nodes.

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

A $\ast$bft‑node’s view 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.

We extend the ${\lceil }^k$ notation to $\ast$bft‑proposals in the obvious way: if $k\ge 1$, $P$ is a $\ast$bft‑proposal and $B$ its parent $\ast$bft‑block, then $P{\lceil }_{\ast \mathrm{bft}}^k:=B{\lceil }_{\ast \mathrm{bft}}^{k-1}$.

For each epoch, there is a fixed number of voting units distributed between the $\ast$bft‑nodes, 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.

Note that a unit should be considered to be cast non-honestly in the case of key compromise, because it is then effectively under the control of an adversary. The key compromise may or may not be attributable to another flaw in the protocol, but such a flaw would not be a break of the consensus mechanism per se.

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 2 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. As previously mentioned, 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.

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}(H{\lceil }_{\ast \mathrm{bc}}^1)<\mathsf{score}(H)$ for any non‑genesis $\ast$bc‑valid‑chain $H$.

Unless an adversary is able to censor knowledge of other chains from a 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 its previous $\ast$bc‑best‑chain.

Let $\mathsf{ch}$ be a view such that ${\mathsf{ch}}_i^t$ is node $i$’s $\ast$bc‑best‑chain at time $t$. (This matches the notation used in [NTT2020].) We define ${\mathsf{ch}}_i^0$ to be ${\mathcal{O}}_{\mathrm{bc}}$.

A $\ast$bc‑valid‑block is assumed to commit to a collection (usually, a sequence) of $\ast$bc‑transactions. Unlike in Crosslink 1 or Snap-and-Chat, we do not need to explicitly model $\ast$bc‑transaction validity or impose any additional constraints on it. The consensus rules applying to $\ast$bc‑transactions are entirely unchanged, including any rules that depend on $\ast$bc‑block height or previous $\ast$bc‑blocks. This is because Crosslink 2 never reorders or selectively “sanitizes” transactions as Snap-and-Chat does. If a bc‑block is included in a Crosslink 2 block chain then its entire parent bc‑block chain is included just as it would have been in ${\Pi }_{\mathrm{origbc}}$ (only modified by the structural additions described later), so block heights are also preserved.

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 2, 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:

Definition of Crosslink 2

Parameters

Crosslink 2 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 chain $\mathsf{fin}{}_i^t⦂\text{bc-valid-chain}$. Unlike in Snap‑and‑Chat or Crosslink 1, this is just a block chain; because we do not need sanitization, there is no need to express it as a log of transactions rather than blocks.

Each node $i$ chooses a potentially different bc‑confirmation‑depth $\mu \in \mathbb{N}$ where $0<\mu \le \sigma$ to obtain its view of the bounded‑available ledger at time $t$, $({\mathsf{ba}}_{\mu }{)}_i^t⦂\text{bc-valid-chain}$. (We make the restriction $\mu \le \sigma$ because there is no reason to choose a larger $\mu$.)

Stalled Mode

Consider, roughly speaking, the number of bc‑blocks that are not yet finalized at time $t$ (a more precise definition will be given in the section on ${\Pi }_{\mathrm{bc}}$ changes from ${\Pi }_{\mathrm{origbc}}$). 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 take to be finalized after being included in a bc‑block (if they are finalized at all) just prior to time $t$.

As explained in detail by The Arguments for Bounded Availability and Finality Overrides, if this bound exceeds a threshold $L$, then it likely signals an exceptional or emergency condition, in which it is undesirable to keep accepting user transactions that spend funds into new bc‑blocks. In practice, $L$ should be at least $2\sigma$.

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

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

In practice a node's view of the finalized chain, $\mathsf{fin}{}_i^t$, is likely to lag only a few blocks behind ${\mathsf{ba}}_{i,\sigma }^t$ (depending on the latency overhead imposed by ${\Pi }_{\mathrm{bft}}$), unless the chain has entered Stalled Mode. So when $\mu =\sigma$, the main factor influencing the choice of a given application to use $\mathsf{fin}{}_i^t$ or $({\mathsf{ba}}_{\mu }{)}_i^t$ is not the average latency, but rather the desired behaviour in the case of a finalization stall: i.e. stall immediately, or keep processing user transactions until $L$ blocks have passed.

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

For a bft‑block or bft‑proposal $B$, define $$\begin{array}{rl}\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}\end{array}$$ For a bc‑block $H$, define $$\begin{array}{rl}\mathsf{LF}(H)& :=\text{bft-last-final}(H.context\_bft)\\ \mathsf{candidate}(H)& :=\text{last-common-ancestor}(\mathsf{snapshot}(\mathsf{LF}(H)),H{\lceil }_{\mathrm{bc}}^{\sigma })\end{array}$$

When $H$ is the tip of a node’s bc‑best‑chain, $\mathsf{candidate}(H)$ will give the candidate finalization point, subject to a condition described below that prevents local rollbacks.

Locally finalized chain

Each node $i$ keeps track of a “locally finalized” bc‑chain $\mathsf{fin}{}_i^t$ at time $t$. Each node’s locally finalized bc‑chain starts at $\mathsf{fin}{}_i^0={\mathcal{O}}_{\mathrm{bc}}$. However, this chain state should not be exposed to clients of the node until it has synced.

When node $i$’s bc‑best‑chain view is updated from ${\mathsf{ch}}_i^s$ to ${\mathsf{ch}}_i^t$, the node’s $\mathsf{fin}{}_i^t$ will become $\mathsf{candidate}({\mathsf{ch}}_i^t)$ if and only if this is a descendant of $\mathsf{fin}{}_i^s$. Otherwise $\mathsf{fin}{}_i^t$ will stay at $\mathsf{fin}{}_i^s$. This guarantees Local finalization linearity by construction.

If when making this update, $\mathsf{candidate}({\mathsf{ch}}_i^t)/⪯⪰\mathsf{fin}{}_i^s$ (i.e. $\mathsf{candidate}({\mathsf{ch}}_i^t)$ and $\mathsf{fin}{}_i^s$ are on different forks), then the node should record a finalization safety hazard. This can only happen if global safety assumptions are violated. Note that Local finalization linearity on each node is not sufficient for Assured Finality, but it is necessary.

This can be expressed by the following state update algorithm, where $s$ is the time of the last update and $t$ is the time of the current update:

$$\begin{gathered} \text{update-fin}(\text{mut }\mathsf{fin}{}_i,{\mathsf{ch}}_i^t,s): \\ \text{let }N=\mathsf{candidate}({\mathsf{ch}}_i^t) \\ \text{if }N⪰\mathsf{fin}{}_i^s\text{:} \\ \mathsf{fin}{}_i^t\leftarrow N \\ \text{else:} \\ \mathsf{fin}{}_i^t\leftarrow \mathsf{fin}{}_i^s \\ \text{if }N/⪯\mathsf{fin}{}_i^s\text{:} \\ \text{record finalization safety hazard} \end{gathered}$$

A safety hazard record should include ${\mathsf{ch}}_i^t$ and the history of $\mathsf{fin}{}_i$ updates including and since the last one that was an ancestor of $N$.

Assured Finality is our main safety goal for Crosslink 2. It is essentially the same goal as Final Agreement but applied to nodes’ locally finalized bc‑chains; intuitively it means that honest nodes never see conflicting locally finalized chains. We intend to prove that this goal holds under reasonable assumptions about either ${\Pi }_{\mathrm{origbft}}$ or ${\Pi }_{\mathrm{origbc}}$.

Note that if an execution of Crosslink 2 has Assured Finality, then all nodes that are honest for that execution have Local finalization linearity. That is because the restriction of Assured Finality to the case $i=j$ is equivalent to Local finalization linearity for node $i$ up to any time at which node $i$ is honest.

Locally bounded‑available chain

Define the locally bounded‑available chain on node $i$ for bc‑confirmation‑depth $\mu$, as $$({\mathsf{ba}}_{\mu }{)}_i^t=\{\begin{array}{ll}{\mathsf{ch}}_i^t{\lceil }_{\mathrm{bc}}^{\mu },& \text{if }\mathsf{fin}{}_i^t⪯{\mathsf{ch}}_i^t{\lceil }_{\mathrm{bc}}^{\mu }\\ \mathsf{fin}{}_i^t,& \text{otherwise.}\end{array}$$

Like the locally finalized bc‑chain, this chain state should not be exposed to clients of the node until it has synced.

Our security goal for ${\mathsf{ba}}_{\mu }$ will be Agreement on ${\mathsf{ba}}_{\mu }$ as already defined.

Syncing and checkpoints

It is recommended that node implementations “bake in” a checkpointed bft‑block $B_{\mathsf{checkpoint}}$ to each released version, and that node $i$ should only expose $\mathsf{fin}{}_i^t$ and $({\mathsf{ba}}_{\mu }{)}_i^t$ to its clients once it is “synced”, that is:

• $B_{\mathsf{checkpoint}}{⪯}_{\mathrm{bft}}\mathsf{LF}({\mathsf{ch}}_i^t)$;  and
• $\mathsf{snapshot}(B_{\mathsf{checkpoint}}){⪯}_{\mathrm{bc}}\mathsf{fin}{}_i^t$;  and
• the timestamp of $\mathsf{fin}{}_i^t$ is within some threshold of the current time.

Π_bft changes from Π_origbft

Π_bft proposal and block validity

Genesis bft‑block rule: ${\mathcal{O}}_{\mathrm{bft}}$ is bft‑block‑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$.
• Linearity rule: $\mathsf{snapshot}(B{\lceil }_{\mathrm{bft}}^1){⪯}_{\mathrm{bc}}\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 Linearity 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

Π_bc block validity

Genesis bc‑block 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)$.
• Last Final Snapshot rule: $\mathsf{snapshot}(\mathsf{LF}(H)){⪯}_{\mathrm{bc}}H$.
• Finality depth rule: Define: $$\text{finality-depth}(H):=\mathsf{height}(H)-\mathsf{height}(\mathsf{snapshot}(\mathsf{LF}(H)))$$ Then either $\text{finality-depth}(H)\le L$ or $\text{is-stalled-block}(H)$.

Π_bc contextual validity

The consensus rule changes above are all non-contextual. Modulo these changes, contextual validity in ${\Pi }_{\mathrm{bc}}$ is the same as in ${\Pi }_{\mathrm{origbc}}$.

Π_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 stalled block if required to do so by the Finality depth rule.

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)))$, and if there is still a tie then by taking $C$ with the smallest hash.

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

For discussion of potentially unifying the roles of bc‑block producer and bft‑proposer, see What about making the bc‑block‑producer the bft‑proposer? in Potential changes to Crosslink.

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

Penalty for Failure to Defend

TODO: This is a paste of a Github ticket Add "penalty-for-failure-to-defend" concept to book #264 in order to ensure the text is committed into the revision.

Our primary conceptual framework for quantitative comparison between Crosslink security properties versus pure PoW or Tendermint-like BFT protocols is called "penalty for failure to defend" (aka $PFD$).

Key Top-Level Details

• PFDs can be specific to compromising specific properties; example: $PF{D}_{liveness}$ and $PF{D}_{finality}$ are different (so there's no simple top-line number for a given protocol).
• $PFD$ is distinct from the confusing misnomer of "cost-to-attack" (because the penalty may accrue to non-attackers, and the nature of successful attacks is that they cost less than designers or security defense analyzers fail to anticipate).
• Neither $PFD$ or the ill-conceived "cost-to-attack" metrics are conclusive about financial feasibility, since they don't capture attacker revenue/profit.
• Some $PFD$ may be a "financial value gauge" such as in Tendermint protocols where a $PFD$ could slash a large bond at stake. Meanwhile others may be a "rate" such as in PoW where the penalty to miners is loss of a future revenue rate over time.
• The two different types of $PFD$ (gauge vs rate) cannot be directly compared for two reasons:
  • The obvious reason that rates and gauges are different unit types.
  • The less obvious reason that the trade-offs in compromise, response, and recovery dynamics are qualitatively incommensurate. (TODO: flesh out the nuance here.)

Security Analysis of Crosslink 2

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

Liveness argument

First note that Crosslink 2 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 2 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 2 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-stalled-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 bc‑block rule doesn’t apply to new bc‑blocks.
• The Valid context rule, Extension rule, and Last Final Snapshot 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 stalled 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 Linearity 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 Linearity 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 ${\Pi }_{\mathrm{origbft}}$.

The only other possibility for a liveness issue in Crosslink 2 would be if the change to the constructions of $\mathsf{fin}{}_i$ or $({\mathsf{ba}}_{\mu }{)}_i$ could cause either of them to stall, even when ${\Pi }_{\mathrm{bft}}$ and ${\Pi }_{\mathrm{bc}}$ are both still live.

However, liveness of ${\Pi }_{\mathrm{bft}}$ and the Linearity 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. $\text{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.

Finally, we need to show that Stalled 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. $\text{TODO:}$ more detailed argument needed, especially for the dependence on $L$.

Safety argument

$\text{TODO:}$ Not updated for Crosslink 2 below this point.

Discussion

Recall the definition of Assured Finality.

First we prove that Assured Finality is implied by Prefix Agreement of ${\Pi }_{\mathrm{bc}}$.

Then we prove that Assured Finality is also implied by Final Agreement of ${\Pi }_{\mathrm{bft}}$.

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:

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

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]))\\ \text{fin}& ⦂& \text{bc-block}\to [\text{bc-chain}]\\ \mathrm{fin}(H)& :=& [\mathsf{snapshot}(B)\text{ for }B{⪯}_{\mathrm{bft}}\mathsf{LF}(H{\lceil }_{\mathrm{bc}}^{\sigma })]\\ \text{fin-ctx}(H)& :=& \text{san-ctx}(\mathrm{fin}(H))\\ \text{ba-ctx}(H,\mu )& :=& \text{san-ctx}(\mathrm{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{ba},\mu ,i}^t& :=& \text{context-txns}(\text{ba-ctx}({\mathsf{ch}}_i^t,\mu ))\end{array}$$