Events generated by definterface-encrypt-init.
(definterface-encrypt-init-fn name key-size init-size name-encrypt-bits name-decrypt-bits name-encrypt-bytes name-decrypt-bytes topic parents short long) → event?
Function:
(defun definterface-encrypt-init-fn (name key-size init-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-init-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 init-size) (integerp (/ init-size 8)))) (raise "The :INIT-SIZE input must be ~ a positive integer multiple of 8, ~ but it is ~x0 instead." init-size)) (init-size-/-8 (/ init-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)) (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)) (guard-bits (cons 'and (cons '(bit-listp key) (cons (cons 'equal (cons '(len key) (cons key-size 'nil))) (cons '(bit-listp init) (cons (cons 'equal (cons '(len init) (cons init-size 'nil))) '((bit-listp data)))))))) (guard-bytes (cons 'and (cons '(byte-listp key) (cons (cons 'equal (cons '(len key) (cons key-size-/-8 'nil))) (cons '(byte-listp init) (cons (cons 'equal (cons '(len init) (cons init-size-/-8 'nil))) '((byte-listp data)))))))) (sig-encrypt-bits (cons (cons name-encrypt-bits '(* * *)) (cons '=> (cons '* (cons ':formals (cons '(key init data) (cons ':guard (cons guard-bits 'nil)))))))) (sig-decrypt-bits (cons (cons name-decrypt-bits '(* * *)) (cons '=> (cons '* (cons ':formals (cons '(key init data) (cons ':guard (cons guard-bits 'nil)))))))) (sig-encrypt-bytes (cons (cons name-encrypt-bytes '(* * *)) (cons '=> (cons '* (cons ':formals (cons '(key init data) (cons ':guard (cons guard-bytes 'nil)))))))) (sig-decrypt-bytes (cons (cons name-decrypt-bytes '(* * *)) (cons '=> (cons '* (cons ':formals (cons '(key init data) (cons ':guard (cons guard-bytes 'nil)))))))) (wit-encrypt-bits (cons 'local (cons (cons 'defun (cons name-encrypt-bits (cons '(key init data) (cons '(declare (ignore key init data)) (cons (cons 'make-list (cons init-size '(:initial-element 0))) 'nil))))) 'nil))) (wit-decrypt-bits (cons 'local (cons (cons 'defun (cons name-decrypt-bits (cons '(key init data) (cons '(declare (ignore key init data)) (cons (cons 'make-list (cons init-size '(:initial-element 0))) 'nil))))) 'nil))) (wit-encrypt-bytes (cons 'local (cons (cons 'defun (cons name-encrypt-bytes (cons '(key init data) (cons '(declare (ignore key init data)) (cons (cons 'make-list (cons init-size-/-8 '(:initial-element 0))) 'nil))))) 'nil))) (wit-decrypt-bytes (cons 'local (cons (cons 'defun (cons name-decrypt-bytes (cons '(key init data) (cons '(declare (ignore key init data)) (cons (cons 'make-list (cons init-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 init data)) 'nil)) 'nil)))) (bit-listp-decrypt-bits-thm (cons 'defrule (cons bit-listp-decrypt-bits (cons (cons 'bit-listp (cons (cons name-decrypt-bits '(key init data)) 'nil)) 'nil)))) (byte-listp-encrypt-bytes-thm (cons 'defrule (cons byte-listp-encrypt-bytes (cons (cons 'byte-listp (cons (cons name-encrypt-bytes '(key init data)) 'nil)) 'nil)))) (byte-listp-decrypt-bytes-thm (cons 'defrule (cons byte-listp-decrypt-bytes (cons (cons 'byte-listp (cons (cons name-decrypt-bytes '(key init data)) 'nil)) 'nil)))) (fix-encrypt-bits-thms (cons 'fty::deffixequiv (cons name-encrypt-bits '(:args ((key bit-listp) (init bit-listp) (data bit-listp)))))) (fix-decrypt-bits-thms (cons 'fty::deffixequiv (cons name-decrypt-bits '(:args ((key bit-listp) (init bit-listp) (data bit-listp)))))) (fix-encrypt-bytes-thms (cons 'fty::deffixequiv (cons name-encrypt-bytes '(:args ((key byte-listp) (init byte-listp) (data byte-listp)))))) (fix-decrypt-bytes-thms (cons 'fty::deffixequiv (cons name-decrypt-bytes '(:args ((key byte-listp) (init byte-listp) (data byte-listp)))))) (true-listp-encrypt-bits-thm (cons 'defrule (cons true-listp-encrypt-bits (cons (cons 'true-listp (cons (cons name-encrypt-bits '(key init data)) '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 init data)) '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 init data)) '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 init data)) 'nil)) '(:rule-classes :type-prescription :enable acl2::true-listp-when-byte-listp-compound-recognizer)))))) (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 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 'nil)))))))))) 'nil)))))))