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. ℚ).

In particular, it can be instantiated for exact backends such as ℚ.

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

inductive Proofs.Autograd.Algebra.TList (α : Type) : List Spec.Shape → Type

A heterogeneous list of tensors indexed by a list of shapes.

TList α Γ is the algebraic (backend-generic) version of the typed tape context: it stores one tensor of each shape in Γ.

PyTorch analogue: the engine carries a runtime list of saved tensors for backward; here Γ tracks the shapes statically.

• nil {α : Type} : TList α []
• cons {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : Spec.Tensor α s → TList α ss → TList α (s :: ss)

def Proofs.Autograd.Algebra.TList.get {α : Type} {ss : List Spec.Shape} : TList α ss → (i : Fin ss.length) → Spec.Tensor α (ss.get i)

Get the ith tensor from a context, with its shape tracked by List.get.

@[simp]

theorem Proofs.Autograd.Algebra.TList.get_cons_zero {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} (x : Spec.Tensor α s) (xs : TList α ss) (h : 0 < (s :: ss).length) : (cons x xs).get ⟨0, h⟩ = x

@[simp]

theorem Proofs.Autograd.Algebra.TList.get_cons_succ {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} (x : Spec.Tensor α s) (xs : TList α ss) (i : ℕ) (h : i.succ < (s :: ss).length) : (cons x xs).get ⟨i.succ, h⟩ = xs.get ⟨i, ⋯⟩

def Proofs.Autograd.Algebra.TList.zero {α : Type} [Zero α] {ss : List Spec.Shape} : TList α ss

All-zero context (fills each tensor entry with zeros).

def Proofs.Autograd.Algebra.TList.add {α : Type} [Add α] {ss : List Spec.Shape} : TList α ss → TList α ss → TList α ss

Pointwise addition of two contexts of the same shape list.

def Proofs.Autograd.Algebra.TList.scale {α : Type} [Mul α] (c : α) {ss : List Spec.Shape} : TList α ss → TList α ss

Scale every tensor in a context by the same scalar.

This is the context-level analogue of scaleSpec. It lives beside zero and add because several proof layers need scalar multiplication on heterogeneous parameter/gradient packs, not just the training-step file.

def Proofs.Autograd.Algebra.TList.sub {α : Type} [Sub α] {ss : List Spec.Shape} : TList α ss → TList α ss → TList α ss

Pointwise subtraction of two contexts with the same shape list.

This is the context-level analogue of subSpec; it is used to state pure optimizer updates over an entire typed parameter context.

def Proofs.Autograd.Algebra.TList.snoc {α : Type} {τ : Spec.Shape} {ss : List Spec.Shape} : TList α ss → Spec.Tensor α τ → TList α (ss ++ [τ])

Append a tensor to the end of a context.

def Proofs.Autograd.Algebra.TList.unsnoc {α : Type} {τ : Spec.Shape} {ss : List Spec.Shape} : TList α (ss ++ [τ]) → TList α ss × Spec.Tensor α τ

Split a context of shape list ss ++ [τ] into its prefix and last tensor.

def Proofs.Autograd.Algebra.TList.cast {α : Type} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : TList α ss₁) : TList α ss₂

Cast a context along an equality of shape lists.

@[simp]

theorem Proofs.Autograd.Algebra.TList.cast_rfl {α : Type} {ss : List Spec.Shape} (xs : TList α ss) : cast ⋯ xs = xs

@[simp]

theorem Proofs.Autograd.Algebra.TList.cast_cast {α : Type} {ss₁ ss₂ ss₃ : List Spec.Shape} (h₁ : ss₁ = ss₂) (h₂ : ss₂ = ss₃) (xs : TList α ss₁) : cast h₂ (cast h₁ xs) = cast ⋯ xs

@[simp]

theorem Proofs.Autograd.Algebra.TList.cast_symm {α : Type} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : TList α ss₁) : cast ⋯ (cast h xs) = xs

