Linear-algebra operations for the eager engine.

The definitions here cover matrix products, batched products, affine layers, and the corresponding runtime graph nodes shared by CPU and CUDA-backed execution.

def Runtime.Autograd.Tape.linear {α : Type} [Add α] [Mul α] [Zero α] [DecidableEq Spec.Shape] {inDim outDim : ℕ} (t : Tape α) (wId bId xId : ℕ) : Result (Tape α × ℕ)

Fully-connected linear layer y = W x + b (matvec).

Type-level shapes enforce W : (outDim, inDim), x : (inDim,), b : (outDim,). PyTorch comparison: torch.nn.functional.linear.

def Runtime.Autograd.Tape.matmul {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {m n p : ℕ} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

2D matrix multiplication.

PyTorch comparison: torch.matmul(a, b) for 2D tensors.

def Runtime.Autograd.Tape.bmm {α : Type} [Add α] [Mul α] [Zero α] [DecidableEq Spec.Shape] {batch m n p : ℕ} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Batched matrix multiplication.

PyTorch comparison: torch.bmm(a, b).

def Runtime.Autograd.Tape.concatVectors {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [DecidableEq Spec.Shape] {n m : ℕ} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Concatenate two 1D vectors along dimension 0.

PyTorch comparison: torch.cat([a, b], dim=0) for vectors.

def Runtime.Autograd.Tape.concatDim0 {α : Type} [DecidableEq Spec.Shape] {n m : ℕ} {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Concatenate two tensors along dimension 0.

PyTorch comparison: torch.cat([a, b], dim=0).

def Runtime.Autograd.Tape.sliceRange0 {α : Type} [Zero α] [DecidableEq Spec.Shape] {n : ℕ} {s : Spec.Shape} (t : Tape α) (xId start len : ℕ) (h : len + start ≤ n) : Result (Tape α × ℕ)

Slice along dimension 0: x[start : start+len].

The proof argument h enforces bounds. PyTorch comparison: x[start:start+len] on tensors with a leading dimension.