structure Hesper.WebGPU.BufferDescriptor : Type

Buffer descriptor for creating GPU buffers

• size : USize
• usage : List BufferUsage
• mappedAtCreation : Bool

def Hesper.WebGPU.instInhabitedBufferDescriptor.default : BufferDescriptor

Equations

• Hesper.WebGPU.instInhabitedBufferDescriptor.default = { size := default, usage := default, mappedAtCreation := default }

instance Hesper.WebGPU.instInhabitedBufferDescriptor : Inhabited BufferDescriptor

Equations

• Hesper.WebGPU.instInhabitedBufferDescriptor = { default := Hesper.WebGPU.instInhabitedBufferDescriptor.default }

@[extern lean_hesper_buffer_id]

opaque Hesper.WebGPU.getBufferIdEarly (buffer : Buffer) : IO UInt64

Early alias of getBufferId (declared before first use; same FFI symbol).

opaque Hesper.WebGPU.jsTraceRegistryRef : IO.Ref (Std.HashMap UInt64 (Buffer × Nat))

JS-trace registry: uid → (buffer, size). Populated only when DG_TRACE_JS is set (keeps the buffers alive for the post-save dump — acceptable in a trace run).

@[extern lean_hesper_create_buffer]

opaque Hesper.WebGPU.createBufferImpl (device : Device) (desc : BufferDescriptor) : IO Buffer

Create a GPU buffer. Resources are automatically cleaned up by Lean's GC via External finalizers.

def Hesper.WebGPU.createBuffer (device : Device) (desc : BufferDescriptor) : IO Buffer

Wrapper with debug output

Equations

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

@[extern lean_hesper_write_buffer]

opaque Hesper.WebGPU.writeBufferImpl (device : Device) (buffer : Buffer) (offset : USize) (data : ByteArray) : IO Unit

Write data to a buffer from the CPU. @param buffer The target buffer @param offset Offset in bytes @param data Pointer to source data (ByteArray)

def Hesper.WebGPU.writeBuffer (device : Device) (buffer : Buffer) (offset : USize) (data : ByteArray) : IO Unit

writeBuffer with an optional JS-trace hook (DG_TRACE_JS): records small writes (params, canvases) with contents so a replayer can reproduce them.

Equations

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

@[extern lean_hesper_map_buffer_read]

opaque Hesper.WebGPU.mapBufferReadImpl (device : Device) (buffer : Buffer) (offset size : USize) : IO ByteArray

Map a buffer for reading. Returns the mapped data as a ByteArray. @param buffer The buffer to map @param offset Offset in bytes @param size Size in bytes to map

def Hesper.WebGPU.mapBufferRead (device : Device) (buffer : Buffer) (offset size : USize) : IO ByteArray

mapBufferRead with a JS-trace hook: readbacks are the replayer's sync points (logits → CPU commit logic).

Equations

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

@[extern lean_hesper_unmap_buffer]

opaque Hesper.WebGPU.unmapBuffer (buffer : Buffer) : IO Unit

Unmap a previously mapped buffer

@[extern lean_hesper_buffer_id]

opaque Hesper.WebGPU.getBufferId (buffer : Buffer) : IO UInt64

Get a stable unique identifier for a GPU buffer (raw WGPUBuffer handle as UInt64). Used for bind group caching — same ID means same underlying GPU buffer.

@[extern lean_hesper_mtl_buffer_probe]

opaque Hesper.WebGPU.mtlBufferProbe (buffer : Buffer) : IO String

metal_replacer STEP 2: the underlying MTLBuffer of this Dawn buffer (via reinterpret to metal::Buffer

• GetMTLBuffer). Reports its length/storageMode/contents — proves the buffer bridge for dispatching llama.cpp's Metal kernels on our data with no copies. See METAL_REPLACER_INTEGRATION.md.

@[extern lean_hesper_metal_dispatch_mul2]

opaque Hesper.WebGPU.metalDispatchMul2 (device : Device) (inBuf outBuf : Buffer) (n : UInt32) : IO Unit

metal_replacer STEP 3: dispatch a CUSTOM Metal kernel (out[i] = in[i]*2) on our Dawn-backed MTLBuffers. Validates running a hand-written Metal kernel on our data end-to-end. Caller syncs the in write first (a mapBufferRead) and reads out after. See METAL_REPLACER_INTEGRATION.md.

@[extern lean_hesper_hash_buffer_array]

opaque Hesper.WebGPU.hashBufferArray (seed : UInt64) (buffers : Array Buffer) : IO UInt64

Hash an array of buffers into a single UInt64 key in one FFI call. Avoids N separate getBufferId calls per dispatch.

def Hesper.WebGPU.float64ToFloat32Bits (f : Float) : UInt32

Convert Float64 to Float32 IEEE 754 bits

Equations

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

def Hesper.WebGPU.floatArrayToBytes (arr : Array Float) : ByteArray

Helper: Convert Float array to ByteArray for buffer upload (Float64 → Float32)

Equations

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

def Hesper.WebGPU.bytesToFloatArray (bytes : ByteArray) : Array Float

Helper: Convert ByteArray to Float array after buffer readback

Equations

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

def Hesper.WebGPU.jsTraceDumpWith (device : Device) (suffix : String) : IO Unit

DG_TRACE_JS_DUMP=1: after JSTrace.save, dump every referenced buffer without provenance (derived weights: predequants, repacks — and activations, harmless) as b<uid>.bin so the JS replayer can load them directly.

Equations

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

def Hesper.WebGPU.jsTraceDumpMissing (device : Device) : IO Unit

Equations

• Hesper.WebGPU.jsTraceDumpMissing device = Hesper.WebGPU.jsTraceDumpWith device ".bin"

def Hesper.WebGPU.jsTraceDumpAllRegistry (device : Device) : IO Unit

dump EVERY registry buffer (no ref-set needed): call at step-0 START so the replayer gets the true PRE-step-0 state — pre-step-N dumps left stale step-(N-1) content in the unwritten tails of reused scratch buffers, which poisoned window-based comparisons (R19).

Equations

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

def Hesper.WebGPU.jsTraceDumpPost (device : Device) : IO Unit

post-state dump (after the recorded step): the replayer compares every buffer against these to LOCALIZE the first diverging kernel.

Equations

• Hesper.WebGPU.jsTraceDumpPost device = Hesper.WebGPU.jsTraceDumpWith device ".post.bin"