BackwardApprox

Reverse-mode (backward) runtime→spec approximation framework.

This is the backward analogue of NN/Proofs/RuntimeApprox/Graph/ForwardApprox.lean.

It models a tape/SSA-style DAG where each node provides:

• a forward map (spec + runtime) with an explicit forward error bound (as in FwdNode);
• a local VJP (reverse-mode) map (spec + runtime) with an explicit VJP error bound.

The global theorem RevGraph.backprop_approx composes these local bounds over the whole graph, analogously to FwdGraph.eval_approx.

Note: reverse-mode accumulation uses context-wise addition; the corresponding bound/soundness for accumulation is an explicit parameter to the theorem (addBound, addSound).

What you get

• RevGraph.eval_approx: a forward approximation theorem for the runtime/spec node contexts.
• RevGraph.backprop_approx: an end-to-end approximation theorem for reverse-mode accumulation (VJP-based backprop on the whole graph).

Reading guide

1. RevNode / RevGraph: nodes carry both forward and VJP approximation data.
2. RevGraph.eval_*: reuse the forward theory by forgetting VJP data.
3. RevGraph.backprop*: reverse-mode accumulation and its explicit bound propagation.
4. RevGraph.backprop_approx: composes node-local VJP bounds and accumulation bounds over the whole graph (induction over the snoc-list).

PyTorch correspondence / citations

This mirrors the structure of reverse-mode AD in PyTorch Autograd: a forward pass produces intermediate values, and a backward pass propagates cotangents/gradients in reverse topological order while accumulating contributions at shared nodes. https://pytorch.org/docs/stable/autograd.html

structure Proofs.RuntimeApprox.RevNode {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) (τ : Spec.Shape) extends Proofs.RuntimeApprox.FwdNode toSpec Γ τ : Type

A node with forward and VJP approximation data.

vjpSound relates the two supplied reverse maps; it does not itself prove that either map is the derivative of the forward map. Derivative correctness requires a separate node contract.

• forwardSpec : TorchLean.TensorPack Spec.SpecScalar Γ → Spec.SpecTensor τ
• forwardRuntime : TorchLean.TensorPack α Γ → TorchLean.Tensor α τ
• bound : EList Γ → TorchLean.TensorPack α Γ → Spec.SpecScalar
• sound (xS : TorchLean.TensorPack Spec.SpecScalar Γ) (xR : TorchLean.TensorPack α Γ) (eps : EList Γ) : approxCtx toSpec xS xR eps → approxTensor toSpec (self.forwardSpec xS) (self.forwardRuntime xR) (self.bound eps xR)
• vjpSpec : TorchLean.TensorPack Spec.SpecScalar Γ → Spec.SpecTensor τ → TorchLean.TensorPack Spec.SpecScalar Γ

  Spec-level VJP: maps a context and an output cotangent into a context cotangent.

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

  Runtime VJP: same shape-level function on the runtime side.

• vjpBound : EList Γ → TorchLean.TensorPack α Γ → Spec.SpecScalar → TorchLean.Tensor α τ → EList Γ

  Explicit bound transformer for VJP: pushes bounds backward through this node.

• vjpSound (ctxS : TorchLean.TensorPack Spec.SpecScalar Γ) (ctxR : TorchLean.TensorPack α Γ) (epsCtx : EList Γ) (δS : Spec.SpecTensor τ) (δR : TorchLean.Tensor α τ) (epsδ : Spec.SpecScalar) : approxCtx toSpec ctxS ctxR epsCtx → approxTensor toSpec δS δR epsδ → approxCtx toSpec (self.vjpSpec ctxS δS) (self.vjpRuntime ctxR δR) (self.vjpBound epsCtx ctxR epsδ δR)

  Soundness of the VJP bound: if context + output cotangent are approximated, so is the VJP.

inductive Proofs.RuntimeApprox.RevGraph {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) : List Spec.Shape → Type

Tape/SSA DAG with reverse-mode metadata (nodes appended in topological order).

Compared to FwdGraph, each node additionally carries a local VJP rule (RevNode.vjp*) plus an explicit error transformer vjpBound and its soundness lemma vjpSound.

