• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
            • Representation-of-integer-operations
            • Atc-arrays
            • Representation-of-integers
              • Def-integer-values
              • Ushort-list-from-integer-list
              • Ullong-list-from-integer-list
              • Sshort-list-from-integer-list
              • Sllong-list-from-integer-list
              • Integer-list-from-ushort-list
              • Integer-list-from-ullong-list
              • Integer-list-from-sshort-list
              • Integer-list-from-sllong-list
              • Ulong-list-from-integer-list
              • Uchar-list-from-integer-list
              • Slong-list-from-integer-list
              • Schar-list-from-integer-list
              • Integer-list-from-ulong-list
              • Integer-list-from-uchar-list
              • Integer-list-from-slong-list
              • Integer-list-from-schar-list
              • Uint-list-from-integer-list
              • Sint-list-from-integer-list
              • Integer-list-from-uint-list
              • Integer-list-from-sint-list
              • Cinteger
              • Sintp
              • Ullongp
              • Ucharp
              • Ushortp
              • Ulongp
              • Uintp
              • Sllongp
              • Slongp
              • Sshortp
              • Scharp
              • Integer-from-sshort
              • Integer-from-sllong
              • Integer-from-sint
              • Integer-from-slong
              • Integer-from-schar
              • Integer-type-to-fixtype
              • Integer-from-ushort
              • Integer-from-ullong
              • Integer-from-uchar
              • Integer-from-cinteger
              • Integer-from-ulong
              • Integer-from-uint
              • Def-integer-values-loop
              • Sint-from-integer
              • Sint
              • Fixtype-to-integer-type
              • Uchar-from-integer
              • Ushort-from-integer-mod
              • Ushort-from-integer
              • Ulong-from-integer-mod
              • Ulong-from-integer
              • Ullong-from-integer-mod
              • Ullong-from-integer
              • Uchar-from-integer-mod
              • Sshort-from-integer
              • Slong-from-integer
              • Sllong-from-integer
              • Schar-from-integer
              • Uint-from-integer-mod
              • Uint-from-integer
              • Uchar
              • Schar
              • Ushort
              • Ulong
              • Ullong
              • Sshort
              • Slong
              • Sllong
              • Ullong-fix
              • Uint
              • Uchar-fix
              • Sint-fix
              • Ushort-fix
              • Ulong-fix
              • Uint-fix
              • Sshort-fix
              • Slong-fix
              • Sllong-fix
              • Schar-fix
              • Ushort-list
              • Ulong-list
              • Ullong-list
              • Uint-list
              • Uchar-list
              • Sshort-list
              • Slong-list
              • Sllong-list
              • Sint-list
              • Schar-list
              • Integer-type-to/from-fixtype-theorems
              • *nonchar-integer-fixtypes*
            • Representation-of-integer-conversions
            • Pointed-integers
            • Shallow-deep-embedding-relation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Representation

Representation-of-integers

A representation of C integers in ACL2.

This is part of the shallow embedding.

We define a representation of the C standard signed and unsigned integer values, except _Bool for now, based on their format definitions and range definitions. As mentioned in the documentation of the integer formats, the definitions of values we give here should still work if the format definitions are changed.

For each C integer type covered by our representation, we define the C values as wrappers of ACL2 integers in appropriate ranges. We also define lists of these C values, and some operations between these lists and lists of ACL2 integers in the corresponding ranges.

For the unsigned types, we also introduce ACL2 functions to turn ACL2 integers into values of those types by reducing them modulo one plus the maximum value of the type. These functions are used to define certain C integer conversions and operations, which are modular for unsigned integer types.

