• 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
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
              • Convert-integer-value
              • Result-integer-value
              • Uaconvert-values
              • Bitnot-integer-value
              • Bitand-integer-values
              • Promote-value
              • Rem-integer-values
              • Shr-integer-values
              • Shl-integer-values
              • Div-integer-values
              • Bitxor-integer-values
              • Bitior-integer-values
              • Value-integer
              • Sub-integer-values
              • Mul-integer-values
              • Add-integer-values
              • Ne-integer-values
              • Lt-integer-values
              • Le-integer-values
              • Gt-integer-values
              • Ge-integer-values
              • Eq-integer-values
              • Minus-integer-value
              • Plus-integer-value
              • Value-integer->get
                • Lognot-integer-value
                • Test-integer-value
                • Value-integer-and-value-integer->get
              • 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
    • Integer-operations

    Value-integer->get

    Turn a C integer value into a mathematical (i.e. ACL2) integer.

    Signature
    (value-integer->get val) → mathint
    Arguments
    val — Guard (valuep val).
    Returns
    mathint — Type (integerp mathint).

    Definitions and Theorems

    Function: value-integer->get

    (defun value-integer->get (val)
      (declare (xargs :guard (valuep val)))
      (declare (xargs :guard (value-integerp val)))
      (let ((__function__ 'value-integer->get))
        (declare (ignorable __function__))
        (value-case val
                    :uchar val.get
                    :schar val.get
                    :ushort val.get
                    :sshort val.get
                    :uint val.get
                    :sint val.get
                    :ulong val.get
                    :slong val.get
                    :ullong val.get
                    :sllong val.get
                    :pointer (ifix (impossible))
                    :array (ifix (impossible))
                    :struct (ifix (impossible)))))

    Theorem: integerp-of-value-integer->get

    (defthm integerp-of-value-integer->get
      (b* ((mathint (value-integer->get val)))
        (integerp mathint))
      :rule-classes :rewrite)

    Theorem: value-integer->get-bounds

    (defthm value-integer->get-bounds
      (and (<= (integer-type-min (type-of-value val))
               (value-integer->get val))
           (<= (value-integer->get val)
               (integer-type-max (type-of-value val))))
      :rule-classes
      ((:linear :trigger-terms ((value-integer->get val)))))

    Theorem: value-integer->get-of-value-fix-val

    (defthm value-integer->get-of-value-fix-val
      (equal (value-integer->get (value-fix val))
             (value-integer->get val)))

    Theorem: value-integer->get-value-equiv-congruence-on-val

    (defthm value-integer->get-value-equiv-congruence-on-val
      (implies (value-equiv val val-equiv)
               (equal (value-integer->get val)
                      (value-integer->get val-equiv)))
      :rule-classes :congruence)