FP32 CROWN/IBP Integration

The CROWN/IBP development (NN/MLTheory/CROWN/*) proves real-valued enclosure theorems of the form “the network output lies in this box”.

This module combines those real enclosures with float32 forward-error bounds (expressed using approxT) to obtain a float32-sound enclosure: we inflate the real box by the explicit forward error budget.

This is the key separation of concerns:

• CROWN/IBP proves a real-valued semantic enclosure.
• RuntimeApprox/FP32 proves the rounded runtime output is close to that real-valued output.
• This file composes the two by uniformly widening the box.

Scalar Margin Lemmas

theorem NN.Proofs.RuntimeApprox.FP32.interval_contains_inflate_of_abs_error {l u y : ℝ} {yR : R} {eps : ℝ} (hy : l ≤ y ∧ y ≤ u) (happrox : |toSpec yR - y| ≤ eps) : l - eps ≤ toSpec yR ∧ toSpec yR ≤ u + eps

If a real value y lies in [l, u] and a runtime value yR is within eps of y, then the interpreted runtime value lies in the widened interval [l - eps, u + eps].

This is the scalar heart of the FP32/CROWN bridge.

theorem NN.Proofs.RuntimeApprox.FP32.fp32_le_of_real_le_sub_margin {y t : ℝ} {yR : R} {eps : ℝ} (h : y ≤ t - eps) (happrox : |toSpec yR - y| ≤ eps) : toSpec yR ≤ t

One-sided upper-margin rule.

If the real value is at least eps below threshold t, then any FP32 value within eps is still below t.

theorem NN.Proofs.RuntimeApprox.FP32.fp32_ge_of_real_ge_add_margin {y t : ℝ} {yR : R} {eps : ℝ} (h : y ≥ t + eps) (happrox : |toSpec yR - y| ≤ eps) : toSpec yR ≥ t

One-sided lower-margin rule.

If the real value is at least eps above threshold t, then any FP32 value within eps is still above t.

Inflating Real Boxes To Cover FP32 Execution

noncomputable def NN.Proofs.RuntimeApprox.FP32.inflateBoxUniform {s : Spec.Shape} (B : MLTheory.CROWN.Box ℝ s) (eps : ℝ) : MLTheory.CROWN.Box ℝ s

Uniformly widen a real-valued CROWN.Box by eps in every component.

The lower face moves down by eps; the upper face moves up by eps. This is intentionally simple and conservative, matching an L∞-style output error bound.

theorem NN.Proofs.RuntimeApprox.FP32.box_contains_inflateUniform_of_approx {s : Spec.Shape} {B : MLTheory.CROWN.Box ℝ s} {yS : Spec.Tensor ℝ s} {yR : Spec.Tensor R s} {eps : ℝ} (hy : B.contains yS) (happrox : Proofs.RuntimeApprox.approxT toSpec yS yR eps) : (inflateBoxUniform B eps).contains (Proofs.RuntimeApprox.tensorToSpec toSpec yR)

Tensor version of interval_contains_inflate_of_abs_error.

If the real-spec output yS is inside a real CROWN/IBP box B, and the FP32 runtime output yR approximates yS within uniform eps, then the interpreted FP32 output is inside the uniformly widened box.

theorem NN.Proofs.RuntimeApprox.FP32.ibpBound_contains_reluMlp2_fp32 {inDim hidDim outDim : ℕ} (netS : MLTheory.CROWN.MLP2 ℝ inDim hidDim outDim) (netR : MLTheory.CROWN.MLP2 R inDim hidDim outDim) (xB : MLTheory.CROWN.Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (xS : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (xR : Spec.Tensor R (Spec.Shape.dim inDim Spec.Shape.scalar)) {eW1 eb1 eW2 eb2 ex : ℝ} (hW1 : Proofs.RuntimeApprox.approxT toSpec netS.W1 netR.W1 eW1) (hb1 : Proofs.RuntimeApprox.approxT toSpec netS.b1 netR.b1 eb1) (hW2 : Proofs.RuntimeApprox.approxT toSpec netS.W2 netR.W2 eW2) (hb2 : Proofs.RuntimeApprox.approxT toSpec netS.b2 netR.b2 eb2) (hx : Proofs.RuntimeApprox.approxT toSpec xS xR ex) (hxB : xB.contains xS) : ∃ (epsOut : ℝ), (inflateBoxUniform (MLTheory.CROWN.boundIbp netS xB) epsOut).contains (Proofs.RuntimeApprox.tensorToSpec toSpec (have l1R := { weights := netR.W1, bias := netR.b1 }; have l2R := { weights := netR.W2, bias := netR.b2 }; have z1R := Spec.linearSpec l1R xR; have a1R := Spec.Tensor.mapSpec Proofs.RuntimeApprox.NFBackend.reluR z1R; Spec.linearSpec l2R a1R))

Float32-sound IBP for a 2-layer ReLU MLP, via uniform output-box inflation:

1. Use the real-spec IBP theorem NN.MLTheory.CROWN.Theorems.bound_ibp_sound.
2. Use approxT to bound FP32 forward error (approxT_reluMlp2_fp32).
3. Inflate the real IBP box by that error bound.

The result is a real-valued interval that is guaranteed to contain the FP32 execution result.