(select-opcode-map map-key) → inst-lst
Function:
(defun select-opcode-map (map-key) (declare (xargs :guard (keywordp map-key))) (declare (xargs :guard (member-equal map-key '(:one-byte :two-byte :0f-38-three-byte :0f-3a-three-byte :vex-0f :vex-0f-38 :vex-0f-3a :evex-0f :evex-0f-38 :evex-0f-3a)))) (let ((__function__ 'select-opcode-map)) (declare (ignorable __function__)) (case map-key (:one-byte *one-byte-opcode-map*) ((:two-byte :vex-0f :evex-0f) *two-byte-opcode-map*) ((:0f-38-three-byte :vex-0f-38 :evex-0f-38) *0f-38-three-byte-opcode-map*) ((:0f-3a-three-byte :vex-0f-3a :evex-0f-3a) *0f-3a-three-byte-opcode-map*))))
Theorem:
(defthm inst-list-p-of-select-opcode-map (implies (and (keywordp map-key) (member-equal map-key '(:one-byte :two-byte :0f-38-three-byte :0f-3a-three-byte :vex-0f :vex-0f-38 :vex-0f-3a :evex-0f :evex-0f-38 :evex-0f-3a))) (b* ((inst-lst (select-opcode-map map-key))) (inst-list-p inst-lst))) :rule-classes :rewrite)