FP32

FP32-specialized entrypoints for the CROWN/LiRPA graph engine.

This is not an executable backend (it is noncomputable in general, because FP32 is modeled on ℝ). It exists so proofs can state “sound w.r.t. float32 semantics” without mentioning Lean’s builtin Float.

This module is an optional convenience layer and lives under NN/MLTheory/CROWN/Extras/.

FP32 entrypoints

@[reducible, inline]

abbrev NN.MLTheory.CROWN.FP32 : Type

FP32 scalar type used for FP32-specialized CROWN/LiRPA statements.

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instBoundOps : BoundOps FP32

Directed endpoint arithmetic for the rounded-real FP32 model.

Each operation is performed on the underlying real values and rounded directly toward the appropriate side of the binary32 grid. The enclosure laws are TorchLean.Floats.Interval.roundDown_le and TorchLean.Floats.Interval.le_roundUp.

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instLawfulBoundOps : LawfulBoundOps FP32

The proof-oriented FP32 endpoint operations enclose exact real arithmetic.

This follows directly from the format-generic floor and ceiling rounding theorems. It is the law dictionary used by sound rounded CROWN statements over FP32.

noncomputable def NN.MLTheory.CROWN.FP32.roundDownEndpoint (x : ℝ) : FP32

Embed a real endpoint after rounding it downward to the binary32 grid.

noncomputable def NN.MLTheory.CROWN.FP32.roundUpEndpoint (x : ℝ) : FP32

Embed a real endpoint after rounding it upward to the binary32 grid.

@[implicit_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instNonlinearBoundOps : NonlinearBoundOps FP32

Exact-real nonlinear operations rounded outward to the binary32 grid.

theorem NN.MLTheory.CROWN.FP32.roundDownEndpoint_le (x : ℝ) : (roundDownEndpoint x).val ≤ x

Downward-rounded proof endpoints do not exceed their exact real inputs.

theorem NN.MLTheory.CROWN.FP32.le_roundUpEndpoint (x : ℝ) : x ≤ (roundUpEndpoint x).val

Upward-rounded proof endpoints do not fall below their exact real inputs.

instance NN.MLTheory.CROWN.FP32.instLawfulNonlinearBoundOps : LawfulNonlinearBoundOps FP32

The rounded-real FP32 nonlinear transfers enclose their exact real meanings.

noncomputable def NN.MLTheory.CROWN.FP32.runIBP (g : Graph) (ps : Graph.ParamStore FP32) : Array (Option (FlatBox FP32))

Run IBP over FP32 graph semantics.

noncomputable def NN.MLTheory.CROWN.FP32.runFirstDerivative1D (g : Graph) (ps : Graph.ParamStore FP32) (ibp : Array (Option (FlatBox FP32))) : Array (Option (FlatBox FP32))

Run the one-dimensional derivative IBP pass over FP32 graph semantics.

noncomputable def NN.MLTheory.CROWN.FP32.runDirectionalDerivative (g : Graph) (ps : Graph.ParamStore FP32) (ibp : Array (Option (FlatBox FP32))) (seed : FlatBox FP32) : Array (Option (FlatBox FP32))

Run a first-derivative pass from an arbitrary interval-valued direction.

noncomputable def NN.MLTheory.CROWN.FP32.runMixedSecondDerivative (g : Graph) (ps : Graph.ParamStore FP32) (ibp dLeft dRight : Array (Option (FlatBox FP32))) : Array (Option (FlatBox FP32))

Run the mixed second-derivative pass D²f[u, v] over FP32 graph semantics.

noncomputable def NN.MLTheory.CROWN.FP32.runSecondDerivative1D (g : Graph) (ps : Graph.ParamStore FP32) (ibp d1 : Array (Option (FlatBox FP32))) : Array (Option (FlatBox FP32))

Run the second-derivative IBP pass over FP32 graph semantics.

noncomputable def NN.MLTheory.CROWN.FP32.runAffine (g : Graph) (ps : Graph.ParamStore FP32) (ctx : Graph.AffineCtx) (ibp : Array (Option (FlatBox FP32))) : Array (Option (Graph.FlatAffine FP32))

Run the forward affine CROWN pass over FP32 graph semantics.

noncomputable def NN.MLTheory.CROWN.FP32.runCROWN (g : Graph) (ps : Graph.ParamStore FP32) (ctx : Graph.AffineCtx) (ibp : Array (Option (FlatBox FP32))) : Array (Option (Graph.FlatAffineBounds FP32))

Run the forward CROWN lower/upper affine-bounds pass over FP32 graph semantics.