A saved graph contains the tensors and locally prepared VJPs from one forward execution. Its dense reference pass is exactly the existing full graph backpropagation, including intermediate seeds and nodes whose incoming cotangent is zero.

inductive Proofs.Autograd.Algebra.SavedGraph (α : Type) [TorchLean.Storage α] (Γ : List Spec.Shape) : List Spec.Shape → Type

Locally saved node programs and their computed primal tensors in evaluation order.

• nil {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} : SavedGraph α Γ []
• snoc {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} {τ : Spec.Shape} (previous : SavedGraph α Γ ss) (prepared : PreparedNode α (Γ ++ ss) τ) (value : TorchLean.Tensor α τ) : SavedGraph α Γ (ss ++ [τ])

def Proofs.Autograd.Algebra.SavedGraph.ofGraph {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : SavedGraph α Γ ss × TensorContext α (Γ ++ ss)

Prepare a graph with one array context, saving only the inputs requested by each node.

def Proofs.Autograd.Algebra.SavedGraph.lowerChecked {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : Except String (SavedGraph α Γ ss × TensorContext α (Γ ++ ss))

Checked preparation validates a node before evaluating or recording its primal.

theorem Proofs.Autograd.Algebra.SavedGraph.lowerChecked_eq {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (result : SavedGraph α Γ ss × TensorContext α (Γ ++ ss)) (checked : lowerChecked graph inputs data = Except.ok result) : result = ofGraph graph inputs data

Successful checked preparation produces the same saved programs as pure preparation.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_context_eq {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : (ofGraph graph inputs data).2 = TensorContext.ofPack (graph.eval inputs data)

Prepared graph primals are the original graph evaluator's complete context.

def Proofs.Autograd.Algebra.SavedGraph.backpropDense {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} [Add α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α (Γ ++ ss)

The dense reference reverse pass preserves the original node and local addition order.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_backpropDense {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} [Add α] {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (ofGraph graph inputs data).1.backpropDense seed = graph.backpropAllCtx inputs data seed

Saved VJPs compute precisely full graph backpropagation for every seed pack.