|
|
|---|
|
|
|
|---|
Injectivity of decoding.
Different valid encodings are decoded differently. This is a direct consequence of encode-of-decodex: if two different instructions were decoded in the same way, the encoder would be unable to restore both at the same time.
Theorem:
(defthm decodex-injective (b* ((instr1? (decodex enc1 feat)) (instr2? (decodex enc2 feat))) (implies (and instr1? instr2?) (equal (equal instr1? instr2?) (equal (ubyte32-fix enc1) (ubyte32-fix enc2))))))