Shared Parameter Gradients

Each use records the value observed at that call. Optimizers combine the cotangents of leaves whose parameter storage is shared, then update that storage once. Grouping at this boundary keeps fresh reads after parameter mutation independent of earlier tape snapshots.

structure Runtime.Autograd.Torch.Internal.EagerSession.ParameterGroup (α : Type) [TorchLean.Storage α] : Type

Parameter leaves in recording order, with the first leaf retained as the optimizer key.

• id : ℕ
• parameter : AnyParam α
• leaves : Array ℕ
• storage? : Option (ParameterStorage α)

def Runtime.Autograd.Torch.Internal.EagerSession.groupParameterRegistrations {α : Type} [TorchLean.Storage α] (parameters : Std.HashMap ℕ (AnyParam α)) (storages : Std.HashMap ℕ (ParameterStorage α)) : IO (Array (ParameterGroup α))

Group registrations by storage identity without touching tensor data.

The same reference index serves eager updates, generic optimizers, and checkpoint schemas. A singleton group borrows its gradient unchanged; only an actual shared parameter requires gradient addition. The first leaf remains the optimizer key, preserving ordered parameter slots. Entries inserted directly into the internal parameter map without a storage descriptor stay separate, because there is no sound alias test for an arbitrary AnyParam closure.

def Runtime.Autograd.Torch.Internal.EagerSession.parameterGroups {α : Type} [TorchLean.Storage α] (session : EagerSession α) : IO (Array (ParameterGroup α))

Group the current eager recording using the shared storage-identity contract.

def Runtime.Autograd.Torch.Internal.EagerSession.parameterOfStorage {α : Type} [TorchLean.Storage α] (storage : ParameterStorage α) : Param α storage.shape

Recover the typed storage view used by the parameter synchronization helpers.

def Runtime.Autograd.Torch.Internal.EagerSession.ParameterGroup.currentHostValue {α : Type} [TorchLean.Storage α] [TensorTransfer α] (group : ParameterGroup α) : IO (Spec.SomeTensor α)

Read current host storage, synchronizing a newer device mirror before a CPU update.

def Runtime.Autograd.Torch.Internal.EagerSession.ParameterGroup.currentCudaValue {α : Type} [TorchLean.Storage α] [TensorTransfer α] (group : ParameterGroup α) : IO LibTorch.AnyBuffer

Read the current parameter value used as the starting point of a CUDA update.

Cotangents belong to the recorded computation, but an optimizer changes current parameter storage. That storage can differ from every leaf snapshot if the parameter changed after its last use. Ordinary registrations share their current mirror here; only an empty cache requires an upload.

An internal registration without a storage descriptor supplies its current host value through AnyParam.get. Its custom getter must honor that contract; a tape leaf is not a substitute.

def Runtime.Autograd.Torch.Internal.EagerSession.denseGroupGradient {α : Type} [TorchLean.Storage α] [Add α] (group : ParameterGroup α) (gradients : Array (Spec.SomeTensor α)) : IO (Spec.SomeTensor α)

Sum host cotangents for one parameter, retaining the original tensor for a singleton.

def Runtime.Autograd.Torch.Internal.EagerSession.withCudaGroupGradient {α β : Type} [TorchLean.Storage α] (group : ParameterGroup α) (gradients : CudaGradMap) (action : LibTorch.AnyBuffer → IO β) : IO β

Borrow a singleton CUDA gradient or own the temporary sum of shared-leaf cotangents.

The input map remains borrowed throughout. Intermediate sums and the final sum are released on both success and failure; the optimizer action must not retain that temporary gradient.