13. Load and Utilization Models🔗

The processor contract is not enough by itself; the resident-weight path must also be fed. This chapter records the small analytical models that set Janus's early physical design rule: a coarse SRAM lattice can keep the kernel compute-bound, while edge-only loading recreates the memory wall.

namespace Janus

def meshR : Nat := 32
def defaultBlockSize : Nat := 32
def macroBlocksPerCycle : Nat := 1
def computePerCellMilli : Nat := 1000

def cellsPerMacro (pitch : Nat) : Nat := pitch * pitch

def loadPerCellMilli (pitch : Nat) : Nat :=
  macroBlocksPerCycle * defaultBlockSize * 1000 / cellsPerMacro pitch

def doubleBufferOK (pitch : Nat) : Bool :=
  decide (computePerCellMilli <= loadPerCellMilli pitch)

def decodeSustainMilli (pitch : Nat) : Nat :=
  Nat.min (loadPerCellMilli pitch) computePerCellMilli * 1000 /
    computePerCellMilli

theorem lattice_pitch_rule :
    doubleBufferOK 4 = true
      /\ doubleBufferOK 5 = true
      /\ doubleBufferOK 8 = false
      /\ decodeSustainMilli 4 = 1000
      /\ decodeSustainMilli 32 < 50 := by⊢ doubleBufferOK 4 = true ∧
  doubleBufferOK 5 = true ∧ doubleBufferOK 8 = false ∧ decodeSustainMilli 4 = 1000 ∧ decodeSustainMilli 32 < 50
  native_decideAll goals completed! 🐙

Routing cost is shaped by precision and physical spread. The default path keeps operand transport narrow and pays for precision in the accumulator, not in every operand hop.

def ceilSqrt (n : Nat) : Nat :=
  let s := Nat.sqrt n
  if s * s < n then s + 1 else s

def spreadOf (memoryComputeRatio : Nat) : Nat :=
  ceilSqrt (memoryComputeRatio + 1)

structure Precision where
  operandBytes : Nat
  accBytes : Nat

def bfp8 : Precision := { operandBytes := 1, accBytes := 4 }
def bf16 : Precision := { operandBytes := 2, accBytes := 4 }
def fp32 : Precision := { operandBytes := 4, accBytes := 4 }

def routedPerMac (p : Precision) (ratio : Nat) : Nat :=
  (p.operandBytes + p.accBytes) * spreadOf ratio

theorem routing_wall_bounded :
    routedPerMac bfp8 7 < routedPerMac fp32 7
      /\ routedPerMac fp32 7 = 3 * routedPerMac fp32 0
      /\ routedPerMac bfp8 0 < routedPerMac bfp8 7 := by⊢ routedPerMac bfp8 7 < routedPerMac fp32 7 ∧
  routedPerMac fp32 7 = 3 * routedPerMac fp32 0 ∧ routedPerMac bfp8 0 < routedPerMac bfp8 7
  native_decideAll goals completed! 🐙

The scoreboard is deliberately same-node and utilization-based: it compares how much of each machine's own compute-bound peak is delivered in each regime. The numbers here are measured or modeled constants recorded in the Janus book, not claims of measured Janus silicon.

def gpuPrefillTokS : Nat := 76206
def gpuDecodeB1TokS : Nat := 430
def gpuDecodeB32TokS : Nat := 8523

def gpuUtilMilli (tokS : Nat) : Nat :=
  tokS * 1000 / gpuPrefillTokS

def janusPrefillUtilMilli : Nat := 900
def janusDecodeUtilMilli (pitch : Nat) : Nat :=
  decodeSustainMilli pitch

def sameNodeRatioMilli (janus gpu : Nat) : Nat :=
  janus * 1000 / Nat.max 1 gpu

theorem utilization_scoreboard :
    janusDecodeUtilMilli 4 > 100 * gpuUtilMilli gpuDecodeB1TokS
      /\ gpuUtilMilli gpuDecodeB1TokS < 10
      /\ janusPrefillUtilMilli < 1000
      /\ janusDecodeUtilMilli 32 < janusDecodeUtilMilli 4 := by⊢ janusDecodeUtilMilli 4 > 100 * gpuUtilMilli gpuDecodeB1TokS ∧
  gpuUtilMilli gpuDecodeB1TokS < 10 ∧ janusPrefillUtilMilli < 1000 ∧ janusDecodeUtilMilli 32 < janusDecodeUtilMilli 4
  native_decideAll goals completed! 🐙

end Janus