Main.lean

import Std

namespace Lean64

-- Native code only owns the window, key polling, and framebuffer presentation.
@[extern "lean64_create_window"]
opaque createWindow (width height : UInt32) (visible : Bool) : IO Bool

@[extern "lean64_key_down"]
opaque keyDown (virtualKey : UInt32) : IO Bool

@[extern "lean64_mouse_delta"]
opaque mouseDelta : IO UInt64

@[extern "lean64_play_shot"]
opaque playShot : IO Unit

@[extern "lean64_play_chaingun"]
opaque playChaingun : IO Unit

@[extern "lean64_play_cue"]
opaque playCue (cue : UInt32) : IO Unit

@[extern "lean64_present"]
opaque present (pixels : @& Array UInt32) (width height : UInt32) : IO Bool

@[extern "lean64_present_gpu"]
opaque presentGpu (triangles : @& Array UInt64) (hud : @& Array UInt32)
  (hudWidth hudHeight : UInt32) (cameraX cameraY cameraZ yaw pitch : UInt64) : IO Bool

@[extern "lean64_close_window"]
opaque closeWindow : IO Unit

def renderWidth : Nat := 128
def renderHeight : Nat := 72
def targetFrameMs : Nat := 16
def nearPlane : Float := 0.08
def focalLength : Float := 92.0

structure Vec3 where
  x : Float
  y : Float
  z : Float

namespace Vec3

def add (a b : Vec3) : Vec3 := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
def sub (a b : Vec3) : Vec3 := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩
def scale (a : Vec3) (s : Float) : Vec3 := ⟨a.x * s, a.y * s, a.z * s⟩
def dot (a b : Vec3) : Float := a.x * b.x + a.y * b.y + a.z * b.z
def length (a : Vec3) : Float := (dot a a).sqrt

def normalize (a : Vec3) : Vec3 :=
  let length := a.length
  if length < 0.0001 then ⟨0.0, 0.0, 0.0⟩ else a.scale (1.0 / length)

end Vec3

structure Color where
  r : Nat
  g : Nat
  b : Nat

structure Triangle where
  a : Vec3
  b : Vec3
  c : Vec3
  color : Color
  material : Nat

structure ScreenVertex where
  x : Float
  y : Float
  depth : Float

structure Camera where
  position : Vec3
  yaw : Float
  pitch : Float

structure Enemy where
  position : Vec3
  health : Nat
  attackCooldown : Float := 0.0
  phase : Float := 0.0
  kind : Nat := 0
  alerted : Bool := false
  painTime : Float := 0.0
  deathTime : Float := 0.0
  attackWindup : Float := 0.0
  countsForExit : Bool := true

structure Barrel where
  position : Vec3
  health : Nat := 1
  blastTime : Float := 0.0

structure Projectile where
  position : Vec3
  velocity : Vec3
  life : Float
  damage : Nat := 12

structure Particle where
  position : Vec3
  velocity : Vec3
  life : Float
  kind : Nat := 0

structure ImpactMark where
  position : Vec3
  kind : Nat := 0

structure Pickup where
  position : Vec3
  kind : Nat
  active : Bool := true

structure GameState where
  camera : Camera
  enemies : Array Enemy
  barrels : Array Barrel
  ammo : Nat
  bullets : Nat
  weapon : Nat
  hasChaingun : Bool
  hasRedKey : Bool
  muzzleFlash : Nat
  health : Nat
  damageFlash : Nat
  score : Nat
  projectiles : Array Projectile
  particles : Array Particle
  marks : Array ImpactMark
  weaponCooldown : Float
  bobPhase : Float
  bobStrength : Float
  recoilKick : Float
  hitMarker : Nat
  pickupFlash : Nat
  pickups : Array Pickup
  doorOpen : Float
  levelComplete : Bool
  shotThisFrame : Bool
  mapOpen : Bool
  secretFound : Bool
  secretFlash : Nat
  keyFlash : Nat
  cacheFound : Bool
  cacheDoorOpen : Float
  started : Bool
  paused : Bool
  playTime : Float
  shotsFired : Nat
  shotsHit : Nat
  killsMade : Nat
  difficulty : Nat
  level : Nat

structure Input where
  forward : Bool
  backward : Bool
  left : Bool
  right : Bool
  lookLeft : Bool
  lookRight : Bool
  lookUp : Bool
  lookDown : Bool
  mouseX : Float
  mouseY : Float
  sprint : Bool
  shoot : Bool
  use : Bool
  weapon1 : Bool
  weapon2 : Bool
  weapon3 : Bool
  map : Bool
  confirm : Bool
  pause : Bool
  restart : Bool
  quit : Bool

def noInput : Input := {
  forward := false, backward := false, left := false, right := false
  lookLeft := false, lookRight := false, lookUp := false, lookDown := false
  mouseX := 0.0, mouseY := 0.0
  sprint := false, shoot := false, use := false, weapon1 := false, weapon2 := false
  weapon3 := false
  map := false, restart := false, quit := false
  confirm := false, pause := false
}

def floatToNat (value : Float) : Nat := value.floor.toUInt64.toNat

def clampedNat (value : Float) (limit : Nat) : Nat :=
  if value < 0.0 then 0 else min limit (floatToNat value)

def colorScale (color : Color) (amount : Float) : Color :=
  let channel (value : Nat) := min 255 (floatToNat (Float.ofNat value * amount))
  ⟨channel color.r, channel color.g, channel color.b⟩

def quadMaterial (a b c d : Vec3) (color : Color) (material : Nat) : Array Triangle := #[
  { a, b, c, color, material }, { a, b := c, c := d, color, material }
]

def quad (a b c d : Vec3) (color : Color) : Array Triangle :=
  quadMaterial a b c d color 0

def boxMeshMaterial (minimum maximum : Vec3) (color : Color) (material : Nat) : Array Triangle :=
  let p000 : Vec3 := ⟨minimum.x, minimum.y, minimum.z⟩
  let p001 : Vec3 := ⟨minimum.x, minimum.y, maximum.z⟩
  let p010 : Vec3 := ⟨minimum.x, maximum.y, minimum.z⟩
  let p011 : Vec3 := ⟨minimum.x, maximum.y, maximum.z⟩
  let p100 : Vec3 := ⟨maximum.x, minimum.y, minimum.z⟩
  let p101 : Vec3 := ⟨maximum.x, minimum.y, maximum.z⟩
  let p110 : Vec3 := ⟨maximum.x, maximum.y, minimum.z⟩
  let p111 : Vec3 := ⟨maximum.x, maximum.y, maximum.z⟩
  let dark := colorScale color 0.55
  let side := colorScale color 0.78
  let top := colorScale color 1.15
  quadMaterial p001 p101 p111 p011 color material ++
  quadMaterial p100 p000 p010 p110 dark material ++
  quadMaterial p000 p001 p011 p010 side material ++
  quadMaterial p101 p100 p110 p111 side material ++
  quadMaterial p010 p011 p111 p110 top material ++
  quadMaterial p000 p100 p101 p001 dark material

def boxMesh (minimum maximum : Vec3) (color : Color) : Array Triangle :=
  boxMeshMaterial minimum maximum color 0

def floorMesh : Array Triangle := Id.run do
  let mut triangles := #[]
  for z in [0:4] do
    for x in [0:4] do
      let x0 := Float.ofNat x * 4.0 - 8.0
      let z0 := Float.ofNat z * 4.0 - 8.0
      let color : Color := if (x + z) % 2 == 0 then ⟨44, 48, 58⟩ else ⟨34, 38, 48⟩
      triangles := triangles ++ quadMaterial
        ⟨x0, 0.0, z0⟩ ⟨x0 + 4.0, 0.0, z0⟩
        ⟨x0 + 4.0, 0.0, z0 + 4.0⟩ ⟨x0, 0.0, z0 + 4.0⟩ color 3
  return triangles

def ceilingMesh : Array Triangle := Id.run do
  let mut triangles := #[]
  for z in [0:4] do
    for x in [0:4] do
      let x0 := Float.ofNat x * 4.0 - 8.0
      let z0 := Float.ofNat z * 4.0 - 8.0
      let color : Color := if (x + z) % 2 == 0 then ⟨32, 34, 43⟩ else ⟨25, 27, 35⟩
      triangles := triangles ++ quadMaterial
        ⟨x0, 3.5, z0⟩ ⟨x0, 3.5, z0 + 4.0⟩
        ⟨x0 + 4.0, 3.5, z0 + 4.0⟩ ⟨x0 + 4.0, 3.5, z0⟩ color 2
  return triangles

def levelOneWorld : Array Triangle :=
  floorMesh ++ ceilingMesh ++
  boxMeshMaterial ⟨-8.2, 0.0, -8.2⟩ ⟨-7.7, 3.5, 8.2⟩ ⟨90, 74, 72⟩ 1 ++
  boxMeshMaterial ⟨7.7, 0.0, -8.2⟩ ⟨8.2, 3.5, 8.2⟩ ⟨90, 74, 72⟩ 1 ++
  boxMeshMaterial ⟨-8.2, 0.0, -8.2⟩ ⟨8.2, 3.5, -7.7⟩ ⟨90, 74, 72⟩ 1 ++
  boxMeshMaterial ⟨-8.2, 0.0, 7.7⟩ ⟨8.2, 3.5, 8.2⟩ ⟨90, 74, 72⟩ 1 ++
  boxMeshMaterial ⟨-3.8, 0.0, -1.0⟩ ⟨-2.2, 2.6, 1.0⟩ ⟨74, 99, 126⟩ 2 ++
  -- Hollow maintenance cache: four thick walls, split front, and a low roof.
  boxMeshMaterial ⟨2.0, 0.0, 1.8⟩ ⟨2.25, 2.35, 3.2⟩ ⟨122, 73, 52⟩ 1 ++
  boxMeshMaterial ⟨3.55, 0.0, 1.8⟩ ⟨3.8, 2.35, 3.2⟩ ⟨122, 73, 52⟩ 1 ++
  boxMeshMaterial ⟨2.25, 0.0, 2.95⟩ ⟨3.55, 2.35, 3.2⟩ ⟨122, 73, 52⟩ 1 ++
  boxMeshMaterial ⟨2.0, 0.0, 1.8⟩ ⟨2.55, 2.35, 2.05⟩ ⟨122, 73, 52⟩ 1 ++
  boxMeshMaterial ⟨3.25, 0.0, 1.8⟩ ⟨3.8, 2.35, 2.05⟩ ⟨122, 73, 52⟩ 1 ++
  boxMeshMaterial ⟨2.0, 2.15, 1.8⟩ ⟨3.8, 2.42, 3.2⟩ ⟨74, 82, 90⟩ 2 ++
  boxMeshMaterial ⟨-0.8, 0.0, 4.2⟩ ⟨0.8, 3.2, 5.4⟩ ⟨65, 91, 72⟩ 2 ++
  -- Low, hot wall lights and a toxic-green exit marker.
  boxMeshMaterial ⟨-7.68, 0.65, -3.2⟩ ⟨-7.58, 1.55, -1.6⟩ ⟨235, 48, 22⟩ 4 ++
  boxMeshMaterial ⟨7.58, 0.65, 2.0⟩ ⟨7.68, 1.55, 3.6⟩ ⟨235, 48, 22⟩ 4 ++
  boxMeshMaterial ⟨-0.55, 2.25, 5.38⟩ ⟨0.55, 2.85, 5.48⟩ ⟨65, 240, 105⟩ 4 ++
  -- A cross-room bulkhead leaves a central doorway between encounters.
  boxMeshMaterial ⟨-8.0, 0.0, 0.45⟩ ⟨-1.28, 3.5, 0.78⟩ ⟨68, 76, 86⟩ 2 ++
  boxMeshMaterial ⟨1.28, 0.0, 0.45⟩ ⟨8.0, 3.5, 0.78⟩ ⟨68, 76, 86⟩ 2 ++
  boxMeshMaterial ⟨-1.72, 3.18, 0.38⟩ ⟨1.72, 3.46, 0.84⟩ ⟨95, 102, 110⟩ 2

def levelTwoWorld : Array Triangle :=
  floorMesh ++ ceilingMesh ++
  boxMeshMaterial ⟨-8.2, 0.0, -8.2⟩ ⟨-7.7, 3.5, 8.2⟩ ⟨52, 76, 78⟩ 2 ++
  boxMeshMaterial ⟨7.7, 0.0, -8.2⟩ ⟨8.2, 3.5, 8.2⟩ ⟨52, 76, 78⟩ 2 ++
  boxMeshMaterial ⟨-8.2, 0.0, -8.2⟩ ⟨8.2, 3.5, -7.7⟩ ⟨52, 76, 78⟩ 2 ++
  boxMeshMaterial ⟨-8.2, 0.0, 7.7⟩ ⟨8.2, 3.5, 8.2⟩ ⟨52, 76, 78⟩ 2 ++
  -- Alternating bulkheads force a right-left-right combat route.
  boxMeshMaterial ⟨-8.0, 0.0, -2.75⟩ ⟨2.0, 2.72, -2.20⟩ ⟨70, 88, 96⟩ 2 ++
  boxMeshMaterial ⟨-2.0, 0.0, 0.68⟩ ⟨8.0, 2.72, 1.23⟩ ⟨70, 88, 96⟩ 2 ++
  boxMeshMaterial ⟨-8.0, 0.0, 4.00⟩ ⟨2.0, 2.72, 4.55⟩ ⟨70, 88, 96⟩ 2 ++
  -- Emissive route beacons and exit-side pylons.
  boxMeshMaterial ⟨1.55, 0.62, -2.82⟩ ⟨1.92, 1.62, -2.72⟩ ⟨35, 215, 205⟩ 4 ++
  boxMeshMaterial ⟨-1.92, 0.62, 1.23⟩ ⟨-1.55, 1.62, 1.33⟩ ⟨35, 215, 205⟩ 4 ++
  boxMeshMaterial ⟨1.55, 0.62, 3.90⟩ ⟨1.92, 1.62, 4.00⟩ ⟨35, 215, 205⟩ 4 ++
  boxMeshMaterial ⟨5.45, 0.0, 5.45⟩ ⟨5.85, 2.25, 5.85⟩ ⟨85, 48, 94⟩ 1 ++
  boxMeshMaterial ⟨6.95, 0.0, 5.45⟩ ⟨7.35, 2.25, 5.85⟩ ⟨85, 48, 94⟩ 1

def doorMesh (openAmount : Float) : Array Triangle :=
  let bottom := openAmount * 3.25
  if bottom >= 3.24 then #[]
  else boxMeshMaterial ⟨-1.26, bottom, 0.47⟩ ⟨1.26, 3.28, 0.76⟩ ⟨110, 104, 88⟩ 2

def doorSwitchMesh (hasKey : Bool) (openAmount : Float) : Array Triangle :=
  let color : Color := if openAmount >= 0.86 then ⟨60, 238, 108⟩
    else if hasKey then ⟨250, 184, 48⟩ else ⟨238, 48, 35⟩
  boxMeshMaterial ⟨1.38, 1.0, 0.38⟩ ⟨1.72, 1.52, 0.46⟩ color 4 ++
  boxMeshMaterial ⟨1.45, 1.16, 0.36⟩ ⟨1.65, 1.36, 0.38⟩
    (if hasKey then ⟨255, 232, 105⟩ else ⟨105, 18, 22⟩) 4

def cacheDoorMesh (openAmount : Float) : Array Triangle :=
  let bottom := openAmount * 2.28
  if bottom >= 2.26 then #[]
  else boxMeshMaterial ⟨2.55, bottom, 1.79⟩ ⟨3.25, 2.30, 2.04⟩ ⟨118, 70, 50⟩ 1

def cacheSwitchMesh (found : Bool) : Array Triangle :=
  let color : Color := if found then ⟨65, 238, 112⟩ else ⟨118, 52, 42⟩
  boxMeshMaterial ⟨2.12, 0.82, 1.70⟩ ⟨2.43, 1.34, 1.82⟩ color 4 ++
  boxMeshMaterial ⟨2.20, 0.98, 1.67⟩ ⟨2.35, 1.18, 1.70⟩
    (if found then ⟨250, 210, 72⟩ else ⟨56, 24, 22⟩) 4

def exitMeshAt (centerX centerZ : Float) (unlocked complete : Bool) : Array Triangle :=
  let color : Color := if complete then ⟨225, 235, 255⟩
    else if unlocked then ⟨52, 245, 102⟩ else ⟨215, 35, 24⟩
  boxMeshMaterial ⟨centerX - 0.78, 0.025, centerZ - 0.38⟩
    ⟨centerX + 0.78, 0.11, centerZ + 0.38⟩ color 4

def secretPanelMesh (found : Bool) : Array Triangle :=
  let panel : Color := if found then ⟨65, 235, 112⟩ else ⟨76, 56, 50⟩
  let rune : Color := if found then ⟨250, 205, 70⟩ else ⟨128, 44, 34⟩
  -- A suspicious inset panel on the western wall. The lit rune changes when used.
  boxMeshMaterial ⟨-7.68, 0.62, -5.0⟩ ⟨-7.57, 1.82, -3.72⟩ panel 2 ++
  boxMeshMaterial ⟨-7.56, 0.92, -4.66⟩ ⟨-7.50, 1.52, -4.52⟩ rune 4 ++
  boxMeshMaterial ⟨-7.56, 1.15, -4.90⟩ ⟨-7.50, 1.29, -4.28⟩ rune 4

