Session-level autograd operations.

This module exposes backward and gradient-readback helpers for session tensors while preserving the host/CUDA synchronization invariants maintained by the runtime.

def Runtime.Autograd.Model.Session.backwardDenseAll {α : Type} [TorchLean.Storage α] (s : Session α) [Add α] [Zero α] [Torch.TensorTransfer α] {sh : Spec.Shape} (out : Torch.TensorRef α sh) (seed : TorchLean.Tensor α sh) : IO (Array (Spec.SomeTensor α))

Run a backward pass and return a dense array of gradients for all leaf tensors.

This is the explicit dense-array version of calling backward and then reading every leaf gradient.

def Runtime.Autograd.Model.Session.Internal.applyGradHook {α : Type} [TorchLean.Storage α] (grads : Array (Spec.SomeTensor α)) (hook : ℕ → Spec.SomeTensor α → IO (Spec.SomeTensor α)) : IO (Array (Spec.SomeTensor α))

Apply a gradient hook pointwise to a dense gradient array.

Invariant: the hook must preserve each gradient tensor's shape; we check this and throw if it changes.

def Runtime.Autograd.Model.Session.backwardDenseAllWithHook {α : Type} [TorchLean.Storage α] (s : Session α) [Add α] [Zero α] [Torch.TensorTransfer α] {sh : Spec.Shape} (out : Torch.TensorRef α sh) (seed : TorchLean.Tensor α sh) (hook : ℕ → Spec.SomeTensor α → IO (Spec.SomeTensor α)) : IO (Array (Spec.SomeTensor α))

Backward pass with an optional gradient hook applied to the dense gradient array.

This is a runtime utility (similar in spirit to PyTorch hooks), not part of the proof semantics.

def Runtime.Autograd.Model.Session.backwardScalarDenseAll {α : Type} [TorchLean.Storage α] (s : Session α) [Add α] [Zero α] [One α] [Torch.TensorTransfer α] (loss : Torch.TensorRef α Spec.Shape.scalar) : IO (Array (Spec.SomeTensor α))

Backward pass for a scalar loss, returning the dense gradient array (seed is implicitly 1).

def Runtime.Autograd.Model.Session.grad {α : Type} [TorchLean.Storage α] (s : Session α) {sh : Spec.Shape} (grads : Array (Spec.SomeTensor α)) (x : Torch.TensorRef α sh) : IO (TorchLean.Tensor α sh)

Extract the gradient for a particular tensor ref from a dense gradient array.

This is the non-mutating counterpart of reading x.grad.

def Runtime.Autograd.Model.Session.vjp {α : Type} [TorchLean.Storage α] (s : Session α) [Add α] [Zero α] [Torch.TensorTransfer α] {shOut shX : Spec.Shape} (out : Torch.TensorRef α shOut) (seed : TorchLean.Tensor α shOut) (x : Torch.TensorRef α shX) : IO (TorchLean.Tensor α shX)

Vector-Jacobian product: vjp(out, seed)[x].

Forward-mode: JVP

def Runtime.Autograd.Model.Session.jvpLeaf {α : Type} [TorchLean.Storage α] (s : Session α) [Zero α] {shOut shX : Spec.Shape} (out : Torch.TensorRef α shOut) (x : Torch.TensorRef α shX) (dx : TorchLean.Tensor α shX) : IO (TorchLean.Tensor α shOut)

Jacobian-vector product for a single leaf (typed graph execution only).

For eager sessions, use the typed graph execution if you need JVPs.

def Runtime.Autograd.Model.Session.jvpScalarLeaf {α : Type} [TorchLean.Storage α] (s : Session α) [Zero α] (loss : Torch.TensorRef α Spec.Shape.scalar) {shX : Spec.Shape} (x : Torch.TensorRef α shX) (dx : TorchLean.Tensor α shX) : IO α

Scalar-loss JVP for a single leaf (typed graph execution only).

Forward-mode: dense JVP (typed graph execution only)

def Runtime.Autograd.Model.Session.jvpDenseAll {α : Type} [TorchLean.Storage α] (s : Session α) [Zero α] {shOut : Spec.Shape} (out : Torch.TensorRef α shOut) (dxs : Array (Spec.SomeTensor α)) : IO (TorchLean.Tensor α shOut)

Jacobian-vector product with explicit tangents for all leaf tensors.

dxs[i] is the tangent for leaf i (same indexing as grad/backwardDenseAll).

def Runtime.Autograd.Model.Session.sgdStepAll {α : Type} [TorchLean.Storage α] (s : Session α) [Sub α] [Mul α] [Add α] [Zero α] [Torch.TensorTransfer α] (lr : α) (grads : Array (Spec.SomeTensor α)) : IO Unit

Apply a dense SGD step to all learnable parameters.

This is an optimizer helper used by examples; for a higher-level API see TorchLean.Trainer and TorchLean.Trainer.Session.