WebGPU Type Definitions

Opaque types for WebGPU resources. Resources are managed via Lean External objects with automatic cleanup by finalizers on the C++ side.

opaque Hesper.WebGPU.Instance : Type

Opaque handle to a WebGPU Instance (Dawn native instance) with automatic cleanup via External finalizer

opaque Hesper.WebGPU.FuturePtr : Type

Internal opaque handle to a GPU work completion Future

structure Hesper.WebGPU.Future : Type

GPU work completion Future that maintains a reference to its parent Instance. This ensures the Instance stays alive while waiting for GPU work to complete.

• ptr : FuturePtr
• parentInstance : Instance

opaque Hesper.WebGPU.DevicePtr : Type

Internal opaque handle to the raw WebGPU Device pointer

structure Hesper.WebGPU.Device : Type

WebGPU Device that maintains a reference to its parent Instance. This ensures the Instance stays alive as long as the Device is in use, preventing premature garbage collection that would cause segfaults.

• ptr : DevicePtr
• parentInstance : Instance

opaque Hesper.WebGPU.BufferPtr : Type

Internal opaque handles for raw WebGPU pointers

opaque Hesper.WebGPU.ShaderModulePtr : Type

opaque Hesper.WebGPU.ComputePipelinePtr : Type

opaque Hesper.WebGPU.BindGroupPtr : Type

opaque Hesper.WebGPU.BindGroupLayoutPtr : Type

opaque Hesper.WebGPU.CommandEncoderPtr : Type

structure Hesper.WebGPU.Buffer : Type

WebGPU Buffer that maintains a reference to its parent Device. This ensures Device (and Instance) stay alive while Buffer is in use.

• ptr : BufferPtr
• parentDevice : Device

structure Hesper.WebGPU.ShaderModule : Type

WebGPU Shader Module that maintains a reference to its parent Device.

• ptr : ShaderModulePtr
• parentDevice : Device

structure Hesper.WebGPU.ComputePipeline : Type

WebGPU Compute Pipeline that maintains a reference to its parent Device.

• ptr : ComputePipelinePtr
• parentDevice : Device

structure Hesper.WebGPU.BindGroup : Type

WebGPU Bind Group that maintains a reference to its parent Device.

• ptr : BindGroupPtr
• parentDevice : Device

structure Hesper.WebGPU.BindGroupLayout : Type

WebGPU Bind Group Layout that maintains a reference to its parent Device.

• ptr : BindGroupLayoutPtr
• parentDevice : Device

structure Hesper.WebGPU.CommandEncoder : Type

WebGPU Command Encoder that maintains a reference to its parent Device.

• ptr : CommandEncoderPtr
• parentDevice : Device

inductive Hesper.WebGPU.BufferUsage : Type

Buffer usage flags

• storage : BufferUsage
• uniform : BufferUsage
• copyDst : BufferUsage
• copySrc : BufferUsage
• mapRead : BufferUsage
• mapWrite : BufferUsage

instance Hesper.WebGPU.instReprBufferUsage : Repr BufferUsage

Equations

• Hesper.WebGPU.instReprBufferUsage = { reprPrec := Hesper.WebGPU.instReprBufferUsage.repr }

def Hesper.WebGPU.instReprBufferUsage.repr : BufferUsage → Nat → Std.Format

Equations

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

def Hesper.WebGPU.instBEqBufferUsage.beq : BufferUsage → BufferUsage → Bool

Equations

• Hesper.WebGPU.instBEqBufferUsage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Hesper.WebGPU.instBEqBufferUsage : BEq BufferUsage

Equations

• Hesper.WebGPU.instBEqBufferUsage = { beq := Hesper.WebGPU.instBEqBufferUsage.beq }

inductive Hesper.WebGPU.ShaderStage : Type

Shader stage visibility

• vertex : ShaderStage
• fragment : ShaderStage
• compute : ShaderStage

instance Hesper.WebGPU.instReprShaderStage : Repr ShaderStage

Equations

• Hesper.WebGPU.instReprShaderStage = { reprPrec := Hesper.WebGPU.instReprShaderStage.repr }

def Hesper.WebGPU.instReprShaderStage.repr : ShaderStage → Nat → Std.Format

Equations

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

def Hesper.WebGPU.instBEqShaderStage.beq : ShaderStage → ShaderStage → Bool

Equations

• Hesper.WebGPU.instBEqShaderStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Hesper.WebGPU.instBEqShaderStage : BEq ShaderStage

Equations

• Hesper.WebGPU.instBEqShaderStage = { beq := Hesper.WebGPU.instBEqShaderStage.beq }

inductive Hesper.WebGPU.BindingType : Type

Binding type for bind group layout

• buffer (readOnly : Bool) : BindingType
• uniformBuffer : BindingType
• sampler : BindingType
• texture : BindingType

instance Hesper.WebGPU.instReprBindingType : Repr BindingType

Equations

• Hesper.WebGPU.instReprBindingType = { reprPrec := Hesper.WebGPU.instReprBindingType.repr }

def Hesper.WebGPU.instReprBindingType.repr : BindingType → Nat → Std.Format

Equations

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

instance Hesper.WebGPU.instBEqBindingType : BEq BindingType

Equations

• Hesper.WebGPU.instBEqBindingType = { beq := Hesper.WebGPU.instBEqBindingType.beq }

def Hesper.WebGPU.instBEqBindingType.beq : BindingType → BindingType → Bool

Equations

• Hesper.WebGPU.instBEqBindingType.beq (Hesper.WebGPU.BindingType.buffer a) (Hesper.WebGPU.BindingType.buffer b) = (a == b)
• Hesper.WebGPU.instBEqBindingType.beq Hesper.WebGPU.BindingType.uniformBuffer Hesper.WebGPU.BindingType.uniformBuffer = true
• Hesper.WebGPU.instBEqBindingType.beq Hesper.WebGPU.BindingType.sampler Hesper.WebGPU.BindingType.sampler = true
• Hesper.WebGPU.instBEqBindingType.beq Hesper.WebGPU.BindingType.texture Hesper.WebGPU.BindingType.texture = true
• Hesper.WebGPU.instBEqBindingType.beq x✝¹ x✝ = false