8.4. Encoding Verification with rfl
A key advantage of this implementation is that encodings can be proved correct at compile time using definitional equality:
theorem nop_is_0x90 : encode 0 Instr.NOP = [0x90] := rfl
theorem ret_is_0xC3 : encode 0 (Instr.RETOP 0) = [0xC3] := rfl
theorem hlt_is_0xF4 : encode 0 Instr.HLT = [0xF4] := rfl
This means the type checker itself verifies that our encoding matches the expected bytes.