Review prototype implementation for Last Final Snapshot, Extension, and Linearity rules from TFL book.

[shielded-nate]

[shielded-nate]

Text around Last Snapshot rule is here

[shielded-nate]

The SL devs met to reread the $\Pi_{bc}$ block validity section from the TFL Book and to discuss the current prototype.

Next steps:

• Analyze the prototype code, document where the validations are performed, or if they aren't performed or may need better scrutiny, track that in this issue tracker to do followup patches to the code.
• Make illustrative diagrams for many of the rules and function/property definitions in the TFL book for reference.

[shielded-nate]

-also, I just recalled the utility and relevance of using tools like quint for exactly these concerns, so I added #278.

[pmttavara]

• Make the "genesis BFT" explicit, or document where and how the genesis BFT state is represented implicitly (in config and elsewhere).
• Write a function or annotated code block identifying each of the block validity rules -- with links connecting each check to each rule as stated in the book.