• 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
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
              • Uinteger-bit-roles-for-sinteger-bit-roles
              • Sinteger-bit-roles-for-uinteger-bit-roles
              • Integer-format
              • Schar-format
              • Uinteger-sinteger-bit-roles-wfp
              • Sinteger-format
              • Integer-format-llong-wfp
              • Integer-format-short-wfp
              • Integer-format-long-wfp
              • Integer-format-int-wfp
              • Uinteger-format
                • Uinteger-format-fix
                • Uinteger-format-equiv
                • Make-uinteger-format
                • Uinteger-format->bits
                • Change-uinteger-format
                • Uinteger-format->traps
                • Uinteger-formatp
              • Schar-format->min
              • Char+short+int+long+llong-format
              • Uchar-format
              • Char-format->min
              • Integer-format-inc-sign-tcnpnt
              • Char-format->max
              • Sinteger-format->min
              • Sinteger-bit-role
              • Sinteger-bit-roles-wfp
              • Schar-format->max
              • Signed-format
              • Short-format-16tcnt
              • Llong-format-64tcnt
              • Ienv
              • Uinteger-bit-roles-wfp
              • Uinteger-bit-role
              • Long-format-32tcnt
              • Int-format-16tcnt
              • Uinteger+sinteger-format
              • Uinteger-bit-roles-value-count
              • Sinteger-bit-roles-value-count
              • Sinteger-bit-roles-inc-n-and-sign
              • Uinteger-bit-roles-inc-n
              • Sinteger-format-inc-sign-tcnpnt
              • Sinteger-bit-roles-inc-n
              • Uchar-format->max
              • Char+short+int+long+llong-format-wfp
              • Uinteger-bit-roles-exponents
              • Sinteger-bit-roles-exponents
              • Integer-format->bit-size
              • Char-format
              • Sinteger-bit-roles-sign-count
              • Ienv->char-min
              • Uinteger-format-inc-npnt
              • Ienv->schar-min
              • Ienv->char-size
              • Ienv->char-max
              • Uinteger-format->max
              • Sinteger-format->max
              • Ienv->schar-max
              • Ienv->uchar-max
              • Ienv->short-bit-size
              • Ienv->long-bit-size
              • Ienv->llong-bit-size
              • Schar-format-8tcnt
              • Ienv->int-bit-size
              • Char-format-8u
              • Char8+short16+int16+long32+llong64-tcnt
              • Uchar-format-8
              • Uinteger-bit-role-list
              • Sinteger-bit-role-list
              • Uinteger-sinteger-bit-roles-wfp-of-inc-n-and-sign
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • 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
  • Implementation-environments

Uinteger-format

Fixtype of formats of unsigned integer objects.

This is a product type introduced by fty::defprod.

Fields
bits — uinteger-bit-role-list
traps
Additional Requirements

The following invariant is enforced on the fields:

(uinteger-bit-roles-wfp bits)

This is for unsigned integer objects other than those of type unsigned char, which are covered by uchar-format. See [C17:6.2.6.2./1].

The format definition includes a list of bit roles, which should be thought as the juxtaposition of the bytes that form the unsigned integer object, in little endian order, i.e. from lower to higher address. The length of the list of bit roles must be a mulitple of CHAR_BIT, which we capture in uchar-format: we express this constraint elsewhere, because we do not have that value available here. The list of bit roles must be well-formed.

We also include a placeholder component meant to define which bit values are trap representations [C17:6.2.6.2/5]. We plan to flesh this out in the future.

Subtopics

Uinteger-format-fix
Fixing function for uinteger-format structures.
Uinteger-format-equiv
Basic equivalence relation for uinteger-format structures.
Make-uinteger-format
Basic constructor macro for uinteger-format structures.
Uinteger-format->bits
Get the bits field from a uinteger-format.
Change-uinteger-format
Modifying constructor for uinteger-format structures.
Uinteger-format->traps
Get the traps field from a uinteger-format.
Uinteger-formatp
Recognizer for uinteger-format structures.