Runtime variables

This module defines a small Variable record that bundles:

• a name/id,
• a value tensor,
• an optional gradient tensor, and
• a requires_grad flag.

This matches the mental model of a PyTorch torch.Tensor with requires_grad, together with a place to store an accumulated .grad. It is used by the runtime layers that want an explicit "parameter object", while NN/Runtime/Context.lean provides a more generic name-based registry.

structure Runtime.Variable (α : Type) (s : Spec.Shape) : Type

A runtime variable with a fixed shape.

gradient is optional so we can represent "no gradient accumulated yet" (or variables that are used only for inference).

• id : ℕ

  Unique numeric id (allocated by the runtime context).

• name : String

  Human-readable name (often a parameter name like "layer1.weight").

• value : Spec.Tensor α s

  The current tensor value.

• gradient : Option (Spec.Tensor α s)

  Optional accumulated gradient.

  This is none when no gradient has been accumulated yet (or when requires_grad = false).

• requires_grad : Bool

  Whether gradient-based optimizers may update this variable.

def Runtime.Variable.createVariable {α : Type} {s : Spec.Shape} (id : ℕ) (name : String) (value : Spec.Tensor α s) (requires_grad : Bool := true) : Variable α s

Create a new variable from an id/name/value.

By default we mark variables as trainable (requires_grad := true), matching common ML defaults.

def Runtime.Variable.getValue {α : Type} {s : Spec.Shape} (v : Variable α s) : Spec.Tensor α s

Read the tensor value stored in a variable.

def Runtime.Variable.setValue {α : Type} {s : Spec.Shape} (v : Variable α s) (new_value : Spec.Tensor α s) : Variable α s

Replace the tensor value stored in a variable.

def Runtime.Variable.getGradient {α : Type} {s : Spec.Shape} (v : Variable α s) : Option (Spec.Tensor α s)

Read the optional gradient stored in a variable.

def Runtime.Variable.setGradient {α : Type} {s : Spec.Shape} (v : Variable α s) (grad : Spec.Tensor α s) : Variable α s

Set (overwrite) the gradient stored in a variable.

def Runtime.Variable.clearGradient {α : Type} {s : Spec.Shape} (v : Variable α s) : Variable α s

Clear the gradient stored in a variable.

def Runtime.Variable.checkRequiresGrad {α : Type} {s : Spec.Shape} (v : Variable α s) : Bool

Check whether gradient-based optimizers may update this variable.

def Runtime.Variable.accumulateGradient {α : Type} [Context α] {s : Spec.Shape} [Add α] (v : Variable α s) (grad : Spec.Tensor α s) : Variable α s

Accumulate a gradient contribution into the variable.

If no gradient was set yet, this behaves like assignment. Otherwise it adds into the existing gradient (analogue of PyTorch param.grad += ...).

def Runtime.Variable.variableToString {α : Type} [ToString α] {s : Spec.Shape} (v : Variable α s) : String

Render a variable for debugging (includes value and optional gradient).

def Runtime.Variable.variableEq {α : Type} {s : Spec.Shape} (v₁ v₂ : Variable α s) : Bool

A simple equality check based on id and name.

def Runtime.Variable.hasShape {α : Type} {s : Spec.Shape} (_v : Variable α s) (expected_shape : Spec.Shape) : Bool

Check that the variable's shape equals the given shape.

def Runtime.Variable.variableNorm {α : Type} [Context α] {s : Spec.Shape} (v : Variable α s) : α

Compute the L2 norm of the variable value (Euclidean norm).

This is a small convenience helper for monitoring/debugging.

def Runtime.Variable.cloneVariable {α : Type} {s : Spec.Shape} (v : Variable α s) (new_id : ℕ) : Variable α s

Clone a variable under a new id, clearing the gradient.

def Runtime.Variable.detachVariable {α : Type} {s : Spec.Shape} (v : Variable α s) : Variable α s

Mark a variable as non-trainable and clear its gradient (inference-only).

def Runtime.Variable.registerInContext {α : Type} {s : Spec.Shape} (ctx : RuntimeContext α) (v : Variable α s) : RuntimeContext α

Register this variable's value in a RuntimeContext under its name.

def Runtime.Variable.getFromContext {α : Type} {s : Spec.Shape} [DecidableEq Spec.Shape] (ctx : RuntimeContext α) (v : Variable α s) : Option (Spec.Tensor α s)

Retrieve this variable's value from a RuntimeContext (with shape checking).

def Runtime.Variable.registerGradientInContext {α : Type} {s : Spec.Shape} (ctx : RuntimeContext α) (v : Variable α s) : RuntimeContext α

If v.gradient is present, register it in the RuntimeContext under v.name.

def Runtime.Variable.error {α : Type} [Zero α] (ctx : RuntimeContext α) (msg : String) : Variable α Spec.Shape.scalar

Create a sentinel scalar variable used to thread error messages through some pipelines.

This is mainly for demos / ergonomic error handling, not for proofs.

def Runtime.Variable.castShape {α : Type} {s₁ s₂ : Spec.Shape} (v : Variable α s₁) (h : s₁ = s₂) : Variable α s₂

Cast a variable to an equal shape.

This is the shape-indexed analogue of Eq.mp: given a proof s₁ = s₂, we can transport the value (and optional gradient) across the equality.