Rounded Convolution

Forward- and reverse-mode error bounds for channels-first convolution at arbitrary spatial rank. The bounds follow the ordered folds in Spec.convSpec and Spec.convBackwardSpec, with separate rounding of products and sums. They do not assume associativity of rounded addition or verify LibTorch's convolution kernels. Inputs and weights are tensors; lists describe the internal coordinate traversal, whose order must be preserved by any replacement implementation.

Ordered rounded sums

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

Error budget after one rounded addition.

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

Error budget after one rounded multiplication.

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

Fold rounded terms with their absolute-error budgets, in the supplied index order.

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

Error budget for a rounded sum beginning at zero.

theorem Proofs.RuntimeApprox.NFBackend.approx_fold {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {ι : Type} (indices : List ι) (ideal : ι → ℝ) (rounded : ι → FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (termError : ι → ℝ) (hTerm : ∀ index ∈ indices, |toSpec (rounded index) - ideal index| ≤ termError index) : |toSpec (List.foldl (fun (acc : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (index : ι) => acc + rounded index) 0 indices) - List.foldl (fun (acc : ℝ) (index : ι) => 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 {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {ι : Type} (indices : List ι) (left right : ι → FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (leftError rightError : ι → ℝ) : ℝ

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

theorem Proofs.RuntimeApprox.NFBackend.approx_product_fold {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {ι : Type} (indices : List ι) (leftIdeal rightIdeal : ι → ℝ) (leftRounded rightRounded : ι → FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (leftError rightError : ι → ℝ) (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 β fexp rnd) (index : ι) => acc + leftRounded index * rightRounded index) 0 indices) - List.foldl (fun (acc : ℝ) (index : ι) => 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 {α : Type} (dims : List ℕ) (initial : α) (step : α → List ℕ → α) : 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.

Flattening preserves the nested loop's order; it does not replace the rounded fold by an unordered sum.

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 {α : Type} (channels : ℕ) (dims : List ℕ) (initial : α) (step : α → Fin channels → List ℕ → α) : List.foldl (fun (state : α) (channel : Fin channels) => Spec.Conv.Internal.foldlIndices dims state fun (x1 : α) (x2 : List ℕ) => step x1 channel x2) initial (List.finRange channels) = List.foldl (fun (state : α) (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 {β : 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 β 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 {α : Type} [Context α] {d inC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (input : TorchLean.Tensor α (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (outIndex : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) (index : Fin inC × List ℕ) : α

Input element for an output position and (channel, offset) pair, or zero outside the input.

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

Weight used by one (input channel, kernel offset) pair at the selected output channel.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionPointError {β : 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 β fexp rnd)) (input : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 spec's multiplication and accumulation order, then accounts for the final bias addition. It is conservative: padded reads still receive the uniform input-error budget even though their exact and rounded values are both zero.

theorem Proofs.RuntimeApprox.NFBackend.approx_convSpec_coordinate {β : 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 β fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 {α : Type} [Context α] {d inC : ℕ} {kernel inSpatial : TorchLean.Tensor ℕ [d]} (stride padding : TorchLean.Tensor ℕ [d]) (input : TorchLean.Tensor α (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (inChannel : Fin inC) (kernelIndex : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ))) (outIndex : List ℕ) : α

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

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

The output-gradient value entering that same term.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionKernelGradientPointError {β : 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 β fexp rnd) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 {β : 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 β fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 β 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 {β : 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 β 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 {β : 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 β fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 β 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 {α : Type} [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding α) (gradOutput : TorchLean.Tensor α (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 ℕ) : α

Input-gradient summand: an output gradient times its kernel weight, or zero when the transposed index has no corresponding output position.

noncomputable def Proofs.RuntimeApprox.NFBackend.convolutionInputGradientPointError {β : 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 β fexp rnd)) (gradOutput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 {β : 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 β fexp rnd)} {idealInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))} {roundedInput : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β 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 β 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.