		Search-engine friendly clone of the ACL2 documentation.

Decoding

Decode

Declarative definition of instruction decoding.

Signature
(decode enc feat) → instr?
Arguments: enc — Guard (ubyte32p enc).; feat — Guard (featp feat).
Returns: instr? — Type (instr-optionp instr?).

If there is some valid instruction whose encoding is enc, we return one such instruction. We use the witness function of encoding-validp for that.

Since encode is injective (as proved elsewhere), there is in fact at most one such instruction. However, this uniqueness is unnecessary for defining the decoder here.

The encoder is left inverse of the decoder over valid encodings. This follows from the same property of the witness function of encoding-validp, which is proved there.

Definitions and Theorems

Function: decode

(defun decode (enc feat)
  (declare (xargs :guard (and (ubyte32p enc) (featp feat))))
  (let ((__function__ 'decode))
    (declare (ignorable __function__))
    (if (encoding-validp enc feat)
        (encoding-valid-witness (ubyte32-fix enc)
                                (feat-fix feat))
      nil)))

Theorem: instr-optionp-of-decode

(defthm instr-optionp-of-decode
  (b* ((instr? (decode enc feat)))
    (instr-optionp instr?))
  :rule-classes :rewrite)

Theorem: decode-of-ubyte32-fix-enc

(defthm decode-of-ubyte32-fix-enc
  (equal (decode (ubyte32-fix enc) feat)
         (decode enc feat)))

Theorem: decode-ubyte32-equiv-congruence-on-enc

(defthm decode-ubyte32-equiv-congruence-on-enc
  (implies (acl2::ubyte32-equiv enc enc-equiv)
           (equal (decode enc feat)
                  (decode enc-equiv feat)))
  :rule-classes :congruence)

Theorem: decode-of-feat-fix-feat

(defthm decode-of-feat-fix-feat
  (equal (decode enc (feat-fix feat))
         (decode enc feat)))

Theorem: decode-feat-equiv-congruence-on-feat

(defthm decode-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (decode enc feat)
                  (decode enc feat-equiv)))
  :rule-classes :congruence)

Theorem: instrp-of-decode

(defthm instrp-of-decode
  (implies (encoding-validp enc feat)
           (b* ((?instr? (decode enc feat)))
             (instrp instr?))))

Theorem: instr-validp-of-decode

(defthm instr-validp-of-decode
  (implies (encoding-validp enc feat)
           (b* ((?instr? (decode enc feat)))
             (instr-validp instr? feat))))

Theorem: encode-of-decode

(defthm encode-of-decode
  (implies (encoding-validp enc feat)
           (equal (encode (decode enc feat) feat)
                  (ubyte32-fix enc))))

Theorem: decode-iff-encoding-validp

(defthm decode-iff-encoding-validp
  (iff (decode enc feat)
       (encoding-validp enc feat)))