|
|
|---|
|
|
|
|---|
Fixtype of transactions.
This is a tagged union type, introduced by fty::deftagsum.
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, via a wrapper of any ACL2 value.
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.