WGSL type system using phantom types for type safety. These types are used at the Lean level to ensure type correctness, but compile down to WGSL primitive types.

inductive Hesper.WGSL.ScalarType : Type

WGSL scalar types

• f32 : ScalarType
• f16 : ScalarType
• i32 : ScalarType
• u32 : ScalarType
• u64 : ScalarType
• bool : ScalarType
• atomicI32 : ScalarType
• atomicU32 : ScalarType

instance Hesper.WGSL.instReprScalarType : Repr ScalarType

Equations

• Hesper.WGSL.instReprScalarType = { reprPrec := Hesper.WGSL.instReprScalarType.repr }

def Hesper.WGSL.instReprScalarType.repr : ScalarType → Nat → Std.Format

Equations

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

def Hesper.WGSL.instBEqScalarType.beq : ScalarType → ScalarType → Bool

Equations

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

instance Hesper.WGSL.instBEqScalarType : BEq ScalarType

Equations

• Hesper.WGSL.instBEqScalarType = { beq := Hesper.WGSL.instBEqScalarType.beq }

instance Hesper.WGSL.instInhabitedScalarType : Inhabited ScalarType

Equations

• Hesper.WGSL.instInhabitedScalarType = { default := Hesper.WGSL.instInhabitedScalarType.default }

def Hesper.WGSL.instInhabitedScalarType.default : ScalarType

Equations

• Hesper.WGSL.instInhabitedScalarType.default = Hesper.WGSL.ScalarType.f32

inductive Hesper.WGSL.MemorySpace : Type

Memory address spaces in WGSL

• storage : MemorySpace
• uniform : MemorySpace
• workgroup : MemorySpace
• priv : MemorySpace
• func : MemorySpace

def Hesper.WGSL.instReprMemorySpace.repr : MemorySpace → Nat → Std.Format

Equations

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

instance Hesper.WGSL.instReprMemorySpace : Repr MemorySpace

Equations

• Hesper.WGSL.instReprMemorySpace = { reprPrec := Hesper.WGSL.instReprMemorySpace.repr }

def Hesper.WGSL.instBEqMemorySpace.beq : MemorySpace → MemorySpace → Bool

Equations

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

instance Hesper.WGSL.instBEqMemorySpace : BEq MemorySpace

Equations

• Hesper.WGSL.instBEqMemorySpace = { beq := Hesper.WGSL.instBEqMemorySpace.beq }

instance Hesper.WGSL.instInhabitedMemorySpace : Inhabited MemorySpace

Equations

• Hesper.WGSL.instInhabitedMemorySpace = { default := Hesper.WGSL.instInhabitedMemorySpace.default }

def Hesper.WGSL.instInhabitedMemorySpace.default : MemorySpace

Equations

• Hesper.WGSL.instInhabitedMemorySpace.default = Hesper.WGSL.MemorySpace.storage

inductive Hesper.WGSL.WGSLType : Type

WGSL composite types

• scalar : ScalarType → WGSLType
• vec2 : ScalarType → WGSLType
• vec3 : ScalarType → WGSLType
• vec4 : ScalarType → WGSLType
• mat2x2 : ScalarType → WGSLType
• mat3x3 : ScalarType → WGSLType
• mat4x4 : ScalarType → WGSLType
• array : WGSLType → Nat → WGSLType
• runtimeArray : WGSLType → WGSLType
• bufferArray : WGSLType → Nat → WGSLType

  Array of N separate runtime-sized storage buffers, indexed at runtime by layer index. Used for cross-layer kernel fusion: e.g. 42 layers of Q4_K weights accessed by the same kernel via readBufferArray name layer elem. On CUDA lowers to a pointer-table constant in global memory; on WGSL lowers to a binding_array<...> (binding_array extension).

• ptr : MemorySpace → WGSLType → WGSLType
• struct : String → WGSLType
• subgroupMatrixLeft : ScalarType → Nat → Nat → WGSLType
• subgroupMatrixRight : ScalarType → Nat → Nat → WGSLType
• subgroupMatrixResult : ScalarType → Nat → Nat → WGSLType
• texture2D : String → WGSLType
• sampler : WGSLType

def Hesper.WGSL.instReprWGSLType.repr : WGSLType → Nat → Std.Format

