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*: executable reverse-mode accumulation + 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

def Proofs.RuntimeApprox.EList.add {ss : List Spec.Shape} : EList ss → EList ss → EList ss

Componentwise addition of error lists (used when accumulating cotangent/gradient bounds).

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

A node with both forward and VJP approximation data.

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

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

• vjpRuntime : TList α Γ → Spec.Tensor α τ → TList α Γ

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

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

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

• vjpSound (ctxS : TList Spec.SpecScalar Γ) (ctxR : TList α Γ) (epsCtx : EList Γ) (δS : Spec.SpecTensor τ) (δR : Spec.Tensor α τ) (epsδ : Spec.SpecScalar) : approxCtx toSpec ctxS ctxR epsCtx → approxT 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 : TList Spec.SpecScalar Γ) : TList 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 : TList α Γ) : TList α (Γ ++ 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 : TList α Γ) : 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 : TList Spec.SpecScalar Γ) (xR : TList α Γ) (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 : TList Spec.SpecScalar Γ) (seed : TList Spec.SpecScalar (Γ ++ ss)) : TList 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 : TList α Γ) (seed : TList α (Γ ++ ss)) : TList α Γ

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 : TList α Γ) (epsSeed : EList (Γ ++ ss)) (seedR : TList α (Γ ++ ss)) (addBound : {Δ : List Spec.Shape} → EList Δ → EList Δ → TList α Δ → TList α Δ → 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 Δ → TList α Δ → TList α Δ → EList Δ) (addSound : ∀ {Δ : List Spec.Shape} (xS yS : TList Spec.SpecScalar Δ) (xR yR : TList α Δ) (epsx epsy : EList Δ), approxCtx toSpec xS xR epsx → approxCtx toSpec yS yR epsy → approxCtx toSpec (TList.add xS yS) (TList.add xR yR) (addBound epsx epsy xR yR)) (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (epsIn : EList Γ) (seedS : TList Spec.SpecScalar (Γ ++ ss)) (seedR : TList α (Γ ++ 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).