This representation of C integers in ACL2 should be treated like abstract data types whose definition is opaque. Consider the representation of unsigned char, for instance. The exact definition of ucharp does not matter. What matters is that the set of ACL2 values that satisfy that predicate is isomorphic to the set of ACL2 integers that satisfy uchar-integerp; the isomorphisms between the two sets are integer-from-uchar and uchar-from-integer. The fixer uchar-fix should be treated opaquely too. There should be sufficient theorems that capture the isomorphism property and that support reasoning about these C integers in ACL2 independently from their representation. On the other hand, uchar-integerp is not opaque: it is a known set of ACL2 integers, and that matters for reasoning. As a practical issue, uchar-integerp-alt-def, which as the name suggests is like an alternative definition, is generally more convenient than the actual definition, because the latter involves powers of two and bit sizes, while the alternate definition involves minima and maxima. As another practical issue, it is generally unnecessary to enable the fixer uchar-integer-fix, which exposes uchar-integerp, which therefore needs to be enabled anyways; there is a theorem that simplifies away uchar-integer-fix when uchar-integerp holds, so enabling uchar-integerp-alt-def should normally suffice. Even with the aforementioned isomorphisms disabled, their executable counterparts are enabled (per ACL2's defaults), exposing the internal representation in some constant cases; we may consider keeping those executable counterparts disabled too.

Subtopics

Def-integer-values
Event to generate the model of the values of a C integer type.
Ushort-list-from-integer-list
Lift ushort to lists.
Ullong-list-from-integer-list
Lift ullong to lists.
Sshort-list-from-integer-list
Lift sshort to lists.
Sllong-list-from-integer-list
Lift sllong to lists.
Integer-list-from-ushort-list
Lift integer-from-ushort to lists.
Integer-list-from-ullong-list
Lift integer-from-ullong to lists.
Integer-list-from-sshort-list
Lift integer-from-sshort to lists.
Integer-list-from-sllong-list
Lift integer-from-sllong to lists.
Ulong-list-from-integer-list
Lift ulong to lists.
Uchar-list-from-integer-list
Lift uchar to lists.
Slong-list-from-integer-list
Lift slong to lists.
Schar-list-from-integer-list
Lift schar to lists.
Integer-list-from-ulong-list
Lift integer-from-ulong to lists.
Integer-list-from-uchar-list
Lift integer-from-uchar to lists.
Integer-list-from-slong-list
Lift integer-from-slong to lists.
Integer-list-from-schar-list
Lift integer-from-schar to lists.
Uint-list-from-integer-list
Lift uint to lists.
Sint-list-from-integer-list
Lift sint to lists.
Integer-list-from-uint-list
Lift integer-from-uint to lists.
Integer-list-from-sint-list
Lift integer-from-sint to lists.
Cinteger
Fixtype of all the supported C integer types.
Sintp
Recognizer of values of type signed int.
Ullongp
Recognizer of values of type unsigned long long.
Ucharp
Recognizer of values of type unsigned char.
Ushortp
Recognizer of values of type unsigned short.
Ulongp
Recognizer of values of type unsigned long.
Uintp
Recognizer of values of type unsigned int.
Sllongp
Recognizer of values of type signed long long.
Slongp
Recognizer of values of type signed long.
Sshortp
Recognizer of values of type signed short.
Scharp
Recognizer of values of type signed char.
Integer-from-sshort
Accessor for values of type signed short.
Integer-from-sllong
Accessor for values of type signed long long.
Integer-from-sint
Accessor for values of type signed int.
Integer-from-slong
Accessor for values of type signed long.
Integer-from-schar
Accessor for values of type signed char.
Integer-type-to-fixtype
Name of the fixtype of the values of a C integer type.
Integer-from-ushort
Accessor for values of type unsigned short.
Integer-from-ullong
Accessor for values of type unsigned long long.
Integer-from-uchar
Accessor for values of type unsigned char.
Integer-from-cinteger
ACL2 integer corresponding to the C integer.
Integer-from-ulong
Accessor for values of type unsigned long.
Integer-from-uint
Accessor for values of type unsigned int.
Def-integer-values-loop
Events to generate the models of the values of some C integer types.
Sint-from-integer
Constructor for values of type signed int.
Sint
Fixtype of values of type signed int.
Fixtype-to-integer-type
Integer type corresponding to a fixtype name, if any.
Uchar-from-integer
Constructor for values of type unsigned char.
Ushort-from-integer-mod
Reduce modularly ACL2 integers to values of type unsigned short.
Ushort-from-integer
Constructor for values of type unsigned short.
Ulong-from-integer-mod
Reduce modularly ACL2 integers to values of type unsigned long.
Ulong-from-integer
Constructor for values of type unsigned long.
Ullong-from-integer-mod
Reduce modularly ACL2 integers to values of type unsigned long long.
Ullong-from-integer
Constructor for values of type unsigned long long.
Uchar-from-integer-mod
Reduce modularly ACL2 integers to values of type unsigned char.
Sshort-from-integer
Constructor for values of type signed short.
Slong-from-integer
Constructor for values of type signed long.
Sllong-from-integer
Constructor for values of type signed long long.
Schar-from-integer
Constructor for values of type signed char.
Uint-from-integer-mod
Reduce modularly ACL2 integers to values of type unsigned int.
Uint-from-integer
Constructor for values of type unsigned int.
Uchar
Fixtype of values of type unsigned char.
Schar
Fixtype of values of type signed char.
Ushort
Fixtype of values of type unsigned short.
Ulong
Fixtype of values of type unsigned long.
Ullong
Fixtype of values of type unsigned long long.
Sshort
Fixtype of values of type signed short.
Slong
Fixtype of values of type signed long.
Sllong
Fixtype of values of type signed long long.
Ullong-fix
Fixer for values of type unsigned long long.
Uint
Fixtype of values of type unsigned int.
Uchar-fix
Fixer for values of type unsigned char.
Sint-fix
Fixer for values of type signed int.
Ushort-fix
Fixer for values of type unsigned short.
Ulong-fix
Fixer for values of type unsigned long.
Uint-fix
Fixer for values of type unsigned int.
Sshort-fix
Fixer for values of type signed short.
Slong-fix
Fixer for values of type signed long.
Sllong-fix
Fixer for values of type signed long long.
Schar-fix
Fixer for values of type signed char.
Ushort-list
Fixtype of lists of values of type unsigned short.
Ulong-list
Fixtype of lists of values of type unsigned long.
Ullong-list
Fixtype of lists of values of type unsigned long long.
Uint-list
Fixtype of lists of values of type unsigned int.
Uchar-list
Fixtype of lists of values of type unsigned char.
Sshort-list
Fixtype of lists of values of type signed short.
Slong-list
Fixtype of lists of values of type signed long.
Sllong-list
Fixtype of lists of values of type signed long long.
Sint-list
Fixtype of lists of values of type signed int.
Schar-list
Fixtype of lists of values of type signed char.
Integer-type-to/from-fixtype-theorems
Inversion theorems about the mappings between integer types and fixtype symbols.
*nonchar-integer-fixtypes*
List of the fixtype names of the (supported) C integer types except plain char.