		Search-engine friendly clone of the ACL2 documentation.

Encoding

Encode-store-funct

Encode the name of an instruction with the STORE opcode into the funct3 field [ISA:2.6] [ISA:4.3] [ISA:35].

Signature
(encode-store-funct funct feat) → funct3
Arguments: funct — Guard (store-funct-p funct).; feat — Guard (featp feat).
Returns: funct3 — Type (ubyte3p funct3).

Definitions and Theorems

Function: encode-store-funct

(defun encode-store-funct (funct feat)
  (declare (xargs :guard (and (store-funct-p funct)
                              (featp feat))))
  (declare (xargs :guard (implies (store-funct-case funct :sd)
                                  (feat-64p feat))))
  (let ((__function__ 'encode-store-funct))
    (declare (ignorable __function__))
    (store-funct-case funct
                      :sb 0
                      :sh 1
                      :sw 2
                      :sd (assert$ (feat-64p feat) 3))))

Theorem: ubyte3p-of-encode-store-funct

(defthm ubyte3p-of-encode-store-funct
  (b* ((funct3 (encode-store-funct funct feat)))
    (ubyte3p funct3))
  :rule-classes :rewrite)

Theorem: encode-store-funct-of-store-funct-fix-funct

(defthm encode-store-funct-of-store-funct-fix-funct
  (equal (encode-store-funct (store-funct-fix funct)
                             feat)
         (encode-store-funct funct feat)))

Theorem: encode-store-funct-store-funct-equiv-congruence-on-funct

(defthm encode-store-funct-store-funct-equiv-congruence-on-funct
  (implies (store-funct-equiv funct funct-equiv)
           (equal (encode-store-funct funct feat)
                  (encode-store-funct funct-equiv feat)))
  :rule-classes :congruence)

Theorem: encode-store-funct-of-feat-fix-feat

(defthm encode-store-funct-of-feat-fix-feat
  (equal (encode-store-funct funct (feat-fix feat))
         (encode-store-funct funct feat)))

Theorem: encode-store-funct-feat-equiv-congruence-on-feat

(defthm encode-store-funct-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (encode-store-funct funct feat)
                  (encode-store-funct funct feat-equiv)))
  :rule-classes :congruence)