4. RTL as a Lean DSL🔗

The generated Janus cell is not a raw SystemVerilog string. It is a Lean value in a small RTL DSL. The emitter renders that value, and CI checks that the checked-in rtl/janus_cell.sv is exactly the renderer output.

The proof boundary is the DSL value. The trusted text renderer is intentionally small; if Janus later needs a parser-level guarantee about external SystemVerilog tooling, that can be added without changing the processor contract.

namespace Janus

Janus.janusCellDesign_refines_isa (c : CellState) (hbusy : c.busy = true) (hhalt : c.arch.halted = false) :
  step defaultConfig (programOf c.imem) c.arch = some (cellExecCycle c).arch#check janusCellDesign_refines_isa

end Janus

The current refinement theorem covers the execute path: when the cell is busy and not halted, one DSL cycle advances the architectural state exactly as the ISA step function does for the decoded instruction at pc.