{"abstract":"Stepping checks only destination NaNs.","category":"Floating-point arithmetic","checks":12,"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.","evaluation_group":"s3-float-next-toward","failed_approach":"The attempted local correction math.isnan(x) and math.isnan(y) still violates the explicit regression fixtures.","family":"s3-floating_point_arithmetic-next-toward-source-nan","id":"FA-15886","implementations":{"attempt":{"sha256":"393e158e194c11a3c5c44688b23407fd0a7ddfef56c4f6f80ea32e991f58699c","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(xb, yb):\n    x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]\n    y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]\n    if math.isnan(x) and math.isnan(y):\n        return 0x7ff8000000000000\n    if x == y:\n        return yb\n    if x == 0:\n        return (yb & (1<<63)) | 1\n    if x > 0:\n        return xb+1 if y>x else xb-1\n    return xb-1 if y>x else xb+1\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)\ncheck('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)\ncheck('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)\ncheck('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)\ncheck('negative zero equality', solve(0, 1<<63), 1<<63)\ncheck('positive zero equality', solve(1<<63, 0), 0)\ncheck('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)\ncheck('zero positive', solve(1<<63, 0x3ff0000000000000), 1)\ncheck('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)\ncheck('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)\ncheck('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)\ncheck('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"4d822f07c0feb560b2ec9a8ea4f74035fea841fcf91c51365db404e00d7bdb5a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(xb, yb):\n    x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]\n    y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]\n    if math.isnan(y):\n        return 0x7ff8000000000000\n    if x == y:\n        return yb\n    if x == 0:\n        return (yb & (1<<63)) | 1\n    if x > 0:\n        return xb+1 if y>x else xb-1\n    return xb-1 if y>x else xb+1\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)\ncheck('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)\ncheck('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)\ncheck('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)\ncheck('negative zero equality', solve(0, 1<<63), 1<<63)\ncheck('positive zero equality', solve(1<<63, 0), 0)\ncheck('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)\ncheck('zero positive', solve(1<<63, 0x3ff0000000000000), 1)\ncheck('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)\ncheck('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)\ncheck('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)\ncheck('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"c9950755b0dc041dffe873301bca78d9e7b725e9a4889164fce6ad10d526d497","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(xb, yb):\n    x=struct.unpack('>d', xb.to_bytes(8,'big'))[0]\n    y=struct.unpack('>d', yb.to_bytes(8,'big'))[0]\n    if math.isnan(x) or math.isnan(y):\n        return 0x7ff8000000000000\n    if x == y:\n        return yb\n    if x == 0:\n        return (yb & (1<<63)) | 1\n    if x > 0:\n        return xb+1 if y>x else xb-1\n    return xb-1 if y>x else xb+1\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('positive step', solve(0x3ff0000000000000, 0x4000000000000000), 0x3ff0000000000001)\ncheck('positive reverse', solve(0x3ff0000000000000, 0), 0x3fefffffffffffff)\ncheck('negative forward', solve(0xbff0000000000000, 0), 0xbfefffffffffffff)\ncheck('negative away', solve(0xbff0000000000000, 0xc000000000000000), 0xbff0000000000001)\ncheck('negative zero equality', solve(0, 1<<63), 1<<63)\ncheck('positive zero equality', solve(1<<63, 0), 0)\ncheck('zero negative', solve(0, 0xbff0000000000000), (1<<63)|1)\ncheck('zero positive', solve(1<<63, 0x3ff0000000000000), 1)\ncheck('nan target', solve(0x3ff0000000000000, (0x7ff<<52)|N), 0x7ff8000000000000)\ncheck('nan source', solve((0x7ff<<52)|N, 0), 0x7ff8000000000000)\ncheck('finite step varies', solve((1023+N)<<52, 0), ((1023+N)<<52)-1)\ncheck('infinity inward', solve(0x7ff0000000000000, 0), 0x7fefffffffffffff)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-floating_point_arithmetic-next-toward-source-nan","generated_at":"2026-09-29T14:39:31.159582+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"An offline floating representation model isolates a reproducible arithmetic fault.","repair":"Apply the contract at this fault site using math.isnan(x) or math.isnan(y).","root_cause":"Stepping checks only destination NaNs. The faulty expression is math.isnan(y).","sha256":"04f59126df637f0bb1e0e549777e3e2f6f3f23e6c7de8e3a53c71494e0ecaf61","title":"Stepping checks only destination NaNs · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":39.294,"exit_code":1,"observations":[{"actual":4607182418800017409,"check":"positive step","expected":4607182418800017409,"passed":true},{"actual":4607182418800017407,"check":"positive reverse","expected":4607182418800017407,"passed":true},{"actual":13830554455654793215,"check":"negative forward","expected":13830554455654793215,"passed":true},{"actual":13830554455654793217,"check":"negative away","expected":13830554455654793217,"passed":true},{"actual":9223372036854775808,"check":"negative zero equality","expected":9223372036854775808,"passed":true},{"actual":0,"check":"positive zero equality","expected":0,"passed":true},{"actual":9223372036854775809,"check":"zero negative","expected":9223372036854775809,"passed":true},{"actual":1,"check":"zero positive","expected":1,"passed":true},{"actual":4607182418800017407,"check":"nan target","expected":9221120237041090560,"passed":false},{"actual":9218868437227405314,"check":"nan source","expected":9221120237041090560,"passed":false},{"actual":4611686018427387903,"check":"finite step varies","expected":4611686018427387903,"passed":true},{"actual":9218868437227405311,"check":"infinity inward","expected":9218868437227405311,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"positive step\", \"actual\": 4607182418800017409, \"expected\": 4607182418800017409, \"passed\": true}, {\"check\": \"positive reverse\", \"actual\": 4607182418800017407, \"expected\": 4607182418800017407, \"passed\": true}, {\"check\": \"negative forward\", \"actual\": 13830554455654793215, \"expected\": 13830554455654793215, \"passed\": true}, {\"check\": \"negative away\", \"actual\": 13830554455654793217, \"expected\": 13830554455654793217, \"passed\": true}, {\"check\": \"negative zero equality\", \"actual\": 9223372036854775808, \"expected\": 9223372036854775808, \"passed\": true}, {\"check\": \"positive zero equality\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"zero negative\", \"actual\": 9223372036854775809, \"expected\": 9223372036854775809, \"passed\": true}, {\"check\": \"zero positive\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"nan target\", \"actual\": 4607182418800017407, \"expected\": 9221120237041090560, \"passed\": false}, {\"check\": \"nan source\", \"actual\": 9218868437227405314, \"expected\": 9221120237041090560, \"passed\": false}, {\"check\": \"finite step varies\", \"actual\": 4611686018427387903, \"expected\": 4611686018427387903, \"passed\": true}, {\"check\": \"infinity inward\", \"actual\": 9218868437227405311, \"expected\": 9218868437227405311, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.05,"exit_code":1,"observations":[{"actual":4607182418800017409,"check":"positive step","expected":4607182418800017409,"passed":true},{"actual":4607182418800017407,"check":"positive reverse","expected":4607182418800017407,"passed":true},{"actual":13830554455654793215,"check":"negative forward","expected":13830554455654793215,"passed":true},{"actual":13830554455654793217,"check":"negative away","expected":13830554455654793217,"passed":true},{"actual":9223372036854775808,"check":"negative zero equality","expected":9223372036854775808,"passed":true},{"actual":0,"check":"positive zero equality","expected":0,"passed":true},{"actual":9223372036854775809,"check":"zero negative","expected":9223372036854775809,"passed":true},{"actual":1,"check":"zero positive","expected":1,"passed":true},{"actual":9221120237041090560,"check":"nan target","expected":9221120237041090560,"passed":true},{"actual":9218868437227405314,"check":"nan source","expected":9221120237041090560,"passed":false},{"actual":4611686018427387903,"check":"finite step varies","expected":4611686018427387903,"passed":true},{"actual":9218868437227405311,"check":"infinity inward","expected":9218868437227405311,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"positive step\", \"actual\": 4607182418800017409, \"expected\": 4607182418800017409, \"passed\": true}, {\"check\": \"positive reverse\", \"actual\": 4607182418800017407, \"expected\": 4607182418800017407, \"passed\": true}, {\"check\": \"negative forward\", \"actual\": 13830554455654793215, \"expected\": 13830554455654793215, \"passed\": true}, {\"check\": \"negative away\", \"actual\": 13830554455654793217, \"expected\": 13830554455654793217, \"passed\": true}, {\"check\": \"negative zero equality\", \"actual\": 9223372036854775808, \"expected\": 9223372036854775808, \"passed\": true}, {\"check\": \"positive zero equality\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"zero negative\", \"actual\": 9223372036854775809, \"expected\": 9223372036854775809, \"passed\": true}, {\"check\": \"zero positive\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"nan target\", \"actual\": 9221120237041090560, \"expected\": 9221120237041090560, \"passed\": true}, {\"check\": \"nan source\", \"actual\": 9218868437227405314, \"expected\": 9221120237041090560, \"passed\": false}, {\"check\": \"finite step varies\", \"actual\": 4611686018427387903, \"expected\": 4611686018427387903, \"passed\": true}, {\"check\": \"infinity inward\", \"actual\": 9218868437227405311, \"expected\": 9218868437227405311, \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":40.497,"exit_code":0,"observations":[{"actual":4607182418800017409,"check":"positive step","expected":4607182418800017409,"passed":true},{"actual":4607182418800017407,"check":"positive reverse","expected":4607182418800017407,"passed":true},{"actual":13830554455654793215,"check":"negative forward","expected":13830554455654793215,"passed":true},{"actual":13830554455654793217,"check":"negative away","expected":13830554455654793217,"passed":true},{"actual":9223372036854775808,"check":"negative zero equality","expected":9223372036854775808,"passed":true},{"actual":0,"check":"positive zero equality","expected":0,"passed":true},{"actual":9223372036854775809,"check":"zero negative","expected":9223372036854775809,"passed":true},{"actual":1,"check":"zero positive","expected":1,"passed":true},{"actual":9221120237041090560,"check":"nan target","expected":9221120237041090560,"passed":true},{"actual":9221120237041090560,"check":"nan source","expected":9221120237041090560,"passed":true},{"actual":4611686018427387903,"check":"finite step varies","expected":4611686018427387903,"passed":true},{"actual":9218868437227405311,"check":"infinity inward","expected":9218868437227405311,"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"positive step\", \"actual\": 4607182418800017409, \"expected\": 4607182418800017409, \"passed\": true}, {\"check\": \"positive reverse\", \"actual\": 4607182418800017407, \"expected\": 4607182418800017407, \"passed\": true}, {\"check\": \"negative forward\", \"actual\": 13830554455654793215, \"expected\": 13830554455654793215, \"passed\": true}, {\"check\": \"negative away\", \"actual\": 13830554455654793217, \"expected\": 13830554455654793217, \"passed\": true}, {\"check\": \"negative zero equality\", \"actual\": 9223372036854775808, \"expected\": 9223372036854775808, \"passed\": true}, {\"check\": \"positive zero equality\", \"actual\": 0, \"expected\": 0, \"passed\": true}, {\"check\": \"zero negative\", \"actual\": 9223372036854775809, \"expected\": 9223372036854775809, \"passed\": true}, {\"check\": \"zero positive\", \"actual\": 1, \"expected\": 1, \"passed\": true}, {\"check\": \"nan target\", \"actual\": 9221120237041090560, \"expected\": 9221120237041090560, \"passed\": true}, {\"check\": \"nan source\", \"actual\": 9221120237041090560, \"expected\": 9221120237041090560, \"passed\": true}, {\"check\": \"finite step varies\", \"actual\": 4611686018427387903, \"expected\": 4611686018427387903, \"passed\": true}, {\"check\": \"infinity inward\", \"actual\": 9218868437227405311, \"expected\": 9218868437227405311, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}