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_cast_left {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (x : TorchLean.TensorPack ℝ ss₁) (y : TorchLean.TensorPack ℝ ss₂) : dotList (TorchLean.TensorPack.cast h x) y = dotList x (TorchLean.TensorPack.cast ⋯ y)

A context cast can be moved from one side of the context dot product to the other.

Casts appear whenever two tapes are composed and their context shape lists are only propositionally equal; without this lemma every adjointness proof would have to cases the equality by hand.

theorem Proofs.Autograd.TensorPack.dotList_add_right {ss : List Spec.Shape} (x y z : TorchLean.TensorPack ℝ ss) : dotList x (y.add z) = dotList x y + dotList x z

dotList is linear in its right argument with respect to TorchLean.TensorPack.add.

Informally: ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ for contexts.

theorem Proofs.Autograd.TensorPack.dotList_snoc {ss : List Spec.Shape} {τ : Spec.Shape} (x y : TorchLean.TensorPack ℝ ss) (a b : TorchLean.Tensor ℝ τ) : dotList (x.snoc a) (y.snoc b) = dotList x y + Spec.dot a b

dotList respects appending: dot of two snoced contexts splits into prefix + last entry.

Informally: ⟪(x,a), (y,b)⟫ = ⟪x,y⟫ + ⟪a,b⟫.

theorem Proofs.Autograd.TensorPack.dot_full_zero_right {s : Spec.Shape} (a : TorchLean.Tensor ℝ s) : Spec.dot a (TorchLean.Tensor.full s 0) = 0

Dotting any tensor with a zero-filled tensor gives 0.

This is the tensor-level fact used to show that “one-hot” cotangents behave as expected.

theorem Proofs.Autograd.TensorPack.dotList_zero_right {ss : List Spec.Shape} (x : TorchLean.TensorPack ℝ ss) : dotList x TorchLean.TensorPack.zero = 0

dotList x 0 = 0 for the all-zero context.

def Proofs.Autograd.TensorPack.single {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (v : TorchLean.Tensor ℝ s) : TorchLean.TensorPack ℝ Γ

Build a sparse context with a single nonzero entry at idx and zeros elsewhere.

This is used to express “one-hot” cotangents when proving local-to-global backprop correctness.

theorem Proofs.Autograd.TensorPack.dotList_single {Γ : List Spec.Shape} {s : Spec.Shape} (dx : TorchLean.TensorPack ℝ Γ) (idx : Idx Γ s) (v : TorchLean.Tensor ℝ s) : dotList dx (single idx v) = Spec.dot (getIdx dx idx) v

single idx v is the “one-hot” context with value v at idx, and zeros elsewhere.

This lemma says the context dot product against single idx v picks out the corresponding entry of dx:

⟪dx, single idx v⟫ = ⟪dx[idx], v⟫.

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.

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.

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.