Linear Algebra NF Reverse Nodes

Reverse-mode approximation nodes for matrix-vector and matrix-matrix multiplication. They compare supplied real adjoint formulas with rounded NF formulas. The local bounds do not establish native-kernel correspondence or independently prove the adjoint identities.

Matrix multiplication permits both operands to refer to the same context slot. That case adds both cotangent contributions and includes the addition's rounding error in the bound.

noncomputable def Proofs.RuntimeApprox.NFBackend.matVecMulRevNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {m n : ℕ} (A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) : RevNode toSpec Γ (Spec.Shape.dim m Spec.Shape.scalar)

Reverse node for matrix-vector multiplication (matVecMulSpec).

VJP uses the standard adjoint identities: δW = δ ⊗ x and δx = Wᵀ δ (expressed in tensor form), with NF error bounds layered over the primitive ops.

noncomputable def Proofs.RuntimeApprox.NFBackend.matMulRevNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ : List Spec.Shape} {m n p : ℕ} (A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (B : Idx Γ (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))) : RevNode toSpec Γ (Spec.Shape.dim m (Spec.Shape.dim p Spec.Shape.scalar))

Reverse node for matrix multiplication (matMulSpec).

VJP uses the standard identities δA = δC * Bᵀ and δB = Aᵀ * δC (in appropriate shapes), with NF error bounds layered over the primitive ops.