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. IEEE32Exec), 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 [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.eval_on_box: min/max over products and accumulation use BoundOps.
  • IBP.linear: interval linear layer propagation uses BoundOps.
• NN.MLTheory.CROWN.Graph
  • box_add, box_sub, box_mul_elem: endpoint propagation uses BoundOps.

The distinction matters for executable certificate replay. 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) [Context α] : Type

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

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

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

Real-semantic enclosure laws for BoundOps.

The executable interface above is intentionally available without this class: a backend may be useful for diagnostics before its arithmetic has been connected to a proof. Sound CROWN theorems require LawfulBoundOps in addition to BoundOps. The interpretation toReal says what a scalar endpoint means mathematically, and the laws compare each directed operation with exact arithmetic on those real values. This is stronger than merely surrounding the backend's ordinary rounded operation.

There is a global instance for ℝ. There is deliberately no global instance for Lean Float or for all IEEE32Exec bit patterns. Host Float is a trusted runtime boundary, while IEEE-754 NaNs, infinities, and overflow require finite-path hypotheses; those facts are stated at the IEEE semantics layer rather than hidden in an invalid ordered-ring instance.

• toReal : α → ℝ

  Mathematical value represented by an endpoint.

• lt_iff (a b : α) : a < b ↔ toReal a < toReal b

  Executable endpoint comparisons agree with the mathematical order.

• addDown_le (a b : α) : toReal (BoundOps.addDown a b) ≤ toReal a + toReal b
• le_addUp (a b : α) : toReal a + toReal b ≤ toReal (BoundOps.addUp a b)
• subDown_le (a b : α) : toReal (BoundOps.subDown a b) ≤ toReal a - toReal b
• le_subUp (a b : α) : toReal a - toReal b ≤ toReal (BoundOps.subUp a b)
• mulDown_le (a b : α) : toReal (BoundOps.mulDown a b) ≤ toReal a * toReal b
• le_mulUp (a b : α) : toReal a * toReal b ≤ toReal (BoundOps.mulUp a b)

@[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) [Context α] : Type

• divBounds : α → α → α → α → Option (α × α)
• expBounds : α → α → Option (α × α)
• logBounds : α → α → Option (α × α)
• sqrtBounds : α → α → Option (α × α)
• sigmoidBounds : α → α → Option (α × α)
• tanhBounds : α → α → Option (α × α)
• sinBounds : α → α → Option (α × α)
• cosBounds : α → α → Option (α × α)
• 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.UnaryEnclosure {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] (f : ℝ → ℝ) (transfer : α → α → Option (α × α)) : Prop

Soundness predicate for a unary interval transfer.

Returning none is always permitted. If the transfer returns endpoints, every real input between the interpreted input endpoints must map between the interpreted output endpoints.

def NN.MLTheory.CROWN.BinaryEnclosure {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] (f : ℝ → ℝ → ℝ) (transfer : α → α → α → α → Option (α × α)) : Prop

Soundness predicate for a binary interval transfer.

class NN.MLTheory.CROWN.LawfulNonlinearBoundOps (α : Type) [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] : Prop

Real-semantic enclosure laws for NonlinearBoundOps.

This class is deliberately separate from the executable transfer table. A backend may implement a transfer for testing before proving it; sound verification entrypoints can require this class and therefore cannot silently promote an unchecked implementation into a theorem.

• divBounds_enclosure : BinaryEnclosure (fun (x1 x2 : ℝ) => x1 / x2) NonlinearBoundOps.divBounds
• expBounds_enclosure : UnaryEnclosure Real.exp NonlinearBoundOps.expBounds
• logBounds_enclosure : UnaryEnclosure Real.log NonlinearBoundOps.logBounds
• sqrtBounds_enclosure : UnaryEnclosure Real.sqrt NonlinearBoundOps.sqrtBounds
• sigmoidBounds_enclosure : UnaryEnclosure (fun (x : ℝ) => 1 / (1 + Real.exp (-x))) NonlinearBoundOps.sigmoidBounds
• tanhBounds_enclosure : UnaryEnclosure Real.tanh NonlinearBoundOps.tanhBounds
• sinBounds_enclosure : UnaryEnclosure Real.sin NonlinearBoundOps.sinBounds
• cosBounds_enclosure : UnaryEnclosure Real.cos NonlinearBoundOps.cosBounds
• layerNormAbsBound_sound {n : ℕ} {radius : α} : NonlinearBoundOps.layerNormAbsBound n = some radius → √↑n ≤ LawfulBoundOps.toReal radius
• coupledDerivatives_exact : NonlinearBoundOps.supportsIdealCoupledDerivatives α = true → BoundOps.supportsExactAffineReassociation α = true

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.

@[implicit_reducible, instance 100]

instance NN.MLTheory.CROWN.instNonlinearBoundOpsConservative {α : Type} [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.

Exact real arithmetic needs no rounding, so its lower and upper operations coincide.

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.instBoundOpsReal : BoundOps ℝ

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.instLawfulBoundOpsReal : LawfulBoundOps ℝ

Exact real endpoint arithmetic satisfies the directed-operation enclosure laws.

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.instNonlinearBoundOpsReal : NonlinearBoundOps ℝ

Exact nonlinear interval transfers over the real numbers.

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 IEEE32Exec instance is connected to TorchLean's bit-level binary32 proofs.

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

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

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

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.

@[implicit_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 IEEE32Exec when the binary32 endpoint calculation itself must be connected to Lean proofs.

@[implicit_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.