NF Linear Algebra

Forward (runtime→spec) approximation lemmas for non-elementwise linear algebra ops over NF.

This extends NN.Proofs.RuntimeApprox.NF.Ops with bounds for the core sum-of-products patterns that appear in linear layers and matrix multiplication.

The central trick is to separate proof-friendly scalar fold bounds for dot products from tensor-level wrappers that turn those fold bounds into approxTensor theorems and graph nodes.

PyTorch correspondence / citations

This is the proof analogue of linear algebra building blocks used throughout PyTorch models: matrix-vector/matrix-matrix multiplication (torch.matmul) and linear layers (torch.nn.functional.linear). https://pytorch.org/docs/stable/generated/torch.matmul.html https://pytorch.org/docs/stable/generated/torch.nn.functional.linear.html

def Proofs.RuntimeApprox.NFBackend.matGet {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {m n : ℕ} (A : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [m, n]) (i : Fin m) (j : Fin n) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd

Extract matrix entry (i,j) from a runtime matrix tensor as an NF scalar.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_unsqueeze_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {shape : Spec.Shape} {xS : Spec.SpecTensor shape} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) shape} {eps : ℝ} (axis : ℕ) (hAxis : axis ≤ shape.rank) (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (TorchLean.Tensor.unsqueezeSpec xS axis hAxis) (xR.unsqueezeSpec axis hAxis) eps

Inserting a singleton axis is a reindexing operation and adds no numerical error.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_swapAdjacentAxes {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {shape : Spec.Shape} {depth : ℕ} {xS : Spec.SpecTensor shape} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) shape} {eps : ℝ} (hx : approxTensor toSpec xS xR eps) : approxTensor toSpec (TorchLean.Tensor.swapAdjacentAxes xS depth) (xR.swapAdjacentAxes depth) eps

Swapping any pair of adjacent axes preserves the approximation error budget.

noncomputable def Proofs.RuntimeApprox.NFBackend.dotStep {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {n : ℕ} (epsa epsb : ℝ) (aR bR : Fin n → FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ → Fin n → FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ

One fold step for building a dot-product and tracking a forward error bound.

This is used to bound the error of foldl (fun acc k => acc + aR k * bR k) compared to the corresponding spec (real) dot-product.

noncomputable def Proofs.RuntimeApprox.NFBackend.dotBound {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {n : ℕ} (epsa epsb : ℝ) (aR bR : Fin n → FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : ℝ

Closed-form bound for a runtime dot-product over List.finRange n.

dot_bound epsa epsb aR bR is the accumulated eps component produced by folding dotStep starting from 0.

noncomputable def Proofs.RuntimeApprox.NFBackend.matVecMulBoundTensor {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {m n : ℕ} (epsA epsV : ℝ) (A : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [m, n]) (v : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [n]) : Spec.SpecTensor [m]

Per-output bound tensor for matVecMulSpec.

Entry i is a dot-product bound for row i of A dotted with v, using dotBound.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_mat_vec_mul_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {m n : ℕ} {AS : Spec.SpecTensor [m, n]} {vS : Spec.SpecTensor [n]} {AR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [m, n]} {vR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [n]} {epsA epsV : ℝ} : approxTensor toSpec AS AR epsA → approxTensor toSpec vS vR epsV → approxTensor toSpec (Spec.matVecMulSpec AS vS) (Spec.matVecMulSpec AR vR) (linfNorm (matVecMulBoundTensor epsA epsV AR vR))

Forward approximation bound for matrix-vector multiplication.

In words: if A and v are each approximated by runtime AR/vR within epsA/epsV, then mat_vec_mul_spec AS vS is approximated by mat_vec_mul_spec AR vR, with error bounded by linf_norm (mat_vec_mul_bound_tensor epsA epsV AR vR).

noncomputable def Proofs.RuntimeApprox.NFBackend.matMulBoundTensor {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {m n p : ℕ} (epsA epsB : ℝ) (A : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [m, n]) (B : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [n, p]) : Spec.SpecTensor [m, p]

Per-entry bound tensor for matMulSpec.

Entry (i,j) is a dot-product bound for row i of A dotted with column j of B, using dotBound.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_mat_mul_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {m n p : ℕ} {AS : Spec.SpecTensor [m, n]} {BS : Spec.SpecTensor [n, p]} {AR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [m, n]} {BR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) [n, p]} {epsA epsB : ℝ} : approxTensor toSpec AS AR epsA → approxTensor toSpec BS BR epsB → approxTensor toSpec (Spec.matMulSpec AS BS) (Spec.matMulSpec AR BR) (linfNorm (matMulBoundTensor epsA epsB AR BR))

Forward approximation bound for matrix-matrix multiplication.

In words: if A and B are approximated by runtime matrices AR/BR within epsA/epsB, then mat_mul_spec AS BS is approximated by mat_mul_spec AR BR, with error bounded by linf_norm (mat_mul_bound_tensor epsA epsB AR BR).

def Proofs.RuntimeApprox.NFBackend.matrixTransposeNode {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {Γ : List Spec.Shape} {m n : ℕ} (x : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : FwdNode toSpec Γ (Spec.Shape.dim n (Spec.Shape.dim m Spec.Shape.scalar))

FwdNode for matrix transpose.

This lifts approxTensor_swapAdjacentAxes at depth zero into the FwdGraph interface so transposes can be used inside larger verified graphs.

noncomputable def Proofs.RuntimeApprox.NFBackend.matVecMulNode {β : 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)) : FwdNode toSpec Γ (Spec.Shape.dim m Spec.Shape.scalar)

FwdNode for matrix-vector multiplication.

The bound is computed by matVecMulBoundTensor and then reduced to a scalar budget via linfNorm.

noncomputable def Proofs.RuntimeApprox.NFBackend.matMulNode {β : 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))) : FwdNode toSpec Γ (Spec.Shape.dim m (Spec.Shape.dim p Spec.Shape.scalar))

FwdNode for matrix-matrix multiplication.

The bound is computed by matMulBoundTensor and then reduced to a scalar budget via linfNorm.