Backpropagation

Reverse-mode is implemented by traversing node ids in reverse order. Each node's backward closure produces parent-gradient contributions, which we accumulate by elementwise summation.

Two traversal variants live here, and it matters which one a caller runs:

• backwardDense (and its totalized form backwardDenseAll) is what the eager trainer executes. It keeps an Option per node and runs a node's VJP only when that node has received a cotangent, so disconnected nodes are never visited. backwardDenseAll then fills the unvisited slots with explicit zero tensors. Skipping is deliberate: on Float, feeding a synthetic zero cotangent through the VJP of a singular value can produce NaN via 0 * (1/0).
• backwardDenseFrom starts from a total gradient array and runs every node's VJP. It is the variant the proof layer reasons about directly (Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx).

The two agree whenever every VJP on the tape sends a zero cotangent to zero contributions of the parents' shapes; that is Proofs.Autograd.Algebra.Graph.ZeroPreserving in NN.Proofs.Autograd.Runtime.Link.BackwardDense, where backwardDenseAll_eq_backwardDenseFrom is proved, and NN.Proofs.Autograd.Runtime.Link.BackwardDenseGraph, where it is instantiated for every tape produced by lowerGraphToTape.

def Runtime.Autograd.Tape.addGradDense {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (grads : Array (Option (Spec.SomeTensor α))) (id : ℕ) (g : Spec.SomeTensor α) : Result (Array (Option (Spec.SomeTensor α)))

Internal helper: add a single parent gradient contribution into the dense optional gradient array.

This is where we implement PyTorch-style accumulation for DAGs: if multiple children contribute to the same parent id, we sum the contributions.

The dense array entry is none until we first reach a node during reverse traversal.

def Runtime.Autograd.Tape.backwardDense {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (outId : ℕ) (seed : Spec.SomeTensor α) : Result (Array (Option (Spec.SomeTensor α)))

Reverse-mode backpropagation producing a dense array of optional gradients.

• The result array has length t.nodes.size.
• Entry id is some g if the node was reached from outId during reverse traversal, otherwise none.
• When multiple paths contribute to the same node, we sum gradients via SomeTensor.add.
• A node's VJP runs only if the node was reached; see the section docstring for why. The proof layer names this per-node step backwardDenseStep and proves backwardDense is the reverse fold of it.

This is the variant the eager trainer executes (through backwardDenseAll). It is loosely analogous to PyTorch's autograd engine walking the dynamic graph and accumulating .grad for leaf tensors, but we keep gradients for every node id rather than leaves alone. That makes the runtime easier to debug and gives proof-bridge code direct access to intermediate cotangents.

Reference (PyTorch): https://pytorch.org/docs/stable/notes/autograd.html

def Runtime.Autograd.Tape.addGradAll {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (grads : Array (Spec.SomeTensor α)) (id : ℕ) (g : Spec.SomeTensor α) : Result (Array (Spec.SomeTensor α))

Internal helper: like addGradDense, but assumes the gradient array is total (no Option).

This is used by the proof-friendly backwardDenseFrom* variants, which start from an explicit gradient tensor for every node.

def Runtime.Autograd.Tape.backwardDenseFromStep {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (acc : Array (Spec.SomeTensor α)) (id : ℕ) : Result (Array (Spec.SomeTensor α))

One reverse-mode backprop step at a single node id, updating a total dense gradient array.

Precondition by convention: acc has one entry per tape node, and every entry has the matching node shape. The function checks those conditions dynamically and returns an error if a caller violates them. This makes it suitable as the small proof-friendly step used by backwardDenseFromLoop.

def Runtime.Autograd.Tape.backwardDenseFromLoop {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) : ℕ → Array (Spec.SomeTensor α) → Result (Array (Spec.SomeTensor α))

Reverse-mode accumulation over the first n nodes in reverse order.

The recursion visits node ids n-1, n-2, ..., 0. Passing n = t.nodes.size therefore traverses the entire tape. This structurally recursive loop is also used by typed graph sessions after lowering.

def Runtime.Autograd.Tape.backwardDenseFrom {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (grads0 : Array (Spec.SomeTensor α)) : Result (Array (Spec.SomeTensor α))

Reverse-mode accumulation starting from an explicit dense gradient array.

This is the variant the proofs reason about directly: it always runs every node's VJP (in reverse order) and keeps a gradient tensor for every node id. The eager trainer does not call it; it calls backwardDenseAll, which agrees with this function on zero-preserving tapes (Proofs.Autograd.Algebra.Graph.backwardDenseAll_eq_backwardDenseFrom).

def Runtime.Autograd.Tape.backwardDenseAll {α : Type} [TorchLean.Storage α] [Add α] [Zero α] (t : Tape α) (outId : ℕ) (seed : Spec.SomeTensor α) : Result (Array (Spec.SomeTensor α))

Reverse-mode accumulation that returns a dense gradient array for every node id.

Propagation uses backwardDense, so local VJP closures run only for nodes reached from outId. The optional result is then totalized with explicit zero tensors for disconnected nodes. This is necessary at singular forward values: applying a disconnected VJP to a synthetic zero cotangent can manufacture NaN through expressions such as 0 * (1 / 0), even though the mathematical gradient of the selected output with respect to that node is zero.

This is the entry point the eager trainer executes. On zero-preserving tapes (in particular every tape produced by lowerGraphToTape) it returns exactly what backwardDenseFrom returns from the one-hot seed array; see NN.Proofs.Autograd.Runtime.Link.BackwardDense.

def Runtime.Autograd.Tape.denseToHashMap {α : Type} [TorchLean.Storage α] (grads : Array (Option (Spec.SomeTensor α))) : Std.HashMap ℕ (Spec.SomeTensor α)

Convert the optional dense gradient array returned by backwardDense into a sparse HashMap.

Only entries that are present (some (some g)) are kept. The result records exactly the nodes reached by reverse-mode propagation.

def Runtime.Autograd.Tape.backward {α : Type} [TorchLean.Storage α] [Add α] (t : Tape α) (outId : ℕ) (seed : Spec.SomeTensor α) : Result (Std.HashMap ℕ (Spec.SomeTensor α))

Reverse-mode backpropagation returning a HashMap of only the nodes that received gradients.

This is the sparse public form of backwardDense: it computes dense gradients first, then drops nodes that did not receive a gradient.

def Runtime.Autograd.Tape.backwardScalar {α : Type} [TorchLean.Storage α] [Add α] [One α] (t : Tape α) (outId : ℕ) : Result (Std.HashMap ℕ (Spec.SomeTensor α))

Backpropagate from a scalar output with seed gradient 1.

PyTorch analogy: loss.backward() when loss is a scalar.