Janus

7. Cell Lifecycle🔗

The execute and fetch proofs cover the running cell. The top-level cell also has a lifecycle protocol: reset, host memory writes, start, gated execution, and debug observation. This chapter gives that protocol an executable Lean model with port-shaped inputs.

namespace Janus Janus.CellInputs : Type#check CellInputs Janus.CellOutputs : Type#check CellOutputs Janus.cellOutputs (i : CellInputs) (c : WordCellState) : CellOutputs#check cellOutputs end Janus

Reset and start are explicit state transformers. Both preserve the loaded memories. Reset leaves the cell halted and not busy; start clears architectural counters, registers, pointers, accumulator, and program counter before making the cell runnable.

namespace Janus Janus.resetArch (s : State defaultConfig) : State defaultConfig#check resetArch Janus.startArch (s : State defaultConfig) : State defaultConfig#check startArch Janus.resetCell (c : WordCellState) : WordCellState#check resetCell Janus.startCell (c : WordCellState) : WordCellState#check startCell Janus.cellClock_reset (i : CellInputs) (c : WordCellState) (hrst : i.rst_n = false) : cellClock i c = resetCell c#check cellClock_reset Janus.cellClock_start (i : CellInputs) (c : WordCellState) (hrst : i.rst_n = true) (hstart : i.start = true) : cellClock i c = startCell (applyHostWrites i c)#check cellClock_start end Janus

Host writes update the physical slots selected by the low memory-index bits of the word instruction memory and the architectural data, resident-weight, and stream memories. With reset inactive and start low, the clock either idles or delegates to the word-backed execute cycle. When the cell is busy and not halted, that lifecycle transition refines the ISA step for the post-load state.

namespace Janus Janus.applyHostWrites (i : CellInputs) (c : WordCellState) : WordCellState#check applyHostWrites Janus.hostWritesIdle (i : CellInputs) : Prop#check hostWritesIdle Janus.applyHostWrites_idle (i : CellInputs) (c : WordCellState) (hidle : hostWritesIdle i) : applyHostWrites i c = c#check applyHostWrites_idle Janus.cellClock_no_start (i : CellInputs) (c : WordCellState) (hrst : i.rst_n = true) (hstart : i.start = false) : cellClock i c = wordCellExecCycle (applyHostWrites i c)#check cellClock_no_start Janus.cellClock_execute_refines_step (i : CellInputs) (c : WordCellState) (hrst : i.rst_n = true) (hstart : i.start = false) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) : step defaultConfig (programOfWords (applyHostWrites i c).imem (applyHostWrites i c).fallback) (applyHostWrites i c).arch = some (cellClock i c).arch#check cellClock_execute_refines_step end Janus

For the ordinary run protocol, host writes are idle during execution. Under that condition, a generated encoded program has the same one-cycle architectural effect as executing the decoded instruction selected by the encoder at pc.

namespace Janus Janus.generatedCellClock_execute_refines_step (i : CellInputs) (p : Nat → EncodedInstr) (fallback : DecodedInstr) (arch : State defaultConfig) (hrst : i.rst_n = true) (hstart : i.start = false) (hidle : hostWritesIdle i) (hhalt : arch.halted = false) : step defaultConfig (programOfWords (encodedWordMem p) fallback) arch = some (cellClock i (generatedWordCell p fallback arch true)).arch#check generatedCellClock_execute_refines_step Janus.generatedCellClock_arch_eq_execDecoded (i : CellInputs) (p : Nat → EncodedInstr) (fallback : DecodedInstr) (arch : State defaultConfig) (hrst : i.rst_n = true) (hstart : i.start = false) (hidle : hostWritesIdle i) (hhalt : arch.halted = false) : (cellClock i (generatedWordCell p fallback arch true)).arch = execDecoded (p (memIndexOfNat defaultConfig (BitVec.toNat arch.pc))).toDecoded arch#check generatedCellClock_arch_eq_execDecoded end Janus