Potential Changes to Crosslink
This page documents suggestions that have not had the same attention to security analysis as the Crosslink 2 construction. Some of them are broken. Some of them also increase the complexity of the protocol (while some simplify it or have a mixed effect on complexity), and so we need to consider the security/complexity trade‑off of each suggestion before we could include it.
This page has not yet been updated for the changes from Crosslink 1 to Crosslink 2.
Attempts to improve safety or to simplify the protocol
[Recommended] Recording more info about the bft‑chain in bc‑blocks
We can allow honest bc‑block‑producers to record information about every proposed and notarized bft‑block, rather than just the one in the field.
Duplicate information that has already been given in an ancestor bc‑block would be omitted.
This would automatically expose the following shenanigans to public view (as long as enough bc‑block‑proposers are honest, which is already assumed):
- any attempt to double‑propose in the same epoch;
- any successful attempt to double‑notarize.
We could also expose attempts to double‑vote.
Note that double‑proposal and double‑voting could be a sign that a proposer or validator’s private key is compromised, rather than that it belongs to the adversary per se. However, the security analysis must treat such a proposer/validator as non‑honest in any case.
Changing the Increasing Score rule to require the score of the tip (rather than the score of the snapshot) to increase
The current Increasing Score rule concerns the score of the snapshot:
Increasing Snapshot Score rule: Either or .
We could instead require the score of to increase:
Increasing Tip Score rule: Either or .
Pros:
- This more directly reflects the fork‑choice rule in .
- In Crosslink 1, an honest bft‑proposer uses its bc‑best‑chain tip with the highest score provided that it is consistent with the Increasing Snapshot Score rule. This change removes the caveat, simplifying honest bft‑proposer behaviour.
- As a result of removing that caveat, we always know about an honest bft‑proposer’s bc‑best‑chain.
Con:
- The score of the snapshot would not necessarily increase. As a result, it is technically possible that the new snapshot can be an ancestor of a previous snapshot. Whether this can actually happen depends on the value of and the difficulty adjustment rule. This causes no particular harm other than adding a corner case in ledger sanitization, but is inelegant.
- This con is removed if we either use the Combined Increasing Score rule variant described below, or we also apply the “Making bc‑rollbacks more difficult” change in the next section.
Apart from the above con, the original motivations for the Increasing Snapshot Score rule also apply to the Increasing Tip Score rule. In particular,
- it still prevents potential attacks that rely on proposing a bc‑valid‑chain that forks from a much earlier block;
- it still limits the extent of disruption an adversary can feasibly cause to \LOG_{\bda}};
- it still always allows a proposal to be made, which may be needed to preserve liveness of relative to ;
- it still prevents potential validation cost DoS attacks due to switching between snapshots with the same score.
If we switch to using the Increasing Tip Score rule, then it would be more consistent for block producers to also change the tie‑breaking rule for choosing to use the tip score, i.e. .
A variation on this suggestion effectively keeps both the Increasing Snapshot Score rule and the Increasing Tip Score rule:
Combined Increasing Score rule: Either ( and ), or .
Note that if , both scores are necessarily equal.
This variation does not simplify honest bft‑proposer behaviour.
Making exploitation of bc‑rollbacks more difficult
Basic idea: Detect the case where the bc‑snapshot is rolling back, and impose a longer confirmation depth to switch to the new bc‑chain. Also temporarily stall finalization of the existing bc‑chain until the conflict has been resolved.
Let be the Crosslink 1 definition of , i.e.
When , we want to go into a mode where we require a longer confirmation depth , say . Because we don’t know in this situation whether the old bc‑chain or the new bc‑chain will win, we stop finalizing both until a winner is clear.
The simplest option is to record the state saying that we are in this mode explicitly, and add a consensus rule requiring it to be correct. That is, add an field to bft‑proposals and bft‑blocks, and add a bft‑proposal and bft‑block validity rule as follows:
- Is Forked rule: or and not
where:
- .
It is intentional that takes precedence over .
Then redefine as follows:
Since , the recursion will terminate.
Note that there is an interaction between the Increasing Snapshot Score rule and this change: the Increasing Snapshot Score rule should arguably use instead of . The Increasing Tip Score rule, on the other hand, works fine as‑is, and so it makes sense to use both of these changes together. The combination of both changes also fixes the con discussed above for the Increasing Tip Score rule; it ensures that the score of the snapshot must increase.
Pros:
- If the winning chain is the chain that was first snapshotted, then there ends up being no disruption whatsoever to \LOG_{\bda}}.
- It becomes extremely difficult for an adversary with less than 50% hash power to get the finalized snapshot to switch between two competing chains more than once.
Cons:
- It is potentially easier to cause a temporary finalization stall. An adversary could try to provoke this situation on the honest chain, either as a DoS attack, or so that its own chain that is not so encumbered can finalize more quickly than the honest chain.
- This does not seem like a practical attack, because such a stall can only happen when the adversary can cause a ‑block rollback or has subverted .
- The definition of becomes more complicated, and there is a risk of this complexity introducing problems.
- It can be argued that, unless is chosen too small, an adversary that can cause a ‑block rollback likely has 50% of hash power, and therefore can cause a ‑block rollback. That is, increasing confirmation depth does not help beyond a certain point, and therefore (it could be argued) this change will also not help.
- This argument may hold for private mining attacks, but does not necessarily hold for partitioning attacks, as discussed in the next section.
Using tip information to detect rollbacks and partitions
In the case of a private mining attack, the adversary will typically conceal the existence of the overtaking chain until it can be used to cause a rollback in \LOG_{\bda}}. So the approach used in the previous section seems to be all we can do against such an attack.
In the case of a partitioning attack, on the other hand, the adversary relies on honest nodes to do mining work on each side of the partition. This relies on the successful miners on each side knowing about their chain, but not the chain on the other side. Subtly, it does not rely on a perfect network partition. An adversary could, for example, attempt to create partitions around the most successful mining pools. Occasional leaks of information across a partition also do not necessarily foil the attack unless that information gets to a successful miner. Therefore, measures that constrain the adversary’s ability to make use of an incomplete partition can be useful.
This also has the benefit of making the protocol more robust against non‑malicious incomplete partitions.
Given that in such an attack the competing chains may be visible to some proposers, there is the possibility of detecting a potential rollback even before it gets snapshotted, by using the fact that previous bft‑blocks created by honest bft‑proposers have been recording the bc‑best‑chain tip blocks ahead. Also, depending on what proportion of validators an adversary has, they may rely on honest validators on each side to ensure that a snapshot of each chain appears in a bft‑valid block; in that case, including information about competing chains in validators' votes (see the next subsection) may be useful.
It is still possible that if an adversary has several consecutive proposal slots, it can get its chain snapshotted. However, if there is an intervening slot with an honest proposer, we can potentially compare its tip with the adversary’s tip and anticipate the need to go into mode.
In order to get this to work, we need to propose a definition to identify bc‑chains that are competing with the current best chain, such that there is some risk of a “long” rollback to a competing chain. Let be a measure of how close (in terms of bc‑blocks) a competing chain’s score needs to be to that of the bc‑best‑chain, and let be a lower bound on the rollback depth we would consider significant if the competing chain were to immediately catch up. (The condition is necessary to avoid false positives that might only be a single‑block fork.)
A node identifies ‑competing chains as follows based on its current view at time :
- A bc‑block is a tip if it has no known descendants.
- Let be node ’s bc‑best‑chain.
- Identify all of the tips such that and .
Details, including how to modify the and conditions.
For now we will assume that all of the competing chain information in a bft‑block has to be checked as bc‑block‑valid in order for that block to be bft‑block‑valid. This might introduce validation DoS attacks and needs to be considered more carefully.
Allowing validators to signal the existence of a competing chain in their votes
This complements the above idea by letting a validator that has seen a competing chain signal it in its signed vote. Then, as long as the adversary is reliant on some votes from honest validators that are signalling the existence of competing chains, we would go into mode without relying on honest proposers to have an intervening slot.
The notarization proof that appears in a bft‑block would need to be modified to preserve these signals. More precisely, it is necessary for a bft‑block to preserve at least:
- the best bc‑chain that credibly competes with , if any.
- the best bc‑chain that does not credibly compete with (this necessarily exists because does not credibly compete with itself).
This is also motivated by the suggested change in the next section.
Enforcing this is relatively straightforward if the evidence is a SNARK. It can also be enforced with aggregate signatures even for schemes that only allow aggregation of signatures over a common message: we just collect the distinct messages (corresponding to either “no competing chain” or each distinct competing chain) and aggregate them separately.
Strengthening the Increasing Tip Score rule
Assume that votes include competing chain information as discussed above. We can assume that an honest proposer has read all of this information from its parent bft‑block. Therefore, we can require the tip score of its proposal to have at least the score of the best tip implied by that information:
Let be the tip mentioned in bft‑block with the highest score. A bft‑block “mentions” the two best tips defined in the previous section.
Strong Increasing Tip Score rule: Either or .
Note that this rule is really quite constraining for a potential adversary, especially in partitioning attacks. It means that if the adversary does not want to acknowledge the existence of a given chain, it cannot use any votes or build on any previous bft‑block that signals the existence of that chain. Essentially, a partitioning adversary with control over only the minimum one‑third of the stake would have to have ensure a perfectly complete partition; it could not get away with any information leakage between honest validators.
Attempts to improve finalization latency
[Broken] Adjusting the last snapshot definition
The Crosslink 1 design imposes a finalization latency of at least block times. Intuitively, this is because in is at least blocks back from (as argued in Questions about Crosslink 1), and therefore blocks back from . So the total finalization latency is block times + BFT overhead + block times + snapshot overhead.
However, the snapshot headers contain information about the proposer’s bc‑best‑chain.
Define . Although it is not guaranteed, normally will be an ancestor of . What if we were to optimistically allow the last snapshot to be taken as ? After all, we know that is confirmed.
Oh, this won’t work. The problem is that we want safety of not to depend on safety of . So we cannot assume (for this purpose) that nodes see the same .
Replacing \LOG_{\bda}} with \LOG_{\opt}}
What if we instead take this to be the definition of \LOG_{\opt}}, replacing \LOG_{\bda}} ("opt" meaning optimistic)?
As stated, a malicious proposer can try to maximize the latency of \LOG_{\opt}} (subject to the Increasing Score rule). For example, if there exists a fork of length , the malicious proposer can force the latency of \LOG_{\opt}} to be block times + BFT overhead. However, this can be improved by applying the idea to each bft‑block in turn after the one pointed to by the best confirmed bc‑block. Then a malicious proposer cannot do anything that it could not do anyway (keeping the finalization point at its current position).
Pros:
- This is always more conservative in terms of safety than the current design.
- The latency of \LOG_{\opt}} will typically be bc‑block times, rather than block times.
Cons:
- \LOG_{\opt}} is not dynamically available in any sense. It just has lower latency and different security characteristics.
- Even under optimistic conditions, \LOG_{\opt}} will lag slightly behind where it would be for the Crosslink 1 design, because will necessarily be ahead of .
[Broken] Using snapshots from the last‑seen bft‑chain when it is consistent with the bc‑best‑chain
The following idea is broken for safety when has been subverted:
We have two potential sources of information about blocks that could plausibly be considered finalized:
- the snapshots on the chain of the last seen final bft‑block, .
We cannot rely only on 1. because we want assured finalization even under partition. We cannot rely only on 2. because if has been subverted, then the chain of final bft‑blocks could fork.
But intuitively, if we combine these sources of information, using them over the Crosslink 1 finalization only when they are consistent, the resulting protocol should still be as safe as the safer of and . In particular, 2. will not roll back unless has been subverted.
If this idea were to pan out, it could improve the latency of finalization by block times.
This approach is essentially a hybrid of Snap‑and‑Chat and Crosslink 1:
- the Snap‑and‑Chat construction gives a finalized ledger under the assumption that has not been subverted;
- the main crosslink idea is used to make sure that outputs from all finalized transactions are eventually spendable;
- safety is still only dependent on the stronger of the safety of and , because we use the additional information from snapshots in final bft‑blocks only up to the point at which they agree with the best confirmed bc‑block.
To explain the safety problem with this idea: suppose that has been subverted. In that case it is possible for a snapshot to be finalized without having being confirmed as in any honest node’s bc‑best‑chain; that is, it is possible for to include transactions from a snapshot in bft‑block such that is not on the consensus bc‑best‑chain. And, because has been subverted, it is also possible that a conflicting final bft‑block omits . And so a node that has seen will think that it is consistent with the best bc‑chain (so that its does not include but does include later transactions on the consensus bc‑best‑chain), but a node that has seen will compute a that does include .
More detailed specification of the above broken idea.
Define as before.
For simplicity assume that extends by only one bft‑block. (This assumption could have been removed if the idea had panned out.)
Then this proposal was to consider this bc‑block as contributing the last finalized snapshot:
There is no need for a tie‑breaking rule for 2.: if we ever see two context bft‑blocks for which the last‑final blocks are conflicting, we know that has been subverted, so we should stall or crash.
Caveat: for a given node, can in theory roll back past , therefore can also roll back. It is okay if we keep state here and refuse to roll back. We should set a “crisis flag”, and unset it if at any point extends . (If is safe and live, it will.)
A similar rule that would give the same result in almost all circumstances is:
What about making the bc‑block‑producer the bft‑proposer?
The answer given for this question at The Crosslink 2 Construction is:
If this were enforced, it could be an alternative way of ensuring that every bft‑proposal snapshots a new bc‑block with a higher score than previous snapshots, potentially making the Increasing Score rule redundant. However, it would require merging bc‑block‑producers and bft‑proposers, which could have concerning knock‑on effects (such as concentrating security into fewer participants).
This may have been too hasty. It is not clear that merging bc‑block‑producers and bft‑proposers actually does “concentrate security into fewer participants” in a way that can have any harmful effect.
Remember, the job of a bft‑proposer in Crosslink is primarily to snapshot the bc‑best‑chain (even more so if the Increasing Tip Score rule is adopted). An honest miner by definition is claiming to build on the best chain, and miners have a strong economic incentive to do so. Therefore, it is entirely reasonable for every newly produced block to be treated as a bft‑proposal. This arguably decentralizes the task of proposing bft‑blocks more effectively than using a leader election protocol would — especially given that in a hybrid protocol we necessarily still rely on there being sufficient honest miners.
[DKT2021], for example, argues for the importance of “the complete unpredictability of who will get to propose a block next, even by the winner itself.” The main basis of this argument is that it makes subversion of the proposer significantly more difficult. A PoW protocol has that property, and most PoS protocols do not. (It is not that PoS protocols are unable to provide this property; indeed, [DKT2021] constructs a PoS protocol, “PoSAT”, that provides it.)
So let’s explore this in more detail. A newly produced bc‑block would implicitly be a bft‑proposal with itself as the tip. The field is therefore not needed. The Tail Confirmation rule goes away since its intent is automatically satisfied. This is already a significant simplification.
The inner proposer signature is also not needed (since the bc‑header is self-authenticating), but the block producer would have to include a public key that can be used to verify its outer signature. It would sign the notarized bft‑block with the corresponding private key. This change is a wash in terms of protocol complexity.
Considered as a bft‑proposal, a bc‑block needs to refer to a parent bft‑block, which requires a field in the bc‑header. With some caveats depending on the design of , it might be possible to merge this with the field, but for now we will assume that it is not merged.
What are the caveats?
If we are in an execution where Final Agreement holds for , then it is possible to show that merging the two fields has no negative effect, provided that has no additional rules that could disallow it in some cases.
This is because, by Final Agreement, for any potential bft‑block that the bc‑block‑producer of a new block could choose as . Suppose that the bc‑block‑producer freely chooses according to the desired honest behaviour for a bft‑proposer in , and then chooses to be the same block (which is always reasonable as long as it is allowed).
In the case , we are done, because this choice of is allowed by the Extension rule.
In the case , we can argue that would be a better choice than for as well as for , because it has a later final ancestor. This is where the argument might fall down if (and therefore ) has any additional rules that could disallow this choice. For now let’s suppose that situtation does not arise, but it is one of the caveats.
Another potential problem is that in an execution where Final Agreement does not hold for , we can no longer infer that either or . In particular it could be the case that the producer of was adversarial, and chose in such a way as to favour its own bft‑block that is final in that context.
However, in that situation it must be possible for the bc‑block‑producer to see (and prove) that the bft‑chain has a final fork. That is, it can produce a witness to the violation of Final Agreement, showing that does not hold, as discussed in the section Recording more info about the bft‑chain in bc‑blocks above.
The second caveat is that in that situation, we still need to set and in order to be able to recover, and they typically should not be the same in order to do so.
The Increasing Tip Score rule is still needed, but it can be simplified. A newly produced bc‑block is also a bft‑proposal such that . This would yield the following bft‑proposal / bc‑block validity rule:
[Candidate rule for discussion] Either or .
except that cannot be , because is newly produced. It turns out we can just drop that part:
Increasing Tip Score (producer = proposer) rule: .
This works because, if does not have a higher score than the bc‑block , the bc‑block‑producer should instead have built on top of that bc‑block — which was necessarily known to the producer in order for it to set in the header of the new block.
The voting would be the same, performed by the same parties. Therefore, there is no concentration of voting into fewer parties. There is no change in the producer/proposer’s incentive to make the bft‑notarization‑proof or its soundness properties. Everything else is roughly the same, including the use of the field of a bc‑block and the validity rules related to it. As far as I can see, all of the security analysis goes through essentially unchanged.
There may be some complication due to the fact that BFT protocols are typically designed to use epochs with a fixed period, whereas bc‑blocks are found at less predictable intervals. However, as long as BFT messages are labelled with the bc‑block they apply to, it seems like most BFT protocols would be tolerant to this change. In fact the adaptations of Snap‑and‑Chat to Hotstuff and PBFT in [NTT2020] already assume that BFT messages can be queued and processed at a later time, and rely on those BFT protocols' tolerance to this.
In most PoS protocols, the requirement to have a minimum amount of stake in order to make a proposal acts as a gatekeeping filter on proposals, and potentially allows parties that make invalid proposals to be slashed.
Strictly speaking, whether there is a stake requirement to make a proposal is independent of whether bc‑block‑producers (e.g. miners) are merged with bft‑proposers. It could be, for example, that a miner is still able to produce bc‑blocks, but is not able to make them into a proposal unless they satisfy a stake requirement. (This would have significant effects on the economics of mining that would need to be analyzed, and that might have governance consequences.)
In a system that uses PoS, validators by definition need to have stake in order to control the ability to vote. This also allows validators to be slashed.
On the other hand, there is no technical reason why the ability to make a bft‑proposal has to be gatekept by a stake requirement — given the situation of Zcash in which we already have a mining infrastructure, and that in a Snap‑and‑Chat or Crosslink‑style hybrid protocol we necessarily still rely on miners not to censor transactions. The potential to make proposals that are expensive to validate as a denial of service is made sufficiently difficult by proof‑of‑work. This option has probably been underexplored by previous PoS protocols because they cannot assume an existing mining infrastructure.
It could be argued that this approach goes less far toward a pure PoS‑based block‑chain protocol, leaving more to be done in the second stage. However, there is a clear route to that second stage, by replacing PoW with a protocol like PoSAT that has full unpredictabilty and dynamic availability. PoSAT does this using a VDF, and as it happens, Halo 2 is a strong candidate to be used to construct such a VDF.
If the arguments in [DKT2021] about the need for proposer unpredictability are persuasive, then this approach defers the complexity of requiring a VDF without losing any security, since Zcash’s PoW is already unpredictable.
Do we need an explicit bft‑chain at all?
Building on the previous idea, we can try to eliminate the explicit bft‑chain by piggybacking the information it would hold onto a bc‑block (in the header and/or the block contents). In the previous section we merged the concepts of a bft‑proposal and a bc‑block; the and fields of a bft‑proposal were moved into the and fields of a bc‑header respectively. A field was also added to hold the producer’s public key, so that the producer can sign the bft‑block constructed from it using the corresponding private key.
This left the concept of a bft‑block intact. Recall that in Crosslink 1, a bft‑block consists of signed by the proposer. So in “Crosslink with proposer = producer”, a bft‑block consists of signed by the producer.
What if a bc‑block were to “inline” its parent and context bft‑blocks rather than referring to them? I.e. a bc‑block with referring to signed for , would instead literally include (either in the header or the coinbase transaction) signed for — and similarly for .
It would still be necessary to have the message type that the proposer/producer previously used to submit a notarized bft‑block. (It cannot be merged with a bc‑block announcement: the producer of a new block is not in general the producer of its parent, and their incentives may differ; also we cannot wait until a new block is found before publishing the previous notarization.) It would also still be necessary for Crosslink nodes to keep track of notarizations that have not made it into any bc‑block. Nevertheless, this is a potential simplification.
Note that unless notarization proofs are particularly short and constant-length, it would not be appropriate to include them in the bc‑block headers, and so they would have to go into the coinbase transaction or another similar variable-length data structure. In that case we would still have an indirection to obtain the bft‑block information; it would just be merged with the indirection to obtain a coinbase transaction (or similar) — which is already needed in order to check validity of the bc‑block.
As discussed under Recording more info about the bft‑chain in bc‑blocks above, we might in any case want to record information about other proposed and notarized bft‑blocks, and the data structure needed for this would necessarily be variable-length. The complexity burden of doing so would be shared between these two changes.
It would be possible to save some space in headers (while keeping them fixed-length), by inlining only one of and in the header and keeping the other as a hash. As discussed under “What are the caveats?” above, the only reason for the two bft‑blocks referred to by these fields to be different, is that the bc‑block producer has observed a violation of Final Agreement in . In that case, we can include an inlining of the other block, and any other information needed to prove that a violation of Final Agreement has occurred, in a variable-length overflow structure.
Pros:
- No additional mechanism or messages are needed to obtain bft‑blocks given their hashes.
- It could be a performance/latency improvement to not have to separately fetch bft‑blocks.
Con:
- Additional complexity of the variable-length overflow mechanism suggested above, if it is used.
- Assumes that notarization proofs are not too large.
Linearity and Last Final Snapshot rules
A potential simplification can be obtained by combining the following two ideas:
- Str4d suggested that the snapshot of each bft‑block should descend from the snapshot of its parent bft‑block.
- Nate suggested that each bc‑block should descend from .
Str4d’s suggestion can be written as:
Linearity rule: .
Notice that this implies the existing Increasing Score rule in Crosslink 1, because score necessarily increases within a bc‑valid‑chain. Therefore it would in practice be a replacement for the Increasing Score rule. It does not imply the Increasing Tip Score rule discussed above, and in fact it could make sense to enforce both the Linearity rule and the Increasing Tip Score rule.
The Linearity rule implies that it is no longer possible for a bft‑valid‑chain to snapshot a bc‑chain that rolls back relative to the previous snapshot. This makes it unnecessary to sanitize : the sequence of snapshots considered by is linear, and so the “sanitization” would just return the transactions in the last snapshot.
To remove the need to sanitize as well, we need a further modification to . Recall that in Crosslink 1 we define: The Linearity rule ensures that is a linear sequence of snapshots, but for to be linear, we also need . In order for this to hold for any choice of with , we require the strongest version of this condition with , i.e. .
Since we can only enforce that this holds for by enforcing that it holds for an arbitrary bc‑valid‑block , the rule becomes:
Last Final Snapshot rule: .
This is exactly Nate’s suggestion discussed in Questions about Crosslink. In that document we argued against this rule, but that argument was made in the context of a protocol without the Linearity rule (and originally, even without the Increasing Score rule).
Combining the Linearity rule and Last Final Snapshot rule, on the other hand, completely eliminates the need for sanitization. This could be a huge simplification — and potentially safer, since it would avoid breaking assumptions that may be made by existing Zcash node implementations and other consumers of the Zcash block chain.
To spell out the resulting simplifications to the definitions of and \LOG^t_{\bda,\mu,i}, we would just have: \begin{array}{rcl} \LOG_{\fin,i}^t &:=& \snapshotlf{\ch_i^t \trunc_{\bc}^\sigma} \ \LOG_{\bda,\mu,i}^t &:=& \ch_i^t \trunc_{\bc}^\mu \end{array}
Here it is no longer necessary to define and \LOG^t_{\bda,\mu,i} as sequences of transactions, since the final and bounded-available chains are both just bc‑valid‑chains.
The definition of in the Finality depth rule becomes much simpler: As before, either or .
Avoiding sanitization also means that the bug we described in Snap‑and‑Chat, that could prevent spending outputs from a snapshotted chain after a -block rollback, cannot occur by construction. That is, the changes in contexual validity relative to are not needed any more.
This almost seems too simple, and indeed we should be skeptical, because the security analysis essentially has to be redone. The reason why Snap‑and‑Chat didn’t take this approach is that it requires a more complicated argument to show that it is reasonable to believe in the safety assumptions of whenever it is reasonable to believe in the corresponding assumptions for . This is because the ... We will need to do some work to show that the changes are benign.
Security Analysis
The key observation needed for this analysis is that neither the Linearity rule nor the Last Final Snapshot rule affect the evolution of unless we are in a situation where its Prefix Consistency or Prefix Agreement properties would be violated.
This implies that any safety property that we can prove given Prefix Consistency plus ****.