def Proofs.Autograd.Algebra.TList.dotList {α : Type} [CommSemiring α] {ss : List Spec.Shape} : TList α ss → TList α 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.TList.dotList_cast_left {α : Type} [CommSemiring α] {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (x : TList α ss₁) (y : TList α ss₂) : (cast h x).dotList y = x.dotList (cast ⋯ y)

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

theorem Proofs.Autograd.Algebra.TList.dotList_add_right {α : Type} [CommSemiring α] {ss : List Spec.Shape} (x y z : TList α ss) : x.dotList (y.add z) = x.dotList y + x.dotList z

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

theorem Proofs.Autograd.Algebra.TList.dotList_snoc {α : Type} [CommSemiring α] {ss : List Spec.Shape} {τ : Spec.Shape} (x y : TList α ss) (a b : Spec.Tensor α τ) : (x.snoc a).dotList (y.snoc b) = x.dotList y + TensorAlgebra.dot a b

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

theorem Proofs.Autograd.Algebra.TList.unsnoc_snoc {α : Type} {ss : List Spec.Shape} {τ : Spec.Shape} (xs : TList α ss) (t : Spec.Tensor α τ) : (xs.snoc t).unsnoc = (xs, t)

unsnoc is a left inverse of snoc.

theorem Proofs.Autograd.Algebra.TList.snoc_unsnoc {α : Type} {ss : List Spec.Shape} {τ : Spec.Shape} (xs : TList α (ss ++ [τ])) : xs.unsnoc.1.snoc xs.unsnoc.2 = xs

snoc is a right inverse of unsnoc.

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

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

Idx Γ s is a “typed index” into a heterogeneous context: it stores a Fin Γ.length together with a proof that the shape at that position is s.

structure Proofs.Autograd.Algebra.Idx (Γ : List Spec.Shape) (s : Spec.Shape) : Type

A typed index into a heterogeneous context Γ, carrying a proof of the expected shape s.

• i : Fin Γ.length

  i.

• h : Γ.get self.i = s

  h.

def Proofs.Autograd.Algebra.getIdx {α : Type} {Γ : List Spec.Shape} {s : Spec.Shape} (xs : TList α Γ) (idx : Idx Γ s) : Spec.Tensor α s

Read a tensor from a context at a typed index, casting along the stored shape equality.

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

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

theorem Proofs.Autograd.Algebra.TList.dotList_single {α : Type} [CommSemiring α] {Γ : List Spec.Shape} {s : Spec.Shape} (dx : TList α Γ) (idx : Idx Γ s) (v : Spec.Tensor α s) : dx.dotList (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) (Γ : 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 : TList α Γ → Δ → Spec.Tensor α τ

  forward.

• jvp : TList α Γ → TList α Γ → Δ → Spec.Tensor α τ

  jvp.

• vjp : TList α Γ → Δ → Spec.Tensor α τ → TList α Γ

  vjp.

structure Proofs.Autograd.Algebra.Node {α : Type} [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 : TList α Γ → Δ → Spec.Tensor α τ
• jvp : TList α Γ → TList α Γ → Δ → Spec.Tensor α τ
• vjp : TList α Γ → Δ → Spec.Tensor α τ → TList α Γ
• correct (x dx : TList α Γ) (d : Δ) (δ : Spec.Tensor α τ) : TensorAlgebra.dot (self.jvp x dx d) δ = dx.dotList (self.vjp x d δ)

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

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

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

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

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

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

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

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

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} [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} [CommSemiring α] {Δ : Type} {Γ : List Spec.Shape} : Graph Δ Γ []
• snoc {α : Type} [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : Graph Δ Γ ss → Node Δ (Γ ++ ss) τ → Graph Δ Γ (ss ++ [τ])

def Proofs.Autograd.Algebra.Graph.toData {α : Type} [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} [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList α Γ) (d : Δ) : TList α (Γ ++ ss)

Evaluate a proof-carrying Graph on an input context x.

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

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

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

Reverse-mode accumulation on contexts (VJP) for a proof-carrying Graph.

theorem Proofs.Autograd.Algebra.Graph.backprop_correct {α : Type} [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x dx : TList α Γ) (d : Δ) (seed : TList α (Γ ++ ss)) : (g.jvpCtx x dx d).dotList seed = dx.dotList (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 TList.dotList.