Link

Link the executable runtime tape (Runtime.Autograd.Tape) to the shape-indexed SSA/DAG models in Proofs.Autograd.Algebra.

GraphData stores executable forward, JVP, and VJP functions without derivative laws. Graph extends that representation with the local adjointness law used by its global backpropagation theorem. Lowering places the stored VJP into each runtime node's backward closure.

What is proved here

• Forward-pass correspondence: lowerGraphToTape and lowerGraphDataToTape produce the same values as Graph.eval and GraphData.eval, respectively. Their ctx_eq_eval and values_eq lemmas show that the returned context and runtime tape store those values in the same order.
• Backward-pass correspondence: running the runtime dense reverse loop Tape.backwardDenseFrom on a lowered tape matches the graph's stored reverse program backpropAllCtx (backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx and its GraphData variant). For GraphData, this is an implementation-equivalence result. For Graph, it can be combined with Graph.backprop_correct to obtain derivative correctness.

The core invariant making the runtime reverse loop well-founded is that lowered nodes only emit contributions to earlier node ids (pid < id).

PyTorch correspondence / citations

This is analogous to lowering a graph representation to an executable autograd tape whose nodes carry backward closures (PyTorch does this internally for the eager autograd engine). https://pytorch.org/docs/stable/autograd.html

def Proofs.Autograd.Algebra.Graph.addLeaves {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) {Γ : List Spec.Shape} : TorchLean.TensorPack α Γ → Runtime.Autograd.Tape (Spec.SomeTensor α)

Extend a tape with leaf nodes for every tensor in the input context Γ.

Each leaf has requiresGrad = true and an empty backward contribution array, so the runtime loop treats them as gradient accumulation slots but never produces parent contributions from them.

def Proofs.Autograd.Algebra.Graph.leafNodeOfSomeTensor {α : Type} [TorchLean.Storage α] (v : Spec.SomeTensor α) : Runtime.Autograd.Node (Spec.SomeTensor α)

Turn a shape-erased tensor into a runtime leaf node.

This is the node-level counterpart of addLeaves: it has no parents and contributes nothing in backward.

Result equations

Result is Except String. The runtime backward functions are written with do notation, so proofs about them repeatedly need the unfolding equations for bind, pure, throw and Except.map. They are stated once here and used with simp only instead of unfolding the Monad instances by hand.

theorem Proofs.Autograd.Algebra.Graph.result_bind_ok {β γ : Type} (a : β) (f : β → Runtime.Autograd.Result γ) : Except.ok a >>= f = f a

Binding a successful Result applies the continuation.

theorem Proofs.Autograd.Algebra.Graph.result_bind_error {β γ : Type} (e : String) (f : β → Runtime.Autograd.Result γ) : Except.error e >>= f = Except.error e

Binding a failed Result propagates the error.

theorem Proofs.Autograd.Algebra.Graph.result_pure_eq_ok {β : Type} (a : β) : pure a = Except.ok a

pure in Result is Except.ok.

theorem Proofs.Autograd.Algebra.Graph.result_throw_eq_error {β : Type} (e : String) : throw e = Except.error e

throw in Result is Except.error.

theorem Proofs.Autograd.Algebra.Graph.result_map_ok {β γ : Type} (f : β → γ) (a : β) : Except.map f (Except.ok a) = Except.ok (f a)

Except.map on a successful Result.

theorem Proofs.Autograd.Algebra.Graph.result_map_error {β γ : Type} (f : β → γ) (e : String) : Except.map f (Except.error e) = Except.error e

Except.map on a failed Result.

def Proofs.Autograd.Algebra.Graph.BackwardPidsLt {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) : Prop

Backward closures of t only point backwards: every contribution emitted by the node stored at id targets a node id strictly smaller than id. This is the invariant that makes the dense reverse loop well-founded; lowerGraphDataToTape_backward_pids_lt_id establishes it for lowered tapes, including those of proved graphs, which lower through Graph.toData.

theorem Proofs.Autograd.Algebra.Graph.shape_getElem_toShapeErasedArray {α : Type} [TorchLean.Storage α] {ss : List Spec.Shape} (xs : TorchLean.TensorPack α ss) {i : ℕ} (hi : i < ss.length) : xs.toShapeErasedArray[i].shape = ss.get ⟨i, hi⟩

Each entry of toShapeErasedArray carries the shape recorded at its position of ss.

theorem Proofs.Autograd.Algebra.Graph.size_addLeaves {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) {Γ : List Spec.Shape} (x : TorchLean.TensorPack α Γ) : (addLeaves t x).nodes.size = t.nodes.size + Γ.length

addLeaves grows the tape by exactly Γ.length nodes.

theorem Proofs.Autograd.Algebra.Graph.nodes_addLeaves {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) {Γ : List Spec.Shape} (x : TorchLean.TensorPack α Γ) : (addLeaves t x).nodes = t.nodes ++ Array.map leafNodeOfSomeTensor x.toShapeErasedArray

addLeaves appends leafNodeOfSomeTensor nodes for each input tensor, in order.

theorem Proofs.Autograd.Algebra.Graph.addLeaves_values {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) {Γ : List Spec.Shape} (x : TorchLean.TensorPack α Γ) : Array.map (fun (node : Runtime.Autograd.Node (Spec.SomeTensor α)) => node.value) (addLeaves t x).nodes = Array.map (fun (node : Runtime.Autograd.Node (Spec.SomeTensor α)) => node.value) t.nodes ++ x.toShapeErasedArray

