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 rounding models such as the noncomputable FloatLib.Floats.Formats.Flocq.NF, whose arithmetic uses Flocq.round. Lean gives builtin Float a logical model, but connecting that model and its runtime implementation to these approximation bounds requires separate per-operation proofs.

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. Autograd.Algebra.TensorPack and EList: heterogeneous contexts and aligned error vectors.
2. approxTensor 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

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.EList.toArray {ss : List Spec.Shape} : EList ss → Array ℝ

Erase shape indices while retaining bounds in context order.

This is the reporting boundary used by architecture-independent numerical traces. Proofs continue to use EList; UI and serialization code receives an array only after propagation has finished.

@[simp]

theorem Proofs.RuntimeApprox.EList.size_toArray {ss : List Spec.Shape} (errors : EList ss) : errors.toArray.size = ss.length

Flattening an error list to an array keeps one entry per shape.

def Proofs.RuntimeApprox.approxTensor {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : TorchLean.Tensor α s) (eps : Spec.SpecScalar) : Prop

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

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

Scoped notation for tensor approximation (approxTensor).

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

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

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

theorem Proofs.RuntimeApprox.approxTensorWithTol_absOnly_iff {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} {eps : ℝ} (heps : 0 ≤ eps) : approxTensorWithTol toSpec spec runtime (ApproxTol.absOnly eps) ↔ approxTensor toSpec spec runtime eps

approxTensorWithTol specialized to an absolute-only tolerance is equivalent to approxTensor.

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

def Proofs.RuntimeApprox.approxCtx {α : Type} [TorchLean.Storage α] (toSpec : α → Spec.SpecScalar) {ss : List Spec.Shape} : TorchLean.TensorPack Spec.SpecScalar ss → TorchLean.TensorPack α ss → EList ss → Prop

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

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

Scoped notation for approxCtx.

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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) {xS : TorchLean.TensorPack Spec.SpecScalar ss₁} {xR : TorchLean.TensorPack α ss₁} {eps : EList ss₁} : approxCtx toSpec xS xR eps → approxCtx toSpec (TorchLean.TensorPack.cast h xS) (TorchLean.TensorPack.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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar ss} {xR : TorchLean.TensorPack α ss} {eps : EList ss} (hx : approxCtx toSpec xS xR eps) {yS : Spec.SpecTensor τ} {yR : TorchLean.Tensor α τ} {e : Spec.SpecScalar} (hy : approxTensor toSpec yS yR e) : approxCtx toSpec (xS.snoc yS) (xR.snoc 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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar Γ} {xR : TorchLean.TensorPack α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (i : Fin Γ.length) : approxTensor toSpec (xS.get i) (xR.get i) (eps.get i)

Extract a single entry approximation from approxCtx.

theorem Proofs.RuntimeApprox.approxCtx_get_tolAbsOnly {α : Type} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar Γ} {xR : TorchLean.TensorPack α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (i : Fin Γ.length) : approxTensorWithTol toSpec (xS.get i) (xR.get i) (ApproxTol.absOnly (eps.get i))

approxCtx_get expressed in terms of approxTensorWithTol 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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar (ss ++ [τ])} {xR : TorchLean.TensorPack α (ss ++ [τ])} {eps : EList (ss ++ [τ])} : approxCtx toSpec xS xR eps → approxCtx toSpec xS.unsnoc.1 xR.unsnoc.1 eps.unsnoc.1 ∧ approxTensor toSpec xS.unsnoc.2 xR.unsnoc.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 τ.

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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {s : Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar Γ} {xR : TorchLean.TensorPack α Γ} {eps : EList Γ} (h : approxCtx toSpec xS xR eps) (idx : Idx Γ s) : approxTensor 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 approxTensor fact with the corresponding scalar bound getIdxEps eps idx.

structure Proofs.RuntimeApprox.FwdNode {α : Type} [TorchLean.Storage α] (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 (approxTensor) with error at most bound.

• forwardSpec : TorchLean.TensorPack Spec.SpecScalar Γ → Spec.SpecTensor τ

  Specification-level semantics of this node.

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

  Runtime semantics of this node.

• bound : EList Γ → TorchLean.TensorPack α Γ → Spec.SpecScalar

  Error bound computed from the current context bounds and runtime values.

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

  Local approximation theorem for this node.

inductive Proofs.RuntimeApprox.FwdGraph {α : Type} [TorchLean.Storage α] (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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} : FwdGraph toSpec Γ []
• snoc {α : Type} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : FwdGraph toSpec Γ ss → FwdNode toSpec (Γ ++ ss) τ → FwdGraph toSpec Γ (ss ++ [τ])

def Proofs.RuntimeApprox.FwdGraph.evalSpec {α : Type} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraph toSpec Γ ss) (x : TorchLean.TensorPack Spec.SpecScalar Γ) : TorchLean.TensorPack 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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraph toSpec Γ ss) (x : TorchLean.TensorPack α Γ) : TorchLean.TensorPack α (Γ ++ 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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraph toSpec Γ ss) (epsIn : EList Γ) (xR : TorchLean.TensorPack α Γ) : 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} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : FwdGraph 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)

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 theorem (FwdNode.sound) and then extend the context approximation via approxCtx_snoc.