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
The witness function decodes the valid encoding to the corresponding valid instruction. Encoding if left inverse of the witness function, over valid encodings.
Theorem:
(defthm encoding-validp-suff (implies (and (instrp instr) (instr-validp instr feat) (equal (encode instr feat) (ubyte32-fix enc))) (encoding-validp enc feat)))
Theorem:
(defthm booleanp-of-encoding-validp (b* ((yes/no (encoding-validp enc feat))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm encoding-validp-of-ubyte32-fix-enc (equal (encoding-validp (ubyte32-fix enc) feat) (encoding-validp enc feat)))
Theorem:
(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:
(defthm encoding-validp-of-feat-fix-feat (equal (encoding-validp enc (feat-fix feat)) (encoding-validp enc feat)))
Theorem:
(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:
(defthm instrp-of-encoding-valid-witness (implies (encoding-validp enc feat) (instrp (encoding-valid-witness enc feat))))
Theorem:
(defthm instr-validp-of-encoding-valid-witness (implies (encoding-validp enc feat) (instr-validp (encoding-valid-witness enc feat) feat)))
Theorem:
(defthm encode-of-encoding-valid-witness (implies (encoding-validp enc feat) (equal (encode (encoding-valid-witness enc feat) feat) (ubyte32-fix enc))))