Eager Tensor Operations

PyTorch-style tensor operations recorded on the session's tape. Each one runs the CPU or the CUDA kernel of the operation, as the session's device selects, and preserves the typed TensorRef surface.

Elementwise operations

def Runtime.Autograd.Torch.Internal.EagerSession.add {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Add α] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise addition a + b. PyTorch: torch.add.

def Runtime.Autograd.Torch.Internal.EagerSession.sub {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Sub α] [Zero α] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise subtraction a - b. PyTorch: torch.sub.

def Runtime.Autograd.Torch.Internal.EagerSession.mul {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Mul α] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise multiplication a * b. PyTorch: torch.mul.

def Runtime.Autograd.Torch.Internal.EagerSession.div {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Div α] [Mul α] [Sub α] [Zero α] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise division without replacing it by multiplication by a reciprocal.

def Runtime.Autograd.Torch.Internal.EagerSession.neg {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Neg α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record direct scalar negation, preserving signed zero in the forward value.

def Runtime.Autograd.Torch.Internal.EagerSession.scale {α : Type} [TorchLean.Storage α] [TensorTransfer α] (s : EagerSession α) [Mul α] {sh : Spec.Shape} (x : TensorRef α sh) (c : α) : IO (TensorRef α sh)

Record scaling by a scalar constant. PyTorch: x * c.

def Runtime.Autograd.Torch.Internal.EagerSession.abs {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise absolute value. PyTorch: torch.abs.

def Runtime.Autograd.Torch.Internal.EagerSession.sqrt {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise square root. PyTorch: torch.sqrt.

def Runtime.Autograd.Torch.Internal.EagerSession.clamp {α : Type} [TorchLean.Storage α] [TensorTransfer α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (x : TensorRef α sh) (minVal maxVal : α) : IO (TensorRef α sh)

Record elementwise clamp to [minVal,maxVal]. PyTorch: torch.clamp.

def Runtime.Autograd.Torch.Internal.EagerSession.max {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise maximum. PyTorch: torch.maximum.

def Runtime.Autograd.Torch.Internal.EagerSession.min {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (a b : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise minimum. PyTorch: torch.minimum.

def Runtime.Autograd.Torch.Internal.EagerSession.topKMask {α : Type} [TorchLean.Storage α] [Context α] [TensorTransfer α] (s : EagerSession α) {sh : Spec.Shape} (k : ℕ) (x : TensorRef α sh) : IO (TensorRef α sh)

Record the top-k mask of x along its last axis (Spec.MoE.topKMaskSpec), a reference that receives no gradient. CUDA computes it with a comparison kernel; the CPU tape evaluates the spec.

def Runtime.Autograd.Torch.Internal.EagerSession.relu {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Mul α] [Zero α] [Max α] [BEq α] [One α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise ReLU. PyTorch: torch.relu / torch.nn.functional.relu.

def Runtime.Autograd.Torch.Internal.EagerSession.sigmoid {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise sigmoid. PyTorch: torch.sigmoid.

def Runtime.Autograd.Torch.Internal.EagerSession.tanh {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise tanh. PyTorch: torch.tanh.

def Runtime.Autograd.Torch.Internal.EagerSession.silu {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record SiLU as one operation; the input is retained for its negative-tail VJP.

def Runtime.Autograd.Torch.Internal.EagerSession.gelu {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record tanh-approximate GELU as one tape operation.

def Runtime.Autograd.Torch.Internal.EagerSession.softmaxLast {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record shape-preserving softmax over the last axis.

PyTorch comparison: torch.softmax(x, dim=-1).

def Runtime.Autograd.Torch.Internal.EagerSession.logSoftmaxLast {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record stable log-softmax (shape-preserving, last-axis convention).

PyTorch comparison: torch.nn.functional.log_softmax(x, dim=-1).

def Runtime.Autograd.Torch.Internal.EagerSession.softplus {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise softplus. PyTorch: torch.nn.functional.softplus.

def Runtime.Autograd.Torch.Internal.EagerSession.exp {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise exponential. PyTorch: torch.exp.

def Runtime.Autograd.Torch.Internal.EagerSession.sin {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise sine and dispatch its value and VJP through the selected backend.

def Runtime.Autograd.Torch.Internal.EagerSession.cos {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise cosine with the selected backend's -sin(x) * dLdy backward rule.

def Runtime.Autograd.Torch.Internal.EagerSession.log {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise log. PyTorch: torch.log.

def Runtime.Autograd.Torch.Internal.EagerSession.inv {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record elementwise inverse 1/x. PyTorch: torch.reciprocal.

def Runtime.Autograd.Torch.Internal.EagerSession.safeLog {α : Type} [TorchLean.Storage α] [TensorTransfer α] (s : EagerSession α) [Context α] {sh : Spec.Shape} (x : TensorRef α sh) (ε : α := Context.defaultEpsilon) : IO (TensorRef α sh)

Record log(softplus(x) + ε) and its derivative.

Backward multiplies the incoming gradient by sigmoid(x) / (softplus(x) + ε). CUDA converts ε to the input dtype; choose a value that stays positive after conversion if softplus can round to zero. Neither backend checks positivity here or guarantees finite results for nonfinite inputs.