CROWN Core

CROWN core definitions for TorchLean.

This file defines:

• Box: element-wise lower/upper bounds (intervals) on tensors
• AffineBounds: per-output affine forms w.r.t. input x, and constant
• Utilities for splitting positive/negative parts and safe affine eval

References:

• Zhang et al., "Efficient Neural Network Robustness Certification with General Activation Functions" (CROWN), arXiv:1811.00866.
• Xu et al., "Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond" (auto_LiRPA), NeurIPS 2020, arXiv:2002.12920. This generalizes LiRPA/CROWN to arbitrary computational graphs and introduces techniques (e.g., loss fusion) widely used in scalable certified training.

structure NN.MLTheory.CROWN.Box (α : Type) [TorchLean.Storage α] (s : Spec.Shape) : Type

Interval box lo <= x <= hi over a tensor shape.

This is the fundamental object for interval bound propagation (IBP).

• lo : TorchLean.Tensor α s

  Elementwise lower bound.

• hi : TorchLean.Tensor α s

  Elementwise upper bound.

def NN.MLTheory.CROWN.Box.leBool {α : Type} [Context α] (a b : α) : Bool

Boolean a <= b using the backend's strict order and Boolean equality.

Reflexivity guards reject NaNs even on backends whose strict comparison uses a total implementation order. For a logical containment theorem, use containsDecBool.

def NN.MLTheory.CROWN.Box.containsBool {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : Box α s → TorchLean.Tensor α s → Bool

Executable containment check: returns true iff every component is within bounds.

This uses leBool and is therefore available for any Context α.

def NN.MLTheory.CROWN.Box.contains {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : Box α s → TorchLean.Tensor α s → Prop

Logical containment: every component of x lies between lo and hi.

containsBool above is a minimal Context-only checker that avoids requiring decidable ≤.

For backends that do provide decidable ≤ (e.g. ℝ, Float, ExecFloat.Binary 8 23), we also expose a checker that uses ≤ directly. We implement it by structural recursion (rather than decide (Box.contains ...)) so it remains executable.

def NN.MLTheory.CROWN.Box.containsDecBool {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {s : Spec.Shape} : Box α s → TorchLean.Tensor α s → Bool

Boolean containment check using decidable ≤ and a finite fold over indices.

theorem NN.MLTheory.CROWN.Box.containsDecBool_sound {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {s : Spec.Shape} (b : Box α s) (x : TorchLean.Tensor α s) : b.containsDecBool x = true → b.contains x

Soundness of containsDecBool: if the Boolean checker returns true, then Box.contains holds.

def NN.MLTheory.CROWN.Box.point {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : Box α s

Degenerate (Dirac) box with lo = hi = t.

theorem NN.MLTheory.CROWN.Box.contains_point_self {α : Type} [TorchLean.Storage α] [Context α] [Std.Refl fun (x1 x2 : α) => x1 ≤ x2] {s : Spec.Shape} (t : TorchLean.Tensor α s) : (point t).contains t

A tensor is contained in its own degenerate box.

def NN.MLTheory.CROWN.FlatBox.loAsDim {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) {m : ℕ} (h : B.dim = m) : TorchLean.Tensor α [m]

Cast the lower endpoint to a checked vector dimension.

def NN.MLTheory.CROWN.FlatBox.hiAsDim {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) {m : ℕ} (h : B.dim = m) : TorchLean.Tensor α [m]

Cast the upper endpoint to a checked vector dimension.

def NN.MLTheory.CROWN.FlatBox.getScalarBox {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) {m : ℕ} (h : B.dim = m) : Box α (Spec.Shape.dim m Spec.Shape.scalar)

View a flattened interval box as a shape-indexed vector box after checking the dimension.

Most CROWN affine evaluators expect a Box α (.dim m .scalar), while graph propagation stores runtime-shaped FlatBox values. This helper keeps the dependent casts in one place.

CROWN affine bounds use one matrix row per output scalar and one column per input scalar. A tensor of shape s contributes s.size coordinates to this flat representation. Graph nodes retain their tensor shapes, and each transfer checks its operator's shape contract.

Graph matmul uses the canonical IR contract, including vector promotion and broadcasting of leading batch axes. The matrix sign-splitting and affine evaluation below operate on the flattened coefficient matrix; they do not restrict the original graph operands to that matrix shape.

structure NN.MLTheory.CROWN.AffineVec (α : Type) [TorchLean.Storage α] (inDim outDim : ℕ) : Type

Affine form y = A*x + c over flat vectors.

This is the representation used by CROWN/DeepPoly-style affine bound propagation.

• A : TorchLean.Tensor α [outDim, inDim]

  Coefficient matrix; each row is an output affine coefficient vector.

• c : TorchLean.Tensor α [outDim]

  Constant offset vector.

def NN.MLTheory.CROWN.IBP.matPos {α : Type} [TorchLean.Storage α] [Context α] {m n : ℕ} (W : TorchLean.Tensor α [m, n]) : TorchLean.Tensor α [m, n]

Positive part of a weight matrix, W⁺ = max(W, 0), used by sign-split bound rules.

def NN.MLTheory.CROWN.IBP.matNeg {α : Type} [TorchLean.Storage α] [Context α] {m n : ℕ} (W : TorchLean.Tensor α [m, n]) : TorchLean.Tensor α [m, n]

Negative part of a weight matrix, W⁻ = min(W, 0), used by sign-split bound rules.

def NN.MLTheory.CROWN.IBP.linear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] {m n : ℕ} (W : TorchLean.Tensor α [m, n]) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (bB : Box α (Spec.Shape.dim m Spec.Shape.scalar)) : Box α (Spec.Shape.dim m Spec.Shape.scalar)

Interval bound propagation for a linear layer.

Given interval inputs xB and bB, this returns an interval box for W*x + b by:

• computing per-coefficient endpoint products with directed rounding (BoundOps.mulDown/mulUp), and
• summing with directed rounding (addDown/addUp).

def NN.MLTheory.CROWN.AffineVec.evalOnBox {α : Type} [TorchLean.Storage α] [Context α] {inDim outDim : ℕ} [BoundOps α] (aff : AffineVec α inDim outDim) (B : Box α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

Evaluate an affine form on an input box, producing an output box.

This performs the standard interval evaluation for linear forms by taking, per coefficient a, the appropriate endpoint (lo or hi) to minimize/maximize a*x.

def NN.MLTheory.CROWN.AffineVec.evalOnFlatBox {α : Type} [TorchLean.Storage α] [Context α] {inDim outDim : ℕ} [BoundOps α] (aff : AffineVec α inDim outDim) (B : FlatBox α) (h : B.dim = inDim) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

Evaluate an affine form on a flattened graph box after checking the input dimension.

Graph-level CROWN stores boxes as FlatBox; affine evaluation works over vector-shaped boxes. This helper keeps that cast at the CROWN boundary instead of repeating it in verifier workflows.

def NN.MLTheory.CROWN.AffineVec.ofLinear {α : Type} [TorchLean.Storage α] {inDim outDim : ℕ} (W : TorchLean.Tensor α [outDim, inDim]) (b : TorchLean.Tensor α [outDim]) : AffineVec α inDim outDim

Build an affine form from a linear layer y = W*x + b.