Maybe-byte-list20
Fixtype of byte arrays of length 20 and nil.
This is an option type introduced by fty::defoption.
Note that defoption is just a wrapper for fty::defflexsum, so there are :none and :some member
types, a case macro, and so forth.
Member Types
- :none → maybe-byte-list20-none
- Represents that no maybe-byte-list20 is available, i.e., Nothing or None.
- :some → maybe-byte-list20-some
- An available maybe-byte-list20, i.e., Just val or Some val.
The \mathbf{to} field of a transaction [YP:4.2] is
either a 20-byte (i.e. 160-bit) address
or the empty array (i.e. the only element of \mathbb{B}_0) [YP:(18)].
Both [YP:4.2] and [YP:(18)] mention \varnothing as
the (only) element of \mathbb{B}_0;
however, according to the definition of \mathbb{B} [YP:(178)],
the empty array should be denoted as ().
Regardless, in our model the empty byte array is nil,
so we use either a list of 20 bytes or nil
to model the \mathbf{to} field of a transaction.
Subtopics
- Maybe-byte-list20-fix
- Fixing function for maybe-byte-list20 structures.
- Maybe-byte-list20-equiv
- Basic equivalence relation for maybe-byte-list20 structures.
- Maybe-byte-list20-case
- Case macro for the different kinds of maybe-byte-list20 structures.
- Maybe-byte-list20-some
- An available maybe-byte-list20, i.e., Just val or Some val.
- Maybe-byte-list20-none
- Represents that no maybe-byte-list20 is available, i.e., Nothing or None.
- Maybe-byte-list20p
- Recognizer for maybe-byte-list20 structures.
