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 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 some net effect at the end of the block; this provides flexibility in modeling validators that change their stake as net effect in a block.
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.