Integer-operations
Integer operations [SD: Types: Integers].
If a binary operator is applied to operands of different types,
there is an (attempted) implicit conversion
from the type of one operand to the type of the other operand [SD: Types: Conversions between Elementary Types: Implicit Conversions]. Thus, once the operator is actually applied to the two operand values,
the implicit conversion must have succeeded
and thus the values must have the same time.
Therefore, the ACL2 functions that model binary integer operations
have guards requiring the two operands to have the same type
(i.e. the same signedness and the same size).
However, the requirement above that the operands of a binary operator
always are of, or can be converted to, the same type,
may need to be relaxed for some operations.
The wording in [SD: Types: Integers: Exponentiation] and [SD: Types: Integers: Shifts] suggests that operands may have different types for these operations,
in a way that no conversion to a common type may be possible.
For now we strictly follow the same-rule type,
and therefore must exclude exponentiation and shifts on signed integers.
However, we may need to adjust our formalization as noted above,
and add exponentiation and shifts involving signed integers
(for their first operands only, not their second operands.
Subtopics
- Def-uint/int-binary-op
- Macro to formalize a Solidity integer binary operation.
- Def-uint/int-unary-op
- Macro to formalize a Solidity integer unary operation.
- Def-uint/int-comparison
- Macro to formalize the Solidity integer comparisons.
- Uint-mod
- Modulo of unsigned integer values.
- Uint-div
- Division of unsigned integer values.
- Uint-shr
- Right shift of unsigned integer values.
- Uint-shl
- Left shift of unsigned integer values.
- Int-mod
- Modulo of signed integer values.
- Int-div
- Division of signed integer values.
- Uint-xor
- Bitwise exclusive disjunction of unsigned integer values.
- Uint-sub
- Subtraction of unsigned integer values.
- Uint-mul
- Multiplication of unsigned integer values.
- Uint-ior
- Bitwise inclusive disjunction of unsigned integer values.
- Uint-exp
- Exponentiation of unsigned integer values.
- Uint-and
- Bitwise conjunction of unsigned integer values.
- Uint-add
- Addition of unsigned integer values.
- Int-xor
- Bitwise exclusive disjunction of signed integer values.
- Int-sub
- Subtraction of signed integer values.
- Int-mul
- Multiplication of signed integer values.
- Int-ior
- Bitwise inclusive disjunction of signed integer values.
- Int-and
- Bitwise conjunction of signed integer values.
- Int-add
- Addition of signed integer values.
- Uint-le
- Less-than-or-equal-to comparison of unsigned integer values.
- Uint-ge
- Greater-than-or-equal-to comparison of unsigned integer values.
- Uint-ne
- Non-equality comparison of unsigned integer values.
- Uint-lt
- Less-than comparison of unsigned integer values.
- Uint-gt
- Greater-than comparison of unsigned integer values.
- Uint-eq
- Equality comparison of unsigned integer values.
- Int-ne
- Non-equality comparison of signed integer values.
- Int-lt
- Less-than comparison of signed integer values.
- Int-le
- Less-than-or-equal-to comparison of signed integer values.
- Int-gt
- Greater-than comparison of signed integer values.
- Int-ge
- Greater-than-or-equal-to comparison of signed integer values.
- Int-eq
- Equality comparison of signed integer values.
- Uint-minus
- Arithmetic negation of unsigned integer values.
- Uint-not
- Bitwise negation of unsigned integer values.
- Int-not
- Bitwise negation of signed integer values.
- Int-minus
- Arithmetic negation of signed integer values.
