Decoding of instructions.
Instructions are encoded as specified in [ISA] and [ISAP], and as formalized in encoding. We declaratively define a decoder as non-executable inverse of the encoder; see decoding-executable for an equivalent executable decoder.