Convolution Bounds

CROWN-IBP bounds and an exact flattened affine map for arbitrary-dimensional convolution.

Design notes:

• We flatten the input and convolution output when constructing the exact affine map. This reuses AffineVec without assigning a special semantic meaning to any spatial axis.
• The convolution operator is explicitly materialized as a matrix 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} [TorchLean.Storage α] {s : Spec.Shape} (B : Box α s) : Box α (Spec.Shape.dim s.size Spec.Shape.scalar)

Flatten a Box to a rank-one box by flattening both endpoints.

def NN.MLTheory.CROWN.ibpConv {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding α) (dilation paddingAfter : TorchLean.Tensor ℕ [d]) (groups : ℕ) (leading : Spec.Shape) (xB : Box α (leading.concat (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))))) : Box α (leading.concat (Spec.Shape.ofList (outC :: (Spec.convOutSpatialDilated inSpatial kernel stride dilation padding paddingAfter).to (List ℕ))))

Interval propagation for grouped convolution with independent leading batches.

Products, accumulation and the final bias addition round outwards. Each row follows the channel/kernel fold order of the convolution specification.

def NN.MLTheory.CROWN.ibpConv.mapRows {α : Type} [TorchLean.Storage α] {d inC outC : ℕ} {inSpatial : TorchLean.Tensor ℕ [d]} (outSpatial : TorchLean.Tensor ℕ [d]) (row : Box α (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))) → Box α (Spec.Shape.ofList (outC :: outSpatial.to (List ℕ)))) (batch : Spec.Shape) : Box α (batch.concat (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) → Box α (batch.concat (Spec.Shape.ofList (outC :: outSpatial.to (List ℕ))))

def NN.MLTheory.CROWN.convKernelCoefficient {α : Type} [Context α] (kernel outIdx inputIdx stride dilation padding : List ℕ) (weight : List ℕ → α) : α

A convolution coefficient for one spatial input/output pair.

With positive dilation at most one kernel coordinate reaches the input coordinate. Reading that weight directly preserves its scalar value, including values that are not on a floating-point grid. Zero dilation can make several kernel coordinates coincide, so that case retains the sum.

def NN.MLTheory.CROWN.convLinearMatrix {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding α) (dilation paddingAfter : TorchLean.Tensor ℕ [d]) (groups : ℕ) (leading : Spec.Shape) : have inShape := leading.concat (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))); have outShape := leading.concat (Spec.Shape.ofList (outC :: (Spec.convOutSpatialDilated inSpatial kernel stride dilation padding paddingAfter).to (List ℕ))); TorchLean.Tensor α [outShape.size, inShape.size]

Explicit matrix for grouped convolution, block diagonal over the leading batch shape.

def NN.MLTheory.CROWN.convBiasBroadcast {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {outSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) (leading : Spec.Shape) : have outShape := leading.concat (Spec.Shape.ofList (outC :: outSpatial.to (List ℕ))); TorchLean.Tensor α [outShape.size]

Flattened broadcast of a convolution bias over spatial and leading batch coordinates.