- Supplementary general tactics and results
- Definitions of Giskard datatypes
- Local state operations, properties, and transitions
- Global state operations, transitions and properties
- Safety property one: Prepare stage height injectivity
- Safety property two: Precommit stage height injectivity
- Precommit stage definition
- Precommit stage height injectivity statement
- Reducing the proof
- Global trigger message blocks as lower bounds
- Ingredient one: All blocks that reach prepare stage in some view must have a PrepareBlock message in the global message buffer in that view.
- Ingredient two: The piggyback block of PrepareBlock messages in some view is equal to the trigger message block from the previous view.
- Ingredient three: All PrepareBlock messages have a lower piggyback block than proposed block
- Proof of the lower bound
- Global trigger message blocks as upper bounds
- Global trigger message blocks increase with view
- Final cases of precommit stage height injectivity
- Safety property three: Commit stage height injectivity