Integer-ranges
Ranges of the integer types.
Based on the nullary functions defined in integer-formats,
for each standard signed and unsigned integer type except _Bool,
we define the following:
- A fixtype of the ACL2 integers in the range of the types.
- A fixtype of the lists of the above ACL2 integers.
- A nullary function returning the maximum ACL2 integer in the range.
- A nullary function returning the minimum ACL2 integer in the range,
if the type is signed (if it is unsigned, the minimum is just 0).
- Theorems about the above items.
We use fty::defbyte to define the ranges,
but we also prove theorems providing alternative definitions
of the signed and unsigned ACL2 integers in terms of minima and maxima.
This gives us the ability to view the integer ranges
as ACL2's signed-byte-p and unsigned-byte-p values,
which is useful for bitwise operations,
but also as plain integers in certain ranges,
which should lead to simpler reasoning about ranges.
As mentioned in integer-formats,
the definitions of ranges we give here
should still work if the format definitions are changed.
Subtopics
- Def-integer-range
- Event to generate fixtypes, functions, and theorems
for ranges of integer types.
- Integer-type-rangep
- Check if a mathematical integer is in the range of an integer type.
- Ushort-integer
- Fixtype of ACL2 integers in the range of type unsigned short.
- Ullong-integer
- Fixtype of ACL2 integers in the range of type unsigned long long.
- Sshort-integer
- Fixtype of ACL2 integers in the range of type signed short.
- Sllong-integer
- Fixtype of ACL2 integers in the range of type signed long long.
- Ulong-integer
- Fixtype of ACL2 integers in the range of type unsigned long.
- Uint-integer
- Fixtype of ACL2 integers in the range of type unsigned int.
- Uchar-integer
- Fixtype of ACL2 integers in the range of type unsigned char.
- Slong-integer
- Fixtype of ACL2 integers in the range of type signed long.
- Sint-integer
- Fixtype of ACL2 integers in the range of type signed int.
- Schar-integer
- Fixtype of ACL2 integers in the range of type signed char.
- Ushort-max
- Maximum ACL2 integer value of type unsigned short.
- Slong-max
- Maximum ACL2 integer value of type signed long.
- Integer-type-max
- Maximum mathematical integer value of an integer type.
- Sllong-max
- Maximum ACL2 integer value of type signed long long.
- Integer-type-min
- Minimum mathematical integer value of an integer type.
- Uint-max
- Maximum ACL2 integer value of type unsigned int.
- Sint-max
- Maximum ACL2 integer value of type signed int.
- Ulong-max
- Maximum ACL2 integer value of type unsigned long.
- Uchar-max
- Maximum ACL2 integer value of type unsigned char.
- Def-integer-range-loop
- Events to generate fixtypes, functions, and theorems
for ranges of integer types.
- Sshort-min
- Minimum ACL2 integer value of type signed short.
- Sshort-max
- Maximum ACL2 integer value of type signed short.
- Slong-min
- Minimum ACL2 integer value of type signed long.
- Sint-min
- Minimum ACL2 integer value of type signed int.
- Ullong-max
- Maximum ACL2 integer value of type unsigned long long.
- Sllong-min
- Minimum ACL2 integer value of type signed long long.
- Schar-min
- Minimum ACL2 integer value of type signed char.
- Schar-max
- Maximum ACL2 integer value of type signed char.
- Ushort-integer-list
- Fixtype of lists of ACL2 integers in the range of type unsigned short.
- Ulong-integer-list
- Fixtype of lists of ACL2 integers in the range of type unsigned long.
- Ullong-integer-list
- Fixtype of lists of ACL2 integers in the range of type unsigned long long.
- Uint-integer-list
- Fixtype of lists of ACL2 integers in the range of type unsigned int.
- Uchar-integer-list
- Fixtype of lists of ACL2 integers in the range of type unsigned char.
- Sshort-integer-list
- Fixtype of lists of ACL2 integers in the range of type signed short.
- Slong-integer-list
- Fixtype of lists of ACL2 integers in the range of type signed long.
- Sllong-integer-list
- Fixtype of lists of ACL2 integers in the range of type signed long long.
- Sint-integer-list
- Fixtype of lists of ACL2 integers in the range of type signed int.
- Schar-integer-list
- Fixtype of lists of ACL2 integers in the range of type signed char.
- Uchar-integerp-alt-def
- Alternative definition of uchar-integerp as integer range.
- Ushort-integerp-alt-def
- Alternative definition of ushort-integerp as integer range.
- Ulong-integerp-alt-def
- Alternative definition of ulong-integerp as integer range.
- Ullong-integerp-alt-def
- Alternative definition of ullong-integerp as integer range.
- Uint-integerp-alt-def
- Alternative definition of uint-integerp as integer range.
- Sshort-integerp-alt-def
- Alternative definition of sshort-integerp as integer range.
- Slong-integerp-alt-def
- Alternative definition of slong-integerp as integer range.
- Sllong-integerp-alt-def
- Alternative definition of sllong-integerp as integer range.
- Sint-integerp-alt-def
- Alternative definition of sint-integerp as integer range.
- Schar-integerp-alt-def
- Alternative definition of schar-integerp as integer range.
