Values
Yul values.
Yul, being generic, is parameterized over
a collection of supported types and their values.
For the EVM dialect of Yul, which is our initial interest,
the only supported type is u256, i.e. unsigned 256-bit integers.
Based on discussions on Gitter,
it is best to view this as a type of 256-bit words,
rather than as a type of 256-bit unsigned integers,
because the intent is to match the EVM notion of word,
which can be operated upon as an either unsigned or signed integer.
Nonetheless, in our ACL2 formalization,
we represent 256-bit words as 256-bit unsigned integers,
which can be thought of as bit vectors.
We define values as wrapped 256-bit unsigned integers,
meant to represent 256-bit words.
As explained in the static semantics, for now we do not have explicit types,
i.e. we have just one type.
This matches the fact that we have just one kind of values.
We should extend and genearalize this.
Subtopics
- Value-list-result
- Fixtype of errors and lists of values.
- Value
- Fixtype of values.
- Value-result
- Fixtype of errors and values.
- Value-list
- Fixtype of lists of values.
