Conv2D Shared Bounds

Shared NF backend utilities for Conv2D forward/backward runtime-to-spec approximation.

This file contains the common arithmetic error updates and tensor-shaped Conv2D bound builders used by both ConvForward and ConvBackward. The node constructors live in the direction-specific files; the shared definitions stay here so the forward and VJP proofs do not duplicate the same fold/error algebra.

The key idea is to treat Conv2D as a pure spec definition (Spec.conv2d_spec / Spec.conv2d_backward_spec) instantiated at:

• spec scalars: ℝ
• runtime scalars: NF β fexp rnd (rounding after each primitive op)

and then prove explicit bounds of the form:

toSpec (runtime_result) ≈ spec_result

compatible with the tape/DAG composition theorems in:

• NN.Proofs.RuntimeApprox.Graph.ForwardApprox
• NN.Proofs.RuntimeApprox.Graph.BackwardApprox

PyTorch correspondence / citations

Our image tensor shape is C × H × W (no batch dimension), and the kernel shape is outC × inC × kH × kW. This matches the per-example core of PyTorch’s conv2d (which normally expects N × C × H × W inputs and supports extra features like groups). https://pytorch.org/docs/stable/generated/torch.nn.functional.conv2d.html https://pytorch.org/docs/stable/generated/torch.nn.Conv2d.html

Small helper bounds for list folds

noncomputable def Proofs.RuntimeApprox.NFBackend.addEps {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (accR termR : TorchLean.Floats.NF β fexp rnd) (epsAcc epsTerm : ℝ) : ℝ

Absolute-error update for one rounded addition in the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.mulEps {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (xR yR : TorchLean.Floats.NF β fexp rnd) (epsx epsy : ℝ) : ℝ

Absolute-error update for one rounded multiplication in the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.foldAddStateFrom {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {ι : Type} (l : List ι) (termR : ι → TorchLean.Floats.NF β fexp rnd) (epsTerm : ι → ℝ) (st0 : TorchLean.Floats.NF β fexp rnd × ℝ) : TorchLean.Floats.NF β fexp rnd × ℝ

Fold a rounded sum while tracking an absolute-error budget, starting from an explicit state.

noncomputable def Proofs.RuntimeApprox.NFBackend.foldAddState {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {ι : Type} (l : List ι) (termR : ι → TorchLean.Floats.NF β fexp rnd) (epsTerm : ι → ℝ) : TorchLean.Floats.NF β fexp rnd × ℝ

foldAddStateFrom started at (0,0).

theorem Proofs.RuntimeApprox.NFBackend.approx_fold_add_state {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {ι : Type} (l : List ι) (termS : ι → ℝ) (termR : ι → TorchLean.Floats.NF β fexp rnd) (epsTerm : ι → ℝ) (accS : ℝ) (st : TorchLean.Floats.NF β fexp rnd × ℝ) : |toSpec st.1 - accS| ≤ st.2 → (∀ i ∈ l, |toSpec (termR i) - termS i| ≤ epsTerm i) → |toSpec (List.foldl (fun (acc : TorchLean.Floats.NF β fexp rnd) (i : ι) => acc + termR i) st.1 l) - List.foldl (fun (acc : ℝ) (i : ι) => acc + termS i) accS l| ≤ (foldAddStateFrom l termR epsTerm st).2

theorem Proofs.RuntimeApprox.NFBackend.approx_fold_add {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {ι : Type} (l : List ι) (termS : ι → ℝ) (termR : ι → TorchLean.Floats.NF β fexp rnd) (epsTerm : ι → ℝ) (hTerm : ∀ i ∈ l, |toSpec (termR i) - termS i| ≤ epsTerm i) : |toSpec (List.foldl (fun (acc : TorchLean.Floats.NF β fexp rnd) (i : ι) => acc + termR i) 0 l) - List.foldl (fun (acc : ℝ) (i : ι) => acc + termS i) 0 l| ≤ (foldAddState l termR epsTerm).2

Component access: getAtOrZero respects approxT

theorem Proofs.RuntimeApprox.NFBackend.approx_get_at_or_zero {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} (_hx : approxT toSpec xS xR eps) (idx : List ℕ) : |toSpec (Spec.getAtOrZero xR idx) - Spec.getAtOrZero xS idx| ≤ eps

Padding reads

theorem Proofs.RuntimeApprox.NFBackend.approx_padded_input_read {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {inC inH inW padding : ℕ} {xS : Spec.MultiChannelImage inC inH inW ℝ} {xR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)} {epsX : ℝ} (hx : approxT toSpec xS xR epsX) (c : Fin inC) (p q : ℕ) : |toSpec (Spec.getAtOrZero (if h4 : padding = 0 then Spec.tensorCast (Spec.Shape.dim inC (Spec.Shape.dim (inH + 2 * padding) (Spec.Shape.dim (inW + 2 * padding) Spec.Shape.scalar))) ⋯ xR else Spec.padMultiChannel xR padding) [↑c, p, q]) - Spec.getAtOrZero (if h4 : padding = 0 then Spec.tensorCast (Spec.Shape.dim inC (Spec.Shape.dim (inH + 2 * padding) (Spec.Shape.dim (inW + 2 * padding) Spec.Shape.scalar))) ⋯ xS else Spec.padMultiChannel xS padding) [↑c, p, q]| ≤ epsX

Approximation bound for reading padded inputs.

Both the forward and backward Conv2D approximation proofs reduce to reading a padded input tensor at indices (c,p,q) and comparing the runtime read (in R) against the spec read (in ℝ).

Conv2D forward: pointwise error bound for one output scalar

def Proofs.RuntimeApprox.NFBackend.conv2dOutH (inH kH stride padding : ℕ) : ℕ

Output height for a 2D convolution.

def Proofs.RuntimeApprox.NFBackend.conv2dOutW (inW kW stride padding : ℕ) : ℕ

Output width for a 2D convolution.

noncomputable def Proofs.RuntimeApprox.NFBackend.conv2dPointBound {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layerR : Spec.Conv2DSpec inC outC kH kW stride padding (TorchLean.Floats.NF β fexp rnd) h1 h2 h3) (inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)) (epsK epsB epsX : ℝ) (out_ch : Fin outC) (i : Fin (conv2dOutH inH kH stride padding)) (j : Fin (conv2dOutW inW kW stride padding)) : ℝ

Pointwise absolute-error bound for one Conv2D output scalar in the NF backend.

Implementation note: we replay the same fold structure as Spec.conv2d_spec, but track an explicit absolute-error budget alongside the runtime accumulator. This keeps the bound aligned with the runtime addition order (which matters for worst-case rounding error).

noncomputable def Proofs.RuntimeApprox.NFBackend.conv2dBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layerR : Spec.Conv2DSpec inC outC kH kW stride padding (TorchLean.Floats.NF β fexp rnd) h1 h2 h3) (inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)) (epsK epsB epsX : ℝ) : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ

Tensor of pointwise Conv2D absolute-error bounds for the full output image.

conv2dPointBound and conv2dBoundTensor provide the data needed for a Conv2D runtime→spec approximation lemma, but the full end-to-end FwdNode/RevNode instances are intentionally deferred.

Reason: a direct proof that these bounds are sound for the current Spec.conv2d_spec definition is non-trivial and requires careful performance engineering (similar to the Conv2D fderiv file). The design intent is to keep Conv2D as a "big op" with its own proof module, instead of slowing down the core NF numeric library.