5. Instruction Encoding🔗

The RTL consumes 32-bit instruction words. The ISA proof layer consumes decoded instructions. This chapter starts the bridge by defining the encoded instruction object, the bit layout, the decoder, and the field-roundtrip theorem that says every encoded field is recovered exactly.

The low sixteen bits are deliberately raw bits. li and blz interpret them as signed two's-complement immediates; local pointer instructions interpret the same bits as an unsigned local address.

namespace Janus

Janus.EncodedInstr : Type#check EncodedInstr
Janus.EncodedInstr.encode (e : EncodedInstr) : BitVec 32#check EncodedInstr.encode
Janus.decodeInstrWord (w : BitVec 32) : Option EncodedInstr#check decodeInstrWord
Janus.EncodedInstr.toDecoded (e : EncodedInstr) : DecodedInstr#check EncodedInstr.toDecoded

end Janus

The encoder is ordinary arithmetic over a natural number before the final 32-bit wrap. The next theorem is the guard: all encoded Janus instruction words fit in 32 bits, so the final BitVec.ofNat does not lose information.

namespace Janus

Janus.codeNat_lt (op rd ra rb imm : Nat) (hop : op < 16) (hrd : rd < 16) (hra : ra < 16) (hrb : rb < 16)
  (himm : imm < 65536) : codeNat op rd ra rb imm < 2 ^ 32#check codeNat_lt
Janus.encode_toNat (e : EncodedInstr) : e.encode.toNat = e.encodeNat#check encode_toNat

end Janus

Field extraction is then a checked arithmetic theorem. This is the base lemma for the next refinement step, where the decoded instruction at the RTL pc will be connected to the ISA-level DecodedInstr.toInstr.

namespace Janus

Janus.field_round_nat (op rd ra rb imm : Nat) (hop : op < 16) (hrd : rd < 16) (hra : ra < 16) (hrb : rb < 16)
  (himm : imm < 65536) :
  opcodeFieldNat (codeNat op rd ra rb imm) = op ∧
    rdFieldNat (codeNat op rd ra rb imm) = rd ∧
      raFieldNat (codeNat op rd ra rb imm) = ra ∧
        rbFieldNat (codeNat op rd ra rb imm) = rb ∧ immFieldNat (codeNat op rd ra rb imm) = imm#check field_round_nat
Janus.encode_fields_correct (e : EncodedInstr) :
  opcodeField e.encode = e.op.opcode ∧
    rdField e.encode = ↑e.rd ∧ raField e.encode = ↑e.ra ∧ rbField e.encode = ↑e.rb ∧ immField e.encode = e.imm16.toNat#check encode_fields_correct
Janus.op_ofOpcode_opcode (op : CellOp) : CellOp.ofOpcode op.opcode = some op#check op_ofOpcode_opcode
Janus.regOfNat_val_eq (r : Reg defaultConfig) : regOfNat ↑r = r#check regOfNat_val_eq
Janus.imm16_of_toNat (x : BitVec 16) : BitVec.ofNat 16 x.toNat = x#check imm16_of_toNat

end Janus

The final roundtrip theorem composes those field facts with the decoder: encoding and then decoding an instruction word returns the same encoded instruction object, and therefore the same decoded ISA instruction.

namespace Janus

Janus.decodeInstrWord_of_fields (w : BitVec 32) (op : CellOp) (rd ra rb : Reg defaultConfig) (imm16 : BitVec 16)
  (hop : opcodeField w = op.opcode) (hrd : rdField w = ↑rd) (hra : raField w = ↑ra) (hrb : rbField w = ↑rb)
  (himm : immField w = imm16.toNat) :
  decodeInstrWord w = some { op := op, rd := rd, ra := ra, rb := rb, imm16 := imm16 }#check decodeInstrWord_of_fields
Janus.decode_encode (e : EncodedInstr) : decodeInstrWord e.encode = some e#check decode_encode
Janus.decode_encode_toDecoded (e : EncodedInstr) :
  Option.map EncodedInstr.toDecoded (decodeInstrWord e.encode) = some e.toDecoded#check decode_encode_toDecoded
Janus.decode_encode_toInstr (e : EncodedInstr) :
  Option.map EncodedInstr.toInstr (decodeInstrWord e.encode) = some e.toInstr#check decode_encode_toInstr

end Janus

The word-memory bridge then lifts the single-word theorem to program memory: if the program memory is generated by the Lean encoder, fetching and decoding the word at pc produces exactly the DecodedInstr consumed by the execute refinement theorem.

namespace Janus

Janus.decodeWordToDecoded (w : BitVec 32) : Option DecodedInstr#check decodeWordToDecoded
Janus.decodeWordOrElse (w : BitVec 32) (fallback : DecodedInstr) : DecodedInstr#check decodeWordOrElse
Janus.decodeWordOrElse_of_some {w : BitVec 32} {fallback d : DecodedInstr} (h : decodeWordToDecoded w = some d) :
  decodeWordOrElse w fallback = d#check decodeWordOrElse_of_some
Janus.decodeWordOrElse_of_none {w : BitVec 32} {fallback : DecodedInstr} (h : decodeWordToDecoded w = none) :
  decodeWordOrElse w fallback = fallback#check decodeWordOrElse_of_none
Janus.encodedWordMem (p : Nat → EncodedInstr) : Nat → BitVec 32#check encodedWordMem
Janus.decodedProgramFromWords (imem : Nat → BitVec 32) (fallback : DecodedInstr) : Nat → DecodedInstr#check decodedProgramFromWords
Janus.programOfWords (imem : Nat → BitVec 32) (fallback : DecodedInstr) : Program defaultConfig#check programOfWords
Janus.decode_encodedWordMem (p : Nat → EncodedInstr) (pc : Nat) :
  decodeWordToDecoded (encodedWordMem p pc) = some (p pc).toDecoded#check decode_encodedWordMem

end Janus