1. Status and Evidence🔗

Janus now has a first generated RTL cell tied to the book's documented boundary. The book proves the executable semantics, kernel arithmetic, block-float identity, small analytical design rules, the RTL DSL execute path against step, the encoded-word fetch bridge feeding that execute path, and the abstract lifecycle protocol around reset, host writes, start, and execute gating. The first-cell 256-entry physical memory index is explicit in those contracts. A first sky130/OpenLane run was recorded for the earlier inferred-memory cell; that run exposed the expected standard-cell memory expansion and did not reach pre-PNR timing. The hot memories now sit behind janus_sram macro-adapter submodules, and a second sky130 synthesis run is recorded against that boundary: the memories bind as SRAM macros and the mapped flip-flop count collapses by roughly fifty times. The book does not yet prove parser-level SystemVerilog refinement, does not yet close macro-backed timing, and does not claim fabricated silicon or measured Janus hardware.

namespace Janus

inductive Evidence where
  | proved
  | modeled
  | recorded
  | target
deriving Repr, DecidableEq

structure StatusClaim where
  name : String
  evidence : Evidence
  closed : Bool
deriving Repr

structure SynthesisAttempt where
  runDate : String
  tool : String
  pdk : String
  flow : String
  runTag : String
  boundedMinutes : Nat
  reachedPrePnrSta : Bool
  yosysCheckProblems : Nat
  memoriesRemaining : Nat
  postDffCells : Nat
  mappedSky130Flops : Nat
  postDffSequentialAreaUm2 : String
  finalAbcCompleted : Bool
deriving Repr

structure MacroSynthesisResult where
  runDate : String
  tool : String
  pdk : String
  flow : String
  runTag : String
  reachedPrePnrSta : Bool
  checkProblems : Nat
  inferredMemoriesRemaining : Nat
  sramMacroInstances : Nat
  physicalSramMacros : Nat
  mappedCells : Nat
  mappedSky130Flops : Nat
  stdCellLogicAreaUm2 : String
  oneSramMacroAreaUm2 : String
  finalMapCompleted : Bool
  cycleFaithful : Bool
deriving Repr

def janusStatus : List StatusClaim :=
  [ { name := "fixed-width processor semantics", evidence := .proved,
      closed := true },
    { name := "branch-free kernel dot correctness", evidence := .proved,
      closed := true },
    { name := "cycle-level kernel scheduler refinement", evidence := .proved,
      closed := true },
    { name := "block-float integer MAC identity", evidence := .proved,
      closed := true },
    { name := "load lattice and utilization design rules", evidence := .modeled,
      closed := true },
    { name := "GPU comparison constants", evidence := .recorded,
      closed := true },
    { name := "generated single-cell RTL from Lean DSL", evidence := .recorded,
      closed := true },
    { name := "single-cycle execute-path RTL DSL refinement", evidence := .proved,
      closed := true },
    { name := "encoded instruction fetch to execute-path refinement",
      evidence := .proved, closed := true },
    { name := "abstract cell lifecycle refinement", evidence := .proved,
      closed := true },
    { name := "first-cell physical memory index contract", evidence := .proved,
      closed := true },
    { name := "sky130/OpenLane inferred-memory synthesis attempt",
      evidence := .recorded, closed := true },
    { name := "janus_sram macro-adapter RTL boundary", evidence := .recorded,
      closed := true },
    { name := "sky130 macro-adapter synthesis area", evidence := .recorded,
      closed := true },
    { name := "macro-backed cell timing closure", evidence := .target,
      closed := false },
    { name := "parser-level SystemVerilog refinement", evidence := .target,
      closed := false },
    { name := "Janus silicon", evidence := .target,
      closed := false } ]

def janusCellOpenLaneAttempt : SynthesisAttempt :=
  { runDate := "2026-07-07",
    tool := "OpenLane v2.3.10",
    pdk := "sky130A open_pdks 0fe599b2afb6708d281543108caf8310912f54af",
    flow := "Classic through OpenROAD.STAPrePNR",
    runTag := "synthesis-2026-07-07-classic",
    boundedMinutes := 30,
    reachedPrePnrSta := false,
    yosysCheckProblems := 0,
    memoriesRemaining := 0,
    postDffCells := 318547,
    mappedSky130Flops := 40994,
    postDffSequentialAreaUm2 := "875972.627200",
    finalAbcCompleted := false }

