Fixtype of transactions.
This is a tagged union type, introduced by fty::deftagsum.
Our model treats transactions as mostly opaque. Certain transactions bond and unbond validators, which is what makes the validator committee dynamic. So we model three kinds of transactions: bond a validator with a given amount of stake, unbond a validator, and something else that does not bond or unbond validators; we leave the details of third third kind open.
Stake is modeled as a positive integer, which can be imagined to be Aleo micro-credits, but the exact unit of stake is irrelevant to our model. A bonding transaction consists of the address of the validator and the stake bonded. An unbonding transaction consists of just the address of the validator; implicitly, the transaction unbonds all the bonded stake. As formalized elsewhere, in our model nothing prevents a block from including multiple transactions that bond and/or unbond the same validator, which have a net effect at the end of the block; this provides flexibility in modeling validators that change their stake as net effect in a block (regardless of whether the full AleoBFT puts restrictions on that).
We do not model AleoBFT solutions and ratifications explicitly. The third kind of transactions in our model can be thought of as including those as well.