Trainer Parameters

Mutable, shape-indexed parameter storage for the Torch-style trainer. Parameter values may retain a CUDA mirror; reads and writes keep host and device ownership explicit through the underlying Param operations.

inductive Runtime.Autograd.Torch.ParamList (α : Type) : List Spec.Shape → Type

A heterogeneous list of mutable parameters indexed by their tensor shapes.

• nil {α : Type} : ParamList α []
• cons {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : Param α s → ParamList α ss → ParamList α (s :: ss)

def Runtime.Autograd.Torch.ParamList.subScaleMaterialize {α : Type} [Sub α] [Mul α] {s : Spec.Shape} : Spec.Tensor α s → Spec.Tensor α s → α → Spec.Tensor α s

Materialize value - rate * gradient in one traversal.

def Runtime.Autograd.Torch.ParamList.ofTList {α : Type} {ss : List Spec.Shape} : TList α ss → IO (ParamList α ss)

Allocate mutable parameters from an ordered tensor pack.

def Runtime.Autograd.Torch.ParamList.ofTListWithRequiresGrad {α : Type} {ss : List Spec.Shape} : TList α ss → List Bool → IO (ParamList α ss)

Allocate mutable parameters with an explicit trainability mask.

The mask follows parameter order and must have exactly the same length as the shape list.

def Runtime.Autograd.Torch.ParamList.requiresGradList {α : Type} {ss : List Spec.Shape} : ParamList α ss → List Bool

Read the trainability mask in parameter order.

def Runtime.Autograd.Torch.ParamList.values {α : Type} {ss : List Spec.Shape} : ParamList α ss → IO (TList α ss)

Read current host parameter values without synchronizing stale CUDA mirrors.

def Runtime.Autograd.Torch.ParamList.valuesSynced {α : Type} [Internal.CudaBridge.TensorConv α] [DecidableEq Spec.Shape] {ss : List Spec.Shape} : ParamList α ss → IO (TList α ss)

Read parameter values after synchronizing any current CUDA mirrors to the host.

def Runtime.Autograd.Torch.ParamList.setValues {α : Type} {ss : List Spec.Shape} : ParamList α ss → TList α ss → IO Unit

Replace host parameter values from an ordered tensor pack.

def Runtime.Autograd.Torch.ParamList.sgdStep {α : Type} [Context α] {ss : List Spec.Shape} : ParamList α ss → α → TList α ss → IO Unit

Apply param := param - rate * gradient to every trainable parameter.