Core Tape Indexing Operations

This file implements gather and scatter-style tape nodes. The forward rules expose typed indexing operations, and the backward rules route upstream gradients back to the selected source coordinates.

def Runtime.Autograd.Tape.gatherScalar {α : Type} [Zero α] [DecidableEq Spec.Shape] {n : ℕ} (t : Tape α) (xId : ℕ) (i : Fin n) : Result (Tape α × ℕ)

Gather a scalar from a 1D vector using a compile-time index Fin n.

PyTorch comparison: x[i] (1D indexing).

def Runtime.Autograd.Tape.gatherRow {α : Type} [Zero α] [DecidableEq Spec.Shape] {rows cols : ℕ} (t : Tape α) (xId : ℕ) (i : Fin rows) : Result (Tape α × ℕ)

Gather a row from a 2D matrix using a compile-time index Fin rows.

PyTorch comparison: x[i] for 2D tensors (row indexing).

def Runtime.Autograd.Tape.gatherScalarNat {α : Type} [Zero α] [DecidableEq Spec.Shape] {n : ℕ} (t : Tape α) (xId i : ℕ) : Result (Tape α × ℕ)

Gather a scalar from a 1D vector using a runtime Nat index.

Out-of-bounds indices are totalized to return 0. PyTorch comparison: x[i] would raise on out-of-range; here we return 0 to keep the op total.

def Runtime.Autograd.Tape.gatherVecNat {α : Type} [Add α] [Zero α] [DecidableEq Spec.Shape] {n k : ℕ} (t : Tape α) (xId : ℕ) (idx : Spec.Tensor ℕ (Spec.Shape.dim k Spec.Shape.scalar)) : Result (Tape α × ℕ)

Gather k scalars from a 1D vector using an explicit index tensor.

Out-of-bounds indices are totalized to 0. In the backward pass, gradients are accumulated for repeated indices (scatter-add semantics). PyTorch comparison: related to torch.gather / advanced indexing.

def Runtime.Autograd.Tape.gatherRowsNat {α : Type} [Add α] [Zero α] [DecidableEq Spec.Shape] {rows cols k : ℕ} (t : Tape α) (xId : ℕ) (idx : Spec.Tensor ℕ (Spec.Shape.dim k Spec.Shape.scalar)) : Result (Tape α × ℕ)

Gather k rows from a 2D matrix using an explicit index tensor.

Out-of-bounds indices are totalized to zero rows; backward accumulates gradients into selected rows (scatter-add), including repeated indices.

def Runtime.Autograd.Tape.scatterAddVec {α : Type} [Add α] [Zero α] [DecidableEq Spec.Shape] {n : ℕ} (t : Tape α) (xId vId : ℕ) (i : Fin n) : Result (Tape α × ℕ)

Scatter-add into a vector: return a copy of x with x[i] += v.

Backward: gradient w.r.t. x is the upstream dL/dy, and gradient w.r.t. v is the gathered scalar dL/dy[i].

def Runtime.Autograd.Tape.scatterAddRow {α : Type} [Add α] [Zero α] [DecidableEq Spec.Shape] {rows cols : ℕ} (t : Tape α) (xId vId : ℕ) (i : Fin rows) : Result (Tape α × ℕ)

Scatter-add into a matrix row: return a copy of x with x[i,:] += v.

Backward: gradient w.r.t. v is the gathered row dL/dy[i,:].