Conv2D

Conv2D CROWN-IBP bounds in TorchLean.

We provide:

• Interval Bound Propagation (IBP) for Conv2D pre-activations
• A CROWN-IBP affine bound for Conv2D+ReLU, evaluated on a flattened input box

Design notes:

• For simplicity and generality, we flatten the 3D image input and the 3D conv output to 1D vectors when evaluating affine forms. This reuses AffineVec and its safe evaluation on input boxes.
• The conv linear operator is explicitly materialized as a matrix Wconv whose rows correspond to output positions and columns to input positions. This keeps the verifier simple and deterministic for the tensor sizes targeted by the CROWN operator layer.

def NN.MLTheory.CROWN.flattenBox {α : Type} {s : Spec.Shape} (B : Box α s) [Inhabited α] : 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 ((inH + 2 * padding - kH) / stride + 1) (Spec.Shape.dim ((inW + 2 * padding - kW) / stride + 1) 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 := (inH + 2 * padding - kH) / stride + 1; have outW := (inW + 2 * padding - kW) / stride + 1; 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.matRowScaleSpec {α : Type} [Context α] {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Spec.Tensor α (Spec.Shape.dim m Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))

Row-wise scaling of a matrix by a vector: scale each row i by v[i].

def NN.MLTheory.CROWN.conv2dBiasBroadcast {α : Type} [Zero α] {outC inH inW kH kW stride padding : ℕ} (bias : Spec.Tensor α (Spec.Shape.dim outC Spec.Shape.scalar)) : have outH := (inH + 2 * padding - kH) / stride + 1; have outW := (inW + 2 * padding - kW) / stride + 1; 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.

def NN.MLTheory.CROWN.crownConv2dAffineForm {α : Type} [Context α] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} [Inhabited α] (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)))) : AffineVec α (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar))).size (Spec.Shape.dim outC (Spec.Shape.dim ((inH + 2 * padding - kH) / stride + 1) (Spec.Shape.dim ((inW + 2 * padding - kW) / stride + 1) Spec.Shape.scalar))).size

Construct the CROWN-IBP affine form for Conv2D followed by ReLU, with respect to the flattened input.

This returns an AffineVec (A,c) so it can be composed with subsequent linear layers. Evaluation on an input box can then be performed with AffineVec.eval_on_box.

def NN.MLTheory.CROWN.crownConv2dAffineFlat {α : Type} [Context α] {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} [Inhabited α] (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 * ((inH + 2 * padding - kH) / stride + 1) * ((inW + 2 * padding - kW) / stride + 1)) Spec.Shape.scalar)

Evaluate the Conv2D+ReLU CROWN-IBP affine bound on a flattened input box.

Returns a Box over the flattened conv output dimension.