Events generated by definterface-encrypt-block.
(definterface-encrypt-block-fn name key-size block-size name-encrypt-bits name-decrypt-bits name-encrypt-bytes name-decrypt-bytes topic parents short long) → event?
Function:
(defun definterface-encrypt-block-fn (name key-size block-size name-encrypt-bits name-decrypt-bits name-encrypt-bytes name-decrypt-bytes topic parents short long) (declare (xargs :guard t)) (let ((__function__ 'definterface-encrypt-block-fn)) (declare (ignorable __function__)) (b* (((unless (symbolp name)) (raise "The NAME input must be a symbol, ~ but is it ~x0 instead." name)) ((unless (and (posp key-size) (integerp (/ key-size 8)))) (raise "The :KEY-SIZE input must be ~ a positive integer multiple of 8, ~ but it is ~x0 instead." key-size)) (key-size-/-8 (/ key-size 8)) ((unless (and (posp block-size) (integerp (/ block-size 8)))) (raise "The :BLOCK-SIZE input must be ~ a positive integer multiple of 8, ~ but it is ~x0 instead." block-size)) (block-size-/-8 (/ block-size 8)) ((unless (symbolp name-encrypt-bits)) (raise "The :NAME-ENCRYPT-BITS input must be a symbol, ~ but it is ~x0 instead." name-encrypt-bits)) ((unless (symbolp name-decrypt-bits)) (raise "The :NAME-DECRYPT-BITS input must be a symbol, ~ but it is ~x0 instead." name-decrypt-bits)) ((unless (symbolp name-encrypt-bytes)) (raise "The :NAME-ENCRYPT-BYTES input must be a symbol, ~ but it is ~x0 instead." name-encrypt-bytes)) ((unless (symbolp name-decrypt-bytes)) (raise "The :NAME-DECRYPT-BYTES input must be a symbol, ~ but it is ~x0 instead." name-decrypt-bytes)) ((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"))) (name-encrypt-bits (or name-encrypt-bits (add-suffix-to-fn name "-ENCRYPT-BITS"))) (name-decrypt-bits (or name-decrypt-bits (add-suffix-to-fn name "-DECRYPT-BITS"))) (name-encrypt-bytes (or name-encrypt-bytes (add-suffix-to-fn name "-ENCRYPT-BYTES"))) (name-decrypt-bytes (or name-decrypt-bytes (add-suffix-to-fn name "-DECRYPT-BYTES"))) (bit-listp-encrypt-bits (acl2::packn-pos (list 'bit-list-of- name-encrypt-bits) pkg-witness)) (bit-listp-decrypt-bits (acl2::packn-pos (list 'bit-list-of- name-decrypt-bits) pkg-witness)) (byte-listp-encrypt-bytes (acl2::packn-pos (list 'byte-list-of- name-encrypt-bytes) pkg-witness)) (byte-listp-decrypt-bytes (acl2::packn-pos (list 'byte-list-of- name-decrypt-bytes) pkg-witness)) (len-encrypt-bits (acl2::packn-pos (list 'len-of- name-encrypt-bits) pkg-witness)) (len-decrypt-bits (acl2::packn-pos (list 'len-of- name-decrypt-bits) pkg-witness)) (len-encrypt-bytes (acl2::packn-pos (list 'len-of- name-encrypt-bytes) pkg-witness)) (len-decrypt-bytes (acl2::packn-pos (list 'len-of- name-decrypt-bytes) pkg-witness)) (true-listp-encrypt-bits (acl2::packn-pos (list 'true-listp-of- name-encrypt-bits) pkg-witness)) (true-listp-decrypt-bits (acl2::packn-pos (list 'true-listp-of- name-decrypt-bits) pkg-witness)) (true-listp-encrypt-bytes (acl2::packn-pos (list 'true-listp-of- name-encrypt-bytes) pkg-witness)) (true-listp-decrypt-bytes (acl2::packn-pos (list 'true-listp-of- name-decrypt-bytes) pkg-witness)) (consp-encrypt-bits (acl2::packn-pos (list 'consp-of- name-encrypt-bits) pkg-witness)) (consp-decrypt-bits (acl2::packn-pos (list 'consp-of- name-decrypt-bits) pkg-witness)) (consp-encrypt-bytes (acl2::packn-pos (list 'consp-of- name-encrypt-bytes) pkg-witness)) (consp-decrypt-bytes (acl2::packn-pos (list 'consp-of- name-decrypt-bytes) pkg-witness)) (guard-bits (cons 'and (cons '(bit-listp key) (cons (cons 'equal (cons '(len key) (cons key-size 'nil))) (cons '(bit-listp block) (cons (cons 'equal (cons '(len block) (cons block-size 'nil))) 'nil)))))) (guard-bytes (cons 'and (cons '(byte-listp key) (cons (cons 'equal (cons '(len key) (cons key-size-/-8 'nil))) (cons '(byte-listp block) (cons (cons 'equal (cons '(len block) (cons block-size-/-8 'nil))) 'nil)))))) (sig-encrypt-bits (cons (cons name-encrypt-bits '(* *)) (cons '=> (cons '* (cons ':formals (cons '(key block) (cons ':guard (cons guard-bits 'nil)))))))) (sig-decrypt-bits (cons (cons name-decrypt-bits '(* *)) (cons '=> (cons '* (cons ':formals (cons '(key block) (cons ':guard (cons guard-bits 'nil)))))))) (sig-encrypt-bytes (cons (cons name-encrypt-bytes '(* *)) (cons '=> (cons '* (cons ':formals (cons '(key block) (cons ':guard (cons guard-bytes 'nil)))))))) (sig-decrypt-bytes (cons (cons name-decrypt-bytes '(* *)) (cons '=> (cons '* (cons ':formals (cons '(key block) (cons ':guard (cons guard-bytes 'nil)))))))) (wit-encrypt-bits (cons 'local (cons (cons 'defun (cons name-encrypt-bits (cons '(key block) (cons '(declare (ignore key block)) (cons (cons 'make-list (cons block-size '(:initial-element 0))) 'nil))))) 'nil))) (wit-decrypt-bits (cons 'local (cons (cons 'defun (cons name-decrypt-bits (cons '(key block) (cons '(declare (ignore key block)) (cons (cons 'make-list (cons block-size '(:initial-element 0))) 'nil))))) 'nil))) (wit-encrypt-bytes (cons 'local (cons (cons 'defun (cons name-encrypt-bytes (cons '(key block) (cons '(declare (ignore key block)) (cons (cons 'make-list (cons block-size-/-8 '(:initial-element 0))) 'nil))))) 'nil))) (wit-decrypt-bytes (cons 'local (cons (cons 'defun (cons name-decrypt-bytes (cons '(key block) (cons '(declare (ignore key block)) (cons (cons 'make-list (cons block-size-/-8 '(:initial-element 0))) 'nil))))) 'nil))) (bit-listp-encrypt-bits-thm (cons 'defrule (cons bit-listp-encrypt-bits (cons (cons 'bit-listp (cons (cons name-encrypt-bits '(key block)) 'nil)) 'nil)))) (bit-listp-decrypt-bits-thm (cons 'defrule (cons bit-listp-decrypt-bits (cons (cons 'bit-listp (cons (cons name-decrypt-bits '(key block)) 'nil)) 'nil)))) (byte-listp-encrypt-bytes-thm (cons 'defrule (cons byte-listp-encrypt-bytes (cons (cons 'byte-listp (cons (cons name-encrypt-bytes '(key block)) 'nil)) 'nil)))) (byte-listp-decrypt-bytes-thm (cons 'defrule (cons byte-listp-decrypt-bytes (cons (cons 'byte-listp (cons (cons name-decrypt-bytes '(key block)) 'nil)) 'nil)))) (len-encrypt-bits-thm (cons 'defrule (cons len-encrypt-bits (cons (cons 'equal (cons (cons 'len (cons (cons name-encrypt-bits '(key block)) 'nil)) (cons block-size 'nil))) 'nil)))) (len-decrypt-bits-thm (cons 'defrule (cons len-decrypt-bits (cons (cons 'equal (cons (cons 'len (cons (cons name-decrypt-bits '(key block)) 'nil)) (cons block-size 'nil))) 'nil)))) (len-encrypt-bytes-thm (cons 'defrule (cons len-encrypt-bytes (cons (cons 'equal (cons (cons 'len (cons (cons name-encrypt-bytes '(key block)) 'nil)) (cons block-size-/-8 'nil))) 'nil)))) (len-decrypt-bytes-thm (cons 'defrule (cons len-decrypt-bytes (cons (cons 'equal (cons (cons 'len (cons (cons name-decrypt-bytes '(key block)) 'nil)) (cons block-size-/-8 'nil))) 'nil)))) (fix-encrypt-bits-thms (cons 'fty::deffixequiv (cons name-encrypt-bits '(:args ((key bit-listp) (block bit-listp)))))) (fix-decrypt-bits-thms (cons 'fty::deffixequiv (cons name-decrypt-bits '(:args ((key bit-listp) (block bit-listp)))))) (fix-encrypt-bytes-thms (cons 'fty::deffixequiv (cons name-encrypt-bytes '(:args ((key byte-listp) (block byte-listp)))))) (fix-decrypt-bytes-thms (cons 'fty::deffixequiv (cons name-decrypt-bytes '(:args ((key byte-listp) (block byte-listp)))))) (true-listp-encrypt-bits-thm (cons 'defrule (cons true-listp-encrypt-bits (cons (cons 'true-listp (cons (cons name-encrypt-bits '(key block)) 'nil)) '(:rule-classes :type-prescription :enable acl2::true-listp-when-bit-listp-compound-recognizer))))) (true-listp-decrypt-bits-thm (cons 'defrule (cons true-listp-decrypt-bits (cons (cons 'true-listp (cons (cons name-decrypt-bits '(key block)) 'nil)) '(:rule-classes :type-prescription :enable acl2::true-listp-when-bit-listp-compound-recognizer))))) (true-listp-encrypt-bytes-thm (cons 'defrule (cons true-listp-encrypt-bytes (cons (cons 'true-listp (cons (cons name-encrypt-bytes '(key block)) 'nil)) '(:rule-classes :type-prescription :enable acl2::true-listp-when-byte-listp-compound-recognizer))))) (true-listp-decrypt-bytes-thm (cons 'defrule (cons true-listp-decrypt-bytes (cons (cons 'true-listp (cons (cons name-decrypt-bytes '(key block)) 'nil)) '(:rule-classes :type-prescription :enable acl2::true-listp-when-byte-listp-compound-recognizer))))) (consp-encrypt-bits-thm (cons 'defrule (cons consp-encrypt-bits (cons (cons 'consp (cons (cons name-encrypt-bits '(key block)) 'nil)) (cons ':rule-classes (cons ':type-prescription (cons ':use (cons len-encrypt-bits (cons ':disable (cons len-encrypt-bits 'nil)))))))))) (consp-decrypt-bits-thm (cons 'defrule (cons consp-decrypt-bits (cons (cons 'consp (cons (cons name-decrypt-bits '(key block)) 'nil)) (cons ':rule-classes (cons ':type-prescription (cons ':use (cons len-decrypt-bits (cons ':disable (cons len-decrypt-bits 'nil)))))))))) (consp-encrypt-bytes-thm (cons 'defrule (cons consp-encrypt-bytes (cons (cons 'consp (cons (cons name-encrypt-bytes '(key block)) 'nil)) (cons ':rule-classes (cons ':type-prescription (cons ':use (cons len-encrypt-bytes (cons ':disable (cons len-encrypt-bytes 'nil)))))))))) (consp-decrypt-bytes-thm (cons 'defrule (cons consp-decrypt-bytes (cons (cons 'consp (cons (cons name-decrypt-bytes '(key block)) 'nil)) (cons ':rule-classes (cons ':type-prescription (cons ':use (cons len-decrypt-bytes (cons ':disable (cons len-decrypt-bytes '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-encrypt-bits (cons sig-decrypt-bits (cons sig-encrypt-bytes (cons sig-decrypt-bytes 'nil)))) (cons wit-encrypt-bits (cons wit-decrypt-bits (cons wit-encrypt-bytes (cons wit-decrypt-bytes (cons bit-listp-encrypt-bits-thm (cons bit-listp-decrypt-bits-thm (cons byte-listp-encrypt-bytes-thm (cons byte-listp-decrypt-bytes-thm (cons len-encrypt-bits-thm (cons len-decrypt-bits-thm (cons len-encrypt-bytes-thm (cons len-decrypt-bytes-thm (cons fix-encrypt-bits-thms (cons fix-decrypt-bits-thms (cons fix-encrypt-bytes-thms (cons fix-decrypt-bytes-thms 'nil)))))))))))))))))) (cons true-listp-encrypt-bits-thm (cons true-listp-decrypt-bits-thm (cons true-listp-encrypt-bytes-thm (cons true-listp-decrypt-bytes-thm (cons consp-encrypt-bits-thm (cons consp-decrypt-bits-thm (cons consp-encrypt-bytes-thm (cons consp-decrypt-bytes-thm 'nil)))))))))))))) 'nil)))))))