Directed-rounding primitives for interval propagation

TorchLean’s IBP/CROWN code represents bounds as endpoint pairs (lo/hi) inside Box/FlatBox. To make those bounds meaningful under different numeric semantics, we abstract the primitive endpoint operations (directed rounding).

Intuition:

• For pure real/interval backends, using ordinary +/* is already enclosure-safe (because the scalar itself is an interval type with outward rounding).
• For finite-precision backends with discrete grids (e.g. ExecFloat.Binary 8 23), we want directed rounding primitives like addDown/addUp and mulDown/mulUp so that interval propagation encloses the corresponding exact real operation.

This file defines two small numeric interfaces:

• BoundOps for directed elementary arithmetic; and
• NonlinearBoundOps for interval transfers that may be unavailable on a backend.

There is intentionally no generic fallback for BoundOps: ordinary finite-precision arithmetic is not directed rounding and must not silently enter a sound bound-propagation path. The nonlinear interface does have a conservative fallback for bounded activations, but operations with unbounded ranges return none unless the scalar backend supplies an implementation. Soundness is a separate obligation, recorded by LawfulNonlinearBoundOps.

Integration points in the current codebase

The intended usage is:

• Keep graphs/layers scalar-polymorphic over [TorchLean.Storage α] [Context α].
• When a routine propagates bounds (IBP/affine/CROWN), also require [BoundOps α] and use addDown/addUp/subDown/subUp/mulDown/mulUp at the endpoints.

Concretely:

• NN/MLTheory/CROWN/Core.lean
  • AffineVec.evalOnBox: min/max over products and accumulation use BoundOps.
  • IBP.linear: interval linear layer propagation uses BoundOps.
• NN.MLTheory.CROWN.Graph
  • boxAdd, boxSub, boxMulElem: endpoint propagation uses BoundOps.

Executable certificate replay relies on this separation. A backend may support directed binary arithmetic without having a correctly rounded exp or log; in that case the graph checker leaves the corresponding node unresolved instead of treating an ordinary library call as an enclosure.

BoundOps α

BoundOps supplies directed-rounding versions of the arithmetic primitives that appear in IBP for affine/linear layers and basic arithmetic nodes.

If you want to swap in a quantized backend, the key is to provide an instance of BoundOps for your scalar type.

class NN.MLTheory.CROWN.BoundOps (α : Type) [TorchLean.Storage α] [Context α] : Type

• addDown : α → α → α
• addUp : α → α → α
• subDown : α → α → α
• subUp : α → α → α
• mulDown : α → α → α
• mulUp : α → α → α
• supportsExactAffineReassociation : Bool

  Whether ordinary scalar algebra may be reassociated without a rounding error.

@[inline]

def NN.MLTheory.CROWN.BoundOps.min2 {α : Type} [Context α] (a b : α) : α

Minimum of two scalar endpoints.

@[inline]

def NN.MLTheory.CROWN.BoundOps.max2 {α : Type} [Context α] (a b : α) : α

Maximum of two scalar endpoints.

Nonlinear enclosure operations

Each method consumes a closed interval [lo, hi]. A successful result is another endpoint pair; none means that this backend does not implement a finite transfer for the requested operation. Division receives both numerator and denominator intervals. The executable result alone makes no soundness claim; LawfulNonlinearBoundOps supplies that claim when a theorem needs it.

The interface is deliberately operational, like BoundOps. The proof layer establishes soundness for the concrete implementations used by checked workflows; an external instance without a lawful instance remains part of the backend trust boundary.

class NN.MLTheory.CROWN.NonlinearBoundOps (α : Type) [TorchLean.Storage α] [Context α] : Type

Interval enclosures for the nonlinear scalar operations a bound-propagation pass needs.

Each method takes the endpoints of the input interval (division takes both operands' endpoints) and returns the endpoints of an enclosure of the image, or none when the backend declines to bound that input, for example a logarithm on an interval reaching zero.

• divBounds : α → α → α → α → Option (α × α)

  Enclose x / y from the endpoints of x and then of y.

• expBounds : α → α → Option (α × α)

  Enclose exp x on [l, u].

• logBounds : α → α → Option (α × α)

  Enclose log x on [l, u].

• sqrtBounds : α → α → Option (α × α)

  Enclose sqrt x on [l, u].

• sigmoidBounds : α → α → Option (α × α)

  Enclose sigmoid x on [l, u].

• tanhBounds : α → α → Option (α × α)

  Enclose tanh x on [l, u].

• sinBounds : α → α → Option (α × α)

  Enclose sin x on [l, u].

• cosBounds : α → α → Option (α × α)

  Enclose cos x on [l, u].

• layerNormAbsBound : ℕ → Option α

  Uniform absolute bound for one last-axis layer-normalization row.

• supportsIdealCoupledDerivatives : Bool

  Whether coupled softmax/layer-normalization derivative formulas use exact scalar arithmetic.

def NN.MLTheory.CROWN.NonlinearBoundOps.min4 {α : Type} [Context α] (a b c d : α) : α

Minimum of four endpoints.

def NN.MLTheory.CROWN.NonlinearBoundOps.max4 {α : Type} [Context α] (a b c d : α) : α

Maximum of four endpoints.

def NN.MLTheory.CROWN.NonlinearBoundOps.denominatorAvoidsZero {α : Type} [Context α] (lo hi : α) : Bool

The denominator interval avoids zero.

def NN.MLTheory.CROWN.NonlinearBoundOps.softplusBounds {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (lo hi : α) : Option (α × α)

A coarse softplus enclosure that stays finite without evaluating an exponential.

For a real input, max x 0 ≤ softplus x ≤ max x 0 + 1: after the sign branch, the remaining logarithm lies between zero and log 2 < 1. Directed addition therefore gives an enclosure even when an endpoint is too large for an exponential-based transfer. The graph checker can use this range as a constant affine bound on every backend that supplies directed arithmetic.

def NN.MLTheory.CROWN.NonlinearBoundOps.safeLogBounds {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (lo hi epsilonLo epsilonHi : α) : Option (α × α)

Enclose safeLog using the complete input and epsilon intervals.

The lower endpoint of softplus(x) + epsilon must be positive. This checks the supplied epsilon, including values smaller than the context default. A backend's logarithm transfer gives the first choice of bounds. If it is unavailable, 1 - 1/z ≤ log z ≤ z - 1 supplies a coarser enclosure using directed reciprocal and subtraction. Neither route evaluates an unbounded exponential.

@[instance_reducible, instance 100]

instance NN.MLTheory.CROWN.instNonlinearBoundOpsConservative {α : Type} [TorchLean.Storage α] [Context α] : NonlinearBoundOps α

Conservative nonlinear ranges available for every scalar context.

Sigmoid, tanh, sine, and cosine have format-independent codomain bounds. Unbounded operations and layer normalization remain unavailable until a concrete backend provides directed implementations.

Host binary64 endpoints

Lean's Float operations round to nearest on the host binary64 format. For executable checking we widen every finite result by one adjacent representable value. This is deliberately an explicit instance rather than a generic fallback: its soundness depends on the host IEEE-754 arithmetic boundary documented by Lean, whereas instBoundOpsReal is exact and the ExecFloat.Binary 8 23 instance is connected to TorchLean's bit-level binary32 proofs.

def NN.MLTheory.CROWN.HostFloat.signMask : UInt64

Sign bit of a binary64 word: clearing it gives the magnitude, testing it gives the sign.

def NN.MLTheory.CROWN.HostFloat.posInfBits : UInt64

Bit pattern of +∞ in binary64. Stepping up from here has to stay put.

def NN.MLTheory.CROWN.HostFloat.negInfBits : UInt64

Bit pattern of -∞ in binary64. Stepping down from here has to stay put.

def NN.MLTheory.CROWN.HostFloat.nextUp (x : Float) : Float

Adjacent binary64 value above x, with the usual IEEE behavior at infinities and zeros.

def NN.MLTheory.CROWN.HostFloat.nextDown (x : Float) : Float

Adjacent binary64 value below x, with the usual IEEE behavior at infinities and zeros.

@[instance_reducible]

instance NN.MLTheory.CROWN.instBoundOpsFloat : BoundOps Float

Outward-widened host binary64 operations.

This instance is suitable for executable certificate replay under the trusted host-Float boundary. Use ExecFloat.Binary 8 23 when the binary32 endpoint calculation itself must be connected to Lean proofs.

@[instance_reducible]

instance NN.MLTheory.CROWN.instNonlinearBoundOpsFloat : NonlinearBoundOps Float

Nonlinear enclosures supplied by host binary64 arithmetic.

Division and square root use hardware operations widened by one adjacent binary64 value. We do not make the same claim for host transcendental-library calls, so exp and log remain unsupported.

Native binary32 endpoints

The same one-ULP widening policy is available for Lean's native Float32. The operations execute with binary32 rounding; moving to the adjacent representable value turns each nearest-rounded result into an outward endpoint.

def NN.MLTheory.CROWN.HostFloat32.signMask : UInt32

Sign bit of a binary32 word, the Float32 counterpart of HostFloat.signMask.

def NN.MLTheory.CROWN.HostFloat32.posInfBits : UInt32

Bit pattern of +∞ in binary32.

def NN.MLTheory.CROWN.HostFloat32.negInfBits : UInt32

Bit pattern of -∞ in binary32.

def NN.MLTheory.CROWN.HostFloat32.nextUp (x : Float32) : Float32

Adjacent binary32 value above x, preserving NaNs and positive infinity.

def NN.MLTheory.CROWN.HostFloat32.nextDown (x : Float32) : Float32

Adjacent binary32 value below x, preserving NaNs and negative infinity.

@[instance_reducible]

instance NN.MLTheory.CROWN.instBoundOpsFloat32 : BoundOps Float32

Outward-widened native binary32 operations.

@[instance_reducible]

instance NN.MLTheory.CROWN.instNonlinearBoundOpsFloat32 : NonlinearBoundOps Float32

Native binary32 nonlinear enclosures for division and square root.