• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Defmacro
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
        • Df
        • Unsigned-byte-p
        • Posp
        • Natp
        • <
        • +
        • Bitp
        • Zero-test-idioms
        • Nat-listp
        • Integerp
        • *
        • -
        • Zp
        • Signed-byte-p
          • Defbyte
            • Defbytelist
            • Defbyte-standard-instances
            • Defbyte-ihs-theorems
            • Defbyte-implementation
              • Defbyte-fn
              • Defbyte-infop
              • Defbyte-check-size
              • Defbyte-fix-support-lemma
              • Defbyte-table
              • Defbyte-macro-definition
              • *defbyte-table-name*
          • Defbytelist
          • Bitops/signed-byte-p
          • Signed-byte-fix
          • Bytep
          • Nibblep
          • Signed-byte-listp
          • Signed-byte-p-logops
          • Ihs/signed-byte-p-lemmas
          • Signed-byte-p*
          • Signed-byte-p-basics
        • Logbitp
        • Sharp-f-reader
        • Expt
        • <=
        • Ash
        • Rationalp
        • =
        • Nfix
        • Logand
        • Floor
        • Random$
        • Integer-listp
        • Complex
        • Numbers-introduction
        • Truncate
        • Code-char
        • Char-code
        • Integer-length
        • Zip
        • Logior
        • Sharp-u-reader
        • Mod
        • Unary--
        • Boole$
        • /
        • Logxor
        • Ifix
        • Lognot
        • Integer-range-p
        • Allocate-fixnum-range
        • ACL2-numberp
        • Sharp-d-reader
        • Mod-expt
        • Ceiling
        • Round
        • Logeqv
        • Fix
        • Explode-nonnegative-integer
        • Max
        • Evenp
        • Zerop
        • Abs
        • Nonnegative-integer-quotient
        • Rfix
        • 1+
        • Pos-listp
        • Signum
        • Rem
        • Real/rationalp
        • Rational-listp
        • >=
        • >
        • Logcount
        • ACL2-number-listp
        • /=
        • Unary-/
        • Realfix
        • Complex/complex-rationalp
        • Logtest
        • Logandc1
        • Logorc1
        • Logandc2
        • Denominator
        • 1-
        • Numerator
        • Logorc2
        • The-number
        • Int=
        • Complex-rationalp
        • Min
        • Lognor
        • Zpf
        • Oddp
        • Minusp
        • Lognand
        • Imagpart
        • Conjugate
        • Realpart
        • Plusp
      • Efficiency
      • Irrelevant-formals
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • <<
      • Primitive
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defbyte-implementation

Defbyte-fn

Events generated by defbyte.

Signature

(defbyte-fn type size signed pred fix equiv parents short long wrld) 
  → 
event

Arguments

wrld — Guard (plist-worldp wrld).

Returns

event — A ACL2::maybe-pseudo-event-formp.

For now we only perform partial validation of the inputs. Future implementations may perform a more thorough validation.

Definitions and Theorems

Function: defbyte-fn

