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⟫.

theorem Proofs.Autograd.Algebra.Contributions.lookup_single {α : Type} [TorchLean.Storage α] [Zero α] {Γ : List Spec.Shape} {shape : Spec.Shape} (idx : Idx Γ shape) (value : TorchLean.Tensor α shape) : TensorLookup.ofPack (TensorPack.single idx value) = (TensorLookup.fill 0).set idx value

A single-parent dense VJP agrees with one exception to the uniform zero reader.

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

One parent contribution, including the original zero entries at every other position.

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

The original programs of a node after saving its inputs for one execution.

• value : Unit → TorchLean.Tensor α τ

  Compute the primal tensor after domain validation has succeeded.

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

  The stored VJP with its primal inputs already captured.

• validate : Unit → Except String Unit

  Domain validation performed before recording the node.

structure Proofs.Autograd.Algebra.PreparedNode (α : Type) [TorchLean.Storage α] (Γ : List Spec.Shape) (τ : Spec.Shape) extends Proofs.Autograd.Algebra.PreparedPrograms α Γ τ : Type

Saved node programs with an optional certified compact backward implementation.

• value : Unit → TorchLean.Tensor α τ
• vjp : TorchLean.Tensor α τ → TorchLean.TensorPack α Γ
• validate : Unit → Except String Unit
• compact? : Option { run : TorchLean.Tensor α τ → Contributions α Γ // ∀ (seed : TorchLean.Tensor α τ), (run seed).dense () = self.vjp seed }

  A compact VJP preserves the complete dense contribution, at every parent position.

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

Executable node payload (no derivative-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.

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

  An optional preparation program that saves only the node's own inputs. Its certificate preserves the complete dense VJP, including zero entries and the order of scalar operations.

def Proofs.Autograd.Algebra.NodeData.ofLocal {α Δ P : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (capture : TensorLookup α Γ → P) (forward : P → Δ → TorchLean.Tensor α τ) (jvp : P → P → Δ → TorchLean.Tensor α τ) (vjp : P → Δ → TorchLean.Tensor α τ → TorchLean.TensorPack α Γ) (validate : P → Δ → Except String Unit := fun (x : P) (x_1 : Δ) => Except.ok ()) : NodeData α Δ Γ τ

Build a node whose runtime preparation captures a fixed collection of tensors. The same scalar programs define the pack interface and the prepared interface, so their agreement is definitional.

def Proofs.Autograd.Algebra.NodeData.ofLocalCompact {α Δ P : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (capture : TensorLookup α Γ → P) (forward : P → Δ → TorchLean.Tensor α τ) (jvp : P → P → Δ → TorchLean.Tensor α τ) (vjp : P → Δ → TorchLean.Tensor α τ → Contributions α Γ) (validate : P → Δ → Except String Unit := fun (x : P) (x_1 : Δ) => Except.ok ()) : NodeData α Δ Γ τ

Local scalar programs with a compact VJP whose dense adapter remains the public VJP.

def Proofs.Autograd.Algebra.NodeData.prepare {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (node : NodeData α Δ Γ τ) (ctx : TensorContext α Γ) (data : Δ) : PreparedNode α Γ τ

Prepare a node from array storage, using the pack adapter for arbitrary custom closures.

@[simp]

theorem Proofs.Autograd.Algebra.NodeData.prepare_ofPack {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (data : Δ) : (node.prepare (TensorContext.ofPack ctx) data).toPreparedPrograms = { value := fun (x : Unit) => node.forward ctx data, vjp := node.vjp ctx data, validate := fun (x : Unit) => node.validate ctx data }

Preparation preserves the original forward, validation, and dense backward programs.

@[simp]

theorem Proofs.Autograd.Algebra.NodeData.prepare_value_ofPack {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (data : Δ) : (node.prepare (TensorContext.ofPack ctx) data).value = fun (x : Unit) => node.forward ctx data

@[simp]

theorem Proofs.Autograd.Algebra.NodeData.prepare_vjp_ofPack {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (data : Δ) : (node.prepare (TensorContext.ofPack ctx) data).vjp = node.vjp ctx data

@[simp]

theorem Proofs.Autograd.Algebra.NodeData.prepare_validate_ofPack {α Δ : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {τ : Spec.Shape} (node : NodeData α Δ Γ τ) (ctx : TorchLean.TensorPack α Γ) (data : Δ) : (node.prepare (TensorContext.ofPack ctx) data).validate = fun (x : Unit) => node.validate ctx data

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
• prepare? : Option { prepare : TensorLookup α Γ → Δ → PreparedNode α Γ τ // ∀ (ctx : TorchLean.TensorPack α Γ) (d : Δ), (prepare (TensorLookup.ofPack ctx) d).toPreparedPrograms = { value := fun (x : Unit) => self.forward ctx d, vjp := self.vjp ctx d, validate := fun (x : Unit) => self.validate ctx d } }
• 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.evalArray {α : Type} [TorchLean.Storage α] {Δ : Type} {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : TensorContext α (Γ ++ ss)

Evaluate using indexed storage and save only each node's local input tensors.

theorem Proofs.Autograd.Algebra.GraphData.evalArray_eq {α : Type} [TorchLean.Storage α] {Δ : Type} {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : g.evalArray x d = TensorContext.ofPack (g.eval x d)

Indexed forward execution computes the original full typed context.

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

Public typed forward result, decoded once after array execution.

@[csimp]

theorem Proofs.Autograd.Algebra.GraphData.eval_eq_array : @eval = @evalWithArray

Compile the public evaluator to the proved array execution path.

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.

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 (fan-out and sharing are allowed). This mirrors the structure of PyTorch’s dynamic autograd graph, but with shape-typed contexts.

• 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.