• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
              • Schar-format
              • Uinteger-sinteger-bit-roles-wfp
              • Integer-format
              • Sinteger-format
              • Integer-format-llong-wfp
                • Integer-format-short-wfp
                • Integer-format-long-wfp
                • Integer-format-int-wfp
                • Uinteger-format
                • Char+short+int+long+llong-format
                • Sinteger-format->min
                • Schar-format->min
                • Uchar-format
                • Char-format->min
                • Integer-format-inc-sign-tcnpnt
                • Char-format->max
                • Sinteger-bit-role
                • Sinteger-bit-roles-wfp
                • Schar-format->max
                • Signed-format
                • Short-format-16tcnt
                • Llong-format-64tcnt
                • Ienv
                • Uinteger-bit-role
                • Long-format-32tcnt
                • Int-format-16tcnt
                • Uinteger-bit-roles-wfp
                • Uinteger+sinteger-format
                • Sinteger-bit-roles-value-count
                • Uinteger-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-format->max
                • Sinteger-bit-roles-exponents
                • Char-format
                • Integer-format->bit-size
                • Uinteger-format->max
                • Sinteger-bit-roles-sign-count
                • Integer-format->signed-min
                • Uinteger-format-inc-npnt
                • Integer-format->unsigned-max
                • Integer-format->signed-max
                • Ienv->schar-min
                • Ienv->char-size
                • Ienv->char-min
                • Ienv->char-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
                • Ienv->sshort-min
                • Ienv->sllong-min
                • Char-format-8u
                • Ienv->ushort-max
                • Ienv->ulong-max
                • Ienv->ullong-max
                • Ienv->uint-max
                • Ienv->sshort-max
                • Ienv->slong-min
                • Ienv->slong-max
                • Ienv->sllong-max
                • Ienv->sint-min
                • Ienv->sint-max
                • 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

    Integer-format-llong-wfp

    Check if an integer format is well-formed when used for (signed and unsigned) long long.

    Signature
    (integer-format-llong-wfp llong-format uchar-format long-format) 
      → 
    yes/no
    Arguments
    llong-format — Guard (integer-formatp llong-format).
    uchar-format — Guard (uchar-formatp uchar-format).
    long-format — Guard (integer-formatp long-format).
    Returns
    yes/no — Type (booleanp yes/no).

    The number of bits must be a multiple of CHAR_BIT [C17:6.2.6.1/4].

    The possible signed values must cover at least the range from -9223372036854775807 to +9223372036854775807 (both inclusive) [C17:5.2.4.2.1/1]. The possible unsigned values must cover at least the range from 0 to 18446744073709551615 (both inclusive) [C17:5.2.4.2.1/1].

    The possible signed values must at least include those of signed long, and the possible unsigned values must at least include those of unsigned long [C17:6.2.5/8].

    Definitions and Theorems

    Function: integer-format-llong-wfp

    (defun integer-format-llong-wfp
           (llong-format uchar-format long-format)
     (declare (xargs :guard (and (integer-formatp llong-format)
                                 (uchar-formatp uchar-format)
                                 (integer-formatp long-format))))
     (let ((__function__ 'integer-format-llong-wfp))
      (declare (ignorable __function__))
      (b*
       ((bit-size (integer-format->bit-size llong-format))
        (signed-llong-min (integer-format->signed-min llong-format))
        (signed-llong-max (integer-format->signed-max llong-format))
        (unsigned-llong-max (integer-format->unsigned-max llong-format))
        (signed-long-min (integer-format->signed-min long-format))
        (signed-long-max (integer-format->signed-max long-format))
        (unsigned-long-max (integer-format->unsigned-max long-format)))
       (and (integerp (/ bit-size
                         (uchar-format->size uchar-format)))
            (<= signed-llong-min -9223372036854775807)
            (<= 9223372036854775807 signed-llong-max)
            (<= 18446744073709551615 unsigned-llong-max)
            (<= signed-llong-min signed-long-min)
            (<= signed-long-max signed-llong-max)
            (<= unsigned-long-max
                unsigned-llong-max)))))

    Theorem: booleanp-of-integer-format-llong-wfp

    (defthm booleanp-of-integer-format-llong-wfp
      (b* ((yes/no (integer-format-llong-wfp
                        llong-format uchar-format long-format)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: integer-format-llong-wfp-of-integer-format-fix-llong-format

    (defthm integer-format-llong-wfp-of-integer-format-fix-llong-format
     (equal
      (integer-format-llong-wfp (integer-format-fix llong-format)
                                uchar-format long-format)
      (integer-format-llong-wfp llong-format uchar-format long-format)))

    Theorem: integer-format-llong-wfp-integer-format-equiv-congruence-on-llong-format

    (defthm
     integer-format-llong-wfp-integer-format-equiv-congruence-on-llong-format
     (implies
      (integer-format-equiv llong-format llong-format-equiv)
      (equal
        (integer-format-llong-wfp llong-format uchar-format long-format)
        (integer-format-llong-wfp llong-format-equiv
                                  uchar-format long-format)))
     :rule-classes :congruence)

    Theorem: integer-format-llong-wfp-of-uchar-format-fix-uchar-format

    (defthm integer-format-llong-wfp-of-uchar-format-fix-uchar-format
     (equal
      (integer-format-llong-wfp llong-format
                                (uchar-format-fix uchar-format)
                                long-format)
      (integer-format-llong-wfp llong-format uchar-format long-format)))

    Theorem: integer-format-llong-wfp-uchar-format-equiv-congruence-on-uchar-format

    (defthm
     integer-format-llong-wfp-uchar-format-equiv-congruence-on-uchar-format
     (implies
      (uchar-format-equiv uchar-format uchar-format-equiv)
      (equal
        (integer-format-llong-wfp llong-format uchar-format long-format)
        (integer-format-llong-wfp llong-format
                                  uchar-format-equiv long-format)))
     :rule-classes :congruence)

    Theorem: integer-format-llong-wfp-of-integer-format-fix-long-format

    (defthm integer-format-llong-wfp-of-integer-format-fix-long-format
     (equal
      (integer-format-llong-wfp llong-format uchar-format
                                (integer-format-fix long-format))
      (integer-format-llong-wfp llong-format uchar-format long-format)))

    Theorem: integer-format-llong-wfp-integer-format-equiv-congruence-on-long-format

    (defthm
     integer-format-llong-wfp-integer-format-equiv-congruence-on-long-format
     (implies
      (integer-format-equiv long-format long-format-equiv)
      (equal
        (integer-format-llong-wfp llong-format uchar-format long-format)
        (integer-format-llong-wfp llong-format
                                  uchar-format long-format-equiv)))
     :rule-classes :congruence)