Equations

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

instance Hesper.WGSL.instReprWGSLType : Repr WGSLType

Equations

• Hesper.WGSL.instReprWGSLType = { reprPrec := Hesper.WGSL.instReprWGSLType.repr }

instance Hesper.WGSL.instBEqWGSLType : BEq WGSLType

Equations

• Hesper.WGSL.instBEqWGSLType = { beq := Hesper.WGSL.instBEqWGSLType.beq }

def Hesper.WGSL.instBEqWGSLType.beq : WGSLType → WGSLType → Bool

Equations

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

structure Hesper.WGSL.StructField : Type

Struct field definition

• name : String
• type : WGSLType

def Hesper.WGSL.instReprStructField.repr : StructField → Nat → Std.Format

Equations

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

instance Hesper.WGSL.instReprStructField : Repr StructField

Equations

• Hesper.WGSL.instReprStructField = { reprPrec := Hesper.WGSL.instReprStructField.repr }

instance Hesper.WGSL.instBEqStructField : BEq StructField

Equations

• Hesper.WGSL.instBEqStructField = { beq := Hesper.WGSL.instBEqStructField.beq }

def Hesper.WGSL.instBEqStructField.beq : StructField → StructField → Bool

Equations

• Hesper.WGSL.instBEqStructField.beq { name := a, type := a_1 } { name := b, type := b_1 } = (a == b && a_1 == b_1)
• Hesper.WGSL.instBEqStructField.beq x✝¹ x✝ = false

structure Hesper.WGSL.StructDef : Type

Struct definition

• name : String
• fields : List StructField

def Hesper.WGSL.instReprStructDef.repr : StructDef → Nat → Std.Format

Equations

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

instance Hesper.WGSL.instReprStructDef : Repr StructDef

Equations

• Hesper.WGSL.instReprStructDef = { reprPrec := Hesper.WGSL.instReprStructDef.repr }

def Hesper.WGSL.instBEqStructDef.beq : StructDef → StructDef → Bool

Equations

• Hesper.WGSL.instBEqStructDef.beq { name := a, fields := a_1 } { name := b, fields := b_1 } = (a == b && a_1 == b_1)
• Hesper.WGSL.instBEqStructDef.beq x✝¹ x✝ = false

instance Hesper.WGSL.instBEqStructDef : BEq StructDef

Equations

• Hesper.WGSL.instBEqStructDef = { beq := Hesper.WGSL.instBEqStructDef.beq }

inductive Hesper.WGSL.BufferUsage : Type

Buffer usage flags (corresponds to WebGPU buffer usage)

• storage : BufferUsage
• uniform : BufferUsage
• copy_src : BufferUsage
• copy_dst : BufferUsage

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

Equations

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

instance Hesper.WGSL.instReprBufferUsage : Repr BufferUsage

Equations

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

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

Equations

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

instance Hesper.WGSL.instBEqBufferUsage : BEq BufferUsage

Equations

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

inductive Hesper.WGSL.LayoutRule : Type

Layout rules for struct alignment

• std140 : LayoutRule
• std430 : LayoutRule

instance Hesper.WGSL.instReprLayoutRule : Repr LayoutRule

Equations

• Hesper.WGSL.instReprLayoutRule = { reprPrec := Hesper.WGSL.instReprLayoutRule.repr }

def Hesper.WGSL.instReprLayoutRule.repr : LayoutRule → Nat → Std.Format

Equations

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

instance Hesper.WGSL.instBEqLayoutRule : BEq LayoutRule

Equations

• Hesper.WGSL.instBEqLayoutRule = { beq := Hesper.WGSL.instBEqLayoutRule.beq }

def Hesper.WGSL.instBEqLayoutRule.beq : LayoutRule → LayoutRule → Bool

Equations

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

instance Hesper.WGSL.instInhabitedLayoutRule : Inhabited LayoutRule

Equations

• Hesper.WGSL.instInhabitedLayoutRule = { default := Hesper.WGSL.instInhabitedLayoutRule.default }

def Hesper.WGSL.instInhabitedLayoutRule.default : LayoutRule

Equations

• Hesper.WGSL.instInhabitedLayoutRule.default = Hesper.WGSL.LayoutRule.std140

