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.decodeFlatIndex : List ℕ → ℕ → List ℕ

Decode a row-major flat index into one coordinate per dimension.

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

Interval propagation for an arbitrary-dimensional convolution.

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 α) : have inShape := Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)); have outShape := Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)); TorchLean.Tensor α [outShape.size, inShape.size]

Explicit flattened linear operator for an arbitrary-dimensional convolution.

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

Flattened broadcast of a convolution bias over every output spatial position.