FA-15896 / Floating-point arithmetic / Open access
An equal-value early return preserves the wrong zero sign · case 01
An equal-value early return preserves the wrong zero sign.
ROOT CAUSE
An equal-value early return preserves the wrong zero sign. The faulty expression is return xb.
VERIFIED REPAIR
Apply the contract at this fault site using return yb.
Unsuccessful approach: The attempted local correction return 0 if x == 0 else xb still violates the explicit regression fixtures.
Case contract
Return the binary64 bit pattern one representable step from x toward y, or canonical quiet NaN for NaN operands. Equal operands return the exact bits of y, including zero sign.
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(xb, yb):
x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]
y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]
if math.isnan(x) or math.isnan(y):
return 0x7ff8000000000000
if x == y:
return xb
if x == 0:
return (yb & (1<<63)) | 1
if x > 0:
return xb+1 if y>x else xb-1
return xb-1 if y>x else xb+1
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)
check('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)
check('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)
check('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)
check('negative zero equality', solve(0, 1<<63), 1<<63)
check('positive zero equality', solve(1<<63, 0), 0)
check('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)
check('zero positive', solve(1<<63, 0x3ff0000000000000), 1)
check('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)
check('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)
check('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)
check('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)
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 |
|---|---|---|---|
| positive step | 4607182418800017409 | 4607182418800017409 | Passed |
| positive reverse | 4607182418800017407 | 4607182418800017407 | Passed |
| negative forward | 13830554455654793215 | 13830554455654793215 | Passed |
| negative away | 13830554455654793217 | 13830554455654793217 | Passed |
| negative zero equality | 0 | 9223372036854775808 | Failed |
| positive zero equality | 9223372036854775808 | 0 | Failed |
| zero negative | 9223372036854775809 | 9223372036854775809 | Passed |
| zero positive | 1 | 1 | Passed |
| nan target | 9221120237041090560 | 9221120237041090560 | Passed |
| nan source | 9221120237041090560 | 9221120237041090560 | Passed |
| finite step varies | 4611686018427387903 | 4611686018427387903 | Passed |
| infinity inward | 9218868437227405311 | 9218868437227405311 | Passed |
SHA-256 / a72a44b5f86cf31ebc300dc3f77a37c536af1503439fd98c442b872b0cfecc64
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(xb, yb):
x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]
y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]
if math.isnan(x) or math.isnan(y):
return 0x7ff8000000000000
if x == y:
return 0 if x == 0 else xb
if x == 0:
return (yb & (1<<63)) | 1
if x > 0:
return xb+1 if y>x else xb-1
return xb-1 if y>x else xb+1
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)
check('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)
check('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)
check('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)
check('negative zero equality', solve(0, 1<<63), 1<<63)
check('positive zero equality', solve(1<<63, 0), 0)
check('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)
check('zero positive', solve(1<<63, 0x3ff0000000000000), 1)
check('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)
check('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)
check('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)
check('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)
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 |
|---|---|---|---|
| positive step | 4607182418800017409 | 4607182418800017409 | Passed |
| positive reverse | 4607182418800017407 | 4607182418800017407 | Passed |
| negative forward | 13830554455654793215 | 13830554455654793215 | Passed |
| negative away | 13830554455654793217 | 13830554455654793217 | Passed |
| negative zero equality | 0 | 9223372036854775808 | Failed |
| positive zero equality | 0 | 0 | Passed |
| zero negative | 9223372036854775809 | 9223372036854775809 | Passed |
| zero positive | 1 | 1 | Passed |
| nan target | 9221120237041090560 | 9221120237041090560 | Passed |
| nan source | 9221120237041090560 | 9221120237041090560 | Passed |
| finite step varies | 4611686018427387903 | 4611686018427387903 | Passed |
| infinity inward | 9218868437227405311 | 9218868437227405311 | Passed |
SHA-256 / de4db382b395c05e2f06a2f94db35d3e8580f279eb941b5a2d86068a1ff7b8e0
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(xb, yb):
x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]
y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]
if math.isnan(x) or math.isnan(y):
return 0x7ff8000000000000
if x == y:
return yb
if x == 0:
return (yb & (1<<63)) | 1
if x > 0:
return xb+1 if y>x else xb-1
return xb-1 if y>x else xb+1
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)
check('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)
check('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)
check('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)
check('negative zero equality', solve(0, 1<<63), 1<<63)
check('positive zero equality', solve(1<<63, 0), 0)
check('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)
check('zero positive', solve(1<<63, 0x3ff0000000000000), 1)
check('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)
check('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)
check('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)
check('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)
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 |
|---|---|---|---|
| positive step | 4607182418800017409 | 4607182418800017409 | Passed |
| positive reverse | 4607182418800017407 | 4607182418800017407 | Passed |
| negative forward | 13830554455654793215 | 13830554455654793215 | Passed |
| negative away | 13830554455654793217 | 13830554455654793217 | Passed |
| negative zero equality | 9223372036854775808 | 9223372036854775808 | Passed |
| positive zero equality | 0 | 0 | Passed |
| zero negative | 9223372036854775809 | 9223372036854775809 | Passed |
| zero positive | 1 | 1 | Passed |
| nan target | 9221120237041090560 | 9221120237041090560 | Passed |
| nan source | 9221120237041090560 | 9221120237041090560 | Passed |
| finite step varies | 4611686018427387903 | 4611686018427387903 | Passed |
| infinity inward | 9218868437227405311 | 9218868437227405311 | Passed |
SHA-256 / c9950755b0dc041dffe873301bca78d9e7b725e9a4889164fce6ad10d526d497
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:31.413415+00:00.
Case digest / 46d0278d00a7374ae43d70b2c6a8d78ba40ab81dc77788d105eba3eb612d4c48