def wardenMesh (enemy : Enemy) : Array Triangle :=
  let p := enemy.position
  let bob := enemy.phase.sin * 0.045
  let armor : Color := if enemy.painTime > 0.0 then ⟨255, 210, 220⟩ else ⟨74, 42, 94⟩
  let flesh : Color := if enemy.painTime > 0.0 then ⟨255, 175, 165⟩ else ⟨165, 58, 72⟩
  let dark := colorScale armor 0.52
  let eye : Color := if enemy.alerted then ⟨255, 92, 245⟩ else ⟨90, 42, 82⟩
  -- Heavy plated torso, horned head, oversized fists, split armored legs, and reactor core.
  boxMeshMaterial ⟨p.x - 0.55, 0.52 + bob, p.z - 0.38⟩
    ⟨p.x + 0.55, 1.55 + bob, p.z + 0.38⟩ armor 2 ++
  boxMesh ⟨p.x - 0.62, 1.45 + bob, p.z - 0.44⟩
    ⟨p.x + 0.62, 2.18 + bob, p.z + 0.44⟩ flesh ++
  boxMeshMaterial ⟨p.x - 0.92, 1.92 + bob, p.z - 0.18⟩
    ⟨p.x - 0.52, 2.38 + bob, p.z + 0.18⟩ dark 2 ++
  boxMeshMaterial ⟨p.x + 0.52, 1.92 + bob, p.z - 0.18⟩
    ⟨p.x + 0.92, 2.38 + bob, p.z + 0.18⟩ dark 2 ++
  boxMeshMaterial ⟨p.x - 0.92, 0.58 + bob, p.z - 0.30⟩
    ⟨p.x - 0.56, 1.55 + bob, p.z + 0.30⟩ armor 2 ++
  boxMeshMaterial ⟨p.x + 0.56, 0.58 + bob, p.z - 0.30⟩
    ⟨p.x + 0.92, 1.55 + bob, p.z + 0.30⟩ armor 2 ++
  boxMeshMaterial ⟨p.x - 0.48, 0.0, p.z - 0.30⟩
    ⟨p.x - 0.08, 0.62 + bob, p.z + 0.30⟩ dark 2 ++
  boxMeshMaterial ⟨p.x + 0.08, 0.0, p.z - 0.30⟩
    ⟨p.x + 0.48, 0.62 + bob, p.z + 0.30⟩ dark 2 ++
  boxMeshMaterial ⟨p.x - 0.36, 1.76 + bob, p.z - 0.47⟩
    ⟨p.x - 0.10, 1.94 + bob, p.z - 0.43⟩ eye 4 ++
  boxMeshMaterial ⟨p.x + 0.10, 1.76 + bob, p.z - 0.47⟩
    ⟨p.x + 0.36, 1.94 + bob, p.z - 0.43⟩ eye 4 ++
  boxMeshMaterial ⟨p.x - 0.22, 0.92 + bob, p.z - 0.41⟩
    ⟨p.x + 0.22, 1.30 + bob, p.z - 0.38⟩ ⟨200, 45, 235⟩ 4 ++
  (if enemy.attackWindup > 0.0 then
    let pulse := 0.18 + (0.30 - enemy.attackWindup) * 0.65
    boxMeshMaterial ⟨p.x - pulse, 1.20 + bob - pulse, p.z - 0.65 - pulse⟩
      ⟨p.x + pulse, 1.20 + bob + pulse, p.z - 0.61 + pulse⟩ ⟨200, 42, 255⟩ 4 ++
    boxMeshMaterial ⟨p.x - pulse * 0.45, 1.20 + bob - pulse * 0.45, p.z - 0.70⟩
      ⟨p.x + pulse * 0.45, 1.20 + bob + pulse * 0.45, p.z - 0.58⟩ ⟨255, 175, 255⟩ 4
  else #[])

def enemyMesh (enemy : Enemy) : Array Triangle :=
  if enemy.health == 0 then
    let p := enemy.position
    let fall := 1.0 - min 1.0 (enemy.deathTime / 0.62)
    let boss := enemy.kind == 3
    let torsoTop := if boss then 1.62 - fall * 1.34 else 1.18 - fall * 0.94
    let headY := if boss then 1.72 - fall * 1.48 else 1.26 - fall * 1.08
    let bodyWidth := if boss then 0.68 else 0.36
    let bodyDepth := if boss then 0.46 else 0.28
    let headWidth := if boss then 0.78 else 0.44
    let corpseColor : Color := if boss then ⟨86, 24, 100⟩ else ⟨120, 34, 28⟩
    boxMeshMaterial ⟨p.x - bodyWidth, 0.04, p.z - bodyDepth⟩
      ⟨p.x + bodyWidth, max 0.17 torsoTop, p.z + bodyDepth⟩ corpseColor 3 ++
    boxMeshMaterial ⟨p.x - headWidth, max 0.05 headY, p.z - bodyDepth⟩
      ⟨p.x + headWidth, max 0.18 (headY + if boss then 0.46 else 0.34), p.z + bodyDepth⟩
        (if boss then ⟨58, 18, 72⟩ else ⟨92, 24, 22⟩) 3
  else if enemy.kind == 3 then wardenMesh enemy
  else
    let p := enemy.position
    let bob := enemy.phase.sin * 0.07
    let skin : Color := if enemy.kind % 2 == 0 then ⟨105, 154, 74⟩ else ⟨155, 74, 92⟩
    let wounded : Color := if enemy.painTime > 0.0 then ⟨255, 205, 180⟩
      else if enemy.health == 1 then ⟨235, 70, 42⟩ else skin
    let dark := colorScale wounded 0.55
    let eye : Color := if enemy.alerted then ⟨255, 225, 72⟩ else ⟨82, 72, 34⟩
    -- Torso, oversized head, swinging arms, split legs, and bright inset eyes.
    boxMesh ⟨p.x - 0.34, 0.48 + bob, p.z - 0.24⟩
      ⟨p.x + 0.34, 1.28 + bob, p.z + 0.24⟩ wounded ++
    boxMesh ⟨p.x - 0.42, 1.22 + bob, p.z - 0.32⟩
      ⟨p.x + 0.42, 1.82 + bob, p.z + 0.32⟩ wounded ++
    boxMesh ⟨p.x - 0.58, 0.52 + bob + enemy.phase.sin * 0.08, p.z - 0.17⟩
      ⟨p.x - 0.36, 1.30 + bob, p.z + 0.17⟩ dark ++
    boxMesh ⟨p.x + 0.36, 0.52 + bob - enemy.phase.sin * 0.08, p.z - 0.17⟩
      ⟨p.x + 0.58, 1.30 + bob, p.z + 0.17⟩ dark ++
    boxMesh ⟨p.x - 0.31, 0.0, p.z - 0.18⟩ ⟨p.x - 0.05, 0.52 + bob, p.z + 0.18⟩ dark ++
    boxMesh ⟨p.x + 0.05, 0.0, p.z - 0.18⟩ ⟨p.x + 0.31, 0.52 + bob, p.z + 0.18⟩ dark ++
    boxMeshMaterial ⟨p.x - 0.25, 1.48 + bob, p.z - 0.345⟩
      ⟨p.x - 0.08, 1.62 + bob, p.z - 0.32⟩ eye 4 ++
    boxMeshMaterial ⟨p.x + 0.08, 1.48 + bob, p.z - 0.345⟩
      ⟨p.x + 0.25, 1.62 + bob, p.z - 0.32⟩ eye 4 ++
    (if enemy.attackWindup > 0.0 then
      let pulse := 0.10 + (0.35 - enemy.attackWindup) * 0.32
      boxMeshMaterial ⟨p.x - pulse, 1.04 + bob - pulse, p.z - 0.48 - pulse⟩
        ⟨p.x + pulse, 1.04 + bob + pulse, p.z - 0.46 + pulse⟩ ⟨255, 112, 24⟩ 4 ++
      boxMeshMaterial ⟨p.x - pulse * 0.45, 1.04 + bob - pulse * 0.45, p.z - 0.52⟩
        ⟨p.x + pulse * 0.45, 1.04 + bob + pulse * 0.45, p.z - 0.44⟩ ⟨255, 238, 125⟩ 4
    else #[])

def projectileMesh (projectile : Projectile) : Array Triangle :=
  let p := projectile.position
  let radius := if projectile.damage > 12 then 0.22 else 0.13
  let core := if projectile.damage > 12 then 0.11 else 0.06
  boxMeshMaterial ⟨p.x - radius, p.y - radius, p.z - radius⟩
    ⟨p.x + radius, p.y + radius, p.z + radius⟩
      (if projectile.damage > 12 then ⟨198, 42, 255⟩ else ⟨255, 82, 18⟩) 4 ++
  boxMeshMaterial ⟨p.x - core, p.y - radius * 1.55, p.z - core⟩
    ⟨p.x + core, p.y + radius * 1.55, p.z + core⟩
      (if projectile.damage > 12 then ⟨255, 155, 255⟩ else ⟨255, 210, 62⟩) 4

def particleMesh (particle : Particle) : Array Triangle :=
  let p := particle.position
  let radius := if particle.kind == 1 then 0.062 else if particle.kind == 2 then 0.082 else 0.086
  let color : Color := if particle.kind == 0 then ⟨195, 24, 32⟩
    else if particle.kind == 1 then ⟨255, 192, 54⟩ else ⟨62, 54, 48⟩
  boxMeshMaterial ⟨p.x - radius, p.y - radius, p.z - radius⟩
    ⟨p.x + radius, p.y + radius, p.z + radius⟩ color
      (if particle.kind == 1 then 4 else 3)

def impactMarkMesh (mark : ImpactMark) : Array Triangle :=
  let p := mark.position
  if mark.kind == 1 then
    boxMeshMaterial ⟨p.x - 0.34, 0.012, p.z - 0.28⟩
      ⟨p.x + 0.34, 0.035, p.z + 0.28⟩ ⟨93, 14, 22⟩ 3 ++
    boxMeshMaterial ⟨p.x - 0.17, 0.035, p.z - 0.13⟩
      ⟨p.x + 0.17, 0.048, p.z + 0.13⟩ ⟨145, 20, 28⟩ 3
  else
    boxMeshMaterial ⟨p.x - 0.085, p.y - 0.085, p.z - 0.085⟩
      ⟨p.x + 0.085, p.y + 0.085, p.z + 0.085⟩ ⟨34, 25, 24⟩ 3 ++
    boxMeshMaterial ⟨p.x - 0.035, p.y - 0.035, p.z - 0.035⟩
      ⟨p.x + 0.035, p.y + 0.035, p.z + 0.035⟩ ⟨190, 74, 35⟩ 4

def barrelMesh (barrel : Barrel) : Array Triangle :=
  let p := barrel.position
  if barrel.health > 0 then
    boxMeshMaterial ⟨p.x - 0.34, 0.05, p.z - 0.34⟩
      ⟨p.x + 0.34, 1.02, p.z + 0.34⟩ ⟨44, 112, 62⟩ 2 ++
    boxMeshMaterial ⟨p.x - 0.38, 0.10, p.z - 0.38⟩
      ⟨p.x + 0.38, 0.23, p.z + 0.38⟩ ⟨52, 58, 61⟩ 2 ++
    boxMeshMaterial ⟨p.x - 0.38, 0.82, p.z - 0.38⟩
      ⟨p.x + 0.38, 0.95, p.z + 0.38⟩ ⟨52, 58, 61⟩ 2 ++
    boxMeshMaterial ⟨p.x - 0.16, 0.42, p.z - 0.355⟩
      ⟨p.x + 0.16, 0.68, p.z - 0.34⟩ ⟨235, 185, 42⟩ 4
  else if barrel.blastTime > 0.0 then
    let progress := 1.0 - barrel.blastTime / 0.28
    let radius := 0.28 + progress * 1.28
    boxMeshMaterial ⟨p.x - radius, 0.18, p.z - radius⟩
      ⟨p.x + radius, 0.58 + radius, p.z + radius⟩ ⟨255, 72, 18⟩ 4 ++
    boxMeshMaterial ⟨p.x - radius * 0.55, 0.32, p.z - radius * 0.55⟩
      ⟨p.x + radius * 0.55, 0.52 + radius, p.z + radius * 0.55⟩ ⟨255, 230, 90⟩ 4
  else
    boxMeshMaterial ⟨p.x - 0.43, 0.02, p.z - 0.38⟩
      ⟨p.x + 0.43, 0.13, p.z + 0.38⟩ ⟨39, 34, 31⟩ 3

def pickupMesh (pickup : Pickup) : Array Triangle :=
  if !pickup.active then #[]
  else
    let p := pickup.position
    if pickup.kind == 0 then
      -- Blue health vial with a bright glass neck.
      boxMeshMaterial ⟨p.x - 0.16, 0.05, p.z - 0.16⟩
        ⟨p.x + 0.16, 0.36, p.z + 0.16⟩ ⟨38, 105, 245⟩ 4 ++
      boxMeshMaterial ⟨p.x - 0.08, 0.36, p.z - 0.08⟩
        ⟨p.x + 0.08, 0.52, p.z + 0.08⟩ ⟨135, 215, 255⟩ 4
    else if pickup.kind == 1 then
      -- Brass-striped shell box.
      boxMeshMaterial ⟨p.x - 0.28, 0.04, p.z - 0.20⟩
        ⟨p.x + 0.28, 0.28, p.z + 0.20⟩ ⟨102, 58, 34⟩ 1 ++
      boxMeshMaterial ⟨p.x - 0.22, 0.28, p.z - 0.15⟩
        ⟨p.x + 0.22, 0.34, p.z + 0.15⟩ ⟨238, 177, 46⟩ 4
    else if pickup.kind == 2 then
      -- Chaingun pickup: heavy receiver, twin grips, and a long barrel cluster.
      boxMeshMaterial ⟨p.x - 0.36, 0.18, p.z - 0.24⟩
        ⟨p.x + 0.36, 0.54, p.z + 0.24⟩ ⟨72, 77, 84⟩ 2 ++
      boxMeshMaterial ⟨p.x - 0.18, 0.54, p.z - 0.13⟩
        ⟨p.x + 0.18, 1.12, p.z + 0.13⟩ ⟨155, 162, 164⟩ 2 ++
      boxMeshMaterial ⟨p.x - 0.32, 0.02, p.z - 0.18⟩
        ⟨p.x - 0.12, 0.30, p.z + 0.18⟩ ⟨96, 56, 32⟩ 1 ++
      boxMeshMaterial ⟨p.x + 0.12, 0.02, p.z - 0.18⟩
        ⟨p.x + 0.32, 0.30, p.z + 0.18⟩ ⟨96, 56, 32⟩ 1
    else
      -- Red access card with a bright brass contact stripe.
      boxMeshMaterial ⟨p.x - 0.34, 0.10, p.z - 0.06⟩
        ⟨p.x + 0.34, 0.62, p.z + 0.06⟩ ⟨218, 38, 45⟩ 4 ++
      boxMeshMaterial ⟨p.x - 0.22, 0.20, p.z - 0.075⟩
        ⟨p.x + 0.22, 0.30, p.z + 0.075⟩ ⟨250, 195, 58⟩ 4 ++
      boxMeshMaterial ⟨p.x - 0.20, 0.42, p.z - 0.075⟩
        ⟨p.x - 0.02, 0.54, p.z + 0.075⟩ ⟨255, 120, 105⟩ 4 ++
      boxMeshMaterial ⟨p.x - 0.06, 0.10, p.z - 0.34⟩
        ⟨p.x + 0.06, 0.62, p.z + 0.34⟩ ⟨218, 38, 45⟩ 4 ++
      boxMeshMaterial ⟨p.x - 0.075, 0.20, p.z - 0.22⟩
        ⟨p.x + 0.075, 0.30, p.z + 0.22⟩ ⟨250, 195, 58⟩ 4

def sceneMesh (state : GameState) : Array Triangle :=
  let cleared := state.enemies.all fun enemy => enemy.health == 0 || !enemy.countsForExit
  let dynamicWorld := if state.level == 0 then
    levelOneWorld ++ doorMesh state.doorOpen ++
      doorSwitchMesh state.hasRedKey state.doorOpen ++
      exitMeshAt 0.0 6.8 cleared state.levelComplete ++ secretPanelMesh state.secretFound ++
      cacheDoorMesh state.cacheDoorOpen ++ cacheSwitchMesh state.cacheFound
    else
      levelTwoWorld ++ exitMeshAt 6.35 6.45 cleared state.levelComplete
  let withBarrels := state.barrels.foldl
    (fun triangles barrel => triangles ++ barrelMesh barrel) dynamicWorld
  let withEnemies := state.enemies.foldl
    (fun triangles enemy => triangles ++ enemyMesh enemy) withBarrels
  let withProjectiles := state.projectiles.foldl
    (fun triangles projectile => triangles ++ projectileMesh projectile) withEnemies
  let withParticles := state.particles.foldl
    (fun triangles particle => triangles ++ particleMesh particle) withProjectiles
  let withMarks := state.marks.foldl
    (fun triangles mark => triangles ++ impactMarkMesh mark) withParticles
  state.pickups.foldl
    (fun triangles pickup => triangles ++ pickupMesh pickup) withMarks

def illuminateTriangle (camera : Camera) (flash : Nat) (triangle : Triangle) : Triangle :=
  if flash == 0 || triangle.material == 4 then triangle
  else
    let center : Vec3 := ⟨(triangle.a.x + triangle.b.x + triangle.c.x) / 3.0,
      (triangle.a.y + triangle.b.y + triangle.c.y) / 3.0,
      (triangle.a.z + triangle.b.z + triangle.c.z) / 3.0⟩
    let distance := (center.sub camera.position).length
    let intensity := Float.ofNat flash / 3.0 * max 0.0 (1.0 - distance / 10.0)
    let addChannel (value : Nat) (boost : Float) : Nat :=
      min 255 (value + floatToNat (boost * intensity))
    { triangle with color := ⟨addChannel triangle.color.r 82.0,
      addChannel triangle.color.g 42.0, addChannel triangle.color.b 12.0⟩ }

def worldToCamera (camera : Camera) (point : Vec3) : Vec3 :=
  let relative := point.sub camera.position
  let cosYaw := camera.yaw.cos
  let sinYaw := camera.yaw.sin
  let horizontalX := cosYaw * relative.x - sinYaw * relative.z
  let horizontalZ := sinYaw * relative.x + cosYaw * relative.z
  let cosPitch := camera.pitch.cos
  let sinPitch := camera.pitch.sin
  ⟨horizontalX,
    cosPitch * relative.y - sinPitch * horizontalZ,
    sinPitch * relative.y + cosPitch * horizontalZ⟩

def projectView (view : Vec3) : Option ScreenVertex :=
  if view.z <= nearPlane then none
  else some {
    x := Float.ofNat renderWidth / 2.0 + view.x / view.z * focalLength
    y := Float.ofNat renderHeight / 2.0 - view.y / view.z * focalLength
    depth := view.z
  }

def intersectNear (a b : Vec3) : Vec3 :=
  let amount := (nearPlane - a.z) / (b.z - a.z)
  a.add ((b.sub a).scale amount)

def clipNear (points : List Vec3) : List Vec3 :=
  match points with
  | [] => []
  | first :: _ =>
    let nextPoints := points.drop 1 ++ [first]
    (points.zip nextPoints).flatMap fun (a, b) =>
      let aInside := a.z > nearPlane
      let bInside := b.z > nearPlane
      if aInside && bInside then [b]
      else if aInside && !bInside then [intersectNear a b]
      else if !aInside && bInside then [intersectNear a b, b]
      else []

structure Framebuffer where
  pixels : Array UInt32
  depth : Array Float

def packedColor (color : Color) : UInt32 :=
  UInt32.ofNat (color.b + color.g * 256 + color.r * 65536 + 255 * 16777216)

def newFramebuffer : Framebuffer := Id.run do
  let mut pixels : Array UInt32 := #[]
  for y in [0:renderHeight] do
    let t := Float.ofNat y / Float.ofNat renderHeight
    let sky := if y < renderHeight / 2 then
      colorScale ⟨24, 38, 68⟩ (1.15 - t * 0.35)
    else ⟨18, 20, 28⟩
    for _ in [0:renderWidth] do
      pixels := pixels.push (packedColor sky)
  return { pixels, depth := Array.replicate (renderWidth * renderHeight) 100000.0 }

def transparentFramebuffer : Framebuffer := {
  pixels := Array.replicate (renderWidth * renderHeight) 0
  depth := Array.replicate (renderWidth * renderHeight) 100000.0
}

def edge (a b : ScreenVertex) (x y : Float) : Float :=
  (x - a.x) * (b.y - a.y) - (y - a.y) * (b.x - a.x)

def putPixel (frame : Framebuffer) (x y : Nat) (depth : Float) (color : Color) : Framebuffer :=
  let index := y * renderWidth + x
  if depth >= frame.depth[index]! then frame
  else
    let pixels := frame.pixels.set! index (packedColor color)
    { pixels, depth := frame.depth.set! index depth }

def materialColor (base : Color) (material x y : Nat) : Color :=
  match material with
  | 1 =>
    let stagger := (x + (y / 7) * 8) % 18
    if y % 7 == 0 || stagger == 0 then colorScale base 0.42
    else if (x + y) % 5 == 0 then colorScale base 0.88
    else base
  | 2 =>
    if x % 14 == 0 then colorScale base 0.38
    else if x % 14 == 2 && y % 11 == 2 then colorScale base 1.55
    else if y % 13 == 0 then colorScale base 0.72
    else base
  | 3 =>
    if (x + y * 3) % 11 == 0 then colorScale base 0.62
    else if (x / 4 + y / 3) % 2 == 0 then colorScale base 0.91
    else base
  | 4 => colorScale base 1.35
  | _ => base

def rasterTriangle (frame : Framebuffer) (a b c : ScreenVertex) (color : Color)
    (material : Nat) : Framebuffer := Id.run do
  let area := edge a b c.x c.y
  -- Clockwise triangles are back faces after the viewport's Y flip.
  if area <= 0.001 then return frame
  let minX := clampedNat (min a.x (min b.x c.x)) (renderWidth - 1)
  let maxX := clampedNat (max a.x (max b.x c.x) + 1.0) (renderWidth - 1)
  let minY := clampedNat (min a.y (min b.y c.y)) (renderHeight - 1)
  let maxY := clampedNat (max a.y (max b.y c.y) + 1.0) (renderHeight - 1)
  let mut output := frame
  for y in [minY:maxY + 1] do
    for x in [minX:maxX + 1] do
      let px := Float.ofNat x + 0.5
      let py := Float.ofNat y + 0.5
      let w0 := edge b c px py / area
      let w1 := edge c a px py / area
      let w2 := edge a b px py / area
      if w0 >= 0.0 && w1 >= 0.0 && w2 >= 0.0 then
        let depth := w0 * a.depth + w1 * b.depth + w2 * c.depth
        output := putPixel output x y depth (materialColor color material x y)
  return output

def renderProjectedTriangle (frame : Framebuffer) (color : Color) (material : Nat)
    (a b c : Vec3) : Framebuffer :=
  match projectView a, projectView b, projectView c with
  | some a, some b, some c =>
    let averageDepth := (a.depth + b.depth + c.depth) / 3.0
    let fog := if material == 4 then 1.0 else max 0.28 (min 1.0 (1.15 - averageDepth / 22.0))
    rasterTriangle frame a b c (colorScale color fog) material
  | _, _, _ => frame

def renderTriangle (camera : Camera) (frame : Framebuffer) (triangle : Triangle) : Framebuffer :=
  let clipped := clipNear [worldToCamera camera triangle.a,
    worldToCamera camera triangle.b, worldToCamera camera triangle.c]
  match clipped with
  | [a, b, c] => renderProjectedTriangle frame triangle.color triangle.material a b c
  | [a, b, c, d] =>
    let frame := renderProjectedTriangle frame triangle.color triangle.material a b c
    renderProjectedTriangle frame triangle.color triangle.material a c d
  | _ => frame

def drawRect (frame : Framebuffer) (left top width height : Nat) (color : Color) : Framebuffer := Id.run do
  let mut output := frame
  for y in [top:min renderHeight (top + height)] do
    for x in [left:min renderWidth (left + width)] do
      output := { output with
        pixels := output.pixels.set! (y * renderWidth + x) (packedColor color) }
  return output

-- Screen-space overlays intentionally bypass the z-buffer. Besides making HUD
-- pixels unconditional, updating only the color array is substantially cheaper
-- than copying both persistent arrays for every automap sample.
def overlayPixel (frame : Framebuffer) (x y : Nat) (color : Color) : Framebuffer :=
  if x >= renderWidth || y >= renderHeight then frame
  else { frame with pixels := frame.pixels.set! (y * renderWidth + x) (packedColor color) }

def drawOverlayRect (frame : Framebuffer) (left top width height : Nat)
    (color : Color) : Framebuffer := Id.run do
  let mut output := frame
  for y in [top:min renderHeight (top + height)] do
    for x in [left:min renderWidth (left + width)] do
      output := overlayPixel output x y color
  return output

def victory (state : GameState) : Bool :=
  state.enemies.all fun enemy => enemy.health == 0 || !enemy.countsForExit

def mapX (x : Float) : Nat :=
  clampedNat (10.0 + (x + 8.0) / 16.0 * 108.0) (renderWidth - 1)

def mapY (z : Float) : Nat :=
  clampedNat (4.0 + (8.0 - z) / 16.0 * 54.0) (renderHeight - 12)

def drawMapLine (frame : Framebuffer) (ax ay bxPos byPos : Nat) (color : Color) : Framebuffer := Id.run do
  let dx := if ax > bxPos then ax - bxPos else bxPos - ax
  let dy := if ay > byPos then ay - byPos else byPos - ay
  let steps := max 1 (max dx dy)
  let mut output := frame
  for step in [0:steps + 1] do
    let t := Float.ofNat step / Float.ofNat steps
    let x := clampedNat (Float.ofNat ax + (Float.ofNat bxPos - Float.ofNat ax) * t) (renderWidth - 1)
    let y := clampedNat (Float.ofNat ay + (Float.ofNat byPos - Float.ofNat ay) * t) (renderHeight - 1)
    output := overlayPixel output x y color
  return output

def drawMapBox (frame : Framebuffer) (minX minZ maxX maxZ : Float)
    (color : Color) : Framebuffer :=
  let left := mapX minX
  let right := mapX maxX
  let top := mapY maxZ
  let bottom := mapY minZ
  let frame := drawMapLine frame left top right top color
  let frame := drawMapLine frame right top right bottom color
  let frame := drawMapLine frame right bottom left bottom color
  drawMapLine frame left bottom left top color

def drawAutomap (state : GameState) (frame : Framebuffer) : Framebuffer := Id.run do
  let wall : Color := ⟨185, 68, 55⟩
  let metal : Color := ⟨96, 126, 148⟩
  let mut output := drawOverlayRect frame 2 2 (renderWidth - 4) (renderHeight - 12) ⟨9, 11, 16⟩
  output := drawMapBox output (-7.7) (-7.7) 7.7 7.7 wall
  output := drawMapBox output (-3.8) (-1.0) (-2.2) 1.0 metal
  output := drawMapBox output 2.0 1.8 3.8 3.2 wall
  if state.cacheFound then
    output := drawMapBox output 2.25 2.05 3.55 2.95 metal
    let cacheColor : Color := if state.cacheDoorOpen >= 0.86 then ⟨55, 235, 108⟩ else ⟨250, 190, 55⟩
    output := drawMapLine output (mapX 2.55) (mapY 1.94) (mapX 3.25) (mapY 1.94) cacheColor
  output := drawMapBox output (-0.8) 4.2 0.8 5.4 metal
  -- Bulkhead segments and live door aperture.
  output := drawMapLine output (mapX (-7.7)) (mapY 0.62) (mapX (-1.28)) (mapY 0.62) metal
  output := drawMapLine output (mapX 1.28) (mapY 0.62) (mapX 7.7) (mapY 0.62) metal
  let doorColor : Color := if state.doorOpen >= 0.86 then ⟨58, 210, 102⟩
    else if state.hasRedKey then ⟨238, 146, 38⟩ else ⟨238, 48, 45⟩
  output := drawMapLine output (mapX (-1.26)) (mapY 0.62) (mapX 1.26) (mapY 0.62) doorColor
  -- Exit and remaining supplies.
  let exitColor : Color := if victory state then ⟨55, 245, 105⟩ else ⟨225, 45, 35⟩
  output := drawMapBox output (-0.78) 6.42 0.78 7.18 exitColor
  if state.secretFound then
    output := drawOverlayRect output (mapX (-7.4)) (mapY (-4.36) - 1) 3 3 ⟨250, 205, 70⟩
  for pickup in state.pickups do
    let hiddenCacheItem := !state.cacheFound && pickup.position.x > 2.2 &&
      pickup.position.x < 3.6 && pickup.position.z > 2.0 && pickup.position.z < 3.0
    if pickup.active && !hiddenCacheItem then
      let color : Color := if pickup.kind == 0 then ⟨55, 135, 255⟩
        else if pickup.kind == 1 then ⟨238, 180, 52⟩
        else if pickup.kind == 2 then ⟨210, 215, 220⟩ else ⟨250, 45, 52⟩
      output := drawOverlayRect output (mapX pickup.position.x - 1) (mapY pickup.position.z - 1) 3 3 color
  for barrel in state.barrels do
    let color : Color := if barrel.health > 0 then ⟨58, 175, 82⟩
      else if barrel.blastTime > 0.0 then ⟨255, 105, 28⟩ else ⟨64, 49, 40⟩
    output := drawOverlayRect output (mapX barrel.position.x - 1)
      (mapY barrel.position.z - 1) 3 3 color
  -- Alerted monsters are visible as red contacts; corpses remain dark marks.
  for enemy in state.enemies do
    if enemy.health == 0 then
      output := drawOverlayRect output (mapX enemy.position.x) (mapY enemy.position.z) 2 2 ⟨75, 25, 23⟩
    else if enemy.alerted then
      if enemy.kind == 3 then
        output := drawOverlayRect output (mapX enemy.position.x - 2) (mapY enemy.position.z - 2) 5 5 ⟨205, 48, 240⟩
      else
        output := drawOverlayRect output (mapX enemy.position.x - 1) (mapY enemy.position.z - 1) 3 3 ⟨245, 45, 35⟩
  let px := mapX state.camera.position.x
  let py := mapY state.camera.position.z
  output := drawOverlayRect output (px - 2) (py - 2) 5 5 ⟨245, 235, 90⟩
  let lookX := state.camera.position.x + state.camera.yaw.sin * 1.35
  let lookZ := state.camera.position.z + state.camera.yaw.cos * 1.35
  output := drawMapLine output px py (mapX lookX) (mapY lookZ) ⟨255, 250, 170⟩
  return output

def drawAutomapTwo (state : GameState) (frame : Framebuffer) : Framebuffer := Id.run do
  let wall : Color := ⟨38, 170, 162⟩
  let metal : Color := ⟨103, 116, 142⟩
  let mut output := drawOverlayRect frame 2 2 (renderWidth - 4) (renderHeight - 12) ⟨7, 12, 18⟩
  output := drawMapBox output (-7.7) (-7.7) 7.7 7.7 wall
  output := drawMapBox output (-7.7) (-2.75) 2.0 (-2.20) metal
  output := drawMapBox output (-2.0) 0.68 7.7 1.23 metal
  output := drawMapBox output (-7.7) 4.0 2.0 4.55 metal
  let exitColor : Color := if victory state then ⟨55, 245, 105⟩ else ⟨220, 58, 238⟩
  output := drawMapBox output 5.57 6.07 7.13 6.83 exitColor
  for pickup in state.pickups do
    if pickup.active then
      let color : Color := if pickup.kind == 0 then ⟨55, 135, 255⟩ else ⟨238, 180, 52⟩
      output := drawOverlayRect output (mapX pickup.position.x - 1) (mapY pickup.position.z - 1) 3 3 color
  for barrel in state.barrels do
    let color : Color := if barrel.health > 0 then ⟨58, 175, 82⟩
      else if barrel.blastTime > 0.0 then ⟨255, 105, 28⟩ else ⟨64, 49, 40⟩
    output := drawOverlayRect output (mapX barrel.position.x - 1)
      (mapY barrel.position.z - 1) 3 3 color
  for enemy in state.enemies do
    if enemy.health == 0 then
      output := drawOverlayRect output (mapX enemy.position.x) (mapY enemy.position.z) 2 2 ⟨75, 25, 23⟩
    else if enemy.alerted then
      if enemy.kind == 3 then
        output := drawOverlayRect output (mapX enemy.position.x - 2) (mapY enemy.position.z - 2) 5 5 ⟨205, 48, 240⟩
      else
        output := drawOverlayRect output (mapX enemy.position.x - 1) (mapY enemy.position.z - 1) 3 3 ⟨245, 45, 35⟩
  let px := mapX state.camera.position.x
  let py := mapY state.camera.position.z
  output := drawOverlayRect output (px - 2) (py - 2) 5 5 ⟨245, 235, 90⟩
  let lookX := state.camera.position.x + state.camera.yaw.sin * 1.35
  let lookZ := state.camera.position.z + state.camera.yaw.cos * 1.35
  output := drawMapLine output px py (mapX lookX) (mapY lookZ) ⟨255, 250, 170⟩
  return output

def drawShotgun (state : GameState) (frame : Framebuffer) (centerX : Nat) : Framebuffer := Id.run do
  let cooling := state.weaponCooldown
  let smoking := state.muzzleFlash == 0 && cooling > 0.56
  let breachOpen := cooling > 0.18 && cooling < 0.52
  let inserting := cooling > 0.18 && cooling < 0.34
  let recoil := if state.muzzleFlash > 0 then 4 else if cooling > 0.62 then 2 else 0
  let reloadDrop := if breachOpen then 5 else 0
  let barrelSpread := if breachOpen then 3 else 0
  let stepBob := if state.bobStrength > 0.2 && (state.bobPhase * 2.0).sin > 0.0 then 1 else 0
  let gunTop := renderHeight - 25 + recoil + reloadDrop + stepBob
  let mut output := frame
  -- A brief smoke curl bridges the flash into the mechanical reload.
  if smoking then
    output := drawRect output (centerX - 5) (gunTop - 13) 2 2 ⟨175, 180, 176⟩
    output := drawRect output (centerX - 3) (gunTop - 16) 2 3 ⟨122, 130, 131⟩
    output := drawRect output (centerX - 1) (gunTop - 18) 3 2 ⟨78, 86, 91⟩
    output := drawRect output (centerX + 5) (gunTop - 12) 2 2 ⟨158, 164, 162⟩
    output := drawRect output (centerX + 7) (gunTop - 15) 2 3 ⟨91, 99, 102⟩
  output := drawRect output (centerX - 7 - barrelSpread) (gunTop - 5) 6 15 ⟨58, 63, 72⟩
  output := drawRect output (centerX + 2 + barrelSpread) (gunTop - 5) 6 15 ⟨58, 63, 72⟩
  output := drawRect output (centerX - 6 - barrelSpread) (gunTop - 4) 4 14 ⟨166, 174, 178⟩
  output := drawRect output (centerX + 3 + barrelSpread) (gunTop - 4) 4 14 ⟨166, 174, 178⟩
  output := drawRect output (centerX - 5 - barrelSpread) (gunTop - 3) 2 12 ⟨54, 59, 67⟩
  output := drawRect output (centerX + 4 + barrelSpread) (gunTop - 3) 2 12 ⟨54, 59, 67⟩
  output := drawRect output centerX (gunTop - 7) 1 5 ⟨190, 196, 194⟩
  output := drawRect output (centerX - 15) (gunTop + 8) 31 11 ⟨66, 71, 79⟩
  output := drawRect output (centerX - 13) (gunTop + 9) 27 7 ⟨148, 88, 44⟩
  output := drawRect output (centerX - 11) (gunTop + 10) 23 2 ⟨205, 137, 70⟩
  output := drawRect output (centerX - 9) (gunTop + 16) 19 8 ⟨70, 39, 25⟩
  output := drawRect output (centerX - 14) (gunTop + 8) 3 9 ⟨164, 170, 166⟩
  output := drawRect output (centerX + 12) (gunTop + 8) 3 9 ⟨164, 170, 166⟩
  if breachOpen then
    -- Brass breech faces and two chunky red shells sell the super-shotgun cycle.
    output := drawRect output (centerX - 10) (gunTop + 3) 8 5 ⟨115, 77, 32⟩
    output := drawRect output (centerX + 3) (gunTop + 3) 8 5 ⟨115, 77, 32⟩
    output := drawRect output (centerX - 8) (gunTop + 4) 4 3 ⟨235, 184, 64⟩
    output := drawRect output (centerX + 5) (gunTop + 4) 4 3 ⟨235, 184, 64⟩
  if inserting then
    output := drawRect output (centerX - 9) (gunTop - 3) 5 8 ⟨178, 30, 35⟩
    output := drawRect output (centerX + 5) (gunTop - 3) 5 8 ⟨178, 30, 35⟩
    output := drawRect output (centerX - 8) (gunTop - 3) 3 2 ⟨248, 196, 70⟩
    output := drawRect output (centerX + 6) (gunTop - 3) 3 2 ⟨248, 196, 70⟩
  if state.muzzleFlash > 0 then
    output := drawRect output (centerX - 12) (gunTop - 13) 25 5 ⟨245, 92, 24⟩
    output := drawRect output (centerX - 8) (gunTop - 18) 17 14 ⟨255, 172, 38⟩
    output := drawRect output (centerX - 3) (gunTop - 22) 7 20 ⟨255, 239, 135⟩
  return output

def drawChaingun (state : GameState) (frame : Framebuffer) (centerX : Nat) : Framebuffer := Id.run do
  let recoil := if state.muzzleFlash > 0 then 2 else 0
  let stepBob := if state.bobStrength > 0.2 && (state.bobPhase * 2.0).sin > 0.0 then 1 else 0
  let gunTop := renderHeight - 30 + recoil + stepBob
  let spin := state.bullets % 3
  let mut output := frame
  -- Three bright barrel jackets with alternating dark bores imply rotation.
  output := drawRect output (centerX - 10) (gunTop - 3 + spin) 5 18 ⟨122, 130, 136⟩
  output := drawRect output (centerX - 2) (gunTop - 5 + ((spin + 1) % 3)) 5 20 ⟨166, 174, 178⟩
  output := drawRect output (centerX + 6) (gunTop - 3 + ((spin + 2) % 3)) 5 18 ⟨122, 130, 136⟩
  output := drawRect output (centerX - 9) gunTop 3 14 ⟨35, 39, 46⟩
  output := drawRect output (centerX - 1) (gunTop - 2) 3 16 ⟨35, 39, 46⟩
  output := drawRect output (centerX + 7) gunTop 3 14 ⟨35, 39, 46⟩
  -- Rotary housing, feed block, grips, and the marine's hands.
  output := drawRect output (centerX - 17) (gunTop + 13) 35 12 ⟨52, 58, 67⟩
  output := drawRect output (centerX - 13) (gunTop + 15) 27 6 ⟨91, 99, 104⟩
  output := drawRect output (centerX - 5) (gunTop + 11) 11 12 ⟨31, 34, 40⟩
  output := drawRect output (centerX - 20) (gunTop + 19) 7 10 ⟨139, 82, 48⟩
  output := drawRect output (centerX + 14) (gunTop + 19) 7 10 ⟨139, 82, 48⟩
  output := drawRect output (centerX - 18) (gunTop + 17) 5 4 ⟨204, 137, 84⟩
  output := drawRect output (centerX + 14) (gunTop + 17) 5 4 ⟨204, 137, 84⟩
  if state.muzzleFlash > 0 then
    let flashX := centerX - 7 + spin * 7
    output := drawRect output (flashX - 3) (gunTop - 12) 9 6 ⟨255, 112, 20⟩
    output := drawRect output flashX (gunTop - 16) 3 12 ⟨255, 232, 105⟩
  return output

def secretGlyphs : Array (Array Nat) := #[
  #[7, 4, 7, 1, 7], -- S
  #[7, 4, 6, 4, 7], -- E
  #[7, 4, 4, 4, 7], -- C
  #[6, 5, 6, 5, 5], -- R
  #[7, 4, 6, 4, 7], -- E
  #[7, 2, 2, 2, 2]  -- T
]

def drawSecretWord (frame : Framebuffer) (left top : Nat) (color : Color) : Framebuffer := Id.run do
  let mut output := frame
  for glyphIndex in [0:secretGlyphs.size] do
    let rows := secretGlyphs[glyphIndex]!
    for row in [0:rows.size] do
      for column in [0:3] do
        let divisor := 2 ^ (2 - column)
        if (rows[row]! / divisor) % 2 == 1 then
          output := drawOverlayRect output (left + glyphIndex * 8 + column * 2)
            (top + row * 2) 2 2 color
  return output

def glyphRows (character : Char) : Array Nat :=
  match character with
  | 'A' => #[2, 5, 7, 5, 5] | 'B' => #[6, 5, 6, 5, 6]
  | 'C' => #[7, 4, 4, 4, 7] | 'D' => #[6, 5, 5, 5, 6]
  | 'E' => #[7, 4, 6, 4, 7] | 'F' => #[7, 4, 6, 4, 4]
  | 'G' => #[7, 4, 5, 5, 7] | 'H' => #[5, 5, 7, 5, 5]
  | 'I' => #[7, 2, 2, 2, 7] | 'J' => #[1, 1, 1, 5, 7]
  | 'K' => #[5, 5, 6, 5, 5] | 'L' => #[4, 4, 4, 4, 7]
  | 'M' => #[5, 7, 7, 5, 5] | 'N' => #[5, 7, 7, 7, 5]
  | 'O' => #[7, 5, 5, 5, 7] | 'P' => #[6, 5, 6, 4, 4]
  | 'Q' => #[7, 5, 5, 7, 1] | 'R' => #[6, 5, 6, 5, 5]
  | 'S' => #[7, 4, 7, 1, 7] | 'T' => #[7, 2, 2, 2, 2]
  | 'U' => #[5, 5, 5, 5, 7] | 'V' => #[5, 5, 5, 5, 2]
  | 'W' => #[5, 5, 7, 7, 5] | 'X' => #[5, 5, 2, 5, 5]
  | 'Y' => #[5, 5, 2, 2, 2] | 'Z' => #[7, 1, 2, 4, 7]
  | '0' => #[7, 5, 5, 5, 7] | '1' => #[2, 6, 2, 2, 7]
  | '2' => #[7, 1, 7, 4, 7] | '3' => #[7, 1, 7, 1, 7]
  | '4' => #[5, 5, 7, 1, 1] | '5' => #[7, 4, 7, 1, 7]
  | '6' => #[7, 4, 7, 5, 7] | '7' => #[7, 1, 2, 2, 2]
  | '8' => #[7, 5, 7, 5, 7] | '9' => #[7, 5, 7, 1, 7]
  | ':' => #[0, 2, 0, 2, 0] | '-' => #[0, 0, 7, 0, 0]
  | '/' => #[1, 1, 2, 4, 4] | '%' => #[5, 1, 2, 4, 5]
  | _ => #[0, 0, 0, 0, 0]

def textWidth (value : String) (scale : Nat) : Nat :=
  if value.length == 0 then 0 else value.length * 4 * scale - scale

def drawText (frame : Framebuffer) (value : String) (left top scale : Nat)
    (color : Color) : Framebuffer := Id.run do
  let mut output := frame
  for (character, index) in value.toList.zipIdx do
    let rows := glyphRows character
    for row in [0:5] do
      for column in [0:3] do
        let divisor := 2 ^ (2 - column)
        if (rows[row]! / divisor) % 2 == 1 then
          output := drawOverlayRect output (left + index * 4 * scale + column * scale)
            (top + row * scale) scale scale color
  return output

def drawTextCentered (frame : Framebuffer) (value : String) (top scale : Nat)
    (color : Color) : Framebuffer :=
  let width := textWidth value scale
  drawText frame value ((renderWidth - min renderWidth width) / 2) top scale color

def difficultyName (difficulty : Nat) : String :=
  if difficulty == 0 then "EASY" else if difficulty == 2 then "NIGHTMARE" else "HARD"

def drawTitle (state : GameState) (frame : Framebuffer) : Framebuffer := Id.run do
  let mut output := drawOverlayRect frame 0 0 renderWidth renderHeight ⟨7, 8, 12⟩
  -- Deep red industrial brick backdrop.
  for row in [0:9] do
    for column in [0:9] do
      let offset := if row % 2 == 0 then 0 else 8
      let left := column * 16 + offset
      output := drawOverlayRect output left (row * 8) 14 6
        (if (row + column) % 3 == 0 then ⟨55, 20, 25⟩ else ⟨41, 17, 22⟩)
  output := drawOverlayRect output 5 1 (renderWidth - 10) 2 ⟨170, 35, 38⟩
  output := drawTextCentered output "LEAN 64" 5 3 ⟨55, 10, 14⟩
  output := drawTextCentered output "LEAN 64" 4 3 ⟨245, 70, 44⟩
  output := drawTextCentered output "PURE LEAN 4 FPS" 21 1 ⟨195, 198, 190⟩
  let modeColor : Color := if state.difficulty == 0 then ⟨75, 210, 125⟩
    else if state.difficulty == 2 then ⟨240, 52, 72⟩ else ⟨250, 170, 55⟩
  output := drawTextCentered output s!"MODE {difficultyName state.difficulty}" 27 1 modeColor
  output := drawTextCentered output "PRESS ENTER" 34 2 ⟨250, 205, 70⟩
  output := drawShotgun { state with muzzleFlash := 0 } output (renderWidth / 2)
  return output

def drawPause (frame : Framebuffer) : Framebuffer := Id.run do
  let mut output := drawOverlayRect frame 19 20 91 31 ⟨10, 11, 16⟩
  output := drawOverlayRect output 21 22 87 2 ⟨175, 38, 45⟩
  output := drawOverlayRect output 21 47 87 2 ⟨175, 38, 45⟩
  output := drawTextCentered output "PAUSED" 27 2 ⟨245, 72, 62⟩
  output := drawTextCentered output "P TO RESUME" 41 1 ⟨215, 215, 205⟩
  return output

def drawIntermission (state : GameState) (frame : Framebuffer) : Framebuffer := Id.run do
  let mut output := drawOverlayRect frame 0 0 renderWidth renderHeight ⟨8, 10, 14⟩
  for row in [0:8] do
    for column in [0:8] do
      let left := column * 18 + (if row % 2 == 0 then 0 else 9)
      output := drawOverlayRect output left (row * 9) 16 7
        (if (row + column) % 2 == 0 then ⟨21, 28, 28⟩ else ⟨17, 22, 25⟩)
  output := drawOverlayRect output 4 3 (renderWidth - 8) 14 ⟨10, 36, 27⟩
  output := drawOverlayRect output 5 4 (renderWidth - 10) 2 ⟨52, 205, 105⟩
  let heading := if state.level == 0 then "MAP 1 CLEAR" else "CAMPAIGN CLEAR"
  output := drawTextCentered output heading 7 2 ⟨76, 240, 132⟩
  output := drawOverlayRect output 7 19 54 32 ⟨11, 13, 18⟩
  output := drawOverlayRect output 67 19 54 32 ⟨11, 13, 18⟩
  let totalSeconds := floatToNat state.playTime
  let minutes := totalSeconds / 60
  let seconds := totalSeconds % 60
  let secondText := if seconds < 10 then s!"0{seconds}" else s!"{seconds}"
  let secretCount := (if state.secretFound then 1 else 0) + (if state.cacheFound then 1 else 0)
  let secretTotal := if state.level == 0 then 2 else 0
  let accuracy := if state.shotsFired == 0 then 0 else state.shotsHit * 100 / state.shotsFired
  output := drawText output s!"TIME {minutes}:{secondText}" 11 23 1 ⟨210, 215, 205⟩
  output := drawText output s!"KILLS {state.killsMade}/{state.enemies.size}" 11 32 1 ⟨235, 72, 65⟩
  output := drawText output s!"SECRETS {secretCount}/{secretTotal}" 11 41 1 ⟨250, 195, 58⟩
  output := drawText output s!"SHOTS {state.shotsFired}" 71 23 1 ⟨210, 215, 205⟩
  output := drawText output s!"HITS {state.shotsHit}" 71 32 1 ⟨210, 215, 205⟩
  output := drawText output s!"ACC {accuracy}%" 71 41 1 ⟨165, 190, 235⟩
  output := drawTextCentered output s!"MODE {difficultyName state.difficulty}" 48 1 ⟨175, 180, 185⟩
  output := drawTextCentered output s!"SCORE {state.score}" 54 2 ⟨250, 195, 58⟩
  let prompt := if state.level == 0 then "ENTER NEXT MAP" else "R REPLAY MAP"
  output := drawTextCentered output prompt 66 1 ⟨220, 225, 215⟩
  return output

def drawHud (state : GameState) (frame : Framebuffer) : Framebuffer := Id.run do
  let centerX := renderWidth / 2
  let centerY := renderHeight / 2
  let mut output := frame
  let bossHealth := state.enemies.foldl (init := 0) fun health enemy =>
    if enemy.kind == 3 && enemy.alerted then max health enemy.health else health
  if bossHealth > 0 then
    output := drawRect output (centerX - 26) 3 53 7 ⟨17, 13, 22⟩
    output := drawRect output (centerX - 25) 4 (min 50 (bossHealth * 50 / 8)) 5 ⟨178, 38, 205⟩
    output := drawRect output (centerX - 24) 5 (min 48 (bossHealth * 48 / 8)) 2 ⟨250, 85, 235⟩
  -- Crosshair.
  let crosshair : Color := if state.hitMarker > 0 then ⟨255, 45, 34⟩ else ⟨220, 230, 235⟩
  output := drawRect output (centerX - 7) centerY 5 1 crosshair
  output := drawRect output (centerX + 3) centerY 5 1 crosshair
  output := drawRect output centerX (centerY - 7) 1 5 crosshair
  output := drawRect output centerX (centerY + 3) 1 5 crosshair
  -- Health and ammo bars.
  output := drawRect output 4 (renderHeight - 8) 42 5 ⟨24, 25, 31⟩
  output := drawRect output 5 (renderHeight - 7) (state.health * 40 / 100) 3 ⟨205, 42, 45⟩
  output := drawRect output (renderWidth - 46) (renderHeight - 8) 42 5 ⟨24, 25, 31⟩
  let ammoWidth := if state.weapon == 0 then min 40 (state.ammo * 2 / 3)
    else min 40 (state.bullets / 5)
  let ammoColor : Color := if state.weapon == 0 then ⟨232, 171, 45⟩ else ⟨235, 93, 36⟩
  output := drawRect output (renderWidth - 45) (renderHeight - 7) ammoWidth 3 ammoColor
  output := drawText output s!"HP {state.health}" 4 (renderHeight - 14) 1 ⟨235, 215, 205⟩
  let ammoValue := if state.weapon == 0 then state.ammo else state.bullets
  let ammoLabel := s!"AMMO {ammoValue}"
  output := drawText output ammoLabel (renderWidth - textWidth ammoLabel 1 - 4)
    (renderHeight - 14) 1 ⟨235, 215, 205⟩
  let scoreLabel := s!"SCORE {state.score}"
  output := drawText output scoreLabel (renderWidth - textWidth scoreLabel 1 - 4) 12 1 ⟨170, 176, 180⟩
  -- Persistent red-key inventory light.
  if state.hasRedKey || state.keyFlash > 0 then
    output := drawRect output 4 4 12 8 ⟨18, 20, 25⟩
    output := drawRect output 5 5 10 6 (if state.hasRedKey then ⟨225, 38, 48⟩ else ⟨55, 28, 32⟩)
  if state.hasRedKey then
    output := drawRect output 7 7 6 2 ⟨250, 192, 58⟩
  let sway := state.bobPhase.sin
  let weaponCenter := if state.bobStrength <= 0.2 then centerX
    else if sway > 0.25 then centerX + 1 else if sway < -0.25 then centerX - 1 else centerX
  output := if state.weapon == 0 then drawShotgun state output weaponCenter
    else drawChaingun state output weaponCenter
  -- Damage vignette and end-state cards.
  if state.damageFlash > 0 then
    output := drawRect output 0 0 renderWidth 3 ⟨170, 18, 24⟩
    output := drawRect output 0 (renderHeight - 3) renderWidth 3 ⟨170, 18, 24⟩
    output := drawRect output 0 0 3 renderHeight ⟨170, 18, 24⟩
    output := drawRect output (renderWidth - 3) 0 3 renderHeight ⟨170, 18, 24⟩
  if state.health == 0 then
    output := drawRect output (centerX - 35) (centerY - 13) 71 27 ⟨76, 10, 16⟩
    output := drawTextCentered output "YOU DIED" (centerY - 8) 2 ⟨245, 55, 55⟩
    output := drawTextCentered output "R TO RESTART" (centerY + 5) 1 ⟨235, 205, 190⟩
  else if state.levelComplete then
    output := drawRect output (centerX - 40) (centerY - 13) 81 27 ⟨13, 65, 42⟩
    output := drawTextCentered output "LEVEL CLEAR" (centerY - 8) 2 ⟨74, 235, 132⟩
    output := drawTextCentered output "R TO RESTART" (centerY + 5) 1 ⟨235, 225, 205⟩
  else if victory state then
    output := drawRect output (centerX - 21) 3 43 8 ⟨12, 48, 30⟩
    output := drawTextCentered output "EXIT OPEN" 5 1 ⟨65, 235, 112⟩
  if state.secretFlash > 0 then
    let glow : Color := if state.secretFlash % 10 < 5 then ⟨255, 220, 78⟩ else ⟨235, 150, 35⟩
    output := drawOverlayRect output (centerX - 28) 9 57 15 ⟨26, 20, 14⟩
    output := drawOverlayRect output (centerX - 27) 10 55 1 glow
    output := drawOverlayRect output (centerX - 27) 22 55 1 glow
    output := drawSecretWord output (centerX - 23) 11 glow
  if state.keyFlash > 0 && state.secretFlash == 0 then
    let keyColor : Color := if state.hasRedKey then ⟨250, 195, 58⟩ else ⟨250, 42, 48⟩
    let keyMessage := if state.hasRedKey then "RED KEY" else "KEY REQUIRED"
    output := drawOverlayRect output (centerX - 29) 4 59 9 ⟨24, 16, 18⟩
    output := drawTextCentered output keyMessage 6 1 keyColor
  if state.playTime < 2.6 && state.secretFlash == 0 && state.keyFlash == 0 then
    let mapName := if state.level == 0 then "MAP 1: THE FOUNDRY" else "MAP 2: BLACK CIRCUIT"
    let panelWidth := textWidth mapName 1 + 10
    output := drawOverlayRect output ((renderWidth - panelWidth) / 2) 17 panelWidth 11 ⟨8, 10, 14⟩
    output := drawOverlayRect output ((renderWidth - panelWidth) / 2) 17 panelWidth 1
      (if state.level == 0 then ⟨195, 48, 42⟩ else ⟨38, 190, 181⟩)
    output := drawTextCentered output mapName 20 1
      (if state.level == 0 then ⟨235, 184, 78⟩ else ⟨130, 238, 226⟩)
  return output

def paletteFlash (state : GameState) (frame : Framebuffer) : Framebuffer :=
  if state.damageFlash == 0 && state.pickupFlash == 0 then frame
  else
    let tint (pixel : UInt32) : UInt32 :=
      let value := pixel.toNat
      let red := (value / 65536) % 256
      let green := (value / 256) % 256
      let blue := value % 256
      let red := if state.damageFlash > 0 then min 255 (red + state.damageFlash * 22) else red
      let green := if state.damageFlash > 0 then green * (100 - state.damageFlash * 7) / 100 else green
      let blue := if state.damageFlash > 0 then blue * (100 - state.damageFlash * 10) / 100 else blue
      let red := if state.pickupFlash > 0 then min 255 (red + state.pickupFlash * 9) else red
      let green := if state.pickupFlash > 0 then min 255 (green + state.pickupFlash * 12) else green
      let blue := if state.pickupFlash > 0 then min 255 (blue + state.pickupFlash * 5) else blue
      packedColor ⟨red, green, blue⟩
    { frame with pixels := frame.pixels.map tint }

def render (state : GameState) : Array UInt32 :=
  if !state.started then (drawTitle state newFramebuffer).pixels
  else if state.levelComplete then (drawIntermission state newFramebuffer).pixels
  else
    let geometry := (sceneMesh state).map (illuminateTriangle state.camera state.muzzleFlash)
    let sideSway := state.bobStrength * state.bobPhase.sin * 0.035
    let verticalBob := state.bobStrength * (state.bobPhase * 2.0).sin * 0.028
    let renderCamera := { state.camera with
      position := state.camera.position.add
        ⟨state.camera.yaw.cos * sideSway, verticalBob, -state.camera.yaw.sin * sideSway⟩
      pitch := state.camera.pitch - state.recoilKick * 0.045 }
    let frame := geometry.foldl (renderTriangle renderCamera) newFramebuffer
    let frame := drawHud state frame
    let frame := if state.mapOpen then
      if state.level == 0 then drawAutomap state frame else drawAutomapTwo state frame
      else frame
    let frame := paletteFlash state frame
    (if state.paused then drawPause frame else frame).pixels

def renderCameraFor (state : GameState) : Camera :=
  let sideSway := state.bobStrength * state.bobPhase.sin * 0.035
  let verticalBob := state.bobStrength * (state.bobPhase * 2.0).sin * 0.028
  { state.camera with
    position := state.camera.position.add
      ⟨state.camera.yaw.cos * sideSway, verticalBob, -state.camera.yaw.sin * sideSway⟩
    pitch := state.camera.pitch - state.recoilKick * 0.045 }

def appendTriangleData (data : Array UInt64) (triangle : Triangle) : Array UInt64 :=
  data.push triangle.a.x.toBits |>.push triangle.a.y.toBits |>.push triangle.a.z.toBits
    |>.push triangle.b.x.toBits |>.push triangle.b.y.toBits |>.push triangle.b.z.toBits
    |>.push triangle.c.x.toBits |>.push triangle.c.y.toBits |>.push triangle.c.z.toBits
    |>.push (UInt64.ofNat (packedColor triangle.color).toNat)
    |>.push (UInt64.ofNat triangle.material)

def gpuSceneData (state : GameState) : Array UInt64 :=
  if !state.started || state.levelComplete then #[]
  else
    (sceneMesh state).foldl (fun data triangle =>
      appendTriangleData data (illuminateTriangle state.camera state.muzzleFlash triangle)) #[]

def gpuOverlay (state : GameState) : Array UInt32 :=
  if !state.started then (drawTitle state newFramebuffer).pixels
  else if state.levelComplete then (drawIntermission state newFramebuffer).pixels
  else
    let frame := drawHud state transparentFramebuffer
    let frame := if state.mapOpen then
      if state.level == 0 then drawAutomap state frame else drawAutomapTwo state frame
      else frame
    (if state.paused then drawPause frame else frame).pixels

def presentGpuState (state : GameState) : IO Bool :=
  let camera := renderCameraFor state
  presentGpu (gpuSceneData state) (gpuOverlay state)
    (UInt32.ofNat renderWidth) (UInt32.ofNat renderHeight)
    camera.position.x.toBits camera.position.y.toBits camera.position.z.toBits
    camera.yaw.toBits camera.pitch.toBits

def pollInput : IO Input := do
  let mouse ← mouseDelta
  let packed := mouse.toNat
  return {
    forward := ← keyDown 0x57
    backward := ← keyDown 0x53
    left := ← keyDown 0x41
    right := ← keyDown 0x44
    lookLeft := ← keyDown 0x25
    lookRight := ← keyDown 0x27
    lookUp := ← keyDown 0x26
    lookDown := ← keyDown 0x28
    mouseX := Float.ofNat (packed % 65536) - 32768.0
    mouseY := Float.ofNat ((packed / 65536) % 65536) - 32768.0
    sprint := ← keyDown 0x10
    shoot := ← keyDown 0x20
    use := ← keyDown 0x45
    weapon1 := ← keyDown 0x31
    weapon2 := ← keyDown 0x32
    weapon3 := ← keyDown 0x33
    map := (← keyDown 0x09) || (← keyDown 0x4D)
    confirm := ← keyDown 0x0D
    pause := ← keyDown 0x50
    restart := ← keyDown 0x52
    quit := (← keyDown 0x1B) || (← keyDown 0x51)
  }

def clampFloat (value low high : Float) : Float := max low (min high value)

def blocked (level : Nat) (x z : Float) : Bool :=
  x < -7.35 || x > 7.35 || z < -7.35 || z > 7.35 ||
  if level == 0 then
    (x > -4.15 && x < -1.85 && z > -1.35 && z < 1.35) ||
    (x > -1.15 && x < 1.15 && z > 3.85 && z < 5.75) ||
    (z > 0.18 && z < 1.05 && (x < -0.98 || x > 0.98))
  else
    (z > -3.05 && z < -1.90 && x < 2.30) ||
    (z > 0.38 && z < 1.53 && x > -2.30) ||
    (z > 3.70 && z < 4.85 && x < 2.30) ||
    (x > 5.10 && x < 6.15 && z > 5.10 && z < 6.15) ||
    (x > 6.65 && x < 7.35 && z > 5.10 && z < 6.15)

def cacheBlocked (cacheOpen x z : Float) : Bool :=
  x > 2.0 && x < 3.8 && z > 1.8 && z < 3.2 &&
    (x < 2.25 || x > 3.55 || z > 2.95 ||
      (z < 2.05 && (x < 2.55 || x > 3.25 || cacheOpen < 0.86)))

def blockedAt (level : Nat) (doorOpen cacheOpen x z : Float) : Bool :=
  blocked level x z ||
    (level == 0 && cacheBlocked cacheOpen x z) ||
    (level == 0 && doorOpen < 0.86 && x > -1.28 && x < 1.28 && z > 0.18 && z < 1.05)

def moveCamera (camera : Camera) (level : Nat) (doorOpen cacheOpen dx dz : Float) : Camera :=
  let nextX := camera.position.x + dx
  let nextZ := camera.position.z + dz
  let afterX := if blockedAt level doorOpen cacheOpen nextX camera.position.z then camera.position else
    { camera.position with x := nextX }
  let afterZ := if blockedAt level doorOpen cacheOpen afterX.x nextZ then afterX else { afterX with z := nextZ }
  { camera with position := afterZ }

def clearShot (level : Nat) (doorOpen cacheOpen : Float) (origin target : Vec3) : Bool :=
  let direction := (target.sub origin).normalize
  let distance := (target.sub origin).length
  let rec check (position : Vec3) (travelled : Float) (fuel : Nat) : Bool :=
    match fuel with
    | 0 => true
    | fuel + 1 =>
      if travelled >= distance then true
      else
        let next := position.add (direction.scale 0.22)
        if blockedAt level doorOpen cacheOpen next.x next.z then false
        else check next (travelled + 0.22) fuel
  check origin 0.0 80

def raycastImpact (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) : Option Vec3 :=
  let direction : Vec3 := ⟨camera.yaw.sin * camera.pitch.cos,
    -camera.pitch.sin, camera.yaw.cos * camera.pitch.cos⟩
  let rec trace (position : Vec3) (fuel : Nat) : Option Vec3 :=
    match fuel with
    | 0 => none
    | fuel + 1 =>
      let next := position.add (direction.scale 0.16)
      if next.y <= 0.04 then some { next with y := 0.05 }
      else if next.y >= 3.46 then some { next with y := 3.44 }
      else if blockedAt level doorOpen cacheOpen next.x next.z then
        -- Collision volumes include player clearance; advance the visual mark
        -- toward the actual rendered surface so it does not appear to float.
        some (next.add (direction.scale 0.24))
      else trace next fuel
  trace camera.position 120

def shootEnemies (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) (damage : Nat)
    (enemies : Array Enemy) : Array Enemy × Bool :=
  let targetIndex := enemies.toList.zipIdx.foldl (init := none) fun best (enemy, index) =>
    if enemy.health == 0 then best
    else
      let target := (enemy.position.add ⟨0.0, 0.8, 0.0⟩).sub camera.position
      let distance := target.length
      let horizontalDistance := (target.x * target.x + target.z * target.z).sqrt
      let alignment := if horizontalDistance <= 0.001 then 1.0 else
        (camera.yaw.sin * target.x + camera.yaw.cos * target.z) / horizontalDistance
      if distance < 16.0 && alignment > 0.996 &&
          clearShot level doorOpen cacheOpen camera.position (enemy.position.add ⟨0.0, 0.8, 0.0⟩) then
        let score := alignment - distance * 0.001
        match best with
        | none => some (index, score)
        | some (_, bestScore) => if score > bestScore then some (index, score) else best
      else best
  match targetIndex with
  | none => (enemies, false)
  | some (hitIndex, _) =>
    (enemies.toList.zipIdx.map (fun (enemy, index) =>
      if index == hitIndex then
        let nextHealth := enemy.health - damage
        { enemy with
          health := nextHealth
          alerted := true
          painTime := if nextHealth == 0 then 0.0 else 0.16
          deathTime := if nextHealth == 0 then 0.62 else enemy.deathTime
          attackWindup := 0.0 }
      else enemy
    ) |>.toArray, true)

def shootBarrels (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) (damage : Nat)
    (barrels : Array Barrel) : Array Barrel × Bool :=
  let targetIndex := barrels.toList.zipIdx.foldl (init := none) fun best (barrel, index) =>
    if barrel.health == 0 then best
    else
      let targetPoint := barrel.position.add ⟨0.0, 0.82, 0.0⟩
      let target := targetPoint.sub camera.position
      let distance := target.length
      let horizontalDistance := (target.x * target.x + target.z * target.z).sqrt
      let alignment := if horizontalDistance <= 0.001 then 1.0 else
        (camera.yaw.sin * target.x + camera.yaw.cos * target.z) / horizontalDistance
      if distance < 16.0 && alignment > 0.996 && clearShot level doorOpen cacheOpen camera.position targetPoint then
        let score := alignment - distance * 0.001
        match best with
        | none => some (index, score)
        | some (_, bestScore) => if score > bestScore then some (index, score) else best
      else best
  match targetIndex with
  | none => (barrels, false)
  | some (hitIndex, _) =>
    (barrels.toList.zipIdx.map (fun (barrel, index) =>
      if index == hitIndex then
        let health := barrel.health - damage
        { barrel with health, blastTime := if health == 0 then 0.28 else barrel.blastTime }
      else barrel
    ) |>.toArray, true)

def shotgunOffsets : Array Float := #[-0.09, -0.045, 0.0, 0.045, 0.09]

def shootShotgun (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float)
    (enemies : Array Enemy) (barrels : Array Barrel) : Array Enemy × Array Barrel × Bool := Id.run do
  let mut nextEnemies := enemies
  let mut nextBarrels := barrels
  let mut hit := false
  for offset in shotgunOffsets do
    let pelletCamera := { camera with yaw := camera.yaw + offset }
    let (pelletEnemies, enemyHit) :=
      shootEnemies pelletCamera level doorOpen cacheOpen 1 nextEnemies
    nextEnemies := pelletEnemies
    if enemyHit then hit := true
    else
      let (pelletBarrels, barrelHit) :=
        shootBarrels pelletCamera level doorOpen cacheOpen 1 nextBarrels
      nextBarrels := pelletBarrels
      if barrelHit then hit := true
  return (nextEnemies, nextBarrels, hit)

def shotgunWallImpacts (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) : Array Vec3 := Id.run do
  let mut impacts := #[]
  for offset in shotgunOffsets do
    let pelletCamera := { camera with yaw := camera.yaw + offset }
    if let some impact := raycastImpact pelletCamera level doorOpen cacheOpen then
      impacts := impacts.push impact
  return impacts

def updateEnemy (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) (heardShot : Bool) (delta : Float) (enemy : Enemy) :
    Enemy × Nat × Option Projectile :=
  if enemy.health == 0 then
    ({ enemy with deathTime := max 0.0 (enemy.deathTime - delta), phase := enemy.phase + delta * 2.0 }, 0, none)
  else
    let cooldown := max 0.0 (enemy.attackCooldown - delta)
    let painTime := max 0.0 (enemy.painTime - delta)
    let wasWinding := enemy.attackWindup > 0.0
    let attackWindup := max 0.0 (enemy.attackWindup - delta)
    let dx := camera.position.x - enemy.position.x
    let dz := camera.position.z - enemy.position.z
    let distance := (dx * dx + dz * dz).sqrt
    let phase := enemy.phase + delta * (4.5 + Float.ofNat enemy.kind)
    let seesPlayer := distance < 10.5 && clearShot level doorOpen cacheOpen
      (enemy.position.add ⟨0.0, 0.9, 0.0⟩) camera.position
    let alerted := enemy.alerted || seesPlayer || (heardShot && distance < 7.0)
    let enemy := { enemy with alerted, painTime, attackWindup }
    if enemy.painTime > 0.0 then
      ({ enemy with attackCooldown := cooldown, attackWindup := 0.0, phase }, 0, none)
    else if !alerted then
      ({ enemy with attackCooldown := cooldown, phase }, 0, none)
    else if wasWinding then
      if attackWindup <= 0.0 then
        let origin := enemy.position.add ⟨0.0, (if enemy.kind == 3 then 1.35 else 1.15), 0.0⟩
        let velocity := (camera.position.sub origin).normalize.scale
          (if enemy.kind == 3 then 3.15 else 2.45)
        let fireball : Projectile := {
          position := origin
          velocity
          life := 5.0
          damage := if enemy.kind == 3 then 18 else 12
        }
        ({ enemy with attackCooldown := cooldown, phase }, 0, some fireball)
      else ({ enemy with attackCooldown := cooldown, phase }, 0, none)
    else if distance < 0.9 then
      let damage := if cooldown <= 0.0 then (if enemy.kind == 3 then 15 else 9) else 0
      ({ enemy with attackCooldown := if damage > 0 then 0.72 else cooldown, phase }, damage, none)
    else if enemy.kind % 2 == 1 && distance < 9.0 && cooldown <= 0.0 &&
        clearShot level doorOpen cacheOpen (enemy.position.add ⟨0.0, 1.15, 0.0⟩) camera.position then
      ({ enemy with
        attackCooldown := if enemy.kind == 3 then 1.02 else 1.65
        attackWindup := if enemy.kind == 3 then 0.30 else 0.35
        phase }, 0, none)
    else if distance < 15.0 then
      let amount := min (distance - 0.75) (delta * (0.72 + Float.ofNat enemy.kind * 0.08))
      let nextX := enemy.position.x + dx / distance * amount
      let nextZ := enemy.position.z + dz / distance * amount
      let afterX := if blockedAt level doorOpen cacheOpen nextX enemy.position.z then enemy.position else
        { enemy.position with x := nextX }
      let afterZ := if blockedAt level doorOpen cacheOpen afterX.x nextZ then afterX else { afterX with z := nextZ }
      ({ enemy with position := afterZ, attackCooldown := cooldown, phase }, 0, none)
    else ({ enemy with attackCooldown := cooldown, phase }, 0, none)

def updateEnemies (camera : Camera) (level : Nat) (doorOpen cacheOpen : Float) (heardShot : Bool) (delta : Float)
    (enemies : Array Enemy) :
    Array Enemy × Nat × Array Projectile := Id.run do
  let mut moved := #[]
  let mut totalDamage := 0
  let mut spawned := #[]
  for enemy in enemies do
    let (next, damage, projectile) := updateEnemy camera level doorOpen cacheOpen heardShot delta enemy
    moved := moved.push next
    totalDamage := totalDamage + damage
    if let some fireball := projectile then spawned := spawned.push fireball
  return (moved, totalDamage, spawned)

def updateProjectiles (camera : Camera) (level : Nat) (doorOpen cacheOpen delta : Float) (projectiles : Array Projectile) :
    Array Projectile × Nat := Id.run do
  let mut active := #[]
  let mut totalDamage := 0
  for projectile in projectiles do
    let nextPosition := projectile.position.add (projectile.velocity.scale delta)
    let nextLife := projectile.life - delta
    let playerDistance := (nextPosition.sub camera.position).length
    if playerDistance < 0.38 then
      totalDamage := totalDamage + projectile.damage
    else if nextLife > 0.0 && !blockedAt level doorOpen cacheOpen nextPosition.x nextPosition.z then
      active := active.push { projectile with position := nextPosition, life := nextLife }
  return (active, totalDamage)

def spawnBurst (origin : Vec3) (kind count : Nat) : Array Particle := Id.run do
  let mut particles := #[]
  for index in [0:count] do
    let spreadX := (Float.ofNat (index % 5) - 2.0) *
      (if kind == 1 then 0.88 else if kind == 2 then 0.62 else 0.74)
    let spreadZ := (Float.ofNat ((index * 3 + 1) % 5) - 2.0) *
      (if kind == 1 then 0.88 else if kind == 2 then 0.62 else 0.74)
    let lift := if kind == 1 then 1.7 + Float.ofNat (index % 3) * 0.35
      else if kind == 2 then 1.25 + Float.ofNat (index % 4) * 0.24
      else 1.15 + Float.ofNat (index % 4) * 0.36
    particles := particles.push {
      position := origin
      velocity := ⟨spreadX, lift, spreadZ⟩
      life := if kind == 1 then 0.34 else if kind == 2 then 0.72 else 0.62
      kind
    }
  return particles

def updateParticles (level : Nat) (doorOpen cacheOpen delta : Float) (particles : Array Particle) : Array Particle := Id.run do
  let mut active := #[]
  for particle in particles do
    let life := particle.life - delta
    if life > 0.0 then
      let gravity := if particle.kind == 1 then 6.8 else 4.4
      let velocity := { particle.velocity with y := particle.velocity.y - gravity * delta }
      let attempted := particle.position.add (velocity.scale delta)
      let hitWall := blockedAt level doorOpen cacheOpen attempted.x attempted.z
      let position := if hitWall then particle.position else
        { attempted with y := max 0.045 (min 3.43 attempted.y) }
      let velocity := if hitWall then ⟨-velocity.x * 0.28, velocity.y * 0.45, -velocity.z * 0.28⟩
        else if attempted.y <= 0.045 then ⟨velocity.x * 0.55, 0.0, velocity.z * 0.55⟩
        else if attempted.y >= 3.43 then ⟨velocity.x, -velocity.y * 0.25, velocity.z⟩
        else velocity
      active := active.push { particle with position, velocity, life }
  return active

def enemyHitParticles (before after : Array Enemy) : Array Particle := Id.run do
  let mut particles := #[]
  for (oldEnemy, newEnemy) in before.toList.zip after.toList do
    if oldEnemy.health > newEnemy.health then
      let height := if newEnemy.kind == 3 then 1.45 else 1.05
      let count := if newEnemy.kind == 3 then 11 else 7
      particles := particles ++ spawnBurst (newEnemy.position.add ⟨0.0, height, -0.18⟩) 0 count
  return particles

def barrelHitParticles (before after : Array Barrel) : Array Particle := Id.run do
  let mut particles := #[]
  for (oldBarrel, newBarrel) in before.toList.zip after.toList do
    if oldBarrel.health > 0 && newBarrel.health == 0 then
      particles := particles ++ spawnBurst (newBarrel.position.add ⟨0.0, 0.72, 0.0⟩) 1 9
  return particles

def explosionParticles (before after : Array Barrel) : Array Particle := Id.run do
  let mut particles := #[]
  for (oldBarrel, newBarrel) in before.toList.zip after.toList do
    if oldBarrel.health == 0 && oldBarrel.blastTime > 0.14 && newBarrel.blastTime <= 0.14 then
      let origin := newBarrel.position.add ⟨0.0, 0.55, 0.0⟩
      particles := particles ++ spawnBurst origin 1 12 ++ spawnBurst origin 2 9
  return particles

def deathMarks (before after : Array Enemy) : Array ImpactMark := Id.run do
  let mut marks := #[]
  for (oldEnemy, newEnemy) in before.toList.zip after.toList do
    if oldEnemy.health > 0 && newEnemy.health == 0 then
      marks := marks.push { position := newEnemy.position, kind := 1 }
  return marks

def capArray {alpha : Type} (limit : Nat) (values : Array alpha) : Array alpha :=
  if values.size <= limit then values else values.extract (values.size - limit) values.size

def updateBarrels (camera : Camera) (delta : Float) (barrels : Array Barrel)
    (enemies : Array Enemy) : Array Barrel × Array Enemy × Nat := Id.run do
  let mut advanced := #[]
  let mut detonations : Array Vec3 := #[]
  for barrel in barrels do
    let nextTime := max 0.0 (barrel.blastTime - delta)
    if barrel.health == 0 && barrel.blastTime > 0.14 && nextTime <= 0.14 then
      detonations := detonations.push barrel.position
    advanced := advanced.push { barrel with blastTime := nextTime }
  let mut nextBarrels := advanced
  let mut nextEnemies := enemies
  let mut playerDamage := 0
  for center in detonations do
    let playerDx := camera.position.x - center.x
    let playerDz := camera.position.z - center.z
    if playerDx * playerDx + playerDz * playerDz < 4.84 then
      playerDamage := playerDamage + 28
    nextEnemies := nextEnemies.map fun enemy =>
      if enemy.health == 0 then enemy
      else
        let dx := enemy.position.x - center.x
        let dz := enemy.position.z - center.z
        if dx * dx + dz * dz < 6.25 then
          let health := enemy.health - 3
          { enemy with
            health
            alerted := true
            painTime := if health == 0 then 0.0 else 0.18
            deathTime := if health == 0 then 0.62 else enemy.deathTime
            attackWindup := 0.0 }
        else enemy
    nextBarrels := nextBarrels.map fun barrel =>
      if barrel.health == 0 then barrel
      else
        let dx := barrel.position.x - center.x
        let dz := barrel.position.z - center.z
        if dx * dx + dz * dz < 5.29 then
          { barrel with health := 0, blastTime := 0.28 }
        else barrel
  return (nextBarrels, nextEnemies, playerDamage)

def aliveCount (enemies : Array Enemy) : Nat :=
  enemies.foldl (fun count enemy => if enemy.health > 0 then count + 1 else count) 0

def updatePickups (camera : Camera) (pickups : Array Pickup) :
    Array Pickup × Nat × Nat × Nat × Bool × Bool := Id.run do
  let mut remaining := #[]
  let mut healthGain := 0
  let mut shellGain := 0
  let mut bulletGain := 0
  let mut gotChaingun := false
  let mut gotRedKey := false
  for pickup in pickups do
    let distance := (pickup.position.sub camera.position).length
    if pickup.active && distance < 1.75 then
      remaining := remaining.push { pickup with active := false }
      if pickup.kind == 0 then healthGain := healthGain + 25
      else if pickup.kind == 1 then shellGain := shellGain + 12
      else if pickup.kind == 2 then
        bulletGain := bulletGain + 40
        gotChaingun := true
      else gotRedKey := true
    else remaining := remaining.push pickup
  return (remaining, healthGain, shellGain, bulletGain, gotChaingun, gotRedKey)

def nearDoor (camera : Camera) : Bool :=
  camera.position.x > -2.0 && camera.position.x < 2.0 &&
    camera.position.z > -1.2 && camera.position.z < 2.0

def updateDoor (camera : Camera) (use hasRedKey : Bool) (current delta : Float) : Float :=
  let opening := current > 0.0 || (use && hasRedKey && nearDoor camera)
  if opening then min 1.0 (current + delta * 1.18) else current

def nearSecretPanel (camera : Camera) : Bool :=
  let dx := camera.position.x + 7.05
  let dz := camera.position.z + 4.36
  dx * dx + dz * dz < 2.25

def nearCacheSwitch (camera : Camera) : Bool :=
  let dx := camera.position.x - 2.28
  let dz := camera.position.z - 1.48
  dx * dx + dz * dz < 1.35

def updateCacheDoor (found : Bool) (current delta : Float) : Float :=
  if found then min 1.0 (current + delta * 1.35) else current

def configureDifficulty (state : GameState) (difficulty : Nat) : GameState :=
  let enemies := state.enemies.map fun enemy =>
    let health := if difficulty == 0 then max 1 ((enemy.health * 3 + 3) / 4)
      else if difficulty == 2 then enemy.health + (enemy.health + 1) / 2 else enemy.health
    { enemy with health, alerted := enemy.alerted || difficulty == 2 }
  { state with
    difficulty
    enemies
    ammo := if difficulty == 0 then 80 else if difficulty == 2 then 40 else 60
  }

def update (state : GameState) (input previous : Input) (delta : Float) : GameState :=
  if !state.started then
    let difficulty := if input.weapon1 then 0 else if input.weapon2 then 1
      else if input.weapon3 then 2 else state.difficulty
    let selected := { state with difficulty }
    if input.confirm && !previous.confirm then
      configureDifficulty { selected with started := true } difficulty
    else selected
  else if input.pause && !previous.pause then
    { state with paused := !state.paused, shotThisFrame := false }
  else if state.paused then
    { state with shotThisFrame := false }
  else if state.health == 0 || state.levelComplete then
    { state with
      muzzleFlash := state.muzzleFlash - 1
      damageFlash := state.damageFlash - 1
      hitMarker := state.hitMarker - 1
      pickupFlash := state.pickupFlash - 1
      keyFlash := state.keyFlash - 1
      weaponCooldown := max 0.0 (state.weaponCooldown - delta)
      shotThisFrame := false }
  else
    let lookX := (if input.lookRight then 1.0 else 0.0) -
      (if input.lookLeft then 1.0 else 0.0)
    let lookY := (if input.lookDown then 1.0 else 0.0) -
      (if input.lookUp then 1.0 else 0.0)
    let camera := { state.camera with
      yaw := state.camera.yaw + lookX * 1.9 * delta + input.mouseX * 0.0032
      pitch := clampFloat
        (state.camera.pitch + lookY * 1.4 * delta + input.mouseY * 0.0028) (-0.85) 0.85 }
    let forwardAxis := (if input.forward then 1.0 else 0.0) -
      (if input.backward then 1.0 else 0.0)
    let sideAxis := (if input.right then 1.0 else 0.0) -
      (if input.left then 1.0 else 0.0)
    let speed := (if input.sprint then 4.8 else 2.8) * delta
    let dx := (camera.yaw.sin * forwardAxis + camera.yaw.cos * sideAxis) * speed
    let dz := (camera.yaw.cos * forwardAxis - camera.yaw.sin * sideAxis) * speed
    let doorOpen := if state.level == 0 then
      updateDoor camera input.use state.hasRedKey state.doorOpen delta else 1.0
    let foundCacheNow := state.level == 0 && !state.cacheFound && input.use && !previous.use && nearCacheSwitch camera
    let cacheFound := state.cacheFound || foundCacheNow
    let cacheDoorOpen := updateCacheDoor cacheFound state.cacheDoorOpen delta
    let movedCamera := moveCamera camera state.level doorOpen cacheDoorOpen dx dz
    let barrelBlocked := state.barrels.any fun barrel =>
      if barrel.health == 0 then false
      else
        let barrelDx := movedCamera.position.x - barrel.position.x
        let barrelDz := movedCamera.position.z - barrel.position.z
        barrelDx * barrelDx + barrelDz * barrelDz < 0.49
    let camera := if barrelBlocked then { movedCamera with position := state.camera.position }
      else movedCamera
    let mapOpen := if input.map && !previous.map then !state.mapOpen else state.mapOpen
    let foundSecretNow := state.level == 0 && !state.secretFound && input.use && !previous.use && nearSecretPanel camera
    let secretFound := state.secretFound || foundSecretNow
    let (pickups, healthGain, shellGain, bulletGain, gotChaingun, gotRedKey) :=
      updatePickups camera state.pickups
    let hasChaingun := state.hasChaingun || gotChaingun
    let hasRedKey := state.hasRedKey || gotRedKey
    let triedLockedDoor := state.level == 0 && input.use && !previous.use && nearDoor camera && !hasRedKey
    let weapon := if gotChaingun then 1
      else if input.weapon1 then 0
      else if input.weapon2 && hasChaingun then 1
      else state.weapon
    let availableShells := min 99 (state.ammo + shellGain + if foundSecretNow then 16 else 0)
    let availableBullets := min 200 (state.bullets + bulletGain + if foundSecretNow then 60 else 0)
    let weaponCooldown := max 0.0 (state.weaponCooldown - delta)
    let hasAmmo := if weapon == 0 then availableShells >= 2 else availableBullets > 0
    let fired := input.shoot && hasAmmo && weaponCooldown <= 0.0
    let (shotEnemies, shotBarrels, hit) := if !fired then
      (state.enemies, state.barrels, false)
      else if weapon == 0 then
        shootShotgun camera state.level doorOpen cacheDoorOpen state.enemies state.barrels
      else
        let (enemies, enemyHit) :=
          shootEnemies camera state.level doorOpen cacheDoorOpen 1 state.enemies
        let (barrels, barrelHit) := if enemyHit then (state.barrels, false) else
          shootBarrels camera state.level doorOpen cacheDoorOpen 1 state.barrels
        (enemies, barrels, enemyHit || barrelHit)
    let (movedEnemies, meleeDamage, spawned) :=
      updateEnemies camera state.level doorOpen cacheDoorOpen fired delta shotEnemies
    let (barrels, enemies, barrelDamage) :=
      updateBarrels camera delta shotBarrels movedEnemies
    let (projectiles, projectileDamage) :=
      updateProjectiles camera state.level doorOpen cacheDoorOpen delta (state.projectiles ++ spawned)
    let wallImpacts : Array Vec3 := if fired && !hit then
      if weapon == 0 then shotgunWallImpacts camera state.level doorOpen cacheDoorOpen
      else match raycastImpact camera state.level doorOpen cacheDoorOpen with
        | some position => #[position]
        | none => #[]
      else #[]
    let wallParticles := wallImpacts.foldl (fun particles position =>
      particles ++ spawnBurst position 1 3) #[]
    let wallMarks : Array ImpactMark := wallImpacts.map fun position => { position, kind := 0 }
    let freshParticles := enemyHitParticles state.enemies shotEnemies ++
      barrelHitParticles state.barrels shotBarrels ++ explosionParticles state.barrels barrels ++
      wallParticles
    let particles := capArray 96
      (updateParticles state.level doorOpen cacheDoorOpen delta state.particles ++ freshParticles)
    let marks := capArray 48 (state.marks ++ deathMarks state.enemies enemies ++ wallMarks)
    let rawDamage := meleeDamage + projectileDamage + barrelDamage
    let damage := if state.difficulty == 0 then rawDamage * 3 / 4
      else if state.difficulty == 2 then (rawDamage * 3 + 1) / 2 else rawDamage
    let kills := aliveCount state.enemies - aliveCount enemies
    let killValue := if state.difficulty == 0 then 75 else if state.difficulty == 2 then 150 else 100
    let bossWasAlive := state.enemies.any fun enemy => enemy.kind == 3 && enemy.health > 0
    let bossStillAlive := enemies.any fun enemy => enemy.kind == 3 && enemy.health > 0
    let bossValue := if state.difficulty == 0 then 750 else if state.difficulty == 2 then 1500 else 1000
    let bossKillBonus := if bossWasAlive && !bossStillAlive then bossValue else 0
    let cleared := enemies.all fun enemy => enemy.health == 0 || !enemy.countsForExit
    let exitX := if state.level == 0 then 0.0 else 6.35
    let exitZ := if state.level == 0 then 6.8 else 6.45
    let exitDx := camera.position.x - exitX
    let exitDz := camera.position.z - exitZ
    let levelComplete := cleared && exitDx * exitDx + exitDz * exitDz < 0.72
    {
      camera
      enemies
      barrels
      ammo := if fired && weapon == 0 then availableShells - 2 else availableShells
      bullets := if fired && weapon == 1 then availableBullets - 1 else availableBullets
      weapon
      hasChaingun
      hasRedKey
      muzzleFlash := if fired then (if weapon == 0 then 3 else 2) else state.muzzleFlash - 1
      health := min 100 (state.health + healthGain + if foundSecretNow then 35 else 0) - damage
      damageFlash := if damage > 0 then 5 else state.damageFlash - 1
      score := state.score + kills * killValue + (if fired && hit then 5 else 0) +
        (if foundSecretNow then 500 else 0) + (if foundCacheNow then 500 else 0) + bossKillBonus
      projectiles
      particles
      marks
      weaponCooldown := if fired then (if weapon == 0 then 0.82 else 0.11) else weaponCooldown
      bobPhase := state.bobPhase + if forwardAxis != 0.0 || sideAxis != 0.0 then
        delta * (if input.sprint then 13.0 else 9.0) else 0.0
      bobStrength := if forwardAxis != 0.0 || sideAxis != 0.0 then
        min 1.0 (state.bobStrength + delta * 6.0) else max 0.0 (state.bobStrength - delta * 7.0)
      recoilKick := if fired && weapon == 0 then 1.0 else
        max 0.0 (state.recoilKick - delta * 5.5)
      hitMarker := if hit then 4 else state.hitMarker - 1
      pickupFlash := if healthGain > 0 || shellGain > 0 || bulletGain > 0 ||
          gotChaingun || gotRedKey then 4 else state.pickupFlash - 1
      pickups
      doorOpen
      levelComplete
      shotThisFrame := fired
      mapOpen
      secretFound
      secretFlash := if foundSecretNow || foundCacheNow then 90 else state.secretFlash - 1
      keyFlash := if gotRedKey then 90 else if triedLockedDoor then 55 else state.keyFlash - 1
      cacheFound
      cacheDoorOpen
      started := state.started
      paused := state.paused
      playTime := state.playTime + delta
      shotsFired := state.shotsFired + if fired then 1 else 0
      shotsHit := state.shotsHit + if fired && hit then 1 else 0
      killsMade := state.killsMade + kills
      difficulty := state.difficulty
      level := state.level
    }

def initialState : GameState := {
  camera := { position := ⟨0.0, 1.6, -5.8⟩, yaw := 0.0, pitch := 0.0 }
  enemies := #[
    { position := ⟨-1.8, 0.0, -2.1⟩, health := 3, kind := 0 },
    { position := ⟨3.7, 0.0, -1.6⟩, health := 3, kind := 2 },
    { position := ⟨4.8, 0.0, 5.4⟩, health := 3, kind := 1 },
    { position := ⟨-5.2, 0.0, 5.8⟩, health := 3, kind := 2 },
    { position := ⟨-3.8, 0.0, 2.6⟩, health := 3, kind := 1 },
    { position := ⟨2.90, 0.0, 2.52⟩, health := 3, kind := 1, countsForExit := false },
    { position := ⟨0.0, 0.0, 6.20⟩, health := 8, kind := 3 }
  ]
  barrels := #[
    { position := ⟨1.2, 0.0, -2.25⟩ },
    { position := ⟨4.25, 0.0, 3.85⟩ },
    { position := ⟨5.35, 0.0, 3.95⟩ }
  ]
  ammo := 60
  bullets := 0
  weapon := 0
  hasChaingun := false
  hasRedKey := false
  muzzleFlash := 0
  health := 100
  damageFlash := 0
  score := 0
  projectiles := #[]
  particles := #[]
  marks := #[]
  weaponCooldown := 0.0
  bobPhase := 0.0
  bobStrength := 0.0
  recoilKick := 0.0
  hitMarker := 0
  pickupFlash := 0
  pickups := #[
    { position := ⟨5.5, 0.0, -2.5⟩, kind := 0 },
    { position := ⟨-5.4, 0.0, 2.2⟩, kind := 1 },
    { position := ⟨-2.0, 0.0, 3.0⟩, kind := 2 },
    { position := ⟨4.9, 0.0, 6.3⟩, kind := 0 },
    { position := ⟨5.75, 0.0, -5.25⟩, kind := 3 },
    { position := ⟨2.65, 0.0, 2.52⟩, kind := 0 },
    { position := ⟨3.25, 0.0, 2.52⟩, kind := 1 }
  ]
  doorOpen := 0.0
  levelComplete := false
  shotThisFrame := false
  mapOpen := false
  secretFound := false
  secretFlash := 0
  keyFlash := 0
  cacheFound := false
  cacheDoorOpen := 0.0
  started := true
  paused := false
  playTime := 0.0
  shotsFired := 0
  shotsHit := 0
  killsMade := 0
  difficulty := 1
  level := 0
}

