{"abstract":"Quiet NaN addition selects the smaller diagnostic payload.","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 chosen=ab still violates the explicit regression fixtures.","family":"s3-floating_point_arithmetic-nan-add-payload-choice","id":"FA-16556","implementations":{"attempt":{"sha256":"23e66c9bf1d50985027fbeeeca731cf954a3318c5b88e915a4d6521c91592222","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\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"},"broken":{"sha256":"3cf09ed11084a84ee3e5b4898a9b588e9498996d2aac21a1b1c88a91cf49fb91","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"},"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-payload-choice","generated_at":"2026-09-29T14:39:37.367805+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 chosen=ab if (ab&((1<<51)-1)) >= (bb&((1<<51)-1)) else bb.","root_cause":"Quiet NaN addition selects the smaller diagnostic payload. The faulty expression is chosen=ab if (ab&((1<<51)-1)) <= (bb&((1<<51)-1)) else bb.","sha256":"95831376a8a8928dc7ff67516aa7228673f1416b9f0a835d749612ff70541d0b","title":"Quiet NaN addition selects the smaller diagnostic payload · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":38.167,"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":[9221120237041090561,false],"check":"larger right payload","expected":[18444492273895866468,false],"passed":false},{"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":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\": [9221120237041090561, false], \"expected\": [18444492273895866468, false], \"passed\": false}, {\"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\": false}\n"},"broken":{"elapsed_ms":40.997,"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":[9221120237041090561,false],"check":"larger right payload","expected":[18444492273895866468,false],"passed":false},{"actual":[9221120237041090561,false],"check":"larger left payload","expected":[18444492273895866468,false],"passed":false},{"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":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\": [9221120237041090561, false], \"expected\": [18444492273895866468, false], \"passed\": false}, {\"check\": \"larger left payload\", \"actual\": [9221120237041090561, false], \"expected\": [18444492273895866468, false], \"passed\": false}, {\"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\": false}\n"},"fixed":{"elapsed_ms":42.72,"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"}