Soundness

Tape-style (SSA/DAG) reverse-mode soundness for the proved-correct layer.

We model a dynamic graph as a sequence of nodes that may reference any previously computed values (so sharing/fan-out is allowed). For each node we assume a local JVP/VJP adjointness law, then prove the global reverse-mode accumulation algorithm is sound.

This is a proof-only layer; the runtime engine in NN.Runtime.Autograd.Engine is an executable implementation of the same idea.

PyTorch correspondence / citations

• This file is the proof analogue of PyTorch’s dynamic autograd engine building a tape of nodes during the forward pass and running a reverse pass that accumulates gradients at shared inputs. https://pytorch.org/docs/stable/autograd.html

References (background):

• Reverse-mode AD as backpropagation on a computation graph is standard; see e.g. Baydin et al. (JMLR 2018) for an overview and terminology (JVP/VJP, duality, etc.).

def Proofs.Autograd.TensorPack.dotList {ss : List Spec.Shape} : TorchLean.TensorPack ℝ ss → TorchLean.TensorPack ℝ ss → ℝ

Dot product over contexts: sum of per-entry tensor dot products.

Informally: dotList xs ys is the “context inner product” used to state global adjointness for tape evaluation and backprop.

theorem Proofs.Autograd.TensorPack.dotList_eq_algebra_dotList {Γ : List Spec.Shape} (x y : TorchLean.TensorPack ℝ Γ) : dotList x y = Algebra.TensorPack.dotList x y

At ℝ the context dot product agrees with the backend-generic one in Algebra, entry by entry through dot_eq_tensorAlgebra_dot.

structure Proofs.Autograd.Node (Γ : List Spec.Shape) (τ : Spec.Shape) : Type

A node with local JVP/VJP and an adjointness proof against the tensor dot product.

• forward : TorchLean.TensorPack ℝ Γ → TorchLean.Tensor ℝ τ

  The node's forward pass, reading the whole context and producing one output tensor.

• jvp : TorchLean.TensorPack ℝ Γ → TorchLean.TensorPack ℝ Γ → TorchLean.Tensor ℝ τ

  Forward-mode derivative: a basepoint and a tangent context give an output tangent.

• vjp : TorchLean.TensorPack ℝ Γ → TorchLean.Tensor ℝ τ → TorchLean.TensorPack ℝ Γ

  Reverse-mode derivative: a basepoint and an output cotangent give a context cotangent.

• correct (x dx : TorchLean.TensorPack ℝ Γ) (δ : TorchLean.Tensor ℝ τ) : Spec.dot (self.jvp x dx) δ = TensorPack.dotList dx (self.vjp x δ)

  vjp is the adjoint of jvp with respect to the tensor dot product. Every node in the tape carries this proof, so backpropagation over a whole graph is a composition of adjoints rather than a separate correctness argument.

• validate : TorchLean.TensorPack ℝ Γ → Except String Unit

  Runtime precondition metadata, preserved by the algebraic bridge; pure semantics ignore it.

• prepare? : Option { prepare : Algebra.TensorLookup ℝ Γ → Algebra.PreparedNode ℝ Γ τ // ∀ (ctx : TorchLean.TensorPack ℝ Γ), (prepare (Algebra.TensorLookup.ofPack ctx)).toPreparedPrograms = { value := fun (x : Unit) => self.forward ctx, vjp := self.vjp ctx, validate := fun (x : Unit) => self.validate ctx } }

  Certified local preparation, retained by both directions of the algebraic bridge.

inductive Proofs.Autograd.Graph (Γ : List Spec.Shape) : List Spec.Shape → Type

A tape/SSA graph: nodes are appended in topological order and may reference any previous value.

• nil {Γ : List Spec.Shape} : Graph Γ []
• snoc {Γ ss : List Spec.Shape} {τ : Spec.Shape} : Graph Γ ss → Node (Γ ++ ss) τ → Graph Γ (ss ++ [τ])

def Proofs.Autograd.Graph.eval {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) : TorchLean.TensorPack ℝ (Γ ++ ss)

Evaluate a tape/graph, returning the full context (inputs ++ intermediates).

def Proofs.Autograd.Graph.jvpCtx {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x dx : TorchLean.TensorPack ℝ Γ) : TorchLean.TensorPack ℝ (Γ ++ ss)

Evaluate the JVP (“forward-mode tangent”) of a graph, producing tangents for all values in the extended context Γ ++ ss.

def Proofs.Autograd.Graph.backpropCtx {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) : TorchLean.TensorPack ℝ Γ

Reverse-mode backpropagation on a tape/graph, returning gradients for the inputs Γ.

This is the proof model of what PyTorch calls “running backward” starting from an output seed cotangent and accumulating gradients at shared parents.

def Proofs.Autograd.Node.toAlgebra {Γ : List Spec.Shape} {τ : Spec.Shape} (node : Node Γ τ) : Algebra.Node Unit Γ τ

Embed an analytic node as an algebraic node over ℝ with a trivial environment.

def Proofs.Autograd.Graph.toAlgebra {Γ ss : List Spec.Shape} : Graph Γ ss → Algebra.Graph Unit Γ ss

Embed an analytic graph as an algebraic graph over ℝ with a trivial environment.

theorem Proofs.Autograd.Graph.eval_toAlgebra {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) : g.toAlgebra.eval x () = g.eval x

Embedding preserves evaluation.

theorem Proofs.Autograd.Graph.jvpCtx_toAlgebra {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x dx : TorchLean.TensorPack ℝ Γ) : g.toAlgebra.jvpCtx x dx () = g.jvpCtx x dx

Embedding preserves the JVP.

theorem Proofs.Autograd.Graph.backpropCtx_toAlgebra {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) : g.toAlgebra.backpropCtx x () seed = g.backpropCtx x seed

Embedding preserves the reverse pass.

theorem Proofs.Autograd.Graph.backprop_correct {Γ ss : List Spec.Shape} (g : Graph Γ ss) (x dx : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.TensorPack ℝ (Γ ++ ss)) : TensorPack.dotList (g.jvpCtx x dx) seed = TensorPack.dotList dx (g.backpropCtx x seed)

Global tape soundness: if each node satisfies a local JVP/VJP adjointness law, then the global reverse-mode accumulation algorithm (backpropCtx) is correct.

Informally: for any input perturbation dx and any output seed cotangent seed,

⟪JVP(g, x, dx), seed⟫ = ⟪dx, backprop(g, x, seed)⟫.

This is the formal analogue of PyTorch’s guarantee that backward() computes vector–Jacobian products and accumulates them through a dynamic DAG/tape. It is the ℝ, Δ := Unit instance of Algebra.Graph.backprop_correct.