Conv2D

Conv2D CROWN-IBP bounds in TorchLean.

We provide:

• Interval Bound Propagation (IBP) for Conv2D pre-activations
• The exact flattened affine map for Conv2D

Design notes:

• We flatten the 3D input and convolution output when constructing the exact affine map. This reuses AffineVec without assigning a special semantic meaning to channel or spatial axes.
• The conv linear operator is explicitly materialized as a matrix Wconv whose rows correspond to output positions and columns to input positions. The verifier stays deterministic for the tensor sizes targeted by the CROWN operator layer.

def NN.MLTheory.CROWN.flattenBox {α : Type} [Context α] {s : Spec.Shape} (B : Box α s) : Box α (Spec.Shape.dim s.size Spec.Shape.scalar)

Flatten a Box to a 1D box by flattening both endpoints.

def NN.MLTheory.CROWN.ibpConv2d {α : Type} [Context α] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding α h1 h2 h3) (xB : Box α (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) : Box α (Spec.Shape.dim outC (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inH kH stride padding) (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inW kW stride padding) Spec.Shape.scalar)))

Interval Bound Propagation (IBP) for Conv2D pre-activations y = conv(x, K) + b.

This computes per-output-position min/max bounds by taking min/max of each product term.

def NN.MLTheory.CROWN.conv2dLinearMatrix {α : Type} [Context α] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding α h1 h2 h3) : have outH := Spec.Shape.slidingWindowOutDim inH kH stride padding; have outW := Spec.Shape.slidingWindowOutDim inW kW stride padding; have inShape := Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)); have outShape := Spec.Shape.dim outC (Spec.Shape.dim outH (Spec.Shape.dim outW Spec.Shape.scalar)); have nIn := inShape.size; have nOut := outShape.size; Spec.Tensor α (Spec.Shape.dim nOut (Spec.Shape.dim nIn Spec.Shape.scalar))

Build the explicit Conv2D linear operator matrix Wconv mapping flat input to flat output.

Shapes:

• Input: inC × inH × inW (flat size inC*inH*inW)
• Output (pre-activation, without bias): outC × outH × outW (flat size outC*outH*outW)

Entry Wconv[r,c] is the contribution of input coordinate c to output coordinate r.

def NN.MLTheory.CROWN.conv2dBiasBroadcast {α : Type} [Context α] {outC inH inW kH kW stride padding : ℕ} (bias : Spec.Tensor α (Spec.Shape.dim outC Spec.Shape.scalar)) : have outH := Spec.Shape.slidingWindowOutDim inH kH stride padding; have outW := Spec.Shape.slidingWindowOutDim inW kW stride padding; have outShape := Spec.Shape.dim outC (Spec.Shape.dim outH (Spec.Shape.dim outW Spec.Shape.scalar)); Spec.Tensor α (Spec.Shape.dim outShape.size Spec.Shape.scalar)

Broadcast a per-channel bias vector across spatial positions, as a flattened output vector.