		Search-engine friendly clone of the ACL2 documentation.

Decoding-as-inverse

Decodei

Declarative definition of instruction decoding.

Signature
(decodei 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, there is in fact at most one such instruction.

Definitions and Theorems

Function: decodei

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

Theorem: instr-optionp-of-decodei

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

Theorem: encode-of-decodei

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

Theorem: decodei-of-ubyte32-fix-enc

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

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

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

Theorem: decodei-of-feat-fix-feat

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

Theorem: decodei-feat-equiv-congruence-on-feat

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