NF Linear Algebra

Forward-error bounds for the noncomputable rounded-real NF model.

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 development separates scalar fold bounds for dot products from the tensor-level wrappers that turn those fold bounds into approxTensor theorems and graph nodes. Each dot product rounds multiplication and addition separately in increasing index order. These results do not establish a native GEMM or fused multiply-add error bound.

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

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) : ℝ

Accumulated error budget for a sequential dot product over List.finRange n. The initial zero contributes a conservative half ULP, followed by separate multiplication and addition budgets at each index.

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 matVecMulSpec AS vS is approximated by matVecMulSpec AR vR, with error bounded by linfNorm (matVecMulBoundTensor 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 matMulSpec AS BS is approximated by matMulSpec AR BR, with error bounded by linfNorm (matMulBoundTensor 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.