ForwardApprox

Forward (runtime→spec) approximation framework.

This file is backend-agnostic: it proves that approximation bounds compose over a tape/SSA-style graph, assuming each node provides a local forward approximation lemma.

It is intended to be instantiated by proof-relevant runtimes such as rounding models (NF / neural_round). Lean's builtin Float is treated as trusted (see NN/Runtime/Scalar.lean).

What you get

• FwdGraph.eval_approx: an end-to-end theorem saying that if the runtime input context is within an explicit per-entry error budget of the spec input context, then runtime graph evaluation is within a computable propagated error budget of the spec evaluation.

Reading guide

1. TList and EList: heterogeneous runtime/spec contexts and aligned error vectors.
2. approxT and approxCtx: the approximation predicates for a single tensor and a whole context.
3. Idx: a typed index into a context (so graph nodes can refer to earlier values safely).
4. FwdNode / FwdGraph: local approximation lemmas and their composition over a snoc-list DAG.

PyTorch correspondence / citations

This is conceptually similar to the “graph of ops” view behind PyTorch Autograd (and tooling like torch.fx), except that our graph nodes carry proof-relevant approximation bounds that can be composed into an end-to-end theorem. https://pytorch.org/docs/stable/autograd.html https://pytorch.org/docs/stable/fx.html

@[reducible, inline]

abbrev Proofs.RuntimeApprox.TList (α : Type) (ss : List Spec.Shape) : Type

A heterogeneous context (one tensor per shape), indexed by a List Shape.

This is just an alias of the canonical tape/autograd-algebra TList so that all the helper operations (get, cast, snoc, unsnoc, add, ...) are shared across proof subsystems.

inductive Proofs.RuntimeApprox.EList : List Spec.Shape → Type

Scalar error bounds aligned with a context shape list.

• nil : EList []
• cons {s : Spec.Shape} {ss : List Spec.Shape} : ℝ → EList ss → EList (s :: ss)

def Proofs.RuntimeApprox.EList.cast {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : EList ss₁) : EList ss₂

Cast an error list along an equality of shape lists.

@[simp]

theorem Proofs.RuntimeApprox.EList.cast_rfl {ss : List Spec.Shape} (xs : EList ss) : cast ⋯ xs = xs

Casting along rfl is the identity.

@[simp]

theorem Proofs.RuntimeApprox.EList.cast_cast {ss₁ ss₂ ss₃ : List Spec.Shape} (h₁ : ss₁ = ss₂) (h₂ : ss₂ = ss₃) (xs : EList ss₁) : cast h₂ (cast h₁ xs) = cast ⋯ xs

EList.cast composes as expected.

def Proofs.RuntimeApprox.EList.snoc {τ : Spec.Shape} {ss : List Spec.Shape} : EList ss → ℝ → EList (ss ++ [τ])

Append a scalar error bound to the end of an error list.

def Proofs.RuntimeApprox.EList.unsnoc {τ : Spec.Shape} {ss : List Spec.Shape} : EList (ss ++ [τ]) → EList ss × ℝ

Split an error list aligned with ss ++ [τ] into its prefix and last scalar.

@[simp]

theorem Proofs.RuntimeApprox.EList.unsnoc_snoc {ss : List Spec.Shape} {τ : Spec.Shape} (xs : EList ss) (e : ℝ) : (xs.snoc e).unsnoc = (xs, e)

unsnoc is a left inverse of snoc.

@[simp]

theorem Proofs.RuntimeApprox.EList.snoc_unsnoc {ss : List Spec.Shape} {τ : Spec.Shape} (xs : EList (ss ++ [τ])) : xs.unsnoc.1.snoc xs.unsnoc.2 = xs

snoc is a left inverse of unsnoc.

def Proofs.RuntimeApprox.EList.get {ss : List Spec.Shape} : EList ss → (i : Fin ss.length) → ℝ

Get the ith scalar bound from an error list.