(defun defbyte-fn (type size signed
                        pred fix equiv parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defbyte-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    ((mv size-valid size-value)
     (defbyte-check-size size wrld))
    ((unless size-valid)
     (raise
      "The SIZE input must be ~
                (1) an explicit positive integer value, or ~
                (2) a named constant whose value is a positive integer, or ~
                (3) a call of a nullary function (defined or constrained) ~
                that provably denotes a positive integer; ~
                but it is ~x0 instead."
      size))
    ((unless (booleanp signed))
     (raise
      "The :SIGNED input must be a boolean, ~
                but it is ~x0 instead."
      signed))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp fix))
     (raise
      "The :FIX input must be a symbol, ~
                but it is ~x0 instead."
      fix))
    ((unless (symbolp equiv))
     (raise
      "The :EQUIV input must be a symbol, ~
                but it is ~x0 instead."
      equiv))
    (binpred (if signed 'signed-byte-p
               'unsigned-byte-p))
    (pkg (symbol-package-name type))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (pred (or pred (add-suffix-to-fn type "-P")))
    (fix (or fix (add-suffix-to-fn type "-FIX")))
    (equiv (or equiv (add-suffix-to-fn type "-EQUIV")))
    (booleanp-of-pred (acl2::packn-pos (list 'booleanp-of- pred)
                                       pkg-witness))
    (pred-forward-binpred
         (acl2::packn-pos (list pred '-forward- binpred)
                          pkg-witness))
    (binpred-rewrite-pred
         (acl2::packn-pos (list binpred '-rewrite- pred)
                          pkg-witness))
    (pred-compound-recognizer
      (acl2::packn-pos (list (if signed 'integerp-when- 'natp-when-)
                             pred)
                       pkg-witness))
    (pred-of-fix (acl2::packn-pos (list pred '-of- fix)
                                  pkg-witness))
    (fix-when-pred (acl2::packn-pos (list fix '-when- pred)
                                    pkg-witness))
    (type-size-is-posp (if size-value nil
                         (acl2::packn-pos (list type '-is-posp)
                                          pkg-witness)))
    (pred-additional-theorems
         (add-suffix-to-fn pred "-ADDITIONAL-THEOREMS"))
    (x (intern-in-package-of-symbol "X" pkg-witness))
    (yes/no (intern-in-package-of-symbol "YES/NO" pkg-witness))
    (fixed-x (intern-in-package-of-symbol "FIXED-X" pkg-witness))
    (type-ref
      (concatenate
           'string
           "@(tsee "
           (common-lisp::string-downcase (symbol-package-name type))
           "::"
           (common-lisp::string-downcase (symbol-name type))
           ")"))
    (pred-ref
      (concatenate
           'string
           "@(tsee "
           (common-lisp::string-downcase (symbol-package-name type))
           "::"
           (common-lisp::string-downcase (symbol-name type))
           ")"))
    ((mv lower-bound upper-bound)
     (if signed
      (if size-value (mv (- (expt 2 (1- size-value)))
                         (expt 2 (1- size-value)))
       (mv (cons '-
                 (cons (cons 'expt
                             (cons '2
                                   (cons (cons '1- (cons size 'nil))
                                         'nil)))
                       'nil))
           (cons 'expt
                 (cons '2
                       (cons (cons '1- (cons size 'nil))
                             'nil)))))
      (if size-value (mv 0 (expt 2 size-value))
        (mv 0
            (cons 'expt
                  (cons '2 (cons size 'nil)))))))
    (type-size-is-posp-event?
     (and
      type-size-is-posp
      (cons
       (cons
        'defrule
        (cons
             type-size-is-posp
             (cons (cons 'posp (cons size 'nil))
                   '(:rule-classes (:rewrite :type-prescription)))))
       'nil)))
    (pred-event
     (if
      (function-symbolp pred wrld)
      (cons
       'defsection
       (cons
        pred-additional-theorems
        (cons
         ':parents
         (cons
          (cons pred (cons type 'nil))
          (cons
           ':short
           (cons
            (concatenate 'string
                         "Additional theorems about "
                         pred-ref ".")
            (cons
             (cons
              'defrule
              (cons
               pred-forward-binpred
               (cons
                (cons
                 'implies
                 (cons
                      (cons pred (cons x 'nil))
                      (cons (cons binpred (cons size (cons x 'nil)))
                            'nil)))
                (cons
                 ':rule-classes
                 (cons
                     ':forward-chaining
                     (cons ':in-theory
                           (cons (cons 'quote
                                       (cons (cons pred 'nil) 'nil))
                                 'nil)))))))
             (cons
              (cons
               'defruled
               (cons
                binpred-rewrite-pred
                (cons
                 (cons
                      'equal
                      (cons (cons binpred (cons size (cons x 'nil)))
                            (cons (cons pred (cons x 'nil)) 'nil)))
                 (cons ':in-theory
                       (cons (cons 'quote
                                   (cons (cons pred 'nil) 'nil))
                             'nil)))))
              (cons
               (cons
                'theory-invariant
                (cons
                 (cons
                    'incompatible
                    (cons (cons ':rewrite
                                (cons binpred-rewrite-pred 'nil))
                          (cons (cons ':definition (cons pred 'nil))
                                'nil)))
                 'nil))
               (cons
                (cons
                 'defrule
                 (cons
                  pred-compound-recognizer
                  (cons
                   (cons
                       'implies
                       (cons (cons pred (cons x 'nil))
                             (cons (cons (if signed 'integerp 'natp)
                                         (cons x 'nil))
                                   'nil)))
                   (cons
                    ':rule-classes
                    (cons
                     ':compound-recognizer
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                          pred-forward-binpred
                          '(acl2::unsigned-byte-p-forward-to-nonnegative-integerp
                             acl2::signed-byte-p-forward-to-integerp
                             integerp natp))
                         'nil))
                       'nil)))))))
                'nil))))))))))
      (cons
       'define
       (cons
        pred
        (cons
         (cons x 'nil)
         (cons
          ':returns
          (cons
           (cons
            yes/no
            (cons
             'booleanp
             (cons
              ':name
              (cons
               booleanp-of-pred
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                       (cons pred
                             (cons (cons ':t (cons binpred 'nil))
                                   '(booleanp-compound-recognizer)))
                       'nil))
                     'nil)))
                  'nil)
                 'nil))))))
           (cons
            ':parents
            (cons
             (cons type 'nil)
             (cons
              ':short
              (cons
               (concatenate 'string
                            "Recognizer for " type-ref ".")
               (cons
                (cons
                 'mbe
                 (cons
                  ':logic
                  (cons
                   (cons binpred (cons size (cons x 'nil)))
                   (cons
                    ':exec
                    (cons
                     (cons
                      'and
                      (cons
                       (cons 'integerp (cons x 'nil))
                       (cons
                        (cons '<=
                              (cons lower-bound (cons x 'nil)))
                        (cons
                             (cons '<
                                   (cons x (cons upper-bound 'nil)))
                             'nil))))
                     'nil)))))
                (cons
                 ':guard-hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons
                       'quote
                       (cons
                        (cons
                         binpred
                         (cons
                             'integer-range-p
                             (cons '(:e expt)
                                   (and type-size-is-posp
                                        (list type-size-is-posp)))))
                        'nil))
                      'nil)))
                   'nil)
                  (cons
                   ':no-function
                   (cons
                    't
                    (cons
                     '///
                     (cons
                      (cons
                       'defrule
                       (cons
                        pred-forward-binpred
                        (cons
                         (cons
                          'implies
                          (cons
                           (cons pred (cons x 'nil))
                           (cons
                            (cons binpred (cons size (cons x 'nil)))
                            'nil)))
                         (cons
                          ':rule-classes
                          (cons
                           ':forward-chaining
                           (cons
                            ':in-theory
                            (cons
                                 (cons 'quote
                                       (cons (cons pred 'nil) 'nil))
                                 'nil)))))))
                      (cons
                       (cons
                        'defruled
                        (cons
                         binpred-rewrite-pred
                         (cons
                          (cons
                           'equal
                           (cons
                            (cons binpred (cons size (cons x 'nil)))
                            (cons (cons pred (cons x 'nil)) 'nil)))
                          (cons
                           ':in-theory
                           (cons (cons 'quote
                                       (cons (cons pred 'nil) 'nil))
                                 'nil)))))
                       (cons
                        (cons
                         'theory-invariant
                         (cons
                          (cons
                           'incompatible
                           (cons
                            (cons ':rewrite
                                  (cons binpred-rewrite-pred 'nil))
                            (cons
                                (cons ':definition (cons pred 'nil))
                                'nil)))
                          'nil))
                        (cons
                         (cons
                          'defrule
                          (cons
                           pred-compound-recognizer
                           (cons
                            (cons
                             'implies
                             (cons
                              (cons pred (cons x 'nil))
                              (cons
                                   (cons (if signed 'integerp 'natp)
                                         (cons x 'nil))
                                   'nil)))
                            (cons
                             ':rule-classes
                             (cons
                              ':compound-recognizer
                              (cons
                               ':in-theory
                               (cons
                                (cons
                                 'quote
                                 (cons
                                  (cons
                                   pred-forward-binpred
                                   '(acl2::unsigned-byte-p-forward-to-nonnegative-integerp
                                     acl2::signed-byte-p-forward-to-integerp
                                     integerp natp))
                                  'nil))
                                'nil)))))))
                         'nil)))))))))))))))))))))
    (fix-event
     (cons
      'define
      (cons
       fix
       (cons
        (cons (cons x (cons pred 'nil)) 'nil)
        (cons
         ':returns
         (cons
          (cons
           fixed-x
           (cons
            pred
            (cons
             ':name
             (cons
              pred-of-fix
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                     'quote
                     (cons
                      (cons
                       pred
                       (cons
                         fix
                         (cons binpred
                               '(posp integer-range-p expt (:e expt)
                                      fix zip))))
                      'nil))
                    (and
                     type-size-is-posp
                     (cons
                      ':use
                      (cons
                       (cons
                        type-size-is-posp
                        (cons
                         (cons
                          ':instance
                          (cons
                            'defbyte-fix-support-lemma
                            (cons (cons 'z (cons size 'nil)) 'nil)))
                         'nil))
                       'nil))))))
                 'nil)
                'nil))))))
          (cons
           ':parents
           (cons
            (cons type 'nil)
            (cons
             ':short
             (cons
              (concatenate 'string
                           "Fixer for " type-ref ".")
              (cons
               (cons
                   'mbe
                   (cons ':logic
                         (cons (cons 'if
                                     (cons (cons pred (cons x 'nil))
                                           (cons x '(0))))
                               (cons ':exec (cons x 'nil)))))
               (cons
                ':no-function
                (cons
                 't
                 (cons
                  '///
                  (cons
                   (cons
                    'defrule
                    (cons
                     fix-when-pred
                     (cons
                      (cons
                       'implies
                       (cons
                          (cons pred (cons x 'nil))
                          (cons (cons 'equal
                                      (cons (cons fix (cons x 'nil))
                                            (cons x 'nil)))
                                'nil)))
                      (cons ':in-theory
                            (cons (cons 'quote
                                        (cons (cons fix 'nil) 'nil))
                                  'nil)))))
                   'nil)))))))))))))))
    (type-event
     (cons
      'defsection
      (cons
       type
       (append
        (and parents (list :parents parents))
        (append
         (and short (list :short short))
         (append
          (and long (list :long long))
          (cons
           (cons
            'deffixtype
            (cons
             type
             (cons
              ':pred
              (cons
               pred
               (cons
                ':fix
                (cons
                   fix
                   (cons ':equiv
                         (cons equiv '(:define t :forward t)))))))))
           'nil)))))))
    (table-event
     (cons
      'table
      (cons
          *defbyte-table-name*
          (cons (cons 'quote (cons type 'nil))
                (cons (cons 'quote
                            (cons (make-defbyte-info :size size
                                                     :signed signed)
                                  'nil))
                      'nil))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (append
          type-size-is-posp-event?
          (cons '(acl2::evmac-prepare-proofs)
                (cons pred-event
                      (cons fix-event
                            (cons type-event
                                  (cons table-event 'nil))))))))))))