• 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
        • 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*
        • Defresult
        • Fold
        • Defsubtype
        • Defset
        • Specific-types
        • Defflatsum
        • Deflist-of-len
        • Pos-list
        • Defbytelist
        • Defomap
        • Defbyte-standard-instances
        • Deffixtype-alias
        • Defbytelist-standard-instances
        • Defunit
        • Byte-list
        • Byte
        • Database
        • Pos-option
        • Nibble
        • Nat-option
        • String-option
        • Byte-list20
        • Byte-list32
        • Byte-list64
        • Pseudo-event-form
        • Natoption/natoptionlist
        • Nati
        • Character-list
        • Nat/natlist
        • Maybe-string
        • Nibble-list
        • Natoption/natoptionlist-result
        • Nat/natlist-result
        • Nat-option-list-result
        • Set
        • String-result
        • String-list-result
        • Nat-result
        • Nat-option-result
        • Nat-list-result
        • Maybe-string-result
        • Integer-result
        • Character-result
        • Character-list-result
        • Boolean-result
        • Map
        • Bag
        • Pos-set
        • Hex-digit-char-list
        • Dec-digit-char-list
        • Pseudo-event-form-list
        • Nat-option-list
        • Symbol-set
        • String-set
        • Nat-set
        • Oct-digit-char-list
        • Bin-digit-char-list
        • Bit-list
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • 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

• 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))))))))))))