def levelTwoBase : GameState := {
  initialState with
  level := 1
  camera := { position := ⟨-5.8, 1.6, -5.8⟩, yaw := 0.68, pitch := 0.0 }
  enemies := #[
    { position := ⟨-2.5, 0.0, -5.0⟩, health := 3, kind := 0 },
    { position := ⟨3.6, 0.0, -4.4⟩, health := 3, kind := 1 },
    { position := ⟨5.6, 0.0, -0.8⟩, health := 3, kind := 2 },
    { position := ⟨-5.0, 0.0, -0.2⟩, health := 3, kind := 1 },
    { position := ⟨-5.4, 0.0, 2.8⟩, health := 3, kind := 2 },
    { position := ⟨3.8, 0.0, 2.9⟩, health := 3, kind := 1 },
    { position := ⟨4.3, 0.0, 5.6⟩, health := 3, kind := 2 },
    { position := ⟨6.35, 0.0, 6.45⟩, health := 10, kind := 3 }
  ]
  barrels := #[
    { position := ⟨0.4, 0.0, -4.1⟩ },
    { position := ⟨-4.2, 0.0, 2.3⟩ },
    { position := ⟨3.4, 0.0, 5.15⟩ }
  ]
  pickups := #[
    { position := ⟨3.5, 0.0, -4.0⟩, kind := 1 },
    { position := ⟨-5.0, 0.0, 2.4⟩, kind := 0 },
    { position := ⟨3.6, 0.0, 5.15⟩, kind := 0 }
  ]
  doorOpen := 1.0
  cacheDoorOpen := 1.0
  projectiles := #[]
  particles := #[]
  marks := #[]
  levelComplete := false
  mapOpen := false
  secretFound := false
  cacheFound := false
  secretFlash := 0
  keyFlash := 0
  playTime := 0.0
  shotsFired := 0
  shotsHit := 0
  killsMade := 0
}

