		Search-engine friendly clone of the ACL2 documentation.

Encoding

Encoding-validp

Check if a 32-bit word is a valid instruction encoding.

This is the case when there exists an instruction, valid for the given features, whose encoding is enc. This is a declarative, non-executable definition.

The witness function decodes the valid encoding to the corresponding valid instruction. Encoding is left inverse of the witness function, over valid encodings.

Definitions and Theorems

Theorem: encoding-validp-suff

(defthm encoding-validp-suff
  (implies (and (instrp instr)
                (instr-validp instr feat)
                (equal (encode instr feat)
                       (ubyte32-fix enc)))
           (encoding-validp enc feat)))

Theorem: booleanp-of-encoding-validp

(defthm booleanp-of-encoding-validp
  (b* ((yes/no (encoding-validp enc feat)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: encoding-validp-of-ubyte32-fix-enc

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

Theorem: encoding-validp-ubyte32-equiv-congruence-on-enc

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

Theorem: encoding-validp-of-feat-fix-feat

(defthm encoding-validp-of-feat-fix-feat
  (equal (encoding-validp enc (feat-fix feat))
         (encoding-validp enc feat)))

Theorem: encoding-validp-feat-equiv-congruence-on-feat

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

Theorem: instrp-of-encoding-valid-witness

(defthm instrp-of-encoding-valid-witness
  (implies (encoding-validp enc feat)
           (instrp (encoding-valid-witness enc feat))))

Theorem: instr-validp-of-encoding-valid-witness

(defthm instr-validp-of-encoding-valid-witness
  (implies (encoding-validp enc feat)
           (instr-validp (encoding-valid-witness enc feat)
                         feat)))

Theorem: encode-of-encoding-valid-witness

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