		Search-engine friendly clone of the ACL2 documentation.

Encoding-decoding-illustration

Illustration of instruction encoding and decoding.

The lighter blue oval consists of all instructions, i.e. all values of type instr.

The lighter green oval consists of all 32-bit words, i.e. all values of type ubyte32.

Given specific features feat, the darker blue oval consists of all valid instructions, i.e. all values of type instr that additionally satisfy instr-validp; this predicate depends on feat.

Given specific features feat, the darker green oval consists of all valid instruction encodings, i.e. all values of type ubyte32 that additionally satisfy encoding-validp; this predicate depends on feat.

The `encode' arrow represents the function encode, which maps each valid instruction to a valid encoding. The validity of the instruction is in the guard of encode. The valid encodings are defined, via encoding-validp, as the image of encode over the valid instructions: thus, the darker green oval is the image of the darker blue oval under encode.

The upper `decode' arrow represents the witness function encoding-valid-witness that accompanies encoding-validp. Given a valid instruction encoding in the darker green oval, indicated by the dot in that oval, encoding-valid-witness maps it back to a valid instruction in the darker blue oval, indicated by the dot in that oval, whose encoding is the one in the green oval. Based solely on the definition of encoding-validp, there is no guarantee that the valid instruction is unique (this is proved elsewhere, as explained shortly), but we know that encode takes us back to the initial encoding in the green oval.

The upper and lower `decode' arrows represent the function decode, which is defined as the inverse of encode. When applied to valid encodings in the darker green oval, decode coincides with encoding-valid-witness; when applied to invalid encodings in the lighter green oval that are not also in the darker green oval, decode) returns nil, i.e. no instruction.

The upper and lower `decode' arrows also represent the executable decoding function decodex, which is proved in decode-is-decodex to be equal to decode.

From decodex-of-encode we also know that if we start with a valid instruction in the darker blue oval, and we encode obtaining a valid encoding in the darker gree oval, then if we apply decode or decodex (they are equal) we go back to the initial valid instruction. So encode is in fact injective, as explicated in encode-injective, and the darker blue and darker green ovals are in bijective correspondence, with encode and decode (or decodex) as the bijections between them.