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.approxT_fill_const
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
{rnd : ℝ → ℤ}
{cS : ℝ}
{cR : TorchLean.Floats.NF β fexp rnd}
{eps : ℝ}
(h : |toSpec cR - cS| ≤ eps)
{s : Spec.Shape}
:
theorem
Proofs.RuntimeApprox.NFBackend.approxT_fill_one
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{s : Spec.Shape}
:
theorem
Proofs.RuntimeApprox.NFBackend.approxT_fill_zero
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{s : Spec.Shape}
:
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)
:
def
Proofs.RuntimeApprox.NFBackend.tensorCastOfIdxEq
{α : Type}
{Γ : List Spec.Shape}
{s₁ s₂ : Spec.Shape}
(a : Idx Γ s₁)
(b : Idx Γ s₂)
(h : a.i = b.i)
:
Spec.Tensor α s₂ → Spec.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₂.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approxT_tensor_cast
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
{rnd : ℝ → ℤ}
{s t : Spec.Shape}
(h : s = t)
{xS : Spec.SpecTensor s}
{xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{eps : ℝ}
(hx : approxT toSpec xS xR eps)
:
approxT toSpec (Spec.tensorCast t h xS) (Spec.tensorCast t h xR) eps
theorem
Proofs.RuntimeApprox.NFBackend.approxCtx_zeros
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
:
theorem
Proofs.RuntimeApprox.NFBackend.approxCtx_setIdx
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{s : Spec.Shape}
(idx : Idx Γ s)
{tS : Spec.SpecTensor s}
{tR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s}
{eps : ℝ}
(ht : approxT toSpec tS tR eps)
:
approxCtx toSpec (TList.setIdx idx tS) (TList.setIdx idx tR) (EList.setIdx idx eps)
theorem
Proofs.RuntimeApprox.NFBackend.approxCtx_set2Idx_ne
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{s₁ s₂ : Spec.Shape}
(a : Idx Γ s₁)
(b : Idx Γ s₂)
{t₁S : Spec.SpecTensor s₁}
{t₁R : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s₁}
{eps₁ : ℝ}
{t₂S : Spec.SpecTensor s₂}
{t₂R : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s₂}
{eps₂ : ℝ}
(h₁ : approxT toSpec t₁S t₁R eps₁)
(h₂ : approxT toSpec t₂S t₂R eps₂)
(hne : a.i ≠ b.i)
:
approxCtx toSpec (TList.set2Idx a t₁S b t₂S) (TList.set2Idx a t₁R b t₂R) (EList.set2Idx a eps₁ b eps₂ 0)
theorem
Proofs.RuntimeApprox.NFBackend.approxCtx_set3Idx_ne
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{s₁ s₂ s₃ : Spec.Shape}
(a : Idx Γ s₁)
(b : Idx Γ s₂)
(c : Idx Γ s₃)
{t₁S : Spec.SpecTensor s₁}
{t₁R : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s₁}
{eps₁ : ℝ}
{t₂S : Spec.SpecTensor s₂}
{t₂R : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s₂}
{eps₂ : ℝ}
{t₃S : Spec.SpecTensor s₃}
{t₃R : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s₃}
{eps₃ : ℝ}
(h₁ : approxT toSpec t₁S t₁R eps₁)
(h₂ : approxT toSpec t₂S t₂R eps₂)
(h₃ : approxT toSpec t₃S t₃R eps₃)
(hab : a.i ≠ b.i)
(hac : a.i ≠ c.i)
(hbc : b.i ≠ c.i)
:
approxCtx toSpec (TList.set3IdxNe a t₁S b t₂S c t₃S hab hac hbc) (TList.set3IdxNe a t₁R b t₂R c t₃R hab hac hbc)
(EList.set3IdxNe a eps₁ b eps₂ c eps₃ hab hac hbc)
def
Proofs.RuntimeApprox.NFBackend.ctxAddBound
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{Δ : List Spec.Shape}
:
EList Δ → EList Δ → TList (TorchLean.Floats.NF β fexp rnd) Δ → TList (TorchLean.Floats.NF β fexp rnd) Δ → EList Δ
Context-wise addition bound (NF runtime vs spec).
This produces an EList of linf_norm bounds for adding two contexts elementwise, and is used when
reverse-mode accumulation must combine contributions from multiple consumers.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approxCtx_add
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Δ : List Spec.Shape}
(xS yS : TList Spec.SpecScalar Δ)
(xR yR : TList (TorchLean.Floats.NF β fexp rnd) Δ)
(epsx epsy : EList Δ)
:
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.