def freshLevel (state : GameState) : GameState :=
  if state.level == 0 then
    configureDifficulty { initialState with difficulty := state.difficulty } state.difficulty
  else
    configureDifficulty { levelTwoBase with difficulty := state.difficulty } state.difficulty

def advanceLevel (state : GameState) : GameState :=
  let next := configureDifficulty { levelTwoBase with difficulty := state.difficulty } state.difficulty
  { next with
    health := min 100 (state.health + 25)
    ammo := min 99 (state.ammo + 12)
    bullets := min 200 (state.bullets + if state.hasChaingun then 25 else 0)
    hasChaingun := state.hasChaingun
    weapon := if state.hasChaingun then state.weapon else 0
    score := state.score
  }

def pairedEnemyEvent (before after : GameState) (predicate : Enemy → Enemy → Bool) : Bool :=
  (before.enemies.toList.zip after.enemies.toList).any fun (oldEnemy, newEnemy) =>
    predicate oldEnemy newEnemy

def pairedBarrelEvent (before after : GameState) (predicate : Barrel → Barrel → Bool) : Bool :=
  (before.barrels.toList.zip after.barrels.toList).any fun (oldBarrel, newBarrel) =>
    predicate oldBarrel newBarrel

def activePickupCount (state : GameState) : Nat :=
  state.pickups.foldl (fun count pickup => if pickup.active then count + 1 else count) 0