def Proofs.RuntimeApprox.approxT {α : Type} {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : Spec.Tensor α s) (eps : Spec.SpecScalar) : Prop

Tensor-level approximation under a toSpec : α → ℝ mapping.

def RuntimeApprox.«term_≈ᵀ[_]_:_» : Lean.TrailingParserDescr

Scoped notation for tensor approximation (approxT).

open scoped RuntimeApprox
spec ≈ᵀ[toSpec] runtime : eps

theorem Proofs.RuntimeApprox.approxTTol_mono {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.Tensor α s} {tol₁ tol₂ : ApproxTol} (habs : tol₁.abs ≤ tol₂.abs) (hrel : tol₁.rel ≤ tol₂.rel) (hslack : tol₁.slack ≤ tol₂.slack) (h : approxTTol toSpec spec runtime tol₁) : approxTTol toSpec spec runtime tol₂

Monotonicity of approxTTol: if you only loosen tolerances, an approximation stays valid.

theorem Proofs.RuntimeApprox.approxTTol_absOnly_iff {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.Tensor α s} {eps : ℝ} (heps : 0 ≤ eps) : approxTTol toSpec spec runtime (ApproxTol.absOnly eps) ↔ approxT toSpec spec runtime eps

approxTTol specialized to an absolute-only tolerance is equivalent to approxT.

This is mostly a convenience lemma for switching between the "tolerance" API and the plain eps : ℝ API.

def Proofs.RuntimeApprox.approxCtx {α : Type} (toSpec : α → Spec.SpecScalar) {ss : List Spec.Shape} : TList Spec.SpecScalar ss → TList α ss → EList ss → Prop

Context-level approximation with a per-entry error list.

def RuntimeApprox.«term_≈ᶜ[_]_:_» : Lean.TrailingParserDescr

Scoped notation for approxCtx.

This keeps end-to-end forward-soundness theorems readable:

open scoped RuntimeApprox
-- `ΓS` is an approximate view of `ΓR` with per-entry bounds `eps`:
ΓS ≈ᶜ[toSpec] ΓR : eps

The notation is scoped to avoid polluting unrelated code.

theorem Proofs.RuntimeApprox.approxCtx_cast {α : Type} {toSpec : α → Spec.SpecScalar} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) {xS : TList Spec.SpecScalar ss₁} {xR : TList α ss₁} {eps : EList ss₁} : approxCtx toSpec xS xR eps → approxCtx toSpec (TList.cast h xS) (TList.cast h xR) (EList.cast h eps)

Transport a context approximation across an equality of shape lists.

This is used any time we need to reassociate Γ ++ ss type indices (casts are unavoidable in this List Shape-indexed encoding).

theorem Proofs.RuntimeApprox.approxCtx_snoc {α : Type} {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TList Spec.SpecScalar ss} {xR : TList α ss} {eps : EList ss} (hx : approxCtx toSpec xS xR eps) {yS : Spec.SpecTensor τ} {yR : Spec.Tensor α τ} {e : Spec.SpecScalar} (hy : approxT toSpec yS yR e) : approxCtx toSpec (TList.snoc xS yS) (TList.snoc xR yR) (eps.snoc e)

Extend a context approximation by appending one more approximated tensor.

This is the core "composition" step used when evaluating a snoc-graph: if the previous context is approximated, and the new node output is approximated with some bound e, then the extended context is approximated with the extended error list.

