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) [TorchLean.Storage α] : List Spec.Shape → Type

A dependent pack of mutable parameters indexed by their tensor shapes.

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

def Runtime.Autograd.Torch.ParamList.optimizerStorage {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} (parameters : ParamList α ss) : Array (Option (Internal.ParameterStorage α))

Parameter storage in list order, retaining none at every frozen slot.

def Runtime.Autograd.Torch.ParamList.optimizerStorage.collect {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} : ParamList α shapes → Array (Option (Internal.ParameterStorage α)) → Array (Option (Internal.ParameterStorage α))

def Runtime.Autograd.Torch.ParamList.canonicalSlotIndices {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} (parameters : ParamList α ss) : IO (Array (Option ℕ))

Map each trainable slot to the first trainable slot sharing all its mutable storage cells.

Frozen slots remain none; list indices are never compressed. This is the shared alias map for optimizer updates and checkpoint schemas. Storage identity does not inspect tensor elements.

Rebuild the reference index from this list on each call. This preserves changes to the alias layout while avoiding pairwise identity checks among independent storages.

def Runtime.Autograd.Torch.ParamList.ofPack {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss → IO (ParamList α ss)

Allocate mutable parameters from an ordered tensor pack.

def Runtime.Autograd.Torch.ParamList.ofPackWithRequiresGrad {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} (values : TorchLean.TensorPack α ss) (flags : Array Bool) : IO (ParamList α ss)

Allocate mutable parameters with an explicit trainability mask.

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

def Runtime.Autograd.Torch.ParamList.ofPackWithRequiresGrad.go {α : Type} [TorchLean.Storage α] (flags : Array Bool) {shapes : List Spec.Shape} : TorchLean.TensorPack α shapes → ℕ → IO (ParamList α shapes)

def Runtime.Autograd.Torch.ParamList.requiresGradArray {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} : ParamList α ss → Array Bool

Read the trainability mask in parameter order.

def Runtime.Autograd.Torch.ParamList.requiresGradArray.collect {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} : ParamList α shapes → Array Bool → Array Bool

def Runtime.Autograd.Torch.ParamList.values {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} : ParamList α ss → IO (TorchLean.TensorPack α ss)

Read current host parameter values without synchronizing stale CUDA mirrors.

def Runtime.Autograd.Torch.ParamList.valuesSynced {α : Type} [TorchLean.Storage α] [TensorTransfer α] {ss : List Spec.Shape} : ParamList α ss → IO (TorchLean.TensorPack α ss)

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

def Runtime.Autograd.Torch.ParamList.setValues {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} : ParamList α ss → TorchLean.TensorPack α ss → IO Unit

Replace host parameter values from an ordered tensor pack.

def Runtime.Autograd.Torch.ParamList.canonicalGradients {α : Type} [TorchLean.Storage α] [Add α] {ss : List Spec.Shape} (slots : Array (Option ℕ)) (gradients : TorchLean.TensorPack α ss) : IO (Array (Option (Spec.SomeTensor α)))

Sum occurrence gradients at their canonical parameter slots, in list order.

Frozen slots contribute nothing. The first gradient is retained directly so a parameter with no aliases keeps the same arithmetic as an ordinary update. Complete shape and index validation precedes any parameter mutation by the caller.

def Runtime.Autograd.Torch.ParamList.canonicalGradients.collect {α : Type} [TorchLean.Storage α] [Add α] (slots : Array (Option ℕ)) {shapes : List Spec.Shape} : TorchLean.TensorPack α shapes → ℕ → Array (Option (Spec.SomeTensor α)) → IO (Array (Option (Spec.SomeTensor α)))

def Runtime.Autograd.Torch.ParamList.canonicalGradient {α : Type} [TorchLean.Storage α] (shape : Spec.Shape) (sums : Array (Option (Spec.SomeTensor α))) (index : ℕ) : IO (TorchLean.Tensor α shape)

Read one canonical gradient, checking its runtime shape.