def audioCue (before after : GameState) : Nat :=
  let died := pairedEnemyEvent before after fun oldEnemy newEnemy =>
    (oldEnemy.health > 0 && newEnemy.health == 0) ||
      (oldEnemy.health == 0 && oldEnemy.deathTime >= 0.60 && newEnemy.deathTime < 0.60)
  let bossDied := pairedEnemyEvent before after fun oldEnemy newEnemy =>
    oldEnemy.kind == 3 && ((oldEnemy.health > 0 && newEnemy.health == 0) ||
      (oldEnemy.health == 0 && oldEnemy.deathTime >= 0.60 && newEnemy.deathTime < 0.60))
  let bossAlerted := pairedEnemyEvent before after fun oldEnemy newEnemy =>
    newEnemy.kind == 3 && !oldEnemy.alerted && newEnemy.alerted
  let alerted := pairedEnemyEvent before after fun oldEnemy newEnemy =>
    oldEnemy.kind != 3 && !oldEnemy.alerted && newEnemy.alerted
  let pain := pairedEnemyEvent before after fun oldEnemy newEnemy =>
    oldEnemy.painTime >= 0.12 && newEnemy.painTime < 0.12 && newEnemy.health > 0
  let barrelBlast := pairedBarrelEvent before after fun oldBarrel newBarrel =>
    oldBarrel.health == 0 && oldBarrel.blastTime > 0.14 && newBarrel.blastTime <= 0.14
  let projectileSpawned := after.projectiles.size > before.projectiles.size
  let bossProjectile := projectileSpawned && after.projectiles.any fun projectile => projectile.damage > 12
  let projectileEnded := before.projectiles.size > after.projectiles.size
  let secretFound := after.secretFlash > before.secretFlash
  let gotKey := !before.hasRedKey && after.hasRedKey
  let doorStarted := (before.doorOpen <= 0.0 && after.doorOpen > 0.0) ||
    (before.cacheDoorOpen <= 0.0 && after.cacheDoorOpen > 0.0)
  let gotPickup := activePickupCount after < activePickupCount before
  if bossDied then 11
  else if barrelBlast then 9
  else if bossAlerted then 10
  else if died then 3
  else if bossProjectile then 13
  else if projectileSpawned then 4
  else if after.health < before.health || projectileEnded then 5
  else if secretFound then 7
  else if gotKey then 12
  else if doorStarted then 6
  else if gotPickup then 8
  else if alerted then 1
  else if pain then 2
  else 0

