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) (s : Spec.Shape) : Type

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

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

• lo : Spec.Tensor α s

  Elementwise lower bound.

• hi : Spec.Tensor α s

  Elementwise upper bound.

def NN.MLTheory.CROWN.Box.width {α : Type} [Context α] {s : Spec.Shape} (b : Box α s) : Spec.Tensor α s

Pointwise box width hi - lo.

def NN.MLTheory.CROWN.Box.center {α : Type} [Context α] {s : Spec.Shape} (b : Box α s) : Spec.Tensor α s

Pointwise box center (lo + hi)/2.

def NN.MLTheory.CROWN.Box.radius {α : Type} [Context α] {s : Spec.Shape} (b : Box α s) : Spec.Tensor α s

Pointwise box radius (hi - lo)/2.

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

Boolean a <= b using only the backend's decidable > from Context.

This is useful for executable checks in backends that do not provide a decidable <=.

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

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

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

def NN.MLTheory.CROWN.Box.contains {α : Type} [Context α] {s : Spec.Shape} : Box α s → Spec.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, IEEE32Exec), we also expose a checker that uses ≤ directly. We implement it by structural recursion (rather than decide (Box.contains ...)) so it remains executable.

@[inline]

def NN.MLTheory.CROWN.Box.leDecBool {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a b : α) : Bool

Boolean a ≤ b using an explicit DecidableRel (· ≤ ·) argument.

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

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

theorem NN.MLTheory.CROWN.Box.containsDecBool_sound {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {s : Spec.Shape} (b : Box α s) (x : Spec.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} {s : Spec.Shape} (t : Spec.Tensor α s) : Box α s

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

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

Cast the lower endpoint to a checked vector dimension.

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

Cast the upper endpoint to a checked vector dimension.

def NN.MLTheory.CROWN.FlatBox.toVecBox {α : Type} [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.

We primarily target vector inputs/outputs for CROWN in this initial integration. To avoid over-generalizing shapes, we use a specialized variant for 1D (flat) vectors.

structure NN.MLTheory.CROWN.AffineVec (α : Type) (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 : Spec.Tensor α (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))

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

• c : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)

  Constant offset vector.

def NN.MLTheory.CROWN.AffineVec.evalOnBox {α : Type} [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} [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.compose {α : Type} [Context α] {n h m : ℕ} (aff2 : AffineVec α h m) (aff1 : AffineVec α n h) : AffineVec α n m

Compose two affine forms: (aff2 ∘ aff1)(x) = aff2(aff1(x)).

def NN.MLTheory.CROWN.AffineVec.ofLinear {α : Type} {inDim outDim : ℕ} (W : Spec.Tensor α (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (b : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)) : AffineVec α inDim outDim

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

def NN.MLTheory.CROWN.IBP.linear {α : Type} [Context α] [BoundOps α] {m n : ℕ} (W : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (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).