Algebraic tape soundness

Tape-style (SSA/DAG) reverse-mode soundness (algebraic, backend-generic).

This is a backend-generic analogue of the tensor-tape soundness layer: it proves the global reverse-mode accumulation algorithm is sound assuming only commutative semiring laws.

This file lives under NN/Proofs/Autograd/Tape/Algebra/ because it is reused by both proof-only and runtime-link developments that target exact backends (e.g. ℚ).

PyTorch correspondence / citations

This corresponds to the high-level structure of PyTorch’s reverse-mode engine, but stated over an arbitrary commutative semiring so we can reuse it for exact backends. https://pytorch.org/docs/stable/autograd.html

def Proofs.Autograd.Algebra.TensorPack.dotList {α : Type} [TorchLean.Storage α] [CommSemiring α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss → TorchLean.TensorPack α ss → α

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

This is the algebraic analogue of Spec.dotList: it uses TensorAlgebra.dot for the backend α.

theorem Proofs.Autograd.Algebra.TensorPack.dotList_cast_left {α : Type} [TorchLean.Storage α] [CommSemiring α] {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)

dotList commutes with casting the left context along a shape-list equality.

theorem Proofs.Autograd.Algebra.TensorPack.dotList_add_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {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.

theorem Proofs.Autograd.Algebra.TensorPack.dotList_snoc {α : Type} [TorchLean.Storage α] [CommSemiring α] {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 + TensorAlgebra.dot a b

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

theorem Proofs.Autograd.Algebra.TensorPack.dotList_zero_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {ss : List Spec.Shape} (x : TorchLean.TensorPack α ss) : dotList x TorchLean.TensorPack.zero = 0

Dotting with the all-zero context on the right yields 0.

def Proofs.Autograd.Algebra.TensorPack.single {α : Type} [TorchLean.Storage α] [Zero α] {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (v : TorchLean.Tensor α s) : TorchLean.TensorPack α Γ

Sparse context with a single nonzero entry at idx (all other tensors are 0).

theorem Proofs.Autograd.Algebra.TensorPack.dotList_single {α : Type} [TorchLean.Storage α] [CommSemiring α] {Γ : List Spec.Shape} {s : Spec.Shape} (dx : TorchLean.TensorPack α Γ) (idx : Idx Γ s) (v : TorchLean.Tensor α s) : dotList dx (single idx v) = TensorAlgebra.dot (getIdx dx idx) v

single is adjoint to getIdx with respect to dotList.

Informally: ⟪dx, single idx v⟫ = ⟪getIdx dx idx, v⟫.

structure Proofs.Autograd.Algebra.NodeData (α : Type) [TorchLean.Storage α] (Δ : Type) (Γ : List Spec.Shape) (τ : Spec.Shape) : Type

Executable node payload (no correctness proof).

Δ is an extra non-differentiable environment threaded through evaluation (e.g. parameters, auxiliary data). The VJP returns gradients only for the differentiable context Γ.

• forward : TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ

  Evaluate the node from the current differentiable context and auxiliary data.

• jvp : TorchLean.TensorPack α Γ → TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ

  Propagate one tangent context through the node.

• vjp : TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ → TorchLean.TensorPack α Γ

  Pull an output cotangent back to the node's differentiable input context.

• validate : TorchLean.TensorPack α Γ → Δ → Except String Unit

  Optional runtime precondition, enforced by checked execution before evaluating this node.

structure Proofs.Autograd.Algebra.Node {α : Type} [TorchLean.Storage α] [CommSemiring α] (Δ : Type) (Γ : List Spec.Shape) (τ : Spec.Shape) extends Proofs.Autograd.Algebra.NodeData α Δ Γ τ : Type

Proof-carrying node: NodeData plus the local adjointness law.

The field correct is the algebraic version of the standard JVP/VJP inner-product law.

• forward : TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ
• jvp : TorchLean.TensorPack α Γ → TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ
• vjp : TorchLean.TensorPack α Γ → Δ → TorchLean.Tensor α τ → TorchLean.TensorPack α Γ
• validate : TorchLean.TensorPack α Γ → Δ → Except String Unit
• correct (x dx : TorchLean.TensorPack α Γ) (d : Δ) (δ : TorchLean.Tensor α τ) : TensorAlgebra.dot (self.jvp x dx d) δ = TensorPack.dotList dx (self.vjp x d δ)

  The node's JVP and VJP satisfy the local dot-product adjoint identity.

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

Executable-only graph: a snoc-list of NodeData.

• nil {α : Type} [TorchLean.Storage α] {Δ : Type} {Γ : List Spec.Shape} : GraphData α Δ Γ []

  A graph with no computed nodes; its context consists only of the inputs Γ.

• snoc {α : Type} [TorchLean.Storage α] {Δ : Type} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : GraphData α Δ Γ ss → NodeData α Δ (Γ ++ ss) τ → GraphData α Δ Γ (ss ++ [τ])

  Append one node whose inputs may use the original and previously computed values.

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

Evaluate a GraphData on an input context x, producing the full context Γ ++ ss.

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

Compute the JVP of eval, producing a tangent context of shape Γ ++ ss.

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

Reverse-mode accumulation on contexts (VJP), given a seed cotangent for Γ ++ ss.

Proof-carrying tape/SSA graphs.

Nodes are appended in topological order and may reference any previously computed value (fan-out and sharing are allowed). This mirrors the structure of PyTorch’s dynamic autograd graph, but with shape-typed contexts.

inductive Proofs.Autograd.Algebra.Graph {α : Type} [TorchLean.Storage α] [CommSemiring α] (Δ : Type) (Γ : List Spec.Shape) : List Spec.Shape → Type

A proof-carrying tape/SSA graph.

Nodes are appended in topological order and may reference any previously computed value.

• nil {α : Type} [TorchLean.Storage α] [CommSemiring α] {Δ : Type} {Γ : List Spec.Shape} : Graph Δ Γ []

  A graph with no computed nodes; its context consists only of the inputs Γ.

• snoc {α : Type} [TorchLean.Storage α] [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : Graph Δ Γ ss → Node Δ (Γ ++ ss) τ → Graph Δ Γ (ss ++ [τ])

  Append one locally correct node that may use the inputs and all preceding results.

def Proofs.Autograd.Algebra.Graph.toData {α : Type} [TorchLean.Storage α] [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} : Graph Δ Γ ss → GraphData α Δ Γ ss

Forget local correctness proofs, yielding an executable GraphData.

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

Evaluate a proof-carrying graph through its executable representation.

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

Propagate tangents with the same evaluator used by the executable graph.

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

Accumulate cotangents with the executable graph's reverse pass.

theorem Proofs.Autograd.Algebra.Graph.backprop_correct {α : Type} [TorchLean.Storage α] [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x dx : TorchLean.TensorPack α Γ) (d : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TensorPack.dotList (g.jvpCtx x dx d) seed = TensorPack.dotList dx (g.backpropCtx x d seed)

Global tape soundness (algebraic form).

Assuming each node satisfies its local adjointness law, backpropCtx is the adjoint of jvpCtx with respect to TensorPack.dotList.