• 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
      • Soft
      • Bv
      • Imp-language
      • 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
            • Ullongp
            • Ucharp
            • Sintp
            • 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
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Representation-of-integers

Def-integer-values

Event to generate the model of the values of a C integer type.

Signature

(def-integer-values type) → event

Arguments

type — Guard (typep type).

Returns

event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: def-integer-values

(defun def-integer-values (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'def-integer-values))
  (declare (ignorable __function__))
  (b* ((type-string (integer-type-xdoc-string type))
       (signedp (type-signed-integerp type))
       (<type> (integer-type-to-fixtype type))
       (<type>p (pack <type> 'p))
       (<type>-fix (pack <type> '-fix))
       (<type>-fix-when-<type>p (pack <type>-fix '-when- <type>p))
       (<type>-equiv (pack <type> '-equiv))
       (<type>-integer (pack <type> '-integer))
       (<type>-integerp (pack <type>-integer 'p))
       (<type>-integerp-alt-def (pack <type>-integerp '-alt-def))
       (<type>-integer-list (pack <type>-integer '-list))
       (<type>-integer-listp (pack <type>-integer-list 'p))
       (<type>-integer-list-fix (pack <type>-integer-list '-fix))
       (<type>-integer-fix (pack <type>-integer '-fix))
       (<type>-max (pack <type> '-max))
       (<type>-min (pack <type> '-min))
       (integer-from-<type> (pack 'integer-from- <type>))
       (<type>-from-integer (pack <type> '-from-integer))
       (<type>-from-integer-of-integer-from-<type>
            (pack <type>-from-integer '-of-
                  integer-from-<type>))
       (integer-from-<type>-of-<type>-from-integer
            (pack integer-from-<type> '-of-
                  <type>-from-integer))
       (equal-of-<type>-from-integer
            (pack 'equal-of- <type>-from-integer))
       (consp-when-<type>p (pack 'consp-when- <type>p))
       (<type>-list (pack <type> '-list))
       (<type>-listp (pack <type>-list 'p))
       (<type>-list-fix (pack <type>-list '-fix))
       (integer-list-from-<type>-list
            (pack 'integer-list-from- <type>-list))
       (<type>-list-from-integer-list
            (pack <type>-list '-from-integer-list))
       (<type>-list-from-integer-list-of-integer-list-from-<type>-list
            (pack <type>-list-from-integer-list '-of-
                  integer-list-from-<type>-list))
       (integer-list-from-<type>-list-of-<type>-list-from-integer-list
            (pack integer-list-from-<type>-list '-of-
                  <type>-list-from-integer-list))
       (<type>-from-integer-mod (pack <type>-from-integer '-mod))
       (true-listp-when-<type>-listp-rewrite
            (pack 'true-listp-when-
                  <type>-listp '-rewrite)))
   (cons
    'progn
    (append
     (and (type-case type :char)
          (raise "Type ~x0 not supported." type))
     (cons
      (cons
       'define
       (cons
        <type>p
        (cons
         '(x)
         (cons
          ':returns
          (cons
           '(yes/no booleanp)
           (cons
            ':short
            (cons
             (str::cat "Recognizer of values of "
                       type-string ".")
             (cons
              (cons
               'and
               (cons
                '(consp x)
                (cons
                 (cons 'eq
                       (cons '(car x)
                             (cons (type-kind type) 'nil)))
                 (cons
                  '(true-listp (cdr x))
                  (cons
                   '(eql (len (cdr x)) 1)
                   (cons
                     (cons 'b*
                           (cons '((get (std::da-nth 0 (cdr x))))
                                 (cons (cons <type>-integerp '(get))
                                       'nil)))
                     'nil))))))
              (cons
               '///
               (cons
                (cons
                 'defrule
                 (cons
                  consp-when-<type>p
                  (cons
                      (cons 'implies
                            (cons (cons <type>p '(x)) '((consp x))))
                      '(:rule-classes :compound-recognizer))))
                'nil))))))))))
      (cons
       (cons
        'define
        (cons
         <type>-fix
         (cons
          (cons (cons 'x (cons <type>p 'nil))
                'nil)
          (cons
           ':returns
           (cons
            (cons 'fixed-x (cons <type>p 'nil))
            (cons
             ':short
             (cons
              (str::cat "Fixer for values of " type-string ".")
              (cons
               (cons
                'mbe
                (cons
                 ':logic
                 (cons
                  (cons
                   'b*
                   (cons
                    (cons
                       (cons 'get
                             (cons (cons <type>-integer-fix
                                         '((std::da-nth 0 (cdr x))))
                                   'nil))
                       'nil)
                    (cons
                        (cons 'cons
                              (cons (type-kind type) '((list get))))
                        'nil)))
                  '(:exec x))))
               (cons
                ':prepwork
                (cons
                 (cons
                  (cons
                   'local
                   (cons
                      (cons 'in-theory
                            (cons (cons 'enable (cons <type>p 'nil))
                                  'nil))
                      'nil))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'defrule
                    (cons
                     <type>-fix-when-<type>p
                     (cons
                      (cons
                       'implies
                       (cons
                        (cons <type>p '(x))
                        (cons
                           (cons 'equal
                                 (cons (cons <type>-fix '(x)) '(x)))
                           'nil)))
                      'nil)))
                   'nil))))))))))))
       (cons
        (cons
         'defsection
         (cons
          <type>
          (cons
           ':short
           (cons
            (str::cat "Fixtype of values of " type-string ".")
            (cons
             (cons
              'fty::deffixtype
              (cons
               <type>
               (cons
                ':pred
                (cons
                 <type>p
                 (cons
                  ':fix
                  (cons
                   <type>-fix
                   (cons
                    ':equiv
                    (cons
                     <type>-equiv
                     (cons
                          ':define
                          (cons 't
                                (cons ':topic
                                      (cons <type>p 'nil))))))))))))
             'nil)))))
        (cons
         (cons
          'define
          (cons
           <type>-from-integer
           (cons
            (cons (cons 'get (cons <type>-integerp 'nil))
                  'nil)
            (cons
             ':returns
             (cons
              (cons
               'y
               (cons
                <type>p
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                      '"Goal"
                      (cons ':in-theory
                            (cons (cons 'enable (cons <type>p 'nil))
                                  'nil)))
                   'nil)
                  'nil))))
              (cons
               ':short
               (cons
                (str::cat "Constructor for values of "
                          type-string ".")
                (cons
                 (cons
                  'b*
                  (cons
                   (cons
                    (cons
                     'get
                     (cons
                      (cons
                        'mbe
                        (cons ':logic
                              (cons (cons <type>-integer-fix '(get))
                                    '(:exec get))))
                      'nil))
                    'nil)
                   (cons
                        (cons 'cons
                              (cons (type-kind type) '((list get))))
                        'nil)))
                 '(:hooks (:fix))))))))))
         (cons
          (cons
           'define
           (cons
            integer-from-<type>
            (cons
             (cons (cons 'x (cons <type>p 'nil))
                   'nil)
             (cons
              ':returns
              (cons
               (cons 'y (cons <type>-integerp 'nil))
               (cons
                ':short
                (cons
                 (str::cat "Accessor for values of "
                           type-string ".")
                 (cons
                  (cons
                   'mbe
                   (cons
                    ':logic
                    (cons
                     (cons
                       'b*
                       (cons '((x (and t x)))
                             (cons (cons <type>-integer-fix
                                         '((std::da-nth 0 (cdr x))))
                                   'nil)))
                     '(:exec (std::da-nth 0 (cdr x))))))
                  (cons
                   ':prepwork
                   (cons
                    (cons
                     (cons
                      'local
                      (cons
                       (cons
                        'in-theory
                        (cons
                         (cons
                              'enable
                              (cons <type>p (cons <type>-fix 'nil)))
                         'nil))
                       'nil))
                     'nil)
                    (cons
                     ':hooks
                     (cons
                      '(:fix)
                      (cons
                       '///
                       (cons
                        (cons
                         'defrule
                         (cons
                          <type>-from-integer-of-integer-from-<type>
                          (cons
                           (cons
                            'equal
                            (cons
                             (cons
                               <type>-from-integer
                               (cons (cons integer-from-<type> '(x))
                                     'nil))
                             (cons (cons <type>-fix '(x)) 'nil)))
                           (cons ':enable
                                 (cons (cons <type>-from-integer
                                             (cons <type>-fix 'nil))
                                       'nil)))))
                        (cons
                         (cons
                          'defrule
                          (cons
                           integer-from-<type>-of-<type>-from-integer
                           (cons
                            (cons
                             'equal
                             (cons
                              (cons
                               integer-from-<type>
                               (cons
                                   (cons <type>-from-integer '(get))
                                   'nil))
                              (cons (cons <type>-integer-fix '(get))
                                    'nil)))
                            (cons
                                 ':enable
                                 (cons <type>-from-integer 'nil)))))
                         (cons
                          (cons
                           'defrule
                           (cons
                            (pack integer-from-<type> '-upper-bound)
                            (cons
                             (cons
                              '<=
                              (cons
                                (cons integer-from-<type> '(x))
                                (cons (cons <type>-max 'nil) 'nil)))
                             (cons
                              ':rule-classes
                              (cons
                               ':linear
                               (cons
                                ':enable
                                (cons
                                 (cons
                                  integer-from-<type>
                                  (cons
                                   <type>-integer-fix
                                   (cons
                                     <type>-integerp-alt-def 'nil)))
                                 'nil)))))))
                          (and
                           signedp
                           (cons
                            (cons
                             'defrule
                             (cons
                              (pack
                                  integer-from-<type> '-lower-bound)
                              (cons
                               (cons
                                '>=
                                (cons
                                     (cons integer-from-<type> '(x))
                                     (cons (cons <type>-min 'nil)
                                           'nil)))
                               (cons
                                ':rule-classes
                                (cons
                                 ':linear
                                 (cons
                                  ':enable
                                  (cons
                                   (cons
                                    integer-from-<type>
                                    (cons
                                       <type>-integer-fix
                                       (cons <type>-integerp-alt-def
                                             'nil)))
                                   'nil)))))))
                            'nil))))))))))))))))))
          (cons
           (cons
            'defruled
            (cons
             equal-of-<type>-from-integer
             (cons
              (cons
               'equal
               (cons
                (cons 'equal
                      (cons (cons <type>-from-integer '(get))
                            '(x)))
                (cons
                 (cons
                  'and
                  (cons
                   (cons <type>p '(x))
                   (cons
                    (cons
                        'equal
                        (cons (cons integer-from-<type> '(x))
                              (cons (cons <type>-integer-fix '(get))
                                    'nil)))
                    'nil)))
                 'nil)))
              (cons
                 ':enable
                 (cons (cons <type>-from-integer
                             (cons <type>p
                                   (cons integer-from-<type> 'nil)))
                       'nil)))))
           (append
            (and
             (not signedp)
             (cons
              (cons
               'define
               (cons
                <type>-from-integer-mod
                (cons
                 '((x integerp))
                 (cons
                  ':returns
                  (cons
                   (cons 'result (cons <type>p 'nil))
                   (cons
                    ':short
                    (cons
                     (str::cat
                      "Reduce modularly ACL2 integers to values of "
                      type-string ".")
                     (cons
                      (cons
                       <type>-from-integer
                       (cons
                        (cons
                         'mod
                         (cons
                          '(ifix x)
                          (cons
                           (cons '1+
                                 (cons (cons <type>-max 'nil) 'nil))
                           'nil)))
                        'nil))
                      (cons
                       ':guard-hints
                       (cons
                        (cons
                         (cons
                          '"Goal"
                          (cons
                           ':in-theory
                           (cons
                            (cons
                                'enable
                                (cons <type>-integerp-alt-def 'nil))
                            'nil)))
                         'nil)
                        '(:hooks (:fix))))))))))))
              'nil))
            (cons
             (cons
              'fty::deflist
              (cons
               <type>-list
               (cons
                ':short
                (cons
                 (str::cat "Fixtype of lists of values of "
                           type-string ".")
                 (cons
                  ':elt-type
                  (cons
                   <type>
                   (cons
                    ':true-listp
                    (cons
                     't
                     (cons
                      ':elementp-of-nil
                      (cons
                       'nil
                       (cons
                        ':pred
                        (cons
                         <type>-listp
                         (cons
                          ':prepwork
                          (cons
                           '((local (in-theory (enable nfix))))
                           (cons
                            '///
                            (cons
                             (cons
                              'defruled
                              (cons
                               true-listp-when-<type>-listp-rewrite
                               (cons
                                (cons 'implies
                                      (cons (cons <type>-listp '(x))
                                            '((true-listp x))))
                                'nil)))
                             'nil))))))))))))))))
             (cons
              (cons
               'std::defprojection
               (cons
                integer-list-from-<type>-list
                (cons
                 (cons (cons 'x (cons <type>-listp 'nil))
                       'nil)
                 (cons
                  ':returns
                  (cons
                   (cons 'result
                         (cons <type>-integer-listp 'nil))
                   (cons
                    ':short
                    (cons
                     (str::cat
                          "Lift @(tsee "
                          (str::downcase-string
                               (symbol-name integer-from-<type>))
                          ") to lists.")
                     (cons
                      (cons integer-from-<type> '(x))
                      (cons
                       '///
                       (cons
                        (cons
                          'fty::deffixequiv
                          (cons integer-list-from-<type>-list 'nil))
                        'nil))))))))))
              (cons
               (cons
                'std::defprojection
                (cons
                 <type>-list-from-integer-list
                 (cons
                  (cons (cons 'x
                              (cons <type>-integer-listp 'nil))
                        'nil)
                  (cons
                   ':returns
                   (cons
                    (cons 'result (cons <type>-listp 'nil))
                    (cons
                     ':short
                     (cons
                      (str::cat
                         "Lift @(tsee "
                         (str::downcase-string (symbol-name <type>))
                         ") to lists.")
                      (cons
                       (cons <type>-from-integer '(x))
                       (cons
                        '///
                        (cons
                         (cons
                          'fty::deffixequiv
                          (cons <type>-list-from-integer-list 'nil))
                         'nil))))))))))
               (cons
                (cons
                 'defrule
                 (cons
                  <type>-list-from-integer-list-of-integer-list-from-<type>-list
                  (cons
                   (cons
                    'equal
                    (cons
                     (cons
                      <type>-list-from-integer-list
                      (cons
                           (cons integer-list-from-<type>-list '(x))
                           'nil))
                     (cons (cons <type>-list-fix '(x))
                           'nil)))
                   (cons
                    ':induct
                    (cons
                     't
                     (cons
                      ':enable
                      (cons
                       (cons
                          integer-list-from-<type>-list
                          (cons <type>-list-from-integer-list 'nil))
                       'nil)))))))
                (cons
                 (cons
                  'defrule
                  (cons
                   integer-list-from-<type>-list-of-<type>-list-from-integer-list
                   (cons
                    (cons
                     'equal
                     (cons
                      (cons
                       integer-list-from-<type>-list
                       (cons
                           (cons <type>-list-from-integer-list '(x))
                           'nil))
                      (cons (cons <type>-integer-list-fix '(x))
                            'nil)))
                    (cons
                     ':induct
                     (cons
                      't
                      (cons
                       ':enable
                       (cons
                        (cons
                          integer-list-from-<type>-list
                          (cons <type>-list-from-integer-list 'nil))
                        'nil)))))))
                 'nil)))))))))))))))))

Theorem: pseudo-event-formp-of-def-integer-values

(defthm pseudo-event-formp-of-def-integer-values
  (b* ((event (def-integer-values type)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: def-integer-values-of-type-fix-type

(defthm def-integer-values-of-type-fix-type
  (equal (def-integer-values (type-fix type))
         (def-integer-values type)))

Theorem: def-integer-values-type-equiv-congruence-on-type

(defthm def-integer-values-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (def-integer-values type)
                  (def-integer-values type-equiv)))
  :rule-classes :congruence)