Checked TypedGraph compilation saves local node programs and an indexed primal context. The all-seeds reverse pass preserves complete dense gradient semantics. Single-output differentiation visits dependencies of that output when storage equality and certified compact support are available. Other cases retain conservative traversal. The explicit Tape adapter connects the dense pass to the runtime tape engine.

def Proofs.Autograd.Algebra.SavedGraph.toTape {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (inputs : TorchLean.TensorPack α Γ) : Runtime.Autograd.Tape (Spec.SomeTensor α)

Adapt saved programs to the runtime tape representation.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_toTape {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : (ofGraph graph inputs data).1.toTape inputs = (Graph.lowerGraphDataToTape graph inputs data).1

Saved programs produce the same runtime tape, including its closures.

theorem Proofs.Autograd.Algebra.SavedGraph.lowerChecked_toTape {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : Except.map (fun (result : SavedGraph α Γ ss × TensorContext α (Γ ++ ss)) => (result.1.toTape inputs, result.2)) (lowerChecked graph inputs data) = Runtime.Autograd.TypedGraph.lowerToArrayChecked graph inputs data

Checked saved programs and indexed lowering have the same errors, tape and context.

structure Runtime.Autograd.TypedGraph.Compiled (α : Type) [TorchLean.Storage α] (Γ ss : List Spec.Shape) : Type

One checked execution, retaining locally saved VJPs and indexed primal tensors.

• inputs : TorchLean.TensorPack α Γ

  Original input tensors, needed only by the raw Tape adapter.

• saved : Proofs.Autograd.Algebra.SavedGraph α Γ ss

  Programs for this execution in graph order.

• context : Proofs.Autograd.Algebra.TensorContext α (Γ ++ ss)

  Input and intermediate values in graph order.

def Runtime.Autograd.TypedGraph.compileChecked {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : Result (Compiled α Γ ss)

Validate and evaluate each node once while recording its certified local reverse program.

def Runtime.Autograd.TypedGraph.Compiled.toTape {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (compiled : Compiled α Γ ss) : Tape (Spec.SomeTensor α)

Materialize the runtime tape when required by another engine consumer.

def Runtime.Autograd.TypedGraph.Compiled.backwardDenseFrom {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} [Add α] (compiled : Compiled α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : Array (Spec.SomeTensor α)

Compute every gradient from a typed seed pack, retaining the dense floating-point order.

def Runtime.Autograd.TypedGraph.Compiled.backwardDenseAllFrom {α : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} [Add α] [Zero α] {shape : Spec.Shape} (compiled : Compiled α Γ ss) (output : Proofs.Idx (Γ ++ ss) shape) (seed : TorchLean.Tensor α shape) : Array (Spec.SomeTensor α)

Seed one output and traverse its certified support when storage equality is available. Opaque VJPs visit the full prefix; carriers without equality use the dense reference.

theorem Runtime.Autograd.TypedGraph.compileChecked_eq_lowerToTapeChecked {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) : Except.map (fun (compiled : Compiled α Γ ss) => (compiled.toTape, compiled.context.toPack)) (compileChecked graph inputs data) = lowerToTapeChecked graph inputs data

Saved execution and tape lowering agree on failures, the tape and every forward value.

theorem Runtime.Autograd.TypedGraph.compileChecked_context {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (compiled : Compiled α Γ ss) (checked : compileChecked graph inputs data = Except.ok compiled) : compiled.context.toPack = graph.eval inputs data

Successful compilation has the original complete forward context.

theorem Runtime.Autograd.TypedGraph.compileChecked_backwardDenseFrom {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (compiled : Compiled α Γ ss) (checked : compileChecked graph inputs data = Except.ok compiled) (seed : TorchLean.TensorPack α (Γ ++ ss)) : compiled.backwardDenseFrom seed = (graph.backpropAllCtx inputs data seed).toShapeErasedArray

Compiled reverse execution agrees with full graph backpropagation for every seed pack.

theorem Runtime.Autograd.TypedGraph.compileChecked_backwardDenseFrom_eq_tape {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (graph : Proofs.Autograd.Algebra.GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (compiled : Compiled α Γ ss) (checked : compileChecked graph inputs data = Except.ok compiled) (seed : TorchLean.TensorPack α (Γ ++ ss)) : Except.ok (compiled.backwardDenseFrom seed) = (Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape graph inputs data).1.backwardDenseFrom seed.toShapeErasedArray

The fast backward interface also agrees with the existing dense runtime Tape engine.