theorem Proofs.RuntimeApprox.approxCtx_get {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TList Spec.SpecScalar Γ} {xR : TList α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (i : Fin Γ.length) : approxT toSpec (TList.get xS i) (TList.get xR i) (eps.get i)

Extract a single entry approximation from approxCtx.

theorem Proofs.RuntimeApprox.approxCtx_get_tolAbsOnly {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TList Spec.SpecScalar Γ} {xR : TList α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (i : Fin Γ.length) : approxTTol toSpec (TList.get xS i) (TList.get xR i) (ApproxTol.absOnly (eps.get i))

approxCtx_get expressed in terms of approxTTol with an absolute-only tolerance.

Many downstream theorems are stated using a tolerance record (ApproxTol) rather than a bare eps : ℝ. For absolute-only bounds, this lemma gives the bridge.

theorem Proofs.RuntimeApprox.approxCtx_unsnoc {α : Type} {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TList Spec.SpecScalar (ss ++ [τ])} {xR : TList α (ss ++ [τ])} {eps : EList (ss ++ [τ])} : approxCtx toSpec xS xR eps → approxCtx toSpec (TList.unsnoc xS).1 (TList.unsnoc xR).1 eps.unsnoc.1 ∧ approxT toSpec (TList.unsnoc xS).2 (TList.unsnoc xR).2 eps.unsnoc.2

Split a context approximation for ss ++ [τ] into:

• a prefix context approximation for ss, and
• a single-tensor approximation for the last entry of shape τ.

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

An index into a heterogeneous context, carrying a proof of the expected shape.

• i : Fin Γ.length

  i.

• h : Γ.get self.i = s

  h.

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

Typed lookup from a heterogeneous context TList α Γ using an index Idx Γ s.

def Proofs.RuntimeApprox.getIdxEps {Γ : List Spec.Shape} {s : Spec.Shape} (es : EList Γ) (idx : Idx Γ s) : ℝ

Lookup the epsilon entry associated to an index Idx Γ s.

theorem Proofs.RuntimeApprox.approxCtx_getIdx {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {s : Spec.Shape} {xS : TList Spec.SpecScalar Γ} {xR : TList α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (idx : Idx Γ s) : approxT toSpec (getIdx xS idx) (getIdx xR idx) (getIdxEps eps idx)

Context approximation implies approximation of any indexed entry.

Informally: if every tensor in the runtime context is close to its spec counterpart (with an aligned error list eps), then reading any entry idx : Idx Γ s yields an approxT fact with the corresponding scalar bound getIdxEps eps idx.

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

A single SSA/DAG node with a local forward approximation lemma.

Fields:

• forwardSpec / forwardRuntime: the spec vs runtime semantics of the node.
• bound: computes an explicit scalar error bound for the node’s output, given current context bounds and the runtime context (to allow data-dependent bounds).
• sound: the “local theorem” that justifies bound.

Informally: if the whole input context is approximated (approxCtx), then this node’s output is approximated (approxT) with error at most bound.

• forwardSpec : TList Spec.SpecScalar Γ → Spec.SpecTensor τ

  forward Spec.

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

  forward Runtime.

• bound : EList Γ → TList α Γ → Spec.SpecScalar

  bound.

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

  sound.

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

Forward-only SSA/DAG graph (nodes appended in topological order).

The type parameter ss : List Shape tracks the shapes of intermediate values produced by the graph; evaluating a graph returns an extended context of shape list Γ ++ ss.

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

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

Evaluate a forward graph in the spec semantics.

Result type: an extended context Γ ++ ss containing the original inputs and all intermediate values produced by the graph.

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

Evaluate a forward graph in the runtime semantics.

This mirrors evalSpec, but uses the backend α tensors and the node runtime closures.

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

Propagate an input error list epsIn through the whole graph, producing output bounds for Γ ++ ss.

Each node can compute its own output bound from the current context bounds and the runtime context; evalBounds just composes those local transformers over the snoc-list DAG.

theorem Proofs.RuntimeApprox.FwdGraph.eval_approx {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraph 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)

End-to-end forward approximation theorem for FwdGraph.

Informally: assume every input tensor in the runtime context xR is within the provided per-entry bounds epsIn of the corresponding spec tensor in xS. Then evaluating the whole graph preserves that approximation relation, with output bounds given by evalBounds.

Proof idea: induction over the snoc-list graph; at each step, apply the node's local bound/soundness lemma (FwdNode.sound) and then extend the context approximation via approxCtx_snoc.