af_range: the absorption is formed term by term so |x0| + e never overflows before it is scaled; AffineTests pin af_from_iv tight near the float maximum

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
This commit is contained in:
Meta Vens 2026-10-04 03:18:44 +02:00
commit 27109f1b2a
2 changed files with 14 additions and 4 deletions

View file

@ -49,8 +49,9 @@ public static partial class math
/// overflow in them. Rounding: x0 and e each round once, and a value of the interval is within e of x0
/// only up to those; S = |x0| + e. Halving a subnormal endpoint loses at most 2^-150, and the sum and
/// difference of subnormals are exact, so 2^-126 covers the underflow (the e of an interval spanning
/// one subnormal step would otherwise round to 0). If e + its absorption exceeds the float maximum
/// it is infinity, which still encloses.
/// one subnormal step would otherwise round to 0). |x0| + e is at most the larger endpoint
/// in magnitude, so it does not overflow. If e + its absorption exceeds the float maximum it is
/// infinity, which still encloses.
/// </summary>
public static float3 af_from_iv(float2 interval)
{
@ -62,14 +63,15 @@ public static partial class math
/// <summary>
/// The interval of every value of the form over every eps: x0 -+ (|a| + e), the bridge to iv_*. The
/// endpoints round inward by at most u (|x0| + |a| + e) each, so each is moved outward by
/// (|x0| + |a| + e) 2^-20. A form with an infinite component (an overflowed op) gives infinite
/// (|x0| + |a| + e) 2^-20, formed term by term so that the sum never passes the float maximum before it
/// is scaled. A form with an infinite component (an overflowed op) gives infinite
/// endpoints, and an endpoint that would be NaN (infinity minus infinity, or a NaN component) is
/// the infinity on its side, so the result is never NaN and still encloses.
/// </summary>
public static float2 af_range(float3 x)
{
var r = abs(x.y) + x.z;
var w = (abs(x.x) + r) * 9.5367431640625e-7f;
var w = abs(x.x) * 9.5367431640625e-7f + r * 9.5367431640625e-7f;
var lo = x.x - r - w;
var hi = x.x + r + w;
return new float2(lo == lo ? lo : float.NegativeInfinity, hi == hi ? hi : float.PositiveInfinity);

View file

@ -582,6 +582,14 @@ public sealed class AffineTests
if (!(range.x <= value && value <= range.y))
misses.Add($"af_range(af_from_iv([{lo:R}, {hi:R}])) = {range} misses {value:R}");
}
// Tight where the answer is representable: an endpoint is no farther than 2^-18 (|lo| + |hi|)
// from the interval's, unless that bound passes the float maximum, where infinity is the answer.
var slack = Math.ScaleB(Math.Abs((double)lo) + Math.Abs((double)hi), -18) + 1.0e-37;
if ((double)lo - slack > -(double)max && range.x < (double)lo - slack)
misses.Add($"af_range(af_from_iv([{lo:R}, {hi:R}])).x = {range.x:R}, more than 2^-18 (|lo| + |hi|) under lo");
if ((double)hi + slack < (double)max && range.y > (double)hi + slack)
misses.Add($"af_range(af_from_iv([{lo:R}, {hi:R}])).y = {range.y:R}, more than 2^-18 (|lo| + |hi|) over hi");
}
foreach (var a in specials)