partial def gameLoop (state : GameState) (previous : Input) (lastFrame : Nat) : IO Unit := do
  let frameStart ← IO.monoMsNow
  let elapsed := max 1 (min 100 (frameStart - lastFrame))
  let input ← pollInput
  if input.quit then closeWindow
  else
    let advanced := state.level == 0 && state.levelComplete && input.confirm && !previous.confirm
    let restarted := input.restart && (state.health == 0 || state.levelComplete)
    let base := if advanced then advanceLevel state else if restarted then freshLevel state else state
    let transitioned := advanced || restarted
    let next := update base input (if transitioned then noInput else previous)
      (Float.ofNat elapsed / 1000.0)
    if next.shotThisFrame && next.weapon == 0 then playShot
    else if next.shotThisFrame && next.weapon == 1 then playChaingun
    else
      let cue := audioCue state next
      if cue > 0 then playCue (UInt32.ofNat cue)
    let running ← presentGpuState next
    if running then
      let frameEnd ← IO.monoMsNow
      let work := frameEnd - frameStart
      if work < targetFrameMs then IO.sleep (UInt32.ofNat (targetFrameMs - work))
      gameLoop next input frameStart
    else closeWindow

def runGame (visible : Bool) : IO Unit := do
  let opened ← createWindow 960 540 visible
  if !opened then throw (IO.userError "Could not create the Lean 64 window")
  let start ← IO.monoMsNow
  gameLoop { initialState with started := false } noInput start

