Account for transaction expiration in Crosslink's model of contextual validity

[daira]

Suggested Improvement

In The Crosslink Construction — Model for best-chain protocols (Π_{origbc,bc}):

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

Another reason for a transaction to be contextually invalid in Zcash is that it has expired.

The reason given to make the above assumption was stated as:

It is needed for equivalence of the following two ways to construct LOG{fin,bda}​:

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

This reason is specific to Crosslink 1. In Crosslink 2 (or 2*) we do not need sanitization at all.

Even in Crosslink 1, it would have been fine to allow expiration as a contextual transaction validity rule, because it would have been sufficient to add this point to the equivalence argument:

• If a transaction is omitted due to expiration, then any subsequent time it is checked, it will still be expired.

The folded section "Is this model of contextual validity sufficient for Zcash?" also does not take expiration into account.