Eager Session State

The tapes and side tables shared by eager operations. Parameters own their CUDA mirrors; the session owns recorded intermediates. Handle generations separate consecutive forward passes.

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

The mutable cells owned by a parameter, without reading or comparing tensor elements.

Two registrations share optimizer storage only when all three cells coincide. Equal values and equal names do not make separately allocated parameters aliases. Keeping this descriptor in the session leaves the public Param record and its construction interface unchanged.

• shape : Spec.Shape
• value : IO.Ref (TorchLean.Tensor α self.shape)
• cudaValue : IO.Ref (Option Cuda.AnyBuffer)
• hostCurrent : IO.Ref Bool

def Runtime.Autograd.Torch.Internal.ParameterStorage.same {α : Type} [TorchLean.Storage α] (left right : ParameterStorage α) : IO Bool

Compare mutable-cell identity using Lean's safe stateful reference operation.

def Runtime.Autograd.Torch.Internal.ParameterStorage.canonicalIndices {α : Type} [TorchLean.Storage α] (storages : Array (Option (ParameterStorage α))) : IO (Array (Option ℕ))

Map each present storage to its first occurrence, retaining absent slots.

A balanced tree of full-width reference keys avoids pairwise searches among independent storages. Reference equality remains authoritative even if keys collide. Representatives retain their cells until the operation ends; neither keys nor references are cached between calls. Consequently a new parameter list or recording can change its alias layout without invalidating a cache.

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

Mutable tapes and side tables for eager execution.

paramsByLeaf links parameter leaves to their persistent storage. A reset drops the recording and advances refGeneration, but keeps the owner id, random counter, and backend selections.

• options : Config

  Session options controlling backend/device/kernel behavior.

• tape : IO.Ref (Tape α)

  CPU eager tape used when Config.device options = .cpu.

• cudaTape : IO.Ref Cuda.Tape

  CUDA eager tape used when Config.device options = .cuda.

• paramsByLeaf : IO.Ref (Std.HashMap ℕ (AnyParam α))

  Map from tape leaf ids to trainable parameter objects.

• parameterStorageByLeaf : IO.Ref (Std.HashMap ℕ (ParameterStorage α))

  Storage identities for this recording's parameter leaves; no tensor snapshots are cached.

• nats : IO.Ref (Array ℕ)

  Non-differentiable integer inputs for dynamic indexing operations.

• rngCounter : IO.Ref ℕ

  Number of seeded random tensors generated by this session.

• selectedBackends : IO.Ref (Array NN.Backend.AcceptedKernel)

  Accepted capsules already reported for this session, in first-use order.

• refOwner : ℕ

  Process-unique owner id for session references.

• refGeneration : IO.Ref ℕ

  Current recording generation for session references.