Encode-of-decode
Encoding the decoding of a valid encoding
yields the original encoding.
Definitions and Theorems
Theorem: encode-of-decode
(defthm encode-of-decode
(b* ((instr? (decode enc feat)))
(implies instr?
(equal (encode instr? feat)
(ubyte32-fix enc)))))
