{"abstract":"Exact ratio conversion removes factors of two from odd mantissas.","category":"Floating-point arithmetic","checks":11,"contract":"Decode a finite binary64 value into its exact reduced signed numerator and positive power-of-two denominator, using (0,1) for either zero. Infinity and NaN return null.","evaluation_group":"s3-float-float-ratio","failed_approach":"The attempted local correction while power<0 and mantissa%2==1: still violates the explicit regression fixtures.","family":"s3-floating_point_arithmetic-float-ratio-reduction-condition","id":"FA-16631","implementations":{"attempt":{"sha256":"fe32d2ae4234a008c8c09cd6725a1c82777a4e974c2e7a83c9f8797a22ed4c42","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(bits):\n    sign=-1 if bits>>63 else 1\n    e=(bits>>52)&2047\n    f=bits&((1<<52)-1)\n    if e==2047: return None\n    if e:\n        mantissa=f|(1<<52)\n        power=e-1023-52\n    else:\n        mantissa=f\n        power=-1074\n    if mantissa==0: return [0,1]\n    while power<0 and mantissa%2==1:\n        mantissa//=2\n        power+=1\n    if power>=0: return [sign*(mantissa<<power),1]\n    return [sign*mantissa,1<<(-power)]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])\ncheck('positive integer', solve((1023+N)<<52), [1<<N,1])\ncheck('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])\ncheck('fraction', solve(0x3fe0000000000000), [1,2])\ncheck('nontrivial fraction', solve(0x3fe8000000000000), [3,4])\ncheck('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))\ncheck('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))\ncheck('zero', solve(0), [0,1])\ncheck('negative zero', solve(1<<63), [0,1])\ncheck('infinity', solve(0x7ff0000000000000), None)\ncheck('nan', solve(0x7ff8000000000000|N), None)\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":"c1b8cb6133e649469c58a06236041f5eccf6881d558896470ba8b8f0c72fe99a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(bits):\n    sign=-1 if bits>>63 else 1\n    e=(bits>>52)&2047\n    f=bits&((1<<52)-1)\n    if e==2047: return None\n    if e:\n        mantissa=f|(1<<52)\n        power=e-1023-52\n    else:\n        mantissa=f\n        power=-1074\n    if mantissa==0: return [0,1]\n    while power<0 and mantissa>1:\n        mantissa//=2\n        power+=1\n    if power>=0: return [sign*(mantissa<<power),1]\n    return [sign*mantissa,1<<(-power)]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])\ncheck('positive integer', solve((1023+N)<<52), [1<<N,1])\ncheck('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])\ncheck('fraction', solve(0x3fe0000000000000), [1,2])\ncheck('nontrivial fraction', solve(0x3fe8000000000000), [3,4])\ncheck('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))\ncheck('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))\ncheck('zero', solve(0), [0,1])\ncheck('negative zero', solve(1<<63), [0,1])\ncheck('infinity', solve(0x7ff0000000000000), None)\ncheck('nan', solve(0x7ff8000000000000|N), None)\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":"232c5cccac878943ca1770bff8d7a21afb5af3860d3181aefa1b46f6590a6293","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\nN = 1\nobservations = []\ndef solve(bits):\n    sign=-1 if bits>>63 else 1\n    e=(bits>>52)&2047\n    f=bits&((1<<52)-1)\n    if e==2047: return None\n    if e:\n        mantissa=f|(1<<52)\n        power=e-1023-52\n    else:\n        mantissa=f\n        power=-1074\n    if mantissa==0: return [0,1]\n    while power<0 and mantissa%2==0:\n        mantissa//=2\n        power+=1\n    if power>=0: return [sign*(mantissa<<power),1]\n    return [sign*mantissa,1<<(-power)]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])\ncheck('positive integer', solve((1023+N)<<52), [1<<N,1])\ncheck('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])\ncheck('fraction', solve(0x3fe0000000000000), [1,2])\ncheck('nontrivial fraction', solve(0x3fe8000000000000), [3,4])\ncheck('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))\ncheck('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))\ncheck('zero', solve(0), [0,1])\ncheck('negative zero', solve(1<<63), [0,1])\ncheck('infinity', solve(0x7ff0000000000000), None)\ncheck('nan', solve(0x7ff8000000000000|N), None)\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-float-ratio-reduction-condition","generated_at":"2026-09-29T14:39:38.069822+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 while power<0 and mantissa%2==0:.","root_cause":"Exact ratio conversion removes factors of two from odd mantissas. The faulty expression is while power<0 and mantissa>1:.","sha256":"da9a3fcfc69c58c6880dd1514d187eb5e525e9238d9cd7c6d0bf8ad064cda017","title":"Exact ratio conversion removes factors of two from odd mantissas · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.304,"exit_code":1,"observations":[{"actual":[2305843009213693952,1],"check":"large integer","expected":[2305843009213693952,1],"passed":true},{"actual":[4503599627370496,2251799813685248],"check":"positive integer","expected":[2,1],"passed":false},{"actual":[-4503599627370496,2251799813685248],"check":"negative integer","expected":[-2,1],"passed":false},{"actual":[4503599627370496,9007199254740992],"check":"fraction","expected":[1,2],"passed":false},{"actual":[6755399441055744,9007199254740992],"check":"nontrivial fraction","expected":[3,4],"passed":false},{"actual":[0,101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392],"check":"minimum subnormal","expected":[1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":false},{"actual":[0,101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392],"check":"negative subnormal","expected":[-1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":false},{"actual":[0,1],"check":"zero","expected":[0,1],"passed":true},{"actual":[0,1],"check":"negative zero","expected":[0,1],"passed":true},{"actual":null,"check":"infinity","expected":null,"passed":true},{"actual":null,"check":"nan","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"large integer\", \"actual\": [2305843009213693952, 1], \"expected\": [2305843009213693952, 1], \"passed\": true}, {\"check\": \"positive integer\", \"actual\": [4503599627370496, 2251799813685248], \"expected\": [2, 1], \"passed\": false}, {\"check\": \"negative integer\", \"actual\": [-4503599627370496, 2251799813685248], \"expected\": [-2, 1], \"passed\": false}, {\"check\": \"fraction\", \"actual\": [4503599627370496, 9007199254740992], \"expected\": [1, 2], \"passed\": false}, {\"check\": \"nontrivial fraction\", \"actual\": [6755399441055744, 9007199254740992], \"expected\": [3, 4], \"passed\": false}, {\"check\": \"minimum subnormal\", \"actual\": [0, 101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392], \"expected\": [1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": false}, {\"check\": \"negative subnormal\", \"actual\": [0, 101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392], \"expected\": [-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": false}, {\"check\": \"zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"negative zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"infinity\", \"actual\": null, \"expected\": null, \"passed\": true}, {\"check\": \"nan\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":41.931,"exit_code":1,"observations":[{"actual":[2305843009213693952,1],"check":"large integer","expected":[2305843009213693952,1],"passed":true},{"actual":[2,1],"check":"positive integer","expected":[2,1],"passed":true},{"actual":[-2,1],"check":"negative integer","expected":[-2,1],"passed":true},{"actual":[1,2],"check":"fraction","expected":[1,2],"passed":true},{"actual":[1,2],"check":"nontrivial fraction","expected":[3,4],"passed":false},{"actual":[1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"check":"minimum subnormal","expected":[1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":true},{"actual":[-1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"check":"negative subnormal","expected":[-1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":true},{"actual":[0,1],"check":"zero","expected":[0,1],"passed":true},{"actual":[0,1],"check":"negative zero","expected":[0,1],"passed":true},{"actual":null,"check":"infinity","expected":null,"passed":true},{"actual":null,"check":"nan","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"large integer\", \"actual\": [2305843009213693952, 1], \"expected\": [2305843009213693952, 1], \"passed\": true}, {\"check\": \"positive integer\", \"actual\": [2, 1], \"expected\": [2, 1], \"passed\": true}, {\"check\": \"negative integer\", \"actual\": [-2, 1], \"expected\": [-2, 1], \"passed\": true}, {\"check\": \"fraction\", \"actual\": [1, 2], \"expected\": [1, 2], \"passed\": true}, {\"check\": \"nontrivial fraction\", \"actual\": [1, 2], \"expected\": [3, 4], \"passed\": false}, {\"check\": \"minimum subnormal\", \"actual\": [1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"expected\": [1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": true}, {\"check\": \"negative subnormal\", \"actual\": [-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"expected\": [-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": true}, {\"check\": \"zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"negative zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"infinity\", \"actual\": null, \"expected\": null, \"passed\": true}, {\"check\": \"nan\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":43.522,"exit_code":0,"observations":[{"actual":[2305843009213693952,1],"check":"large integer","expected":[2305843009213693952,1],"passed":true},{"actual":[2,1],"check":"positive integer","expected":[2,1],"passed":true},{"actual":[-2,1],"check":"negative integer","expected":[-2,1],"passed":true},{"actual":[1,2],"check":"fraction","expected":[1,2],"passed":true},{"actual":[3,4],"check":"nontrivial fraction","expected":[3,4],"passed":true},{"actual":[1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"check":"minimum subnormal","expected":[1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":true},{"actual":[-1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"check":"negative subnormal","expected":[-1,202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784],"passed":true},{"actual":[0,1],"check":"zero","expected":[0,1],"passed":true},{"actual":[0,1],"check":"negative zero","expected":[0,1],"passed":true},{"actual":null,"check":"infinity","expected":null,"passed":true},{"actual":null,"check":"nan","expected":null,"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"large integer\", \"actual\": [2305843009213693952, 1], \"expected\": [2305843009213693952, 1], \"passed\": true}, {\"check\": \"positive integer\", \"actual\": [2, 1], \"expected\": [2, 1], \"passed\": true}, {\"check\": \"negative integer\", \"actual\": [-2, 1], \"expected\": [-2, 1], \"passed\": true}, {\"check\": \"fraction\", \"actual\": [1, 2], \"expected\": [1, 2], \"passed\": true}, {\"check\": \"nontrivial fraction\", \"actual\": [3, 4], \"expected\": [3, 4], \"passed\": true}, {\"check\": \"minimum subnormal\", \"actual\": [1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"expected\": [1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": true}, {\"check\": \"negative subnormal\", \"actual\": [-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"expected\": [-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784], \"passed\": true}, {\"check\": \"zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"negative zero\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}, {\"check\": \"infinity\", \"actual\": null, \"expected\": null, \"passed\": true}, {\"check\": \"nan\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}