Value projection of nodes_addLeaves: node.value agrees with toShapeErasedArray for added leaves.

def Proofs.Autograd.Algebra.Graph.lowerNode {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (name : Option String) (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (d : Δ) : Runtime.Autograd.Node (Spec.SomeTensor α)

Runtime node produced by lowering one graph node.

The node stores the forward value and wraps the stored vjp in a runtime backward closure that checks the shape of the upstream cotangent and emits one contribution per entry of the node's input context, indexed from 0. The name only serves debugging output.

@[simp]

theorem Proofs.Autograd.Algebra.Graph.lowerNode_value {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (name : Option String) (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (d : Δ) : (lowerNode name node ctx d).value = Spec.SomeTensor.ofTensor (node.forward ctx d)

The lowered node stores the node's forward value.

@[simp]

theorem Proofs.Autograd.Algebra.Graph.lowerNode_requiresGrad {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (name : Option String) (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (d : Δ) : (lowerNode name node ctx d).requiresGrad = true

Lowered nodes always take part in gradient accumulation.

theorem Proofs.Autograd.Algebra.Graph.lowerNode_backward_of_shape {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (name : Option String) (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (d : Δ) (v : Spec.SomeTensor α) (h : v.shape = τ) : (lowerNode name node ctx d).backward v = Except.ok ((node.vjp ctx d (v.cast h)).toIndexedShapeErasedArray 0)

On an upstream cotangent of the right shape, the lowered backward runs the stored vjp.

theorem Proofs.Autograd.Algebra.Graph.lowerNode_backward_of_ne {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (name : Option String) (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (d : Δ) (v : Spec.SomeTensor α) (h : v.shape ≠ τ) : (lowerNode name node ctx d).backward v = Except.error "autograd: upstream gradient shape mismatch"

On an upstream cotangent of the wrong shape, the lowered backward fails.

def Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : Runtime.Autograd.Tape (Spec.SomeTensor α) × TorchLean.TensorPack α (Γ ++ ss)

Lower an executable graph (GraphData) to a runtime tape by evaluating forward nodes and storing each node's vjp program in its runtime backward closure.

PyTorch analogy: this corresponds to building a tape of autograd nodes during the forward pass, where each node stores enough information to compute parent contributions when given an upstream cotangent.

Forward-pass correspondence

The next lemmas show that lowerGraphDataToTape preserves executable forward semantics, and that the resulting runtime tape contains exactly the evaluated context as shape-erased tensors in order.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_ctx_eq_eval {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : (lowerGraphDataToTape g x d).2 = g.eval x d

The context returned by lowerGraphDataToTape agrees with GraphData.eval.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_values_eq {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : Array.map (fun (node : Runtime.Autograd.Node (Spec.SomeTensor α)) => node.value) (lowerGraphDataToTape g x d).1.nodes = (lowerGraphDataToTape g x d).2.toShapeErasedArray

The lowered tape's .value array is GraphData.eval with shapes erased in the same order.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_nodes_size {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : (lowerGraphDataToTape g x d).1.nodes.size = Γ.length + ss.length

Size bookkeeping: the lowered tape contains one runtime node for each element of Γ ++ ss.

def Proofs.Autograd.Algebra.Graph.lowerGraphToTape {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : Runtime.Autograd.Tape (Spec.SomeTensor α) × TorchLean.TensorPack α (Γ ++ ss)

Lower a proved graph (Graph) to a runtime tape: the tape lowerGraphDataToTape builds for the executable graph g.toData. Both interfaces share one lowering; the local adjointness proofs a Graph carries are used only by the theorems about the tape.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphToTape_ctx_eq_eval {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : (g.lowerGraphToTape x d).2 = g.eval x d

The context returned by lowerGraphToTape agrees with the proved Graph.eval.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphToTape_values_eq {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : Array.map (fun (node : Runtime.Autograd.Node (Spec.SomeTensor α)) => node.value) (g.lowerGraphToTape x d).1.nodes = (g.lowerGraphToTape x d).2.toShapeErasedArray

The lowered tape's .value array is Graph.eval with shapes erased in the same order.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphToTape_nodes_size {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : (g.lowerGraphToTape x d).1.nodes.size = Γ.length + ss.length

Size bookkeeping: lowerGraphToTape produces Γ.length + ss.length runtime nodes.

Full backpropagation (dense) for proofs and runtime

The runtime engine computes a dense gradient array, accumulating cotangents for every node in the tape (inputs and intermediates). The following definitions connect that behavior to the proved backpropagation semantics.

def Proofs.Autograd.Algebra.GraphData.backpropAllCtx {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α (Γ ++ ss)

"Full" backpropagation for GraphData: gradients for every value in Γ ++ ss, including inputs.

Peel off the last node, apply its VJP to the seed on that node, add the result into the previous seed, and recurse. Only [Add α] is needed. Graph.backpropAllCtx runs this program on the executable graph g.toData.

def Proofs.Autograd.Algebra.Graph.backpropAllCtx {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α (Γ ++ ss)

"Full" backpropagation for a proof-carrying graph: gradients for every value in Γ ++ ss, including inputs. It runs the executable reverse program of g.toData, exactly as Graph.eval and Graph.backpropCtx run its forward and inputs-only reverse programs.