NF Backward Approximation Backend

Core approximation lemmas for the rounded NF backend: constants, sparse context writes, and the context-addition bound used when reverse-mode contributions have to be accumulated.

theorem Proofs.RuntimeApprox.NFBackend.idx_shape_eq_of_i_eq {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (a : Idx Γ s₁) (b : Idx Γ s₂) (h : a.i = b.i) : s₁ = s₂

Two context indices pointing at the same position must have the same shape.

An Idx Γ s bundles a position with a proof that Γ holds shape s there, so equal positions force equal shapes. This is what makes the disjointness lemmas below usable: a proof that two indices differ can be given by comparing positions only, with no shape reasoning.

def Proofs.RuntimeApprox.NFBackend.tensorCastOfIdxEq {α : Type} [TorchLean.Storage α] {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (a : Idx Γ s₁) (b : Idx Γ s₂) (h : a.i = b.i) : TorchLean.Tensor α s₂ → TorchLean.Tensor α s₁

Cast a tensor across a shape equality induced by equal Idx positions.

Given a : Idx Γ s₁, b : Idx Γ s₂, and h : a.i = b.i, this produces a function Tensor α s₂ → Tensor α s₁ that casts along the implied equality s₁ = s₂.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_cast_shape {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s t : Spec.Shape} (h : s = t) {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (TorchLean.Tensor.castShape xS h) (xR.castShape h) eps

Approximation is stable under transporting both tensors along the same shape equality.

theorem Proofs.RuntimeApprox.NFBackend.approxCtx_zeros {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} : approxCtx toSpec TorchLean.TensorPack.zero TorchLean.TensorPack.zero EList.zeros

The all-zero context approximates the all-zero context, at zero error.

This is the base case of every backward-pass bound: gradient accumulation starts from zeros on both the spec and the runtime side, and zero is exactly representable, so nothing is lost yet.

theorem Proofs.RuntimeApprox.NFBackend.approxCtx_setIdx {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) {tS : Spec.SpecTensor s} {tR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} (ht : approxTensor toSpec tS tR eps) : approxCtx toSpec (SparseContext.setIdx idx tS) (SparseContext.setIdx idx tR) (EList.setIdx idx eps)

Writing one approximate tensor into an otherwise-zero context keeps the context approximate, with the error recorded at that slot alone.

theorem Proofs.RuntimeApprox.NFBackend.approxCtx_set2Idx_ne {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} (a : Idx Γ s₁) (b : Idx Γ s₂) {t₁S : Spec.SpecTensor s₁} {t₁R : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s₁} {eps₁ : ℝ} {t₂S : Spec.SpecTensor s₂} {t₂R : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s₂} {eps₂ : ℝ} (h₁ : approxTensor toSpec t₁S t₁R eps₁) (h₂ : approxTensor toSpec t₂S t₂R eps₂) (hne : a.i ≠ b.i) : approxCtx toSpec (SparseContext.set2Idx a t₁S b t₂S) (SparseContext.set2Idx a t₁R b t₂R) (EList.set2Idx a eps₁ b eps₂ 0)

Two writes at distinct positions do not interfere: each slot carries its own error bound.

Distinctness is essential. At a shared index the contributions must be added, with a combined bound that includes addition rounding as well as both input errors.

Context-wise addition bound, used by global backprop accumulation

def Proofs.RuntimeApprox.NFBackend.ctxAddBound {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {Δ : List Spec.Shape} : EList Δ → EList Δ → TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) Δ → TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) Δ → EList Δ

Context-wise addition bound (NF runtime vs spec).

This produces an EList of linfNorm bounds for adding two contexts elementwise, and is used when reverse-mode accumulation must combine contributions from multiple consumers.

theorem Proofs.RuntimeApprox.NFBackend.approxCtx_add {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Δ : List Spec.Shape} (xS yS : TorchLean.TensorPack Spec.SpecScalar Δ) (xR yR : TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) Δ) (epsx epsy : EList Δ) : approxCtx toSpec xS xR epsx → approxCtx toSpec yS yR epsy → approxCtx toSpec (xS.add yS) (xR.add yR) (ctxAddBound epsx epsy xR yR)

Soundness of context-wise addition under approxCtx.

If xS ~ xR ± epsx and yS ~ yR ± epsy, then (xS + yS) ~ (xR + yR) with error bounded by ctxAddBound epsx epsy xR yR.