FA-16631 / Floating-point arithmetic / Open access

Exact ratio conversion removes factors of two from odd mantissas · case 01

Exact ratio conversion removes factors of two from odd mantissas.

Verified by executionVariant 1 · 11 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

Exact ratio conversion removes factors of two from odd mantissas. The faulty expression is while power<0 and mantissa>1:.

VERIFIED REPAIR

Apply the contract at this fault site using while power<0 and mantissa%2==0:.

Unsuccessful approach: The attempted local correction while power<0 and mantissa%2==1: still violates the explicit regression fixtures.

Case 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.

Why this case matters

An offline floating representation model isolates a reproducible arithmetic fault.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(bits):
    sign=-1 if bits>>63 else 1
    e=(bits>>52)&2047
    f=bits&((1<<52)-1)
    if e==2047: return None
    if e:
        mantissa=f|(1<<52)
        power=e-1023-52
    else:
        mantissa=f
        power=-1074
    if mantissa==0: return [0,1]
    while power<0 and mantissa>1:
        mantissa//=2
        power+=1
    if power>=0: return [sign*(mantissa<<power),1]
    return [sign*mantissa,1<<(-power)]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])
check('positive integer', solve((1023+N)<<52), [1<<N,1])
check('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])
check('fraction', solve(0x3fe0000000000000), [1,2])
check('nontrivial fraction', solve(0x3fe8000000000000), [3,4])
check('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))
check('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))
check('zero', solve(0), [0,1])
check('negative zero', solve(1<<63), [0,1])
check('infinity', solve(0x7ff0000000000000), None)
check('nan', solve(0x7ff8000000000000|N), None)
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
large integer	`[2305843009213693952, 1]`	`[2305843009213693952, 1]`	Passed
positive integer	`[2, 1]`	`[2, 1]`	Passed
negative integer	`[-2, 1]`	`[-2, 1]`	Passed
fraction	`[1, 2]`	`[1, 2]`	Passed
nontrivial fraction	`[1, 2]`	`[3, 4]`	Failed
minimum subnormal	`[1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	`[1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Passed
negative subnormal	`[-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	`[-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Passed
zero	`[0, 1]`	`[0, 1]`	Passed
negative zero	`[0, 1]`	`[0, 1]`	Passed
infinity	`None`	`None`	Passed
nan	`None`	`None`	Passed

SHA-256 / c1b8cb6133e649469c58a06236041f5eccf6881d558896470ba8b8f0c72fe99a

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(bits):
    sign=-1 if bits>>63 else 1
    e=(bits>>52)&2047
    f=bits&((1<<52)-1)
    if e==2047: return None
    if e:
        mantissa=f|(1<<52)
        power=e-1023-52
    else:
        mantissa=f
        power=-1074
    if mantissa==0: return [0,1]
    while power<0 and mantissa%2==1:
        mantissa//=2
        power+=1
    if power>=0: return [sign*(mantissa<<power),1]
    return [sign*mantissa,1<<(-power)]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])
check('positive integer', solve((1023+N)<<52), [1<<N,1])
check('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])
check('fraction', solve(0x3fe0000000000000), [1,2])
check('nontrivial fraction', solve(0x3fe8000000000000), [3,4])
check('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))
check('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))
check('zero', solve(0), [0,1])
check('negative zero', solve(1<<63), [0,1])
check('infinity', solve(0x7ff0000000000000), None)
check('nan', solve(0x7ff8000000000000|N), None)
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
large integer	`[2305843009213693952, 1]`	`[2305843009213693952, 1]`	Passed
positive integer	`[4503599627370496, 2251799813685248]`	`[2, 1]`	Failed
negative integer	`[-4503599627370496, 2251799813685248]`	`[-2, 1]`	Failed
fraction	`[4503599627370496, 9007199254740992]`	`[1, 2]`	Failed
nontrivial fraction	`[6755399441055744, 9007199254740992]`	`[3, 4]`	Failed
minimum subnormal	`[0, 101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392]`	`[1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Failed
negative subnormal	`[0, 101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392]`	`[-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Failed
zero	`[0, 1]`	`[0, 1]`	Passed
negative zero	`[0, 1]`	`[0, 1]`	Passed
infinity	`None`	`None`	Passed
nan	`None`	`None`	Passed

SHA-256 / fe32d2ae4234a008c8c09cd6725a1c82777a4e974c2e7a83c9f8797a22ed4c42

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(bits):
    sign=-1 if bits>>63 else 1
    e=(bits>>52)&2047
    f=bits&((1<<52)-1)
    if e==2047: return None
    if e:
        mantissa=f|(1<<52)
        power=e-1023-52
    else:
        mantissa=f
        power=-1074
    if mantissa==0: return [0,1]
    while power<0 and mantissa%2==0:
        mantissa//=2
        power+=1
    if power>=0: return [sign*(mantissa<<power),1]
    return [sign*mantissa,1<<(-power)]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('large integer', solve((1023+60+N)<<52), [1<<(60+N),1])
check('positive integer', solve((1023+N)<<52), [1<<N,1])
check('negative integer', solve((1<<63)|((1023+N)<<52)), [-(1<<N),1])
check('fraction', solve(0x3fe0000000000000), [1,2])
check('nontrivial fraction', solve(0x3fe8000000000000), [3,4])
check('minimum subnormal', solve(N), list(math.ldexp(float(N),-1074).as_integer_ratio()))
check('negative subnormal', solve((1<<63)|N), list((-math.ldexp(float(N),-1074)).as_integer_ratio()))
check('zero', solve(0), [0,1])
check('negative zero', solve(1<<63), [0,1])
check('infinity', solve(0x7ff0000000000000), None)
check('nan', solve(0x7ff8000000000000|N), None)
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
large integer	`[2305843009213693952, 1]`	`[2305843009213693952, 1]`	Passed
positive integer	`[2, 1]`	`[2, 1]`	Passed
negative integer	`[-2, 1]`	`[-2, 1]`	Passed
fraction	`[1, 2]`	`[1, 2]`	Passed
nontrivial fraction	`[3, 4]`	`[3, 4]`	Passed
minimum subnormal	`[1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	`[1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Passed
negative subnormal	`[-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	`[-1, 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784]`	Passed
zero	`[0, 1]`	`[0, 1]`	Passed
negative zero	`[0, 1]`	`[0, 1]`	Passed
infinity	`None`	`None`	Passed
nan	`None`	`None`	Passed

SHA-256 / 232c5cccac878943ca1770bff8d7a21afb5af3860d3181aefa1b46f6590a6293

Verification & scope

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.

Observations recorded using Python 3.12.14 at 2026-09-29T14:39:38.069822+00:00.

Case digest / da9a3fcfc69c58c6880dd1514d187eb5e525e9238d9cd7c6d0bf8ad064cda017