Transitions for proposal creation.
Here we define the system state changes caused by
A correct validator creates a proposal only under certain conditions; in particular, it never creates an equivocal proposal, i.e. one with the same author and round as an existing one. A faulty validator is not so constrained, but it cannot forge signatures of correct validators (because if a validator's private key is compromised, the validator is considered faulty).
Either way, the proposal is broadcast to other validators. A correct validator sends it exactly to all the other members of the active committee; a faulty validator may send it to any validators. However, in order to model the possibility that a faulty validator in the committee forwards the proposal to a faulty validator not in the committee, so that the latter might endorse the proposal and send the endorsement back to the proposer, we relax our model of proposal broadcasting by allowing a proposal to be sent also to faulty validators not in the committee.
If the validator is correct, it stores the proposal into its internal state, along with information about endorsements received by other validators; initially there are no such endorsements.