• nil {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} : RevGraph toSpec Γ []
• snoc {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : RevGraph toSpec Γ ss → RevNode toSpec (Γ ++ ss) τ → RevGraph toSpec Γ (ss ++ [τ])

def Proofs.RuntimeApprox.RevGraph.toFwdGraph {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} : RevGraph toSpec Γ ss → FwdGraph toSpec Γ ss

Forget the VJP metadata of a RevGraph, yielding a FwdGraph with the same node ordering.

This lets us reuse the forward approximation theorem (FwdGraph.eval_approx) for free.

def Proofs.RuntimeApprox.RevGraph.evalSpec {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (x : TorchLean.TensorPack Spec.SpecScalar Γ) : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss)

Spec-level evaluation of a RevGraph (delegates to toFwdGraph).

def Proofs.RuntimeApprox.RevGraph.evalRuntime {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (x : TorchLean.TensorPack α Γ) : TorchLean.TensorPack α (Γ ++ ss)

Runtime-level evaluation of a RevGraph (delegates to toFwdGraph).

def Proofs.RuntimeApprox.RevGraph.evalBounds {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (epsIn : EList Γ) (xR : TorchLean.TensorPack α Γ) : EList (Γ ++ ss)

Forward bound propagation for a RevGraph (delegates to toFwdGraph).

theorem Proofs.RuntimeApprox.RevGraph.eval_approx {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xS : TorchLean.TensorPack Spec.SpecScalar Γ) (xR : TorchLean.TensorPack α Γ) (epsIn : EList Γ) : approxCtx toSpec xS xR epsIn → approxCtx toSpec (g.evalSpec xS) (g.evalRuntime xR) (g.evalBounds epsIn xR)

Forward approximation theorem for RevGraph (just FwdGraph.eval_approx via toFwdGraph).

def Proofs.RuntimeApprox.RevGraph.backpropSpec {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (x : TorchLean.TensorPack Spec.SpecScalar Γ) (seed : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss)) : TorchLean.TensorPack Spec.SpecScalar Γ

Spec-level reverse-mode evaluation.

Informally: run the forward pass to get node contexts, then traverse nodes in reverse topological order, applying each node’s VJP and accumulating the resulting context-cotangent into the running seed.

def Proofs.RuntimeApprox.RevGraph.backpropRuntime {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) [Add α] (x : TorchLean.TensorPack α Γ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Runtime-level reverse-mode accumulation.

This mirrors backpropSpec, but uses runtime tensors and relies on an Add α instance to accumulate contributions at shared nodes.

def Proofs.RuntimeApprox.RevGraph.backpropBounds {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) [Add α] (epsIn : EList Γ) (xR : TorchLean.TensorPack α Γ) (epsSeed : EList (Γ ++ ss)) (seedR : TorchLean.TensorPack α (Γ ++ ss)) (addBound : {Δ : List Spec.Shape} → EList Δ → EList Δ → TorchLean.TensorPack α Δ → TorchLean.TensorPack α Δ → EList Δ) : EList Γ

Backward error propagation for backprop*.

This is parameterized by:

• addBound: how to compute the (per-entry) error list for context-wise addition.

addBound may depend on the runtime addends, to account for rounding models.

theorem Proofs.RuntimeApprox.RevGraph.backprop_approx {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) [Add α] (addBound : {Δ : List Spec.Shape} → EList Δ → EList Δ → TorchLean.TensorPack α Δ → TorchLean.TensorPack α Δ → EList Δ) (addSound : ∀ {Δ : List Spec.Shape} (xS yS : TorchLean.TensorPack Spec.SpecScalar Δ) (xR yR : TorchLean.TensorPack α Δ) (epsx epsy : EList Δ), approxCtx toSpec xS xR epsx → approxCtx toSpec yS yR epsy → approxCtx toSpec (xS.add yS) (xR.add yR) (addBound epsx epsy xR yR)) (xS : TorchLean.TensorPack Spec.SpecScalar Γ) (xR : TorchLean.TensorPack α Γ) (epsIn : EList Γ) (seedS : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss)) (seedR : TorchLean.TensorPack α (Γ ++ ss)) (epsSeed : EList (Γ ++ ss)) : approxCtx toSpec xS xR epsIn → approxCtx toSpec seedS seedR epsSeed → approxCtx toSpec (g.backpropSpec xS seedS) (g.backpropRuntime xR seedR) (g.backpropBounds epsIn xR epsSeed seedR fun {Δ : List Spec.Shape} => addBound)

End-to-end reverse-mode approximation theorem for RevGraph.backprop*.

Informally: assume (1) the runtime inputs xR approximate the spec inputs xS with bounds epsIn, and (2) the runtime seed cotangents seedR approximate the spec seeds seedS with bounds epsSeed. Then the whole backprop result backpropRuntime g xR seedR approximates the spec backprop result backpropSpec g xS seedS, with an explicit bound computed by backpropBounds.

The only "extra" ingredient beyond per-node VJP approximation is how we accumulate contributions: addBound describes how addition affects error bounds, and addSound is the theorem justifying it (e.g. for exact reals it is trivial; for rounding models it carries the rounding-error analysis).