def cinematicDemoState (frame : Nat) : GameState :=
  let phase := frame % 360
  let travel := min 1.0 (Float.ofNat phase / 150.0)
  let distance := travel * 1.68
  let shotAge := if phase >= 165 then phase - 165 else 0
  let fired := phase >= 165
  let recoil := if shotAge < 2 then 1.0 else if shotAge < 5 then 0.7
    else if shotAge < 10 then 0.35 else 0.0
  let enemies := levelTwoBase.enemies.toList.zipIdx.map (fun (enemy, index) =>
    if index == 0 then
      { enemy with
        health := if shotAge >= 5 then 0 else 3
        alerted := true
        phase := Float.ofNat phase * 0.035
        painTime := if shotAge >= 2 && shotAge < 5 then 0.14 else 0.0
        deathTime := if shotAge >= 5 && shotAge < 38 then
          max 0.08 (0.62 - Float.ofNat (shotAge - 5) / 55.0) else 0.0 }
    else { enemy with alerted := false }) |>.toArray
  { levelTwoBase with
    camera := { position := ⟨-5.65 + 0.9246 * distance, 1.6,
      -5.75 + 0.3809 * distance⟩, yaw := 1.18 + travel * 0.28, pitch := -0.02 }
    enemies
    hasChaingun := true
    weapon := 0
    bobPhase := Float.ofNat phase * 0.12
    bobStrength := if fired then 0.35 else 1.0
    recoilKick := recoil
    muzzleFlash := if shotAge < 2 && fired then 3 else if shotAge < 4 && fired then 2 else 0
    weaponCooldown := if fired && shotAge < 45 then max 0.0 (0.82 - Float.ofNat shotAge / 55.0) else 0.0
    ammo := if fired then 32 else 34
    playTime := 4.0 + Float.ofNat phase / 60.0
    particles := if shotAge < 36 && fired then
      updateParticles 0 1.0 1.0 (Float.ofNat shotAge / 60.0)
        (spawnBurst ⟨-2.5, 1.05, -5.0⟩ 0 14) else #[]
    marks := if shotAge >= 5 then #[{ position := ⟨-2.5, 0.04, -5.0⟩, kind := 1 }] else #[] }

partial def demoLoop (frame lastFrame : Nat) : IO Unit := do
  let running ← presentGpuState (cinematicDemoState frame)
  if running then
    let now ← IO.monoMsNow
    let target := lastFrame + 16
    if now < target then IO.sleep (UInt32.ofNat (target - now))
    demoLoop (frame + 1) (max target now)
  else closeWindow

def runDemo : IO Unit := do
  let opened ← createWindow 1280 720 true
  if !opened then throw (IO.userError "Could not create demo window")
  let start ← IO.monoMsNow
  demoLoop 0 start

def smokeTest (withWindow : Bool) : IO Unit := do
  let audioAssets : List System.FilePath := [
    "assets/alert.wav", "assets/pain.wav", "assets/death.wav", "assets/fireball.wav",
    "assets/impact.wav", "assets/door.wav", "assets/secret.wav", "assets/pickup.wav",
    "assets/barrel.wav", "assets/boss_alert.wav", "assets/boss_death.wav",
    "assets/key.wav", "assets/boss_fire.wav", "assets/shot.wav", "assets/chaingun.wav"
  ]
  for path in audioAssets do
    let bytes ← IO.FS.readBinFile path
    if bytes.size <= 44 then throw (IO.userError s!"Invalid or empty audio asset: {path}")
  playCue 0
  let renderStart ← IO.monoMsNow
  let pixels := render initialState
  let pixelCount := pixels.size
  let renderEnd ← IO.monoMsNow
  if pixelCount != renderWidth * renderHeight then
    throw (IO.userError s!"Framebuffer has the wrong size: {pixelCount}")
  let titleState := { initialState with started := false }
  let titlePixels := render titleState
  let startInput := { noInput with confirm := true }
  let startedState := update titleState startInput noInput 0.01
  if titlePixels.size != pixelCount || !startedState.started then
    throw (IO.userError "Title/start transition smoke test failed")
  let easyStarted := update titleState { noInput with weapon1 := true, confirm := true } noInput 0.01
  let nightmareStarted := update titleState { noInput with weapon3 := true, confirm := true } noInput 0.01
  let easyBossHealth := easyStarted.enemies.foldl (init := 0) fun health enemy =>
    if enemy.kind == 3 then enemy.health else health
  let nightmareBossHealth := nightmareStarted.enemies.foldl (init := 0) fun health enemy =>
    if enemy.kind == 3 then enemy.health else health
  if easyStarted.difficulty != 0 || easyStarted.ammo != 80 || easyBossHealth != 6 ||
      nightmareStarted.difficulty != 2 || nightmareStarted.ammo != 40 ||
      nightmareBossHealth != 12 || !nightmareStarted.enemies.all (fun enemy => enemy.alerted) then
    throw (IO.userError "Difficulty deployment configuration smoke test failed")
  let pauseInput := { noInput with pause := true }
  let pausedState := update initialState pauseInput noInput 0.01
  let heldPause := update pausedState pauseInput pauseInput 0.5
  let pausedMovement := update pausedState { noInput with forward := true } noInput 0.5
  let resumedState := update pausedState pauseInput noInput 0.01
  if !pausedState.paused || !heldPause.paused ||
      pausedMovement.camera.position.z != pausedState.camera.position.z ||
      pausedMovement.playTime != pausedState.playTime || resumedState.paused then
    throw (IO.userError "Pause edge/freeze smoke test failed")
  let motionBase := { initialState with enemies := #[], barrels := #[], pickups := #[] }
  let walkedBob := update motionBase { noInput with forward := true } noInput 0.1
  let sprintedBob := update motionBase { noInput with forward := true, sprint := true } noInput 0.1
  let settledBob := update walkedBob noInput noInput 0.1
  let kickedView := update motionBase { noInput with shoot := true } noInput 0.01
  let recoveredView := update kickedView noInput noInput 0.1
  if walkedBob.bobStrength <= 0.0 || walkedBob.bobPhase <= 0.0 ||
      sprintedBob.bobPhase <= walkedBob.bobPhase || settledBob.bobStrength >= walkedBob.bobStrength ||
      kickedView.recoilKick != 1.0 || recoveredView.recoilKick >= kickedView.recoilKick then
    throw (IO.userError "Movement bob/sprint/recoil recovery smoke test failed")
  let stillView := { motionBase with playTime := 3.0 }
  let bobbedPixels := render { stillView with bobPhase := 1.1, bobStrength := 1.0 }
  let kickedPixels := render { stillView with recoilKick := 1.0 }
  let stillPixels := render stillView
  if bobbedPixels == stillPixels || kickedPixels == stillPixels then
    throw (IO.userError "Rendered view bob/recoil kick smoke test failed")
  match (sceneMesh stillView)[0]? with
  | some triangle =>
    let lit := illuminateTriangle stillView.camera 3 triangle
    if lit.color.r <= triangle.color.r || lit.color.g <= triangle.color.g then
      throw (IO.userError "Distance-aware muzzle illumination smoke test failed")
  | none => throw (IO.userError "Muzzle illumination test had no world triangle")
  let damagedPalette := render { stillView with damageFlash := 5 }
  let pickupPalette := render { stillView with pickupFlash := 4 }
  if damagedPalette == stillPixels || pickupPalette == stillPixels || damagedPalette == pickupPalette then
    throw (IO.userError "Damage/pickup palette render smoke test failed")
  let pausedPixels := render pausedState
  if pausedPixels[20 * renderWidth + 20]? != some (packedColor ⟨10, 11, 16⟩) then
    throw (IO.userError "Pause overlay smoke test failed")
  let keyHudPixels := render { initialState with hasRedKey := true }
  if keyHudPixels[7 * renderWidth + 7]? != some (packedColor ⟨250, 192, 58⟩) then
    throw (IO.userError "Screen-space HUD layering smoke test failed")
  let testBurst := spawnBurst ⟨0.0, 1.0, 0.0⟩ 0 7
  if testBurst.size != 7 || !(updateParticles 0 1.0 1.0 1.0 testBurst).isEmpty then
    throw (IO.userError "Particle spawn/lifetime smoke test failed")
  let wallCamera : Camera := { position := ⟨0.0, 1.6, -7.0⟩, yaw := 3.14159, pitch := 0.0 }
  if (raycastImpact wallCamera 0 1.0 1.0).isNone then
    throw (IO.userError "World impact raycast smoke test failed")
  let wallShotState := { initialState with
    camera := wallCamera
    enemies := #[]
    barrels := #[]
    pickups := #[]
    projectiles := #[]
  }
  let markedWall := update wallShotState { noInput with shoot := true } noInput 0.01
  if markedWall.marks.size != 5 || markedWall.particles.size != 15 ||
      (shotgunWallImpacts wallCamera 0 1.0 1.0).size != 5 then
    throw (IO.userError "Missed-shot spark/mark smoke test failed")
  let testEnemy : Enemy := { position := ⟨0.0, 0.0, 0.0⟩, health := 3 }
  let (shot, hit) := shootEnemies initialState.camera 0 1.0 1.0 2 #[testEnemy]
  match shot[0]? with
  | some enemy =>
    if !hit || enemy.health != 1 || enemy.painTime <= 0.0 then
      throw (IO.userError "Hitscan combat smoke test failed")
  | none => throw (IO.userError "Hitscan removed the test monster")
  let leftTarget : Enemy := { position := ⟨-0.8, 0.0, 0.0⟩, health := 2 }
  let rightTarget : Enemy := { position := ⟨0.8, 0.0, 0.0⟩, health := 2 }
  let (spreadTargets, _, spreadHit) := shootShotgun initialState.camera 0 1.0 1.0
    #[leftTarget, rightTarget] #[]
  match spreadTargets[0]?, spreadTargets[1]? with
  | some left, some right =>
    if !spreadHit || left.health >= leftTarget.health || right.health >= rightTarget.health then
      throw (IO.userError "Shotgun multi-target spread smoke test failed")
  | _, _ => throw (IO.userError "Shotgun spread removed a test monster")
  let (closeBlast, _, closeHit) := shootShotgun initialState.camera 0 1.0 1.0 #[testEnemy] #[]
  match closeBlast[0]? with
  | some target =>
    if !closeHit || target.health != 0 then
      throw (IO.userError "Shotgun close-range pellet damage smoke test failed")
  | none => throw (IO.userError "Shotgun close blast removed the test monster")
  let fragile : Enemy := { position := ⟨0.0, 0.0, 0.0⟩, health := 1 }
  let (killed, lethalHit) := shootEnemies initialState.camera 0 1.0 1.0 2 #[fragile]
  match killed[0]? with
  | some corpse =>
    let (falling, _, _) := updateEnemy initialState.camera 0 1.0 1.0 false 0.1 corpse
    if !lethalHit || corpse.health != 0 || corpse.deathTime <= 0.0 ||
        falling.deathTime >= corpse.deathTime then
      throw (IO.userError "Monster death animation smoke test failed")
  | none => throw (IO.userError "Lethal hit removed the test monster")
  let attacker : Enemy := {
    position := ⟨initialState.camera.position.x, 0.0, initialState.camera.position.z + 0.5⟩
    health := 3
  }
  let (_, damage, _) := updateEnemy initialState.camera 0 1.0 1.0 false 0.1 attacker
  if damage != 9 then throw (IO.userError "Monster attack smoke test failed")
  let ranged : Enemy := { position := ⟨0.0, 0.0, 0.0⟩, health := 3, kind := 1 }
  let (charging, _, earlyProjectile) := updateEnemy initialState.camera 0 1.0 1.0 false 0.1 ranged
  let (_, _, spawned) := updateEnemy initialState.camera 0 1.0 1.0 false 0.36 charging
  if charging.attackWindup <= 0.0 || earlyProjectile.isSome || spawned.isNone then
    throw (IO.userError "Ranged monster charge/release smoke test failed")
  let boss : Enemy := { position := ⟨0.0, 0.0, 0.0⟩, health := 8, kind := 3 }
  let (bossCharging, _, bossEarly) := updateEnemy initialState.camera 0 1.0 1.0 false 0.1 boss
  let (_, _, bossShot) := updateEnemy initialState.camera 0 1.0 1.0 false 0.31 bossCharging
  match bossShot with
  | some projectile =>
    if bossCharging.attackWindup <= 0.0 || bossEarly.isSome || projectile.damage != 18 then
      throw (IO.userError "Warden charge/projectile smoke test failed")
  | none => throw (IO.userError "Warden did not release its charged projectile")
  let quietBossState := { initialState with enemies := #[boss], projectiles := #[] }
  let loudBossState := { quietBossState with enemies := #[{ boss with alerted := true }] }
  if audioCue quietBossState loudBossState != 10 then
    throw (IO.userError "Warden alert audio event smoke test failed")
  let deadBossState := { loudBossState with
    enemies := #[{ boss with health := 0, alerted := true, deathTime := 0.62 }]
  }
  if audioCue loudBossState deadBossState != 11 then
    throw (IO.userError "Warden death audio event smoke test failed")
  let bossProjectileState := { loudBossState with projectiles := #[{
    position := ⟨0.0, 1.0, 1.0⟩
    velocity := ⟨0.0, 0.0, 1.0⟩
    life := 1.0
    damage := 18
  }] }
  if audioCue loudBossState bossProjectileState != 13 then
    throw (IO.userError "Warden fire audio event smoke test failed")
  let impact : Projectile := {
    position := initialState.camera.position.add ⟨0.0, 0.0, 0.1⟩
    velocity := ⟨0.0, 0.0, 0.0⟩
    life := 1.0
  }
  let (_, projectileDamage) := updateProjectiles initialState.camera 0 1.0 1.0 0.1 #[impact]
  if projectileDamage != 12 then throw (IO.userError "Fireball impact smoke test failed")
  let damageBase := { initialState with
    enemies := #[]
    barrels := #[]
    pickups := #[]
    projectiles := #[impact]
  }
  let easyDamage := update { damageBase with difficulty := 0 } noInput noInput 0.01
  let nightmareDamage := update { damageBase with difficulty := 2 } noInput noInput 0.01
  if easyDamage.health != 91 || nightmareDamage.health != 82 then
    throw (IO.userError "Difficulty damage scaling smoke test failed")
  let bossImpact : Projectile := { impact with damage := 18 }
  let (_, bossProjectileDamage) := updateProjectiles initialState.camera 0 1.0 1.0 0.1 #[bossImpact]
  if bossProjectileDamage != 18 then throw (IO.userError "Warden projectile damage smoke test failed")
  let targetBarrel : Barrel := { position := ⟨0.0, 0.0, 0.0⟩ }
  let (armedBarrels, barrelHit) := shootBarrels initialState.camera 0 1.0 1.0 2 #[targetBarrel]
  match armedBarrels[0]? with
  | some barrel =>
    if !barrelHit || barrel.health != 0 || barrel.blastTime <= 0.0 then
      throw (IO.userError "Explosive barrel hitscan smoke test failed")
  | none => throw (IO.userError "Barrel hitscan removed the barrel")
  let blastEnemy : Enemy := { position := ⟨0.8, 0.0, 0.0⟩, health := 3 }
  let primed : Barrel := { position := ⟨0.0, 0.0, 0.0⟩, health := 0, blastTime := 0.15 }
  let chained : Barrel := { position := ⟨1.1, 0.0, 0.0⟩ }
  let (blastBarrels, blastEnemies, distantDamage) :=
    updateBarrels initialState.camera 0.02 #[primed, chained] #[blastEnemy]
  match blastEnemies[0]?, blastBarrels[1]? with
  | some enemy, some barrel =>
    if enemy.health != 0 || enemy.deathTime <= 0.0 || barrel.health != 0 ||
        barrel.blastTime <= 0.0 || distantDamage != 0 then
      throw (IO.userError "Barrel splash/chain reaction smoke test failed")
  | _, _ => throw (IO.userError "Barrel splash/chain reaction removed test actors")
  let closeCamera : Camera := { initialState.camera with position := ⟨0.0, 1.6, 0.0⟩ }
  let (_, _, closeDamage) := updateBarrels closeCamera 0.02 #[primed] #[]
  if closeDamage != 28 then throw (IO.userError "Barrel player splash smoke test failed")
  let blastAudioBefore := { initialState with barrels := #[primed] }
  let blastAudioAfter := { blastAudioBefore with
    barrels := #[{ primed with blastTime := 0.13 }]
  }
  if audioCue blastAudioBefore blastAudioAfter != 9 then
    throw (IO.userError "Barrel audio event smoke test failed")
  let collisionState := { initialState with
    enemies := #[]
    barrels := #[{ position := ⟨0.0, 0.0, -5.05⟩ }]
    pickups := #[]
  }
  let walkedIntoBarrel := update collisionState { noInput with forward := true } noInput 0.2
  if walkedIntoBarrel.camera.position.z != collisionState.camera.position.z then
    throw (IO.userError "Player walked through a live barrel")
  let nearbyHealth : Pickup := {
    position := ⟨initialState.camera.position.x, 0.0, initialState.camera.position.z⟩
    kind := 0
  }
  let (_, healthGain, _, _, _, _) := updatePickups initialState.camera #[nearbyHealth]
  if healthGain != 25 then throw (IO.userError "Health pickup smoke test failed")
  let pickupPulse := update { initialState with
    health := 50
    enemies := #[]
    barrels := #[]
    pickups := #[nearbyHealth]
  } noInput noInput 0.01
  if pickupPulse.health != 75 || pickupPulse.pickupFlash != 4 then
    throw (IO.userError "Pickup palette pulse state smoke test failed")
  let nearbyChaingun : Pickup := {
    position := ⟨initialState.camera.position.x, 0.0, initialState.camera.position.z⟩
    kind := 2
  }
  let (_, _, _, bulletGain, gotChaingun, _) :=
    updatePickups initialState.camera #[nearbyChaingun]
  if !gotChaingun || bulletGain != 40 then
    throw (IO.userError "Chaingun pickup smoke test failed")
  let nearbyKey : Pickup := {
    position := ⟨initialState.camera.position.x, 0.0, initialState.camera.position.z⟩
    kind := 3
  }
  let (_, _, _, _, _, gotRedKey) := updatePickups initialState.camera #[nearbyKey]
  if !gotRedKey then throw (IO.userError "Red keycard pickup smoke test failed")
  if audioCue initialState { initialState with hasRedKey := true } != 12 then
    throw (IO.userError "Keycard audio event smoke test failed")
  let armed := { initialState with hasChaingun := true, bullets := 5 }
  let chaingunInput := { noInput with weapon2 := true, shoot := true }
  let firedChaingun := update armed chaingunInput noInput 0.01
  if firedChaingun.weapon != 1 || firedChaingun.bullets != 4 || !firedChaingun.shotThisFrame then
    throw (IO.userError "Chaingun switch/fire smoke test failed")
  let fragileBoss := { boss with health := 1, alerted := true }
  let bossFight := { initialState with
    enemies := #[fragileBoss]
    barrels := #[]
    pickups := #[]
    projectiles := #[]
  }
  let bossKilled := update bossFight { noInput with shoot := true } noInput 0.01
  if victory bossFight || !victory bossKilled || bossKilled.particles.size != 11 ||
      bossKilled.marks.size != 1 || bossKilled.enemies.any (fun enemy => enemy.health > 0) ||
      bossKilled.score != 1105 || bossKilled.shotsFired != 1 || bossKilled.shotsHit != 1 ||
      bossKilled.killsMade != 1 then
    throw (IO.userError "Warden kill bonus smoke test failed")
  let bossHud := render { bossFight with enemies := #[{ boss with alerted := true }] }
  if bossHud[5 * renderWidth + renderWidth / 2]? != some (packedColor ⟨250, 85, 235⟩) then
    throw (IO.userError "Warden health bar smoke test failed")
  let mapInput := { noInput with map := true }
  let mapped := update initialState mapInput noInput 0.01
  let heldMap := update mapped mapInput mapInput 0.01
  if !mapped.mapOpen || !heldMap.mapOpen then
    throw (IO.userError "Automap edge-toggle smoke test failed")
  let secretState := { initialState with
    camera := { initialState.camera with position := ⟨-7.05, 1.6, -4.36⟩ }
    health := 50
    ammo := 10
    bullets := 0
  }
  let secretInput := { noInput with use := true }
  let discovered := update secretState secretInput noInput 0.01
  let heldSecret := update discovered secretInput secretInput 0.01
  if !discovered.secretFound || discovered.secretFlash == 0 || discovered.health != 85 ||
      discovered.ammo != 26 || discovered.bullets != 60 || discovered.score != 500 ||
      heldSecret.score != 500 then
    throw (IO.userError "Secret discovery/reward smoke test failed")
  if !blockedAt 0 1.0 0.0 2.90 1.92 || blockedAt 0 1.0 1.0 2.90 1.92 ||
      !blockedAt 0 1.0 1.0 2.10 2.45 then
    throw (IO.userError "Secret chamber collision smoke test failed")
  let cacheCamera : Camera := { initialState.camera with position := ⟨2.90, 1.6, 1.30⟩ }
  let cacheEnemy : Enemy := {
    position := ⟨2.90, 0.0, 2.52⟩
    health := 3
    kind := 1
    countsForExit := false
  }
  let (sealedEnemy, _, _) := updateEnemy cacheCamera 0 1.0 0.0 false 0.1 cacheEnemy
  let (revealedEnemy, _, _) := updateEnemy cacheCamera 0 1.0 1.0 false 0.1 cacheEnemy
  if sealedEnemy.alerted || !revealedEnemy.alerted then
    throw (IO.userError "Secret chamber sight gating smoke test failed")
  let cacheSwitchCamera : Camera := { cacheCamera with position := ⟨2.28, 1.6, 1.48⟩ }
  let cacheState := { initialState with
    camera := cacheSwitchCamera
    enemies := #[cacheEnemy]
    barrels := #[]
    pickups := #[]
    doorOpen := 1.0
  }
  let openedCache := update cacheState secretInput noInput 0.1
  let heldCache := update openedCache secretInput secretInput 0.1
  if !openedCache.cacheFound || openedCache.cacheDoorOpen <= 0.0 ||
      openedCache.secretFlash == 0 || openedCache.score != 500 || heldCache.score != 500 then
    throw (IO.userError "Secret chamber discovery smoke test failed")
  if !victory cacheState then
    throw (IO.userError "Optional secret encounter incorrectly gated the exit")
  let sleeping : Enemy := { position := ⟨0.0, 0.0, 1.1⟩, health := 3, kind := 0 }
  let (behindDoor, _, _) := updateEnemy initialState.camera 0 0.0 1.0 false 0.1 sleeping
  if behindDoor.alerted then throw (IO.userError "Closed door leaked monster sight")
  let (heard, _, _) := updateEnemy initialState.camera 0 0.0 1.0 true 0.1 sleeping
  if !heard.alerted then throw (IO.userError "Nearby gunshot did not alert monster")
  if !blockedAt 0 0.0 1.0 0.0 0.6 || blockedAt 0 1.0 1.0 0.0 0.6 then
    throw (IO.userError "Dynamic door collision smoke test failed")
  let switchCamera : Camera := { initialState.camera with position := ⟨0.0, 1.6, -0.5⟩ }
  if updateDoor switchCamera true false 0.0 0.5 > 0.0 then
    throw (IO.userError "Key-locked door opened without the red key")
  if updateDoor switchCamera true true 0.0 0.5 <= 0.0 then
    throw (IO.userError "Door interaction smoke test failed")
  let lockedAttempt := update { initialState with camera := switchCamera }
    { noInput with use := true } noInput 0.1
  if lockedAttempt.doorOpen > 0.0 || lockedAttempt.keyFlash == 0 then
    throw (IO.userError "Locked-door feedback smoke test failed")
  let deadEnemies := initialState.enemies.map fun enemy => { enemy with health := 0 }
  let exitState := { initialState with
    camera := { initialState.camera with position := ⟨0.0, 1.6, 6.8⟩ }
    enemies := deadEnemies
    doorOpen := 1.0
  }
  let completedState := update exitState noInput noInput 0.1
  if !completedState.levelComplete then
    throw (IO.userError "Level exit smoke test failed")
  if !blockedAt 1 1.0 1.0 0.0 (-2.5) || blockedAt 1 1.0 1.0 4.0 (-2.5) ||
      !blockedAt 1 1.0 1.0 4.0 1.0 || blockedAt 1 1.0 1.0 (-4.0) 1.0 ||
      !blockedAt 1 1.0 1.0 0.0 4.2 || blockedAt 1 1.0 1.0 4.0 4.2 then
    throw (IO.userError "Map 2 alternating bulkhead collision smoke test failed")
  let carried := advanceLevel { completedState with
    health := 63
    ammo := 14
    bullets := 22
    hasChaingun := true
    weapon := 1
    score := 2400
  }
  if carried.level != 1 || carried.health != 88 || carried.ammo != 26 ||
      carried.bullets != 47 || !carried.hasChaingun || carried.weapon != 1 ||
      carried.score != 2400 || carried.enemies.size != 8 then
    throw (IO.userError "Campaign transition/inventory carry smoke test failed")
  let mapTwoDead := levelTwoBase.enemies.map fun enemy => { enemy with health := 0 }
  let mapTwoExit := { levelTwoBase with
    camera := { levelTwoBase.camera with position := ⟨6.35, 1.6, 6.45⟩ }
    enemies := mapTwoDead
  }
  let mapTwoComplete := update mapTwoExit noInput noInput 0.01
  if !mapTwoComplete.levelComplete then
    throw (IO.userError "Map 2 campaign exit smoke test failed")
  let mapTwoPixels := render { levelTwoBase with mapOpen := true }
  if mapTwoPixels.size != pixelCount then
    throw (IO.userError "Map 2 automap render smoke test failed")
  let intermissionPixels := render { completedState with
    playTime := 83.0
    shotsFired := 10
    shotsHit := 7
    killsMade := 6
    secretFound := true
    cacheFound := true
  }
  if intermissionPixels[19 * renderWidth + 7]? != some (packedColor ⟨11, 13, 18⟩) then
    throw (IO.userError "Intermission render smoke test failed")
  if withWindow then
    let opened ← createWindow 960 540 false
    if !opened then throw (IO.userError "Hidden window creation failed")
    let running ← present pixels (UInt32.ofNat renderWidth) (UInt32.ofNat renderHeight)
    closeWindow
    if !running then throw (IO.userError "Hidden framebuffer presentation failed")
  IO.println s!"3D smoke test passed ({pixelCount * 4} bytes, {renderEnd - renderStart} ms)"

def writePixels (path : System.FilePath) (pixels : Array UInt32) : IO Unit := do
  let mut bytes := s!"P6\n{renderWidth} {renderHeight}\n255\n".toUTF8
  for pixel in pixels do
    let value := pixel.toNat
    bytes := bytes.push (UInt8.ofNat ((value / 65536) % 256))
    bytes := bytes.push (UInt8.ofNat ((value / 256) % 256))
    bytes := bytes.push (UInt8.ofNat (value % 256))
  IO.FS.writeBinFile path bytes
  IO.println s!"Wrote {path}"

def previewBurst (origin : Vec3) (kind frame start count : Nat) : Array Particle :=
  if frame < start then #[]
  else updateParticles 0 1.0 1.0 (Float.ofNat (frame - start) * 0.14)
    (spawnBurst origin kind count)

def promoState (frame : Nat) : GameState :=
  let firing := frame == 2 || frame == 5
  let flash := if firing then 3 else if frame == 3 || frame == 6 then 2 else 0
  let monsterHealth := if frame >= 5 then 0 else if frame >= 2 then 1 else 3
  let painTime := if frame == 2 then 0.16 else if frame == 3 then 0.06 else 0.0
  let deathTime := if frame == 5 then 0.62 else if frame == 6 then 0.38
    else if frame == 7 then 0.12 else 0.0
  let particles := previewBurst ⟨0.0, 1.08, 0.02⟩ 0 frame 2 8 ++
    previewBurst ⟨0.0, 1.00, 0.08⟩ 0 frame 5 10
  { initialState with
    camera := { position := ⟨0.0, 1.6, -4.8⟩, yaw := 0.0, pitch := 0.0 }
    enemies := #[{
      position := ⟨0.0, 0.0, 0.2⟩
      health := monsterHealth
      phase := Float.ofNat frame * 0.42
      kind := 1
      alerted := true
      painTime
      deathTime
    }]
    ammo := 8 - (if frame >= 5 then 4 else if frame >= 2 then 2 else 0)
    muzzleFlash := flash
    particles
    marks := if frame >= 5 then #[{ position := ⟨0.0, 0.0, 0.2⟩, kind := 1 }] else #[]
  }

def writeScreenshot (path : System.FilePath) : IO Unit :=
  writePixels path (render (promoState 2))

def writeLevelScreenshot : IO Unit :=
  let preview := { initialState with
    camera := { position := ⟨0.0, 1.6, -2.15⟩, yaw := 0.0, pitch := 0.0 }
    doorOpen := 0.48
    hasRedKey := true
    muzzleFlash := 0
  }
  writePixels "lean64-level.ppm" (render preview)

def writeMapScreenshot : IO Unit :=
  let contacts := initialState.enemies.map fun enemy =>
    { enemy with alerted := enemy.position.z < 1.5 || enemy.kind == 3 }
  let preview := { initialState with
    camera := { position := ⟨0.0, 1.6, -2.4⟩, yaw := 0.35, pitch := 0.0 }
    enemies := contacts
    doorOpen := 0.58
    hasRedKey := true
    mapOpen := true
    cacheFound := true
    cacheDoorOpen := 0.62
  }
  writePixels "lean64-map.ppm" (render preview)

def writeSecretScreenshot : IO Unit :=
  let preview := { initialState with
    camera := { position := ⟨-5.35, 1.6, -4.36⟩, yaw := -1.57, pitch := 0.0 }
    secretFound := true
    secretFlash := 84
    ammo := 76
    bullets := 60
  }
  writePixels "lean64-secret.ppm" (render preview)

def shotgunCycleState (frame : Nat) : GameState :=
  let cooldown := if frame == 1 then 0.82 else if frame == 2 then 0.72
    else if frame == 3 then 0.62 else if frame == 4 then 0.50
    else if frame == 5 then 0.40 else if frame == 6 then 0.28
    else if frame == 7 then 0.17 else if frame == 8 then 0.05 else 0.0
  let flash := if frame == 1 then 3 else if frame == 2 then 2 else 0
  let dead := frame >= 2
  let deathTime := if frame == 2 then 0.62 else if frame == 3 then 0.48
    else if frame == 4 then 0.34 else if frame == 5 then 0.20 else if dead then 0.08 else 0.0
  { initialState with
    camera := { position := ⟨0.0, 1.6, -4.8⟩, yaw := 0.0, pitch := 0.0 }
    enemies := #[
      { position := ⟨-0.75, 0.0, 0.2⟩, health := if dead then 0 else 1
        phase := Float.ofNat frame * 0.28, kind := 0, alerted := true, deathTime },
      { position := ⟨0.75, 0.0, 0.2⟩, health := if dead then 0 else 1
        phase := Float.ofNat frame * 0.31, kind := 1, alerted := true, deathTime }
    ]
    barrels := #[]
    pickups := #[]
    ammo := if frame == 0 then 8 else 6
    muzzleFlash := flash
    weaponCooldown := cooldown
    recoilKick := if frame == 1 then 1.0 else if frame == 2 then 0.72
      else if frame == 3 then 0.38 else 0.0
    playTime := 3.0
    particles := previewBurst ⟨-0.75, 1.08, 0.02⟩ 0 frame 1 8 ++
      previewBurst ⟨0.75, 1.08, 0.02⟩ 0 frame 1 8
    marks := if dead then #[
      { position := ⟨-0.75, 0.04, 0.2⟩, kind := 1 },
      { position := ⟨0.75, 0.04, 0.2⟩, kind := 1 }
    ] else #[]
  }

def writePromoFrames : IO Unit := do
  for frame in [0:10] do
    let path : System.FilePath := s!"lean64-x-{frame}.ppm"
    writePixels path (render (shotgunCycleState frame))

def chaingunPromoState (frame : Nat) : GameState :=
  let firing := frame >= 2 && frame <= 5
  { initialState with
    camera := { position := ⟨0.0, 1.6, -4.8⟩, yaw := 0.0, pitch := 0.0 }
    enemies := #[{
      position := ⟨0.0, 0.0, 0.2⟩
      health := if frame >= 4 then 1 else 3
      phase := Float.ofNat frame * 0.55
      kind := 0
      alerted := true
      painTime := if frame == 4 then 0.14 else 0.0
    }]
    weapon := 1
    hasChaingun := true
    bullets := 84 - frame
    muzzleFlash := if firing then 2 else 0
    doorOpen := 1.0
    particles := previewBurst ⟨0.0, 1.05, 0.02⟩ 0 frame 4 9
  }

def writeChaingunFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-chain-{frame}.ppm"
    writePixels path (render (chaingunPromoState frame))

