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

Events generated by definterface-hmac.
Signature
(definterface-pbkdf2-fn name hmac 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-pbkdf2-fn
(defun definterface-pbkdf2-fn
       (name hmac topic parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'definterface-pbkdf2-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but is it ~x0 instead."
      name))
    ((unless (symbolp hmac))
     (raise
      "The :HMAC input must be a symbol, ~
                but it is ~x0 instead."
      hmac))
    (table (table-alist *definterface-hmac-table-name* wrld)
)
    (pair (assoc-eq hmac table))
    ((unless pair)
     (raise
      "The :HMAC input ~x0 must name ~
                an existing HMAC function interface ~
                introduced via DEFINTERFACE-HMAC, ~
                but this is not the case."
      hmac))
    (info (cdr pair))
    (key-size-limit (definterface-hmac-info->key-size-limit info))
    (block-size (definterface-hmac-info->block-size info))
    (output-size (definterface-hmac-info->output-size info))
    ((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 key-size-limit
      (cons
       'and
       (cons
        '(byte-listp password)
        (cons
         (cons '<
               (cons '(len password)
                     (cons key-size-limit 'nil)))
         (cons
          '(byte-listp salt)
          (cons
           (cons
            '<
            (cons
             '(len salt)
             (cons
              (cons
               '-
               (cons
                 (cons '-
                       (cons key-size-limit (cons block-size 'nil)))
                 '(4)))
              'nil)))
           (cons
            '(posp iterations)
            (cons
             '(posp length)
             (cons
              (cons
                   '<=
                   (cons 'length
                         (cons (cons '*
                                     (cons '(1- (expt 2 32))
                                           (cons output-size 'nil)))
                               'nil)))
              'nil))))))))
      (cons
       'and
       (cons
        '(byte-listp password)
        (cons
         '(byte-listp salt)
         (cons
          '(posp iterations)
          (cons
           '(posp length)
           (cons
             (cons '<=
                   (cons 'length
                         (cons (cons '*
                                     (cons '(1- (expt 2 32))
                                           (cons output-size 'nil)))
                               'nil)))
             'nil))))))))
    (sig
     (cons
      (cons name '(* * * *))
      (cons '=>
            (cons '*
                  (cons ':formals
                        (cons '(password salt iterations length)
                              (cons ':guard (cons guard 'nil))))))))
    (wit
     (cons
      'local
      (cons
           (cons 'defun
                 (cons name
                       '((password salt iterations length)
                         (declare (ignore password salt iterations))
                         (make-list (pos-fix length)
                                    :initial-element 0))))
           'nil)))
    (byte-listp-thm
     (cons
      'defrule
      (cons
       byte-listp-thm-name
       (cons
          (cons 'byte-listp
                (cons (cons name '(password salt iterations length))
                      'nil))
          'nil))))
    (len-thm
     (cons
      'defrule
      (cons
       len-thm-name
       (cons
        (cons
         'equal
         (cons
          (cons 'len
                (cons (cons name '(password salt iterations length))
                      'nil))
          '((pos-fix length))))
        'nil))))
    (fix-thms (cons 'fty::deffixequiv
                    (cons name
                          '(:args ((password byte-listp)
                                   (salt byte-listp)
                                   (iterations posp)
                                   (length posp))))))
    (true-listp-thm
     (cons
      'defrule
      (cons
       true-listp-thm-name
       (cons
        (cons 'true-listp
              (cons (cons name '(password salt iterations length))
                    '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 '(password salt iterations length))
                    'nil))
        (cons
          ':rule-classes
          (cons ':type-prescription
                (cons ':use
                      (cons len-thm-name
                            (cons ':disable
                                  (cons len-thm-name '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))))))))
       'nil)))))))