Runtime CROWN operators

Executable helper operators for the graph-based CROWN/IBP engine.

This file keeps runtime certificate replay separate from proof imports:

• Some proof-facing CROWN modules import Mathlib and large theorem developments. Native executables that only replay certificates should not pay that import cost.
• The graph verifier and executable certificate checks only need a compact set of computational definitions: ReLU relaxations plus interval rules for a few scalar activations.

These definitions live under NN.MLTheory.CROWN.Runtime.Ops, with no direct Mathlib dependency. The proof modules can cite these functions, but this file itself stays focused on the runtime support code used for fast certificate replay.

References (bound propagation background):

• Zhang et al., "Efficient Neural Network Robustness Certification with General Activation Functions" (CROWN), 2018: https://arxiv.org/abs/1811.00866
• Singh et al., "An Abstract Domain for Certifying Neural Networks" (DeepPoly), POPL 2019.

structure NN.MLTheory.CROWN.Runtime.Ops.ReLURelax (α : Type) : Type

Parameters of a per-neuron affine relaxation y = slope * x + bias used in CROWN/DeepPoly.

• slope : α

  Linear coefficient.

• bias : α

  Constant offset.

def NN.MLTheory.CROWN.Runtime.Ops.ReLU.relaxScalar {α : Type} [Context α] (l u : α) : ReLURelax α

Upper (over-approx) affine relaxation for ReLU on an interval [l,u].

Returns parameters (slope, bias) for a line y = slope * x + bias that upper-bounds relu x for all x ∈ [l,u].

Lower (under-approx) relaxation for ReLU.

For crossing bounds l < 0 < u, basic CROWN/DeepPoly chooses either:

• y ≥ 0 (slope 0), or
• y ≥ x (slope 1), based on which side of 0 is “wider”. This keeps the relaxation sound without α-optimization.

def NN.MLTheory.CROWN.Runtime.Ops.ReLU.relaxScalarLower {α : Type} [Context α] (l u : α) : ReLURelax α

def NN.MLTheory.CROWN.Runtime.Ops.ReLU.relaxVector {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)

Vectorized relax_scalar, applied componentwise to lo/hi.

def NN.MLTheory.CROWN.Runtime.Ops.ReLU.relaxVectorLower {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)

Vectorized relax_scalar_lower, applied componentwise to lo/hi.

def NN.MLTheory.CROWN.Runtime.Ops.ReLU.propagateAffine {α : Type} [Context α] {inDim hidDim : ℕ} (relax : Spec.Tensor (ReLURelax α) (Spec.Shape.dim hidDim Spec.Shape.scalar)) (aff : AffineVec α inDim hidDim) : AffineVec α inDim hidDim

Propagate an affine form through ReLU using a per-neuron relaxation.

Given y ≈ A*x + c and per-output relaxations (slopeᵢ, biasᵢ), produces the affine form y' ≈ diag(slope) * (A*x + c) + bias.

def NN.MLTheory.CROWN.Runtime.Ops.IBP.mapMinmax {α : Type} [Context α] {n : ℕ} (f : α → α) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Generic elementwise bound propagation for monotone activations (min/max of endpoints).

def NN.MLTheory.CROWN.Runtime.Ops.IBP.sigmoid {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bound propagation for sigmoid (monotone, so min/max of endpoints).

def NN.MLTheory.CROWN.Runtime.Ops.IBP.tanh {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bound propagation for tanh (monotone, so min/max of endpoints).

def NN.MLTheory.CROWN.Runtime.Ops.IBP.sin {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Conservative IBP for sin using a 1-Lipschitz enclosure: sin([l,u]) ⊆ [sin(m)-r, sin(m)+r] ∩ [-1,1], m=(l+u)/2, r=(u-l)/2.

This avoids periodic case splits (no floor/ceil in Context α) while remaining sound.

def NN.MLTheory.CROWN.Runtime.Ops.IBP.cos {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Same 1-Lipschitz enclosure as IBP.sin, but for cos.