def barrelPromoState (frame : Nat) : GameState :=
  let blastTime := if frame == 2 then 0.28 else if frame == 3 then 0.22
    else if frame == 4 then 0.14 else if frame == 5 then 0.06 else 0.0
  let enemyDead := frame >= 4
  let deathTime := if frame == 4 then 0.62 else if frame == 5 then 0.40
    else if frame == 6 then 0.16 else 0.0
  let particles := previewBurst ⟨0.0, 0.72, -1.05⟩ 1 frame 2 10 ++
    previewBurst ⟨0.0, 0.58, -1.05⟩ 2 frame 4 12
  { initialState with
    camera := { position := ⟨0.0, 1.6, -5.35⟩, yaw := 0.0, pitch := -0.06 }
    enemies := #[{
      position := ⟨1.25, 0.0, -0.15⟩
      health := if enemyDead then 0 else 3
      kind := 1
      alerted := true
      attackWindup := if frame == 0 then 0.32 else if frame == 1 then 0.18 else 0.0
      deathTime
    }]
    barrels := #[{
      position := ⟨0.0, 0.0, -1.05⟩
      health := if frame >= 2 then 0 else 1
      blastTime
    }]
    ammo := if frame >= 2 then 6 else 8
    muzzleFlash := if frame == 2 then 3 else if frame == 3 then 1 else 0
    doorOpen := 1.0
    particles
    marks := if frame >= 4 then #[{ position := ⟨1.25, 0.0, -0.15⟩, kind := 1 }] else #[]
  }

def writeBarrelFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-barrel-{frame}.ppm"
    writePixels path (render (barrelPromoState frame))

def keyPromoState (frame : Nat) : GameState :=
  if frame < 3 then
    let collected := frame == 2
    let cameraX := 3.5 + Float.ofNat frame * 0.55
    let previewCamera : Camera := {
      position := ⟨cameraX, 1.25, -5.80⟩
      yaw := 1.57
      pitch := -0.24
    }
    { initialState with
      camera := previewCamera
      enemies := #[{ position := ⟨-6.0, 0.0, 6.5⟩, health := 3 }]
      barrels := #[]
      pickups := #[{ position := ⟨5.75, 0.0, -5.25⟩, kind := 3, active := !collected }]
      hasRedKey := collected
      keyFlash := if collected then 90 else 0
    }
  else
    let doorAmount := if frame == 5 then 0.34 else if frame == 6 then 0.72
      else if frame >= 7 then 1.0 else 0.0
    { initialState with
      camera := { position := ⟨0.0, 1.6, -1.55⟩, yaw := 0.0, pitch := 0.0 }
      enemies := #[{ position := ⟨-6.0, 0.0, 6.5⟩, health := 3 }]
      barrels := #[]
      pickups := #[]
      hasRedKey := true
      keyFlash := if frame == 3 then 36 else 0
      doorOpen := doorAmount
    }

def writeKeyFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-key-{frame}.ppm"
    writePixels path (render (keyPromoState frame))

def cachePromoState (frame : Nat) : GameState :=
  let found := frame >= 1
  let openAmount := if frame == 1 then 0.12 else if frame == 2 then 0.42
    else if frame == 3 then 0.74 else if frame >= 4 then 1.0 else 0.0
  let dead := frame >= 6
  { initialState with
    camera := { position := ⟨2.90, 1.6, 1.18⟩, yaw := 0.0, pitch := -0.05 }
    enemies := #[
      {
        position := ⟨2.90, 0.0, 2.52⟩
        health := if dead then 0 else if frame == 5 then 1 else 3
        kind := 1
        alerted := frame >= 4
        painTime := if frame == 5 then 0.14 else 0.0
        deathTime := if frame == 6 then 0.52 else if frame == 7 then 0.12 else 0.0
        countsForExit := false
      },
      { position := ⟨-6.0, 0.0, 6.5⟩, health := 3 }
    ]
    barrels := #[]
    pickups := #[
      { position := ⟨2.65, 0.0, 2.52⟩, kind := 0 },
      { position := ⟨3.25, 0.0, 2.52⟩, kind := 1 }
    ]
    hasRedKey := true
    doorOpen := 1.0
    cacheFound := found
    cacheDoorOpen := openAmount
    secretFlash := if frame == 1 then 88 else 0
    muzzleFlash := if frame == 5 then 3 else if frame == 6 then 1 else 0
    ammo := if frame >= 5 then 10 else 12
    particles := previewBurst ⟨2.90, 1.05, 2.34⟩ 0 frame 5 9
    marks := if frame >= 6 then #[{ position := ⟨2.90, 0.0, 2.52⟩, kind := 1 }] else #[]
  }

def writeCacheFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-cache-{frame}.ppm"
    writePixels path (render (cachePromoState frame))

def bossPromoState (frame : Nat) : GameState :=
  let dead := frame >= 8
  let health := if dead then 0 else if frame >= 7 then 2 else if frame >= 5 then 4
    else if frame >= 4 then 6 else 8
  let pain := frame == 4 || frame == 5 || frame == 7
  let projectile : Array Projectile := if frame == 3 then #[{
    position := ⟨1.10, 1.35, 4.85⟩
    velocity := ⟨0.0, 0.0, 0.0⟩
    life := 2.0
    damage := 18
  }] else #[]
  let particles := if frame >= 8 then previewBurst ⟨0.0, 1.35, 6.00⟩ 0 frame 8 14
    else if frame >= 7 then previewBurst ⟨0.0, 1.45, 6.00⟩ 0 frame 7 12
    else if frame >= 5 then previewBurst ⟨0.0, 1.45, 6.00⟩ 0 frame 5 11
    else previewBurst ⟨0.0, 1.45, 6.00⟩ 0 frame 4 11
  { initialState with
    camera := { position := ⟨2.10, 1.6, 3.55⟩, yaw := -0.68, pitch := -0.04 }
    enemies := #[{
      position := ⟨0.0, 0.0, 6.20⟩
      health
      kind := 3
      alerted := frame >= 1
      painTime := if pain then 0.14 else 0.0
      attackWindup := if frame == 1 then 0.28 else if frame == 2 then 0.10
        else if frame == 6 then 0.22 else 0.0
      deathTime := if frame == 8 then 0.62 else if frame == 9 then 0.12 else 0.0
    }]
    barrels := #[]
    pickups := #[]
    projectiles := projectile
    hasRedKey := true
    doorOpen := 1.0
    cacheFound := true
    cacheDoorOpen := 1.0
    muzzleFlash := if frame == 4 || frame == 5 || frame == 7 || frame == 8 then 3 else 0
    ammo := 20 - (min 8 frame)
    particles
    marks := if frame >= 8 then #[{ position := ⟨0.0, 0.0, 6.20⟩, kind := 1 }] else #[]
  }

def writeBossFrames : IO Unit := do
  for frame in [0:10] do
    let path : System.FilePath := s!"lean64-boss-{frame}.ppm"
    writePixels path (render (bossPromoState frame))

def impactPromoState (frame : Nat) : GameState :=
  let first : ImpactMark := { position := ⟨-0.28, 1.48, -7.62⟩, kind := 0 }
  let second : ImpactMark := { position := ⟨0.18, 1.72, -7.62⟩, kind := 0 }
  let third : ImpactMark := { position := ⟨0.42, 1.30, -7.62⟩, kind := 0 }
  let marks := (if frame >= 1 then #[first] else #[]) ++
    (if frame >= 3 then #[second] else #[]) ++ (if frame >= 5 then #[third] else #[])
  let particles := previewBurst ⟨-0.28, 1.48, -7.30⟩ 1 frame 1 7 ++
    previewBurst ⟨0.18, 1.72, -7.30⟩ 1 frame 3 7 ++
    previewBurst ⟨0.42, 1.30, -7.30⟩ 1 frame 5 7
  { initialState with
    camera := { position := ⟨0.0, 1.6, -5.65⟩, yaw := 3.14159, pitch := 0.0 }
    enemies := #[{ position := ⟨-6.0, 0.0, 6.5⟩, health := 3 }]
    barrels := #[]
    pickups := #[]
    marks
    particles
    muzzleFlash := if frame == 1 || frame == 3 || frame == 5 then 3 else 0
    ammo := 12 - min 6 frame
  }

def writeImpactFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-impact-{frame}.ppm"
    writePixels path (render (impactPromoState frame))

def writeTitleScreenshot : IO Unit :=
  writePixels "lean64-title.ppm" (render { initialState with started := false })

def writeDifficultyFrames : IO Unit := do
  for difficulty in [0:3] do
    let path : System.FilePath := s!"lean64-difficulty-{difficulty}.ppm"
    writePixels path (render { initialState with started := false, difficulty := difficulty })

def writePauseScreenshot : IO Unit :=
  let preview := { bossPromoState 2 with paused := true }
  writePixels "lean64-pause.ppm" (render preview)

def writeIntermissionScreenshot : IO Unit :=
  let preview := { initialState with
    levelComplete := true
    playTime := 83.0
    shotsFired := 37
    shotsHit := 29
    killsMade := 7
    secretFound := true
    cacheFound := true
    score := 2845
  }
  writePixels "lean64-intermission.ppm" (render preview)

def mapTwoPreview : GameState :=
  { levelTwoBase with
    camera := { position := ⟨-5.65, 1.6, -5.75⟩, yaw := 1.18, pitch := -0.02 }
    enemies := levelTwoBase.enemies.map fun enemy =>
      { enemy with alerted := true }
    hasChaingun := true
    weapon := 0
    ammo := 34
    bullets := 70
    muzzleFlash := 3
  }

def writeMapTwoScreenshot : IO Unit :=
  writePixels "lean64-map2.ppm" (render mapTwoPreview)

def writeMapTwoAutomap : IO Unit :=
  writePixels "lean64-map2-automap.ppm" (render { mapTwoPreview with mapOpen := true, muzzleFlash := 0 })

def rushPromoState (frame : Nat) : GameState :=
  let distance := Float.ofNat (min 6 frame) * 0.28
  let yaw := 1.18 + Float.ofNat frame * 0.045
  let cameraPosition : Vec3 := ⟨-5.65 + 0.9246 * distance, 1.6,
    -5.75 + 0.3809 * distance⟩
  let fired := frame >= 6
  let enemies := levelTwoBase.enemies.toList.zipIdx.map (fun (enemy, index) =>
    if index == 0 then
      { enemy with
        health := if frame >= 7 then 0 else 3
        alerted := true
        painTime := if frame == 6 then 0.14 else 0.0
        deathTime := if frame == 7 then 0.62 else 0.0 }
    else { enemy with alerted := false }) |>.toArray
  { mapTwoPreview with
    camera := { position := cameraPosition, yaw := yaw, pitch := -0.02 }
    enemies
    bobPhase := Float.ofNat frame * 1.15
    bobStrength := if fired then 0.45 else 1.0
    recoilKick := if frame == 6 then 1.0 else if frame == 7 then 0.65 else 0.0
    muzzleFlash := if frame == 6 then 3 else if frame == 7 then 1 else 0
    weaponCooldown := if frame == 6 then 0.82 else if frame == 7 then 0.64 else 0.0
    ammo := if fired then 32 else 34
    playTime := 3.0
    particles := previewBurst ⟨-2.5, 1.05, -5.0⟩ 0 frame 6 12
    marks := if frame >= 7 then #[{ position := ⟨-2.5, 0.04, -5.0⟩, kind := 1 }] else #[]
  }

def writeRushFrames : IO Unit := do
  for frame in [0:8] do
    let path : System.FilePath := s!"lean64-rush-{frame}.ppm"
    writePixels path (render (rushPromoState frame))

def campaignPromoState (frame : Nat) : GameState :=
  if frame < 2 then
    { initialState with
      levelComplete := true
      playTime := 83.0
      shotsFired := 37
      shotsHit := 29
      killsMade := 7
      secretFound := true
      cacheFound := true
      score := 2845
    }
  else
    let action := frame - 2
    let enemies := levelTwoBase.enemies.toList.zipIdx.map (fun (enemy, index) =>
      if index == 0 then
        { enemy with
          health := if action >= 2 then 1 else 3
          alerted := true
          painTime := if action == 2 then 0.14 else 0.0
          deathTime := 0.0 }
      else { enemy with alerted := index < 3 }) |>.toArray
    let cooldown := if action == 1 then 0.82 else if action == 2 then 0.64
      else if action == 3 then 0.50 else if action == 4 then 0.38
      else if action == 5 then 0.26 else if action == 6 then 0.12 else 0.0
    { mapTwoPreview with
      enemies
      muzzleFlash := if action == 1 then 3 else if action == 2 then 1 else 0
      weaponCooldown := cooldown
      ammo := if action == 0 then 34 else 32
      playTime := Float.ofNat action * 0.55
      particles := previewBurst ⟨-2.5, 1.05, -5.0⟩ 0 action 1 10
      marks := #[]
    }

def writeCampaignFrames : IO Unit := do
  for frame in [0:9] do
    let path : System.FilePath := s!"lean64-campaign-{frame}.ppm"
    writePixels path (render (campaignPromoState frame))

def audioDemo : IO Unit := do
  IO.println "Playing Lean 64 synthesized cue bank..."
  for cue in [1:14] do
    IO.println s!"cue {cue}"
    playCue (UInt32.ofNat cue)
    IO.sleep 900

def trailerState (frame : Nat) : GameState :=
  let phase := frame % 840
  if phase < 240 then
    let travel := min 1.0 (Float.ofNat phase / 145.0)
    let distance := travel * 1.68
    let secondShot := phase >= 202
    let shotAge := if secondShot then phase - 202 else if phase >= 145 then phase - 145 else 999
    let base := rushPromoState 0
    let enemies := base.enemies.toList.zipIdx.map (fun (enemy, index) =>
      if index == 0 then { enemy with
        health := if secondShot && shotAge >= 4 then 0 else if phase >= 149 then 1 else 3
        alerted := true
        painTime := if shotAge < 5 then 0.14 else 0.0
        deathTime := if secondShot && shotAge >= 4 && shotAge < 42 then
          max 0.08 (0.62 - Float.ofNat (shotAge - 4) / 62.0) else 0.0 }
      else { enemy with alerted := index < 3 }) |>.toArray
    { base with
      camera := { position := ⟨-5.65 + 0.9246 * distance, 1.6,
        -5.75 + 0.3809 * distance⟩, yaw := 1.18 + travel * 0.28, pitch := -0.02 }
      enemies
      bobPhase := Float.ofNat phase * 0.13
      bobStrength := if shotAge < 14 then 0.25 else 1.0
      recoilKick := if shotAge < 2 then 1.0 else if shotAge < 5 then 0.65
        else if shotAge < 10 then 0.3 else 0.0
      muzzleFlash := if shotAge < 3 then 3 else if shotAge < 6 then 2 else 0
      ammo := if secondShot then 30 else if phase >= 145 then 32 else 34
      playTime := 6.0
      particles := if shotAge < 50 then
        updateParticles 0 1.0 1.0 (Float.ofNat shotAge / 60.0)
          (spawnBurst ⟨-2.5, 1.05, -5.0⟩ 0 18) else #[] }
  else if phase < 390 then
    let segmentFrame := phase - 240
    let action := min 7 (segmentFrame / 18)
    let base := chaingunPromoState action
    let firing := segmentFrame >= 18 && segmentFrame < 132
    { base with
      camera := { base.camera with yaw := (Float.ofNat (segmentFrame % 60) - 30.0) * 0.0015 }
      muzzleFlash := if firing && (segmentFrame / 3) % 2 == 0 then 3 else 0
      bullets := 96 - min 70 (segmentFrame / 2)
      recoilKick := if firing && segmentFrame % 6 < 3 then 0.22 else 0.0
      bobPhase := Float.ofNat segmentFrame * 0.17
      playTime := 7.0 }
  else if phase < 540 then
    let segmentFrame := phase - 390
    let action := if segmentFrame < 36 then 0 else if segmentFrame < 48 then 1
      else min 7 (2 + (segmentFrame - 48) / 16)
    let base := barrelPromoState action
    { base with
      camera := { base.camera with yaw := (Float.ofNat (segmentFrame % 50) - 25.0) * 0.001 }
      muzzleFlash := if segmentFrame >= 38 && segmentFrame < 44 then 3 else 0
      recoilKick := if segmentFrame >= 38 && segmentFrame < 45 then 0.8 else 0.0
      playTime := 8.0 }
  else
    let segmentFrame := phase - 540
    let action := min 9 (segmentFrame / 28)
    let base := bossPromoState action
    { base with
      camera := { base.camera with yaw := base.camera.yaw +
        (Float.ofNat (segmentFrame % 80) - 40.0) * 0.0008 }
      muzzleFlash := if (segmentFrame >= 104 && segmentFrame < 112) ||
        (segmentFrame >= 160 && segmentFrame < 168) || (segmentFrame >= 216 && segmentFrame < 224) then 3
        else base.muzzleFlash
      recoilKick := if segmentFrame % 56 < 7 && segmentFrame >= 104 then 0.72 else 0.0
      playTime := 9.0 }

def trailerAudio (phase : Nat) : IO Unit := do
  if phase == 0 || phase == 390 then playCue 1
  else if phase == 145 || phase == 202 || phase == 428 || phase == 644 ||
      phase == 700 || phase == 756 then playShot
  else if phase == 240 then playCue 8
  else if phase == 262 || phase == 286 || phase == 310 || phase == 334 || phase == 358 then
    playChaingun
  else if phase == 438 then playCue 9
  else if phase == 540 then playCue 10
  else if phase == 612 then playCue 13
  else if phase == 796 then playCue 11

partial def engagementDemoLoop (frame lastFrame : Nat) : IO Unit := do
  let phase := frame % 300
  let sourceFrame := if phase < 80 then 90 + phase * 2
    else if phase < 150 then 240 + (phase - 80) * 2
    else if phase < 220 then 390 + (phase - 150) * 2
    else 540 + (phase - 220) * 3
  if phase == 24 || phase == 56 || phase == 174 || phase == 258 then playShot
  else if phase == 86 || phase == 101 || phase == 116 || phase == 131 then playChaingun
  else if phase == 181 then playCue 9
  else if phase == 220 then playCue 10
  else if phase == 240 then playCue 13
  else if phase == 288 then playCue 11
  let running ← presentGpuState (trailerState sourceFrame)
  if running then
    let now ← IO.monoMsNow
    let target := lastFrame + 16
    if now < target then IO.sleep (UInt32.ofNat (target - now))
    engagementDemoLoop (frame + 1) (max target now)
  else closeWindow

def runEngagementDemo : IO Unit := do
  let opened ← createWindow 1280 720 true
  if !opened then throw (IO.userError "Could not create engagement demo window")
  let start ← IO.monoMsNow
  engagementDemoLoop 0 start

def benchmarkRender : IO Unit := do
  let frameCount := 240
  let start ← IO.monoMsNow
  let mut checksum := 0
  for frame in [0:frameCount] do
    let pixels := render (rushPromoState (frame % 8))
    checksum := checksum + pixels[(frame * 97) % pixels.size]!.toNat
  let elapsed := max 1 ((← IO.monoMsNow) - start)
  let fps := frameCount * 1000 / elapsed
  IO.println s!"Rendered {frameCount} frames in {elapsed} ms ({fps} FPS, checksum {checksum % 1000003})"

def benchmarkGpu : IO Unit := do
  let opened ← createWindow 1280 720 false
  if !opened then throw (IO.userError "Could not create GPU benchmark window")
  let frameCount := 240
  let start ← IO.monoMsNow
  let mut running := true
  for frame in [0:frameCount] do
    if running then running ← presentGpuState (rushPromoState (frame % 8))
  let elapsed := max 1 ((← IO.monoMsNow) - start)
  closeWindow
  let fps := frameCount * 1000 / elapsed
  IO.println s!"Submitted {frameCount} GPU frames in {elapsed} ms ({fps} FPS)"

def debugGpuData : IO Unit := do
  let state := configureDifficulty { initialState with started := true } 1
  let scene := gpuSceneData state
  let hud := gpuOverlay state
  let visibleHud := hud.foldl (fun count pixel =>
    if pixel.toNat / 16777216 > 0 then count + 1 else count) 0
  IO.println s!"GPU scene words: {scene.size}, triangles: {scene.size / 11}"
  IO.println s!"HUD pixels: {hud.size}, visible: {visibleHud}"
  if scene.size >= 11 then
    IO.println s!"First vertex bits: {scene[0]!}, {scene[1]!}, {scene[2]!}; color: {scene[9]!}"

def cliMain (args : List String) : IO Unit := do
  if args.contains "--smoke-test" then smokeTest false
  else if args.contains "--benchmark" then benchmarkRender
  else if args.contains "--gpu-benchmark" then benchmarkGpu
  else if args.contains "--gpu-debug" then debugGpuData
  else if args.contains "--window-smoke" then smokeTest true
  else if args.contains "--promo-frames" then writePromoFrames
  else if args.contains "--chaingun-frames" then writeChaingunFrames
  else if args.contains "--barrel-frames" then writeBarrelFrames
  else if args.contains "--key-frames" then writeKeyFrames
  else if args.contains "--cache-frames" then writeCacheFrames
  else if args.contains "--boss-frames" then writeBossFrames
  else if args.contains "--impact-frames" then writeImpactFrames
  else if args.contains "--title-screenshot" then writeTitleScreenshot
  else if args.contains "--difficulty-frames" then writeDifficultyFrames
  else if args.contains "--pause-screenshot" then writePauseScreenshot
  else if args.contains "--intermission-screenshot" then writeIntermissionScreenshot
  else if args.contains "--map2-screenshot" then writeMapTwoScreenshot
  else if args.contains "--map2-automap" then writeMapTwoAutomap
  else if args.contains "--rush-frames" then writeRushFrames
  else if args.contains "--campaign-frames" then writeCampaignFrames
  else if args.contains "--audio-demo" then audioDemo
  else if args.contains "--level-screenshot" then writeLevelScreenshot
  else if args.contains "--map-screenshot" then writeMapScreenshot
  else if args.contains "--secret-screenshot" then writeSecretScreenshot
  else if args.contains "--screenshot" then writeScreenshot "lean64.ppm"
  else runGame true

end Lean64

def runLean64 (args : List String) : IO Unit := Lean64.cliMain args