FA-17091 / Floating-point arithmetic / Open access

Opposite-sign midpoint overflows its endpoint difference · case 01

Opposite-sign midpoint overflows its endpoint difference.

Verified by executionVariant 1 · 9 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

Opposite-sign midpoint overflows its endpoint difference. The faulty expression is midpoint=a+(b-a)/2.

VERIFIED REPAIR

Apply the contract at this fault site using midpoint=a/2+b/2.

Unsuccessful approach: The attempted local correction midpoint=a+min(b-a,1e308)/2 still violates the explicit regression fixtures.

Case contract

Finite ordered binary64 midpoint rendered as hex. Opposite-sign endpoints use half-sums to avoid difference overflow; same-sign endpoints use a difference to preserve subnormal increments. Exact equal endpoints preserve their bits.

Why this case matters

An offline floating representation model isolates a reproducible arithmetic fault.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(a,b):
    if a>b: return 'invalid'
    if a==b: return a.hex()
    if a<0<b:
        midpoint=a+(b-a)/2
    else:
        midpoint=a+(b-a)/2
    return midpoint.hex()
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('opposite huge', solve(-1e308,1e308), 0.0.hex())
check('positive huge', solve(1e308,1.5e308), (1.25e308).hex())
check('negative huge', solve(-1.5e308,-1e308), (-1.25e308).hex())
check('subnormal midpoint', solve(math.ldexp(1.0,-1074),math.ldexp(5.0,-1074)), math.ldexp(3.0,-1074).hex())
check('subnormal same', solve(math.ldexp(1.0,-1074),math.ldexp(3.0,-1074)), math.ldexp(2.0,-1074).hex())
check('negative subnormal', solve(-math.ldexp(3.0,-1074),-math.ldexp(1.0,-1074)), (-math.ldexp(2.0,-1074)).hex())
check('negative zero equal', solve(-0.0,-0.0), (-0.0).hex())
check('ordinary', solve(float(N),float(N+8)), float(N+4).hex())
check('reverse', solve(float(N+1),float(N)), "invalid")
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
opposite huge	`inf`	`0x0.0p+0`	Failed
positive huge	`0x1.640306766bac8p+1023`	`0x1.640306766bac8p+1023`	Passed
negative huge	`-0x1.640306766bac8p+1023`	`-0x1.640306766bac8p+1023`	Passed
subnormal midpoint	`0x0.0000000000003p-1022`	`0x0.0000000000003p-1022`	Passed
subnormal same	`0x0.0000000000002p-1022`	`0x0.0000000000002p-1022`	Passed
negative subnormal	`-0x0.0000000000002p-1022`	`-0x0.0000000000002p-1022`	Passed
negative zero equal	`-0x0.0p+0`	`-0x0.0p+0`	Passed
ordinary	`0x1.4000000000000p+2`	`0x1.4000000000000p+2`	Passed
reverse	`invalid`	`invalid`	Passed

SHA-256 / d7d1c49bacbb2877fbbc15abd4e2bbad25ba526f84b86ea210f953911625d47c

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(a,b):
    if a>b: return 'invalid'
    if a==b: return a.hex()
    if a<0<b:
        midpoint=a+min(b-a,1e308)/2
    else:
        midpoint=a+(b-a)/2
    return midpoint.hex()
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('opposite huge', solve(-1e308,1e308), 0.0.hex())
check('positive huge', solve(1e308,1.5e308), (1.25e308).hex())
check('negative huge', solve(-1.5e308,-1e308), (-1.25e308).hex())
check('subnormal midpoint', solve(math.ldexp(1.0,-1074),math.ldexp(5.0,-1074)), math.ldexp(3.0,-1074).hex())
check('subnormal same', solve(math.ldexp(1.0,-1074),math.ldexp(3.0,-1074)), math.ldexp(2.0,-1074).hex())
check('negative subnormal', solve(-math.ldexp(3.0,-1074),-math.ldexp(1.0,-1074)), (-math.ldexp(2.0,-1074)).hex())
check('negative zero equal', solve(-0.0,-0.0), (-0.0).hex())
check('ordinary', solve(float(N),float(N+8)), float(N+4).hex())
check('reverse', solve(float(N+1),float(N)), "invalid")
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
opposite huge	`-0x1.1ccf385ebc8a0p+1022`	`0x0.0p+0`	Failed
positive huge	`0x1.640306766bac8p+1023`	`0x1.640306766bac8p+1023`	Passed
negative huge	`-0x1.640306766bac8p+1023`	`-0x1.640306766bac8p+1023`	Passed
subnormal midpoint	`0x0.0000000000003p-1022`	`0x0.0000000000003p-1022`	Passed
subnormal same	`0x0.0000000000002p-1022`	`0x0.0000000000002p-1022`	Passed
negative subnormal	`-0x0.0000000000002p-1022`	`-0x0.0000000000002p-1022`	Passed
negative zero equal	`-0x0.0p+0`	`-0x0.0p+0`	Passed
ordinary	`0x1.4000000000000p+2`	`0x1.4000000000000p+2`	Passed
reverse	`invalid`	`invalid`	Passed

SHA-256 / 4af7527e992b0903b8e555b9d50f51e384e010e44e4fc8aa8155d4db8262edab

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(a,b):
    if a>b: return 'invalid'
    if a==b: return a.hex()
    if a<0<b:
        midpoint=a/2+b/2
    else:
        midpoint=a+(b-a)/2
    return midpoint.hex()
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('opposite huge', solve(-1e308,1e308), 0.0.hex())
check('positive huge', solve(1e308,1.5e308), (1.25e308).hex())
check('negative huge', solve(-1.5e308,-1e308), (-1.25e308).hex())
check('subnormal midpoint', solve(math.ldexp(1.0,-1074),math.ldexp(5.0,-1074)), math.ldexp(3.0,-1074).hex())
check('subnormal same', solve(math.ldexp(1.0,-1074),math.ldexp(3.0,-1074)), math.ldexp(2.0,-1074).hex())
check('negative subnormal', solve(-math.ldexp(3.0,-1074),-math.ldexp(1.0,-1074)), (-math.ldexp(2.0,-1074)).hex())
check('negative zero equal', solve(-0.0,-0.0), (-0.0).hex())
check('ordinary', solve(float(N),float(N+8)), float(N+4).hex())
check('reverse', solve(float(N+1),float(N)), "invalid")
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
opposite huge	`0x0.0p+0`	`0x0.0p+0`	Passed
positive huge	`0x1.640306766bac8p+1023`	`0x1.640306766bac8p+1023`	Passed
negative huge	`-0x1.640306766bac8p+1023`	`-0x1.640306766bac8p+1023`	Passed
subnormal midpoint	`0x0.0000000000003p-1022`	`0x0.0000000000003p-1022`	Passed
subnormal same	`0x0.0000000000002p-1022`	`0x0.0000000000002p-1022`	Passed
negative subnormal	`-0x0.0000000000002p-1022`	`-0x0.0000000000002p-1022`	Passed
negative zero equal	`-0x0.0p+0`	`-0x0.0p+0`	Passed
ordinary	`0x1.4000000000000p+2`	`0x1.4000000000000p+2`	Passed
reverse	`invalid`	`invalid`	Passed

SHA-256 / 0012a90273b46b3f5e0d0c84c54b3347f32324dff9ac8f78b39bd3527c153291

Verification & scope

Controlled binary64 or explicitly stipulated miniature format; no hardware exception flags or platform floating environment are modeled. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:39:42.988400+00:00.

Case digest / ded74c6abc17bf3e487e4f43f8a307834973dac2d245912589a4af0fe9afbed1