CPU tape values

The CPU tape is Tape (Spec.SomeTensor α): the one tape of NN.Runtime.Autograd.Engine.Tape, storing shape-erased CPU tensors. This module gives those values their GradValue instance and the typed constructors that every CPU operation is built from.

Design goals:

• Works for arbitrary Tensor α s shapes using Spec.SomeTensor values.
• Supports DAGs (shared subexpressions): gradients are accumulated by summation.
• Preserves typed tensors at operator boundaries and reports dynamic shape mismatches as errors.

This module defines and executes the tape; it does not by itself prove every registered VJP. Analytic correctness theorems for supported operations live under NN.Proofs.Autograd, while runtime checks cover the integration between those operations and the tape. For the imperative frontend over this engine, see NN.Runtime.Autograd.Torch.Core.

References (PyTorch / background reading):

• PyTorch docs: torch.autograd and "Autograd mechanics": https://pytorch.org/docs/stable/autograd.html https://pytorch.org/docs/stable/notes/autograd.html
• "micrograd" (small autograd engine, useful for intuition): https://github.com/karpathy/micrograd

def Runtime.Autograd.SomeTensor.add {α : Type} [TorchLean.Storage α] [Add α] (a b : Spec.SomeTensor α) : Result (Spec.SomeTensor α)

Accumulate two packed tensors by elementwise addition, with a dynamic shape check.

This is the heart of DAG support: if two different paths contribute gradients to the same parent, we sum the contributions.

@[instance_reducible]

instance Runtime.Autograd.instGradValueSomeTensorOfAdd {α : Type} [TorchLean.Storage α] [Add α] : GradValue (Spec.SomeTensor α)

CPU gradients are shape-erased tensors; ownership needs no bookkeeping.

@[instance_reducible]

instance Runtime.Autograd.instGradZeroSomeTensorOfZero {α : Type} [TorchLean.Storage α] [Zero α] : GradZero (Spec.SomeTensor α)

The CPU zero gradient of a value.

@[simp]

theorem Runtime.Autograd.GradValue.shape_someTensor {α : Type} [TorchLean.Storage α] [Add α] (v : Spec.SomeTensor α) : shape v = v.shape

@[simp]

theorem Runtime.Autograd.GradValue.retag_someTensor {α : Type} [TorchLean.Storage α] [Add α] (g v : Spec.SomeTensor α) (h : shape g = shape v) : retag g v h = Spec.SomeTensor.ofTensor (g.cast h)

@[simp]

theorem Runtime.Autograd.GradValue.check_someTensor {α : Type} [TorchLean.Storage α] [Add α] (g v : Spec.SomeTensor α) : check g v = Except.ok ()

@[simp]

theorem Runtime.Autograd.GradValue.add_someTensor {α : Type} [TorchLean.Storage α] [Add α] (a b : Spec.SomeTensor α) : add a b = SomeTensor.add a b

@[simp]

theorem Runtime.Autograd.GradValue.drop_someTensor {α β : Type} [TorchLean.Storage α] [Add α] (g : Spec.SomeTensor α) (rest : β) : drop g rest = rest

@[simp]

theorem Runtime.Autograd.GradZero.zerosLike_someTensor {α : Type} [TorchLean.Storage α] [Zero α] (v : Spec.SomeTensor α) : zerosLike v = Spec.SomeTensor.ofTensor (TorchLean.Tensor.full v.shape 0)

Tape Construction

The Tape namespace provides pure constructors for building a recorded computation graph. Each op appends exactly one node and returns the updated tape plus the new node id.

def Runtime.Autograd.Tape.leaf {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (t : Tape (Spec.SomeTensor α)) (value : TorchLean.Tensor α s) (name : Option String := none) (requiresGrad : Bool := true) : Tape (Spec.SomeTensor α) × ℕ

Add a leaf node (no parents).

PyTorch comparison: a tensor that enters the graph as a leaf (e.g. input or parameter value).

def Runtime.Autograd.Tape.requireValue {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (t : Tape (Spec.SomeTensor α)) (id : ℕ) : Result (TorchLean.Tensor α s)

Read a typed tensor value from a tape node id.

This is the main "dynamic check" boundary in the eager runtime:

• fails if the id is invalid, or
• fails if the stored runtime shape doesn't match the expected dependent shape s.

def Runtime.Autograd.Tape.requireGrad {α : Type} [TorchLean.Storage α] {τ : Spec.Shape} (dLdyAny : Spec.SomeTensor α) : Result (TorchLean.Tensor α τ)

Read a typed upstream gradient tensor from a packed tensor.

This is the backward analogue of Tape.requireValue: it checks that the upstream gradient has the expected shape τ and then performs the dependent cast.

@[inline]

def Runtime.Autograd.Tape.unary {α : Type} [TorchLean.Storage α] {σ τ : Spec.Shape} (t : Tape (Spec.SomeTensor α)) (opName : String) (xId : ℕ) (forward : TorchLean.Tensor α σ → TorchLean.Tensor α τ) (backward : TorchLean.Tensor α σ → TorchLean.Tensor α τ → TorchLean.Tensor α σ) : Result (Tape (Spec.SomeTensor α) × ℕ)

Generic constructor for unary ops.

You provide:

• forward : Tensor α σ → Tensor α τ
• backward : Tensor α σ → Tensor α τ → Tensor α σ (a VJP rule; note it may depend on the input)

The returned node inherits the parent's gradient flag and stores the forward value and a backward closure that checks the upstream gradient's shape and returns the parent contribution.

@[inline]

def Runtime.Autograd.Tape.binary {α : Type} [TorchLean.Storage α] {σ₁ σ₂ τ : Spec.Shape} (t : Tape (Spec.SomeTensor α)) (opName : String) (aId bId : ℕ) (forward : TorchLean.Tensor α σ₁ → TorchLean.Tensor α σ₂ → TorchLean.Tensor α τ) (backward : TorchLean.Tensor α σ₁ → TorchLean.Tensor α σ₂ → TorchLean.Tensor α τ → TorchLean.Tensor α σ₁ × TorchLean.Tensor α σ₂) : Result (Tape (Spec.SomeTensor α) × ℕ)

Record a binary operation with typed inputs and cotangents.

Input lookup, parent metadata, and backward contributions all follow the order a, then b. The backward function runs after the upstream shape check and receives both saved inputs.