{"abstract":"Nearest floating remainder keeps the sign of the divisor.","category":"Floating-point arithmetic","checks":12,"contract":"For finite x and finite nonzero y, return the remainder x-n*y with n the nearest integer quotient, ties to even. The output has magnitude at most abs(y)/2; exact zero has the sign of x. Finite results are rendered to eleven significant decimal digits; modeled domain violations and arithmetic errors are explicit strings.","evaluation_group":"s3-float-nearest-remainder","failed_approach":"The attempted local correction ay=-abs(y) still violates the explicit regression fixtures.","family":"s3-floating_point_arithmetic-nearest-remainder-negative-divisor-normalize","id":"FA-17336","implementations":{"attempt":{"sha256":"a70cccbe6c30282d75cc18e1928d4166159bfde302962b028579177191aabd32","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\ndef render(x):\n    if math.isnan(x): return 'nan'\n    if math.isinf(x): return '-infinity' if x<0 else '+infinity'\n    return format(x,'.11g')\n\nN = 1\nobservations = []\ndef solve(x,y):\n    try:\n        if y==0: return 'domain'\n        ay=-abs(y)\n        r=math.fmod(x,ay)\n        a=abs(r)\n        other=ay-a\n        odd=math.fmod(abs(x),2*ay)>=ay\n        if a>other or (a==other and odd):\n            r-=math.copysign(ay,x)\n        if r==0: r=math.copysign(0.0,x)\n        return render(r)\n    except (ValueError, OverflowError, ZeroDivisionError, TypeError):\n        return \"arithmetic-error\"\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('even tie', solve(2.0*N*4+2,4.0), \"2\")\ncheck('odd tie', solve((2.0*N+1)*4+2,4.0), \"-2\")\ncheck('negative even tie', solve(-2.0*N*4-2,4.0), \"-2\")\ncheck('negative odd tie', solve(-(2.0*N+1)*4-2,4.0), \"2\")\ncheck('above half', solve(4.0*N+3,4.0), \"-1\")\ncheck('below half', solve(4.0*N+1,4.0), \"1\")\ncheck('negative divisor below half', solve(4.0*N+1,-4.0), \"1\")\ncheck('negative divisor', solve(4.0*N+3,-4.0), \"-1\")\ncheck('negative exact', solve(-4.0*N,4.0), \"-0\")\ncheck('positive exact', solve(4.0*N,4.0), \"0\")\ncheck('zero divisor', solve(float(N),0.0), \"domain\")\ncheck('huge finite', solve(1.5e308,1e308), render(math.remainder(1.5e308,1e308)))\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":"8b8c15d97698895b0be3a516d1888b5c148eaaed651c8e15751ac35449cf2fad","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\ndef render(x):\n    if math.isnan(x): return 'nan'\n    if math.isinf(x): return '-infinity' if x<0 else '+infinity'\n    return format(x,'.11g')\n\nN = 1\nobservations = []\ndef solve(x,y):\n    try:\n        if y==0: return 'domain'\n        ay=y\n        r=math.fmod(x,ay)\n        a=abs(r)\n        other=ay-a\n        odd=math.fmod(abs(x),2*ay)>=ay\n        if a>other or (a==other and odd):\n            r-=math.copysign(ay,x)\n        if r==0: r=math.copysign(0.0,x)\n        return render(r)\n    except (ValueError, OverflowError, ZeroDivisionError, TypeError):\n        return \"arithmetic-error\"\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('even tie', solve(2.0*N*4+2,4.0), \"2\")\ncheck('odd tie', solve((2.0*N+1)*4+2,4.0), \"-2\")\ncheck('negative even tie', solve(-2.0*N*4-2,4.0), \"-2\")\ncheck('negative odd tie', solve(-(2.0*N+1)*4-2,4.0), \"2\")\ncheck('above half', solve(4.0*N+3,4.0), \"-1\")\ncheck('below half', solve(4.0*N+1,4.0), \"1\")\ncheck('negative divisor below half', solve(4.0*N+1,-4.0), \"1\")\ncheck('negative divisor', solve(4.0*N+3,-4.0), \"-1\")\ncheck('negative exact', solve(-4.0*N,4.0), \"-0\")\ncheck('positive exact', solve(4.0*N,4.0), \"0\")\ncheck('zero divisor', solve(float(N),0.0), \"domain\")\ncheck('huge finite', solve(1.5e308,1e308), render(math.remainder(1.5e308,1e308)))\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":"219b3658834515af71ddcc114790af2e7ee62879adddbee7d0d062833b3403a6","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\nimport math\nimport struct\ndef render(x):\n    if math.isnan(x): return 'nan'\n    if math.isinf(x): return '-infinity' if x<0 else '+infinity'\n    return format(x,'.11g')\n\nN = 1\nobservations = []\ndef solve(x,y):\n    try:\n        if y==0: return 'domain'\n        ay=abs(y)\n        r=math.fmod(x,ay)\n        a=abs(r)\n        other=ay-a\n        odd=math.fmod(abs(x),2*ay)>=ay\n        if a>other or (a==other and odd):\n            r-=math.copysign(ay,x)\n        if r==0: r=math.copysign(0.0,x)\n        return render(r)\n    except (ValueError, OverflowError, ZeroDivisionError, TypeError):\n        return \"arithmetic-error\"\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('even tie', solve(2.0*N*4+2,4.0), \"2\")\ncheck('odd tie', solve((2.0*N+1)*4+2,4.0), \"-2\")\ncheck('negative even tie', solve(-2.0*N*4-2,4.0), \"-2\")\ncheck('negative odd tie', solve(-(2.0*N+1)*4-2,4.0), \"2\")\ncheck('above half', solve(4.0*N+3,4.0), \"-1\")\ncheck('below half', solve(4.0*N+1,4.0), \"1\")\ncheck('negative divisor below half', solve(4.0*N+1,-4.0), \"1\")\ncheck('negative divisor', solve(4.0*N+3,-4.0), \"-1\")\ncheck('negative exact', solve(-4.0*N,4.0), \"-0\")\ncheck('positive exact', solve(4.0*N,4.0), \"0\")\ncheck('zero divisor', solve(float(N),0.0), \"domain\")\ncheck('huge finite', solve(1.5e308,1e308), render(math.remainder(1.5e308,1e308)))\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-nearest-remainder-negative-divisor-normalize","generated_at":"2026-09-29T14:39:45.192120+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 ay=abs(y).","root_cause":"Nearest floating remainder keeps the sign of the divisor. The faulty expression is ay=y.","sha256":"3e8c11bc9dfae2a384867567b05828e056eaf951b27a117520841b35a8f2aee5","title":"Nearest floating remainder keeps the sign of the divisor · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":43.569,"exit_code":1,"observations":[{"actual":"-2","check":"even tie","expected":"2","passed":false},{"actual":"-2","check":"odd tie","expected":"-2","passed":true},{"actual":"2","check":"negative even tie","expected":"-2","passed":false},{"actual":"2","check":"negative odd tie","expected":"2","passed":true},{"actual":"-1","check":"above half","expected":"-1","passed":true},{"actual":"-3","check":"below half","expected":"1","passed":false},{"actual":"-3","check":"negative divisor below half","expected":"1","passed":false},{"actual":"-1","check":"negative divisor","expected":"-1","passed":true},{"actual":"4","check":"negative exact","expected":"-0","passed":false},{"actual":"-4","check":"positive exact","expected":"0","passed":false},{"actual":"domain","check":"zero divisor","expected":"domain","passed":true},{"actual":"-5e+307","check":"huge finite","expected":"-5e+307","passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"even tie\", \"actual\": \"-2\", \"expected\": \"2\", \"passed\": false}, {\"check\": \"odd tie\", \"actual\": \"-2\", \"expected\": \"-2\", \"passed\": true}, {\"check\": \"negative even tie\", \"actual\": \"2\", \"expected\": \"-2\", \"passed\": false}, {\"check\": \"negative odd tie\", \"actual\": \"2\", \"expected\": \"2\", \"passed\": true}, {\"check\": \"above half\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"below half\", \"actual\": \"-3\", \"expected\": \"1\", \"passed\": false}, {\"check\": \"negative divisor below half\", \"actual\": \"-3\", \"expected\": \"1\", \"passed\": false}, {\"check\": \"negative divisor\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"negative exact\", \"actual\": \"4\", \"expected\": \"-0\", \"passed\": false}, {\"check\": \"positive exact\", \"actual\": \"-4\", \"expected\": \"0\", \"passed\": false}, {\"check\": \"zero divisor\", \"actual\": \"domain\", \"expected\": \"domain\", \"passed\": true}, {\"check\": \"huge finite\", \"actual\": \"-5e+307\", \"expected\": \"-5e+307\", \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":46.433,"exit_code":1,"observations":[{"actual":"2","check":"even tie","expected":"2","passed":true},{"actual":"-2","check":"odd tie","expected":"-2","passed":true},{"actual":"-2","check":"negative even tie","expected":"-2","passed":true},{"actual":"2","check":"negative odd tie","expected":"2","passed":true},{"actual":"-1","check":"above half","expected":"-1","passed":true},{"actual":"1","check":"below half","expected":"1","passed":true},{"actual":"-3","check":"negative divisor below half","expected":"1","passed":false},{"actual":"-1","check":"negative divisor","expected":"-1","passed":true},{"actual":"-0","check":"negative exact","expected":"-0","passed":true},{"actual":"0","check":"positive exact","expected":"0","passed":true},{"actual":"domain","check":"zero divisor","expected":"domain","passed":true},{"actual":"-5e+307","check":"huge finite","expected":"-5e+307","passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"even tie\", \"actual\": \"2\", \"expected\": \"2\", \"passed\": true}, {\"check\": \"odd tie\", \"actual\": \"-2\", \"expected\": \"-2\", \"passed\": true}, {\"check\": \"negative even tie\", \"actual\": \"-2\", \"expected\": \"-2\", \"passed\": true}, {\"check\": \"negative odd tie\", \"actual\": \"2\", \"expected\": \"2\", \"passed\": true}, {\"check\": \"above half\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"below half\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"negative divisor below half\", \"actual\": \"-3\", \"expected\": \"1\", \"passed\": false}, {\"check\": \"negative divisor\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"negative exact\", \"actual\": \"-0\", \"expected\": \"-0\", \"passed\": true}, {\"check\": \"positive exact\", \"actual\": \"0\", \"expected\": \"0\", \"passed\": true}, {\"check\": \"zero divisor\", \"actual\": \"domain\", \"expected\": \"domain\", \"passed\": true}, {\"check\": \"huge finite\", \"actual\": \"-5e+307\", \"expected\": \"-5e+307\", \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":42.338,"exit_code":0,"observations":[{"actual":"2","check":"even tie","expected":"2","passed":true},{"actual":"-2","check":"odd tie","expected":"-2","passed":true},{"actual":"-2","check":"negative even tie","expected":"-2","passed":true},{"actual":"2","check":"negative odd tie","expected":"2","passed":true},{"actual":"-1","check":"above half","expected":"-1","passed":true},{"actual":"1","check":"below half","expected":"1","passed":true},{"actual":"1","check":"negative divisor below half","expected":"1","passed":true},{"actual":"-1","check":"negative divisor","expected":"-1","passed":true},{"actual":"-0","check":"negative exact","expected":"-0","passed":true},{"actual":"0","check":"positive exact","expected":"0","passed":true},{"actual":"domain","check":"zero divisor","expected":"domain","passed":true},{"actual":"-5e+307","check":"huge finite","expected":"-5e+307","passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"even tie\", \"actual\": \"2\", \"expected\": \"2\", \"passed\": true}, {\"check\": \"odd tie\", \"actual\": \"-2\", \"expected\": \"-2\", \"passed\": true}, {\"check\": \"negative even tie\", \"actual\": \"-2\", \"expected\": \"-2\", \"passed\": true}, {\"check\": \"negative odd tie\", \"actual\": \"2\", \"expected\": \"2\", \"passed\": true}, {\"check\": \"above half\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"below half\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"negative divisor below half\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"negative divisor\", \"actual\": \"-1\", \"expected\": \"-1\", \"passed\": true}, {\"check\": \"negative exact\", \"actual\": \"-0\", \"expected\": \"-0\", \"passed\": true}, {\"check\": \"positive exact\", \"actual\": \"0\", \"expected\": \"0\", \"passed\": true}, {\"check\": \"zero divisor\", \"actual\": \"domain\", \"expected\": \"domain\", \"passed\": true}, {\"check\": \"huge finite\", \"actual\": \"-5e+307\", \"expected\": \"-5e+307\", \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}