FA-11466 / Compiler transformation correctness / Open access
Division strength reduction rounds negative dividends downward · case 01
Division strength reduction rounds negative dividends downward.
ROOT CAUSE
Signed truncating division by a power of two is replaced by arithmetic shift.
VERIFIED REPAIR
Bias negative dividends before arithmetic shifting to preserve truncation toward zero.
Unsuccessful approach: Adding a bias to every dividend corrupts positive nonmultiples.
Case contract
Lower signed mathematical integer division by 2**shift, shift>=0, returning truncation toward zero. No finite-width overflow is modeled.
Why this case matters
A deterministic miniature compiler-pass model; inputs are explicit IR facts, not a production compiler.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(value, shift):
return value >> shift
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('negative nonmultiple', solve(-(2**N+1),N), -1)
check('positive nonmultiple', solve(2**N+1,N), 1)
check('negative exact', solve(-2**N,N), -1)
check('positive exact', solve(2**N,N), 1)
check('zero', solve(0,N), 0)
check('identity shift', solve(-N,0), -N)
check('small negative', solve(-1,N), 0)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| negative nonmultiple | -2 | -1 | Failed |
| positive nonmultiple | 1 | 1 | Passed |
| negative exact | -1 | -1 | Passed |
| positive exact | 1 | 1 | Passed |
| zero | 0 | 0 | Passed |
| identity shift | -1 | -1 | Passed |
| small negative | -1 | 0 | Failed |
SHA-256 / 546e69a352f42e2a86cdea85a3f41f4f19b8e58ca9ee9e813b5f025d68fd47ad
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(value, shift):
return (value + (1 << shift) - 1) >> shift
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('negative nonmultiple', solve(-(2**N+1),N), -1)
check('positive nonmultiple', solve(2**N+1,N), 1)
check('negative exact', solve(-2**N,N), -1)
check('positive exact', solve(2**N,N), 1)
check('zero', solve(0,N), 0)
check('identity shift', solve(-N,0), -N)
check('small negative', solve(-1,N), 0)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| negative nonmultiple | -1 | -1 | Passed |
| positive nonmultiple | 2 | 1 | Failed |
| negative exact | -1 | -1 | Passed |
| positive exact | 1 | 1 | Passed |
| zero | 0 | 0 | Passed |
| identity shift | -1 | -1 | Passed |
| small negative | 0 | 0 | Passed |
SHA-256 / bbbd376cbb180f1a62d2a4bfbb61d45b9759cc3e1857271d8d751d01a5b3a423
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(value, shift):
return (value + ((1 << shift) - 1 if value < 0 else 0)) >> shift
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('negative nonmultiple', solve(-(2**N+1),N), -1)
check('positive nonmultiple', solve(2**N+1,N), 1)
check('negative exact', solve(-2**N,N), -1)
check('positive exact', solve(2**N,N), 1)
check('zero', solve(0,N), 0)
check('identity shift', solve(-N,0), -N)
check('small negative', solve(-1,N), 0)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| negative nonmultiple | -1 | -1 | Passed |
| positive nonmultiple | 1 | 1 | Passed |
| negative exact | -1 | -1 | Passed |
| positive exact | 1 | 1 | Passed |
| zero | 0 | 0 | Passed |
| identity shift | -1 | -1 | Passed |
| small negative | 0 | 0 | Passed |
SHA-256 / 42913d6074f5a590d2c971c8bb7ff10282939e6cd7493bb6ba756e8bb097e65c
Verification & scope
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.
Observations recorded using Python 3.12.14 at 2026-09-29T14:38:48.112340+00:00.
Case digest / ddf302cfc1296cb74c083c30e87afc70aaf99e70c1c8d86d703ca823e42031e0