structure Hesper.WGSL.BindingInfo : Type

Binding layout information for type-safe pipeline creation

• group : Nat
• binding : Nat
• type : WGSLType
• usage : BufferUsage

structure Hesper.WGSL.Layout : Type

Shader layout - collection of bindings with type information

• bindings : List BindingInfo

def Hesper.WGSL.instInhabitedLayout.default : Layout

Equations

• Hesper.WGSL.instInhabitedLayout.default = { bindings := default }

instance Hesper.WGSL.instInhabitedLayout : Inhabited Layout

Equations

• Hesper.WGSL.instInhabitedLayout = { default := Hesper.WGSL.instInhabitedLayout.default }

def Hesper.WGSL.ScalarType.toWGSL : ScalarType → String

Convert scalar type to WGSL string

Equations

• Hesper.WGSL.ScalarType.f32.toWGSL = "f32"
• Hesper.WGSL.ScalarType.f16.toWGSL = "f16"
• Hesper.WGSL.ScalarType.i32.toWGSL = "i32"
• Hesper.WGSL.ScalarType.u32.toWGSL = "u32"
• Hesper.WGSL.ScalarType.u64.toWGSL = "u64"
• Hesper.WGSL.ScalarType.bool.toWGSL = "bool"
• Hesper.WGSL.ScalarType.atomicI32.toWGSL = "atomic<i32>"
• Hesper.WGSL.ScalarType.atomicU32.toWGSL = "atomic<u32>"

def Hesper.WGSL.MemorySpace.toWGSL : MemorySpace → String

Convert memory space to WGSL string

Equations

• Hesper.WGSL.MemorySpace.storage.toWGSL = "storage"
• Hesper.WGSL.MemorySpace.uniform.toWGSL = "uniform"
• Hesper.WGSL.MemorySpace.workgroup.toWGSL = "workgroup"
• Hesper.WGSL.MemorySpace.priv.toWGSL = "private"
• Hesper.WGSL.MemorySpace.func.toWGSL = "function"

def Hesper.WGSL.WGSLType.toWGSL : WGSLType → String

Convert WGSL type to WGSL string

Equations

• One or more equations did not get rendered due to their size.
• (Hesper.WGSL.WGSLType.scalar a).toWGSL = a.toWGSL
• (Hesper.WGSL.WGSLType.vec2 a).toWGSL = toString "vec2<" ++ toString a.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.vec3 a).toWGSL = toString "vec3<" ++ toString a.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.vec4 a).toWGSL = toString "vec4<" ++ toString a.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.mat2x2 a).toWGSL = toString "mat2x2<" ++ toString a.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.mat3x3 a).toWGSL = toString "mat3x3<" ++ toString a.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.mat4x4 a).toWGSL = toString "mat4x4<" ++ toString a.toWGSL ++ toString ">"
• (a.array a_1).toWGSL = toString "array<" ++ toString a.toWGSL ++ toString ", " ++ toString a_1 ++ toString ">"
• a.runtimeArray.toWGSL = toString "array<" ++ toString a.toWGSL ++ toString ">"
• (a.bufferArray a_1).toWGSL = toString "binding_array<array<" ++ toString a.toWGSL ++ toString ">, " ++ toString a_1 ++ toString ">"
• (Hesper.WGSL.WGSLType.ptr a a_1).toWGSL = toString "ptr<" ++ toString a.toWGSL ++ toString ", " ++ toString a_1.toWGSL ++ toString ">"
• (Hesper.WGSL.WGSLType.struct a).toWGSL = a
• (Hesper.WGSL.WGSLType.texture2D a).toWGSL = toString "texture_2d<" ++ toString a ++ toString ">"
• Hesper.WGSL.WGSLType.sampler.toWGSL = "sampler"

def Hesper.WGSL.ScalarType.byteSize : ScalarType → Nat

Byte size of a scalar type

Equations

• Hesper.WGSL.ScalarType.f32.byteSize = 4
• Hesper.WGSL.ScalarType.f16.byteSize = 2
• Hesper.WGSL.ScalarType.i32.byteSize = 4
• Hesper.WGSL.ScalarType.u32.byteSize = 4
• Hesper.WGSL.ScalarType.u64.byteSize = 8
• Hesper.WGSL.ScalarType.bool.byteSize = 4
• Hesper.WGSL.ScalarType.atomicI32.byteSize = 4
• Hesper.WGSL.ScalarType.atomicU32.byteSize = 4

