`BoundOps` instance for `ExecFloat.Binary 8 23` #

This instance plugs FloatLib's configured binary32 directed-rounding primitives into the IBP/CROWN endpoint propagation code.

With this, IBP code written in terms of BoundOps can use α := ExecFloat.Binary 8 23 to get float32-grid, outward-rounded interval propagation (subject to the usual finiteness preconditions).

source

@[instance_reducible]

instance NN.MLTheory.CROWN.instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode :

BoundOps (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_1 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_2 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_3 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_4)

BoundOps for ExecFloat.Binary 8 23, using the executable directed-rounding endpoint primitives.

source

def NN.MLTheory.CROWN.IEEE32ExecBounds.unaryBounds? (f : FloatLib.Numerics.Interval ℚ → Option (FloatLib.Numerics.Interval ℚ)) (lo hi : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_1 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_2 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_3 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_4) :

Decode a finite ordered interval, compute a rational enclosure of its entire real image, and round the enclosure outward. Exceptional inputs and nonfinite rounded endpoints return none.

Instances For

source

def NN.MLTheory.CROWN.IEEE32ExecBounds.expRationalBounds? (I : FloatLib.Numerics.Interval ℚ) :

Option (FloatLib.Numerics.Interval ℚ)

Keep exponential argument reduction bounded on ordered input intervals. An upper endpoint above 128 already makes a finite binary32 enclosure impossible, so return none. For inputs below -128, use zero as a lower bound and the enclosure of exp (-128) as an upper bound. Intervals crossing -128 retain the exponential upper bound at their original upper endpoint.

The clamp avoids repeatedly squaring enormous exact rationals for extreme finite inputs.

Instances For

source

def NN.MLTheory.CROWN.IEEE32ExecBounds.sqrtRationalBounds? (I : FloatLib.Numerics.Interval ℚ) :

Option (FloatLib.Numerics.Interval ℚ)

Preserve the nonnegative part of intervals crossing zero. The dyadic grid has enough precision to resolve binary32 square roots even at the smallest positive input.

Instances For

source

@[instance_reducible]

instance NN.MLTheory.CROWN.instNonlinearBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode :

NonlinearBoundOps (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_1 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_2 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_3 instBoundOpsBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_4)

Nonlinear enclosures computed by FloatLib's whole-interval rational kernels and checked directed binary32 rounding. Successful results have finite endpoints. Reversed intervals, NaN, infinity, division through zero, invalid logarithm/square-root domains, and overflow return none.

The containment theorems below interpret endpoints by exact finite decoding. They do not assert a global lawful arithmetic instance for the IEEE carrier, which also contains exceptional values.

source