Proof-Linked Session: Neural-Network Operations

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

Record elementwise logistic sigmoid.

PyTorch comparison: torch.sigmoid(x).

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

Record elementwise hyperbolic tangent.

PyTorch comparison: torch.tanh(x).

def Runtime.Autograd.Torch.Internal.SessionIR.softmax {α : Type} (s : SessionIR α) [Context α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record softmax (shape-preserving).

PyTorch comparison: torch.softmax(x, dim=...). This helper uses the convention baked into the underlying GraphM.softmax implementation.

def Runtime.Autograd.Torch.Internal.SessionIR.logSoftmax {α : Type} (s : SessionIR α) [Context α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α sh)

Record stable log-softmax in the linked compiled session.

This commits a single GraphM.logSoftmax node instead of expanding to softmax followed by log, so compiled execution keeps the same stable semantics as eager CPU/CUDA.

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

Record elementwise softplus.

PyTorch comparison: torch.nn.functional.softplus(x).

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

Record elementwise exponential.

PyTorch comparison: torch.exp(x).

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

Record elementwise natural logarithm.

PyTorch comparison: torch.log(x).

def Runtime.Autograd.Torch.Internal.SessionIR.safeLog {α : Type} (s : SessionIR α) [Context α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (x : TensorRef α sh) (ε : α := Numbers.epsilon) : IO (TensorRef α sh)

Record elementwise log with epsilon guard.

This is intended for numerically stable losses; it corresponds approximately to log(max(x, ε)). PyTorch comparison: torch.log(torch.clamp(x, min=ε)).

def Runtime.Autograd.Torch.Internal.SessionIR.sum {α : Type} (s : SessionIR α) [Context α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (x : TensorRef α sh) : IO (TensorRef α Spec.Shape.scalar)

Sum-reduce all elements to a scalar.

PyTorch comparison: x.sum().

def Runtime.Autograd.Torch.Internal.SessionIR.linear {α : Type} (s : SessionIR α) [Add α] [Mul α] [Zero α] [DecidableEq Spec.Shape] {inDim outDim : ℕ} (w : TensorRef α (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (b : TensorRef α (Spec.Shape.dim outDim Spec.Shape.scalar)) (x : TensorRef α (Spec.Shape.dim inDim Spec.Shape.scalar)) : IO (TensorRef α (Spec.Shape.dim outDim Spec.Shape.scalar))

Record a fully-connected linear layer: y = w • x + b.

Type-level shapes enforce w : (outDim, inDim), b : (outDim,), and x : (inDim,). PyTorch comparison: torch.nn.functional.linear(x, weight=w, bias=b) (with the same weight layout).

def Runtime.Autograd.Torch.Internal.SessionIR.mseLoss {α : Type} (s : SessionIR α) [Add α] [Sub α] [Mul α] [Div α] [Zero α] [One α] [Coe ℕ α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (yhat target : TensorRef α sh) : IO (TensorRef α Spec.Shape.scalar)

Mean-squared-error loss returning a scalar.

PyTorch comparison: torch.nn.functional.mse_loss(yhat, target, reduction="mean").

def Runtime.Autograd.Torch.Internal.SessionIR.layerNorm {α : Type} (s : SessionIR α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {seqLen embedDim : ℕ} (h_seq_pos : seqLen > 0) (h_embed_pos : embedDim > 0) (x : TensorRef α (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar))) (gamma beta : TensorRef α (Spec.Shape.dim embedDim Spec.Shape.scalar)) : IO (TensorRef α (Spec.Shape.dim seqLen (Spec.Shape.dim embedDim Spec.Shape.scalar)))

Layer normalization over the trailing embedding dimension.

This variant is specialized to 2D tensors of shape (seqLen, embedDim) and expects positive dimensions for numerical stability and well-formedness. PyTorch comparison: torch.nn.LayerNorm(embedDim) (applied per token), or torch.nn.functional.layer_norm.

def Runtime.Autograd.Torch.Internal.SessionIR.batchnormChannelFirst {α : Type} (s : SessionIR α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {channels height width : ℕ} (h_c : channels > 0) (h_h : height > 0) (h_w : width > 0) (x : TensorRef α (Spec.Shape.dim channels (Spec.Shape.dim height (Spec.Shape.dim width Spec.Shape.scalar)))) (gamma beta : TensorRef α (Spec.Shape.dim channels Spec.Shape.scalar)) : IO (TensorRef α (Spec.Shape.dim channels (Spec.Shape.dim height (Spec.Shape.dim width Spec.Shape.scalar))))

Batch normalization for a channel-first image (C,H,W) (no batch axis).

gamma and beta are per-channel scale/shift parameters. PyTorch comparison: torch.nn.BatchNorm2d(C) (conceptually), or torch.nn.functional.batch_norm specialized to a single "batch element" with NCHW layout.