6. Fetch Refinement🔗

The execute-path theorem starts from a decoded instruction. The generated program artifacts are encoded thirty-two-bit instruction words. This chapter connects those layers without making a global function-equality proof do more work than necessary: the bridge is pointwise at the physical instruction slot selected by the current program counter.

namespace Honeycomb

Honeycomb.decodedProgramFrom_encodedWordMem (p : Nat → EncodedInstr) (fallback : DecodedInstr) (pc : Nat) :
  decodedProgramFromWords (encodedWordMem p) fallback pc = (p pc).toDecoded#check decodedProgramFrom_encodedWordMem
Honeycomb.fetchDecoded_encodedWordMem (p : Nat → EncodedInstr) (fallback : DecodedInstr) (pc : Nat) :
  fetchDecoded (encodedWordMem p) fallback pc = (p pc).toDecoded#check fetchDecoded_encodedWordMem
Honeycomb.programOfWords_encodedWordMem (p : Nat → EncodedInstr) (fallback : DecodedInstr) (pc : Nat) :
  programOfWords (encodedWordMem p) fallback pc = (p (memIndexOfNat defaultConfig pc)).toInstr#check programOfWords_encodedWordMem

end Honeycomb

The word-backed cell state keeps instruction memory as BitVec 32 words and decodes the word at pc before calling the same execute function used by the RTL DSL proof. Invalid opcodes are modeled by an explicit fallback decoded instruction; haltDecodedInstr matches the current generated cell's default case.

namespace Honeycomb

Honeycomb.haltDecodedInstr : DecodedInstr#check haltDecodedInstr
Honeycomb.WordCellState : Type#check WordCellState
Honeycomb.wordCellExecCycle (c : WordCellState) : WordCellState#check wordCellExecCycle
Honeycomb.wordCellExecCycle_refines_step (c : WordCellState) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) :
  step defaultConfig (programOfWords c.imem c.fallback) c.arch = some (wordCellExecCycle c).arch#check wordCellExecCycle_refines_step

end Honeycomb

For memories produced by the Lean encoder, the fallback is unreachable at the fetched address. One word-backed cell cycle therefore refines the ISA step for the decoded instruction that the encoder intended.

namespace Honeycomb

Honeycomb.generatedWordCell_fetch (p : Nat → EncodedInstr) (fallback : DecodedInstr) (arch : State defaultConfig)
  (busy : Bool) :
  fetchDecoded (generatedWordCell p fallback arch busy).imem (generatedWordCell p fallback arch busy).fallback
      (memIndexOfNat defaultConfig (BitVec.toNat arch.pc)) =
    (p (memIndexOfNat defaultConfig (BitVec.toNat arch.pc))).toDecoded#check generatedWordCell_fetch
Honeycomb.generatedWordCellExecCycle_refines_step (p : Nat → EncodedInstr) (fallback : DecodedInstr)
  (arch : State defaultConfig) (hhalt : arch.halted = false) :
  step defaultConfig (programOfWords (encodedWordMem p) fallback) arch =
    some (wordCellExecCycle (generatedWordCell p fallback arch true)).arch#check generatedWordCellExecCycle_refines_step
Honeycomb.generatedWordCellExecCycle_uses_encoded_decode (p : Nat → EncodedInstr) (fallback : DecodedInstr)
  (arch : State defaultConfig) (hhalt : arch.halted = false) :
  step defaultConfig (programOfWords (encodedWordMem p) fallback) arch =
    some (execDecoded (p (memIndexOfNat defaultConfig (BitVec.toNat arch.pc))).toDecoded arch)#check generatedWordCellExecCycle_uses_encoded_decode

end Honeycomb