Rounded Convolution

Forward- and reverse-mode error bounds for channels-first convolution at arbitrary spatial rank. The bounds replay the exact ordered folds in Spec.convSpec and Spec.convBackwardSpec; no associativity of rounded addition is assumed.

Ordered rounded sums

noncomputable def Proofs.RuntimeApprox.NFBackend.accumulationError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (acc term : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (accError termError : ℝ) : ℝ

Error budget after one rounded addition.

noncomputable def Proofs.RuntimeApprox.NFBackend.productError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (x y : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (xError yError : ℝ) : ℝ

Error budget after one rounded multiplication.

noncomputable def Proofs.RuntimeApprox.NFBackend.foldErrorState {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {iota : Type} (indices : List iota) (term : iota → FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (termError : iota → ℝ) (initial : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd × ℝ) : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd × ℝ

Replay a rounded sum while carrying its absolute-error budget.

noncomputable def Proofs.RuntimeApprox.NFBackend.foldError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {iota : Type} (indices : List iota) (term : iota → FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (termError : iota → ℝ) : ℝ

Error budget for a rounded sum beginning at zero.

theorem Proofs.RuntimeApprox.NFBackend.approx_fold {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {iota : Type} (indices : List iota) (ideal : iota → ℝ) (rounded : iota → FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (termError : iota → ℝ) (hTerm : ∀ index ∈ indices, |toSpec (rounded index) - ideal index| ≤ termError index) : |toSpec (List.foldl (fun (acc : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (index : iota) => acc + rounded index) 0 indices) - List.foldl (fun (acc : ℝ) (index : iota) => acc + ideal index) 0 indices| ≤ foldError indices rounded termError

A fold of individually bounded rounded terms is bounded by foldError.

noncomputable def Proofs.RuntimeApprox.NFBackend.productFoldError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {iota : Type} (indices : List iota) (left right : iota → FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (leftError rightError : iota → ℝ) : ℝ

Replay bound for a dot product whose two arguments are already approximated pointwise.

theorem Proofs.RuntimeApprox.NFBackend.approx_product_fold {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {iota : Type} (indices : List iota) (leftIdeal rightIdeal : iota → ℝ) (leftRounded rightRounded : iota → FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (leftError rightError : iota → ℝ) (hLeft : ∀ index ∈ indices, |toSpec (leftRounded index) - leftIdeal index| ≤ leftError index) (hRight : ∀ index ∈ indices, |toSpec (rightRounded index) - rightIdeal index| ≤ rightError index) : |toSpec (List.foldl (fun (acc : FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (index : iota) => acc + leftRounded index * rightRounded index) 0 indices) - List.foldl (fun (acc : ℝ) (index : iota) => acc + leftIdeal index * rightIdeal index) 0 indices| ≤ productFoldError indices leftRounded rightRounded leftError rightError

An ordered rounded dot product is enclosed by productFoldError.

Arbitrary-rank index traversal

def Proofs.RuntimeApprox.NFBackend.enumerateIndices : List ℕ → List (List ℕ)

Runtime order of all bounded coordinates of a list-shaped tensor.

theorem Proofs.RuntimeApprox.NFBackend.foldlIndices_eq_enumerateIndices {a : Type} (dims : List ℕ) (initial : a) (step : a → List ℕ → a) : Spec.Conv.Internal.foldlIndices dims initial step = List.foldl step initial (enumerateIndices dims)

The nested index loop equals a single fold over the flattened index list.

This is the workhorse of the file. The implementation loops over dimensions recursively, whereas an error bound is much easier to state as one sum over coordinates; turning one into the other once, here, keeps every later bound free of nested inductions.

def Proofs.RuntimeApprox.NFBackend.enumerateChannelIndices (channels : ℕ) (dims : List ℕ) : List (Fin channels × List ℕ)

Flatten a channel loop followed by an arbitrary spatial index loop.

theorem Proofs.RuntimeApprox.NFBackend.foldChannelsIndices_eq_foldl {a : Type} (channels : ℕ) (dims : List ℕ) (initial : a) (step : a → Fin channels → List ℕ → a) : List.foldl (fun (state : a) (channel : Fin channels) => Spec.Conv.Internal.foldlIndices dims state fun (x1 : a) (x2 : List ℕ) => step x1 channel x2) initial (List.finRange channels) = List.foldl (fun (state : a) (index : Fin channels × List ℕ) => step state index.1 index.2) initial (enumerateChannelIndices channels dims)

Same flattening one level up, for the channel loop wrapped around the spatial loop.

Tensor coordinates

theorem Proofs.RuntimeApprox.NFBackend.approx_getAtOrZero {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {shape : Spec.Shape} {ideal : TorchLean.Tensor ℝ shape} {rounded : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) shape} {error : ℝ} (h : approxTensor toSpec ideal rounded error) (index : List ℕ) : |toSpec (Spec.getAtOrZero rounded index) - Spec.getAtOrZero ideal index| ≤ error

Total tensor lookup preserves a uniform tensor approximation.

Forward convolution

def Proofs.RuntimeApprox.NFBackend.convolutionInputValue {alpha : Type} [Context alpha] {d inC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (input : TorchLean.Tensor alpha (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (outIndex : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) (index : Fin inC × List ℕ) : alpha

The input element a convolution reads for one output position and one (channel, offset) pair, or zero when the strided, padded index falls outside the input.

Naming the read explicitly is what lets the approximation proof treat padding as an exact zero rather than as another rounded value.

def Proofs.RuntimeApprox.NFBackend.convolutionWeightValue {alpha : Type} [Context alpha] {d inC outC : ℕ} {kernel : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor alpha (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (outChannel : Fin outC) (index : Fin inC × List ℕ) : alpha

The weight a given input coordinate is multiplied by, as the implementation reads it.

Named so the error bound can talk about the summands of the accumulation in the same order the code produces them, which is what makes the bound tight rather than merely valid.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionPointError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)) (input : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (weightError biasError inputError : ℝ) (outChannel : Fin outC) (outIndex : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : ℝ

Absolute-error budget for one coordinate of a rounded arbitrary-rank convolution.

The budget follows the implementation's multiplication and accumulation order, then accounts for the final bias addition.

theorem Proofs.RuntimeApprox.NFBackend.approx_convSpec_coordinate {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} {idealLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ} {roundedLayer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {weightError biasError inputError : ℝ} (hWeight : approxTensor toSpec idealLayer.kernel roundedLayer.kernel weightError) (hBias : approxTensor toSpec idealLayer.bias roundedLayer.bias biasError) (hInput : approxTensor toSpec idealInput roundedInput inputError) (outChannel : Fin outC) (outIndex : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : |toSpec (Spec.Conv.Internal.MultiIndex.get (Spec.convSpec roundedLayer roundedInput) (outChannel, outIndex)) - Spec.Conv.Internal.MultiIndex.get (Spec.convSpec idealLayer idealInput) (outChannel, outIndex)| ≤ convolutionPointError roundedLayer roundedInput weightError biasError inputError outChannel outIndex

One coordinate of rounded convolution is enclosed by convolutionPointError.

Backward convolution

def Proofs.RuntimeApprox.NFBackend.kernelGradientInputValue {alpha : Type} [Context alpha] {d inC : ℕ} {kernel inSpatial : TorchLean.Tensor ℕ [d]} (stride padding : TorchLean.Tensor ℕ [d]) (input : TorchLean.Tensor alpha (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (inChannel : Fin inC) (kernelIndex : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ))) (outIndex : List ℕ) : alpha

The input value entering one term of the kernel-gradient accumulation, zero outside the padding.

def Proofs.RuntimeApprox.NFBackend.kernelGradientOutputValue {alpha : Type} [Context alpha] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (gradOutput : TorchLean.Tensor alpha (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (outChannel : Fin outC) (outIndex : List ℕ) : alpha

The output-gradient value entering that same term.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionKernelGradientPointError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (input : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (inputError gradOutputError : ℝ) (outChannel : Fin outC) (inChannel : Fin inC) (kernelIndex : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ))) : ℝ

Error budget for one coordinate of the rounded convolution kernel gradient.

theorem Proofs.RuntimeApprox.NFBackend.approx_convKernelDerivSpec_coordinate {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} {idealLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ} {roundedLayer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {idealGradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {roundedGradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {inputError gradOutputError : ℝ} (hInput : approxTensor toSpec idealInput roundedInput inputError) (hGradOutput : approxTensor toSpec idealGradOutput roundedGradOutput gradOutputError) (outChannel : Fin outC) (inChannel : Fin inC) (kernelIndex : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ))) : |toSpec (Spec.Conv.Internal.MultiIndex.get (Spec.convKernelDerivSpec roundedLayer roundedInput roundedGradOutput) (outChannel, inChannel, kernelIndex)) - Spec.Conv.Internal.MultiIndex.get (Spec.convKernelDerivSpec idealLayer idealInput idealGradOutput) (outChannel, inChannel, kernelIndex)| ≤ convolutionKernelGradientPointError roundedInput roundedGradOutput inputError gradOutputError outChannel inChannel kernelIndex

Every coordinate of the rounded kernel gradient encloses its ideal real value.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionBiasGradientPointError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (gradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (gradOutputError : ℝ) (outChannel : Fin outC) : ℝ

Error budget for one coordinate of the rounded convolution bias gradient.

theorem Proofs.RuntimeApprox.NFBackend.approx_convBiasDerivSpec_coordinate {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} {idealLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ} {roundedLayer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {idealGradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {roundedGradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {gradOutputError : ℝ} (hGradOutput : approxTensor toSpec idealGradOutput roundedGradOutput gradOutputError) (outChannel : Fin outC) : |toSpec (Spec.Conv.Internal.MultiIndex.get (Spec.convBiasDerivSpec roundedLayer roundedInput roundedGradOutput) (outChannel, PUnit.unit)) - Spec.Conv.Internal.MultiIndex.get (Spec.convBiasDerivSpec idealLayer idealInput idealGradOutput) (outChannel, PUnit.unit)| ≤ convolutionBiasGradientPointError roundedGradOutput gradOutputError outChannel

Every coordinate of the rounded bias gradient encloses its ideal real value.

def Proofs.RuntimeApprox.NFBackend.inputGradientTermValue {alpha : Type} [Context alpha] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding alpha) (gradOutput : TorchLean.Tensor alpha (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (inChannel : Fin inC) (inputIndex : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) (index : Fin outC × List ℕ) : alpha

One summand of the input-gradient accumulation: an output gradient times the kernel weight that connected them, or zero when the transposed index falls outside the input.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionInputGradientPointError {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)) (gradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (weightError gradOutputError : ℝ) (inChannel : Fin inC) (inputIndex : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) : ℝ

Error budget for one coordinate of the rounded convolution input gradient.

theorem Proofs.RuntimeApprox.NFBackend.approx_convInputDerivSpec_coordinate {beta : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} {idealLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ} {roundedLayer : Spec.ConvSpec d inC outC kernel stride padding (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {idealGradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {roundedGradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF beta fexp rnd) (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))} {weightError gradOutputError : ℝ} (hWeight : approxTensor toSpec idealLayer.kernel roundedLayer.kernel weightError) (hGradOutput : approxTensor toSpec idealGradOutput roundedGradOutput gradOutputError) (inChannel : Fin inC) (inputIndex : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) : |toSpec (Spec.Conv.Internal.MultiIndex.get (Spec.convInputDerivSpec roundedLayer roundedInput roundedGradOutput) (inChannel, inputIndex)) - Spec.Conv.Internal.MultiIndex.get (Spec.convInputDerivSpec idealLayer idealInput idealGradOutput) (inChannel, inputIndex)| ≤ convolutionInputGradientPointError roundedLayer roundedGradOutput weightError gradOutputError inChannel inputIndex

Every coordinate of the rounded input gradient encloses its ideal real value.