def janusCellMacroSynth : MacroSynthesisResult :=
  { runDate := "2026-07-07",
    tool := "Yosys 0.52",
    pdk := "sky130 open_pdks 0fe599b2afb6708d281543108caf8310912f54af",
    flow :=
      "synth + dfflibmap + abc; janus_sram adapters blackboxed as SRAM macros",
    runTag := "macro-synth-2026-07-07",
    reachedPrePnrSta := false,
    checkProblems := 0,
    inferredMemoriesRemaining := 0,
    sramMacroInstances := 4,
    physicalSramMacros := 5,
    mappedCells := 16511,
    mappedSky130Flops := 802,
    stdCellLogicAreaUm2 := "125809.411200",
    oneSramMacroAreaUm2 := "190712.550000",
    finalMapCompleted := true,
    cycleFaithful := false }

def rtlReleased : Bool := true
def janusSiliconExists : Bool := false

theorem rtl_no_silicon_status :
    rtlReleased = true /\ janusSiliconExists = false := by⊢ rtlReleased = true ∧ janusSiliconExists = false
  native_decideAll goals completed! 🐙

theorem openlane_attempt_did_not_reach_sta :
    janusCellOpenLaneAttempt.reachedPrePnrSta = false := rfl

theorem openlane_attempt_erased_inferred_memories :
    janusCellOpenLaneAttempt.memoriesRemaining = 0 := rfl

theorem macro_synth_completed_mapping :
    janusCellMacroSynth.finalMapCompleted = true := rfl

theorem macro_synth_kept_memories_as_macros :
    janusCellMacroSynth.inferredMemoriesRemaining = 0
      /\ janusCellMacroSynth.sramMacroInstances = 4 := by⊢ janusCellMacroSynth.inferredMemoriesRemaining = 0 ∧ janusCellMacroSynth.sramMacroInstances = 4 native_decideAll goals completed! 🐙

theorem macro_synth_collapsed_flops :
    janusCellMacroSynth.mappedSky130Flops
      < janusCellOpenLaneAttempt.mappedSky130Flops := by⊢ janusCellMacroSynth.mappedSky130Flops < janusCellOpenLaneAttempt.mappedSky130Flops native_decideAll goals completed! 🐙

theorem macro_synth_not_cycle_faithful :
    janusCellMacroSynth.cycleFaithful = false := rfl

end Janus

The status vocabulary is intentionally conservative:

proved means the claim is a Lean theorem in this book.
modeled means the claim follows from a checked analytical model and its stated constants.
recorded means a measured or externally observed constant is copied into the book as evidence, but the book does not reproduce the measurement.
target means design intent, not completed implementation.

This distinction matters because Janus is meant to become hardware. The book can be exact about a processor contract today while still being explicit that parser-level RTL refinement, timing closure, physical area, and power are future work.

The recorded OpenLane run is deliberately conservative evidence, not a usable tile-area claim. It used the generated janus_cell as-is, with inferred 256-entry program, scalar-data, resident-weight, and stream memories. Yosys reported zero pre-synthesis check problems and no inferred latches, but replaced all memories with registers. After DFF legalization the design contained 318547 cells and 40994 mapped sky130 flip-flops; the reported 875972.627200 square microns covers the mapped sequential cells, while the remaining combinational primitives were still before the final technology-mapped netlist. Final ABC mapping did not complete within the bounded run, so no pre-PNR timing number is recorded.

The important warning is architectural rather than cosmetic: the bare inferred-memory cell is a simulator and proof boundary, but standard-cell synthesis turns the hot storage into a very large flop-and-mux fabric. A credible physical area and timing number needs a macro-backed memory boundary.

The second run answers that warning. With the four hot memories behind janus_sram adapters, the same sky130 standard-cell library, and the sky130_sram_1kbyte_1rw1r_32x256_8 macro bound as a blackbox, synthesis reaches a complete technology-mapped netlist. The program, resident-weight, and stream memories become one 32-bit SRAM macro each, and the 64-bit scalar-data memory becomes a dual-read 64-bit adapter that maps to two of the same 32×256 macros, for five physical SRAM macros in all. The mapped design keeps just 802 sky130 flip-flops for the register file and control state, down from 40994, and 16511 total mapped cells, down from 318547, with zero synthesis check problems and no inferred memories left in the logic. The standard-cell logic occupies about 125809 square microns, dominated by the 64-bit MAC datapath; each SRAM macro is about 190712 square microns, so a macro-backed tile is roughly nine-tenths SRAM by area.

This is deliberately recorded as a synthesis-shape experiment, not a cycle-faithful implementation. The proved janus_sram adapter reads combinationally, while the sky130 macro is a synchronous-read SRAM. Binding the macro therefore demonstrates area and mappability at the documented boundary; a cycle-accurate macro cell needs a registered-read pipeline stage and its own refinement obligation, and full placement, routing, and static timing over the placed macros remain the next physical step.