{"abstract":"Opposite infinities fail to raise invalid on addition.","category":"Floating-point arithmetic","checks":14,"contract":"Stipulated binary64 addition policy: propagate first signaling NaN, otherwise largest quiet-NaN diagnostic payload (left wins ties); quiet propagated NaNs preserving sign. Opposite infinities produce canonical quiet NaN. Finite values use Python binary64 addition. Return bits and invalid flag.","evaluation_group":"s3-float-nan-add","failed_approach":"The attempted local correction return [0x7ff0000000000000,False] still violates the explicit regression fixtures.","family":"s3-floating_point_arithmetic-nan-add-infinity-invalid","id":"FA-16576","implementations":{"attempt":{"sha256":"3f4346fd1a7bbae80d7beb702b2770475469b032d5cb959e011bbe7811c22f35","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(ab,bb):\n    mask=(1<<52)-1\n    an=(ab>>52)&2047==2047 and bool(ab&mask)\n    bn=(bb>>52)&2047==2047 and bool(bb&mask)\n    asig=an and not bool(ab&(1<<51))\n    bsig=bn and not bool(bb&(1<<51))\n    if asig or bsig:\n        chosen=ab if asig else bb\n        return [chosen|(1<<51),True]\n    if an or bn:\n        if an and bn:\n            chosen=ab if (ab&((1<<51)-1)) >= (bb&((1<<51)-1)) else bb\n        else:\n            chosen=ab if an else bb\n        return [chosen,False]\n    a=struct.unpack('>d',ab.to_bytes(8,'big'))[0]\n    b=struct.unpack('>d',bb.to_bytes(8,'big'))[0]\n    if math.isinf(a) and math.isinf(b) and a!=b:\n        return [0x7ff0000000000000,False]\n    result=a+b\n    return [int.from_bytes(struct.pack('>d',result),'big'),False]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('left signaling', solve(0x7ff0000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,True])\ncheck('right signaling', solve(0x3ff0000000000000,0xfff0000000000000|N), [0xfff8000000000000|N,True])\ncheck('signaling precedence', solve(0x7ff8000000000064,0x7ff0000000000000|N), [0x7ff8000000000000|N,True])\ncheck('two signaling', solve(0xfff0000000000000|N,0x7ff0000000000010), [0xfff8000000000000|N,True])\ncheck('larger right payload', solve(0x7ff8000000000000|N,0xfff8000000000064), [0xfff8000000000064,False])\ncheck('larger left payload', solve(0xfff8000000000064,0x7ff8000000000000|N), [0xfff8000000000064,False])\ncheck('equal left wins', solve(0xfff8000000000000|N,0x7ff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('positive quiet', solve(0x7ff8000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,False])\ncheck('quiet left only', solve(0xfff8000000000000|N,0x3ff0000000000000), [0xfff8000000000000|N,False])\ncheck('quiet right only', solve(0x3ff0000000000000,0xfff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('opposite infinities', solve(0x7ff0000000000000,0xfff0000000000000), [0x7ff8000000000000,True])\ncheck('same infinity', solve(0xfff0000000000000,0xfff0000000000000), [0xfff0000000000000,False])\ncheck('finite addition', solve(0x3ff0000000000000,0x3ff0000000000000), [0x4000000000000000,False])\ncheck('negative zeros', solve(1<<63,1<<63), [1<<63,False])\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":"57396420b2b43f9f58a5e0891b2cdb456bb169b27db8c33a640a95dc1d381be7","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(ab,bb):\n    mask=(1<<52)-1\n    an=(ab>>52)&2047==2047 and bool(ab&mask)\n    bn=(bb>>52)&2047==2047 and bool(bb&mask)\n    asig=an and not bool(ab&(1<<51))\n    bsig=bn and not bool(bb&(1<<51))\n    if asig or bsig:\n        chosen=ab if asig else bb\n        return [chosen|(1<<51),True]\n    if an or bn:\n        if an and bn:\n            chosen=ab if (ab&((1<<51)-1)) >= (bb&((1<<51)-1)) else bb\n        else:\n            chosen=ab if an else bb\n        return [chosen,False]\n    a=struct.unpack('>d',ab.to_bytes(8,'big'))[0]\n    b=struct.unpack('>d',bb.to_bytes(8,'big'))[0]\n    if math.isinf(a) and math.isinf(b) and a!=b:\n        return [0x7ff8000000000000,False]\n    result=a+b\n    return [int.from_bytes(struct.pack('>d',result),'big'),False]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('left signaling', solve(0x7ff0000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,True])\ncheck('right signaling', solve(0x3ff0000000000000,0xfff0000000000000|N), [0xfff8000000000000|N,True])\ncheck('signaling precedence', solve(0x7ff8000000000064,0x7ff0000000000000|N), [0x7ff8000000000000|N,True])\ncheck('two signaling', solve(0xfff0000000000000|N,0x7ff0000000000010), [0xfff8000000000000|N,True])\ncheck('larger right payload', solve(0x7ff8000000000000|N,0xfff8000000000064), [0xfff8000000000064,False])\ncheck('larger left payload', solve(0xfff8000000000064,0x7ff8000000000000|N), [0xfff8000000000064,False])\ncheck('equal left wins', solve(0xfff8000000000000|N,0x7ff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('positive quiet', solve(0x7ff8000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,False])\ncheck('quiet left only', solve(0xfff8000000000000|N,0x3ff0000000000000), [0xfff8000000000000|N,False])\ncheck('quiet right only', solve(0x3ff0000000000000,0xfff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('opposite infinities', solve(0x7ff0000000000000,0xfff0000000000000), [0x7ff8000000000000,True])\ncheck('same infinity', solve(0xfff0000000000000,0xfff0000000000000), [0xfff0000000000000,False])\ncheck('finite addition', solve(0x3ff0000000000000,0x3ff0000000000000), [0x4000000000000000,False])\ncheck('negative zeros', solve(1<<63,1<<63), [1<<63,False])\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":"a22a003c8dfdecc224fbfc96d6bd9268c4c9fc9fb4044fdbdad84b62a3040788","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(ab,bb):\n    mask=(1<<52)-1\n    an=(ab>>52)&2047==2047 and bool(ab&mask)\n    bn=(bb>>52)&2047==2047 and bool(bb&mask)\n    asig=an and not bool(ab&(1<<51))\n    bsig=bn and not bool(bb&(1<<51))\n    if asig or bsig:\n        chosen=ab if asig else bb\n        return [chosen|(1<<51),True]\n    if an or bn:\n        if an and bn:\n            chosen=ab if (ab&((1<<51)-1)) >= (bb&((1<<51)-1)) else bb\n        else:\n            chosen=ab if an else bb\n        return [chosen,False]\n    a=struct.unpack('>d',ab.to_bytes(8,'big'))[0]\n    b=struct.unpack('>d',bb.to_bytes(8,'big'))[0]\n    if math.isinf(a) and math.isinf(b) and a!=b:\n        return [0x7ff8000000000000,True]\n    result=a+b\n    return [int.from_bytes(struct.pack('>d',result),'big'),False]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('left signaling', solve(0x7ff0000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,True])\ncheck('right signaling', solve(0x3ff0000000000000,0xfff0000000000000|N), [0xfff8000000000000|N,True])\ncheck('signaling precedence', solve(0x7ff8000000000064,0x7ff0000000000000|N), [0x7ff8000000000000|N,True])\ncheck('two signaling', solve(0xfff0000000000000|N,0x7ff0000000000010), [0xfff8000000000000|N,True])\ncheck('larger right payload', solve(0x7ff8000000000000|N,0xfff8000000000064), [0xfff8000000000064,False])\ncheck('larger left payload', solve(0xfff8000000000064,0x7ff8000000000000|N), [0xfff8000000000064,False])\ncheck('equal left wins', solve(0xfff8000000000000|N,0x7ff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('positive quiet', solve(0x7ff8000000000000|N,0x3ff0000000000000), [0x7ff8000000000000|N,False])\ncheck('quiet left only', solve(0xfff8000000000000|N,0x3ff0000000000000), [0xfff8000000000000|N,False])\ncheck('quiet right only', solve(0x3ff0000000000000,0xfff8000000000000|N), [0xfff8000000000000|N,False])\ncheck('opposite infinities', solve(0x7ff0000000000000,0xfff0000000000000), [0x7ff8000000000000,True])\ncheck('same infinity', solve(0xfff0000000000000,0xfff0000000000000), [0xfff0000000000000,False])\ncheck('finite addition', solve(0x3ff0000000000000,0x3ff0000000000000), [0x4000000000000000,False])\ncheck('negative zeros', solve(1<<63,1<<63), [1<<63,False])\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-nan-add-infinity-invalid","generated_at":"2026-09-29T14:39:37.676379+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 return [0x7ff8000000000000,True].","root_cause":"Opposite infinities fail to raise invalid on addition. The faulty expression is return [0x7ff8000000000000,False].","sha256":"ae759177549d047a81f6e498034dd424fadccc02c5b30330f09b5e4ab8d41d19","title":"Opposite infinities fail to raise invalid on addition · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.929,"exit_code":1,"observations":[{"actual":[9221120237041090561,true],"check":"left signaling","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"right signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[9221120237041090561,true],"check":"signaling precedence","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"two signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[18444492273895866468,false],"check":"larger right payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866468,false],"check":"larger left payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866369,false],"check":"equal left wins","expected":[18444492273895866369,false],"passed":true},{"actual":[9221120237041090561,false],"check":"positive quiet","expected":[9221120237041090561,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet left only","expected":[18444492273895866369,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet right only","expected":[18444492273895866369,false],"passed":true},{"actual":[9218868437227405312,false],"check":"opposite infinities","expected":[9221120237041090560,true],"passed":false},{"actual":[18442240474082181120,false],"check":"same infinity","expected":[18442240474082181120,false],"passed":true},{"actual":[4611686018427387904,false],"check":"finite addition","expected":[4611686018427387904,false],"passed":true},{"actual":[9223372036854775808,false],"check":"negative zeros","expected":[9223372036854775808,false],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"left signaling\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"right signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"signaling precedence\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"two signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"larger right payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"larger left payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"equal left wins\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"positive quiet\", \"actual\": [9221120237041090561, false], \"expected\": [9221120237041090561, false], \"passed\": true}, {\"check\": \"quiet left only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"quiet right only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"opposite infinities\", \"actual\": [9218868437227405312, false], \"expected\": [9221120237041090560, true], \"passed\": false}, {\"check\": \"same infinity\", \"actual\": [18442240474082181120, false], \"expected\": [18442240474082181120, false], \"passed\": true}, {\"check\": \"finite addition\", \"actual\": [4611686018427387904, false], \"expected\": [4611686018427387904, false], \"passed\": true}, {\"check\": \"negative zeros\", \"actual\": [9223372036854775808, false], \"expected\": [9223372036854775808, false], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":44.339,"exit_code":1,"observations":[{"actual":[9221120237041090561,true],"check":"left signaling","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"right signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[9221120237041090561,true],"check":"signaling precedence","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"two signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[18444492273895866468,false],"check":"larger right payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866468,false],"check":"larger left payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866369,false],"check":"equal left wins","expected":[18444492273895866369,false],"passed":true},{"actual":[9221120237041090561,false],"check":"positive quiet","expected":[9221120237041090561,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet left only","expected":[18444492273895866369,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet right only","expected":[18444492273895866369,false],"passed":true},{"actual":[9221120237041090560,false],"check":"opposite infinities","expected":[9221120237041090560,true],"passed":false},{"actual":[18442240474082181120,false],"check":"same infinity","expected":[18442240474082181120,false],"passed":true},{"actual":[4611686018427387904,false],"check":"finite addition","expected":[4611686018427387904,false],"passed":true},{"actual":[9223372036854775808,false],"check":"negative zeros","expected":[9223372036854775808,false],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"left signaling\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"right signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"signaling precedence\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"two signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"larger right payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"larger left payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"equal left wins\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"positive quiet\", \"actual\": [9221120237041090561, false], \"expected\": [9221120237041090561, false], \"passed\": true}, {\"check\": \"quiet left only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"quiet right only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"opposite infinities\", \"actual\": [9221120237041090560, false], \"expected\": [9221120237041090560, true], \"passed\": false}, {\"check\": \"same infinity\", \"actual\": [18442240474082181120, false], \"expected\": [18442240474082181120, false], \"passed\": true}, {\"check\": \"finite addition\", \"actual\": [4611686018427387904, false], \"expected\": [4611686018427387904, false], \"passed\": true}, {\"check\": \"negative zeros\", \"actual\": [9223372036854775808, false], \"expected\": [9223372036854775808, false], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":41.136,"exit_code":0,"observations":[{"actual":[9221120237041090561,true],"check":"left signaling","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"right signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[9221120237041090561,true],"check":"signaling precedence","expected":[9221120237041090561,true],"passed":true},{"actual":[18444492273895866369,true],"check":"two signaling","expected":[18444492273895866369,true],"passed":true},{"actual":[18444492273895866468,false],"check":"larger right payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866468,false],"check":"larger left payload","expected":[18444492273895866468,false],"passed":true},{"actual":[18444492273895866369,false],"check":"equal left wins","expected":[18444492273895866369,false],"passed":true},{"actual":[9221120237041090561,false],"check":"positive quiet","expected":[9221120237041090561,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet left only","expected":[18444492273895866369,false],"passed":true},{"actual":[18444492273895866369,false],"check":"quiet right only","expected":[18444492273895866369,false],"passed":true},{"actual":[9221120237041090560,true],"check":"opposite infinities","expected":[9221120237041090560,true],"passed":true},{"actual":[18442240474082181120,false],"check":"same infinity","expected":[18442240474082181120,false],"passed":true},{"actual":[4611686018427387904,false],"check":"finite addition","expected":[4611686018427387904,false],"passed":true},{"actual":[9223372036854775808,false],"check":"negative zeros","expected":[9223372036854775808,false],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"left signaling\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"right signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"signaling precedence\", \"actual\": [9221120237041090561, true], \"expected\": [9221120237041090561, true], \"passed\": true}, {\"check\": \"two signaling\", \"actual\": [18444492273895866369, true], \"expected\": [18444492273895866369, true], \"passed\": true}, {\"check\": \"larger right payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"larger left payload\", \"actual\": [18444492273895866468, false], \"expected\": [18444492273895866468, false], \"passed\": true}, {\"check\": \"equal left wins\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"positive quiet\", \"actual\": [9221120237041090561, false], \"expected\": [9221120237041090561, false], \"passed\": true}, {\"check\": \"quiet left only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"quiet right only\", \"actual\": [18444492273895866369, false], \"expected\": [18444492273895866369, false], \"passed\": true}, {\"check\": \"opposite infinities\", \"actual\": [9221120237041090560, true], \"expected\": [9221120237041090560, true], \"passed\": true}, {\"check\": \"same infinity\", \"actual\": [18442240474082181120, false], \"expected\": [18442240474082181120, false], \"passed\": true}, {\"check\": \"finite addition\", \"actual\": [4611686018427387904, false], \"expected\": [4611686018427387904, false], \"passed\": true}, {\"check\": \"negative zeros\", \"actual\": [9223372036854775808, false], \"expected\": [9223372036854775808, false], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}