		Search-engine friendly clone of the ACL2 documentation.
Definterface-hmac-implementation
Definterface-hmac-fn

Events generated by definterface-hmac.
Signature
(definterface-hmac-fn name hash block-size topic parents short long wrld) → event?
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event? — A ACL2::maybe-pseudo-event-formp.
Definitions and Theorems

Function: definterface-hmac-fn
(defun definterface-hmac-fn (name hash block-size
                                  topic parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'definterface-hmac-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but is it ~x0 instead."
      name))
    ((unless (symbolp hash))
     (raise
      "The :HASH input must be a symbol, ~
                but it is ~x0 instead."
      hash))
    (table (table-alist *definterface-hash-table-name* wrld)
)
    (pair (assoc-eq hash table))
    ((unless pair)
     (raise
      "The :HASH input ~x0 must name ~
                an existing hash function interface ~
                introduced via DEFINTERFACE-HASH, ~
                but this is not the case."
      hash))
    (info (cdr pair))
    (input-size-limit
         (definterface-hash-info->input-size-limit info))
    (input-size-limit-/-8 (and input-size-limit
                               (/ input-size-limit 8)))
    (output-size (definterface-hash-info->output-size info))
    (output-size-/-8 (/ output-size 8))
    ((when (and input-size-limit
                (not (posp block-size))))
     (raise
      "Since the hash function ~x0 has an input size limit, ~
                the :BLOCK-SIZE input must be a positive integer, ~
                but it is ~x1 instead."
      hash block-size))
    ((when (and (not input-size-limit) block-size))
     (raise
      "Since the hash function ~x0 has no input size limit, ~
                the :BLOCK-SIZE input must be absent, ~
                but it is ~x1 instead."
      hash block-size))
    ((unless (symbolp topic))
     (raise
      "The :TOPIC input must be a symbol, ~
                but it is ~x0 instead."
      topic))
    (pkg (symbol-package-name name))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (topic (or topic
               (add-suffix-to-fn name "-INTERFACE")))
    (byte-listp-thm-name (acl2::packn-pos (list 'byte-list-of- name)
                                          pkg-witness))
    (len-thm-name (acl2::packn-pos (list 'len-of- name)
                                   pkg-witness))
    (true-listp-thm-name
         (acl2::packn-pos (list 'true-listp-of- name)
                          pkg-witness))
    (consp-thm-name (acl2::packn-pos (list 'consp-of- name)
                                     pkg-witness))
    (guard
     (if input-size-limit
      (cons
       'and
       (cons
        '(byte-listp key)
        (cons
         (cons '<
               (cons '(len key)
                     (cons input-size-limit-/-8 'nil)))
         (cons
          '(byte-listp text)
          (cons
              (cons '<
                    (cons '(len text)
                          (cons (cons '-
                                      (cons input-size-limit-/-8
                                            (cons block-size 'nil)))
                                'nil)))
              'nil)))))
      '(and (byte-listp key)
            (byte-listp text))))
    (sig
     (cons
      (cons name '(* *))
      (cons '=>
            (cons '*
                  (cons ':formals
                        (cons '(key text)
                              (cons ':guard (cons guard 'nil))))))))
    (wit
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         name
         (cons
          '(key text)
          (cons
           '(declare (ignore key text))
           (cons (cons 'make-list
                       (cons output-size-/-8 '(:initial-element 0)))
                 'nil)))))
       'nil)))
    (byte-listp-thm
        (cons 'defrule
              (cons byte-listp-thm-name
                    (cons (cons 'byte-listp
                                (cons (cons name '(key text)) 'nil))
                          'nil))))
    (len-thm
     (cons
      'defrule
      (cons
        len-thm-name
        (cons (cons 'equal
                    (cons (cons 'len
                                (cons (cons name '(key text)) 'nil))
                          (cons output-size-/-8 'nil)))
              'nil))))
    (fix-thms
        (cons 'fty::deffixequiv
              (cons name
                    '(:args ((key byte-listp) (text byte-listp))))))
    (true-listp-thm
     (cons
      'defrule
      (cons
       true-listp-thm-name
       (cons
        (cons 'true-listp
              (cons (cons name '(key text)) 'nil))
        '(:rule-classes
           :type-prescription
           :enable
           acl2::true-listp-when-byte-listp-compound-recognizer)))))
    (consp-thm
     (cons
      'defrule
      (cons
       consp-thm-name
       (cons
        (cons 'consp
              (cons (cons name '(key text)) 'nil))
        (cons
           ':rule-classes
           (cons ':type-prescription
                 (cons ':use
                       (cons len-thm-name
                             (cons ':disable
                                   (cons len-thm-name 'nil))))))))))
    (table-event
     (cons
      'table
      (cons
       *definterface-hmac-table-name*
       (cons
         (cons 'quote (cons name 'nil))
         (cons (cons 'quote
                     (cons (make-definterface-hmac-info
                                :key-size-limit input-size-limit-/-8
                                :block-size block-size
                                :output-size output-size-/-8)
                           'nil))
               'nil))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (cons
       (cons
        'defsection
        (cons
         topic
         (append
          (and parents (list :parents parents))
          (append
           (and short (list :short short))
           (append
            (and long (list :long long))
            (cons
             (cons
              'encapsulate
              (cons
                 (cons sig 'nil)
                 (cons wit
                       (cons byte-listp-thm
                             (cons len-thm (cons fix-thms 'nil))))))
             (cons true-listp-thm
                   (cons consp-thm 'nil))))))))
       (cons table-event 'nil))))))))