def Hesper.WGSL.WGSLType.byteSize : WGSLType → Nat

Calculate byte size of a type (for buffer allocation)

Equations

• (Hesper.WGSL.WGSLType.scalar a).byteSize = a.byteSize
• (Hesper.WGSL.WGSLType.vec2 a).byteSize = 2 * a.byteSize
• (Hesper.WGSL.WGSLType.vec3 a).byteSize = 3 * a.byteSize
• (Hesper.WGSL.WGSLType.vec4 a).byteSize = 4 * a.byteSize
• (Hesper.WGSL.WGSLType.mat2x2 a).byteSize = 4 * a.byteSize
• (Hesper.WGSL.WGSLType.mat3x3 a).byteSize = 9 * a.byteSize
• (Hesper.WGSL.WGSLType.mat4x4 a).byteSize = 16 * a.byteSize
• (a.array a_1).byteSize = a_1 * a.byteSize
• a.runtimeArray.byteSize = 0
• (a.bufferArray a_1).byteSize = 0
• (Hesper.WGSL.WGSLType.ptr a a_1).byteSize = 8
• (Hesper.WGSL.WGSLType.struct a).byteSize = 0
• (Hesper.WGSL.WGSLType.subgroupMatrixLeft a a_1 a_2).byteSize = a_1 * a_2 * a.byteSize
• (Hesper.WGSL.WGSLType.subgroupMatrixRight a a_1 a_2).byteSize = a_1 * a_2 * a.byteSize
• (Hesper.WGSL.WGSLType.subgroupMatrixResult a a_1 a_2).byteSize = a_1 * a_2 * a.byteSize
• (Hesper.WGSL.WGSLType.texture2D a).byteSize = 0
• Hesper.WGSL.WGSLType.sampler.byteSize = 0

def Hesper.WGSL.ScalarType.alignment : ScalarType → Nat

Alignment of a scalar type

Equations

• Hesper.WGSL.ScalarType.f32.alignment = 4
• Hesper.WGSL.ScalarType.f16.alignment = 2
• Hesper.WGSL.ScalarType.i32.alignment = 4
• Hesper.WGSL.ScalarType.u32.alignment = 4
• Hesper.WGSL.ScalarType.u64.alignment = 8
• Hesper.WGSL.ScalarType.bool.alignment = 4
• Hesper.WGSL.ScalarType.atomicI32.alignment = 4
• Hesper.WGSL.ScalarType.atomicU32.alignment = 4

def Hesper.WGSL.WGSLType.alignment (rule : LayoutRule) : WGSLType → Nat

Calculate alignment of a type according to layout rules

Equations

• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.scalar a) = a.alignment
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.vec2 a) = 2 * a.alignment
• Hesper.WGSL.WGSLType.alignment Hesper.WGSL.LayoutRule.std140 (Hesper.WGSL.WGSLType.vec3 a) = 16
• Hesper.WGSL.WGSLType.alignment Hesper.WGSL.LayoutRule.std430 (Hesper.WGSL.WGSLType.vec3 a) = 4 * a.alignment
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.vec4 a) = 4 * a.alignment
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.mat2x2 a) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.mat3x3 a) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.mat4x4 a) = 16
• Hesper.WGSL.WGSLType.alignment rule (a.array a_1) = Hesper.WGSL.WGSLType.alignment rule a
• Hesper.WGSL.WGSLType.alignment rule a.runtimeArray = Hesper.WGSL.WGSLType.alignment rule a
• Hesper.WGSL.WGSLType.alignment rule (a.bufferArray a_1) = Hesper.WGSL.WGSLType.alignment rule a
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.ptr a a_1) = 8
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.struct a) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.subgroupMatrixLeft a a_1 a_2) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.subgroupMatrixRight a a_1 a_2) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.subgroupMatrixResult a a_1 a_2) = 16
• Hesper.WGSL.WGSLType.alignment rule (Hesper.WGSL.WGSLType.texture2D a) = 0
• Hesper.WGSL.WGSLType.alignment rule Hesper.WGSL.WGSLType.sampler = 0