Parameter Mirrors

CUDA updates leave the host tensor stale. We only download it at an explicit readback boundary; writing a host value removes the cached mirror without invalidating recorded CUDA snapshots.

def Runtime.Autograd.Torch.Internal.syncParamCudaToHost {α : Type} [TorchLean.Storage α] [TensorTransfer α] {sh : Spec.Shape} (p : Param α sh) : IO Unit

Synchronize a CUDA-updated parameter back to its host tensor, if needed.

This synchronization point is explicit. Training hot paths keep parameters resident on device; public readback APIs call this helper before exposing parameter tensors to the Lean side.

def Runtime.Autograd.Torch.Internal.setParamCudaValue {α : Type} [TorchLean.Storage α] {sh : Spec.Shape} (p : Param α sh) (any : LibTorch.AnyBuffer) : IO Unit

Store/update the CUDA mirror of a parameter and mark the host tensor stale.

Replacing the mirror drops its previous reference without invalidating recorded snapshots. The incoming buffer must not remain subject to another scope's explicit release; installing an owned tape intermediate requires a copy or transfer of that scope's release responsibility.

def Runtime.Autograd.Torch.Internal.setParamHostValue {α : Type} [TorchLean.Storage α] {sh : Spec.Shape} (p : Param α sh) (v : TorchLean.Tensor α sh) : IO Unit

Overwrite a host parameter value and invalidate any stale CUDA mirror.

def Runtime.Autograd.Torch.Internal.getParamCudaValue {α : Type} [TorchLean.Storage α] [TensorTransfer α] {sh : Spec.Shape} (p : Param α sh) : IO LibTorch.AnyBuffer

Read the current CUDA mirror, uploading a current host value when the cache is empty.

The returned buffer is shared with the parameter. A caller may retain it as a recorded snapshot; replacing the cache later drops only the parameter's reference. A cache with the wrong shape, or an absent cache paired with a stale host value, has no justified current value to use.