Native Metal replay (Experiment 2 Phase A/B)

Falsification test of the post-mortem's C2 ("the E2B gap is the dispatch layer, not the kernels"), in two phases:

• Phase A (timing): capture every dispatch of ONE decode token — Tint-CLI MSL, the Dawn buffers in MSL binding order, grid/workgroup dims, threadgroup bytes — then replay the token natively (replayRun): Serial 6.78 ms ≈ Dawn's 7.7 ms, Concurrent no-barrier 3.43 ms, per-layer barriers 3.92 ms (M4 Max, identical kernels).

• Phase B (real execution): mode := .nativeExec makes the executeShaderNamed hook SKIP the Dawn dispatch entirely; the token's ops are recorded and then executed ONCE by commitToken on Dawn's own MTLCommandQueue (single-queue FIFO keeps ordering with Dawn staging writes and readbacks) with mode-3 automatic hazard barriers (llama.cpp ggml_mem_ranges-style, whole-buffer granularity). Correctness is gated on the generated text.

MSL comes from running the tint CLI (HESPER_TINT_BIN, same Tint version as the pinned Dawn) on the exact WGSL we hand Dawn; the CLI assigns its own [[buffer(i)]] indices and may RENAME the entry point (main → v), so both are parsed from the MSL. Steady state is served from a cache keyed by the caller's authoritative cacheKey, so the per-dispatch host cost is a HashMap probe + buffer-pointer pushes — no WGSL regeneration.

inductive Hesper.WGSL.NativeReplay.Mode : Type

• off : Mode
• capture : Mode

  Record ops AND still execute them through Dawn (Phase A timing capture).

• nativeExec : Mode

  Record ops and SKIP the Dawn dispatch; commitToken executes them natively.

• frozen : Mode

  FROZEN token replay (CUDA-Graphs analogue): the dispatch sequence recorded by an earlier nativeExec token is token-invariant from cacheLen ≥ 8 (identical buffers, grids; positions live in params-buffer CONTENT), so subsequent tokens skip both the Dawn dispatch AND the re-record — the hook returns immediately and commitToken (reset := false) re-executes the frozen list. Kills the per-token host record cost. Correctness gate: token sequence must equal the Dawn path.

def Hesper.WGSL.NativeReplay.instBEqMode.beq : Mode → Mode → Bool

Equations

• Hesper.WGSL.NativeReplay.instBEqMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Hesper.WGSL.NativeReplay.instBEqMode : BEq Mode

Equations

• Hesper.WGSL.NativeReplay.instBEqMode = { beq := Hesper.WGSL.NativeReplay.instBEqMode.beq }

def Hesper.WGSL.NativeReplay.instInhabitedMode.default : Mode

Equations

• Hesper.WGSL.NativeReplay.instInhabitedMode.default = Hesper.WGSL.NativeReplay.Mode.off

instance Hesper.WGSL.NativeReplay.instInhabitedMode : Inhabited Mode

Equations

• Hesper.WGSL.NativeReplay.instInhabitedMode = { default := Hesper.WGSL.NativeReplay.instInhabitedMode.default }

opaque Hesper.WGSL.NativeReplay.modeRef : IO.Ref Mode

opaque Hesper.WGSL.NativeReplay.recordedRef : IO.Ref Nat

opaque Hesper.WGSL.NativeReplay.missesRef : IO.Ref (List String)

opaque Hesper.WGSL.NativeReplay.namesRef : IO.Ref (Array String)

Kernel name per recorded dispatch, in record order (drives per-class profiling).

structure Hesper.WGSL.NativeReplay.CacheEntry : Type

• msl : String
• mslEntry : String

  Actual MSL entry name (Tint may rename, e.g. main → v). Empty = unusable.

• order : Array String

  Buffer names in MSL [[buffer(i)]] order.

• tgBytes : UInt32

  Threadgroup bytes to bind at index 0 (0 = kernel has no threadgroup param).

• writeMask : UInt32

  Bit i set ⇒ order[i] is a read_write binding (drives mode-3 hazard barriers).

• perm : Array Nat

  perm[i] = position of order[i] in the call site's namedBuffers list (captured at build time). Steady-state emit indexes instead of string-searching; a name mismatch (different call-site ordering under the same key) falls back to find.

opaque Hesper.WGSL.NativeReplay.cacheRef : IO.Ref (Std.HashMap UInt64 CacheEntry)

Keyed by the caller's authoritative cacheKey (or hash of the WGSL when unkeyed).

def Hesper.WGSL.NativeReplay.currentMode : IO Mode

Equations

• Hesper.WGSL.NativeReplay.currentMode = ST.Ref.get Hesper.WGSL.NativeReplay.modeRef

def Hesper.WGSL.NativeReplay.isActive : IO Bool

Equations

• Hesper.WGSL.NativeReplay.isActive = do let __do_lift ← ST.Ref.get Hesper.WGSL.NativeReplay.modeRef pure (__do_lift != Hesper.WGSL.NativeReplay.Mode.off)

def Hesper.WGSL.NativeReplay.startCapture : IO Unit

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.stopCapture : IO (Nat × List String)

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.beginNativeToken : IO Unit

Phase B: begin recording a token that will NOT be dispatched through Dawn.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.beginFrozenToken : IO Unit

Frozen-mode token: the hook drops every dispatch instantly; the previously recorded list is re-executed by commitToken.

Equations

• Hesper.WGSL.NativeReplay.beginFrozenToken = ST.Ref.set Hesper.WGSL.NativeReplay.modeRef Hesper.WGSL.NativeReplay.Mode.frozen

def Hesper.WGSL.NativeReplay.commitToken (mode : UInt32 := 3) : IO String

Phase B: execute the recorded token natively (mode 3 = concurrent + hazard barriers by default) and drop back to normal Dawn dispatching. Throws if any dispatch was missed (a partial token would silently corrupt the decode).

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.layerBarrier : IO Unit

Layer-boundary marker (honored by replayRun mode=2). No-op unless active.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.sharedBytes (vars : List (String × WGSLType)) : Nat

Total threadgroup-memory upper bound: Tint packs all shared vars into one struct at [[threadgroup(0)]]; over-allocating is harmless, so pad each member to 16.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.tryRecordFast (device : WebGPU.Device) (key : UInt64) (dbgName : String) (namedBuffers : List (String × WebGPU.Buffer)) (numWorkgroups : Nat × Nat × Nat) (wgX wgY wgZ : Nat) : IO Bool

Steady-state record: cache hit on the caller's authoritative key ⇒ record with no WGSL/tint work at all. Returns false on miss (caller falls back to recordSlow).

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.recordSlow (device : WebGPU.Device) (key : UInt64) (wgsl dbgName : String) (namedBuffers : List (String × WebGPU.Buffer)) (writableNames : List String) (tgBytes : Nat) (numWorkgroups : Nat × Nat × Nat) (wgX wgY wgZ : Nat) : IO Unit

Cold-path record: run tint, parse the entry/bindings, compute the write mask from the declared read_write buffer names, cache under key, and record.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.profileClasses (iters : UInt32 := 30) : IO String

DEVPLAN §12: per-kernel-class GPU-time budget of the captured token. Groups the recorded dispatches by kernel name and times each class alone (serial, back-to-back) — an approximation (no inter-class cache interactions) whose sum should land near the whole-token serial time. Returns one line per class, largest first.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.WGSL.NativeReplay.runAll (iters : UInt32 := 20) : IO String

Run the captured token natively in all four timing modes and return a report. Device-free: the MTLDevice was stashed at record time. TIMING ONLY.

Equations

• One or more equations did not get rendered due to their size.