Forward graph approximation

FwdGraph.eval_approx composes the local bounds supplied by FwdNode.sound. Each node receives a heterogeneous context of tensors and an aligned EList of scalar error bounds. Shape lists describe context entries; they do not replace tensor storage.

The framework is backend-independent and allows noncomputable rounding models such as FloatLib's NF. An explicit propagated bound need not be an executable numerical calculation. Instantiating the node contracts with native arithmetic requires separate per-operation correspondence proofs.

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)

Read an indexed tensor approximation with its aligned scalar error bound.

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.