structure Hesper.WebGPU.BindGroupLayoutEntry : Type

Bind group layout entry descriptor

• binding : UInt32
• visibility : ShaderStage
• bindingType : BindingType

instance Hesper.WebGPU.instInhabitedBindGroupLayoutEntry : Inhabited BindGroupLayoutEntry

Equations

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

@[extern lean_hesper_create_bind_group_layout]

opaque Hesper.WebGPU.createBindGroupLayout (device : Device) (entries : Array BindGroupLayoutEntry) : IO BindGroupLayout

Create a bind group layout. Defines the interface between shader and bound resources. Resources are automatically cleaned up by Lean's GC via External finalizers. @param device The GPU device @param entries List of binding entries

structure Hesper.WebGPU.BindGroupEntry : Type

Bind group entry - associates a buffer with a binding point

• binding : UInt32
• buffer : Buffer
• offset : USize
• size : USize

@[extern lean_hesper_create_bind_group]

opaque Hesper.WebGPU.createBindGroup (device : Device) (layout : BindGroupLayout) (entries : Array BindGroupEntry) : IO BindGroup

Create a bind group. Binds actual resources (buffers) to the layout. Resources are automatically cleaned up by Lean's GC via External finalizers. @param device The GPU device @param layout The bind group layout @param entries The buffer bindings

structure Hesper.WebGPU.ComputePipelineDescriptor : Type

Compute pipeline descriptor

• shaderModule : ShaderModule
• entryPoint : String
• bindGroupLayout : BindGroupLayout

@[extern lean_hesper_create_compute_pipeline]

opaque Hesper.WebGPU.createComputePipeline (device : Device) (desc : ComputePipelineDescriptor) : IO ComputePipeline

Create a compute pipeline. Resources are automatically cleaned up by Lean's GC via External finalizers. @param device The GPU device @param desc Pipeline configuration

@[extern lean_hesper_dispatch_compute]

opaque Hesper.WebGPU.dispatchCompute (device : Device) (pipeline : ComputePipeline) (bindGroup : BindGroup) (workgroupsX : UInt32) (workgroupsY workgroupsZ : UInt32 := 1) : IO Future

Dispatch compute work (async - returns Future). @param device The GPU device @param pipeline The compute pipeline to execute @param bindGroup The bound resources @param workgroupsX Number of workgroups in X dimension @param workgroupsY Number of workgroups in Y dimension (default 1) @param workgroupsZ Number of workgroups in Z dimension (default 1) @return Future for GPU work completion (pass to deviceWait to wait)

Command Buffer Batching

Record multiple dispatches into a single command encoder, then submit once. Eliminates per-dispatch overhead (command encoder creation + queue submit + wait).

@[extern lean_hesper_create_command_encoder]

opaque Hesper.WebGPU.createCommandEncoder (device : Device) : IO CommandEncoder

Create a new command encoder for recording multiple dispatches.

@[extern lean_hesper_record_dispatch]

opaque Hesper.WebGPU.recordDispatch (encoder : CommandEncoder) (pipeline : ComputePipeline) (bindGroup : BindGroup) (workgroupsX : UInt32) (workgroupsY workgroupsZ : UInt32 := 1) : IO Unit

Record a compute dispatch into an existing command encoder (no submit, no wait).

@[extern lean_hesper_submit_and_wait]

opaque Hesper.WebGPU.submitAndWait (device : Device) (encoder : CommandEncoder) : IO Unit

Finish the command encoder, submit to queue, and wait for all recorded work to complete.

@[extern lean_hesper_submit_no_wait]

opaque Hesper.WebGPU.submitNoWait (device : Device) (encoder : CommandEncoder) : IO Unit

Finish the command encoder and submit to queue WITHOUT waiting. Queue submits are ordered, and cross-command-buffer buffer hazards are tracked by the driver, so this is a cheap batch split: it lets Dawn-on-Metal keep its per-encoder inter-pass barriers correct (which it drops in a very large single encoder) without paying a CPU round-trip per split.