Core training helpers

These are small, reusable utilities that keep training scripts short and readable. They are pure and local.

def Runtime.Autograd.Train.tagError (tag msg : String) : String

Prefix an error message with a caller-provided tag.

This is used throughout the training helpers to keep error messages readable when multiple subsystems can fail (tape execution, dataset loading, shape checks, etc.).

Typed extraction helpers

The autograd engine stores values and gradients as Runtime.AnyTensor (shape tag + tensor). These helpers check shapes and give you back a typed tensor or a scalar value.

def Runtime.Autograd.Train.requireGradTensor {a : Type} [DecidableEq Spec.Shape] {s : Spec.Shape} (tag : String) (grads : Std.HashMap ℕ (AnyTensor a)) (id : ℕ) : Result (Spec.Tensor a s)

Read a typed gradient tensor Tensor a s from a gradient map keyed by node id.

The eager tape engine stores gradients in a shape-erased form (Runtime.AnyTensor a), so this helper performs the dynamic shape check and returns a typed tensor on success.

def Runtime.Autograd.Train.requireValueTensor {a : Type} [DecidableEq Spec.Shape] {s : Spec.Shape} (tag : String) (t : Tape a) (id : ℕ) : Result (Spec.Tensor a s)

Read a typed forward value Tensor a s from a tape node id.

This is the value-side analogue of requireGradTensor: it performs a dynamic shape check on the shape tag stored in AnyTensor.

def Runtime.Autograd.Train.requireScalarValue {a : Type} [DecidableEq Spec.Shape] (tag : String) (t : Tape a) (id : ℕ) : Result a

Read a scalar forward value from a tape node id.

This is a common pattern in training scripts where the loss is a scalar node.

SGD update helper

This is a small tensor-level update used by many tests.