Sparse VJP Contexts

Shape-indexed context builders used by the NF reverse-mode proofs. These helpers write only the positions touched by a local VJP rule and leave every other component at zero, which lets the sparse cases avoid unnecessary rounded additions.

Sparse Contexts For Local VJPs

def Proofs.RuntimeApprox.TList.zeros {α : Type} [Zero α] {ss : List Spec.Shape} : TList α ss

A TList filled with zeros (shape-wise), used to build sparse contexts for local VJPs.

def Proofs.RuntimeApprox.TList.setIdx {α : Type} [Zero α] {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → Spec.Tensor α s → TList α Γ

Set a single Idx position in a TList, filling all other entries with zeros.

def Proofs.RuntimeApprox.TList.set2Idx {α : Type} [Zero α] [Add α] {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → Spec.Tensor α s₁ → Idx Γ s₂ → Spec.Tensor α s₂ → TList α Γ

Set two indices; if they coincide, add the contributions at that position.

def Proofs.RuntimeApprox.EList.zeros {ss : List Spec.Shape} : EList ss

An EList filled with zeros, used for sparse error-bound contexts.

def Proofs.RuntimeApprox.EList.setIdx {Γ : List Spec.Shape} {s : Spec.Shape} : Idx Γ s → ℝ → EList Γ

Set a single Idx position in an EList, filling all other entries with zeros.

def Proofs.RuntimeApprox.EList.set2Idx {Γ : List Spec.Shape} {s₁ s₂ : Spec.Shape} : Idx Γ s₁ → ℝ → Idx Γ s₂ → ℝ → ℝ → EList Γ

Set two indices in an EList; if they coincide, use the supplied combined value eBoth.

def Proofs.RuntimeApprox.TList.set3IdxNe {α : Type} [Zero α] [Add α] {Γ : List Spec.Shape} {s₁ s₂ s₃ : Spec.Shape} (a : Idx Γ s₁) : Spec.Tensor α s₁ → (b : Idx Γ s₂) → Spec.Tensor α s₂ → (c : Idx Γ s₃) → Spec.Tensor α s₃ → a.i ≠ b.i → a.i ≠ c.i → b.i ≠ c.i → TList α Γ

Set three indices when the positions are pairwise distinct.

This avoids any context-wise addition: only the three targeted positions are written, and all others are 0. This is important for NF, where even x + 0 would incur rounding.

def Proofs.RuntimeApprox.EList.set3IdxNe {Γ : List Spec.Shape} {s₁ s₂ s₃ : Spec.Shape} (a : Idx Γ s₁) : ℝ → (b : Idx Γ s₂) → ℝ → (c : Idx Γ s₃) → ℝ → a.i ≠ b.i → a.i ≠ c.i → b.i ≠ c.i → EList Γ

Error list for TList.set3Idx_ne: set the three designated positions, 0 elsewhere.